Uses of Interface
org.smtlib.IExpr.IExists
Packages that use IExpr.IExists
Package
Description
This package contains the main classes and abstract interfaces for this
SMT-LIB tool; the tool provides a stand-alone SMT-LIB-compliant command-line
application, an application that responds to SMT-LIB commands over a
network port, and an SMT-LIB Java API.
This package is an implementation of the interfaces defined in org.smtlib.
This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.
This package implements various instances of org.smtlib.ISolver, which are
specific solvers that wrap and interact with various off-the-shelf SMT solvers
currently available.
-
Uses of IExpr.IExists in org.smtlib
Methods in org.smtlib that return IExpr.IExistsModifier and TypeMethodDescriptionIExpr.IFactory.exists(List<IExpr.IDeclaration> params, IExpr e) Creates an Exists expression.Creates an Exists expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as:pattern (p).Methods in org.smtlib with parameters of type IExpr.IExistsModifier and TypeMethodDescriptionIVisitor.TreeVisitor.visit(IExpr.IExists e) IVisitor.visit(IExpr.IExists e) TypeChecker.visit(IExpr.IExists e) -
Uses of IExpr.IExists in org.smtlib.impl
Classes in org.smtlib.impl that implement IExpr.IExistsModifier and TypeClassDescriptionstatic classRepresents an SMT-LIB existential quantifier expression.Methods in org.smtlib.impl that return IExpr.IExists -
Uses of IExpr.IExists in org.smtlib.sexpr
Methods in org.smtlib.sexpr with parameters of type IExpr.IExists -
Uses of IExpr.IExists in org.smtlib.solvers
Methods in org.smtlib.solvers with parameters of type IExpr.IExistsModifier and TypeMethodDescriptionPrinter.visit(IExpr.IExists e) Solver_simplify.Translator.visit(IExpr.IExists e)