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]

InterpolationContext ( )

inline

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.

         {
             Contract.Requires(cnsts.Length == parents.Length);
             Contract.Requires(cnsts.Length == interps.Length + 1);
             IntPtr n_err_str;
             int r = Native.Z3_check_interpolant(nCtx,
                                                 (uint)cnsts.Length,
                                                 Expr.ArrayToNative(cnsts),
                                                 parents,
                                                 Expr.ArrayToNative(interps),
                                                 out n_err_str,
                                                 (uint)theory.Length,
                                                 Expr.ArrayToNative(theory));
             error = Marshal.PtrToStringAnsi(n_err_str);
             return r;
         }

◆ 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.

         {
             Contract.Requires(pat != null);
             Contract.Requires(p != null);
             Contract.Ensures(Contract.ValueAtReturn(out interp) != null);
             Contract.Ensures(Contract.ValueAtReturn(out model) != null);
 
             CheckContextMatch(pat);
             CheckContextMatch(p);
 
             IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
             int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
             interp = new ASTVector(this, i).ToBoolExprArray();
             model = new Model(this, m);
             return (Z3_lbool)r;
         }

◆ 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.

         {
             Contract.Requires(pf != null);
             Contract.Requires(pat != null);
             Contract.Requires(p != null);
             Contract.Ensures(Contract.Result<Expr>() != null);
 
             CheckContextMatch(pf);
             CheckContextMatch(pat);
             CheckContextMatch(p);
 
             ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
             return seq.ToBoolExprArray();
         }

◆ 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.

         {
             return Native.Z3_interpolation_profile(nCtx);
         }

◆ MkInterpolant()

BoolExpr MkInterpolant ( BoolExpr a )

inline

Create an expression that marks a formula position for interpolation.

Definition at line 40 of file InterpolationContext.cs.

         {
             Contract.Requires(a != null);
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
 
             CheckContextMatch(a);
             return new BoolExpr(this, Native.Z3_mk_interpolant(nCtx, a.NativeObject));
         }

◆ 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.

         {
             uint num = 0, num_theory = 0;
             IntPtr[] n_cnsts;
             IntPtr[] n_theory;
             IntPtr n_err_str;
             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);
             error = Marshal.PtrToStringAnsi(n_err_str);
             cnsts = new Expr[num];
             parents = new uint[num];
             theory = new Expr[num_theory];
             for (int i = 0; i < num; i++)
                 cnsts[i] = Expr.Create(this, n_cnsts[i]);
             for (int i = 0; i < num_theory; i++)
                 theory[i] = Expr.Create(this, n_theory[i]);
             return r;
         }

◆ 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.

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

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ InterpolationContext() [1/2]

◆ InterpolationContext() [2/2]

Member Function Documentation

◆ CheckInterpolant()

◆ ComputeInterpolant()

◆ GetInterpolant()

◆ InterpolationProfile()

◆ MkInterpolant()

◆ ReadInterpolationProblem()

◆ WriteInterpolationProblem()