Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions | Protected Member Functions
Context Class Reference
+ Inheritance diagram for Context:

Public Member Functions

 Context ()
 
 Context (Map< String, String > settings)
 
IntSymbol mkSymbol (int i)
 
StringSymbol mkSymbol (String name)
 
BoolSort getBoolSort ()
 
IntSort getIntSort ()
 
RealSort getRealSort ()
 
BoolSort mkBoolSort ()
 
SeqSort getStringSort ()
 
UninterpretedSort mkUninterpretedSort (Symbol s)
 
UninterpretedSort mkUninterpretedSort (String str)
 
IntSort mkIntSort ()
 
RealSort mkRealSort ()
 
BitVecSort mkBitVecSort (int size)
 
ArraySort mkArraySort (Sort domain, Sort range)
 
ArraySort mkArraySort (Sort[] domains, Sort range)
 
SeqSort mkStringSort ()
 
SeqSort mkSeqSort (Sort s)
 
ReSort mkReSort (Sort s)
 
TupleSort mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
 
EnumSort mkEnumSort (Symbol name, Symbol...enumNames)
 
EnumSort mkEnumSort (String name, String...enumNames)
 
ListSort mkListSort (Symbol name, Sort elemSort)
 
ListSort mkListSort (String name, Sort elemSort)
 
FiniteDomainSort mkFiniteDomainSort (Symbol name, long size)
 
FiniteDomainSort mkFiniteDomainSort (String name, long size)
 
Constructor mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
 
Constructor mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
 
DatatypeSort mkDatatypeSort (Symbol name, Constructor[] constructors)
 
DatatypeSort mkDatatypeSort (String name, Constructor[] constructors)
 
DatatypeSort[] mkDatatypeSorts (Symbol[] names, Constructor[][] c)
 
DatatypeSort[] mkDatatypeSorts (String[] names, Constructor[][] c)
 
Expr mkUpdateField (FuncDecl field, Expr t, Expr v) throws Z3Exception
 
FuncDecl mkFuncDecl (Symbol name, Sort[] domain, Sort range)
 
FuncDecl mkFuncDecl (Symbol name, Sort domain, Sort range)
 
FuncDecl mkFuncDecl (String name, Sort[] domain, Sort range)
 
FuncDecl mkFuncDecl (String name, Sort domain, Sort range)
 
FuncDecl mkFreshFuncDecl (String prefix, Sort[] domain, Sort range)
 
FuncDecl mkConstDecl (Symbol name, Sort range)
 
FuncDecl mkConstDecl (String name, Sort range)
 
FuncDecl mkFreshConstDecl (String prefix, Sort range)
 
Expr mkBound (int index, Sort ty)
 
Pattern mkPattern (Expr...terms)
 
Expr mkConst (Symbol name, Sort range)
 
Expr mkConst (String name, Sort range)
 
Expr mkFreshConst (String prefix, Sort range)
 
Expr mkConst (FuncDecl f)
 
BoolExpr mkBoolConst (Symbol name)
 
BoolExpr mkBoolConst (String name)
 
IntExpr mkIntConst (Symbol name)
 
IntExpr mkIntConst (String name)
 
RealExpr mkRealConst (Symbol name)
 
RealExpr mkRealConst (String name)
 
BitVecExpr mkBVConst (Symbol name, int size)
 
BitVecExpr mkBVConst (String name, int size)
 
Expr mkApp (FuncDecl f, Expr...args)
 
BoolExpr mkTrue ()
 
BoolExpr mkFalse ()
 
BoolExpr mkBool (boolean value)
 
BoolExpr mkEq (Expr x, Expr y)
 
BoolExpr mkDistinct (Expr...args)
 
BoolExpr mkNot (BoolExpr a)
 
Expr mkITE (BoolExpr t1, Expr t2, Expr t3)
 
