Z3
Public Member Functions
InterpolationContext Class Reference

The InterpolationContext is suitable for generation of interpolants. More...

+ Inheritance diagram for InterpolationContext:

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...
 
- Public Member Functions inherited from Context
 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...
 
SeqSort MkSeqSort (Sort s)
 Create a new sequence sort. More...
 
ReSort MkReSort (SeqSort s)
 Create a new regular expression 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.

Returns
The result is a sort
More...
 
FiniteDomainSort MkFiniteDomainSort (string name, ulong size)
 Create a new finite domain sort.

Returns
The result is a sort

Elements of the sort are created using

See also
MkNumeral(ulong, Sort)

, and the elements range from 0 to size-1. 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...
 
Expr MkApp (FuncDecl f, IEnumerable< 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 MkAnd (IEnumerable< 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...
 
BoolExpr MkOr (IEnumerable< 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 MkAdd (IEnumerable< 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 MkMul (IEnumerable< 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...
 
Expr MkArrayExt (ArrayExpr arg1, ArrayExpr arg2)
 Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt. 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...
 
SeqExpr MkEmptySeq (Sort s)
 Create the empty sequence. More...
 
SeqExpr MkUnit (Expr elem)
 Create the singleton sequence. More...
 
SeqExpr MkString (string s)
 Create a string constant. More...
 
SeqExpr MkConcat (params SeqExpr[] t)
 Concatentate sequences. More...
 
IntExpr MkLength (SeqExpr s)
 Retrieve the length of a given sequence. More...
 
BoolExpr MkPrefixOf (SeqExpr s1, SeqExpr s2)
 Check for sequence prefix. More...
 
BoolExpr MkSuffixOf (SeqExpr s1, SeqExpr s2)
 Check for sequence suffix. More...
 
BoolExpr MkContains (SeqExpr s1, SeqExpr s2)
 Check for sequence containment of s2 in s1. More...
 
SeqExpr MkAt (SeqExpr s, IntExpr index)
 Retrieve sequence of length one at index. More...
 
SeqExpr MkExtract (SeqExpr s, IntExpr offset, IntExpr length)
 Extract subsequence. More...
 
IntExpr MkIndexOf (SeqExpr s, SeqExpr substr, ArithExpr offset)
 Extract index of sub-string starting at offset. More...
 
SeqExpr MkReplace (SeqExpr s, SeqExpr src, SeqExpr dst)
 Replace the first occurrence of src by dst in s. More...
 
ReExpr MkToRe (SeqExpr s)
 Convert a regular expression that accepts sequence s. More...
 
BoolExpr MkInRe (SeqExpr s, ReExpr re)
 Check for regular expression membership. More...
 
ReExpr MkStar (ReExpr re)
 Take the Kleene star of a regular expression. More...
 
ReExpr MPlus (ReExpr re)
 Take the Kleene plus of a regular expression. More...
 
ReExpr MOption (ReExpr re)
 Create the optional regular expression. More...
 
ReExpr MkConcat (params ReExpr[] t)
 Create the concatenation of regular languages. More...
 
ReExpr MkUnion (params ReExpr[] t)
 Create the union of regular languages. 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...
 
BoolExpr MkPBEq (int[] coeffs, BoolExpr[] args, int k)
 Create a pseudo-Boolean 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 until one of them succeeds (i.e., the first that doesn't fail). 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

- Properties inherited from Context
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...
 
SeqSort StringSort [get]
 Retrieves the String 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...
 

Detailed Description

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.

Constructor & Destructor Documentation

§ InterpolationContext() [1/2]

Constructor.

Definition at line 28 of file InterpolationContext.cs.

28 : base() { }

§ InterpolationContext() [2/2]

InterpolationContext ( Dictionary< string, string >  settings)
inline

Constructor.

See also
Context

Definition at line 34 of file InterpolationContext.cs.

34 : base(settings) { }

Member Function Documentation

§ CheckInterpolant()

int CheckInterpolant ( Expr []  cnsts,
uint []  parents,
BoolExpr []  interps,
out string  error,
Expr []  theory 
)
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.

112  {
113  Contract.Requires(cnsts.Length == parents.Length);
114  Contract.Requires(cnsts.Length == interps.Length + 1);
115  IntPtr n_err_str;
116  int r = Native.Z3_check_interpolant(nCtx,
117  (uint)cnsts.Length,
118  Expr.ArrayToNative(cnsts),
119  parents,
120  Expr.ArrayToNative(interps),
121  out n_err_str,
122  (uint)theory.Length,
123  Expr.ArrayToNative(theory));
124  error = Marshal.PtrToStringAnsi(n_err_str);
125  return r;
126  }

§ ComputeInterpolant()

Z3_lbool ComputeInterpolant ( Expr  pat,
Params  p,
out BoolExpr []  interp,
out Model  model 
)
inline

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.

78  {
79  Contract.Requires(pat != null);
80  Contract.Requires(p != null);
81  Contract.Ensures(Contract.ValueAtReturn(out interp) != null);
82  Contract.Ensures(Contract.ValueAtReturn(out model) != null);
83 
84  CheckContextMatch(pat);
85  CheckContextMatch(p);
86 
87  IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
88  int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
89  interp = new ASTVector(this, i).ToBoolExprArray();
90  model = new Model(this, m);
91  return (Z3_lbool)r;
92  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105

§ GetInterpolant()

BoolExpr [] GetInterpolant ( Expr  pf,
Expr  pat,
Params  p 
)
inline

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.

57  {
58  Contract.Requires(pf != null);
59  Contract.Requires(pat != null);
60  Contract.Requires(p != null);
61  Contract.Ensures(Contract.Result<Expr>() != null);
62 
63  CheckContextMatch(pf);
64  CheckContextMatch(pat);
65  CheckContextMatch(p);
66 
67  ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
68  return seq.ToBoolExprArray();
69  }

§ InterpolationProfile()

string InterpolationProfile ( )
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.

101  {
102  return Native.Z3_interpolation_profile(nCtx);
103  }

§ MkInterpolant()

BoolExpr MkInterpolant ( BoolExpr  a)
inline

Create an expression that marks a formula position for interpolation.

Definition at line 40 of file InterpolationContext.cs.

41  {
42  Contract.Requires(a != null);
43  Contract.Ensures(Contract.Result<BoolExpr>() != null);
44 
45  CheckContextMatch(a);
46  return new BoolExpr(this, Native.Z3_mk_interpolant(nCtx, a.NativeObject));
47  }

§ ReadInterpolationProblem()

int ReadInterpolationProblem ( string  filename,
out Expr []  cnsts,
out uint []  parents,
out string  error,
out Expr []  theory 
)
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.

135  {
136  uint num = 0, num_theory = 0;
137  IntPtr[] n_cnsts;
138  IntPtr[] n_theory;
139  IntPtr n_err_str;
140  int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out n_theory);
141  error = Marshal.PtrToStringAnsi(n_err_str);
142  cnsts = new Expr[num];
143  parents = new uint[num];
144  theory = new Expr[num_theory];
145  for (int i = 0; i < num; i++)
146  cnsts[i] = Expr.Create(this, n_cnsts[i]);
147  for (int i = 0; i < num_theory; i++)
148  theory[i] = Expr.Create(this, n_theory[i]);
149  return r;
150  }

§ WriteInterpolationProblem()

void WriteInterpolationProblem ( string  filename,
Expr []  cnsts,
uint []  parents,
Expr []  theory 
)
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.

159  {
160  Contract.Requires(cnsts.Length == parents.Length);
161  Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length, Expr.ArrayToNative(theory));
162  }