The InterpolationContext is suitable for generation of interpolants. More...
Public Member Functions | |
InterpolationContext () | |
Constructor. More... | |
InterpolationContext (Dictionary< string, string > settings) | |
Constructor. More... | |
BoolExpr | MkInterpolant (BoolExpr a) |
Create an expression that marks a formula position for interpolation. More... | |
BoolExpr[] | GetInterpolant (Expr pf, Expr pat, Params p) |
Computes an interpolant. More... | |
Z3_lbool | ComputeInterpolant (Expr pat, Params p, out BoolExpr[] interp, out Model model) |
Computes an interpolant. More... | |
string | InterpolationProfile () |
Return a string summarizing cumulative time used for interpolation. More... | |
int | CheckInterpolant (Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory) |
Checks the correctness of an interpolant. More... | |
int | ReadInterpolationProblem (string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory) |
Reads an interpolation problem from a file. More... | |
void | WriteInterpolationProblem (string filename, Expr[] cnsts, uint[] parents, Expr[] theory) |
Writes an interpolation problem to a file. More... | |
![]() | |
Context () | |
Constructor. More... | |
Context (Dictionary< string, string > settings) | |
Constructor. More... | |
IntSymbol | MkSymbol (int i) |
Creates a new symbol using an integer. More... | |
StringSymbol | MkSymbol (string name) |
Create a symbol using a string. More... | |
BoolSort | MkBoolSort () |
Create a new Boolean sort. More... | |
UninterpretedSort | MkUninterpretedSort (Symbol s) |
Create a new uninterpreted sort. More... | |
UninterpretedSort | MkUninterpretedSort (string str) |
Create a new uninterpreted sort. More... | |
IntSort | MkIntSort () |
Create a new integer sort. More... | |
RealSort | MkRealSort () |
Create a real sort. More... | |
BitVecSort | MkBitVecSort (uint size) |
Create a new bit-vector sort. More... | |
ArraySort | MkArraySort (Sort domain, Sort range) |
Create a new array sort. More... | |
TupleSort | MkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts) |
Create a new tuple sort. More... | |
EnumSort | MkEnumSort (Symbol name, params Symbol[] enumNames) |
Create a new enumeration sort. More... | |
EnumSort | MkEnumSort (string name, params string[] enumNames) |
Create a new enumeration sort. More... | |
ListSort | MkListSort (Symbol name, Sort elemSort) |
Create a new list sort. More... | |
ListSort | MkListSort (string name, Sort elemSort) |
Create a new list sort. More... | |
FiniteDomainSort | MkFiniteDomainSort (Symbol name, ulong size) |
Create a new finite domain sort. More... | |
FiniteDomainSort | MkFiniteDomainSort (string name, ulong size) |
Create a new finite domain sort. More... | |
Constructor | MkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null) |
Create a datatype constructor. More... | |
Constructor | MkConstructor (string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null) |
Create a datatype constructor. More... | |
DatatypeSort | MkDatatypeSort (Symbol name, Constructor[] constructors) |
Create a new datatype sort. More... | |
DatatypeSort | MkDatatypeSort (string name, Constructor[] constructors) |
Create a new datatype sort. More... | |
DatatypeSort[] | MkDatatypeSorts (Symbol[] names, Constructor[][] c) |
Create mutually recursive datatypes. More... | |
DatatypeSort[] | MkDatatypeSorts (string[] names, Constructor[][] c) |
Create mutually recursive data-types. More... | |
Expr | MkUpdateField (FuncDecl field, Expr t, Expr v) |
Update a datatype field at expression t with value v. The function performs a record update at t. The field that is passed in as argument is updated with value v, the remainig fields of t are unchanged. More... | |
FuncDecl | MkFuncDecl (Symbol name, Sort[] domain, Sort range) |
Creates a new function declaration. More... | |
FuncDecl | MkFuncDecl (Symbol name, Sort domain, Sort range) |
Creates a new function declaration. More... | |
FuncDecl | MkFuncDecl (string name, Sort[] domain, Sort range) |
Creates a new function declaration. More... | |
FuncDecl | MkFuncDecl (string name, Sort domain, Sort range) |
Creates a new function declaration. More... | |
FuncDecl | MkFreshFuncDecl (string prefix, Sort[] domain, Sort range) |
Creates a fresh function declaration with a name prefixed with prefix . More... | |
FuncDecl | MkConstDecl (Symbol name, Sort range) |
Creates a new constant function declaration. More... | |
FuncDecl | MkConstDecl (string name, Sort range) |
Creates a new constant function declaration. More... | |
FuncDecl | MkFreshConstDecl (string prefix, Sort range) |
Creates a fresh constant function declaration with a name prefixed with prefix . More... | |
Expr | MkBound (uint index, Sort ty) |
Creates a new bound variable. More... | |
Pattern | MkPattern (params Expr[] terms) |
Create a quantifier pattern. More... | |
Expr | MkConst (Symbol name, Sort range) |
Creates a new Constant of sort range and named name . More... | |
Expr | MkConst (string name, Sort range) |
Creates a new Constant of sort range and named name . More... | |
Expr | MkFreshConst (string prefix, Sort range) |
Creates a fresh Constant of sort range and a name prefixed with prefix . More... | |
Expr | MkConst (FuncDecl f) |
Creates a fresh constant from the FuncDecl f . More... | |
BoolExpr | MkBoolConst (Symbol name) |
Create a Boolean constant. More... | |
BoolExpr | MkBoolConst (string name) |
Create a Boolean constant. More... | |
IntExpr | MkIntConst (Symbol name) |
Creates an integer constant. More... | |
IntExpr | MkIntConst (string name) |
Creates an integer constant. More... | |
RealExpr | MkRealConst (Symbol name) |
Creates a real constant. More... | |
RealExpr | MkRealConst (string name) |
Creates a real constant. More... | |
BitVecExpr | MkBVConst (Symbol name, uint size) |
Creates a bit-vector constant. More... | |
BitVecExpr | MkBVConst (string name, uint size) |
Creates a bit-vector constant. More... | |
Expr | MkApp (FuncDecl f, params Expr[] args) |
Create a new function application. More... | |
BoolExpr | MkTrue () |
The true Term. More... | |
BoolExpr | MkFalse () |
The false Term. More... | |
BoolExpr | MkBool (bool value) |
Creates a Boolean value. More... | |
BoolExpr | MkEq (Expr x, Expr y) |
Creates the equality x = y . More... | |
BoolExpr | MkDistinct (params Expr[] args) |
Creates a distinct term. More... | |
BoolExpr | MkNot (BoolExpr a) |
Mk an expression representing not(a) . More... | |
Expr | MkITE (BoolExpr t1, Expr t2, Expr t3) |
Create an expression representing an if-then-else: ite(t1, t2, t3) . More... | |
BoolExpr | MkIff (BoolExpr t1, BoolExpr t2) |
Create an expression representing t1 iff t2 . More... | |
BoolExpr | MkImplies (BoolExpr t1, BoolExpr t2) |
Create an expression representing t1 -> t2 . More... | |
BoolExpr | MkXor (BoolExpr t1, BoolExpr t2) |
Create an expression representing t1 xor t2 . More... | |
BoolExpr | MkAnd (params BoolExpr[] t) |
Create an expression representing t[0] and t[1] and ... . More... | |
BoolExpr | MkOr (params BoolExpr[] t) |
Create an expression representing t[0] or t[1] or ... . More... | |
ArithExpr | MkAdd (params ArithExpr[] t) |
Create an expression representing t[0] + t[1] + ... . More... | |
ArithExpr | MkMul (params ArithExpr[] t) |
Create an expression representing t[0] * t[1] * ... . More... | |
ArithExpr | MkSub (params ArithExpr[] t) |
Create an expression representing t[0] - t[1] - ... . More... | |
ArithExpr | MkUnaryMinus (ArithExpr t) |
Create an expression representing -t . More... | |
ArithExpr | MkDiv (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 / t2 . More... | |
IntExpr | MkMod (IntExpr t1, IntExpr t2) |
Create an expression representing t1 mod t2 . More... | |
IntExpr | MkRem (IntExpr t1, IntExpr t2) |
Create an expression representing t1 rem t2 . More... | |
ArithExpr | MkPower (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 ^ t2 . More... | |
BoolExpr | MkLt (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 < t2 More... | |
BoolExpr | MkLe (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 <= t2 More... | |
BoolExpr | MkGt (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 > t2 More... | |
BoolExpr | MkGe (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 >= t2 More... | |
RealExpr | MkInt2Real (IntExpr t) |
Coerce an integer to a real. More... | |
IntExpr | MkReal2Int (RealExpr t) |
Coerce a real to an integer. More... | |
BoolExpr | MkIsInteger (RealExpr t) |
Creates an expression that checks whether a real number is an integer. More... | |
BitVecExpr | MkBVNot (BitVecExpr t) |
Bitwise negation. More... | |
BitVecExpr | MkBVRedAND (BitVecExpr t) |
Take conjunction of bits in a vector, return vector of length 1. More... | |
BitVecExpr | MkBVRedOR (BitVecExpr t) |
Take disjunction of bits in a vector, return vector of length 1. More... | |
BitVecExpr | MkBVAND (BitVecExpr t1, BitVecExpr t2) |
Bitwise conjunction. More... | |
BitVecExpr | MkBVOR (BitVecExpr t1, BitVecExpr t2) |
Bitwise disjunction. More... | |
BitVecExpr | MkBVXOR (BitVecExpr t1, BitVecExpr t2) |
Bitwise XOR. More... | |
BitVecExpr | MkBVNAND (BitVecExpr t1, BitVecExpr t2) |
Bitwise NAND. More... | |
BitVecExpr | MkBVNOR (BitVecExpr t1, BitVecExpr t2) |
Bitwise NOR. More... | |
BitVecExpr | MkBVXNOR (BitVecExpr t1, BitVecExpr t2) |
Bitwise XNOR. More... | |
BitVecExpr | MkBVNeg (BitVecExpr t) |
Standard two's complement unary minus. More... | |
BitVecExpr | MkBVAdd (BitVecExpr t1, BitVecExpr t2) |
Two's complement addition. More... | |
BitVecExpr | MkBVSub (BitVecExpr t1, BitVecExpr t2) |
Two's complement subtraction. More... | |
BitVecExpr | MkBVMul (BitVecExpr t1, BitVecExpr t2) |
Two's complement multiplication. More... | |
BitVecExpr | MkBVUDiv (BitVecExpr t1, BitVecExpr t2) |
Unsigned division. More... | |
BitVecExpr | MkBVSDiv (BitVecExpr t1, BitVecExpr t2) |
Signed division. More... | |
BitVecExpr | MkBVURem (BitVecExpr t1, BitVecExpr t2) |
Unsigned remainder. More... | |
BitVecExpr | MkBVSRem (BitVecExpr t1, BitVecExpr t2) |
Signed remainder. More... | |
BitVecExpr | MkBVSMod (BitVecExpr t1, BitVecExpr t2) |
Two's complement signed remainder (sign follows divisor). More... | |
BoolExpr | MkBVULT (BitVecExpr t1, BitVecExpr t2) |
Unsigned less-than More... | |
BoolExpr | MkBVSLT (BitVecExpr t1, BitVecExpr t2) |
Two's complement signed less-than More... | |
BoolExpr | MkBVULE (BitVecExpr t1, BitVecExpr t2) |
Unsigned less-than or equal to. More... | |
BoolExpr | MkBVSLE (BitVecExpr t1, BitVecExpr t2) |
Two's complement signed less-than or equal to. More... | |
BoolExpr | MkBVUGE (BitVecExpr t1, BitVecExpr t2) |
Unsigned greater than or equal to. More... | |
BoolExpr | MkBVSGE (BitVecExpr t1, BitVecExpr t2) |
Two's complement signed greater than or equal to. More... | |
BoolExpr | MkBVUGT (BitVecExpr t1, BitVecExpr t2) |
Unsigned greater-than. More... | |
BoolExpr | MkBVSGT (BitVecExpr t1, BitVecExpr t2) |
Two's complement signed greater-than. More... | |
BitVecExpr | MkConcat (BitVecExpr t1, BitVecExpr t2) |
Bit-vector concatenation. More... | |
BitVecExpr | MkExtract (uint high, uint low, BitVecExpr t) |
Bit-vector extraction. More... | |
BitVecExpr | MkSignExt (uint i, BitVecExpr t) |
Bit-vector sign extension. More... | |
BitVecExpr | MkZeroExt (uint i, BitVecExpr t) |
Bit-vector zero extension. More... | |
BitVecExpr | MkRepeat (uint i, BitVecExpr t) |
Bit-vector repetition. More... | |
BitVecExpr | MkBVSHL (BitVecExpr t1, BitVecExpr t2) |
Shift left. More... | |
BitVecExpr | MkBVLSHR (BitVecExpr t1, BitVecExpr t2) |
Logical shift right More... | |
BitVecExpr | MkBVASHR (BitVecExpr t1, BitVecExpr t2) |
Arithmetic shift right More... | |
BitVecExpr | MkBVRotateLeft (uint i, BitVecExpr t) |
Rotate Left. More... | |
BitVecExpr | MkBVRotateRight (uint i, BitVecExpr t) |
Rotate Right. More... | |
BitVecExpr | MkBVRotateLeft (BitVecExpr t1, BitVecExpr t2) |
Rotate Left. More... | |
BitVecExpr | MkBVRotateRight (BitVecExpr t1, BitVecExpr t2) |
Rotate Right. More... | |
BitVecExpr | MkInt2BV (uint n, IntExpr t) |
Create an n bit bit-vector from the integer argument t . More... | |
IntExpr | MkBV2Int (BitVecExpr t, bool signed) |
Create an integer from the bit-vector argument t . More... | |
BoolExpr | MkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned) |
Create a predicate that checks that the bit-wise addition does not overflow. More... | |
BoolExpr | MkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2) |
Create a predicate that checks that the bit-wise addition does not underflow. More... | |
BoolExpr | MkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2) |
Create a predicate that checks that the bit-wise subtraction does not overflow. More... | |
BoolExpr | MkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, bool isSigned) |
Create a predicate that checks that the bit-wise subtraction does not underflow. More... | |
BoolExpr | MkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2) |
Create a predicate that checks that the bit-wise signed division does not overflow. More... | |
BoolExpr | MkBVNegNoOverflow (BitVecExpr t) |
Create a predicate that checks that the bit-wise negation does not overflow. More... | |
BoolExpr | MkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned) |
Create a predicate that checks that the bit-wise multiplication does not overflow. More... | |
BoolExpr | MkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2) |
Create a predicate that checks that the bit-wise multiplication does not underflow. More... | |
ArrayExpr | MkArrayConst (Symbol name, Sort domain, Sort range) |
Create an array constant. More... | |
ArrayExpr | MkArrayConst (string name, Sort domain, Sort range) |
Create an array constant. More... | |
Expr | MkSelect (ArrayExpr a, Expr i) |
Array read. More... | |
ArrayExpr | MkStore (ArrayExpr a, Expr i, Expr v) |
Array update. More... | |
ArrayExpr | MkConstArray (Sort domain, Expr v) |
Create a constant array. More... | |
ArrayExpr | MkMap (FuncDecl f, params ArrayExpr[] args) |
Maps f on the argument arrays. More... | |
Expr | MkTermArray (ArrayExpr array) |
Access the array default value. More... | |
SetSort | MkSetSort (Sort ty) |
Create a set type. More... | |
ArrayExpr | MkEmptySet (Sort domain) |
Create an empty set. More... | |
ArrayExpr | MkFullSet (Sort domain) |
Create the full set. More... | |
ArrayExpr | MkSetAdd (ArrayExpr set, Expr element) |
Add an element to the set. More... | |
ArrayExpr | MkSetDel (ArrayExpr set, Expr element) |
Remove an element from a set. More... | |
ArrayExpr | MkSetUnion (params ArrayExpr[] args) |
Take the union of a list of sets. More... | |
ArrayExpr | MkSetIntersection (params ArrayExpr[] args) |
Take the intersection of a list of sets. More... | |
ArrayExpr | MkSetDifference (ArrayExpr arg1, ArrayExpr arg2) |
Take the difference between two sets. More... | |
ArrayExpr | MkSetComplement (ArrayExpr arg) |
Take the complement of a set. More... | |
BoolExpr | MkSetMembership (Expr elem, ArrayExpr set) |
Check for set membership. More... | |
BoolExpr | MkSetSubset (ArrayExpr arg1, ArrayExpr arg2) |
Check for subsetness of sets. More... | |
BoolExpr | MkAtMost (BoolExpr[] args, uint k) |
Create an at-most-k constraint. More... | |
BoolExpr | MkPBLe (int[] coeffs, BoolExpr[] args, int k) |
Create a pseudo-Boolean less-or-equal constraint. More... | |
Expr | MkNumeral (string v, Sort ty) |
Create a Term of a given sort. More... | |
Expr | MkNumeral (int v, Sort ty) |
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. More... | |
Expr | MkNumeral (uint v, Sort ty) |
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. More... | |
Expr | MkNumeral (long v, Sort ty) |
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. More... | |
Expr | MkNumeral (ulong v, Sort ty) |
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. More... | |
RatNum | MkReal (int num, int den) |
Create a real from a fraction. More... | |
RatNum | MkReal (string v) |
Create a real numeral. More... | |
RatNum | MkReal (int v) |
Create a real numeral. More... | |
RatNum | MkReal (uint v) |
Create a real numeral. More... | |
RatNum | MkReal (long v) |
Create a real numeral. More... | |
RatNum | MkReal (ulong v) |
Create a real numeral. More... | |
IntNum | MkInt (string v) |
Create an integer numeral. More... | |
IntNum | MkInt (int v) |
Create an integer numeral. More... | |
IntNum | MkInt (uint v) |
Create an integer numeral. More... | |
IntNum | MkInt (long v) |
Create an integer numeral. More... | |
IntNum | MkInt (ulong v) |
Create an integer numeral. More... | |
BitVecNum | MkBV (string v, uint size) |
Create a bit-vector numeral. More... | |
BitVecNum | MkBV (int v, uint size) |
Create a bit-vector numeral. More... | |
BitVecNum | MkBV (uint v, uint size) |
Create a bit-vector numeral. More... | |
BitVecNum | MkBV (long v, uint size) |
Create a bit-vector numeral. More... | |
BitVecNum | MkBV (ulong v, uint size) |
Create a bit-vector numeral. More... | |
Quantifier | MkForall (Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
Create a universal Quantifier. More... | |
Quantifier | MkForall (Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
Create a universal Quantifier. More... | |
Quantifier | MkExists (Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
Create an existential Quantifier. More... | |
Quantifier | MkExists (Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
Create an existential Quantifier. More... | |
Quantifier | MkQuantifier (bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
Create a Quantifier. More... | |
Quantifier | MkQuantifier (bool universal, Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
Create a Quantifier. More... | |
string | BenchmarkToSMTString (string name, string logic, string status, string attributes, BoolExpr[] assumptions, BoolExpr formula) |
Convert a benchmark into an SMT-LIB formatted string. More... | |
void | ParseSMTLIBString (string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null) |
Parse the given string using the SMT-LIB parser. More... | |
void | ParseSMTLIBFile (string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null) |
Parse the given file using the SMT-LIB parser. More... | |
BoolExpr | ParseSMTLIB2String (string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null) |
Parse the given string using the SMT-LIB2 parser. More... | |
BoolExpr | ParseSMTLIB2File (string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null) |
Parse the given file using the SMT-LIB2 parser. More... | |
Goal | MkGoal (bool models=true, bool unsatCores=false, bool proofs=false) |
Creates a new Goal. More... | |
Params | MkParams () |
Creates a new ParameterSet. More... | |
string | TacticDescription (string name) |
Returns a string containing a description of the tactic with the given name. More... | |
Tactic | MkTactic (string name) |
Creates a new Tactic. More... | |
Tactic | AndThen (Tactic t1, Tactic t2, params Tactic[] ts) |
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 . More... | |
Tactic | Then (Tactic t1, Tactic t2, params Tactic[] ts) |
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 . More... | |
Tactic | OrElse (Tactic t1, Tactic t2) |
Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal. More... | |
Tactic | TryFor (Tactic t, uint ms) |
Create a tactic that applies t to a goal for ms milliseconds. More... | |
Tactic | When (Probe p, Tactic t) |
Create a tactic that applies t to a given goal if the probe p evaluates to true. More... | |
Tactic | Cond (Probe p, Tactic t1, Tactic t2) |
Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise. More... | |
Tactic | Repeat (Tactic t, uint max=uint.MaxValue) |
Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached. More... | |
Tactic | Skip () |
Create a tactic that just returns the given goal. More... | |
Tactic | Fail () |
Create a tactic always fails. More... | |
Tactic | FailIf (Probe p) |
Create a tactic that fails if the probe p evaluates to false. More... | |
Tactic | FailIfNotDecided () |
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false'). More... | |
Tactic | UsingParams (Tactic t, Params p) |
Create a tactic that applies t using the given set of parameters p . More... | |
Tactic | With (Tactic t, Params p) |
Create a tactic that applies t using the given set of parameters p . More... | |
Tactic | ParOr (params Tactic[] t) |
Create a tactic that applies the given tactics in parallel. More... | |
Tactic | ParAndThen (Tactic t1, Tactic t2) |
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. More... | |
void | Interrupt () |
Interrupt the execution of a Z3 procedure. More... | |
string | ProbeDescription (string name) |
Returns a string containing a description of the probe with the given name. More... | |
Probe | MkProbe (string name) |
Creates a new Probe. More... | |
Probe | ConstProbe (double val) |
Create a probe that always evaluates to val . More... | |
Probe | Lt (Probe p1, Probe p2) |
Create a probe that evaluates to "true" when the value returned by p1 is less than the value returned by p2 More... | |
Probe | Gt (Probe p1, Probe p2) |
Create a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2 More... | |
Probe | Le (Probe p1, Probe p2) |
Create a probe that evaluates to "true" when the value returned by p1 is less than or equal the value returned by p2 More... | |
Probe | Ge (Probe p1, Probe p2) |
Create a probe that evaluates to "true" when the value returned by p1 is greater than or equal the value returned by p2 More... | |
Probe | Eq (Probe p1, Probe p2) |
Create a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2 More... | |
Probe | And (Probe p1, Probe p2) |
Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true". More... | |
Probe | Or (Probe p1, Probe p2) |
Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true". More... | |
Probe | Not (Probe p) |
Create a probe that evaluates to "true" when the value p does not evaluate to "true". More... | |
Solver | MkSolver (Symbol logic=null) |
Creates a new (incremental) solver. More... | |
Solver | MkSolver (string logic) |
Creates a new (incremental) solver. More... | |
Solver | MkSimpleSolver () |
Creates a new (incremental) solver. More... | |
Solver | MkSolver (Tactic t) |
Creates a solver that is implemented using the given tactic. More... | |
Fixedpoint | MkFixedpoint () |
Create a Fixedpoint context. More... | |
Optimize | MkOptimize () |
Create an Optimization context. More... | |
FPRMSort | MkFPRoundingModeSort () |
Create the floating-point RoundingMode sort. More... | |
FPRMExpr | MkFPRoundNearestTiesToEven () |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More... | |
FPRMNum | MkFPRNE () |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More... | |
FPRMNum | MkFPRoundNearestTiesToAway () |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More... | |
FPRMNum | MkFPRNA () |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More... | |
FPRMNum | MkFPRoundTowardPositive () |
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. More... | |
FPRMNum | MkFPRTP () |
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. More... | |
FPRMNum | MkFPRoundTowardNegative () |
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. More... | |
FPRMNum | MkFPRTN () |
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. More... | |
FPRMNum | MkFPRoundTowardZero () |
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. More... | |
FPRMNum | MkFPRTZ () |
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. More... | |
FPSort | MkFPSort (uint ebits, uint sbits) |
Create a FloatingPoint sort. More... | |
FPSort | MkFPSortHalf () |
Create the half-precision (16-bit) FloatingPoint sort. More... | |
FPSort | MkFPSort16 () |
Create the half-precision (16-bit) FloatingPoint sort. More... | |
FPSort | MkFPSortSingle () |
Create the single-precision (32-bit) FloatingPoint sort. More... | |
FPSort | MkFPSort32 () |
Create the single-precision (32-bit) FloatingPoint sort. More... | |
FPSort | MkFPSortDouble () |
Create the double-precision (64-bit) FloatingPoint sort. More... | |
FPSort | MkFPSort64 () |
Create the double-precision (64-bit) FloatingPoint sort. More... | |
FPSort | MkFPSortQuadruple () |
Create the quadruple-precision (128-bit) FloatingPoint sort. More... | |
FPSort | MkFPSort128 () |
Create the quadruple-precision (128-bit) FloatingPoint sort. More... | |
FPNum | MkFPNaN (FPSort s) |
Create a NaN of sort s. More... | |
FPNum | MkFPInf (FPSort s, bool negative) |
Create a floating-point infinity of sort s. More... | |
FPNum | MkFPZero (FPSort s, bool negative) |
Create a floating-point zero of sort s. More... | |
FPNum | MkFPNumeral (float v, FPSort s) |
Create a numeral of FloatingPoint sort from a float. More... | |
FPNum | MkFPNumeral (double v, FPSort s) |
Create a numeral of FloatingPoint sort from a float. More... | |
FPNum | MkFPNumeral (int v, FPSort s) |
Create a numeral of FloatingPoint sort from an int. More... | |
FPNum | MkFPNumeral (bool sgn, uint sig, int exp, FPSort s) |
Create a numeral of FloatingPoint sort from a sign bit and two integers. More... | |
FPNum | MkFPNumeral (bool sgn, Int64 exp, UInt64 sig, FPSort s) |
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. More... | |
FPNum | MkFP (float v, FPSort s) |
Create a numeral of FloatingPoint sort from a float. More... | |
FPNum | MkFP (double v, FPSort s) |
Create a numeral of FloatingPoint sort from a float. More... | |
FPNum | MkFP (int v, FPSort s) |
Create a numeral of FloatingPoint sort from an int. More... | |
FPNum | MkFP (bool sgn, int exp, uint sig, FPSort s) |
Create a numeral of FloatingPoint sort from a sign bit and two integers. More... | |
FPNum | MkFP (bool sgn, Int64 exp, UInt64 sig, FPSort s) |
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. More... | |
FPExpr | MkFPAbs (FPExpr t) |
Floating-point absolute value More... | |
FPExpr | MkFPNeg (FPExpr t) |
Floating-point negation More... | |
FPExpr | MkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2) |
Floating-point addition More... | |
FPExpr | MkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2) |
Floating-point subtraction More... | |
FPExpr | MkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2) |
Floating-point multiplication More... | |
FPExpr | MkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2) |
Floating-point division More... | |
FPExpr | MkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) |
Floating-point fused multiply-add More... | |
FPExpr | MkFPSqrt (FPRMExpr rm, FPExpr t) |
Floating-point square root More... | |
FPExpr | MkFPRem (FPExpr t1, FPExpr t2) |
Floating-point remainder More... | |
FPExpr | MkFPRoundToIntegral (FPRMExpr rm, FPExpr t) |
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number. More... | |
FPExpr | MkFPMin (FPExpr t1, FPExpr t2) |
Minimum of floating-point numbers. More... | |
FPExpr | MkFPMax (FPExpr t1, FPExpr t2) |
Maximum of floating-point numbers. More... | |
BoolExpr | MkFPLEq (FPExpr t1, FPExpr t2) |
Floating-point less than or equal. More... | |
BoolExpr | MkFPLt (FPExpr t1, FPExpr t2) |
Floating-point less than. More... | |
BoolExpr | MkFPGEq (FPExpr t1, FPExpr t2) |
Floating-point greater than or equal. More... | |
BoolExpr | MkFPGt (FPExpr t1, FPExpr t2) |
Floating-point greater than. More... | |
BoolExpr | MkFPEq (FPExpr t1, FPExpr t2) |
Floating-point equality. More... | |
BoolExpr | MkFPIsNormal (FPExpr t) |
Predicate indicating whether t is a normal floating-point number. More... | |
BoolExpr | MkFPIsSubnormal (FPExpr t) |
Predicate indicating whether t is a subnormal floating-point number. More... | |
BoolExpr | MkFPIsZero (FPExpr t) |
Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0. More... | |
BoolExpr | MkFPIsInfinite (FPExpr t) |
Predicate indicating whether t is a floating-point number representing +oo or -oo. More... | |
BoolExpr | MkFPIsNaN (FPExpr t) |
Predicate indicating whether t is a NaN. More... | |
BoolExpr | MkFPIsNegative (FPExpr t) |
Predicate indicating whether t is a negative floating-point number. More... | |
BoolExpr | MkFPIsPositive (FPExpr t) |
Predicate indicating whether t is a positive floating-point number. More... | |
FPExpr | MkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp) |
Create an expression of FloatingPoint sort from three bit-vector expressions. More... | |
FPExpr | MkFPToFP (BitVecExpr bv, FPSort s) |
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. More... | |
FPExpr | MkFPToFP (FPRMExpr rm, FPExpr t, FPSort s) |
Conversion of a FloatingPoint term into another term of different FloatingPoint sort. More... | |
FPExpr | MkFPToFP (FPRMExpr rm, RealExpr t, FPSort s) |
Conversion of a term of real sort into a term of FloatingPoint sort. More... | |
FPExpr | MkFPToFP (FPRMExpr rm, BitVecExpr t, FPSort s, bool signed) |
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort. More... | |
FPExpr | MkFPToFP (FPSort s, FPRMExpr rm, FPExpr t) |
Conversion of a floating-point number to another FloatingPoint sort s. More... | |
BitVecExpr | MkFPToBV (FPRMExpr rm, FPExpr t, uint sz, bool signed) |
Conversion of a floating-point term into a bit-vector. More... | |
RealExpr | MkFPToReal (FPExpr t) |
Conversion of a floating-point term into a real-numbered term. More... | |
BitVecExpr | MkFPToIEEEBV (FPExpr t) |
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. More... | |
BitVecExpr | MkFPToFP (FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s) |
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. More... | |
AST | WrapAST (IntPtr nativeObject) |
Wraps an AST. More... | |
IntPtr | UnwrapAST (AST a) |
Unwraps an AST. More... | |
string | SimplifyHelp () |
Return a string describing all available parameters to Expr.Simplify . More... | |
void | UpdateParamValue (string id, string value) |
Update a mutable configuration parameter. More... | |
void | Dispose () |
Disposes of the context. More... | |
Additional Inherited Members | |
![]() | |
BoolSort | BoolSort [get] |
Retrieves the Boolean sort of the context. More... | |
IntSort | IntSort [get] |
Retrieves the Integer sort of the context. More... | |
RealSort | RealSort [get] |
Retrieves the Real sort of the context. More... | |
Z3_ast_print_mode | PrintMode [set] |
Selects the format used for pretty-printing expressions. More... | |
uint | NumSMTLIBFormulas [get] |
The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile . More... | |
BoolExpr[] | SMTLIBFormulas [get] |
The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile . More... | |
uint | NumSMTLIBAssumptions [get] |
The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile . More... | |
BoolExpr[] | SMTLIBAssumptions [get] |
The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile . More... | |
uint | NumSMTLIBDecls [get] |
The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile . More... | |
FuncDecl[] | SMTLIBDecls [get] |
The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile . More... | |
uint | NumSMTLIBSorts [get] |
The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile . More... | |
Sort[] | SMTLIBSorts [get] |
The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile . More... | |
uint | NumTactics [get] |
The number of supported tactics. More... | |
string[] | TacticNames [get] |
The names of all supported tactics. More... | |
uint | NumProbes [get] |
The number of supported Probes. More... | |
string[] | ProbeNames [get] |
The names of all supported Probes. More... | |
ParamDescrs | SimplifyParameterDescriptions [get] |
Retrieves parameter descriptions for simplifier. More... | |
IDecRefQueue | AST_DRQ [get] |
AST DRQ More... | |
IDecRefQueue | ASTMap_DRQ [get] |
ASTMap DRQ More... | |
IDecRefQueue | ASTVector_DRQ [get] |
ASTVector DRQ More... | |
IDecRefQueue | ApplyResult_DRQ [get] |
ApplyResult DRQ More... | |
IDecRefQueue | FuncEntry_DRQ [get] |
FuncEntry DRQ More... | |
IDecRefQueue | FuncInterp_DRQ [get] |
FuncInterp DRQ More... | |
IDecRefQueue | Goal_DRQ [get] |
Goal DRQ More... | |
IDecRefQueue | Model_DRQ [get] |
Model DRQ More... | |
IDecRefQueue | Params_DRQ [get] |
Params DRQ More... | |
IDecRefQueue | ParamDescrs_DRQ [get] |
ParamDescrs DRQ More... | |
IDecRefQueue | Probe_DRQ [get] |
Probe DRQ More... | |
IDecRefQueue | Solver_DRQ [get] |
Solver DRQ More... | |
IDecRefQueue | Statistics_DRQ [get] |
Statistics DRQ More... | |
IDecRefQueue | Tactic_DRQ [get] |
Tactic DRQ More... | |
IDecRefQueue | Fixedpoint_DRQ [get] |
FixedPoint DRQ More... | |
IDecRefQueue | Optimize_DRQ [get] |
Optimize DRQ More... | |
The InterpolationContext is suitable for generation of interpolants.
For more information on interpolation please refer too the C/C++ API, which is well documented.
Definition at line 22 of file InterpolationContext.cs.
|
inline |
|
inline |
Definition at line 34 of file InterpolationContext.cs.
|
inline |
Checks the correctness of an interpolant.
For more information on interpolation please refer too the function Z3_check_interpolant in the C/C++ API, which is well documented.
Definition at line 111 of file InterpolationContext.cs.
Computes an interpolant.
For more information on interpolation please refer too the function Z3_compute_interpolant in the C/C++ API, which is well documented.
Definition at line 77 of file InterpolationContext.cs.
Computes an interpolant.
For more information on interpolation please refer too the function Z3_get_interpolant in the C/C++ API, which is well documented.
Definition at line 56 of file InterpolationContext.cs.
|
inline |
Return a string summarizing cumulative time used for interpolation.
For more information on interpolation please refer too the function Z3_interpolation_profile in the C/C++ API, which is well documented.
Definition at line 100 of file InterpolationContext.cs.
Create an expression that marks a formula position for interpolation.
Definition at line 40 of file InterpolationContext.cs.
|
inline |
Reads an interpolation problem from a file.
For more information on interpolation please refer too the function Z3_read_interpolation_problem in the C/C++ API, which is well documented.
Definition at line 134 of file InterpolationContext.cs.
|
inline |
Writes an interpolation problem to a file.
For more information on interpolation please refer too the function Z3_write_interpolation_problem in the C/C++ API, which is well documented.
Definition at line 158 of file InterpolationContext.cs.