BoolExpr mkIff (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkImplies (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkXor (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkAnd (BoolExpr...t)
 
BoolExpr mkOr (BoolExpr...t)
 
ArithExpr mkAdd (ArithExpr...t)
 
ArithExpr mkMul (ArithExpr...t)
 
ArithExpr mkSub (ArithExpr...t)
 
ArithExpr mkUnaryMinus (ArithExpr t)
 
ArithExpr mkDiv (ArithExpr t1, ArithExpr t2)
 
IntExpr mkMod (IntExpr t1, IntExpr t2)
 
IntExpr mkRem (IntExpr t1, IntExpr t2)
 
ArithExpr mkPower (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkLt (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkLe (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkGt (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkGe (ArithExpr t1, ArithExpr t2)
 
RealExpr mkInt2Real (IntExpr t)
 
IntExpr mkReal2Int (RealExpr t)
 
BoolExpr mkIsInteger (RealExpr t)
 
BitVecExpr mkBVNot (BitVecExpr t)
 
BitVecExpr mkBVRedAND (BitVecExpr t)
 
BitVecExpr mkBVRedOR (BitVecExpr t)
 
BitVecExpr mkBVAND (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVXOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNAND (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVXNOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNeg (BitVecExpr t)
 
BitVecExpr mkBVAdd (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSub (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVMul (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVUDiv (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSDiv (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVURem (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSRem (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSMod (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVULT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSLT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVULE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSLE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVUGE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSGE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVUGT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSGT (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkConcat (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkExtract (int high, int low, BitVecExpr t)
 
BitVecExpr mkSignExt (int i, BitVecExpr t)
 
BitVecExpr mkZeroExt (int i, BitVecExpr t)
 
BitVecExpr mkRepeat (int i, BitVecExpr t)
 
BitVecExpr mkBVSHL (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVLSHR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVASHR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVRotateLeft (int i, BitVecExpr t)
 
BitVecExpr mkBVRotateRight (int i, BitVecExpr t)
 
BitVecExpr mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVRotateRight (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkInt2BV (int n, IntExpr t)
 
IntExpr mkBV2Int (BitVecExpr t, boolean signed)
 
BoolExpr mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVNegNoOverflow (BitVecExpr t)
 
BoolExpr mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 
ArrayExpr mkArrayConst (Symbol name, Sort domain, Sort range)
 
ArrayExpr mkArrayConst (String name, Sort domain, Sort range)
 
Expr mkSelect (ArrayExpr a, Expr i)
 
Expr mkSelect (ArrayExpr a, Expr[] args)
 
ArrayExpr mkStore (ArrayExpr a, Expr i, Expr v)
 
ArrayExpr mkStore (ArrayExpr a, Expr[] args, Expr v)
 
ArrayExpr mkConstArray (Sort domain, Expr v)
 
ArrayExpr mkMap (FuncDecl f, ArrayExpr...args)
 
Expr mkTermArray (ArrayExpr array)
 
Expr mkArrayExt (ArrayExpr arg1, ArrayExpr arg2)
 
SetSort mkSetSort (Sort ty)
 
ArrayExpr mkEmptySet (Sort domain)
 
ArrayExpr mkFullSet (Sort domain)
 
ArrayExpr mkSetAdd (ArrayExpr set, Expr element)
 
ArrayExpr mkSetDel (ArrayExpr set, Expr element)
 
ArrayExpr mkSetUnion (ArrayExpr...args)
 
ArrayExpr mkSetIntersection (ArrayExpr...args)
 
ArrayExpr mkSetDifference (ArrayExpr arg1, ArrayExpr arg2)
 
ArrayExpr mkSetComplement (ArrayExpr arg)
 
BoolExpr mkSetMembership (Expr elem, ArrayExpr set)
 
BoolExpr mkSetSubset (ArrayExpr arg1, ArrayExpr arg2)
 
SeqExpr mkEmptySeq (Sort s)
 
SeqExpr mkUnit (Expr elem)
 
SeqExpr mkString (String s)
 
SeqExpr intToString (Expr e)
 
IntExpr stringToInt (Expr e)
 
SeqExpr mkConcat (SeqExpr...t)
 
IntExpr mkLength (SeqExpr s)
 
BoolExpr mkPrefixOf (SeqExpr s1, SeqExpr s2)
 
BoolExpr mkSuffixOf (SeqExpr s1, SeqExpr s2)
 
BoolExpr mkContains (SeqExpr s1, SeqExpr s2)
 
SeqExpr mkAt (SeqExpr s, IntExpr index)
 
SeqExpr mkExtract (SeqExpr s, IntExpr offset, IntExpr length)
 
IntExpr mkIndexOf (SeqExpr s, SeqExpr substr, ArithExpr offset)
 
SeqExpr mkReplace (SeqExpr s, SeqExpr src, SeqExpr dst)
 
ReExpr mkToRe (SeqExpr s)
 
BoolExpr mkInRe (SeqExpr s, ReExpr re)
 
ReExpr mkStar (ReExpr re)
 
ReExpr mkLoop (ReExpr re, int lo, int hi)
 
ReExpr mkLoop (ReExpr re, int lo)
 
ReExpr mkPlus (ReExpr re)
 
ReExpr mkOption (ReExpr re)
 
ReExpr mkComplement (ReExpr re)
 
ReExpr mkConcat (ReExpr...t)
 
ReExpr mkUnion (ReExpr...t)
 
ReExpr mkIntersect (ReExpr...t)
 
ReExpr mkEmptyRe (Sort s)
 
ReExpr mkFullRe (Sort s)
 
ReExpr mkRange (SeqExpr lo, SeqExpr hi)
 
BoolExpr mkAtMost (BoolExpr[] args, int k)
 
BoolExpr mkAtLeast (BoolExpr[] args, int k)
 
BoolExpr mkPBLe (int[] coeffs, BoolExpr[] args, int k)
 
BoolExpr mkPBGe (int[] coeffs, BoolExpr[] args, int k)
 
BoolExpr mkPBEq (int[] coeffs, BoolExpr[] args, int k)
 
Expr mkNumeral (String v, Sort ty)
 
Expr mkNumeral (int v, Sort ty)
 
Expr mkNumeral (long v, Sort ty)
 
RatNum mkReal (int num, int den)
 
RatNum mkReal (String v)
 
RatNum mkReal (int v)
 
RatNum mkReal (long v)
 
IntNum mkInt (String v)
 
IntNum mkInt (int v)
 
IntNum mkInt (long v)
 
BitVecNum mkBV (String v, int size)
 
BitVecNum mkBV (int v, int size)
 
BitVecNum mkBV (long v, int size)
 
Quantifier mkForall (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkForall (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkExists (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkExists (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkQuantifier (boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Lambda mkLambda (Sort[] sorts, Symbol[] names, Expr body)
 
Lambda mkLambda (Expr[] boundConstants, Expr body)
 
void setPrintMode (Z3_ast_print_mode value)
 
String benchmarkToSMTString (String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
 
BoolExpr[] parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
 
BoolExpr[] parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
 
Goal mkGoal (boolean models, boolean unsatCores, boolean proofs)
 
Params mkParams ()
 
int getNumTactics ()
 
String[] getTacticNames ()
 
String getTacticDescription (String name)
 
Tactic mkTactic (String name)
 
Tactic andThen (Tactic t1, Tactic t2, Tactic...ts)
 
Tactic then (Tactic t1, Tactic t2, Tactic...ts)
 
Tactic orElse (Tactic t1, Tactic t2)
 
Tactic tryFor (Tactic t, int ms)
 
Tactic when (Probe p, Tactic t)
 
Tactic cond (Probe p, Tactic t1, Tactic t2)
 
Tactic repeat (Tactic t, int max)
 
Tactic skip ()
 
Tactic fail ()
 
Tactic failIf (Probe p)
 
Tactic failIfNotDecided ()
 
Tactic usingParams (Tactic t, Params p)
 
Tactic with (Tactic t, Params p)
 
Tactic parOr (Tactic...t)
 
Tactic parAndThen (Tactic t1, Tactic t2)
 
void interrupt ()
 
int getNumProbes ()
 
String[] getProbeNames ()
 
String getProbeDescription (String name)
 
Probe mkProbe (String name)
 
Probe constProbe (double val)
 
Probe lt (Probe p1, Probe p2)
 
Probe gt (Probe p1, Probe p2)
 
Probe le (Probe p1, Probe p2)
 
Probe ge (Probe p1, Probe p2)
 
Probe eq (Probe p1, Probe p2)
 
Probe and (Probe p1, Probe p2)
 
Probe or (Probe p1, Probe p2)
 
Probe not (Probe p)
 
Solver mkSolver ()
 
Solver mkSolver (Symbol logic)
 
Solver mkSolver (String logic)
 
Solver mkSimpleSolver ()
 
Solver mkSolver (Tactic t)
 
Fixedpoint mkFixedpoint ()
 
Optimize mkOptimize ()
 
FPRMSort mkFPRoundingModeSort ()
 
FPRMExpr mkFPRoundNearestTiesToEven ()
 
FPRMNum mkFPRNE ()
 
FPRMNum mkFPRoundNearestTiesToAway ()
 
FPRMNum mkFPRNA ()
 
FPRMNum mkFPRoundTowardPositive ()
 
FPRMNum mkFPRTP ()
 
FPRMNum mkFPRoundTowardNegative ()
 
FPRMNum mkFPRTN ()
 
FPRMNum mkFPRoundTowardZero ()
 
FPRMNum mkFPRTZ ()
 
FPSort mkFPSort (int ebits, int sbits)
 
FPSort mkFPSortHalf ()
 
FPSort mkFPSort16 ()
 
FPSort mkFPSortSingle ()
 
FPSort mkFPSort32 ()
 
FPSort mkFPSortDouble ()
 
FPSort mkFPSort64 ()
 
FPSort mkFPSortQuadruple ()
 
FPSort mkFPSort128 ()
 
FPNum mkFPNaN (FPSort s)
 
FPNum mkFPInf (FPSort s, boolean negative)
 
FPNum mkFPZero (FPSort s, boolean negative)
 
FPNum mkFPNumeral (float v, FPSort s)
 
FPNum mkFPNumeral (double v, FPSort s)
 
FPNum mkFPNumeral (int v, FPSort s)
 
FPNum mkFPNumeral (boolean sgn, int exp, int sig, FPSort s)
 
FPNum mkFPNumeral (boolean sgn, long exp, long sig, FPSort s)
 
FPNum mkFP (float v, FPSort s)
 
FPNum mkFP (double v, FPSort s)
 
FPNum mkFP (int v, FPSort s)
 
FPNum mkFP (boolean sgn, int exp, int sig, FPSort s)
 
FPNum mkFP (boolean sgn, long exp, long sig, FPSort s)
 
FPExpr mkFPAbs (FPExpr t)
 
FPExpr mkFPNeg (FPExpr t)
 
FPExpr mkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
 
FPExpr mkFPSqrt (FPRMExpr rm, FPExpr t)
 
FPExpr mkFPRem (FPExpr t1, FPExpr t2)
 
FPExpr mkFPRoundToIntegral (FPRMExpr rm, FPExpr t)
 
FPExpr mkFPMin (FPExpr t1, FPExpr t2)
 
FPExpr mkFPMax (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPLEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPLt (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPGEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPGt (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPIsNormal (FPExpr t)
 
BoolExpr mkFPIsSubnormal (FPExpr t)
 
BoolExpr mkFPIsZero (FPExpr t)
 
BoolExpr mkFPIsInfinite (FPExpr t)
 
BoolExpr mkFPIsNaN (FPExpr t)
 
BoolExpr mkFPIsNegative (FPExpr t)
 
BoolExpr mkFPIsPositive (FPExpr t)
 
FPExpr mkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
 
FPExpr mkFPToFP (BitVecExpr bv, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, FPExpr t, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, RealExpr t, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
 
FPExpr mkFPToFP (FPSort s, FPRMExpr rm, FPExpr t)
 
BitVecExpr mkFPToBV (FPRMExpr rm, FPExpr t, int sz, boolean signed)
 
RealExpr mkFPToReal (FPExpr t)
 
BitVecExpr mkFPToIEEEBV (FPExpr t)
 
BitVecExpr mkFPToFP (FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
 
AST wrapAST (long nativeObject)
 
long unwrapAST (AST a)
 
String SimplifyHelp ()
 
ParamDescrs getSimplifyParameterDescriptions ()
 
void updateParamValue (String id, String value)
 
IDecRefQueue< ConstructorgetConstructorDRQ ()
 
IDecRefQueue< ConstructorListgetConstructorListDRQ ()
 
IDecRefQueue< ASTgetASTDRQ ()
 
IDecRefQueue< ASTMap > getASTMapDRQ ()
 
IDecRefQueue< ASTVectorgetASTVectorDRQ ()
 
IDecRefQueue< ApplyResultgetApplyResultDRQ ()
 
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ ()
 
IDecRefQueue< FuncInterpgetFuncInterpDRQ ()
 
IDecRefQueue< GoalgetGoalDRQ ()
 
IDecRefQueue< ModelgetModelDRQ ()
 
IDecRefQueue< ParamsgetParamsDRQ ()
 
IDecRefQueue< ParamDescrsgetParamDescrsDRQ ()
 
IDecRefQueue< ProbegetProbeDRQ ()
 
IDecRefQueue< SolvergetSolverDRQ ()
 
IDecRefQueue< StatisticsgetStatisticsDRQ ()
 
IDecRefQueue< TacticgetTacticDRQ ()
 
IDecRefQueue< FixedpointgetFixedpointDRQ ()
 
IDecRefQueue< OptimizegetOptimizeDRQ ()
 
void close ()
 

Protected Member Functions

 Context (long m_ctx)
 

Detailed Description

The main interaction with Z3 happens via the Context. For applications that spawn an unbounded number of contexts, the proper use is within a try-with-resources scope so that the Context object gets garbage collected in a predictable way. Contexts maintain all data-structures related to terms and formulas that are created relative to them.

Definition at line 35 of file Context.java.

Constructor & Destructor Documentation

Context ( )
inline

Definition at line 39 of file Context.java.

39  {
40  synchronized (creation_lock) {
41  m_ctx = Native.mkContextRc(0);
42  init();
43  }
44  }
Context ( long  m_ctx)
inlineprotected

Definition at line 46 of file Context.java.

46  {
47  synchronized (creation_lock) {
48  this.m_ctx = m_ctx;
49  init();
50  }
51  }
Context ( Map< String, String >  settings)
inline

Constructor. Remarks: The following parameters can be set:

  • proof (Boolean) Enable proof generation
  • debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
  • trace (Boolean) Tracing support for VCC
  • trace_file_name (String) Trace out file for VCC traces
  • timeout (unsigned) default timeout (in milliseconds) used for solvers
  • well_sorted_check type checker
  • auto_config use heuristics to automatically select solver and configure it
  • model model generation for solvers, this parameter can be overwritten when creating a solver
  • model_validate validate models produced by solvers
  • unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver Note that in previous versions of Z3, this constructor was also used to set global and module parameters. For this purpose we should now use
    Global.setParameter

Definition at line 71 of file Context.java.

71  {
72  synchronized (creation_lock) {
73  long cfg = Native.mkConfig();
74  for (Map.Entry<String, String> kv : settings.entrySet()) {
75  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
76  }
77  m_ctx = Native.mkContextRc(cfg);
78  Native.delConfig(cfg);
79  init();
80  }
81  }
def String
Definition: z3py.py:10043
def Map
Definition: z3py.py:4459

Member Function Documentation

Probe and ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value

p1

and

p2

evaluate to

true

.

Definition at line 3028 of file Context.java.

3029  {
3030  checkContextMatch(p1);
3031  checkContextMatch(p2);
3032  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
3033  p2.getNativeObject()));
3034  }
Tactic andThen ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
)
inline

Create a tactic that applies

t1

to a Goal and then

t2

to every subgoal produced by

t1

Definition at line 2724 of file Context.java.

Referenced by Context.then().

2726  {
2727  checkContextMatch(t1);
2728  checkContextMatch(t2);
2729  checkContextMatch(ts);
2730 
2731  long last = 0;
2732  if (ts != null && ts.length > 0)
2733  {
2734  last = ts[ts.length - 1].getNativeObject();
2735  for (int i = ts.length - 2; i >= 0; i--) {
2736  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2737  last);
2738  }
2739  }
2740  if (last != 0)
2741  {
2742  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2743  return new Tactic(this, Native.tacticAndThen(nCtx(),
2744  t1.getNativeObject(), last));
2745  } else
2746  return new Tactic(this, Native.tacticAndThen(nCtx(),
2747  t1.getNativeObject(), t2.getNativeObject()));
2748  }
String benchmarkToSMTString ( String  name,
String  logic,
String  status,
String  attributes,
BoolExpr[]  assumptions,
BoolExpr  formula 
)
inline

Convert a benchmark into an SMT-LIB formatted string.

Parameters
nameName of the benchmark. The argument is optional.
logicThe benchmark logic.
statusThe status string (sat, unsat, or unknown)
attributesOther attributes, such as source, difficulty or category.
assumptionsAuxiliary assumptions.
formulaFormula to be checked for consistency in conjunction with assumptions.
Returns
A string representation of the benchmark.

Definition at line 2599 of file Context.java.

2602  {
2603 
2604  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2605  attributes, assumptions.length,
2606  AST.arrayToNative(assumptions), formula.getNativeObject());
2607  }
void close ( )
inline

Disposes of the context.

Definition at line 4110 of file Context.java.

4111  {
4112  m_AST_DRQ.forceClear(this);
4113  m_ASTMap_DRQ.forceClear(this);
4114  m_ASTVector_DRQ.forceClear(this);
4115  m_ApplyResult_DRQ.forceClear(this);
4116  m_FuncEntry_DRQ.forceClear(this);
4117  m_FuncInterp_DRQ.forceClear(this);
4118  m_Goal_DRQ.forceClear(this);
4119  m_Model_DRQ.forceClear(this);
4120  m_Params_DRQ.forceClear(this);
4121  m_Probe_DRQ.forceClear(this);
4122  m_Solver_DRQ.forceClear(this);
4123  m_Optimize_DRQ.forceClear(this);
4124  m_Statistics_DRQ.forceClear(this);
4125  m_Tactic_DRQ.forceClear(this);
4126  m_Fixedpoint_DRQ.forceClear(this);
4127 
4128  m_boolSort = null;
4129  m_intSort = null;
4130  m_realSort = null;
4131  m_stringSort = null;
4132 
4133  synchronized (creation_lock) {
4134  Native.delContext(m_ctx);
4135  }
4136  }
Tactic cond ( Probe  p,
Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that applies

t1

to a given goal if the probe

p

evaluates to true and

t2

otherwise.

Definition at line 2806 of file Context.java.

2807  {
2808  checkContextMatch(p);
2809  checkContextMatch(t1);
2810  checkContextMatch(t2);
2811  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2812  t1.getNativeObject(), t2.getNativeObject()));
2813  }
Probe constProbe ( double  val)
inline

Create a probe that always evaluates to

val

.

Definition at line 2958 of file Context.java.

2959  {
2960  return new Probe(this, Native.probeConst(nCtx(), val));
2961  }
Probe eq ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value returned by

p1

is equal to the value returned by

p2

Definition at line 3017 of file Context.java.

3018  {
3019  checkContextMatch(p1);
3020  checkContextMatch(p2);
3021  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
3022  p2.getNativeObject()));
3023  }
Tactic fail ( )
inline

Create a tactic always fails.

Definition at line 2837 of file Context.java.

2838  {
2839  return new Tactic(this, Native.tacticFail(nCtx()));
2840  }
Tactic failIf ( Probe  p)
inline

Create a tactic that fails if the probe

p

evaluates to false.

Definition at line 2846 of file Context.java.

2847  {
2848  checkContextMatch(p);
2849  return new Tactic(this,
2850  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2851  }
Tactic failIfNotDecided ( )
inline

Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false').

Definition at line 2857 of file Context.java.

2858  {
2859  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2860  }
Probe ge ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value returned by

p1

is greater than or equal the value returned by

p2

Definition at line 3005 of file Context.java.

3006  {
3007  checkContextMatch(p1);
3008  checkContextMatch(p2);
3009  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
3010  p2.getNativeObject()));
3011  }
IDecRefQueue<ApplyResult> getApplyResultDRQ ( )
inline

Definition at line 4041 of file Context.java.

4042  {
4043  return m_ApplyResult_DRQ;
4044  }
IDecRefQueue<AST> getASTDRQ ( )
inline

Definition at line 4026 of file Context.java.

4027  {
4028  return m_AST_DRQ;
4029  }
IDecRefQueue<ASTMap> getASTMapDRQ ( )
inline

Definition at line 4031 of file Context.java.

4032  {
4033  return m_ASTMap_DRQ;
4034  }
IDecRefQueue<ASTVector> getASTVectorDRQ ( )
inline

Definition at line 4036 of file Context.java.

4037  {
4038  return m_ASTVector_DRQ;
4039  }
BoolSort getBoolSort ( )
inline

Retrieves the Boolean sort of the context.

Definition at line 127 of file Context.java.

Referenced by Context.mkBoolConst().

128  {
129  if (m_boolSort == null) {
130  m_boolSort = new BoolSort(this);
131  }
132  return m_boolSort;
133  }
def BoolSort
Definition: z3py.py:1523
IDecRefQueue<Constructor> getConstructorDRQ ( )
inline

Definition at line 4018 of file Context.java.

4018  {
4019  return m_Constructor_DRQ;
4020  }
IDecRefQueue<ConstructorList> getConstructorListDRQ ( )
inline

Definition at line 4022 of file Context.java.

4022  {
4023  return m_ConstructorList_DRQ;
4024  }
IDecRefQueue<Fixedpoint> getFixedpointDRQ ( )
inline

Definition at line 4096 of file Context.java.

4097  {
4098  return m_Fixedpoint_DRQ;
4099  }
IDecRefQueue<FuncInterp.Entry> getFuncEntryDRQ ( )
inline

Definition at line 4046 of file Context.java.

4047  {
4048  return m_FuncEntry_DRQ;
4049  }
IDecRefQueue<FuncInterp> getFuncInterpDRQ ( )
inline

Definition at line 4051 of file Context.java.

4052  {
4053  return m_FuncInterp_DRQ;
4054  }
IDecRefQueue<Goal> getGoalDRQ ( )
inline

Definition at line 4056 of file Context.java.

4057  {
4058  return m_Goal_DRQ;
4059  }
IntSort getIntSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 138 of file Context.java.

Referenced by Context.mkInt(), and Context.mkIntConst().

139  {
140  if (m_intSort == null) {
141  m_intSort = new IntSort(this);
142  }
143  return m_intSort;
144  }
def IntSort
Definition: z3py.py:2890
IDecRefQueue<Model> getModelDRQ ( )
inline

Definition at line 4061 of file Context.java.

4062  {
4063  return m_Model_DRQ;
4064  }
int getNumProbes ( )
inline

The number of supported Probes.

Definition at line 2920 of file Context.java.

Referenced by Context.getProbeNames().

2921  {
2922  return Native.getNumProbes(nCtx());
2923  }
int getNumTactics ( )
inline

The number of supported tactics.

Definition at line 2685 of file Context.java.

Referenced by Context.getTacticNames().

2686  {
2687  return Native.getNumTactics(nCtx());
2688  }
IDecRefQueue<Optimize> getOptimizeDRQ ( )
inline

Definition at line 4101 of file Context.java.

4102  {
4103  return m_Optimize_DRQ;
4104  }
IDecRefQueue<ParamDescrs> getParamDescrsDRQ ( )
inline

Definition at line 4071 of file Context.java.

4072  {
4073  return m_ParamDescrs_DRQ;
4074  }
IDecRefQueue<Params> getParamsDRQ ( )
inline

Definition at line 4066 of file Context.java.

4067  {
4068  return m_Params_DRQ;
4069  }
String getProbeDescription ( String  name)
inline

Returns a string containing a description of the probe with the given name.

Definition at line 2942 of file Context.java.

2943  {
2944  return Native.probeGetDescr(nCtx(), name);
2945  }
IDecRefQueue<Probe> getProbeDRQ ( )
inline

Definition at line 4076 of file Context.java.

4077  {
4078  return m_Probe_DRQ;
4079  }
String [] getProbeNames ( )
inline

The names of all supported Probes.

Definition at line 2928 of file Context.java.

2929  {
2930 
2931  int n = getNumProbes();
2932  String[] res = new String[n];
2933  for (int i = 0; i < n; i++)
2934  res[i] = Native.getProbeName(nCtx(), i);
2935  return res;
2936  }
def String
Definition: z3py.py:10043
RealSort getRealSort ( )
inline

Retrieves the Real sort of the context.

Definition at line 149 of file Context.java.

Referenced by Context.mkReal(), and Context.mkRealConst().

150  {
151  if (m_realSort == null) {
152  m_realSort = new RealSort(this);
153  }
154  return m_realSort;
155  }
def RealSort
Definition: z3py.py:2906
ParamDescrs getSimplifyParameterDescriptions ( )
inline

Retrieves parameter descriptions for simplifier.

Definition at line 3947 of file Context.java.

3948  {
3949  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3950  }
IDecRefQueue<Solver> getSolverDRQ ( )
inline

Definition at line 4081 of file Context.java.

4082  {
4083  return m_Solver_DRQ;
4084  }
IDecRefQueue<Statistics> getStatisticsDRQ ( )
inline

Definition at line 4086 of file Context.java.

4087  {
4088  return m_Statistics_DRQ;
4089  }
SeqSort getStringSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 168 of file Context.java.

169  {
170  if (m_stringSort == null) {
171  m_stringSort = mkStringSort();
172  }
173  return m_stringSort;
174  }
String getTacticDescription ( String  name)
inline

Returns a string containing a description of the tactic with the given name.

Definition at line 2707 of file Context.java.

2708  {
2709  return Native.tacticGetDescr(nCtx(), name);
2710  }
IDecRefQueue<Tactic> getTacticDRQ ( )
inline

Definition at line 4091 of file Context.java.

4092  {
4093  return m_Tactic_DRQ;
4094  }
String [] getTacticNames ( )
inline

The names of all supported tactics.

Definition at line 2693 of file Context.java.

2694  {
2695 
2696  int n = getNumTactics();
2697  String[] res = new String[n];
2698  for (int i = 0; i < n; i++)
2699  res[i] = Native.getTacticName(nCtx(), i);
2700  return res;
2701  }
def String
Definition: z3py.py:10043
Probe gt ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value returned by

p1

is greater than the value returned by

p2

Definition at line 2979 of file Context.java.

2980  {
2981  checkContextMatch(p1);
2982  checkContextMatch(p2);
2983  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2984  p2.getNativeObject()));
2985  }
void interrupt ( )
inline

Interrupt the execution of a Z3 procedure. Remarks: This procedure can be used to interrupt: solvers, simplifiers and tactics.

Definition at line 2912 of file Context.java.

2913  {
2914  Native.interrupt(nCtx());
2915  }
SeqExpr intToString ( Expr  e)
inline

Convert an integer expression to a string.

Definition at line 1983 of file Context.java.

1984  {
1985  return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
1986  }
Probe le ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value returned by

p1

is less than or equal the value returned by

p2

Definition at line 2992 of file Context.java.

2993  {
2994  checkContextMatch(p1);
2995  checkContextMatch(p2);
2996  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2997  p2.getNativeObject()));
2998  }
Probe lt ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value returned by

p1

is less than the value returned by

p2

Definition at line 2967 of file Context.java.

2968  {
2969  checkContextMatch(p1);
2970  checkContextMatch(p2);
2971  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2972  p2.getNativeObject()));
2973  }
ArithExpr mkAdd ( ArithExpr...  t)
inline

Create an expression representing

t[0] + t[1] + ...

.

Definition at line 800 of file Context.java.

801  {
802  checkContextMatch(t);
803  return (ArithExpr) Expr.create(this,
804  Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
805  }
BoolExpr mkAnd ( BoolExpr...  t)
inline

Create an expression representing

t[0] and t[1] and ...

.

Definition at line 780 of file Context.java.

Referenced by Goal.AsBoolExpr().

781  {
782  checkContextMatch(t);
783  return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
784  AST.arrayToNative(t)));
785  }
Expr mkApp ( FuncDecl  f,
Expr...  args 
)
inline

Create a new function application.

Definition at line 667 of file Context.java.

Referenced by EnumSort.getConst(), EnumSort.getConsts(), ListSort.getNil(), and Context.mkConst().

668  {
669  checkContextMatch(f);
670  checkContextMatch(args);
671  return Expr.create(this, f, args);
672  }
ArrayExpr mkArrayConst ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1655 of file Context.java.

1657  {
1658  return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1659  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:220
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
ArrayExpr mkArrayConst ( String  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1664 of file Context.java.

1666  {
1667  return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1668  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
IntSymbol mkSymbol(int i)
Definition: Context.java:93
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:220
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
Expr mkArrayExt ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.

Definition at line 1820 of file Context.java.

1821  {
1822  checkContextMatch(arg1);
1823  checkContextMatch(arg2);
1824  return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
1825  }
ArraySort mkArraySort ( Sort  domain,
Sort  range 
)
inline

Create a new array sort.

Definition at line 220 of file Context.java.

Referenced by Context.mkArrayConst().

221  {
222  checkContextMatch(domain);
223  checkContextMatch(range);
224  return new ArraySort(this, domain, range);
225  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
def ArraySort
Definition: z3py.py:4351
ArraySort mkArraySort ( Sort[]  domains,
Sort  range 
)
inline

Create a new array sort.

Definition at line 231 of file Context.java.

232  {
233  checkContextMatch(domains);
234  checkContextMatch(range);
235  return new ArraySort(this, domains, range);
236  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
def ArraySort
Definition: z3py.py:4351
SeqExpr mkAt ( SeqExpr  s,
IntExpr  index 
)
inline

Retrieve sequence of length one at index.

Definition at line 2045 of file Context.java.

2046  {
2047  checkContextMatch(s, index);
2048  return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
2049  }
BoolExpr mkAtLeast ( BoolExpr[]  args,
int  k 
)
inline

Create an at-least-k constraint.

Definition at line 2216 of file Context.java.

2217  {
2218  checkContextMatch(args);
2219  return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
2220  }
BoolExpr mkAtMost ( BoolExpr[]  args,
int  k 
)
inline

Create an at-most-k constraint.

Definition at line 2207 of file Context.java.

2208  {
2209  checkContextMatch(args);
2210  return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
2211  }
BitVecSort mkBitVecSort ( int  size)
inline

Create a new bit-vector sort.

Definition at line 212 of file Context.java.

Referenced by Context.mkBV(), and Context.mkBVConst().

213  {
214  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
215  }
def BitVecSort
Definition: z3py.py:3723
BoolExpr mkBool ( boolean  value)
inline

Creates a Boolean value.

Definition at line 693 of file Context.java.

694  {
695  return value ? mkTrue() : mkFalse();
696  }
BoolExpr mkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 603 of file Context.java.

604  {
605  return (BoolExpr) mkConst(name, getBoolSort());
606  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
BoolExpr mkBoolConst ( String  name)
inline

Create a Boolean constant.

Definition at line 611 of file Context.java.

612  {
613  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
614  }
IntSymbol mkSymbol(int i)
Definition: Context.java:93
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
BoolSort mkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 160 of file Context.java.

161  {
162  return new BoolSort(this);
163  }
def BoolSort
Definition: z3py.py:1523
Expr mkBound ( int  index,
Sort  ty 
)
inline

Creates a new bound variable.

Parameters
indexThe de-Bruijn index of the variable
tyThe sort of the variable

Definition at line 537 of file Context.java.

538  {
539  return Expr.create(this,
540  Native.mkBound(nCtx(), index, ty.getNativeObject()));
541  }
BitVecNum mkBV ( String  v,
int  size 
)
inline

Create a bit-vector numeral.

Parameters
vA string representing the value in decimal notation.
sizethe size of the bit-vector

Definition at line 2400 of file Context.java.

2401  {
2402  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2403  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2261
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212
BitVecNum mkBV ( int  v,
int  size 
)
inline

Create a bit-vector numeral.

Parameters
vvalue of the numeral.
sizethe size of the bit-vector

Definition at line 2410 of file Context.java.

2411  {
2412  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2413  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2261
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212
BitVecNum mkBV ( long  v,
int  size 
)
inline

Create a bit-vector numeral.

Parameters
vvalue of the numeral. *
sizethe size of the bit-vector

Definition at line 2420 of file Context.java.

2421  {
2422  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2423  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2261
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212
IntExpr mkBV2Int ( BitVecExpr  t,
boolean  signed 
)
inline

Create an integer from the bit-vector argument

t

. Remarks: If is_signed is false, then the bit-vector t1 is treated as unsigned. So the result is non-negative and in the range

[0..2^N-1]

, where N are the number of bits in

t

. If is_signed is true, t1 is treated as a signed bit-vector.

NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The argument must be of bit-vector sort.

Definition at line 1535 of file Context.java.

1536  {
1537  checkContextMatch(t);
1538  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1539  (signed)));
1540  }
BitVecExpr mkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement addition. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1098 of file Context.java.

1099  {
1100  checkContextMatch(t1);
1101  checkContextMatch(t2);
1102  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1103  t1.getNativeObject(), t2.getNativeObject()));
1104  }
BoolExpr mkBVAddNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
)
inline

Create a predicate that checks that the bit-wise addition does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1547 of file Context.java.

1549  {
1550  checkContextMatch(t1);
1551  checkContextMatch(t2);
1552  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1553  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1554  }
BoolExpr mkBVAddNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Create a predicate that checks that the bit-wise addition does not underflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1561 of file Context.java.

1563  {
1564  checkContextMatch(t1);
1565  checkContextMatch(t2);
1566  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1567  t1.getNativeObject(), t2.getNativeObject()));
1568  }
BitVecExpr mkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise conjunction. Remarks: The arguments must have a bit-vector sort.

Definition at line 1009 of file Context.java.

1010  {
1011  checkContextMatch(t1);
1012  checkContextMatch(t2);
1013  return new BitVecExpr(this, Native.mkBvand(nCtx(),
1014  t1.getNativeObject(), t2.getNativeObject()));
1015  }
BitVecExpr mkBVASHR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Arithmetic shift right Remarks: It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The arguments must have a bit-vector sort.

Definition at line 1443 of file Context.java.

1444  {
1445  checkContextMatch(t1);
1446  checkContextMatch(t2);
1447  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1448  t1.getNativeObject(), t2.getNativeObject()));
1449  }
BitVecExpr mkBVConst ( Symbol  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 651 of file Context.java.

652  {
653  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
654  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
BitVecExpr mkBVConst ( String  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 659 of file Context.java.

660  {
661  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
662  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
BitVecExpr mkBVLSHR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Logical shift right Remarks: It is equivalent to unsigned division by

2^x

where x is the value of

t2

.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The arguments must have a bit-vector sort.

Definition at line 1423 of file Context.java.

1424  {
1425  checkContextMatch(t1);
1426  checkContextMatch(t2);
1427  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1428  t1.getNativeObject(), t2.getNativeObject()));
1429  }
BitVecExpr mkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement multiplication. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1124 of file Context.java.

1125  {
1126  checkContextMatch(t1);
1127  checkContextMatch(t2);
1128  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1129  t1.getNativeObject(), t2.getNativeObject()));
1130  }
BoolExpr mkBVMulNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
)
inline

Create a predicate that checks that the bit-wise multiplication does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1629 of file Context.java.

1631  {
1632  checkContextMatch(t1);
1633  checkContextMatch(t2);
1634  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1635  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1636  }
BoolExpr mkBVMulNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Create a predicate that checks that the bit-wise multiplication does not underflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1643 of file Context.java.

1645  {
1646  checkContextMatch(t1);
1647  checkContextMatch(t2);
1648  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1649  t1.getNativeObject(), t2.getNativeObject()));
1650  }
BitVecExpr mkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NAND. Remarks: The arguments must have a bit-vector sort.

Definition at line 1048 of file Context.java.

1049  {
1050  checkContextMatch(t1);
1051  checkContextMatch(t2);
1052  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1053  t1.getNativeObject(), t2.getNativeObject()));
1054  }
BitVecExpr mkBVNeg ( BitVecExpr  t)
inline

Standard two's complement unary minus. Remarks: The arguments must have a bit-vector sort.

Definition at line 1087 of file Context.java.

1088  {
1089  checkContextMatch(t);
1090  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1091  }
BoolExpr mkBVNegNoOverflow ( BitVecExpr  t)
inline

Create a predicate that checks that the bit-wise negation does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1617 of file Context.java.

1618  {
1619  checkContextMatch(t);
1620  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1621  t.getNativeObject()));
1622  }
BitVecExpr mkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NOR. Remarks: The arguments must have a bit-vector sort.

Definition at line 1061 of file Context.java.

1062  {
1063  checkContextMatch(t1);
1064  checkContextMatch(t2);
1065  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1066  t1.getNativeObject(), t2.getNativeObject()));
1067  }
BitVecExpr mkBVNot ( BitVecExpr  t)
inline

Bitwise negation. Remarks: The argument must have a bit-vector sort.

Definition at line 974 of file Context.java.

975  {
976  checkContextMatch(t);
977  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
978  }
BitVecExpr mkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise disjunction. Remarks: The arguments must have a bit-vector sort.

Definition at line 1022 of file Context.java.

1023  {
1024  checkContextMatch(t1);
1025  checkContextMatch(t2);
1026  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1027  t2.getNativeObject()));
1028  }
BitVecExpr mkBVRedAND ( BitVecExpr  t)
inline

Take conjunction of bits in a vector, return vector of length 1.

Remarks: The argument must have a bit-vector sort.

Definition at line 985 of file Context.java.

986  {
987  checkContextMatch(t);
988  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
989  t.getNativeObject()));
990  }
BitVecExpr mkBVRedOR ( BitVecExpr  t)
inline

Take disjunction of bits in a vector, return vector of length 1.

Remarks: The argument must have a bit-vector sort.

Definition at line 997 of file Context.java.

998  {
999  checkContextMatch(t);
1000  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
1001  t.getNativeObject()));
1002  }
BitVecExpr mkBVRotateLeft ( int  i,
BitVecExpr  t 
)
inline

Rotate Left. Remarks: Rotate bits of t to the left i times. The argument

t

must have a bit-vector sort.

Definition at line 1456 of file Context.java.

1457  {
1458  checkContextMatch(t);
1459  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1460  t.getNativeObject()));
1461  }
BitVecExpr mkBVRotateLeft ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Rotate Left. Remarks: Rotate bits of

