Public Member Functions | |
Context () throws Z3Exception | |
Context (Map< String, String > settings) throws Z3Exception | |
IntSymbol | mkSymbol (int i) throws Z3Exception |
StringSymbol | mkSymbol (String name) throws Z3Exception |
BoolSort | getBoolSort () throws Z3Exception |
IntSort | getIntSort () throws Z3Exception |
RealSort | getRealSort () throws Z3Exception |
BoolSort | mkBoolSort () throws Z3Exception |
UninterpretedSort | mkUninterpretedSort (Symbol s) throws Z3Exception |
UninterpretedSort | mkUninterpretedSort (String str) throws Z3Exception |
IntSort | mkIntSort () throws Z3Exception |
RealSort | mkRealSort () throws Z3Exception |
BitVecSort | mkBitVecSort (int size) throws Z3Exception |
ArraySort | mkArraySort (Sort domain, Sort range) throws Z3Exception |
TupleSort | mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts) throws Z3Exception |
EnumSort | mkEnumSort (Symbol name, Symbol...enumNames) throws Z3Exception |
EnumSort | mkEnumSort (String name, String...enumNames) throws Z3Exception |
ListSort | mkListSort (Symbol name, Sort elemSort) throws Z3Exception |
ListSort | mkListSort (String name, Sort elemSort) throws Z3Exception |
FiniteDomainSort | mkFiniteDomainSort (Symbol name, long size) throws Z3Exception |
FiniteDomainSort | mkFiniteDomainSort (String name, long size) throws Z3Exception |
Constructor | mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception |
Constructor | mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception |
DatatypeSort | mkDatatypeSort (Symbol name, Constructor[] constructors) throws Z3Exception |
DatatypeSort | mkDatatypeSort (String name, Constructor[] constructors) throws Z3Exception |
DatatypeSort[] | mkDatatypeSorts (Symbol[] names, Constructor[][] c) throws Z3Exception |
DatatypeSort[] | mkDatatypeSorts (String[] names, Constructor[][] c) throws Z3Exception |
FuncDecl | mkFuncDecl (Symbol name, Sort[] domain, Sort range) throws Z3Exception |
FuncDecl | mkFuncDecl (Symbol name, Sort domain, Sort range) throws Z3Exception |
FuncDecl | mkFuncDecl (String name, Sort[] domain, Sort range) throws Z3Exception |
FuncDecl | mkFuncDecl (String name, Sort domain, Sort range) throws Z3Exception |
FuncDecl | mkFreshFuncDecl (String prefix, Sort[] domain, Sort range) throws Z3Exception |
FuncDecl | mkConstDecl (Symbol name, Sort range) throws Z3Exception |
FuncDecl | mkConstDecl (String name, Sort range) throws Z3Exception |
FuncDecl | mkFreshConstDecl (String prefix, Sort range) throws Z3Exception |
Expr | mkBound (int index, Sort ty) throws Z3Exception |
Pattern | mkPattern (Expr...terms) throws Z3Exception |
Expr | mkConst (Symbol name, Sort range) throws Z3Exception |
Expr | mkConst (String name, Sort range) throws Z3Exception |
Expr | mkFreshConst (String prefix, Sort range) throws Z3Exception |
Expr | mkConst (FuncDecl f) throws Z3Exception |
BoolExpr | mkBoolConst (Symbol name) throws Z3Exception |
BoolExpr | mkBoolConst (String name) throws Z3Exception |
IntExpr | mkIntConst (Symbol name) throws Z3Exception |
IntExpr | mkIntConst (String name) throws Z3Exception |
RealExpr | mkRealConst (Symbol name) throws Z3Exception |
RealExpr | mkRealConst (String name) throws Z3Exception |
BitVecExpr | mkBVConst (Symbol name, int size) throws Z3Exception |
BitVecExpr | mkBVConst (String name, int size) throws Z3Exception |
Expr | mkApp (FuncDecl f, Expr...args) throws Z3Exception |
BoolExpr | mkTrue () throws Z3Exception |
BoolExpr | mkFalse () throws Z3Exception |
BoolExpr | mkBool (boolean value) throws Z3Exception |
BoolExpr | mkEq (Expr x, Expr y) throws Z3Exception |
BoolExpr | mkDistinct (Expr...args) throws Z3Exception |
BoolExpr | mkNot (BoolExpr a) throws Z3Exception |
Expr | mkITE (BoolExpr t1, Expr t2, Expr t3) throws Z3Exception |
BoolExpr | mkIff (BoolExpr t1, BoolExpr t2) throws Z3Exception |
BoolExpr | mkImplies (BoolExpr t1, BoolExpr t2) throws Z3Exception |
BoolExpr | mkXor (BoolExpr t1, BoolExpr t2) throws Z3Exception |
BoolExpr | mkAnd (BoolExpr...t) throws Z3Exception |
BoolExpr | mkOr (BoolExpr...t) throws Z3Exception |
ArithExpr | mkAdd (ArithExpr...t) throws Z3Exception |
ArithExpr | mkMul (ArithExpr...t) throws Z3Exception |
ArithExpr | mkSub (ArithExpr...t) throws Z3Exception |
ArithExpr | mkUnaryMinus (ArithExpr t) throws Z3Exception |
ArithExpr | mkDiv (ArithExpr t1, ArithExpr t2) throws Z3Exception |
IntExpr | mkMod (IntExpr t1, IntExpr t2) throws Z3Exception |
IntExpr | mkRem (IntExpr t1, IntExpr t2) throws Z3Exception |
ArithExpr | mkPower (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkLt (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkLe (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkGt (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkGe (ArithExpr t1, ArithExpr t2) throws Z3Exception |
RealExpr | mkInt2Real (IntExpr t) throws Z3Exception |
IntExpr | mkReal2Int (RealExpr t) throws Z3Exception |
BoolExpr | mkIsInteger (RealExpr t) throws Z3Exception |
BitVecExpr | mkBVNot (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRedAND (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRedOR (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVAND (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVXOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVNAND (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVNOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVXNOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVNeg (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVAdd (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSub (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVMul (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVUDiv (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSDiv (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVURem (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSRem (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSMod (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVULT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSLT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVULE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSLE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVUGE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSGE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVUGT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSGT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkConcat (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkExtract (int high, int low, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkSignExt (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkZeroExt (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkRepeat (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVSHL (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVLSHR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVASHR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVRotateLeft (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRotateRight (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVRotateRight (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkInt2BV (int n, IntExpr t) throws Z3Exception |
IntExpr | mkBV2Int (BitVecExpr t, boolean signed) throws Z3Exception |
BoolExpr | mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception |
BoolExpr | mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception |
BoolExpr | mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVNegNoOverflow (BitVecExpr t) throws Z3Exception |
BoolExpr | mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception |
BoolExpr | mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
ArrayExpr | mkArrayConst (Symbol name, Sort domain, Sort range) throws Z3Exception |
ArrayExpr | mkArrayConst (String name, Sort domain, Sort range) throws Z3Exception |
Expr | mkSelect (ArrayExpr a, Expr i) throws Z3Exception |
ArrayExpr | mkStore (ArrayExpr a, Expr i, Expr v) throws Z3Exception |
ArrayExpr | mkConstArray (Sort domain, Expr v) throws Z3Exception |
ArrayExpr | mkMap (FuncDecl f, ArrayExpr...args) throws Z3Exception |
Expr | mkTermArray (ArrayExpr array) throws Z3Exception |
SetSort | mkSetSort (Sort ty) throws Z3Exception |
Expr | mkEmptySet (Sort domain) throws Z3Exception |
Expr | mkFullSet (Sort domain) throws Z3Exception |
Expr | mkSetAdd (Expr set, Expr element) throws Z3Exception |
Expr | mkSetDel (Expr set, Expr element) throws Z3Exception |
Expr | mkSetUnion (Expr...args) throws Z3Exception |
Expr | mkSetIntersection (Expr...args) throws Z3Exception |
Expr | mkSetDifference (Expr arg1, Expr arg2) throws Z3Exception |
Expr | mkSetComplement (Expr arg) throws Z3Exception |
Expr | mkSetMembership (Expr elem, Expr set) throws Z3Exception |
Expr | mkSetSubset (Expr arg1, Expr arg2) throws Z3Exception |
Expr | mkNumeral (String v, Sort ty) throws Z3Exception |
Expr | mkNumeral (int v, Sort ty) throws Z3Exception |
Expr | mkNumeral (long v, Sort ty) throws Z3Exception |
RatNum | mkReal (int num, int den) throws Z3Exception |
RatNum | mkReal (String v) throws Z3Exception |
RatNum | mkReal (int v) throws Z3Exception |
RatNum | mkReal (long v) throws Z3Exception |
IntNum | mkInt (String v) throws Z3Exception |
IntNum | mkInt (int v) throws Z3Exception |
IntNum | mkInt (long v) throws Z3Exception |
BitVecNum | mkBV (String v, int size) throws Z3Exception |
BitVecNum | mkBV (int v, int size) throws Z3Exception |
BitVecNum | mkBV (long v, int size) throws Z3Exception |
Quantifier | mkForall (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkForall (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkExists (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkExists (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkQuantifier (boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
void | setPrintMode (Z3_ast_print_mode value) throws Z3Exception |
String | benchmarkToSMTString (String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula) throws Z3Exception |
void | parseSMTLIBString (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
void | parseSMTLIBFile (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
int | getNumSMTLIBFormulas () throws Z3Exception |
BoolExpr[] | getSMTLIBFormulas () throws Z3Exception |
int | getNumSMTLIBAssumptions () throws Z3Exception |
BoolExpr[] | getSMTLIBAssumptions () throws Z3Exception |
int | getNumSMTLIBDecls () throws Z3Exception |
FuncDecl[] | getSMTLIBDecls () throws Z3Exception |
int | getNumSMTLIBSorts () throws Z3Exception |
Sort[] | getSMTLIBSorts () throws Z3Exception |
BoolExpr | parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
BoolExpr | parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
Goal | mkGoal (boolean models, boolean unsatCores, boolean proofs) throws Z3Exception |
Params | mkParams () throws Z3Exception |
int | getNumTactics () throws Z3Exception |
String[] | getTacticNames () throws Z3Exception |
String | getTacticDescription (String name) throws Z3Exception |
Tactic | mkTactic (String name) throws Z3Exception |
Tactic | andThen (Tactic t1, Tactic t2, Tactic...ts) throws Z3Exception |
Tactic | then (Tactic t1, Tactic t2, Tactic...ts) throws Z3Exception |
Tactic | orElse (Tactic t1, Tactic t2) throws Z3Exception |
Tactic | tryFor (Tactic t, int ms) throws Z3Exception |
Tactic | when (Probe p, Tactic t) throws Z3Exception |
Tactic | cond (Probe p, Tactic t1, Tactic t2) throws Z3Exception |
Tactic | repeat (Tactic t, int max) throws Z3Exception |
Tactic | skip () throws Z3Exception |
Tactic | fail () throws Z3Exception |
Tactic | failIf (Probe p) throws Z3Exception |
Tactic | failIfNotDecided () throws Z3Exception |
Tactic | usingParams (Tactic t, Params p) throws Z3Exception |
Tactic | with (Tactic t, Params p) throws Z3Exception |
Tactic | parOr (Tactic...t) throws Z3Exception |
Tactic | parAndThen (Tactic t1, Tactic t2) throws Z3Exception |
void | interrupt () throws Z3Exception |
int | getNumProbes () throws Z3Exception |
String[] | getProbeNames () throws Z3Exception |
String | getProbeDescription (String name) throws Z3Exception |
Probe | mkProbe (String name) throws Z3Exception |
Probe | constProbe (double val) throws Z3Exception |
Probe | lt (Probe p1, Probe p2) throws Z3Exception |
Probe | gt (Probe p1, Probe p2) throws Z3Exception |
Probe | le (Probe p1, Probe p2) throws Z3Exception |
Probe | ge (Probe p1, Probe p2) throws Z3Exception |
Probe | eq (Probe p1, Probe p2) throws Z3Exception |
Probe | and (Probe p1, Probe p2) throws Z3Exception |
Probe | or (Probe p1, Probe p2) throws Z3Exception |
Probe | not (Probe p) throws Z3Exception |
Solver | mkSolver () throws Z3Exception |
Solver | mkSolver (Symbol logic) throws Z3Exception |
Solver | mkSolver (String logic) throws Z3Exception |
Solver | mkSimpleSolver () throws Z3Exception |
Solver | mkSolver (Tactic t) throws Z3Exception |
Fixedpoint | mkFixedpoint () throws Z3Exception |
AST | wrapAST (long nativeObject) throws Z3Exception |
long | unwrapAST (AST a) |
String | SimplifyHelp () throws Z3Exception |
ParamDescrs | getSimplifyParameterDescriptions () throws Z3Exception |
void | updateParamValue (String id, String value) throws Z3Exception |
void | dispose () |
![]() | |
void | dispose () throws Z3Exception |
Static Public Member Functions | |
static void | ToggleWarningMessages (boolean enabled) throws Z3Exception |
Protected Member Functions | |
void | finalize () |
Protected Attributes | |
long | m_refCount = 0 |
The main interaction with Z3 happens via the Context.
Definition at line 27 of file Context.java.
|
inline |
Definition at line 32 of file Context.java.
|
inline |
The following parameters can be set:
Definition at line 57 of file Context.java.
|
inline |
Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".
Definition at line 2758 of file Context.java.
|
inline |
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .
Definition at line 2440 of file Context.java.
Referenced by Context.then().
|
inline |
Convert a benchmark into an SMT-LIB formatted string.
name | Name of the benchmark. The argument is optional. |
logic | The benchmark logic. |
status | The status string (sat, unsat, or unknown) |
attributes | Other attributes, such as source, difficulty or category. |
assumptions | Auxiliary assumptions. |
formula | Formula to be checked for consistency in conjunction with assumptions. |
Definition at line 2177 of file Context.java.
|
inline |
Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise.
Definition at line 2523 of file Context.java.
|
inline |
Create a probe that always evaluates to val .
Definition at line 2681 of file Context.java.
|
inline |
Disposes of the context.
Definition at line 3070 of file Context.java.
Referenced by Context.finalize().
|
inline |
Create a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2
Definition at line 2746 of file Context.java.
Referenced by SortRef.cast(), and BoolSortRef.cast().
|
inline |
Create a tactic always fails.
Definition at line 2558 of file Context.java.
|
inline |
Create a tactic that fails if the probe p evaluates to false.
Definition at line 2568 of file Context.java.
|
inline |
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false').
Definition at line 2580 of file Context.java.
|
inlineprotected |
|
inline |
Create a probe that evaluates to "true" when the value returned by p1 is greater than or equal the value returned by p2
Definition at line 2733 of file Context.java.
|
inline |
Retrieves the Boolean sort of the context.
Definition at line 106 of file Context.java.
Referenced by Context.mkBoolConst().
|
inline |
Retrieves the Integer sort of the context.
Definition at line 116 of file Context.java.
Referenced by Context.mkInt(), and Context.mkIntConst().
|
inline |
The number of supported Probes.
Definition at line 2643 of file Context.java.
Referenced by Context.getProbeNames().
|
inline |
The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2259 of file Context.java.
Referenced by Context.getSMTLIBAssumptions().
|
inline |
The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2283 of file Context.java.
Referenced by Context.getSMTLIBDecls().
|
inline |
The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2235 of file Context.java.
Referenced by Context.getSMTLIBFormulas().
|
inline |
The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2306 of file Context.java.
Referenced by Context.getSMTLIBSorts().
|
inline |
The number of supported tactics.
Definition at line 2399 of file Context.java.
Referenced by Context.getTacticNames().
|
inline |
Returns a string containing a description of the probe with the given name.
Definition at line 2665 of file Context.java.
|
inline |
|
inline |
Retrieves the Real sort of the context.
Definition at line 126 of file Context.java.
Referenced by Context.mkReal(), and Context.mkRealConst().
|
inline |
Retrieves parameter descriptions for simplifier.
Definition at line 2897 of file Context.java.
|
inline |
The assumptions parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2268 of file Context.java.
|
inline |
The declarations parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2292 of file Context.java.
|
inline |
The formulas parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2244 of file Context.java.
|
inline |
The declarations parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2315 of file Context.java.
|
inline |
Returns a string containing a description of the tactic with the given name.
Definition at line 2421 of file Context.java.
|
inline |
|
inline |
Create a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2
Definition at line 2705 of file Context.java.
|
inline |
Interrupt the execution of a Z3 procedure.
This procedure can be used to interrupt: solvers, simplifiers and tactics.
Definition at line 2635 of file Context.java.
|
inline |
Create a probe that evaluates to "true" when the value returned by p1 is less than or equal the value returned by p2
Definition at line 2719 of file Context.java.
|
inline |
Create a probe that evaluates to "true" when the value returned by p1 is less than the value returned by p2
Definition at line 2691 of file Context.java.
|
inline |
Create an expression representing t[0] + t[1] + ...
.
Definition at line 763 of file Context.java.
|
inline |
Create an expression representing t[0] and t[1] and ...
.
Definition at line 741 of file Context.java.
|
inline |
Create a new function application.
Definition at line 624 of file Context.java.
Referenced by EnumSort.getConsts(), ListSort.getNil(), and Context.mkConst().
|
inline |
Create an array constant.
Definition at line 1633 of file Context.java.
|
inline |
Create an array constant.
Definition at line 1643 of file Context.java.
|
inline |
Create a new array sort.
Definition at line 191 of file Context.java.
Referenced by Context.mkArrayConst().
|
inline |
Create a new bit-vector sort.
Definition at line 182 of file Context.java.
Referenced by Context.mkBV(), and Context.mkBVConst().
|
inline |
|
inline |
|
inline |
|
inline |
Create a new Boolean sort.
Definition at line 136 of file Context.java.
|
inline |
Creates a new bound variable.
index | The de-Bruijn index of the variable |
ty | The sort of the variable |
Definition at line 482 of file Context.java.
|
inline |
Create a bit-vector numeral.
v | A string representing the value in decimal notation. |
size | the size of the bit-vector |
Definition at line 2025 of file Context.java.
|
inline |
Create a bit-vector numeral.
v | value of the numeral. |
size | the size of the bit-vector |
Definition at line 2035 of file Context.java.
|
inline |
Create a bit-vector numeral.
v | value of the numeral. |
*
size | the size of the bit-vector |
Definition at line 2045 of file Context.java.
|
inline |
Create an integer from the bit-vector argument t .
If is_signed
is false, then the bit-vector t1
is treated as unsigned. So the result is non-negative and in the range
, where N are the number of bits in t . If is_signed
is true, t1
is treated as a signed bit-vector.
NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.
The argument must be of bit-vector sort.
Definition at line 1509 of file Context.java.
|
inline |
Two's complement addition.
The arguments must have the same bit-vector sort.
Definition at line 1071 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise addition does not overflow.
The arguments must be of bit-vector sort.
Definition at line 1521 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise addition does not underflow.
The arguments must be of bit-vector sort.
Definition at line 1536 of file Context.java.
|
inline |
Bitwise conjunction.
The arguments must have a bit-vector sort.
Definition at line 982 of file Context.java.
|
inline |
Arithmetic shift right
It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1416 of file Context.java.
|
inline |
|
inline |
|
inline |
Logical shift right
It is equivalent to unsigned division by
where x
is the value of t2 .
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1396 of file Context.java.
|
inline |
Two's complement multiplication.
The arguments must have the same bit-vector sort.
Definition at line 1097 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise multiplication does not overflow.
The arguments must be of bit-vector sort.
Definition at line 1605 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise multiplication does not underflow.
The arguments must be of bit-vector sort.
Definition at line 1620 of file Context.java.
|
inline |
Bitwise NAND.
The arguments must have a bit-vector sort.
Definition at line 1021 of file Context.java.
|
inline |
Standard two's complement unary minus.
The arguments must have a bit-vector sort.
Definition at line 1060 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise negation does not overflow.
The arguments must be of bit-vector sort.
Definition at line 1593 of file Context.java.
|
inline |
Bitwise NOR.
The arguments must have a bit-vector sort.
Definition at line 1034 of file Context.java.
|
inline |
Bitwise negation.
The argument must have a bit-vector sort.
Definition at line 947 of file Context.java.
|
inline |
Bitwise disjunction.
The arguments must have a bit-vector sort.
Definition at line 995 of file Context.java.
|
inline |
Take conjunction of bits in a vector, return vector of length 1.
The argument must have a bit-vector sort.
Definition at line 958 of file Context.java.
|
inline |
Take disjunction of bits in a vector, return vector of length 1.
The argument must have a bit-vector sort.
Definition at line 970 of file Context.java.
|
inline |
Rotate Left.
Rotate bits of t
to the left i
times. The argument t must have a bit-vector sort.
Definition at line 1429 of file Context.java.
|
inline |
Rotate Left.
Rotate bits of t1 to the left t2 times. The arguments must have the same bit-vector sort.
Definition at line 1454 of file Context.java.
|
inline |
Rotate Right.
Rotate bits of t
to the right i
times. The argument t must have a bit-vector sort.
Definition at line 1441 of file Context.java.
|
inline |
Rotate Right.
Rotate bits of t1 to the rightt2 times. The arguments must have the same bit-vector sort.
Definition at line 1469 of file Context.java.
|
inline |
Signed division.
It is defined in the following way:
floor
of t2
is different from zero, and ceiling
of t2
is different from zero, and If
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1133 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise signed division does not overflow.
The arguments must be of bit-vector sort.
Definition at line 1579 of file Context.java.
|
inline |
Two's complement signed greater than or equal to.
The arguments must have the same bit-vector sort.
Definition at line 1258 of file Context.java.
|
inline |
Two's complement signed greater-than.
The arguments must have the same bit-vector sort.
Definition at line 1284 of file Context.java.
|
inline |
Shift left.
It is equivalent to multiplication by
where x
is the value of t2 .
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1377 of file Context.java.
|
inline |
Two's complement signed less-than or equal to.
The arguments must have the same bit-vector sort.
Definition at line 1232 of file Context.java.
|
inline |
Two's complement signed less-than
The arguments must have the same bit-vector sort.
Definition at line 1206 of file Context.java.
|
inline |
Two's complement signed remainder (sign follows divisor).
If
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1180 of file Context.java.
|
inline |
Signed remainder.
It is defined as
, where
represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1
.
If
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1166 of file Context.java.
|
inline |
Two's complement subtraction.
The arguments must have the same bit-vector sort.
Definition at line 1084 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise subtraction does not overflow.
The arguments must be of bit-vector sort.
Definition at line 1550 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise subtraction does not underflow.
The arguments must be of bit-vector sort.
Definition at line 1564 of file Context.java.
|
inline |
Unsigned division.
It is defined as the floor of
if t2
is different from zero. If
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1112 of file Context.java.
|
inline |
Unsigned greater than or equal to.
The arguments must have the same bit-vector sort.
Definition at line 1245 of file Context.java.
|
inline |
Unsigned greater-than.
The arguments must have the same bit-vector sort.
Definition at line 1271 of file Context.java.
|
inline |
Unsigned less-than or equal to.
The arguments must have the same bit-vector sort.
Definition at line 1219 of file Context.java.
|
inline |
Unsigned less-than
The arguments must have the same bit-vector sort.
Definition at line 1193 of file Context.java.
|
inline |
Unsigned remainder.
It is defined as
, where
represents unsigned division. If
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1148 of file Context.java.
|
inline |
Bitwise XNOR.
The arguments must have a bit-vector sort.
Definition at line 1047 of file Context.java.
|
inline |
Bitwise XOR.
The arguments must have a bit-vector sort.
Definition at line 1008 of file Context.java.
|
inline |
Bit-vector concatenation.
The arguments must have a bit-vector sort.
Definition at line 1302 of file Context.java.
|
inline |
Creates a new Constant of sort range and named name .
Definition at line 505 of file Context.java.
Referenced by Context.mkArrayConst(), Context.mkBoolConst(), Context.mkBVConst(), Context.mkConst(), Context.mkIntConst(), and Context.mkRealConst().
|
inline |
|
inline |
Creates a fresh constant from the FuncDecl f .
f | A decl of a 0-arity function |
Definition at line 543 of file Context.java.
|
inline |
Create a constant array.
The resulting term is an array, such that a
on an arbitrary index produces the value
.
Definition at line 1699 of file Context.java.
|
inline |
Creates a new constant function declaration.
Definition at line 447 of file Context.java.
|
inline |
|
inline |
Create a datatype constructor.
name | constructor name |
recognizer | name of recognizer function. |
fieldNames | names of the constructor fields. |
sorts | field sorts, 0 if the field sort refers to a recursive sort. |
sortRefs | reference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared. |
Definition at line 287 of file Context.java.
|
inline |
Create a datatype constructor.
name | |
recognizer | |
fieldNames | |
sorts | |
sortRefs |
Definition at line 303 of file Context.java.
|
inline |
Create a new datatype sort.
Definition at line 315 of file Context.java.
|
inline |
|
inline |
Create mutually recursive datatypes.
names | names of datatype sorts |
c | list of constructors, one list per sort. |
Definition at line 340 of file Context.java.
Referenced by Context.mkDatatypeSorts().
|
inline |
Create mutually recursive data-types.
names | |
c |
Definition at line 371 of file Context.java.
|
inline |
Creates a distinct
term.
Definition at line 669 of file Context.java.
|
inline |
Create an expression representing t1 / t2
.
Definition at line 807 of file Context.java.
|
inline |
Create an empty set.
Definition at line 1753 of file Context.java.
|
inline |
|
inline |
|
inline |
Creates the equality x = y .
Definition at line 658 of file Context.java.
|
inline |
Create an existential Quantifier.
Definition at line 2095 of file Context.java.
Referenced by Context.mkQuantifier().
|
inline |
Create an existential Quantifier.
Definition at line 2107 of file Context.java.
|
inline |
Bit-vector extraction.
Extract the bits high down to low from a bitvector of size
to yield a new bitvector of size
, where
. The argument t must have a bit-vector sort.
Definition at line 1318 of file Context.java.
|
inline |
|
inline |
Create a new finite domain sort.
Definition at line 258 of file Context.java.
|
inline |
|
inline |
Create a Fixedpoint context.
Definition at line 2849 of file Context.java.
|
inline |
Create a universal Quantifier.
Creates a forall formula, where weight is the weight, patterns is an array of patterns, sorts is an array with the sorts of the bound variables, names is an array with the 'names' of the bound variables, and body is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation.
sorts | the sorts of the bound variables. |
names | names of the bound variables |
body | the body of the quantifier. |
weight | quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. |
patterns | array containing the patterns created using MkPattern
|
noPatterns | array containing the anti-patterns created using MkPattern
|
quantifierID | optional symbol to track quantifier. |
skolemID | optional symbol to track skolem constants. |
Definition at line 2070 of file Context.java.
Referenced by Context.mkQuantifier().
|
inline |
Create a universal Quantifier.
Definition at line 2082 of file Context.java.
|
inline |
Creates a fresh Constant of sort range and a name prefixed with prefix .
Definition at line 531 of file Context.java.
|
inline |
Creates a fresh constant function declaration with a name prefixed with prefix .
Definition at line 470 of file Context.java.
|
inline |
Creates a fresh function declaration with a name prefixed with prefix .
Definition at line 435 of file Context.java.
|
inline |
Create the full set.
Definition at line 1764 of file Context.java.
|
inline |
Creates a new function declaration.
Definition at line 381 of file Context.java.
|
inline |
Creates a new function declaration.
Definition at line 394 of file Context.java.
|
inline |
|
inline |
|
inline |
Create an expression representing t1 >= t2
Definition at line 895 of file Context.java.
|
inline |
Creates a new Goal.
Note that the Context must have been created with proof generation support if proofs is set to true here.
models | Indicates whether model generation should be enabled. |
unsatCores | Indicates whether unsat core generation should be enabled. |
proofs | Indicates whether proof generation should be enabled. |
Definition at line 2380 of file Context.java.
|
inline |
Create an expression representing t1 > t2
Definition at line 883 of file Context.java.
|
inline |
Create an expression representing t1 iff t2
.
Definition at line 705 of file Context.java.
|
inline |
Create an expression representing t1 -> t2
.
Definition at line 717 of file Context.java.
|
inline |
Create an integer numeral.
v | A string representing the Term value in decimal notation. |
Definition at line 1989 of file Context.java.
|
inline |
Create an integer numeral.
v | value of the numeral. |
Definition at line 2001 of file Context.java.
|
inline |
Create an integer numeral.
v | value of the numeral. |
Definition at line 2013 of file Context.java.
|
inline |
Create an n bit bit-vector from the integer argument t .
NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.
The argument must be of integer sort.
Definition at line 1487 of file Context.java.
|
inline |
Coerce an integer to a real.
There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
You can take the floor of a real by creating an auxiliary integer Term
and and asserting
. The argument must be of integer sort.
Definition at line 913 of file Context.java.
|
inline |
|
inline |
|
inline |
Create a new integer sort.
Definition at line 164 of file Context.java.
|
inline |
Creates an expression that checks whether a real number is an integer.
Definition at line 936 of file Context.java.
|
inline |
Create an expression representing an if-then-else: ite(t1, t2, t3)
.
t1 | An expression with Boolean sort |
t2 | An expression |
t3 | An expression with the same sort as t2 |
Definition at line 692 of file Context.java.
|
inline |
Create an expression representing t1 <= t2
Definition at line 871 of file Context.java.
|
inline |
Create a new list sort.
Definition at line 237 of file Context.java.
|
inline |
|
inline |
Create an expression representing t1 < t2
Definition at line 859 of file Context.java.
|
inline |
Maps f on the argument arrays.
Eeach element of
must be of an array sort
. The function declaration
must have type
.
must have sort range. The sort of the result is
.
Definition at line 1717 of file Context.java.
|
inline |
Create an expression representing t1 mod t2
.
The arguments must have int type.
Definition at line 820 of file Context.java.
|
inline |
Create an expression representing t[0] * t[1] * ...
.
Definition at line 774 of file Context.java.
|
inline |
Mk an expression representing not(a)
.
Definition at line 679 of file Context.java.
|
inline |
Create a Term of a given sort.
v | A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*
|
ty | The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size. |
Definition at line 1890 of file Context.java.
Referenced by Context.mkBV().
|
inline |
Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral
since it is not necessary to parse a string.
v | Value of the numeral |
ty | Sort of the numeral |
Definition at line 1908 of file Context.java.
|
inline |
Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral
since it is not necessary to parse a string.
v | Value of the numeral |
ty | Sort of the numeral |
Definition at line 1925 of file Context.java.
|
inline |
Create an expression representing t[0] or t[1] or ...
.
Definition at line 752 of file Context.java.
|
inline |
Creates a new ParameterSet.
Definition at line 2390 of file Context.java.
|
inline |
Create a quantifier pattern.
Definition at line 491 of file Context.java.
|
inline |
Create an expression representing t1 ^ t2
.
Definition at line 845 of file Context.java.
|
inline |
Creates a new Probe.
Definition at line 2673 of file Context.java.
|
inline |
Create a Quantifier.
Definition at line 2119 of file Context.java.
|
inline |
Create a Quantifier.
Definition at line 2136 of file Context.java.
|
inline |
Create a real from a fraction.
num | numerator of rational. |
den | denominator of rational. |
Definition at line 1940 of file Context.java.
|
inline |
Create a real numeral.
v | A string representing the Term value in decimal notation. |
Definition at line 1954 of file Context.java.
|
inline |
Create a real numeral.
v | value of the numeral. |
Definition at line 1966 of file Context.java.
|
inline |
Create a real numeral.
v | value of the numeral. |
Definition at line 1978 of file Context.java.
|
inline |
Coerce a real to an integer.
The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort.
Definition at line 926 of file Context.java.
|
inline |
|
inline |
|
inline |
Create a real sort.
Definition at line 173 of file Context.java.
|
inline |
Create an expression representing t1 rem t2
.
The arguments must have int type.
Definition at line 833 of file Context.java.
|
inline |
Bit-vector repetition.
The argument t must have a bit-vector sort.
Definition at line 1359 of file Context.java.
|
inline |
Array read.
The argument
is the array and
is the index of the array that gets read.
The node
must have an array sort
, and
must have the sort
. The sort of the result is
.
Definition at line 1659 of file Context.java.
|
inline |
Add an element to the set.
Definition at line 1775 of file Context.java.
|
inline |
Take the complement of a set.
Definition at line 1843 of file Context.java.
|
inline |
Remove an element from a set.
Definition at line 1789 of file Context.java.
|
inline |
Take the difference between two sets.
Definition at line 1829 of file Context.java.
|
inline |
Take the intersection of a list of sets.
Definition at line 1816 of file Context.java.
|
inline |
Check for set membership.
Definition at line 1854 of file Context.java.
|
inline |
Create a set type.
Definition at line 1743 of file Context.java.
|
inline |
Check for subsetness of sets.
Definition at line 1868 of file Context.java.
|
inline |
Take the union of a list of sets.
Definition at line 1803 of file Context.java.
|
inline |
Bit-vector sign extension.
Sign-extends the given bit-vector to the (signed) equivalent bitvector of size
, where m
is the size of the given bit-vector. The argument t must have a bit-vector sort.
Definition at line 1333 of file Context.java.
|
inline |
Creates a new (incremental) solver.
Definition at line 2828 of file Context.java.
|
inline |
Creates a new (incremental) solver.
This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.
Definition at line 2795 of file Context.java.
Referenced by Tactic.getSolver(), and Context.mkSolver().
|
inline |
Creates a new (incremental) solver.
This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.
Definition at line 2806 of file Context.java.
|
inline |
Creates a new (incremental) solver.
Definition at line 2819 of file Context.java.
|
inline |
Creates a solver that is implemented using the given tactic.
The solver supports the commands
and
, but it will always solve each check from scratch.
Definition at line 2839 of file Context.java.
|
inline |
Array update.
The node
must have an array sort
,
must have sort
,
must have sort range. The sort of the result is
. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to
(with respect to
) on all indices except for
, where it maps to
(and the
of
with respect to
may be a different value).
Definition at line 1683 of file Context.java.
|
inline |
Create an expression representing t[0] - t[1] - ...
.
Definition at line 785 of file Context.java.
|
inline |
Creates a new symbol using an integer.
Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.
Definition at line 73 of file Context.java.
Referenced by Params.add(), Context.mkArrayConst(), Context.mkBoolConst(), Context.mkConst(), Context.mkConstDecl(), Context.mkConstructor(), Context.mkDatatypeSort(), Context.mkEnumSort(), Context.mkFiniteDomainSort(), Context.mkFuncDecl(), Context.mkListSort(), Context.mkSolver(), and Context.mkUninterpretedSort().
|
inline |
Create a symbol using a string.
Definition at line 81 of file Context.java.
|
inline |
|
inline |
Access the array default value.
Produces the default range value, for arrays that can be represented as finite maps with a default range value.
Definition at line 1732 of file Context.java.
|
inline |
|
inline |
Create a new tuple sort.
Definition at line 202 of file Context.java.
|
inline |
Create an expression representing -t
.
Definition at line 796 of file Context.java.
|
inline |
Create a new uninterpreted sort.
Definition at line 145 of file Context.java.
Referenced by Context.mkUninterpretedSort().
|
inline |
Create a new uninterpreted sort.
Definition at line 155 of file Context.java.
|
inline |
Create an expression representing t1 xor t2
.
Definition at line 729 of file Context.java.
|
inline |
Bit-vector zero extension.
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size
, where m
is the size of the given bit-vector. The argument t must have a bit-vector sort.
Definition at line 1347 of file Context.java.
|
inline |
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
Definition at line 2782 of file Context.java.
|
inline |
Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".
Definition at line 2770 of file Context.java.
|
inline |
Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal.
Definition at line 2480 of file Context.java.
|
inline |
Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 . The subgoals are processed in parallel.
Definition at line 2622 of file Context.java.
|
inline |
Create a tactic that applies the given tactics in parallel.
Definition at line 2610 of file Context.java.
|
inline |
Parse the given file using the SMT-LIB2 parser.
Definition at line 2353 of file Context.java.
|
inline |
Parse the given string using the SMT-LIB2 parser.
Definition at line 2332 of file Context.java.
|
inline |
Parse the given file using the SMT-LIB parser.
Definition at line 2215 of file Context.java.
|
inline |
Parse the given string using the SMT-LIB parser.
The symbol table of the parser can be initialized using the given sorts and declarations. The symbols in the arrays sortNames and declNames don't need to match the names of the sorts and declarations in the arrays sorts and decls . This is a useful feature since we can use arbitrary names to reference sorts and declarations.
Definition at line 2196 of file Context.java.
|
inline |
Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.
Definition at line 2538 of file Context.java.
|
inline |
Selects the format used for pretty-printing expressions.
The default mode for pretty printing expressions is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.
Definition at line 2160 of file Context.java.
|
inline |
Return a string describing all available parameters to Expr.Simplify
.
Definition at line 2888 of file Context.java.
|
inline |
Create a tactic that just returns the given goal.
Definition at line 2549 of file Context.java.
|
inline |
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .
Shorthand for
.
Definition at line 2470 of file Context.java.
|
inlinestatic |
Enable/disable printing of warning messages to the console.
Note that this function is static and effects the behaviour of all contexts globally.
Definition at line 2907 of file Context.java.
|
inline |
Create a tactic that applies t to a goal for ms milliseconds.
If t does not terminate within ms milliseconds, then it fails.
Definition at line 2495 of file Context.java.
|
inline |
Unwraps an AST.
This function is used for transitions between native and managed objects. It returns the native pointer to the AST. Note that AST objects are reference counted and unwrapping an AST disables automatic reference counting, i.e., all references to the IntPtr that is returned must be handled externally and through native calls (see e.g.,
).
a | The AST to unwrap. |
Definition at line 2879 of file Context.java.
|
inline |
Update a mutable configuration parameter.
The list of all configuration parameters can be obtained using the Z3 executable:
Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.
Definition at line 2920 of file Context.java.
|
inline |
Create a tactic that applies t using the given set of parameters p .
Definition at line 2589 of file Context.java.
Referenced by Context.with().
|
inline |
Create a tactic that applies t to a given goal if the probe p evaluates to true.
If p evaluates to false, then the new tactic behaves like the
tactic.
Definition at line 2509 of file Context.java.
|
inline |
Create a tactic that applies t using the given set of parameters p .
Alias for
Definition at line 2602 of file Context.java.
|
inline |
Wraps an AST.
This function is used for transitions between native and managed objects. Note that nativeObject must be a native object obtained from Z3 (e.g., through
) and that it must have a correct reference count (see e.g., .
nativeObject | The native pointer to wrap. |
Definition at line 2864 of file Context.java.
|
protected |
Definition at line 3042 of file Context.java.
Referenced by Z3Object.dispose().