Index
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form
Q
- QF_ABV - Class in org.smtlib.logic
-
This logic does not allow quantifiers or uninterpreted functions
- QF_ABV(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_ABV
- QF_AUFBV - Class in org.smtlib.logic
-
This logic does not allow quantifiers; all array terms have sort (Array (_ BitVec i) (_ BitVec j))
- QF_AUFBV(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_AUFBV
- QF_AUFLIA - Class in org.smtlib.logic
- QF_AUFLIA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_AUFLIA
- QF_AX - Class in org.smtlib.logic
- QF_AX(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_AX
- QF_BV - Class in org.smtlib.logic
- QF_BV(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_BV
- QF_EIA - Class in org.smtlib.logic
- QF_EIA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_EIA
- QF_FP - Class in org.smtlib.logic
-
Not an official SMT-LIB logic -- see QF_FP.smt2's own :notes: a jSMTLIB-invented convenience logic for exercising the FloatingPoint theory in this project's own test suite without needing the broad ALL logic.
- QF_FP(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_FP
- QF_IDL - Class in org.smtlib.logic
-
QF_IDL atoms (QF_IDL.smt2): (op x y), (op (- x y) n) and (op (- x y) (- n)), with x, y free constants of sort Int and n a numeral.
- QF_IDL(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_IDL
- QF_LIA - Class in org.smtlib.logic
- QF_LIA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_LIA
- QF_LRA - Class in org.smtlib.logic
- QF_LRA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_LRA
- QF_NIA - Class in org.smtlib.logic
- QF_NIA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_NIA
- QF_NRA - Class in org.smtlib.logic
- QF_NRA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_NRA
- QF_RDL - Class in org.smtlib.logic
-
QF_RDL atoms (QF_RDL.smt2): (op x y), (op (- x y) c), (op (- (+ x ...
- QF_RDL(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_RDL
- QF_UF - Class in org.smtlib.logic
- QF_UF(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_UF
- QF_UFBV - Class in org.smtlib.logic
-
Quantifier-free, with uninterpreted functions and sorts permitted -- identical restrictions to QF_UF, all inherited from it (the bit-vector vs.
- QF_UFBV(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_UFBV
- QF_UFIDL - Class in org.smtlib.logic
- QF_UFIDL(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_UFIDL
- QF_UFLIA - Class in org.smtlib.logic
- QF_UFLIA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_UFLIA
- QF_UFLRA - Class in org.smtlib.logic
- QF_UFLRA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_UFLRA
- QF_UFNRA - Class in org.smtlib.logic
- QF_UFNRA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.QF_UFNRA
- qualifier - Variable in class org.smtlib.impl.SMTExpr.AsIdentifier
- qualifier() - Method in interface org.smtlib.IExpr.IAsIdentifier
-
The Sort qualifier
- qualifier() - Method in class org.smtlib.impl.SMTExpr.AsIdentifier
- quantifierBody - Variable in class org.smtlib.TypeChecker
-
The body of the innermost quantifier being checked (the only place a :pattern may appear), or null.
- quiet - Variable in class org.smtlib.Driver
-
If true, do not echo 'success' responses (unless verbose is enabled)
- quote(String) - Method in class org.smtlib.Utils
-
Quotes a string, adding enclosing quotes and putting in SMT-LIBv2 escapes as needed
- quotedString(String) - Method in interface org.smtlib.IExpr.IFactory
-
Creates an IStringLiteral from a string that is SMT-LIB escaped with enclosing quotes.
- quotedString(String) - Method in class org.smtlib.impl.Factory
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form