t1

to the left

t2

times. The arguments must have the same bit-vector sort.

Definition at line 1481 of file Context.java.

1483  {
1484  checkContextMatch(t1);
1485  checkContextMatch(t2);
1486  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1487  t1.getNativeObject(), t2.getNativeObject()));
1488  }
BitVecExpr mkBVRotateRight ( int  i,
BitVecExpr  t 
)
inline

Rotate Right. Remarks: Rotate bits of t to the right i times. The argument

t

must have a bit-vector sort.

Definition at line 1468 of file Context.java.

1469  {
1470  checkContextMatch(t);
1471  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1472  t.getNativeObject()));
1473  }
BitVecExpr mkBVRotateRight ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Rotate Right. Remarks: Rotate bits of

t1

to the right

t2

times. The arguments must have the same bit-vector sort.

Definition at line 1496 of file Context.java.

1498  {
1499  checkContextMatch(t1);
1500  checkContextMatch(t2);
1501  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1502  t1.getNativeObject(), t2.getNativeObject()));
1503  }
BitVecExpr mkBVSDiv ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Signed division. Remarks: It is defined in the following way:

  • The floor of
    t1/t2
    if t2 is different from zero, and
    t1*t2 >= 0
    .
  • The ceiling of
    t1/t2
    if t2 is different from zero, and
    t1*t2 &lt; 0
    .

If

t2

is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1160 of file Context.java.

1161  {
1162  checkContextMatch(t1);
1163  checkContextMatch(t2);
1164  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1165  t1.getNativeObject(), t2.getNativeObject()));
1166  }
BoolExpr mkBVSDivNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Create a predicate that checks that the bit-wise signed division does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1603 of file Context.java.

1605  {
1606  checkContextMatch(t1);
1607  checkContextMatch(t2);
1608  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1609  t1.getNativeObject(), t2.getNativeObject()));
1610  }
BoolExpr mkBVSGE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed greater than or equal to. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1285 of file Context.java.

1286  {
1287  checkContextMatch(t1);
1288  checkContextMatch(t2);
1289  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1290  t2.getNativeObject()));
1291  }
BoolExpr mkBVSGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed greater-than. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1311 of file Context.java.

1312  {
1313  checkContextMatch(t1);
1314  checkContextMatch(t2);
1315  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1316  t2.getNativeObject()));
1317  }
BitVecExpr mkBVSHL ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Shift left. Remarks: It is equivalent to multiplication by

2^x

where x is the value of

t2

.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The arguments must have a bit-vector sort.

Definition at line 1404 of file Context.java.

1405  {
1406  checkContextMatch(t1);
1407  checkContextMatch(t2);
1408  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1409  t1.getNativeObject(), t2.getNativeObject()));
1410  }
BoolExpr mkBVSLE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed less-than or equal to. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1259 of file Context.java.

1260  {
1261  checkContextMatch(t1);
1262  checkContextMatch(t2);
1263  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1264  t2.getNativeObject()));
1265  }
BoolExpr mkBVSLT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed less-than Remarks: The arguments must have the same bit-vector sort.

Definition at line 1233 of file Context.java.

1234  {
1235  checkContextMatch(t1);
1236  checkContextMatch(t2);
1237  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1238  t2.getNativeObject()));
1239  }
BitVecExpr mkBVSMod ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed remainder (sign follows divisor). Remarks: If

t2

is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1207 of file Context.java.

1208  {
1209  checkContextMatch(t1);
1210  checkContextMatch(t2);
1211  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1212  t1.getNativeObject(), t2.getNativeObject()));
1213  }
BitVecExpr mkBVSRem ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Signed remainder. Remarks: It is defined as

t1 - (t1 /s t2) * t2

, where

/s

represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1.

If

t2

is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1193 of file Context.java.

1194  {
1195  checkContextMatch(t1);
1196  checkContextMatch(t2);
1197  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1198  t1.getNativeObject(), t2.getNativeObject()));
1199  }
BitVecExpr mkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement subtraction. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1111 of file Context.java.

1112  {
1113  checkContextMatch(t1);
1114  checkContextMatch(t2);
1115  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1116  t1.getNativeObject(), t2.getNativeObject()));
1117  }
BoolExpr mkBVSubNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Create a predicate that checks that the bit-wise subtraction does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1575 of file Context.java.

1577  {
1578  checkContextMatch(t1);
1579  checkContextMatch(t2);
1580  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1581  t1.getNativeObject(), t2.getNativeObject()));
1582  }
BoolExpr mkBVSubNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
)
inline

Create a predicate that checks that the bit-wise subtraction does not underflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1589 of file Context.java.

1591  {
1592  checkContextMatch(t1);
1593  checkContextMatch(t2);
1594  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1595  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1596  }
BitVecExpr mkBVUDiv ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned division. Remarks: It is defined as the floor of

t1/t2

if t2 is different from zero. If

t2

is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1139 of file Context.java.

1140  {
1141  checkContextMatch(t1);
1142  checkContextMatch(t2);
1143  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1144  t1.getNativeObject(), t2.getNativeObject()));
1145  }
BoolExpr mkBVUGE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater than or equal to. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1272 of file Context.java.

1273  {
1274  checkContextMatch(t1);
1275  checkContextMatch(t2);
1276  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1277  t2.getNativeObject()));
1278  }
BoolExpr mkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater-than. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1298 of file Context.java.

1299  {
1300  checkContextMatch(t1);
1301  checkContextMatch(t2);
1302  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1303  t2.getNativeObject()));
1304  }
BoolExpr mkBVULE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned less-than or equal to. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1246 of file Context.java.

1247  {
1248  checkContextMatch(t1);
1249  checkContextMatch(t2);
1250  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1251  t2.getNativeObject()));
1252  }
BoolExpr mkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned less-than Remarks: The arguments must have the same bit-vector sort.

Definition at line 1220 of file Context.java.

1221  {
1222  checkContextMatch(t1);
1223  checkContextMatch(t2);
1224  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1225  t2.getNativeObject()));
1226  }
BitVecExpr mkBVURem ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned remainder. Remarks: It is defined as

t1 - (t1 /u t2) * t2

, where

/u

represents unsigned division. If

t2

is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1175 of file Context.java.

1176  {
1177  checkContextMatch(t1);
1178  checkContextMatch(t2);
1179  return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1180  t1.getNativeObject(), t2.getNativeObject()));
1181  }
BitVecExpr mkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XNOR. Remarks: The arguments must have a bit-vector sort.

Definition at line 1074 of file Context.java.

1075  {
1076  checkContextMatch(t1);
1077  checkContextMatch(t2);
1078  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1079  t1.getNativeObject(), t2.getNativeObject()));
1080  }
BitVecExpr mkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XOR. Remarks: The arguments must have a bit-vector sort.

Definition at line 1035 of file Context.java.

1036  {
1037  checkContextMatch(t1);
1038  checkContextMatch(t2);
1039  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1040  t1.getNativeObject(), t2.getNativeObject()));
1041  }
ReExpr mkComplement ( ReExpr  re)
inline

Create the complement regular expression.

Definition at line 2145 of file Context.java.

2146  {
2147  checkContextMatch(re);
2148  return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
2149  }
BitVecExpr mkConcat ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bit-vector concatenation. Remarks: The arguments must have a bit-vector sort.

Returns
The result is a bit-vector of size
n1+n2
, where
n1
(
n2
) is the size of
t1
(
t2
).

Definition at line 1329 of file Context.java.

1330  {
1331  checkContextMatch(t1);
1332  checkContextMatch(t2);
1333  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1334  t1.getNativeObject(), t2.getNativeObject()));
1335  }
SeqExpr mkConcat ( SeqExpr...  t)
inline

Concatenate sequences.

Definition at line 1999 of file Context.java.

2000  {
2001  checkContextMatch(t);
2002  return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
2003  }
ReExpr mkConcat ( ReExpr...  t)
inline

Create the concatenation of regular languages.

Definition at line 2154 of file Context.java.

2155  {
2156  checkContextMatch(t);
2157  return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2158  }
Expr mkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort

and named

name

.

Definition at line 560 of file Context.java.

Referenced by Context.mkArrayConst(), Context.mkBoolConst(), Context.mkBVConst(), Context.mkConst(), Context.mkIntConst(), and Context.mkRealConst().

561  {
562  checkContextMatch(name);
563  checkContextMatch(range);
564 
565  return Expr.create(
566  this,
567  Native.mkConst(nCtx(), name.getNativeObject(),
568  range.getNativeObject()));
569  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
Expr mkConst ( String  name,
Sort  range 
)
inline

Creates a new Constant of sort

and named

name

.

Definition at line 575 of file Context.java.

576  {
577  return mkConst(mkSymbol(name), range);
578  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
IntSymbol mkSymbol(int i)
Definition: Context.java:93
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
Expr mkConst ( FuncDecl  f)
inline

Creates a fresh constant from the FuncDecl

f

.

Parameters
fA decl of a 0-arity function

Definition at line 595 of file Context.java.

596  {
597  return mkApp(f, (Expr[]) null);
598  }
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:667
ArrayExpr mkConstArray ( Sort  domain,
Expr  v 
)
inline

Create a constant array. Remarks: The resulting term is an array, such that a

on an arbitrary index produces the value

v

.

See also
mkArraySort
mkSelect

Definition at line 1774 of file Context.java.

1775  {
1776  checkContextMatch(domain);
1777  checkContextMatch(v);
1778  return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1779  domain.getNativeObject(), v.getNativeObject()));
1780  }
FuncDecl mkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 503 of file Context.java.

504  {
505  checkContextMatch(name);
506  checkContextMatch(range);
507  return new FuncDecl(this, name, null, range);
508  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
FuncDecl mkConstDecl ( String  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 513 of file Context.java.

514  {
515  checkContextMatch(range);
516  return new FuncDecl(this, mkSymbol(name), null, range);
517  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
IntSymbol mkSymbol(int i)
Definition: Context.java:93
Constructor mkConstructor ( Symbol  name,
Symbol  recognizer,
Symbol[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
)
inline

Create a datatype constructor.

Parameters
nameconstructor name
recognizername of recognizer function.
fieldNamesnames of the constructor fields.
sortsfield sorts, 0 if the field sort refers to a recursive sort.
sortRefsreference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared.

Definition at line 345 of file Context.java.

348  {
349  return of(this, name, recognizer, fieldNames, sorts,
350  sortRefs);
351  }
Constructor mkConstructor ( String  name,
String  recognizer,
String[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
)
inline

Create a datatype constructor.

Definition at line 356 of file Context.java.

358  {
359  return of(this, mkSymbol(name), mkSymbol(recognizer),
360  mkSymbols(fieldNames), sorts, sortRefs);
361  }
IntSymbol mkSymbol(int i)
Definition: Context.java:93
BoolExpr mkContains ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence containment of s2 in s1.

Definition at line 2036 of file Context.java.

2037  {
2038  checkContextMatch(s1, s2);
2039  return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2040  }
DatatypeSort mkDatatypeSort ( Symbol  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 366 of file Context.java.

368  {
369  checkContextMatch(name);
370  checkContextMatch(constructors);
371  return new DatatypeSort(this, name, constructors);
372  }
DatatypeSort mkDatatypeSort ( String  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 377 of file Context.java.

379  {
380  checkContextMatch(constructors);
381  return new DatatypeSort(this, mkSymbol(name), constructors);
382  }
IntSymbol mkSymbol(int i)
Definition: Context.java:93
DatatypeSort [] mkDatatypeSorts ( Symbol[]  names,
Constructor  c[][] 
)
inline

Create mutually recursive datatypes.

Parameters
namesnames of datatype sorts
clist of constructors, one list per sort.

Definition at line 389 of file Context.java.

Referenced by Context.mkDatatypeSorts().

391  {
392  checkContextMatch(names);
393  int n = names.length;
394  ConstructorList[] cla = new ConstructorList[n];
395  long[] n_constr = new long[n];
396  for (int i = 0; i < n; i++)
397  {
398  Constructor[] constructor = c[i];
399 
400  checkContextMatch(constructor);
401  cla[i] = new ConstructorList(this, constructor);
402  n_constr[i] = cla[i].getNativeObject();
403  }
404  long[] n_res = new long[n];
405  Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
406  n_constr);
407  DatatypeSort[] res = new DatatypeSort[n];
408  for (int i = 0; i < n; i++)
409  res[i] = new DatatypeSort(this, n_res[i]);
410  return res;
411  }
DatatypeSort [] mkDatatypeSorts ( String[]  names,
Constructor  c[][] 
)
inline

Create mutually recursive data-types.

Definition at line 416 of file Context.java.

418  {
419  return mkDatatypeSorts(mkSymbols(names), c);
420  }
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:389
BoolExpr mkDistinct ( Expr...  args)
inline

Creates a

term.

Definition at line 712 of file Context.java.

713  {
714  checkContextMatch(args);
715  return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
716  AST.arrayToNative(args)));
717  }
ArithExpr mkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 / t2

.

Definition at line 840 of file Context.java.

841  {
842  checkContextMatch(t1);
843  checkContextMatch(t2);
844  return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
845  t1.getNativeObject(), t2.getNativeObject()));
846  }
ReExpr mkEmptyRe ( Sort  s)
inline

Create the empty regular expression.

Definition at line 2181 of file Context.java.

2182  {
2183  return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
2184  }
SeqExpr mkEmptySeq ( Sort  s)
inline

Sequences, Strings and regular expressions. Create the empty sequence.

Definition at line 1957 of file Context.java.

1958  {
1959  checkContextMatch(s);
1960  return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
1961  }
ArrayExpr mkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 1840 of file Context.java.

1841  {
1842  checkContextMatch(domain);
1843  return (ArrayExpr)Expr.create(this,
1844  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1845  }
EnumSort mkEnumSort ( Symbol  name,
Symbol...  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 279 of file Context.java.

281  {
282  checkContextMatch(name);
283  checkContextMatch(enumNames);
284  return new EnumSort(this, name, enumNames);
285  }
def EnumSort
Definition: z3py.py:4974
EnumSort mkEnumSort ( String  name,
String...  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 290 of file Context.java.

292  {
293  return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
294  }
def EnumSort
Definition: z3py.py:4974
IntSymbol mkSymbol(int i)
Definition: Context.java:93
BoolExpr mkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality

x = y

Definition at line 701 of file Context.java.

702  {
703  checkContextMatch(x);
704  checkContextMatch(y);
705  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
706  y.getNativeObject()));
707  }
Quantifier mkExists ( Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Creates an existential quantifier using de-Bruijn indexed variables.

See also
mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)

Definition at line 2476 of file Context.java.

Referenced by Context.mkQuantifier().

2479  {
2480 
2481  return Quantifier.of(this, false, sorts, names, body, weight,
2482  patterns, noPatterns, quantifierID, skolemID);
2483  }
Quantifier mkExists ( Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Creates an existential quantifier using a list of constants that will form the set of bound variables.

See also
mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)

Definition at line 2489 of file Context.java.

2492  {
2493 
2494  return Quantifier.of(this, false, boundConstants, body, weight,
2495  patterns, noPatterns, quantifierID, skolemID);
2496  }
BitVecExpr mkExtract ( int  high,
int  low,
BitVecExpr  t 
)
inline

Bit-vector extraction. Remarks: Extract the bits

high

down to

low

from a bitvector of size

m

to yield a new bitvector of size

n

, where

n = high - low + 1

. The argument

t

must have a bit-vector sort.

Definition at line 1345 of file Context.java.

1347  {
1348  checkContextMatch(t);
1349  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1350  t.getNativeObject()));
1351  }
SeqExpr mkExtract ( SeqExpr  s,
IntExpr  offset,
IntExpr  length 
)
inline

Extract subsequence.

Definition at line 2054 of file Context.java.

2055  {
2056  checkContextMatch(s, offset, length);
2057  return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
2058  }
BoolExpr mkFalse ( )
inline

The false Term.

Definition at line 685 of file Context.java.

Referenced by Context.mkBool().

686  {
687  return new BoolExpr(this, Native.mkFalse(nCtx()));
688  }
FiniteDomainSort mkFiniteDomainSort ( Symbol  name,
long  size 
)
inline

Create a new finite domain sort.

Definition at line 318 of file Context.java.

320  {
321  checkContextMatch(name);
322  return new FiniteDomainSort(this, name, size);
323  }
def FiniteDomainSort
Definition: z3py.py:7188
FiniteDomainSort mkFiniteDomainSort ( String  name,
long  size 
)
inline

Create a new finite domain sort.

Definition at line 328 of file Context.java.

330  {
331  return new FiniteDomainSort(this, mkSymbol(name), size);
332  }
def FiniteDomainSort
Definition: z3py.py:7188
IntSymbol mkSymbol(int i)
Definition: Context.java:93
Fixedpoint mkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3118 of file Context.java.

3119  {
3120  return new Fixedpoint(this);
3121  }
Quantifier mkForall ( Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a universal Quantifier.

Parameters
sortsthe sorts of the bound variables.
namesnames of the bound variables
bodythe body of the quantifier.
weightquantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
patternsarray containing the patterns created using
MkPattern
.
noPatternsarray containing the anti-patterns created using
MkPattern
.
quantifierIDoptional symbol to track quantifier.
skolemIDoptional symbol to track skolem constants.
Returns
Creates a forall formula, where
weight
is the weight,
patterns
is an array of patterns,
sorts
is an array with the sorts of the bound variables,
names
is an array with the 'names' of the bound variables, and
body
is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. Note that the bound variables are de-Bruijn indices created using mkBound. Z3 applies the convention that the last element in
names
and
sorts
refers to the variable with index 0, the second to last element of
names
and
sorts
refers to the variable with index 1, etc.

Definition at line 2450 of file Context.java.

Referenced by Context.mkQuantifier().

2453  {
2454 
2455  return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2456  noPatterns, quantifierID, skolemID);
2457  }
Quantifier mkForall ( Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Creates a universal quantifier using a list of constants that will form the set of bound variables.

See also
mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)

Definition at line 2463 of file Context.java.

2466  {
2467 
2468  return Quantifier.of(this, true, boundConstants, body, weight,
2469  patterns, noPatterns, quantifierID, skolemID);
2470  }
FPNum mkFP ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3412 of file Context.java.

3413  {
3414  return mkFPNumeral(v, s);
3415  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3353
FPNum mkFP ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a double.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3423 of file Context.java.

3424  {
3425  return mkFPNumeral(v, s);
3426  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3353
FPNum mkFP ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3435 of file Context.java.

3436  {
3437  return mkFPNumeral(v, s);
3438  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3353
FPNum mkFP ( boolean  sgn,
int  exp,
int  sig,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a sign bit and two integers.

Parameters
sgnthe sign.
expthe exponent.
sigthe significand.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3448 of file Context.java.

3449  {
3450  return mkFPNumeral(sgn, exp, sig, s);
3451  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3353
FPNum mkFP ( boolean  sgn,
long  exp,
long  sig,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.

Parameters
sgnthe sign.
expthe exponent.
sigthe significand.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3461 of file Context.java.

3462  {
3463  return mkFPNumeral(sgn, exp, sig, s);
3464  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3353
FPExpr mkFP ( BitVecExpr  sgn,
BitVecExpr  sig,
BitVecExpr  exp 
)
inline

Create an expression of FloatingPoint sort from three bit-vector expressions.

Parameters
sgnbit-vector term (of size 1) representing the sign.
sigbit-vector term representing the significand.
expbit-vector term representing the exponent. Remarks: This is the operator named `fp' in the SMT FP theory definition. Note that sgn is required to be a bit-vector of size 1. Significand and exponent are required to be greater than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments.
Exceptions
Z3Exception

Definition at line 3746 of file Context.java.

3747  {
3748  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3749  }
FPExpr mkFPAbs ( FPExpr  t)
inline

Floating-point absolute value

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3472 of file Context.java.

3473  {
3474  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3475  }
FPExpr mkFPAdd ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point addition

Parameters
rmrounding mode term
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3494 of file Context.java.

3495  {
3496  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3497  }
FPExpr mkFPDiv ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point division

Parameters
rmrounding mode term
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3530 of file Context.java.

3531  {
3532  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3533  }
BoolExpr mkFPEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point equality.

Parameters
t1floating-point term
t2floating-point term Remarks: Note that this is IEEE 754 equality (as opposed to standard =).
Exceptions
Z3Exception

Definition at line 3658 of file Context.java.

3659  {
3660  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3661  }
FPExpr mkFPFMA ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2,
FPExpr  t3 
)
inline

Floating-point fused multiply-add

Parameters
rmrounding mode term
t1floating-point term
t2floating-point term
t3floating-point term Remarks: The result is round((t1 * t2) + t3)
Exceptions
Z3Exception

Definition at line 3545 of file Context.java.

3546  {
3547  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3548  }
BoolExpr mkFPGEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3634 of file Context.java.

3635  {
3636  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3637  }
BoolExpr mkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3645 of file Context.java.

3646  {
3647  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3648  }
FPNum mkFPInf ( FPSort  s,
boolean  negative 
)
inline

Create a floating-point infinity of sort s.

Parameters
sFloatingPoint sort.
negativeindicates whether the result should be negative.
Exceptions
Z3Exception

Definition at line 3331 of file Context.java.

3332  {
3333  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3334  }
BoolExpr mkFPIsInfinite ( FPExpr  t)
inline

Predicate indicating whether t is a floating-point number representing +oo or -oo.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3698 of file Context.java.

3699  {
3700  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3701  }
BoolExpr mkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3708 of file Context.java.

3709  {
3710  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3711  }
BoolExpr mkFPIsNegative ( FPExpr  t)
inline

Predicate indicating whether t is a negative floating-point number.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3718 of file Context.java.

3719  {
3720  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3721  }
BoolExpr mkFPIsNormal ( FPExpr  t)
inline

Predicate indicating whether t is a normal floating-point number.\

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3668 of file Context.java.

3669  {
3670  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3671  }
BoolExpr mkFPIsPositive ( FPExpr  t)
inline

Predicate indicating whether t is a positive floating-point number.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3728 of file Context.java.

3729  {
3730  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3731  }
BoolExpr mkFPIsSubnormal ( FPExpr  t)
inline

Predicate indicating whether t is a subnormal floating-point number.\

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3678 of file Context.java.

3679  {
3680  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3681  }
BoolExpr mkFPIsZero ( FPExpr  t)
inline

Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3688 of file Context.java.

3689  {
3690  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3691  }
BoolExpr mkFPLEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3612 of file Context.java.

3613  {
3614  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3615  }
BoolExpr mkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3623 of file Context.java.

3624  {
3625  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3626  }
FPExpr mkFPMax ( FPExpr  t1,
FPExpr  t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3601 of file Context.java.

3602  {
3603  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3604  }
FPExpr mkFPMin ( FPExpr  t1,
FPExpr  t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3590 of file Context.java.

3591  {
3592  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3593  }
FPExpr mkFPMul ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point multiplication

Parameters
rmrounding mode term
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3518 of file Context.java.

3519  {
3520  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3521  }
FPNum mkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3320 of file Context.java.

3321  {
3322  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3323  }
FPExpr mkFPNeg ( FPExpr  t)
inline

Floating-point negation

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3482 of file Context.java.

3483  {
3484  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3485  }
FPNum mkFPNumeral ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3353 of file Context.java.

Referenced by Context.mkFP().

3354  {
3355  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3356  }
FPNum mkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a double.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3364 of file Context.java.

3365  {
3366  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3367  }
FPNum mkFPNumeral ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3375 of file Context.java.

3376  {
3377  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3378  }
FPNum mkFPNumeral ( boolean  sgn,
int  exp,
int  sig,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a sign bit and two integers.

Parameters
sgnthe sign.
expthe exponent.
sigthe significand.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3388 of file Context.java.

3389  {
3390  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3391  }
FPNum mkFPNumeral ( boolean  sgn,
long  exp,
long  sig,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.

Parameters
sgnthe sign.
expthe exponent.
sigthe significand.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3401 of file Context.java.

3402  {
3403  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3404  }
FPExpr mkFPRem ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3567 of file Context.java.

3568  {
3569  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3570  }
FPRMNum mkFPRNA ( )
inline

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Exceptions
Z3Exception

Definition at line 3172 of file Context.java.

3173  {
3174  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3175  }
FPRMNum mkFPRNE ( )
inline

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Exceptions
Z3Exception

Definition at line 3154 of file Context.java.

3155  {
3156  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3157  }
FPRMSort mkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Exceptions
Z3Exception

Definition at line 3136 of file Context.java.

3137  {
3138  return new FPRMSort(this);
3139  }
FPRMNum mkFPRoundNearestTiesToAway ( )
inline

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Exceptions
Z3Exception

Definition at line 3163 of file Context.java.

3164  {
3165  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3166  }
FPRMExpr mkFPRoundNearestTiesToEven ( )
inline

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Exceptions
Z3Exception

Definition at line 3145 of file Context.java.

3146  {
3147  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3148  }
FPExpr mkFPRoundToIntegral ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.

Parameters
rmterm of RoundingMode sort
tfloating-point term
Exceptions
Z3Exception

Definition at line 3579 of file Context.java.

3580  {
3581  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3582  }
FPRMNum mkFPRoundTowardNegative ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.

Exceptions
Z3Exception

Definition at line 3199 of file Context.java.

3200  {
3201  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3202  }
FPRMNum mkFPRoundTowardPositive ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.

Exceptions
Z3Exception

Definition at line 3181 of file Context.java.

3182  {
3183  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3184  }
FPRMNum mkFPRoundTowardZero ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.

Exceptions
Z3Exception

Definition at line 3217 of file Context.java.

3218  {
3219  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3220  }
FPRMNum mkFPRTN ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.

Exceptions
Z3Exception

Definition at line 3208 of file Context.java.

3209  {
3210  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3211  }
FPRMNum mkFPRTP ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.

Exceptions
Z3Exception

Definition at line 3190 of file Context.java.

3191  {
3192  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3193  }
FPRMNum mkFPRTZ ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.

Exceptions
Z3Exception

Definition at line 3226 of file Context.java.

3227  {
3228  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3229  }
FPSort mkFPSort ( int  ebits,
int  sbits 
)
inline

Create a FloatingPoint sort.

Parameters
ebitsexponent bits in the FloatingPoint sort.
sbitssignificand bits in the FloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3237 of file Context.java.

3238  {
3239  return new FPSort(this, ebits, sbits);
3240  }
def FPSort
Definition: z3py.py:9145
FPSort mkFPSort128 ( )
inline

Create the quadruple-precision (128-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3309 of file Context.java.

3310  {
3311  return new FPSort(this, Native.mkFpaSort128(nCtx()));
3312  }
def FPSort
Definition: z3py.py:9145
FPSort mkFPSort16 ( )
inline

Create the half-precision (16-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3255 of file Context.java.

3256  {
3257  return new FPSort(this, Native.mkFpaSort16(nCtx()));
3258  }
def FPSort
Definition: z3py.py:9145
FPSort mkFPSort32 ( )
inline

Create the single-precision (32-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3273 of file Context.java.

3274  {
3275  return new FPSort(this, Native.mkFpaSort32(nCtx()));
3276  }
def FPSort
Definition: z3py.py:9145
FPSort mkFPSort64 ( )
inline

Create the double-precision (64-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3291 of file Context.java.

3292  {
3293  return new FPSort(this, Native.mkFpaSort64(nCtx()));
3294  }
def FPSort
Definition: z3py.py:9145
FPSort mkFPSortDouble ( )
inline

Create the double-precision (64-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3282 of file Context.java.

3283  {
3284  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3285  }
def FPSort
Definition: z3py.py:9145
FPSort mkFPSortHalf ( )
inline

Create the half-precision (16-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3246 of file Context.java.

3247  {
3248  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3249  }
def FPSort
Definition: z3py.py:9145
FPSort mkFPSortQuadruple ( )
inline

Create the quadruple-precision (128-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3300 of file Context.java.

3301  {
3302  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3303  }
def FPSort
Definition: z3py.py:9145
FPSort mkFPSortSingle ( )
inline

Create the single-precision (32-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3264 of file Context.java.

3265  {
3266  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3267  }
def FPSort
Definition: z3py.py:9145
FPExpr mkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term
Exceptions
Z3Exception

Definition at line 3556 of file Context.java.

3557  {
3558  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3559  }
FPExpr mkFPSub ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point subtraction

Parameters
rmrounding mode term
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3506 of file Context.java.

3507  {
3508  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3509  }
BitVecExpr mkFPToBV ( FPRMExpr  rm,
FPExpr  t,
int  sz,
boolean  signed 
)
inline

Conversion of a floating-point term into a bit-vector.

Parameters
rmRoundingMode term.
tFloatingPoint term
szSize of the resulting bit-vector.
signedIndicates whether the result is a signed or unsigned bit-vector. Remarks: Produces a term that represents the conversion of the floating-point term t into a bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, the result will be rounded according to rounding mode rm.
Exceptions
Z3Exception

Definition at line 3847 of file Context.java.

3848  {
3849  if (signed)
3850  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3851  else
3852  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3853  }
FPExpr mkFPToFP ( BitVecExpr  bv,
FPSort  s 
)
inline

Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.

Parameters
bvbit-vector value (of size m).
sFloatingPoint sort (ebits+sbits == m) Remarks: Produces a term that represents the conversion of a bit-vector term bv to a floating-point term of sort s. The bit-vector size of bv (m) must be equal to ebits+sbits of s. The format of the bit-vector is as defined by the IEEE 754-2008 interchange format.
Exceptions
Z3Exception

Definition at line 3762 of file Context.java.

3763  {
3764  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3765  }
FPExpr mkFPToFP ( FPRMExpr  rm,
FPExpr  t,
FPSort  s 
)
inline

Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

Parameters
rmRoundingMode term.
tFloatingPoint term.
sFloatingPoint sort. Remarks: Produces a term that represents the conversion of a floating-point term t to a floating-point term of sort s. If necessary, the result will be rounded according to rounding mode rm.
Exceptions
Z3Exception

Definition at line 3778 of file Context.java.

3779  {
3780  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3781  }
FPExpr mkFPToFP ( FPRMExpr  rm,
RealExpr  t,
FPSort  s 
)
inline

Conversion of a term of real sort into a term of FloatingPoint sort.

Parameters
rmRoundingMode term.
tterm of Real sort.
sFloatingPoint sort. Remarks: Produces a term that represents the conversion of term t of real sort into a floating-point term of sort s. If necessary, the result will be rounded according to rounding mode rm.
Exceptions
Z3Exception

Definition at line 3794 of file Context.java.

3795  {
3796  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3797  }
FPExpr mkFPToFP ( FPRMExpr  rm,
BitVecExpr  t,
FPSort  s,
boolean  signed 
)
inline

Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.

Parameters
rmRoundingMode term.
tterm of bit-vector sort.
sFloatingPoint sort.
signedflag indicating whether t is interpreted as signed or unsigned bit-vector. Remarks: Produces a term that represents the conversion of the bit-vector term t into a floating-point term of sort s. The bit-vector t is taken to be in signed 2's complement format (when signed==true, otherwise unsigned). If necessary, the result will be rounded according to rounding mode rm.
Exceptions
Z3Exception

Definition at line 3812 of file Context.java.

3813  {
3814  if (signed)
3815  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3816  else
3817  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3818  }
FPExpr mkFPToFP ( FPSort  s,
FPRMExpr  rm,
FPExpr  t 
)
inline

Conversion of a floating-point number to another FloatingPoint sort s.

Parameters
sFloatingPoint sort
rmfloating-point rounding mode term
tfloating-point term Remarks: Produces a term that represents the conversion of a floating-point term t to a different FloatingPoint sort s. If necessary, rounding according to rm is applied.
Exceptions
Z3Exception

Definition at line 3830 of file Context.java.

3831  {
3832  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3833  }
BitVecExpr mkFPToFP ( FPRMExpr  rm,
IntExpr  exp,
RealExpr  sig,
FPSort  s 
)
inline

Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.

Parameters
rmRoundingMode term.
expExponent term of Int sort.
sigSignificand term of Real sort.
sFloatingPoint sort. Remarks: Produces a term that represents the conversion of sig * 2^exp into a floating-point term of sort s. If necessary, the result will be rounded according to rounding mode rm.
Exceptions
Z3Exception

Definition at line 3897 of file Context.java.

3898  {
3899  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3900  }
BitVecExpr mkFPToIEEEBV ( FPExpr  t)
inline

Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

Parameters
tFloatingPoint term. Remarks: The size of the resulting bit-vector is automatically determined. Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector representation of that NaN.
Exceptions
Z3Exception

Definition at line 3879 of file Context.java.

3880  {
3881  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3882  }
RealExpr mkFPToReal ( FPExpr  t)
inline

Conversion of a floating-point term into a real-numbered term.

Parameters
tFloatingPoint term Remarks: Produces a term that represents the conversion of the floating-point term t into a real number. Note that this type of conversion will often result in non-linear constraints over real terms.
Exceptions
Z3Exception

Definition at line 3864 of file Context.java.

3865  {
3866  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3867  }
FPNum mkFPZero ( FPSort  s,
boolean  negative 
)
inline

Create a floating-point zero of sort s.

Parameters
sFloatingPoint sort.
negativeindicates whether the result should be negative.
Exceptions
Z3Exception

Definition at line 3342 of file Context.java.

3343  {
3344  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3345  }
Expr mkFreshConst ( String  prefix,
Sort  range 
)
inline

Creates a fresh Constant of sort

and a name prefixed with

prefix

.

Definition at line 584 of file Context.java.

585  {
586  checkContextMatch(range);
587  return Expr.create(this,
588  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
589  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
FuncDecl mkFreshConstDecl ( String  prefix,
Sort  range 
)
inline

Creates a fresh constant function declaration with a name prefixed with

prefix

.

See also
mkFuncDecl(String,Sort,Sort)
mkFuncDecl(String,Sort[],Sort)

Definition at line 525 of file Context.java.

527  {
528  checkContextMatch(range);
529  return new FuncDecl(this, prefix, null, range);
530  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
FuncDecl mkFreshFuncDecl ( String  prefix,
Sort[]  domain,
Sort  range 
)
inline

Creates a fresh function declaration with a name prefixed with

prefix

.

See also
mkFuncDecl(String,Sort,Sort)
mkFuncDecl(String,Sort[],Sort)

Definition at line 492 of file Context.java.

494  {
495  checkContextMatch(domain);
496  checkContextMatch(range);
497  return new FuncDecl(this, prefix, domain, range);
498  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
ReExpr mkFullRe ( Sort  s)
inline

Create the full regular expression.

Definition at line 2189 of file Context.java.

2190  {
2191  return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
2192  }
ArrayExpr mkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 1850 of file Context.java.

1851  {
1852  checkContextMatch(domain);
1853  return (ArrayExpr)Expr.create(this,
1854  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1855  }
FuncDecl mkFuncDecl ( Symbol  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 441 of file Context.java.

443  {
444  checkContextMatch(name);
445  checkContextMatch(domain);
446  checkContextMatch(range);
447  return new FuncDecl(this, name, domain, range);
448  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
FuncDecl mkFuncDecl ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 453 of file Context.java.

455  {
456  checkContextMatch(name);
457  checkContextMatch(domain);
458  checkContextMatch(range);
459  Sort[] q = new Sort[] { domain };
460  return new FuncDecl(this, name, q, range);
461  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
FuncDecl mkFuncDecl ( String  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 466 of file Context.java.

468  {
469  checkContextMatch(domain);
470  checkContextMatch(range);
471  return new FuncDecl(this, mkSymbol(name), domain, range);
472  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
IntSymbol mkSymbol(int i)
Definition: Context.java:93
FuncDecl mkFuncDecl ( String  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 477 of file Context.java.

479  {
480  checkContextMatch(domain);
481  checkContextMatch(range);
482  Sort[] q = new Sort[] { domain };
483  return new FuncDecl(this, mkSymbol(name), q, range);
484  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
IntSymbol mkSymbol(int i)
Definition: Context.java:93
BoolExpr mkGe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &gt;= t2

Definition at line 923 of file Context.java.

924  {
925  checkContextMatch(t1);
926  checkContextMatch(t2);
927  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
928  t2.getNativeObject()));
929  }
Goal mkGoal ( boolean  models,
boolean  unsatCores,
boolean  proofs 
)
inline

Creates a new Goal. Remarks: Note that the Context must have been created with proof generation support if

proofs

is set to true here.

Parameters
modelsIndicates whether model generation should be enabled.
unsatCoresIndicates whether unsat core generation should be enabled.
proofsIndicates whether proof generation should be enabled.

Definition at line 2668 of file Context.java.

2670  {
2671  return new Goal(this, models, unsatCores, proofs);
2672  }
BoolExpr mkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &gt; t2

Definition at line 912 of file Context.java.

913  {
914  checkContextMatch(t1);
915  checkContextMatch(t2);
916  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
917  t2.getNativeObject()));
918  }
BoolExpr mkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 iff t2

.

Definition at line 747 of file Context.java.

748  {
749  checkContextMatch(t1);
750  checkContextMatch(t2);
751  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
752  t2.getNativeObject()));
753  }
BoolExpr mkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 -> t2

.

Definition at line 758 of file Context.java.

759  {
760  checkContextMatch(t1);
761  checkContextMatch(t2);
762  return new BoolExpr(this, Native.mkImplies(nCtx(),
763  t1.getNativeObject(), t2.getNativeObject()));
764  }
IntExpr mkIndexOf ( SeqExpr  s,
SeqExpr  substr,
ArithExpr  offset 
)
inline

Extract index of sub-string starting at offset.

Definition at line 2063 of file Context.java.

2064  {
2065  checkContextMatch(s, substr, offset);
2066  return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
2067  }
BoolExpr mkInRe ( SeqExpr  s,
ReExpr  re 
)
inline

Check for regular expression membership.

Definition at line 2091 of file Context.java.

2092  {
2093  checkContextMatch(s, re);
2094  return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
2095  }
IntNum mkInt ( String  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 2362 of file Context.java.

2363  {
2364 
2365  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2366  .getNativeObject()));
2367  }
IntNum mkInt ( int  v)
inline

Create an integer numeral.

Parameters
vvalue of the numeral.
Returns
A Term with value
v
and sort Integer

Definition at line 2375 of file Context.java.

2376  {
2377 
2378  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2379  .getNativeObject()));
2380  }
IntNum mkInt ( long  v)
inline

Create an integer numeral.

Parameters
vvalue of the numeral.
Returns
A Term with value
v
and sort Integer

Definition at line 2388 of file Context.java.

2389  {
2390 
2391  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2392  .getNativeObject()));
2393  }
BitVecExpr mkInt2BV ( int  n,
IntExpr  t 
)
inline

Create an

n

bit bit-vector from the integer argument

t

. Remarks: NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The argument must be of integer sort.

Definition at line 1514 of file Context.java.

1515  {
1516  checkContextMatch(t);
1517  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1518  t.getNativeObject()));
1519  }
RealExpr mkInt2Real ( IntExpr  t)
inline

Coerce an integer to a real. Remarks: There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.

You can take the floor of a real by creating an auxiliary integer Term

k

and asserting

MakeInt2Real(k) &lt;= t1 &lt; MkInt2Real(k)+1

. The argument must be of integer sort.

Definition at line 941 of file Context.java.

942  {
943  checkContextMatch(t);
944  return new RealExpr(this,
945  Native.mkInt2real(nCtx(), t.getNativeObject()));
946  }
IntExpr mkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 619 of file Context.java.

620  {
621  return (IntExpr) mkConst(name, getIntSort());
622  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
IntExpr mkIntConst ( String  name)
inline

Creates an integer constant.

Definition at line 627 of file Context.java.

628  {
629  return (IntExpr) mkConst(name, getIntSort());
630  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
ReExpr mkIntersect ( ReExpr...  t)
inline

Create the intersection of regular languages.

Definition at line 2172 of file Context.java.

2173  {
2174  checkContextMatch(t);
2175  return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
2176  }
IntSort mkIntSort ( )
inline

Create a new integer sort.

Definition at line 196 of file Context.java.

197  {
198  return new IntSort(this);
199  }
def IntSort
Definition: z3py.py:2890
BoolExpr mkIsInteger ( RealExpr  t)
inline

Creates an expression that checks whether a real number is an integer.

Definition at line 963 of file Context.java.

964  {
965  checkContextMatch(t);
966  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
967  }
Expr mkITE ( BoolExpr  t1,
Expr  t2,
Expr  t3 
)
inline

Create an expression representing an if-then-else:

ite(t1, t2, t3)

.

Parameters
t1An expression with Boolean sort
t2An expression
t3An expression with the same sort as
t2

Definition at line 735 of file Context.java.

736  {
737  checkContextMatch(t1);
738  checkContextMatch(t2);
739  checkContextMatch(t3);
740  return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
741  t2.getNativeObject(), t3.getNativeObject()));
742  }
Lambda mkLambda ( Sort[]  sorts,
Symbol[]  names,
Expr  body 
)
inline

Create a lambda expression.

sorts

is an array with the sorts of the bound variables,

names

is an array with the 'names' of the bound variables, and

body

is the body of the lambda. Note that the bound variables are de-Bruijn indices created using mkBound Z3 applies the convention that the last element in

names

and

sorts

refers to the variable with index 0, the second to last element of

names

and

sorts

refers to the variable with index 1, etc.

Parameters
sortsthe sorts of the bound variables.
namesnames of the bound variables.
bodythe body of the quantifier.

Definition at line 2550 of file Context.java.

2551  {
2552  return Lambda.of(this, sorts, names, body);
2553  }
def Lambda
Definition: z3py.py:2064
Lambda mkLambda ( Expr[]  boundConstants,
Expr  body 
)
inline

Create a lambda expression.

Creates a lambda expression using a list of constants that will form the set of bound variables.

Definition at line 2561 of file Context.java.

2562  {
2563  return Lambda.of(this, boundConstants, body);
2564  }
def Lambda
Definition: z3py.py:2064
BoolExpr mkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &lt;= t2

Definition at line 901 of file Context.java.

902  {
903  checkContextMatch(t1);
904  checkContextMatch(t2);
905  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
906  t2.getNativeObject()));
907  }
IntExpr mkLength ( SeqExpr  s)
inline

Retrieve the length of a given sequence.

Definition at line 2009 of file Context.java.

2010  {
2011  checkContextMatch(s);
2012  return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
2013  }
ListSort mkListSort ( Symbol  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 299 of file Context.java.

300  {
301  checkContextMatch(name);
302  checkContextMatch(elemSort);
303  return new ListSort(this, name, elemSort);
304  }
ListSort mkListSort ( String  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 309 of file Context.java.

310  {
311  checkContextMatch(elemSort);
312  return new ListSort(this, mkSymbol(name), elemSort);
313  }
IntSymbol mkSymbol(int i)
Definition: Context.java:93
ReExpr mkLoop ( ReExpr  re,
int  lo,
int  hi 
)
inline

Take the lower and upper-bounded Kleene star of a regular expression.

Definition at line 2109 of file Context.java.

2110  {
2111  return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
2112  }
ReExpr mkLoop ( ReExpr  re,
int  lo 
)
inline

Take the lower-bounded Kleene star of a regular expression.

Definition at line 2117 of file Context.java.

2118  {
2119  return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
2120  }
BoolExpr mkLt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &lt; t2

Definition at line 890 of file Context.java.

891  {
892  checkContextMatch(t1);
893  checkContextMatch(t2);
894  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
895  t2.getNativeObject()));
896  }
ArrayExpr mkMap ( FuncDecl  f,
ArrayExpr...  args 
)
inline

Maps f on the argument arrays. Remarks: Each element of

args

must be of an array sort

[domain_i -> range_i]

. The function declaration

f

must have type

range_1 .. range_n -> range

.

v

must have sort range. The sort of the result is

[domain_i -> range]

.

See also
mkArraySort
mkSelect
mkStore

Definition at line 1795 of file Context.java.

1796  {
1797  checkContextMatch(f);
1798  checkContextMatch(args);
1799  return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1800  f.getNativeObject(), AST.arrayLength(args),
1801  AST.arrayToNative(args)));
1802  }
IntExpr mkMod ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing

t1 mod t2

. Remarks: The arguments must have int type.

Definition at line 853 of file Context.java.

854  {
855  checkContextMatch(t1);
856  checkContextMatch(t2);
857  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
858  t2.getNativeObject()));
859  }
ArithExpr mkMul ( ArithExpr...  t)
inline

Create an expression representing

t[0] * t[1] * ...

.

Definition at line 810 of file Context.java.

811  {
812  checkContextMatch(t);
813  return (ArithExpr) Expr.create(this,
814  Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
815  }
BoolExpr mkNot ( BoolExpr  a)
inline

Create an expression representing

not(a)

.

Definition at line 722 of file Context.java.

723  {
724  checkContextMatch(a);
725  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
726  }
Expr mkNumeral ( String  v,
Sort  ty 
)
inline

Create a Term of a given sort.

Parameters
vA string representing the term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form
[num]* / [num]*
.
tyThe sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size.
Returns
A Term with value
v
and sort
ty

Definition at line 2261 of file Context.java.

Referenced by Context.mkBV().

2262  {
2263  checkContextMatch(ty);
2264  return Expr.create(this,
2265  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
2266  }
Expr mkNumeral ( int  v,
Sort  ty 
)
inline

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than

MakeNumeral

since it is not necessary to parse a string.

Parameters
vValue of the numeral
tySort of the numeral
Returns
A Term with value
v
and type
ty

Definition at line 2278 of file Context.java.

2279  {
2280  checkContextMatch(ty);
2281  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
2282  }
Expr mkNumeral ( long  v,
Sort  ty 
)
inline

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than

MakeNumeral

since it is not necessary to parse a string.

Parameters
vValue of the numeral
tySort of the numeral
Returns
A Term with value
v
and type
ty

Definition at line 2294 of file Context.java.

2295  {
2296  checkContextMatch(ty);
2297  return Expr.create(this,
2298  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
2299  }
Optimize mkOptimize ( )
inline

Create a Optimize context.

Definition at line 3126 of file Context.java.

3127  {
3128  return new Optimize(this);
3129  }
ReExpr mkOption ( ReExpr  re)
inline

Create the optional regular expression.

Definition at line 2135 of file Context.java.

2136  {
2137  checkContextMatch(re);
2138  return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
2139  }
BoolExpr mkOr ( BoolExpr...  t)
inline

Create an expression representing

t[0] or t[1] or ...

.

Definition at line 790 of file Context.java.

791  {
792  checkContextMatch(t);
793  return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
794  AST.arrayToNative(t)));
795  }
Params mkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2677 of file Context.java.

2678  {
2679  return new Params(this);
2680  }
Pattern mkPattern ( Expr...  terms)
inline

Create a quantifier pattern.

Definition at line 546 of file Context.java.

547  {
548  if (terms.length == 0)
549  throw new Z3Exception("Cannot create a pattern from zero terms");
550 
551  long[] termsNative = AST.arrayToNative(terms);
552  return new Pattern(this, Native.mkPattern(nCtx(), terms.length,
553  termsNative));
554  }
BoolExpr mkPBEq ( int[]  coeffs,
BoolExpr[]  args,
int  k 
)
inline

Create a pseudo-Boolean equal constraint.

Definition at line 2243 of file Context.java.

2244  {
2245  checkContextMatch(args);
2246  return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2247  }
BoolExpr mkPBGe ( int[]  coeffs,
BoolExpr[]  args,
int  k 
)
inline

Create a pseudo-Boolean greater-or-equal constraint.

Definition at line 2234 of file Context.java.

2235  {
2236  checkContextMatch(args);
2237  return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2238  }
BoolExpr mkPBLe ( int[]  coeffs,
BoolExpr[]  args,
int  k 
)
inline

Create a pseudo-Boolean less-or-equal constraint.

Definition at line 2225 of file Context.java.

2226  {
2227  checkContextMatch(args);
2228  return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2229  }
ReExpr mkPlus ( ReExpr  re)
inline

Take the Kleene plus of a regular expression.

Definition at line 2126 of file Context.java.

2127  {
2128  checkContextMatch(re);
2129  return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
2130  }
ArithExpr mkPower ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 ^ t2

.

Definition at line 877 of file Context.java.

878  {
879  checkContextMatch(t1);
880  checkContextMatch(t2);
881  return (ArithExpr) Expr.create(
882  this,
883  Native.mkPower(nCtx(), t1.getNativeObject(),
884  t2.getNativeObject()));
885  }
BoolExpr mkPrefixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence prefix.

Definition at line 2018 of file Context.java.

2019  {
2020  checkContextMatch(s1, s2);
2021  return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2022  }
Probe mkProbe ( String  name)
inline

Creates a new Probe.

Definition at line 2950 of file Context.java.

2951  {
2952  return new Probe(this, name);
2953  }
Quantifier mkQuantifier ( boolean  universal,
Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a Quantifier.

See also
mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)

Definition at line 2502 of file Context.java.

2506  {
2507 
2508  if (universal)
2509  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2510  quantifierID, skolemID);
2511  else
2512  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2513  quantifierID, skolemID);
2514  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2476
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2450
Quantifier mkQuantifier ( boolean  universal,
Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a Quantifier

See also
mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)

Definition at line 2520 of file Context.java.

2523  {
2524 
2525  if (universal)
2526  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2527  quantifierID, skolemID);
2528  else
2529  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2530  quantifierID, skolemID);
2531  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2476
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2450
ReExpr mkRange ( SeqExpr  lo,
SeqExpr  hi 
)
inline

Create a range expression.

Definition at line 2197 of file Context.java.

2198  {
2199  checkContextMatch(lo, hi);
2200  return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
2201  }
RatNum mkReal ( int  num,
int  den 
)
inline

Create a real from a fraction.

Parameters
numnumerator of rational.
dendenominator of rational.
Returns
A Term with value
num
/
den
and sort Real
See also
mkNumeral(String,Sort)

Definition at line 2310 of file Context.java.

2311  {
2312  if (den == 0) {
2313  throw new Z3Exception("Denominator is zero");
2314  }
2315 
2316  return new RatNum(this, Native.mkReal(nCtx(), num, den));
2317  }
RatNum mkReal ( String  v)
inline

Create a real numeral.

Parameters
vA string representing the Term value in decimal notation.
Returns
A Term with value
v
and sort Real

Definition at line 2325 of file Context.java.

2326  {
2327 
2328  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2329  .getNativeObject()));
2330  }
RatNum mkReal ( int  v)
inline

Create a real numeral.

Parameters
vvalue of the numeral.
Returns
A Term with value
v
and sort Real

Definition at line 2338 of file Context.java.

2339  {
2340 
2341  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2342  .getNativeObject()));
2343  }
RatNum mkReal ( long  v)
inline

Create a real numeral.

Parameters
vvalue of the numeral.
Returns
A Term with value
v
and sort Real

Definition at line 2351 of file Context.java.

2352  {
2353 
2354  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2355  .getNativeObject()));
2356  }
IntExpr mkReal2Int ( RealExpr  t)
inline

Coerce a real to an integer. Remarks: The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort.

Definition at line 954 of file Context.java.

955  {
956  checkContextMatch(t);
957  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
958  }
RealExpr mkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 635 of file Context.java.

636  {
637  return (RealExpr) mkConst(name, getRealSort());
638  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
RealExpr mkRealConst ( String  name)
inline

Creates a real constant.

Definition at line 643 of file Context.java.

644  {
645  return (RealExpr) mkConst(name, getRealSort());
646  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
RealSort mkRealSort ( )
inline

Create a real sort.

Definition at line 204 of file Context.java.

205  {
206  return new RealSort(this);
207  }
def RealSort
Definition: z3py.py:2906
IntExpr mkRem ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing

t1 rem t2

. Remarks: The arguments must have int type.

Definition at line 866 of file Context.java.

867  {
868  checkContextMatch(t1);
869  checkContextMatch(t2);
870  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
871  t2.getNativeObject()));
872  }
BitVecExpr mkRepeat ( int  i,
BitVecExpr  t 
)
inline

Bit-vector repetition. Remarks: The argument

t

must have a bit-vector sort.

Definition at line 1386 of file Context.java.

1387  {
1388  checkContextMatch(t);
1389  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1390  t.getNativeObject()));
1391  }
SeqExpr mkReplace ( SeqExpr  s,
SeqExpr  src,
SeqExpr  dst 
)
inline

Replace the first occurrence of src by dst in s.

Definition at line 2072 of file Context.java.

2073  {
2074  checkContextMatch(s, src, dst);
2075  return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
2076  }
ReSort mkReSort ( Sort  s)
inline

Create a new regular expression sort

Definition at line 257 of file Context.java.

258  {
259  return new ReSort(this, Native.mkReSort(nCtx(), s.getNativeObject()));
260  }
def ReSort
Definition: z3py.py:10245
Expr mkSelect ( ArrayExpr  a,
Expr  i 
)
inline

Array read. Remarks: The argument

a

is the array and

i

is the index of the array that gets read.

The node

a

must have an array sort

[domain -> range]

, and

i

must have the sort

domain

. The sort of the result is

.

See also
mkArraySort
mkStore

Definition at line 1683 of file Context.java.

1684  {
1685  checkContextMatch(a);
1686  checkContextMatch(i);
1687  return Expr.create(
1688  this,
1689  Native.mkSelect(nCtx(), a.getNativeObject(),
1690  i.getNativeObject()));
1691  }
Expr mkSelect ( ArrayExpr  a,
Expr[]  args 
)
inline

Array read. Remarks: The argument

a

is the array and

args

are the indices of the array that gets read.

The node

a

must have an array sort

[domains -> range]

, and

args

must have the sorts

domains

. The sort of the result is

.

See also
mkArraySort
mkStore

Definition at line 1706 of file Context.java.

1707  {
1708  checkContextMatch(a);
1709  checkContextMatch(args);
1710  return Expr.create(
1711  this,
1712  Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
1713  }
SeqSort mkSeqSort ( Sort  s)
inline

Create a new sequence sort

Definition at line 249 of file Context.java.

250  {
251  return new SeqSort(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
252  }
def SeqSort
Definition: z3py.py:9950
ArrayExpr mkSetAdd ( ArrayExpr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 1860 of file Context.java.

1861  {
1862  checkContextMatch(set);
1863  checkContextMatch(element);
1864  return (ArrayExpr)Expr.create(this,
1865  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1866  element.getNativeObject()));
1867  }
ArrayExpr mkSetComplement ( ArrayExpr  arg)
inline

Take the complement of a set.

Definition at line 1918 of file Context.java.

1919  {
1920  checkContextMatch(arg);
1921  return (ArrayExpr)Expr.create(this,
1922  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1923  }
ArrayExpr mkSetDel ( ArrayExpr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 1872 of file Context.java.

1873  {
1874  checkContextMatch(set);
1875  checkContextMatch(element);
1876  return (ArrayExpr)Expr.create(this,
1877  Native.mkSetDel(nCtx(), set.getNativeObject(),
1878  element.getNativeObject()));
1879  }
ArrayExpr mkSetDifference ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Take the difference between two sets.

Definition at line 1906 of file Context.java.

1907  {
1908  checkContextMatch(arg1);
1909  checkContextMatch(arg2);
1910  return (ArrayExpr)Expr.create(this,
1911  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1912  arg2.getNativeObject()));
1913  }
ArrayExpr mkSetIntersection ( ArrayExpr...  args)
inline

Take the intersection of a list of sets.

Definition at line 1895 of file Context.java.

1896  {
1897  checkContextMatch(args);
1898  return (ArrayExpr)Expr.create(this,
1899  Native.mkSetIntersect(nCtx(), args.length,
1900  AST.arrayToNative(args)));
1901  }
BoolExpr mkSetMembership ( Expr  elem,
ArrayExpr  set 
)
inline

Check for set membership.

Definition at line 1928 of file Context.java.

1929  {
1930  checkContextMatch(elem);
1931  checkContextMatch(set);
1932  return (BoolExpr) Expr.create(this,
1933  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1934  set.getNativeObject()));
1935  }
SetSort mkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 1831 of file Context.java.

1832  {
1833  checkContextMatch(ty);
1834  return new SetSort(this, ty);
1835  }
def SetSort
Sets.
Definition: z3py.py:4548
BoolExpr mkSetSubset ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 1940 of file Context.java.

1941  {
1942  checkContextMatch(arg1);
1943  checkContextMatch(arg2);
1944  return (BoolExpr) Expr.create(this,
1945  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1946  arg2.getNativeObject()));
1947  }
ArrayExpr mkSetUnion ( ArrayExpr...  args)
inline

Take the union of a list of sets.

Definition at line 1884 of file Context.java.

1885  {
1886  checkContextMatch(args);
1887  return (ArrayExpr)Expr.create(this,
1888  Native.mkSetUnion(nCtx(), args.length,
1889  AST.arrayToNative(args)));
1890  }
BitVecExpr mkSignExt ( int  i,
BitVecExpr  t 
)
inline

Bit-vector sign extension. Remarks: Sign-extends the given bit-vector to the (signed) equivalent bitvector of size

m+i

, where m is the size of the given bit-vector. The argument

t

must have a bit-vector sort.

Definition at line 1360 of file Context.java.

1361  {
1362  checkContextMatch(t);
1363  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1364  t.getNativeObject()));
1365  }
Solver mkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3097 of file Context.java.

3098  {
3099  return new Solver(this, Native.mkSimpleSolver(nCtx()));
3100  }
Solver mkSolver ( )
inline

Creates a new (incremental) solver. Remarks: This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.

Definition at line 3063 of file Context.java.

Referenced by Tactic.getSolver(), and Context.mkSolver().

3064  {
3065  return mkSolver((Symbol) null);
3066  }
Solver mkSolver ( Symbol  logic)
inline

Creates a new (incremental) solver. Remarks: This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.

Definition at line 3075 of file Context.java.

3076  {
3077 
3078  if (logic == null)
3079  return new Solver(this, Native.mkSolver(nCtx()));
3080  else
3081  return new Solver(this, Native.mkSolverForLogic(nCtx(),
3082  logic.getNativeObject()));
3083  }
Solver mkSolver ( String  logic)
inline

Creates a new (incremental) solver.

See also
mkSolver(Symbol)

Definition at line 3089 of file Context.java.

3090  {
3091  return mkSolver(mkSymbol(logic));
3092  }
IntSymbol mkSymbol(int i)
Definition: Context.java:93
Solver mkSolver ( Tactic  t)
inline

Creates a solver that is implemented using the given tactic. Remarks: The solver supports the commands

Push

and

Pop

, but it will always solve each check from scratch.

Definition at line 3108 of file Context.java.

3109  {
3110 
3111  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3112  t.getNativeObject()));
3113  }
ReExpr mkStar ( ReExpr  re)
inline

Take the Kleene star of a regular expression.

Definition at line 2100 of file Context.java.

2101  {
2102  checkContextMatch(re);
2103  return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
2104  }
ArrayExpr mkStore ( ArrayExpr  a,
Expr  i,
Expr  v 
)
inline

Array update. Remarks: The node

a

must have an array sort

[domain -> range]

,

i

must have sort

domain

,

v

must have sort range. The sort of the result is

[domain -> range]

. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to

a

(with respect to

) on all indices except for

i

, where it maps to

v

(and the

of

a

with respect to

i

may be a different value).

See also
mkArraySort
mkSelect

Definition at line 1731 of file Context.java.

1732  {
1733  checkContextMatch(a);
1734  checkContextMatch(i);
1735  checkContextMatch(v);
1736  return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1737  i.getNativeObject(), v.getNativeObject()));
1738  }
ArrayExpr mkStore ( ArrayExpr  a,
Expr[]  args,
Expr  v 
)
inline

Array update. Remarks: The node

a

must have an array sort

[domains -> range]

,

i

must have sort

domain

,

v

must have sort range. The sort of the result is

[domains -> range]

. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to

a

(with respect to

) on all indices except for

args

, where it maps to

v

(and the

of

a

with respect to

args

may be a different value).

See also
mkArraySort
mkSelect

Definition at line 1756 of file Context.java.

1757  {
1758  checkContextMatch(a);
1759  checkContextMatch(args);
1760  checkContextMatch(v);
1761  return new ArrayExpr(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
1762  args.length, AST.arrayToNative(args), v.getNativeObject()));
1763  }
SeqExpr mkString ( String  s)
inline

Create a string constant.

Definition at line 1975 of file Context.java.

1976  {
1977  return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
1978  }
SeqSort mkStringSort ( )
inline

Create a new string sort

Definition at line 241 of file Context.java.

Referenced by Context.getStringSort().

242  {
243  return new SeqSort(this, Native.mkStringSort(nCtx()));
244  }
def SeqSort
Definition: z3py.py:9950
ArithExpr mkSub ( ArithExpr...  t)
inline

Create an expression representing

t[0] - t[1] - ...

.

Definition at line 820 of file Context.java.

821  {
822  checkContextMatch(t);
823  return (ArithExpr) Expr.create(this,
824  Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
825  }
BoolExpr mkSuffixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence suffix.

Definition at line 2027 of file Context.java.

2028  {
2029  checkContextMatch(s1, s2);
2030  return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2031  }
IntSymbol mkSymbol ( int  i)
inline

Creates a new symbol using an integer. Remarks: Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.

Definition at line 93 of file Context.java.

Referenced by Params.add(), Optimize.AssertSoft(), Context.mkArrayConst(), Context.mkBoolConst(), Context.mkConst(), Context.mkConstDecl(), Context.mkConstructor(), Context.mkDatatypeSort(), Context.mkEnumSort(), Context.mkFiniteDomainSort(), Context.mkFuncDecl(), Context.mkListSort(), Context.mkSolver(), and Context.mkUninterpretedSort().

94  {
95  return new IntSymbol(this, i);
96  }
StringSymbol mkSymbol ( String  name)
inline

Create a symbol using a string.

Definition at line 101 of file Context.java.

102  {
103  return new StringSymbol(this, name);
104  }
Tactic mkTactic ( String  name)
inline

Creates a new Tactic.

Definition at line 2715 of file Context.java.

Referenced by Goal.simplify().

2716  {
2717  return new Tactic(this, name);
2718  }
Expr mkTermArray ( ArrayExpr  array)
inline

Access the array default value. Remarks: Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Definition at line 1810 of file Context.java.

1811  {
1812  checkContextMatch(array);
1813  return Expr.create(this,
1814  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1815  }
ReExpr mkToRe ( SeqExpr  s)
inline

Convert a regular expression that accepts sequence s.

Definition at line 2081 of file Context.java.

2082  {
2083  checkContextMatch(s);
2084  return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
2085  }
BoolExpr mkTrue ( )
inline

The true Term.

Definition at line 677 of file Context.java.

Referenced by Goal.AsBoolExpr(), and Context.mkBool().

678  {
679  return new BoolExpr(this, Native.mkTrue(nCtx()));
680  }
TupleSort mkTupleSort ( Symbol  name,
Symbol[]  fieldNames,
Sort[]  fieldSorts 
)
inline

Create a new tuple sort.

Definition at line 266 of file Context.java.

268  {
269  checkContextMatch(name);
270  checkContextMatch(fieldNames);
271  checkContextMatch(fieldSorts);
272  return new TupleSort(this, name, fieldNames.length, fieldNames,
273  fieldSorts);
274  }
def TupleSort
Definition: z3py.py:4951
ArithExpr mkUnaryMinus ( ArithExpr  t)
inline

Create an expression representing

-t

.

Definition at line 830 of file Context.java.

831  {
832  checkContextMatch(t);
833  return (ArithExpr) Expr.create(this,
834  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
835  }
UninterpretedSort mkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 179 of file Context.java.

Referenced by Context.mkUninterpretedSort().

180  {
181  checkContextMatch(s);
182  return new UninterpretedSort(this, s);
183  }
UninterpretedSort mkUninterpretedSort ( String  str)
inline

Create a new uninterpreted sort.

Definition at line 188 of file Context.java.

189  {
190  return mkUninterpretedSort(mkSymbol(str));
191  }
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:179
IntSymbol mkSymbol(int i)
Definition: Context.java:93
ReExpr mkUnion ( ReExpr...  t)
inline

Create the union of regular languages.

Definition at line 2163 of file Context.java.

2164  {
2165  checkContextMatch(t);
2166  return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2167  }
SeqExpr mkUnit ( Expr  elem)
inline

Create the singleton sequence.

Definition at line 1966 of file Context.java.

1967  {
1968  checkContextMatch(elem);
1969  return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
1970  }
Expr mkUpdateField ( FuncDecl  field,
Expr  t,
Expr  v 
) throws Z3Exception
inline

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 remaining fields of t are unchanged.

Definition at line 428 of file Context.java.

430  {
431  return Expr.create (this,
432  Native.datatypeUpdateField
433  (nCtx(), field.getNativeObject(),
434  t.getNativeObject(), v.getNativeObject()));
435  }
BoolExpr mkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 xor t2

.

Definition at line 769 of file Context.java.

770  {
771  checkContextMatch(t1);
772  checkContextMatch(t2);
773  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
774  t2.getNativeObject()));
775  }
BitVecExpr mkZeroExt ( int  i,
BitVecExpr  t 
)
inline

Bit-vector zero extension. Remarks: Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size

m+i

, where m is the size of the given bit-vector. The argument

t

must have a bit-vector sort.

Definition at line 1374 of file Context.java.

1375  {
1376  checkContextMatch(t);
1377  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1378  t.getNativeObject()));
1379  }
Probe not ( Probe  p)
inline

Create a probe that evaluates to

true

when the value

p

does not evaluate to

true

.

Definition at line 3050 of file Context.java.

3051  {
3052  checkContextMatch(p);
3053  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
3054  }
Probe or ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value

p1

or

p2

evaluate to

true

.

Definition at line 3039 of file Context.java.

3040  {
3041  checkContextMatch(p1);
3042  checkContextMatch(p2);
3043  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
3044  p2.getNativeObject()));
3045  }
Tactic orElse ( Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that first applies

t1

to a Goal and if it fails then returns the result of

t2

applied to the Goal.

Definition at line 2766 of file Context.java.

2767  {
2768  checkContextMatch(t1);
2769  checkContextMatch(t2);
2770  return new Tactic(this, Native.tacticOrElse(nCtx(),
2771  t1.getNativeObject(), t2.getNativeObject()));
2772  }
Tactic parAndThen ( Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that applies

t1

to a given goal and then

t2

to every subgoal produced by

t1

. The subgoals are processed in parallel.

Definition at line 2899 of file Context.java.

2900  {
2901  checkContextMatch(t1);
2902  checkContextMatch(t2);
2903  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2904  t1.getNativeObject(), t2.getNativeObject()));
2905  }
Tactic parOr ( Tactic...  t)
inline

Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).

Definition at line 2888 of file Context.java.

2889  {
2890  checkContextMatch(t);
2891  return new Tactic(this, Native.tacticParOr(nCtx(),
2892  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2893  }
BoolExpr [] parseSMTLIB2File ( String  fileName,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
)
inline

Parse the given file using the SMT-LIB2 parser.

See also
parseSMTLIB2String

Definition at line 2640 of file Context.java.

2643  {
2644  int csn = Symbol.arrayLength(sortNames);
2645  int cs = Sort.arrayLength(sorts);
2646  int cdn = Symbol.arrayLength(declNames);
2647  int cd = AST.arrayLength(decls);
2648  if (csn != cs || cdn != cd)
2649  throw new Z3Exception("Argument size mismatch");
2650  ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
2651  fileName, AST.arrayLength(sorts),
2652  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2653  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2654  AST.arrayToNative(decls)));
2655  return v.ToBoolExprArray();
2656  }
BoolExpr [] parseSMTLIB2String ( String  str,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
)
inline

Parse the given string using the SMT-LIB2 parser.

Returns
A conjunction of assertions.

If the string contains push/pop commands, the set of assertions returned are the ones in the last scope level.

Definition at line 2618 of file Context.java.

2621  {
2622  int csn = Symbol.arrayLength(sortNames);
2623  int cs = Sort.arrayLength(sorts);
2624  int cdn = Symbol.arrayLength(declNames);
2625  int cd = AST.arrayLength(decls);
2626  if (csn != cs || cdn != cd) {
2627  throw new Z3Exception("Argument size mismatch");
2628  }
2629  ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
2630  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2631  AST.arrayToNative(sorts), AST.arrayLength(decls),
2632  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2633  return v.ToBoolExprArray();
2634  }
Tactic repeat ( Tactic  t,
int  max 
)
inline

Create a tactic that keeps applying

t

until the goal is not modified anymore or the maximum number of iterations

is reached.

Definition at line 2819 of file Context.java.

2820  {
2821  checkContextMatch(t);
2822  return new Tactic(this, Native.tacticRepeat(nCtx(),
2823  t.getNativeObject(), max));
2824  }
expr max(expr const &a, expr const &b)
Definition: z3++.h:1568
void setPrintMode ( Z3_ast_print_mode  value)
inline

Selects the format used for pretty-printing expressions. Remarks: The default mode for pretty printing expressions is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.

See also
AST::toString
Pattern::toString
FuncDecl::toString
Sort::toString

Definition at line 2581 of file Context.java.

2582  {
2583  Native.setAstPrintMode(nCtx(), value.toInt());
2584  }
String SimplifyHelp ( )
inline

Return a string describing all available parameters to

Expr.Simplify

.

Definition at line 3939 of file Context.java.

3940  {
3941  return Native.simplifyGetHelp(nCtx());
3942  }
Tactic skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 2829 of file Context.java.

2830  {
2831  return new Tactic(this, Native.tacticSkip(nCtx()));
2832  }
IntExpr stringToInt ( Expr  e)
inline

Convert an integer expression to a string.

Definition at line 1991 of file Context.java.

1992  {
1993  return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
1994  }
Tactic then ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
)
inline

Create a tactic that applies

t1

to a Goal and then

t2

to every subgoal produced by

t1

Remarks: Shorthand for

.

Definition at line 2756 of file Context.java.

2757  {
2758  return andThen(t1, t2, ts);
2759  }
Tactic andThen(Tactic t1, Tactic t2, Tactic...ts)
Definition: Context.java:2724
Tactic tryFor ( Tactic  t,
int  ms 
)
inline

Create a tactic that applies

t

to a goal for

ms

milliseconds. Remarks: If

t

does not terminate within

ms

milliseconds, then it fails.

Definition at line 2780 of file Context.java.

2781  {
2782  checkContextMatch(t);
2783  return new Tactic(this, Native.tacticTryFor(nCtx(),
2784  t.getNativeObject(), ms));
2785  }
long unwrapAST ( AST  a)
inline

Unwraps an AST. Remarks: This function is used for transitions between native and managed objects. It returns the native pointer to the AST. Note that AST objects are reference counted and unwrapping an AST disables automatic reference counting, i.e., all references to the IntPtr that is returned must be handled externally and through native calls (see e.g.,

See also
Native::incRef
wrapAST
Parameters
aThe AST to unwrap.

Definition at line 3930 of file Context.java.

3931  {
3932  return a.getNativeObject();
3933  }
void updateParamValue ( String  id,
String  value 
)
inline

Update a mutable configuration parameter. Remarks: The list of all configuration parameters can be obtained using the Z3 executable:

z3.exe -ini?

Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.

Definition at line 3960 of file Context.java.

3961  {
3962  Native.updateParamValue(nCtx(), id, value);
3963  }
Tactic usingParams ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

.

Definition at line 2866 of file Context.java.

Referenced by Context.with().

2867  {
2868  checkContextMatch(t);
2869  checkContextMatch(p);
2870  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2871  t.getNativeObject(), p.getNativeObject()));
2872  }
Tactic when ( Probe  p,
Tactic  t 
)
inline

Create a tactic that applies

t

to a given goal if the probe

p

evaluates to true. Remarks: If

p

evaluates to false, then the new tactic behaves like the

tactic.

Definition at line 2793 of file Context.java.

2794  {
2795  checkContextMatch(t);
2796  checkContextMatch(p);
2797  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2798  t.getNativeObject()));
2799  }
Tactic with ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

. Remarks: Alias for

UsingParams

Definition at line 2880 of file Context.java.

2881  {
2882  return usingParams(t, p);
2883  }
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2866
AST wrapAST ( long  nativeObject)
inline

Wraps an AST. Remarks: This function is used for transitions between native and managed objects. Note that

nativeObject

must be a native object obtained from Z3 (e.g., through

UnwrapAST

) and that it must have a correct reference count.

See also
Native::incRef
unwrapAST
Parameters
nativeObjectThe native pointer to wrap.

Definition at line 3913 of file Context.java.

3914  {
3915  return AST.create(this, nativeObject);
3916  }