Z3
Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes
Context Class Reference
+ Inheritance diagram for Context:

Public Member Functions

 Context () throws Z3Exception
 
 Context (Map< String, String > settings) throws Z3Exception
 
IntSymbol mkSymbol (int i) throws Z3Exception
 
StringSymbol mkSymbol (String name) throws Z3Exception
 
BoolSort getBoolSort () throws Z3Exception
 
IntSort getIntSort () throws Z3Exception
 
RealSort getRealSort () throws Z3Exception
 
BoolSort mkBoolSort () throws Z3Exception
 
UninterpretedSort mkUninterpretedSort (Symbol s) throws Z3Exception
 
UninterpretedSort mkUninterpretedSort (String str) throws Z3Exception
 
IntSort mkIntSort () throws Z3Exception
 
RealSort mkRealSort () throws Z3Exception
 
BitVecSort mkBitVecSort (int size) throws Z3Exception
 
ArraySort mkArraySort (Sort domain, Sort range) throws Z3Exception
 
TupleSort mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts) throws Z3Exception
 
EnumSort mkEnumSort (Symbol name, Symbol...enumNames) throws Z3Exception
 
EnumSort mkEnumSort (String name, String...enumNames) throws Z3Exception
 
ListSort mkListSort (Symbol name, Sort elemSort) throws Z3Exception
 
ListSort mkListSort (String name, Sort elemSort) throws Z3Exception
 
FiniteDomainSort mkFiniteDomainSort (Symbol name, long size) throws Z3Exception
 
FiniteDomainSort mkFiniteDomainSort (String name, long size) throws Z3Exception
 
Constructor mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception
 
Constructor mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception
 
DatatypeSort mkDatatypeSort (Symbol name, Constructor[] constructors) throws Z3Exception
 
DatatypeSort mkDatatypeSort (String name, Constructor[] constructors) throws Z3Exception
 
DatatypeSort[] mkDatatypeSorts (Symbol[] names, Constructor[][] c) throws Z3Exception
 
DatatypeSort[] mkDatatypeSorts (String[] names, Constructor[][] c) throws Z3Exception
 
FuncDecl mkFuncDecl (Symbol name, Sort[] domain, Sort range) throws Z3Exception
 
FuncDecl mkFuncDecl (Symbol name, Sort domain, Sort range) throws Z3Exception
 
FuncDecl mkFuncDecl (String name, Sort[] domain, Sort range) throws Z3Exception
 
FuncDecl mkFuncDecl (String name, Sort domain, Sort range) throws Z3Exception
 
FuncDecl mkFreshFuncDecl (String prefix, Sort[] domain, Sort range) throws Z3Exception
 
FuncDecl mkConstDecl (Symbol name, Sort range) throws Z3Exception
 
FuncDecl mkConstDecl (String name, Sort range) throws Z3Exception
 
FuncDecl mkFreshConstDecl (String prefix, Sort range) throws Z3Exception
 
Expr mkBound (int index, Sort ty) throws Z3Exception
 
Pattern mkPattern (Expr...terms) throws Z3Exception
 
Expr mkConst (Symbol name, Sort range) throws Z3Exception
 
Expr mkConst (String name, Sort range) throws Z3Exception
 
Expr mkFreshConst (String prefix, Sort range) throws Z3Exception
 
Expr mkConst (FuncDecl f) throws Z3Exception
 
BoolExpr mkBoolConst (Symbol name) throws Z3Exception
 
BoolExpr mkBoolConst (String name) throws Z3Exception
 
IntExpr mkIntConst (Symbol name) throws Z3Exception
 
IntExpr mkIntConst (String name) throws Z3Exception
 
RealExpr mkRealConst (Symbol name) throws Z3Exception
 
RealExpr mkRealConst (String name) throws Z3Exception
 
BitVecExpr mkBVConst (Symbol name, int size) throws Z3Exception
 
BitVecExpr mkBVConst (String name, int size) throws Z3Exception
 
Expr mkApp (FuncDecl f, Expr...args) throws Z3Exception
 
BoolExpr mkTrue () throws Z3Exception
 
BoolExpr mkFalse () throws Z3Exception
 
BoolExpr mkBool (boolean value) throws Z3Exception
 
BoolExpr mkEq (Expr x, Expr y) throws Z3Exception
 
BoolExpr mkDistinct (Expr...args) throws Z3Exception
 
BoolExpr mkNot (BoolExpr a) throws Z3Exception
 
Expr mkITE (BoolExpr t1, Expr t2, Expr t3) throws Z3Exception
 
BoolExpr mkIff (BoolExpr t1, BoolExpr t2) throws Z3Exception
 
BoolExpr mkImplies (BoolExpr t1, BoolExpr t2) throws Z3Exception
 
BoolExpr mkXor (BoolExpr t1, BoolExpr t2) throws Z3Exception
 
BoolExpr mkAnd (BoolExpr...t) throws Z3Exception
 
BoolExpr mkOr (BoolExpr...t) throws Z3Exception
 
ArithExpr mkAdd (ArithExpr...t) throws Z3Exception
 
ArithExpr mkMul (ArithExpr...t) throws Z3Exception
 
ArithExpr mkSub (ArithExpr...t) throws Z3Exception
 
ArithExpr mkUnaryMinus (ArithExpr t) throws Z3Exception
 
ArithExpr mkDiv (ArithExpr t1, ArithExpr t2) throws Z3Exception
 
IntExpr mkMod (IntExpr t1, IntExpr t2) throws Z3Exception
 
IntExpr mkRem (IntExpr t1, IntExpr t2) throws Z3Exception
 
ArithExpr mkPower (ArithExpr t1, ArithExpr t2) throws Z3Exception
 
BoolExpr mkLt (ArithExpr t1, ArithExpr t2) throws Z3Exception
 
BoolExpr mkLe (ArithExpr t1, ArithExpr t2) throws Z3Exception
 
BoolExpr mkGt (ArithExpr t1, ArithExpr t2) throws Z3Exception
 
BoolExpr mkGe (ArithExpr t1, ArithExpr t2) throws Z3Exception
 
RealExpr mkInt2Real (IntExpr t) throws Z3Exception
 
IntExpr mkReal2Int (RealExpr t) throws Z3Exception
 
BoolExpr mkIsInteger (RealExpr t) throws Z3Exception
 
BitVecExpr mkBVNot (BitVecExpr t) throws Z3Exception
 
BitVecExpr mkBVRedAND (BitVecExpr t) throws Z3Exception
 
BitVecExpr mkBVRedOR (BitVecExpr t) throws Z3Exception
 
BitVecExpr mkBVAND (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVXOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVNAND (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVNOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVXNOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVNeg (BitVecExpr t) throws Z3Exception
 
BitVecExpr mkBVAdd (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVSub (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVMul (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVUDiv (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVSDiv (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVURem (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVSRem (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVSMod (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVULT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVSLT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVULE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVSLE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVUGE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVSGE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVUGT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVSGT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkConcat (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkExtract (int high, int low, BitVecExpr t) throws Z3Exception
 
BitVecExpr mkSignExt (int i, BitVecExpr t) throws Z3Exception
 
BitVecExpr mkZeroExt (int i, BitVecExpr t) throws Z3Exception
 
BitVecExpr mkRepeat (int i, BitVecExpr t) throws Z3Exception
 
BitVecExpr mkBVSHL (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVLSHR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVASHR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVRotateLeft (int i, BitVecExpr t) throws Z3Exception
 
BitVecExpr mkBVRotateRight (int i, BitVecExpr t) throws Z3Exception
 
BitVecExpr mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkBVRotateRight (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BitVecExpr mkInt2BV (int n, IntExpr t) throws Z3Exception
 
IntExpr mkBV2Int (BitVecExpr t, boolean signed) throws Z3Exception
 
BoolExpr mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception
 
BoolExpr mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception
 
BoolExpr mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
BoolExpr mkBVNegNoOverflow (BitVecExpr t) throws Z3Exception
 
BoolExpr mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception
 
BoolExpr mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
 
ArrayExpr mkArrayConst (Symbol name, Sort domain, Sort range) throws Z3Exception
 
ArrayExpr mkArrayConst (String name, Sort domain, Sort range) throws Z3Exception
 
Expr mkSelect (ArrayExpr a, Expr i) throws Z3Exception
 
ArrayExpr mkStore (ArrayExpr a, Expr i, Expr v) throws Z3Exception
 
ArrayExpr mkConstArray (Sort domain, Expr v) throws Z3Exception
 
ArrayExpr mkMap (FuncDecl f, ArrayExpr...args) throws Z3Exception
 
Expr mkTermArray (ArrayExpr array) throws Z3Exception
 
SetSort mkSetSort (Sort ty) throws Z3Exception
 
Expr mkEmptySet (Sort domain) throws Z3Exception
 
Expr mkFullSet (Sort domain) throws Z3Exception
 
Expr mkSetAdd (Expr set, Expr element) throws Z3Exception
 
Expr mkSetDel (Expr set, Expr element) throws Z3Exception
 
Expr mkSetUnion (Expr...args) throws Z3Exception
 
Expr mkSetIntersection (Expr...args) throws Z3Exception
 
Expr mkSetDifference (Expr arg1, Expr arg2) throws Z3Exception
 
Expr mkSetComplement (Expr arg) throws Z3Exception
 
Expr mkSetMembership (Expr elem, Expr set) throws Z3Exception
 
Expr mkSetSubset (Expr arg1, Expr arg2) throws Z3Exception
 
Expr mkNumeral (String v, Sort ty) throws Z3Exception
 
Expr mkNumeral (int v, Sort ty) throws Z3Exception
 
Expr mkNumeral (long v, Sort ty) throws Z3Exception
 
RatNum mkReal (int num, int den) throws Z3Exception
 
RatNum mkReal (String v) throws Z3Exception
 
RatNum mkReal (int v) throws Z3Exception
 
RatNum mkReal (long v) throws Z3Exception
 
IntNum mkInt (String v) throws Z3Exception
 
IntNum mkInt (int v) throws Z3Exception
 
IntNum mkInt (long v) throws Z3Exception
 
BitVecNum mkBV (String v, int size) throws Z3Exception
 
BitVecNum mkBV (int v, int size) throws Z3Exception
 
BitVecNum mkBV (long v, int size) throws Z3Exception
 
Quantifier mkForall (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
 
Quantifier mkForall (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
 
Quantifier mkExists (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
 
Quantifier mkExists (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
 
Quantifier mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
 
Quantifier mkQuantifier (boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
 
void setPrintMode (Z3_ast_print_mode value) throws Z3Exception
 
String benchmarkToSMTString (String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula) throws Z3Exception
 
void parseSMTLIBString (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception
 
void parseSMTLIBFile (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception
 
int getNumSMTLIBFormulas () throws Z3Exception
 
BoolExpr[] getSMTLIBFormulas () throws Z3Exception
 
int getNumSMTLIBAssumptions () throws Z3Exception
 
BoolExpr[] getSMTLIBAssumptions () throws Z3Exception
 
int getNumSMTLIBDecls () throws Z3Exception
 
FuncDecl[] getSMTLIBDecls () throws Z3Exception
 
int getNumSMTLIBSorts () throws Z3Exception
 
Sort[] getSMTLIBSorts () throws Z3Exception
 
BoolExpr parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception
 
BoolExpr parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception
 
Goal mkGoal (boolean models, boolean unsatCores, boolean proofs) throws Z3Exception
 
Params mkParams () throws Z3Exception
 
int getNumTactics () throws Z3Exception
 
String[] getTacticNames () throws Z3Exception
 
String getTacticDescription (String name) throws Z3Exception
 
Tactic mkTactic (String name) throws Z3Exception
 
Tactic andThen (Tactic t1, Tactic t2, Tactic...ts) throws Z3Exception
 
Tactic then (Tactic t1, Tactic t2, Tactic...ts) throws Z3Exception
 
Tactic orElse (Tactic t1, Tactic t2) throws Z3Exception
 
Tactic tryFor (Tactic t, int ms) throws Z3Exception
 
Tactic when (Probe p, Tactic t) throws Z3Exception
 
Tactic cond (Probe p, Tactic t1, Tactic t2) throws Z3Exception
 
Tactic repeat (Tactic t, int max) throws Z3Exception
 
Tactic skip () throws Z3Exception
 
Tactic fail () throws Z3Exception
 
Tactic failIf (Probe p) throws Z3Exception
 
Tactic failIfNotDecided () throws Z3Exception
 
Tactic usingParams (Tactic t, Params p) throws Z3Exception
 
Tactic with (Tactic t, Params p) throws Z3Exception
 
Tactic parOr (Tactic...t) throws Z3Exception
 
Tactic parAndThen (Tactic t1, Tactic t2) throws Z3Exception
 
void interrupt () throws Z3Exception
 
int getNumProbes () throws Z3Exception
 
String[] getProbeNames () throws Z3Exception
 
String getProbeDescription (String name) throws Z3Exception
 
Probe mkProbe (String name) throws Z3Exception
 
Probe constProbe (double val) throws Z3Exception
 
Probe lt (Probe p1, Probe p2) throws Z3Exception
 
Probe gt (Probe p1, Probe p2) throws Z3Exception
 
Probe le (Probe p1, Probe p2) throws Z3Exception
 
Probe ge (Probe p1, Probe p2) throws Z3Exception
 
Probe eq (Probe p1, Probe p2) throws Z3Exception
 
Probe and (Probe p1, Probe p2) throws Z3Exception
 
Probe or (Probe p1, Probe p2) throws Z3Exception
 
Probe not (Probe p) throws Z3Exception
 
Solver mkSolver () throws Z3Exception
 
Solver mkSolver (Symbol logic) throws Z3Exception
 
Solver mkSolver (String logic) throws Z3Exception
 
Solver mkSimpleSolver () throws Z3Exception
 
Solver mkSolver (Tactic t) throws Z3Exception
 
Fixedpoint mkFixedpoint () throws Z3Exception
 
AST wrapAST (long nativeObject) throws Z3Exception
 
long unwrapAST (AST a)
 
String SimplifyHelp () throws Z3Exception
 
ParamDescrs getSimplifyParameterDescriptions () throws Z3Exception
 
void updateParamValue (String id, String value) throws Z3Exception
 
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Static Public Member Functions

static void ToggleWarningMessages (boolean enabled) throws Z3Exception
 

Protected Member Functions

void finalize ()
 

Protected Attributes

long m_refCount = 0
 

Detailed Description

The main interaction with Z3 happens via the Context.

Definition at line 27 of file Context.java.

Constructor & Destructor Documentation

Context ( ) throws Z3Exception
inline

Constructor.

Definition at line 32 of file Context.java.

33  {
34  super();
35  m_ctx = Native.mkContextRc(0);
36  initContext();
37  }
Context ( Map< String, String >  settings) throws Z3Exception
inline

Constructor.

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 57 of file Context.java.

58  {
59  super();
60  long cfg = Native.mkConfig();
61  for (Map.Entry<String, String> kv : settings.entrySet())
62  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
63  m_ctx = Native.mkContextRc(cfg);
64  Native.delConfig(cfg);
65  initContext();
66  }
def Map(f, args)
Definition: z3py.py:4040

Member Function Documentation

Probe and ( Probe  p1,
Probe  p2 
) throws Z3Exception
inline

Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".

Definition at line 2758 of file Context.java.

2759  {
2760  checkContextMatch(p1);
2761  checkContextMatch(p2);
2762  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
2763  p2.getNativeObject()));
2764  }
Tactic andThen ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
) throws Z3Exception
inline

Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .

Definition at line 2440 of file Context.java.

Referenced by Context.then().

2442  {
2443  checkContextMatch(t1);
2444  checkContextMatch(t2);
2445  checkContextMatch(ts);
2446 
2447  long last = 0;
2448  if (ts != null && ts.length > 0)
2449  {
2450  last = ts[ts.length - 1].getNativeObject();
2451  for (int i = ts.length - 2; i >= 0; i--)
2452  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2453  last);
2454  }
2455  if (last != 0)
2456  {
2457  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2458  return new Tactic(this, Native.tacticAndThen(nCtx(),
2459  t1.getNativeObject(), last));
2460  } else
2461  return new Tactic(this, Native.tacticAndThen(nCtx(),
2462  t1.getNativeObject(), t2.getNativeObject()));
2463  }
String benchmarkToSMTString ( String  name,
String  logic,
String  status,
String  attributes,
BoolExpr[]  assumptions,
BoolExpr  formula 
) throws Z3Exception
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 2177 of file Context.java.

2180  {
2181 
2182  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2183  attributes, (int) assumptions.length,
2184  AST.arrayToNative(assumptions), formula.getNativeObject());
2185  }
Tactic cond ( Probe  p,
Tactic  t1,
Tactic  t2 
) throws Z3Exception
inline

Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise.

Definition at line 2523 of file Context.java.

2524  {
2525 
2526  checkContextMatch(p);
2527  checkContextMatch(t1);
2528  checkContextMatch(t2);
2529  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2530  t1.getNativeObject(), t2.getNativeObject()));
2531  }
Probe constProbe ( double  val) throws Z3Exception
inline

Create a probe that always evaluates to val .

Definition at line 2681 of file Context.java.

2682  {
2683  return new Probe(this, Native.probeConst(nCtx(), val));
2684  }
void dispose ( )
inline

Disposes of the context.

Definition at line 3070 of file Context.java.

Referenced by Context.finalize().

3071  {
3072  m_AST_DRQ.clear(this);
3073  m_ASTMap_DRQ.clear(this);
3074  m_ASTVector_DRQ.clear(this);
3075  m_ApplyResult_DRQ.clear(this);
3076  m_FuncEntry_DRQ.clear(this);
3077  m_FuncInterp_DRQ.clear(this);
3078  m_Goal_DRQ.clear(this);
3079  m_Model_DRQ.clear(this);
3080  m_Params_DRQ.clear(this);
3081  m_Probe_DRQ.clear(this);
3082  m_Solver_DRQ.clear(this);
3083  m_Statistics_DRQ.clear(this);
3084  m_Tactic_DRQ.clear(this);
3085  m_Fixedpoint_DRQ.clear(this);
3086 
3087  m_boolSort = null;
3088  m_intSort = null;
3089  m_realSort = null;
3090  }
Probe eq ( Probe  p1,
Probe  p2 
) throws Z3Exception
inline

Create a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2

Definition at line 2746 of file Context.java.

Referenced by SortRef.cast(), and BoolSortRef.cast().

2747  {
2748  checkContextMatch(p1);
2749  checkContextMatch(p2);
2750  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2751  p2.getNativeObject()));
2752  }
Tactic fail ( ) throws Z3Exception
inline

Create a tactic always fails.

Definition at line 2558 of file Context.java.

2559  {
2560 
2561  return new Tactic(this, Native.tacticFail(nCtx()));
2562  }
Tactic failIf ( Probe  p) throws Z3Exception
inline

Create a tactic that fails if the probe p evaluates to false.

Definition at line 2568 of file Context.java.

2569  {
2570 
2571  checkContextMatch(p);
2572  return new Tactic(this,
2573  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2574  }
Tactic failIfNotDecided ( ) throws Z3Exception
inline

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

Definition at line 2580 of file Context.java.

2581  {
2582  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2583  }
void finalize ( )
inlineprotected

Finalizer.

Definition at line 3047 of file Context.java.

3048  {
3049  dispose();
3050 
3051  if (m_refCount == 0)
3052  {
3053  try
3054  {
3055  Native.delContext(m_ctx);
3056  } catch (Z3Exception e)
3057  {
3058  // OK.
3059  }
3060  m_ctx = 0;
3061  }
3062  /*
3063  else
3064  CMW: re-queue the finalizer? */
3065  }
Probe ge ( Probe  p1,
Probe  p2 
) throws Z3Exception
inline

Create a probe that evaluates to "true" when the value returned by p1 is greater than or equal the value returned by p2

Definition at line 2733 of file Context.java.

2734  {
2735  checkContextMatch(p1);
2736  checkContextMatch(p2);
2737  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2738  p2.getNativeObject()));
2739  }
BoolSort getBoolSort ( ) throws Z3Exception
inline

Retrieves the Boolean sort of the context.

Definition at line 106 of file Context.java.

Referenced by Context.mkBoolConst().

107  {
108  if (m_boolSort == null)
109  m_boolSort = new BoolSort(this);
110  return m_boolSort;
111  }
def BoolSort
Definition: z3py.py:1325
IntSort getIntSort ( ) throws Z3Exception
inline

Retrieves the Integer sort of the context.

Definition at line 116 of file Context.java.

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

117  {
118  if (m_intSort == null)
119  m_intSort = new IntSort(this);
120  return m_intSort;
121  }
def IntSort
Definition: z3py.py:2614
int getNumProbes ( ) throws Z3Exception
inline

The number of supported Probes.

Definition at line 2643 of file Context.java.

Referenced by Context.getProbeNames().

2644  {
2645  return Native.getNumProbes(nCtx());
2646  }
int getNumSMTLIBAssumptions ( ) throws Z3Exception
inline

The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2259 of file Context.java.

Referenced by Context.getSMTLIBAssumptions().

2260  {
2261  return Native.getSmtlibNumAssumptions(nCtx());
2262  }
int getNumSMTLIBDecls ( ) throws Z3Exception
inline

The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2283 of file Context.java.

Referenced by Context.getSMTLIBDecls().

2284  {
2285  return Native.getSmtlibNumDecls(nCtx());
2286  }
int getNumSMTLIBFormulas ( ) throws Z3Exception
inline

The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2235 of file Context.java.

Referenced by Context.getSMTLIBFormulas().

2236  {
2237  return Native.getSmtlibNumFormulas(nCtx());
2238  }
int getNumSMTLIBSorts ( ) throws Z3Exception
inline

The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2306 of file Context.java.

Referenced by Context.getSMTLIBSorts().

2307  {
2308  return Native.getSmtlibNumSorts(nCtx());
2309  }
int getNumTactics ( ) throws Z3Exception
inline

The number of supported tactics.

Definition at line 2399 of file Context.java.

Referenced by Context.getTacticNames().

2400  {
2401  return Native.getNumTactics(nCtx());
2402  }
String getProbeDescription ( String  name) throws Z3Exception
inline

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

Definition at line 2665 of file Context.java.

2666  {
2667  return Native.probeGetDescr(nCtx(), name);
2668  }
String [] getProbeNames ( ) throws Z3Exception
inline

The names of all supported Probes.

Definition at line 2651 of file Context.java.

2652  {
2653 
2654  int n = getNumProbes();
2655  String[] res = new String[n];
2656  for (int i = 0; i < n; i++)
2657  res[i] = Native.getProbeName(nCtx(), i);
2658  return res;
2659  }
RealSort getRealSort ( ) throws Z3Exception
inline

Retrieves the Real sort of the context.

Definition at line 126 of file Context.java.

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

127  {
128  if (m_realSort == null)
129  m_realSort = new RealSort(this);
130  return m_realSort;
131  }
def RealSort
Definition: z3py.py:2630
ParamDescrs getSimplifyParameterDescriptions ( ) throws Z3Exception
inline

Retrieves parameter descriptions for simplifier.

Definition at line 2897 of file Context.java.

2898  {
2899  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
2900  }
BoolExpr [] getSMTLIBAssumptions ( ) throws Z3Exception
inline

The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2268 of file Context.java.

2269  {
2270 
2271  int n = getNumSMTLIBAssumptions();
2272  BoolExpr[] res = new BoolExpr[n];
2273  for (int i = 0; i < n; i++)
2274  res[i] = (BoolExpr) Expr.create(this,
2275  Native.getSmtlibAssumption(nCtx(), i));
2276  return res;
2277  }
FuncDecl [] getSMTLIBDecls ( ) throws Z3Exception
inline

The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2292 of file Context.java.

2293  {
2294 
2295  int n = getNumSMTLIBDecls();
2296  FuncDecl[] res = new FuncDecl[n];
2297  for (int i = 0; i < n; i++)
2298  res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
2299  return res;
2300  }
BoolExpr [] getSMTLIBFormulas ( ) throws Z3Exception
inline

The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2244 of file Context.java.

2245  {
2246 
2247  int n = getNumSMTLIBFormulas();
2248  BoolExpr[] res = new BoolExpr[n];
2249  for (int i = 0; i < n; i++)
2250  res[i] = (BoolExpr) Expr.create(this,
2251  Native.getSmtlibFormula(nCtx(), i));
2252  return res;
2253  }
Sort [] getSMTLIBSorts ( ) throws Z3Exception
inline

The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2315 of file Context.java.

2316  {
2317 
2318  int n = getNumSMTLIBSorts();
2319  Sort[] res = new Sort[n];
2320  for (int i = 0; i < n; i++)
2321  res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
2322  return res;
2323  }
String getTacticDescription ( String  name) throws Z3Exception
inline

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

Definition at line 2421 of file Context.java.

2422  {
2423 
2424  return Native.tacticGetDescr(nCtx(), name);
2425  }
String [] getTacticNames ( ) throws Z3Exception
inline

The names of all supported tactics.

Definition at line 2407 of file Context.java.

2408  {
2409 
2410  int n = getNumTactics();
2411  String[] res = new String[n];
2412  for (int i = 0; i < n; i++)
2413  res[i] = Native.getTacticName(nCtx(), i);
2414  return res;
2415  }
Probe gt ( Probe  p1,
Probe  p2 
) throws Z3Exception
inline

Create a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2

Definition at line 2705 of file Context.java.

2706  {
2707 
2708  checkContextMatch(p1);
2709  checkContextMatch(p2);
2710  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2711  p2.getNativeObject()));
2712  }
void interrupt ( ) throws Z3Exception
inline

Interrupt the execution of a Z3 procedure.

This procedure can be used to interrupt: solvers, simplifiers and tactics.

Definition at line 2635 of file Context.java.

2636  {
2637  Native.interrupt(nCtx());
2638  }
Probe le ( Probe  p1,
Probe  p2 
) throws Z3Exception
inline

Create a probe that evaluates to "true" when the value returned by p1 is less than or equal the value returned by p2

Definition at line 2719 of file Context.java.

2720  {
2721 
2722  checkContextMatch(p1);
2723  checkContextMatch(p2);
2724  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2725  p2.getNativeObject()));
2726  }
Probe lt ( Probe  p1,
Probe  p2 
) throws Z3Exception
inline

Create a probe that evaluates to "true" when the value returned by p1 is less than the value returned by p2

Definition at line 2691 of file Context.java.

2692  {
2693 
2694  checkContextMatch(p1);
2695  checkContextMatch(p2);
2696  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2697  p2.getNativeObject()));
2698  }
ArithExpr mkAdd ( ArithExpr...  t) throws Z3Exception
inline

Create an expression representing t[0] + t[1] + ....

Definition at line 763 of file Context.java.

764  {
765 
766  checkContextMatch(t);
767  return (ArithExpr) Expr.create(this,
768  Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t)));
769  }
BoolExpr mkAnd ( BoolExpr...  t) throws Z3Exception
inline

Create an expression representing t[0] and t[1] and ....

Definition at line 741 of file Context.java.

742  {
743 
744  checkContextMatch(t);
745  return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length,
746  AST.arrayToNative(t)));
747  }
Expr mkApp ( FuncDecl  f,
Expr...  args 
) throws Z3Exception
inline

Create a new function application.

Definition at line 624 of file Context.java.

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

625  {
626  checkContextMatch(f);
627  checkContextMatch(args);
628  return Expr.create(this, f, args);
629  }
ArrayExpr mkArrayConst ( Symbol  name,
Sort  domain,
Sort  range 
) throws Z3Exception
inline

Create an array constant.

Definition at line 1633 of file Context.java.

1635  {
1636 
1637  return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1638  }
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:191
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
ArrayExpr mkArrayConst ( String  name,
Sort  domain,
Sort  range 
) throws Z3Exception
inline

Create an array constant.

Definition at line 1643 of file Context.java.

1645  {
1646 
1647  return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1648  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:191
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
ArraySort mkArraySort ( Sort  domain,
Sort  range 
) throws Z3Exception
inline

Create a new array sort.

Definition at line 191 of file Context.java.

Referenced by Context.mkArrayConst().

192  {
193 
194  checkContextMatch(domain);
195  checkContextMatch(range);
196  return new ArraySort(this, domain, range);
197  }
def ArraySort(d, r)
Definition: z3py.py:3955
BitVecSort mkBitVecSort ( int  size) throws Z3Exception
inline

Create a new bit-vector sort.

Definition at line 182 of file Context.java.

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

183  {
184 
185  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
186  }
def BitVecSort
Definition: z3py.py:3435
BoolExpr mkBool ( boolean  value) throws Z3Exception
inline

Creates a Boolean value.

Definition at line 650 of file Context.java.

651  {
652  return value ? mkTrue() : mkFalse();
653  }
BoolExpr mkBoolConst ( Symbol  name) throws Z3Exception
inline

Create a Boolean constant.

Definition at line 552 of file Context.java.

553  {
554 
555  return (BoolExpr) mkConst(name, getBoolSort());
556  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
BoolExpr mkBoolConst ( String  name) throws Z3Exception
inline

Create a Boolean constant.

Definition at line 561 of file Context.java.

562  {
563 
564  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
565  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
BoolSort mkBoolSort ( ) throws Z3Exception
inline

Create a new Boolean sort.

Definition at line 136 of file Context.java.

137  {
138 
139  return new BoolSort(this);
140  }
def BoolSort
Definition: z3py.py:1325
Expr mkBound ( int  index,
Sort  ty 
) throws Z3Exception
inline

Creates a new bound variable.

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

Definition at line 482 of file Context.java.

483  {
484  return Expr.create(this,
485  Native.mkBound(nCtx(), index, ty.getNativeObject()));
486  }
BitVecNum mkBV ( String  v,
int  size 
) throws Z3Exception
inline

Create a bit-vector numeral.

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

Definition at line 2025 of file Context.java.

2026  {
2027 
2028  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2029  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1890
BitVecSort mkBitVecSort(int size)
Definition: Context.java:182
BitVecNum mkBV ( int  v,
int  size 
) throws Z3Exception
inline

Create a bit-vector numeral.

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

Definition at line 2035 of file Context.java.

2036  {
2037 
2038  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2039  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1890
BitVecSort mkBitVecSort(int size)
Definition: Context.java:182
BitVecNum mkBV ( long  v,
int  size 
) throws Z3Exception
inline

Create a bit-vector numeral.

Parameters
vvalue of the numeral.

*

Parameters
sizethe size of the bit-vector

Definition at line 2045 of file Context.java.

2046  {
2047 
2048  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2049  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1890
BitVecSort mkBitVecSort(int size)
Definition: Context.java:182
IntExpr mkBV2Int ( BitVecExpr  t,
boolean  signed 
) throws Z3Exception
inline

Create an integer from the bit-vector argument t .

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

[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 1509 of file Context.java.

1510  {
1511 
1512  checkContextMatch(t);
1513  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1514  (signed) ? true : false));
1515  }
BitVecExpr mkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 1071 of file Context.java.

1072  {
1073 
1074  checkContextMatch(t1);
1075  checkContextMatch(t2);
1076  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1077  t1.getNativeObject(), t2.getNativeObject()));
1078  }
BoolExpr mkBVAddNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
) throws Z3Exception
inline

Create a predicate that checks that the bit-wise addition does not overflow.

The arguments must be of bit-vector sort.

Definition at line 1521 of file Context.java.

1523  {
1524 
1525  checkContextMatch(t1);
1526  checkContextMatch(t2);
1527  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1528  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1529  : false));
1530  }
BoolExpr mkBVAddNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Create a predicate that checks that the bit-wise addition does not underflow.

The arguments must be of bit-vector sort.

Definition at line 1536 of file Context.java.

1538  {
1539 
1540  checkContextMatch(t1);
1541  checkContextMatch(t2);
1542  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1543  t1.getNativeObject(), t2.getNativeObject()));
1544  }
BitVecExpr mkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 982 of file Context.java.

983  {
984 
985  checkContextMatch(t1);
986  checkContextMatch(t2);
987  return new BitVecExpr(this, Native.mkBvand(nCtx(),
988  t1.getNativeObject(), t2.getNativeObject()));
989  }
BitVecExpr mkBVASHR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Arithmetic shift right

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

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

The arguments must have a bit-vector sort.

Definition at line 1416 of file Context.java.

1417  {
1418 
1419  checkContextMatch(t1);
1420  checkContextMatch(t2);
1421  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1422  t1.getNativeObject(), t2.getNativeObject()));
1423  }
BitVecExpr mkBVConst ( Symbol  name,
int  size 
) throws Z3Exception
inline

Creates a bit-vector constant.

Definition at line 606 of file Context.java.

607  {
608 
609  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
610  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:182
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
BitVecExpr mkBVConst ( String  name,
int  size 
) throws Z3Exception
inline

Creates a bit-vector constant.

Definition at line 615 of file Context.java.

616  {
617 
618  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
619  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:182
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
BitVecExpr mkBVLSHR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Logical shift right

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 1396 of file Context.java.

1397  {
1398 
1399  checkContextMatch(t1);
1400  checkContextMatch(t2);
1401  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1402  t1.getNativeObject(), t2.getNativeObject()));
1403  }
BitVecExpr mkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 1097 of file Context.java.

1098  {
1099 
1100  checkContextMatch(t1);
1101  checkContextMatch(t2);
1102  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1103  t1.getNativeObject(), t2.getNativeObject()));
1104  }
BoolExpr mkBVMulNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
) throws Z3Exception
inline

Create a predicate that checks that the bit-wise multiplication does not overflow.

The arguments must be of bit-vector sort.

Definition at line 1605 of file Context.java.

1607  {
1608 
1609  checkContextMatch(t1);
1610  checkContextMatch(t2);
1611  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1612  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1613  : false));
1614  }
BoolExpr mkBVMulNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Create a predicate that checks that the bit-wise multiplication does not underflow.

The arguments must be of bit-vector sort.

Definition at line 1620 of file Context.java.

1622  {
1623 
1624  checkContextMatch(t1);
1625  checkContextMatch(t2);
1626  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1627  t1.getNativeObject(), t2.getNativeObject()));
1628  }
BitVecExpr mkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Bitwise NAND.

The arguments must have a bit-vector sort.

Definition at line 1021 of file Context.java.

1022  {
1023 
1024  checkContextMatch(t1);
1025  checkContextMatch(t2);
1026  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1027  t1.getNativeObject(), t2.getNativeObject()));
1028  }
BitVecExpr mkBVNeg ( BitVecExpr  t) throws Z3Exception
inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 1060 of file Context.java.

1061  {
1062 
1063  checkContextMatch(t);
1064  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1065  }
BoolExpr mkBVNegNoOverflow ( BitVecExpr  t) throws Z3Exception
inline

Create a predicate that checks that the bit-wise negation does not overflow.

The arguments must be of bit-vector sort.

Definition at line 1593 of file Context.java.

1594  {
1595 
1596  checkContextMatch(t);
1597  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1598  t.getNativeObject()));
1599  }
BitVecExpr mkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Bitwise NOR.

The arguments must have a bit-vector sort.

Definition at line 1034 of file Context.java.

1035  {
1036 
1037  checkContextMatch(t1);
1038  checkContextMatch(t2);
1039  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1040  t1.getNativeObject(), t2.getNativeObject()));
1041  }
BitVecExpr mkBVNot ( BitVecExpr  t) throws Z3Exception
inline

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 947 of file Context.java.

948  {
949 
950  checkContextMatch(t);
951  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
952  }
BitVecExpr mkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 995 of file Context.java.

996  {
997 
998  checkContextMatch(t1);
999  checkContextMatch(t2);
1000  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1001  t2.getNativeObject()));
1002  }
BitVecExpr mkBVRedAND ( BitVecExpr  t) throws Z3Exception
inline

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

The argument must have a bit-vector sort.

Definition at line 958 of file Context.java.

959  {
960 
961  checkContextMatch(t);
962  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
963  t.getNativeObject()));
964  }
BitVecExpr mkBVRedOR ( BitVecExpr  t) throws Z3Exception
inline

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

The argument must have a bit-vector sort.

Definition at line 970 of file Context.java.

971  {
972 
973  checkContextMatch(t);
974  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
975  t.getNativeObject()));
976  }
BitVecExpr mkBVRotateLeft ( int  i,
BitVecExpr  t 
) throws Z3Exception
inline

Rotate Left.

Rotate bits of t to the left i times. The argument t must have a bit-vector sort.

Definition at line 1429 of file Context.java.

1430  {
1431 
1432  checkContextMatch(t);
1433  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1434  t.getNativeObject()));
1435  }
BitVecExpr mkBVRotateLeft ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Rotate Left.

Rotate bits of t1 to the left t2 times. The arguments must have the same bit-vector sort.

Definition at line 1454 of file Context.java.

1456  {
1457 
1458  checkContextMatch(t1);
1459  checkContextMatch(t2);
1460  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1461  t1.getNativeObject(), t2.getNativeObject()));
1462  }
BitVecExpr mkBVRotateRight ( int  i,
BitVecExpr  t 
) throws Z3Exception
inline

Rotate Right.

Rotate bits of t to the right i times. The argument t must have a bit-vector sort.

Definition at line 1441 of file Context.java.

1442  {
1443 
1444  checkContextMatch(t);
1445  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1446  t.getNativeObject()));
1447  }
BitVecExpr mkBVRotateRight ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Rotate Right.

Rotate bits of t1 to the rightt2 times. The arguments must have the same bit-vector sort.

Definition at line 1469 of file Context.java.

1471  {
1472 
1473  checkContextMatch(t1);
1474  checkContextMatch(t2);
1475  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1476  t1.getNativeObject(), t2.getNativeObject()));
1477  }
BitVecExpr mkBVSDiv ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Signed division.

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

If

t2

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

Definition at line 1133 of file Context.java.

1134  {
1135 
1136  checkContextMatch(t1);
1137  checkContextMatch(t2);
1138  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1139  t1.getNativeObject(), t2.getNativeObject()));
1140  }
BoolExpr mkBVSDivNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Create a predicate that checks that the bit-wise signed division does not overflow.

The arguments must be of bit-vector sort.

Definition at line 1579 of file Context.java.

1581  {
1582 
1583  checkContextMatch(t1);
1584  checkContextMatch(t2);
1585  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1586  t1.getNativeObject(), t2.getNativeObject()));
1587  }
BoolExpr mkBVSGE ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Two's complement signed greater than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1258 of file Context.java.

1259  {
1260 
1261  checkContextMatch(t1);
1262  checkContextMatch(t2);
1263  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1264  t2.getNativeObject()));
1265  }
BoolExpr mkBVSGT ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Two's complement signed greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1284 of file Context.java.

1285  {
1286 
1287  checkContextMatch(t1);
1288  checkContextMatch(t2);
1289  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1290  t2.getNativeObject()));
1291  }
BitVecExpr mkBVSHL ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Shift left.

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 1377 of file Context.java.

1378  {
1379 
1380  checkContextMatch(t1);
1381  checkContextMatch(t2);
1382  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1383  t1.getNativeObject(), t2.getNativeObject()));
1384  }
BoolExpr mkBVSLE ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Two's complement signed less-than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1232 of file Context.java.

1233  {
1234 
1235  checkContextMatch(t1);
1236  checkContextMatch(t2);
1237  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1238  t2.getNativeObject()));
1239  }
BoolExpr mkBVSLT ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Two's complement signed less-than

The arguments must have the same bit-vector sort.

Definition at line 1206 of file Context.java.

1207  {
1208 
1209  checkContextMatch(t1);
1210  checkContextMatch(t2);
1211  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1212  t2.getNativeObject()));
1213  }
BitVecExpr mkBVSMod ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

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

If

t2

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

Definition at line 1180 of file Context.java.

1181  {
1182 
1183  checkContextMatch(t1);
1184  checkContextMatch(t2);
1185  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1186  t1.getNativeObject(), t2.getNativeObject()));
1187  }
BitVecExpr mkBVSRem ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Signed remainder.

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 1166 of file Context.java.

1167  {
1168 
1169  checkContextMatch(t1);
1170  checkContextMatch(t2);
1171  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1172  t1.getNativeObject(), t2.getNativeObject()));
1173  }
BitVecExpr mkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 1084 of file Context.java.

1085  {
1086 
1087  checkContextMatch(t1);
1088  checkContextMatch(t2);
1089  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1090  t1.getNativeObject(), t2.getNativeObject()));
1091  }
BoolExpr mkBVSubNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Create a predicate that checks that the bit-wise subtraction does not overflow.

The arguments must be of bit-vector sort.

Definition at line 1550 of file Context.java.

1552  {
1553 
1554  checkContextMatch(t1);
1555  checkContextMatch(t2);
1556  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1557  t1.getNativeObject(), t2.getNativeObject()));
1558  }
BoolExpr mkBVSubNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
) throws Z3Exception
inline

Create a predicate that checks that the bit-wise subtraction does not underflow.

The arguments must be of bit-vector sort.

Definition at line 1564 of file Context.java.

1566  {
1567 
1568  checkContextMatch(t1);
1569  checkContextMatch(t2);
1570  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1571  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1572  : false));
1573  }
BitVecExpr mkBVUDiv ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Unsigned division.

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 1112 of file Context.java.

1113  {
1114 
1115  checkContextMatch(t1);
1116  checkContextMatch(t2);
1117  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1118  t1.getNativeObject(), t2.getNativeObject()));
1119  }
BoolExpr mkBVUGE ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Unsigned greater than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1245 of file Context.java.

1246  {
1247 
1248  checkContextMatch(t1);
1249  checkContextMatch(t2);
1250  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1251  t2.getNativeObject()));
1252  }
BoolExpr mkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Unsigned greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1271 of file Context.java.

1272  {
1273 
1274  checkContextMatch(t1);
1275  checkContextMatch(t2);
1276  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1277  t2.getNativeObject()));
1278  }
BoolExpr mkBVULE ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Unsigned less-than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1219 of file Context.java.

1220  {
1221 
1222  checkContextMatch(t1);
1223  checkContextMatch(t2);
1224  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1225  t2.getNativeObject()));
1226  }
BoolExpr mkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Unsigned less-than

The arguments must have the same bit-vector sort.

Definition at line 1193 of file Context.java.

1194  {
1195 
1196  checkContextMatch(t1);
1197  checkContextMatch(t2);
1198  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1199  t2.getNativeObject()));
1200  }
BitVecExpr mkBVURem ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Unsigned remainder.

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 1148 of file Context.java.

1149  {
1150 
1151  checkContextMatch(t1);
1152  checkContextMatch(t2);
1153  return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1154  t1.getNativeObject(), t2.getNativeObject()));
1155  }
BitVecExpr mkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Bitwise XNOR.

The arguments must have a bit-vector sort.

Definition at line 1047 of file Context.java.

1048  {
1049 
1050  checkContextMatch(t1);
1051  checkContextMatch(t2);
1052  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1053  t1.getNativeObject(), t2.getNativeObject()));
1054  }
BitVecExpr mkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 1008 of file Context.java.

1009  {
1010 
1011  checkContextMatch(t1);
1012  checkContextMatch(t2);
1013  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1014  t1.getNativeObject(), t2.getNativeObject()));
1015  }
BitVecExpr mkConcat ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception
inline

Bit-vector concatenation.

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 1302 of file Context.java.

1303  {
1304 
1305  checkContextMatch(t1);
1306  checkContextMatch(t2);
1307  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1308  t1.getNativeObject(), t2.getNativeObject()));
1309  }
Expr mkConst ( Symbol  name,
Sort  range 
) throws Z3Exception
inline

Creates a new Constant of sort range and named name .

Definition at line 505 of file Context.java.

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

506  {
507 
508  checkContextMatch(name);
509  checkContextMatch(range);
510 
511  return Expr.create(
512  this,
513  Native.mkConst(nCtx(), name.getNativeObject(),
514  range.getNativeObject()));
515  }
Expr mkConst ( String  name,
Sort  range 
) throws Z3Exception
inline

Creates a new Constant of sort range and named name .

Definition at line 521 of file Context.java.

522  {
523 
524  return mkConst(mkSymbol(name), range);
525  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
Expr mkConst ( FuncDecl  f) throws Z3Exception
inline

Creates a fresh constant from the FuncDecl f .

Parameters
fA decl of a 0-arity function

Definition at line 543 of file Context.java.

544  {
545 
546  return mkApp(f, (Expr[]) null);
547  }
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:624
ArrayExpr mkConstArray ( Sort  domain,
Expr  v 
) throws Z3Exception
inline

Create a constant array.

The resulting term is an array, such that a

on an arbitrary index produces the value

v

.

See also
MkArraySort, MkSelect

Definition at line 1699 of file Context.java.

1700  {
1701 
1702  checkContextMatch(domain);
1703  checkContextMatch(v);
1704  return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1705  domain.getNativeObject(), v.getNativeObject()));
1706  }
FuncDecl mkConstDecl ( Symbol  name,
Sort  range 
) throws Z3Exception
inline

Creates a new constant function declaration.

Definition at line 447 of file Context.java.

448  {
449 
450  checkContextMatch(name);
451  checkContextMatch(range);
452  return new FuncDecl(this, name, null, range);
453  }
FuncDecl mkConstDecl ( String  name,
Sort  range 
) throws Z3Exception
inline

Creates a new constant function declaration.

Definition at line 458 of file Context.java.

459  {
460 
461  checkContextMatch(range);
462  return new FuncDecl(this, mkSymbol(name), null, range);
463  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
Constructor mkConstructor ( Symbol  name,
Symbol  recognizer,
Symbol[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
) throws Z3Exception
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 287 of file Context.java.

290  {
291 
292  return new Constructor(this, name, recognizer, fieldNames, sorts,
293  sortRefs);
294  }
Constructor mkConstructor ( String  name,
String  recognizer,
String[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
) throws Z3Exception
inline

Create a datatype constructor.

Parameters
name
recognizer
fieldNames
sorts
sortRefs
Returns

Definition at line 303 of file Context.java.

306  {
307 
308  return new Constructor(this, mkSymbol(name), mkSymbol(recognizer),
309  MkSymbols(fieldNames), sorts, sortRefs);
310  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
DatatypeSort mkDatatypeSort ( Symbol  name,
Constructor[]  constructors 
) throws Z3Exception
inline

Create a new datatype sort.

Definition at line 315 of file Context.java.

317  {
318 
319  checkContextMatch(name);
320  checkContextMatch(constructors);
321  return new DatatypeSort(this, name, constructors);
322  }
DatatypeSort mkDatatypeSort ( String  name,
Constructor[]  constructors 
) throws Z3Exception
inline

Create a new datatype sort.

Definition at line 327 of file Context.java.

329  {
330 
331  checkContextMatch(constructors);
332  return new DatatypeSort(this, mkSymbol(name), constructors);
333  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
DatatypeSort [] mkDatatypeSorts ( Symbol[]  names,
Constructor  c[][] 
) throws Z3Exception
inline

Create mutually recursive datatypes.

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

Definition at line 340 of file Context.java.

Referenced by Context.mkDatatypeSorts().

342  {
343 
344  checkContextMatch(names);
345  int n = (int) names.length;
346  ConstructorList[] cla = new ConstructorList[n];
347  long[] n_constr = new long[n];
348  for (int i = 0; i < n; i++)
349  {
350  Constructor[] constructor = c[i];
351 
352  checkContextMatch(constructor);
353  cla[i] = new ConstructorList(this, constructor);
354  n_constr[i] = cla[i].getNativeObject();
355  }
356  long[] n_res = new long[n];
357  Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
358  n_constr);
359  DatatypeSort[] res = new DatatypeSort[n];
360  for (int i = 0; i < n; i++)
361  res[i] = new DatatypeSort(this, n_res[i]);
362  return res;
363  }
DatatypeSort [] mkDatatypeSorts ( String[]  names,
Constructor  c[][] 
) throws Z3Exception
inline

Create mutually recursive data-types.

Parameters
names
c
Returns

Definition at line 371 of file Context.java.

373  {
374 
375  return mkDatatypeSorts(MkSymbols(names), c);
376  }
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:340
BoolExpr mkDistinct ( Expr...  args) throws Z3Exception
inline

Creates a distinct term.

Definition at line 669 of file Context.java.

670  {
671  checkContextMatch(args);
672  return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length,
673  AST.arrayToNative(args)));
674  }
ArithExpr mkDiv ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 / t2.

Definition at line 807 of file Context.java.

808  {
809 
810  checkContextMatch(t1);
811  checkContextMatch(t2);
812  return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
813  t1.getNativeObject(), t2.getNativeObject()));
814  }
Expr mkEmptySet ( Sort  domain) throws Z3Exception
inline

Create an empty set.

Definition at line 1753 of file Context.java.

1754  {
1755 
1756  checkContextMatch(domain);
1757  return Expr.create(this,
1758  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1759  }
EnumSort mkEnumSort ( Symbol  name,
Symbol...  enumNames 
) throws Z3Exception
inline

Create a new enumeration sort.

Definition at line 216 of file Context.java.

218  {
219 
220  checkContextMatch(name);
221  checkContextMatch(enumNames);
222  return new EnumSort(this, name, enumNames);
223  }
def EnumSort
Definition: z3py.py:4398
EnumSort mkEnumSort ( String  name,
String...  enumNames 
) throws Z3Exception
inline

Create a new enumeration sort.

Definition at line 228 of file Context.java.

230  {
231  return new EnumSort(this, mkSymbol(name), MkSymbols(enumNames));
232  }
def EnumSort
Definition: z3py.py:4398
IntSymbol mkSymbol(int i)
Definition: Context.java:73
BoolExpr mkEq ( Expr  x,
Expr  y 
) throws Z3Exception
inline

Creates the equality x = y .

Definition at line 658 of file Context.java.

659  {
660  checkContextMatch(x);
661  checkContextMatch(y);
662  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
663  y.getNativeObject()));
664  }
Quantifier mkExists ( Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception
inline

Create an existential Quantifier.

See also
MkForall(Sort[],Symbol[],Expr,uint,Pattern[],Expr[],Symbol,Symbol)

Definition at line 2095 of file Context.java.

Referenced by Context.mkQuantifier().

2098  {
2099 
2100  return new Quantifier(this, false, sorts, names, body, weight,
2101  patterns, noPatterns, quantifierID, skolemID);
2102  }
Quantifier mkExists ( Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception
inline

Create an existential Quantifier.

Definition at line 2107 of file Context.java.

2110  {
2111 
2112  return new Quantifier(this, false, boundConstants, body, weight,
2113  patterns, noPatterns, quantifierID, skolemID);
2114  }
BitVecExpr mkExtract ( int  high,
int  low,
BitVecExpr  t 
) throws Z3Exception
inline

Bit-vector extraction.

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 1318 of file Context.java.

1320  {
1321 
1322  checkContextMatch(t);
1323  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1324  t.getNativeObject()));
1325  }
BoolExpr mkFalse ( ) throws Z3Exception
inline

The false Term.

Definition at line 642 of file Context.java.

Referenced by Context.mkBool().

643  {
644  return new BoolExpr(this, Native.mkFalse(nCtx()));
645  }
FiniteDomainSort mkFiniteDomainSort ( Symbol  name,
long  size 
) throws Z3Exception
inline

Create a new finite domain sort.

Definition at line 258 of file Context.java.

260  {
261 
262  checkContextMatch(name);
263  return new FiniteDomainSort(this, name, size);
264  }
FiniteDomainSort mkFiniteDomainSort ( String  name,
long  size 
) throws Z3Exception
inline

Create a new finite domain sort.

Definition at line 269 of file Context.java.

271  {
272 
273  return new FiniteDomainSort(this, mkSymbol(name), size);
274  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
Fixedpoint mkFixedpoint ( ) throws Z3Exception
inline

Create a Fixedpoint context.

Definition at line 2849 of file Context.java.

2850  {
2851 
2852  return new Fixedpoint(this);
2853  }
Quantifier mkForall ( Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception
inline

Create a universal Quantifier.

Creates a forall formula, where weight is the weight, patterns is an array of patterns, sorts is an array with the sorts of the bound variables, names is an array with the 'names' of the bound variables, and body is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation.

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.

Definition at line 2070 of file Context.java.

Referenced by Context.mkQuantifier().

2073  {
2074 
2075  return new Quantifier(this, true, sorts, names, body, weight, patterns,
2076  noPatterns, quantifierID, skolemID);
2077  }
Quantifier mkForall ( Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception
inline

Create a universal Quantifier.

Definition at line 2082 of file Context.java.

2085  {
2086 
2087  return new Quantifier(this, true, boundConstants, body, weight,
2088  patterns, noPatterns, quantifierID, skolemID);
2089  }
Expr mkFreshConst ( String  prefix,
Sort  range 
) throws Z3Exception
inline

Creates a fresh Constant of sort range and a name prefixed with prefix .

Definition at line 531 of file Context.java.

532  {
533 
534  checkContextMatch(range);
535  return Expr.create(this,
536  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
537  }
FuncDecl mkFreshConstDecl ( String  prefix,
Sort  range 
) throws Z3Exception
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 470 of file Context.java.

472  {
473 
474  checkContextMatch(range);
475  return new FuncDecl(this, prefix, null, range);
476  }
FuncDecl mkFreshFuncDecl ( String  prefix,
Sort[]  domain,
Sort  range 
) throws Z3Exception
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 435 of file Context.java.

437  {
438 
439  checkContextMatch(domain);
440  checkContextMatch(range);
441  return new FuncDecl(this, prefix, domain, range);
442  }
Expr mkFullSet ( Sort  domain) throws Z3Exception
inline

Create the full set.

Definition at line 1764 of file Context.java.

1765  {
1766 
1767  checkContextMatch(domain);
1768  return Expr.create(this,
1769  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1770  }
FuncDecl mkFuncDecl ( Symbol  name,
Sort[]  domain,
Sort  range 
) throws Z3Exception
inline

Creates a new function declaration.

Definition at line 381 of file Context.java.

383  {
384 
385  checkContextMatch(name);
386  checkContextMatch(domain);
387  checkContextMatch(range);
388  return new FuncDecl(this, name, domain, range);
389  }
FuncDecl mkFuncDecl ( Symbol  name,
Sort  domain,
Sort  range 
) throws Z3Exception
inline

Creates a new function declaration.

Definition at line 394 of file Context.java.

396  {
397 
398  checkContextMatch(name);
399  checkContextMatch(domain);
400  checkContextMatch(range);
401  Sort[] q = new Sort[] { domain };
402  return new FuncDecl(this, name, q, range);
403  }
FuncDecl mkFuncDecl ( String  name,
Sort[]  domain,
Sort  range 
) throws Z3Exception
inline

Creates a new function declaration.

Definition at line 408 of file Context.java.

410  {
411 
412  checkContextMatch(domain);
413  checkContextMatch(range);
414  return new FuncDecl(this, mkSymbol(name), domain, range);
415  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
FuncDecl mkFuncDecl ( String  name,
Sort  domain,
Sort  range 
) throws Z3Exception
inline

Creates a new function declaration.

Definition at line 420 of file Context.java.

422  {
423 
424  checkContextMatch(domain);
425  checkContextMatch(range);
426  Sort[] q = new Sort[] { domain };
427  return new FuncDecl(this, mkSymbol(name), q, range);
428  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
BoolExpr mkGe ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 >= t2

Definition at line 895 of file Context.java.

896  {
897 
898  checkContextMatch(t1);
899  checkContextMatch(t2);
900  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
901  t2.getNativeObject()));
902  }
Goal mkGoal ( boolean  models,
boolean  unsatCores,
boolean  proofs 
) throws Z3Exception
inline

Creates a new Goal.

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 2380 of file Context.java.

2382  {
2383 
2384  return new Goal(this, models, unsatCores, proofs);
2385  }
BoolExpr mkGt ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 > t2

Definition at line 883 of file Context.java.

884  {
885 
886  checkContextMatch(t1);
887  checkContextMatch(t2);
888  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
889  t2.getNativeObject()));
890  }
BoolExpr mkIff ( BoolExpr  t1,
BoolExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 iff t2.

Definition at line 705 of file Context.java.

706  {
707 
708  checkContextMatch(t1);
709  checkContextMatch(t2);
710  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
711  t2.getNativeObject()));
712  }
BoolExpr mkImplies ( BoolExpr  t1,
BoolExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 -> t2.

Definition at line 717 of file Context.java.

718  {
719 
720  checkContextMatch(t1);
721  checkContextMatch(t2);
722  return new BoolExpr(this, Native.mkImplies(nCtx(),
723  t1.getNativeObject(), t2.getNativeObject()));
724  }
IntNum mkInt ( String  v) throws Z3Exception
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 1989 of file Context.java.

1990  {
1991 
1992  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
1993  .getNativeObject()));
1994  }
IntNum mkInt ( int  v) throws Z3Exception
inline

Create an integer numeral.

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

Definition at line 2001 of file Context.java.

2002  {
2003 
2004  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2005  .getNativeObject()));
2006  }
IntNum mkInt ( long  v) throws Z3Exception
inline

Create an integer numeral.

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

Definition at line 2013 of file Context.java.

2014  {
2015 
2016  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2017  .getNativeObject()));
2018  }
BitVecExpr mkInt2BV ( int  n,
IntExpr  t 
) throws Z3Exception
inline

Create an n bit bit-vector from the integer argument t .

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

The argument must be of integer sort.

Definition at line 1487 of file Context.java.

1488  {
1489 
1490  checkContextMatch(t);
1491  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1492  t.getNativeObject()));
1493  }
RealExpr mkInt2Real ( IntExpr  t) throws Z3Exception
inline

Coerce an integer to a real.

There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.

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

k

and and asserting

MakeInt2Real(k) <= t1 < MkInt2Real(k)+1

. The argument must be of integer sort.

Definition at line 913 of file Context.java.

914  {
915 
916  checkContextMatch(t);
917  return new RealExpr(this,
918  Native.mkInt2real(nCtx(), t.getNativeObject()));
919  }
IntExpr mkIntConst ( Symbol  name) throws Z3Exception
inline

Creates an integer constant.

Definition at line 570 of file Context.java.

571  {
572 
573  return (IntExpr) mkConst(name, getIntSort());
574  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
IntExpr mkIntConst ( String  name) throws Z3Exception
inline

Creates an integer constant.

Definition at line 579 of file Context.java.

580  {
581 
582  return (IntExpr) mkConst(name, getIntSort());
583  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
IntSort mkIntSort ( ) throws Z3Exception
inline

Create a new integer sort.

Definition at line 164 of file Context.java.

165  {
166 
167  return new IntSort(this);
168  }
def IntSort
Definition: z3py.py:2614
BoolExpr mkIsInteger ( RealExpr  t) throws Z3Exception
inline

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

Definition at line 936 of file Context.java.

937  {
938 
939  checkContextMatch(t);
940  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
941  }
Expr mkITE ( BoolExpr  t1,
Expr  t2,
Expr  t3 
) throws Z3Exception
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 692 of file Context.java.

693  {
694 
695  checkContextMatch(t1);
696  checkContextMatch(t2);
697  checkContextMatch(t3);
698  return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
699  t2.getNativeObject(), t3.getNativeObject()));
700  }
BoolExpr mkLe ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 <= t2

Definition at line 871 of file Context.java.

872  {
873 
874  checkContextMatch(t1);
875  checkContextMatch(t2);
876  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
877  t2.getNativeObject()));
878  }
ListSort mkListSort ( Symbol  name,
Sort  elemSort 
) throws Z3Exception
inline

Create a new list sort.

Definition at line 237 of file Context.java.

238  {
239 
240  checkContextMatch(name);
241  checkContextMatch(elemSort);
242  return new ListSort(this, name, elemSort);
243  }
ListSort mkListSort ( String  name,
Sort  elemSort 
) throws Z3Exception
inline

Create a new list sort.

Definition at line 248 of file Context.java.

249  {
250 
251  checkContextMatch(elemSort);
252  return new ListSort(this, mkSymbol(name), elemSort);
253  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
BoolExpr mkLt ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 < t2

Definition at line 859 of file Context.java.

860  {
861 
862  checkContextMatch(t1);
863  checkContextMatch(t2);
864  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
865  t2.getNativeObject()));
866  }
ArrayExpr mkMap ( FuncDecl  f,
ArrayExpr...  args 
) throws Z3Exception
inline

Maps f on the argument arrays.

Eeach 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 1717 of file Context.java.

1718  {
1719 
1720  checkContextMatch(f);
1721  checkContextMatch(args);
1722  return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1723  f.getNativeObject(), AST.arrayLength(args),
1724  AST.arrayToNative(args)));
1725  }
IntExpr mkMod ( IntExpr  t1,
IntExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 mod t2.

The arguments must have int type.

Definition at line 820 of file Context.java.

821  {
822 
823  checkContextMatch(t1);
824  checkContextMatch(t2);
825  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
826  t2.getNativeObject()));
827  }
ArithExpr mkMul ( ArithExpr...  t) throws Z3Exception
inline

Create an expression representing t[0] * t[1] * ....

Definition at line 774 of file Context.java.

775  {
776 
777  checkContextMatch(t);
778  return (ArithExpr) Expr.create(this,
779  Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t)));
780  }
BoolExpr mkNot ( BoolExpr  a) throws Z3Exception
inline

Mk an expression representing not(a).

Definition at line 679 of file Context.java.

680  {
681 
682  checkContextMatch(a);
683  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
684  }
Expr mkNumeral ( String  v,
Sort  ty 
) throws Z3Exception
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 1890 of file Context.java.

Referenced by Context.mkBV().

1891  {
1892 
1893  checkContextMatch(ty);
1894  return Expr.create(this,
1895  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
1896  }
Expr mkNumeral ( int  v,
Sort  ty 
) throws Z3Exception
inline

Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.

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

Definition at line 1908 of file Context.java.

1909  {
1910 
1911  checkContextMatch(ty);
1912  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
1913  }
Expr mkNumeral ( long  v,
Sort  ty 
) throws Z3Exception
inline

Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.

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

Definition at line 1925 of file Context.java.

1926  {
1927 
1928  checkContextMatch(ty);
1929  return Expr.create(this,
1930  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
1931  }
BoolExpr mkOr ( BoolExpr...  t) throws Z3Exception
inline

Create an expression representing t[0] or t[1] or ....

Definition at line 752 of file Context.java.

753  {
754 
755  checkContextMatch(t);
756  return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length,
757  AST.arrayToNative(t)));
758  }
Params mkParams ( ) throws Z3Exception
inline

Creates a new ParameterSet.

Definition at line 2390 of file Context.java.

2391  {
2392 
2393  return new Params(this);
2394  }
Pattern mkPattern ( Expr...  terms) throws Z3Exception
inline

Create a quantifier pattern.

Definition at line 491 of file Context.java.

492  {
493  if (terms.length == 0)
494  throw new Z3Exception("Cannot create a pattern from zero terms");
495 
496  long[] termsNative = AST.arrayToNative(terms);
497  return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length,
498  termsNative));
499  }
ArithExpr mkPower ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 ^ t2.

Definition at line 845 of file Context.java.

846  {
847 
848  checkContextMatch(t1);
849  checkContextMatch(t2);
850  return (ArithExpr) Expr.create(
851  this,
852  Native.mkPower(nCtx(), t1.getNativeObject(),
853  t2.getNativeObject()));
854  }
Probe mkProbe ( String  name) throws Z3Exception
inline

Creates a new Probe.

Definition at line 2673 of file Context.java.

2674  {
2675  return new Probe(this, name);
2676  }
Quantifier mkQuantifier ( boolean  universal,
Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception
inline

Create a Quantifier.

Definition at line 2119 of file Context.java.

2123  {
2124 
2125  if (universal)
2126  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2127  quantifierID, skolemID);
2128  else
2129  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2130  quantifierID, skolemID);
2131  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2095
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2070
Quantifier mkQuantifier ( boolean  universal,
Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception
inline

Create a Quantifier.

Definition at line 2136 of file Context.java.

2139  {
2140 
2141  if (universal)
2142  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2143  quantifierID, skolemID);
2144  else
2145  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2146  quantifierID, skolemID);
2147  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2095
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2070
RatNum mkReal ( int  num,
int  den 
) throws Z3Exception
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 1940 of file Context.java.

1941  {
1942  if (den == 0)
1943  throw new Z3Exception("Denominator is zero");
1944 
1945  return new RatNum(this, Native.mkReal(nCtx(), num, den));
1946  }
RatNum mkReal ( String  v) throws Z3Exception
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 1954 of file Context.java.

1955  {
1956 
1957  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
1958  .getNativeObject()));
1959  }
RatNum mkReal ( int  v) throws Z3Exception
inline

Create a real numeral.

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

Definition at line 1966 of file Context.java.

1967  {
1968 
1969  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
1970  .getNativeObject()));
1971  }
RatNum mkReal ( long  v) throws Z3Exception
inline

Create a real numeral.

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

Definition at line 1978 of file Context.java.

1979  {
1980 
1981  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
1982  .getNativeObject()));
1983  }
IntExpr mkReal2Int ( RealExpr  t) throws Z3Exception
inline

Coerce a real to an integer.

The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort.

Definition at line 926 of file Context.java.

927  {
928 
929  checkContextMatch(t);
930  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
931  }
RealExpr mkRealConst ( Symbol  name) throws Z3Exception
inline

Creates a real constant.

Definition at line 588 of file Context.java.

589  {
590 
591  return (RealExpr) mkConst(name, getRealSort());
592  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
RealExpr mkRealConst ( String  name) throws Z3Exception
inline

Creates a real constant.

Definition at line 597 of file Context.java.

598  {
599 
600  return (RealExpr) mkConst(name, getRealSort());
601  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
RealSort mkRealSort ( ) throws Z3Exception
inline

Create a real sort.

Definition at line 173 of file Context.java.

174  {
175 
176  return new RealSort(this);
177  }
def RealSort
Definition: z3py.py:2630
IntExpr mkRem ( IntExpr  t1,
IntExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 rem t2.

The arguments must have int type.

Definition at line 833 of file Context.java.

834  {
835 
836  checkContextMatch(t1);
837  checkContextMatch(t2);
838  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
839  t2.getNativeObject()));
840  }
BitVecExpr mkRepeat ( int  i,
BitVecExpr  t 
) throws Z3Exception
inline

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1359 of file Context.java.

1360  {
1361 
1362  checkContextMatch(t);
1363  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1364  t.getNativeObject()));
1365  }
Expr mkSelect ( ArrayExpr  a,
Expr  i 
) throws Z3Exception
inline

Array read.

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

range

.

See also
MkArraySort, MkStore

Definition at line 1659 of file Context.java.

1660  {
1661 
1662  checkContextMatch(a);
1663  checkContextMatch(i);
1664  return Expr.create(
1665  this,
1666  Native.mkSelect(nCtx(), a.getNativeObject(),
1667  i.getNativeObject()));
1668  }
Expr mkSetAdd ( Expr  set,
Expr  element 
) throws Z3Exception
inline

Add an element to the set.

Definition at line 1775 of file Context.java.

1776  {
1777 
1778  checkContextMatch(set);
1779  checkContextMatch(element);
1780  return Expr.create(
1781  this,
1782  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1783  element.getNativeObject()));
1784  }
Expr mkSetComplement ( Expr  arg) throws Z3Exception
inline

Take the complement of a set.

Definition at line 1843 of file Context.java.

1844  {
1845 
1846  checkContextMatch(arg);
1847  return Expr.create(this,
1848  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1849  }
Expr mkSetDel ( Expr  set,
Expr  element 
) throws Z3Exception
inline

Remove an element from a set.

Definition at line 1789 of file Context.java.

1790  {
1791 
1792  checkContextMatch(set);
1793  checkContextMatch(element);
1794  return Expr.create(
1795  this,
1796  Native.mkSetDel(nCtx(), set.getNativeObject(),
1797  element.getNativeObject()));
1798  }
Expr mkSetDifference ( Expr  arg1,
Expr  arg2 
) throws Z3Exception
inline

Take the difference between two sets.

Definition at line 1829 of file Context.java.

1830  {
1831 
1832  checkContextMatch(arg1);
1833  checkContextMatch(arg2);
1834  return Expr.create(
1835  this,
1836  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1837  arg2.getNativeObject()));
1838  }
Expr mkSetIntersection ( Expr...  args) throws Z3Exception
inline

Take the intersection of a list of sets.

Definition at line 1816 of file Context.java.

1817  {
1818 
1819  checkContextMatch(args);
1820  return Expr.create(
1821  this,
1822  Native.mkSetIntersect(nCtx(), (int) args.length,
1823  AST.arrayToNative(args)));
1824  }
Expr mkSetMembership ( Expr  elem,
Expr  set 
) throws Z3Exception
inline

Check for set membership.

Definition at line 1854 of file Context.java.

1855  {
1856 
1857  checkContextMatch(elem);
1858  checkContextMatch(set);
1859  return Expr.create(
1860  this,
1861  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1862  set.getNativeObject()));
1863  }
SetSort mkSetSort ( Sort  ty) throws Z3Exception
inline

Create a set type.

Definition at line 1743 of file Context.java.

1744  {
1745 
1746  checkContextMatch(ty);
1747  return new SetSort(this, ty);
1748  }
Expr mkSetSubset ( Expr  arg1,
Expr  arg2 
) throws Z3Exception
inline

Check for subsetness of sets.

Definition at line 1868 of file Context.java.

1869  {
1870 
1871  checkContextMatch(arg1);
1872  checkContextMatch(arg2);
1873  return Expr.create(
1874  this,
1875  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1876  arg2.getNativeObject()));
1877  }
Expr mkSetUnion ( Expr...  args) throws Z3Exception
inline

Take the union of a list of sets.

Definition at line 1803 of file Context.java.

1804  {
1805 
1806  checkContextMatch(args);
1807  return Expr.create(
1808  this,
1809  Native.mkSetUnion(nCtx(), (int) args.length,
1810  AST.arrayToNative(args)));
1811  }
BitVecExpr mkSignExt ( int  i,
BitVecExpr  t 
) throws Z3Exception
inline

Bit-vector sign extension.

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 1333 of file Context.java.

1334  {
1335 
1336  checkContextMatch(t);
1337  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1338  t.getNativeObject()));
1339  }
Solver mkSimpleSolver ( ) throws Z3Exception
inline

Creates a new (incremental) solver.

Definition at line 2828 of file Context.java.

2829  {
2830 
2831  return new Solver(this, Native.mkSimpleSolver(nCtx()));
2832  }
Solver mkSolver ( ) throws Z3Exception
inline

Creates a new (incremental) solver.

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

Definition at line 2795 of file Context.java.

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

2796  {
2797  return mkSolver((Symbol) null);
2798  }
Solver mkSolver ( Symbol  logic) throws Z3Exception
inline

Creates a new (incremental) solver.

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

Definition at line 2806 of file Context.java.

2807  {
2808 
2809  if (logic == null)
2810  return new Solver(this, Native.mkSolver(nCtx()));
2811  else
2812  return new Solver(this, Native.mkSolverForLogic(nCtx(),
2813  logic.getNativeObject()));
2814  }
Solver mkSolver ( String  logic) throws Z3Exception
inline

Creates a new (incremental) solver.

See also
MkSolver(Symbol)

Definition at line 2819 of file Context.java.

2820  {
2821 
2822  return mkSolver(mkSymbol(logic));
2823  }
IntSymbol mkSymbol(int i)
Definition: Context.java:73
Solver mkSolver ( Tactic  t) throws Z3Exception
inline

Creates a solver that is implemented using the given tactic.

The solver supports the commands

Push

and

Pop

, but it will always solve each check from scratch.

Definition at line 2839 of file Context.java.

2840  {
2841 
2842  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
2843  t.getNativeObject()));
2844  }
ArrayExpr mkStore ( ArrayExpr  a,
Expr  i,
Expr  v 
) throws Z3Exception
inline

Array update.

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 1683 of file Context.java.

1684  {
1685 
1686  checkContextMatch(a);
1687  checkContextMatch(i);
1688  checkContextMatch(v);
1689  return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1690  i.getNativeObject(), v.getNativeObject()));
1691  }
ArithExpr mkSub ( ArithExpr...  t) throws Z3Exception
inline

Create an expression representing t[0] - t[1] - ....

Definition at line 785 of file Context.java.

786  {
787 
788  checkContextMatch(t);
789  return (ArithExpr) Expr.create(this,
790  Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t)));
791  }
IntSymbol mkSymbol ( int  i) throws Z3Exception
inline

Creates a new symbol using an integer.

Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.

Definition at line 73 of file Context.java.

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

74  {
75  return new IntSymbol(this, i);
76  }
StringSymbol mkSymbol ( String  name) throws Z3Exception
inline

Create a symbol using a string.

Definition at line 81 of file Context.java.

82  {
83  return new StringSymbol(this, name);
84  }
Tactic mkTactic ( String  name) throws Z3Exception
inline

Creates a new Tactic.

Definition at line 2430 of file Context.java.

Referenced by Goal.simplify().

2431  {
2432 
2433  return new Tactic(this, name);
2434  }
Expr mkTermArray ( ArrayExpr  array) throws Z3Exception
inline

Access the array default value.

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

Definition at line 1732 of file Context.java.

1733  {
1734 
1735  checkContextMatch(array);
1736  return Expr.create(this,
1737  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1738  }
BoolExpr mkTrue ( ) throws Z3Exception
inline

The true Term.

Definition at line 634 of file Context.java.

Referenced by Context.mkBool().

635  {
636  return new BoolExpr(this, Native.mkTrue(nCtx()));
637  }
TupleSort mkTupleSort ( Symbol  name,
Symbol[]  fieldNames,
Sort[]  fieldSorts 
) throws Z3Exception
inline

Create a new tuple sort.

Definition at line 202 of file Context.java.

204  {
205 
206  checkContextMatch(name);
207  checkContextMatch(fieldNames);
208  checkContextMatch(fieldSorts);
209  return new TupleSort(this, name, (int) fieldNames.length, fieldNames,
210  fieldSorts);
211  }
ArithExpr mkUnaryMinus ( ArithExpr  t) throws Z3Exception
inline

Create an expression representing -t.

Definition at line 796 of file Context.java.

797  {
798 
799  checkContextMatch(t);
800  return (ArithExpr) Expr.create(this,
801  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
802  }
UninterpretedSort mkUninterpretedSort ( Symbol  s) throws Z3Exception
inline

Create a new uninterpreted sort.

Definition at line 145 of file Context.java.

Referenced by Context.mkUninterpretedSort().

146  {
147 
148  checkContextMatch(s);
149  return new UninterpretedSort(this, s);
150  }
UninterpretedSort mkUninterpretedSort ( String  str) throws Z3Exception
inline

Create a new uninterpreted sort.

Definition at line 155 of file Context.java.

156  {
157 
158  return mkUninterpretedSort(mkSymbol(str));
159  }
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:145
IntSymbol mkSymbol(int i)
Definition: Context.java:73
BoolExpr mkXor ( BoolExpr  t1,
BoolExpr  t2 
) throws Z3Exception
inline

Create an expression representing t1 xor t2.

Definition at line 729 of file Context.java.

730  {
731 
732  checkContextMatch(t1);
733  checkContextMatch(t2);
734  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
735  t2.getNativeObject()));
736  }
BitVecExpr mkZeroExt ( int  i,
BitVecExpr  t 
) throws Z3Exception
inline

Bit-vector zero extension.

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 1347 of file Context.java.

1348  {
1349 
1350  checkContextMatch(t);
1351  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1352  t.getNativeObject()));
1353  }
Probe not ( Probe  p) throws Z3Exception
inline

Create a probe that evaluates to "true" when the value p does not evaluate to "true".

Definition at line 2782 of file Context.java.

2783  {
2784 
2785  checkContextMatch(p);
2786  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2787  }
Probe or ( Probe  p1,
Probe  p2 
) throws Z3Exception
inline

Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".

Definition at line 2770 of file Context.java.

2771  {
2772  checkContextMatch(p1);
2773  checkContextMatch(p2);
2774  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
2775  p2.getNativeObject()));
2776  }
Tactic orElse ( Tactic  t1,
Tactic  t2 
) throws Z3Exception
inline

Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal.

Definition at line 2480 of file Context.java.

2481  {
2482 
2483  checkContextMatch(t1);
2484  checkContextMatch(t2);
2485  return new Tactic(this, Native.tacticOrElse(nCtx(),
2486  t1.getNativeObject(), t2.getNativeObject()));
2487  }
Tactic parAndThen ( Tactic  t1,
Tactic  t2 
) throws Z3Exception
inline

Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 . The subgoals are processed in parallel.

Definition at line 2622 of file Context.java.

2623  {
2624 
2625  checkContextMatch(t1);
2626  checkContextMatch(t2);
2627  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2628  t1.getNativeObject(), t2.getNativeObject()));
2629  }
Tactic parOr ( Tactic...  t) throws Z3Exception
inline

Create a tactic that applies the given tactics in parallel.

Definition at line 2610 of file Context.java.

2611  {
2612  checkContextMatch(t);
2613  return new Tactic(this, Native.tacticParOr(nCtx(),
2614  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2615  }
BoolExpr parseSMTLIB2File ( String  fileName,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
) throws Z3Exception
inline

Parse the given file using the SMT-LIB2 parser.

See also
ParseSMTLIB2String

Definition at line 2353 of file Context.java.

2356  {
2357 
2358  int csn = Symbol.arrayLength(sortNames);
2359  int cs = Sort.arrayLength(sorts);
2360  int cdn = Symbol.arrayLength(declNames);
2361  int cd = AST.arrayLength(decls);
2362  if (csn != cs || cdn != cd)
2363  throw new Z3Exception("Argument size mismatch");
2364  return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
2365  fileName, AST.arrayLength(sorts),
2366  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2367  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2368  AST.arrayToNative(decls)));
2369  }
BoolExpr parseSMTLIB2String ( String  str,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
) throws Z3Exception
inline

Parse the given string using the SMT-LIB2 parser.

See also
ParseSMTLIBString
Returns
A conjunction of assertions in the scope (up to push/pop) at the end of the string.

Definition at line 2332 of file Context.java.

2335  {
2336 
2337  int csn = Symbol.arrayLength(sortNames);
2338  int cs = Sort.arrayLength(sorts);
2339  int cdn = Symbol.arrayLength(declNames);
2340  int cd = AST.arrayLength(decls);
2341  if (csn != cs || cdn != cd)
2342  throw new Z3Exception("Argument size mismatch");
2343  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2344  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2345  AST.arrayToNative(sorts), AST.arrayLength(decls),
2346  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2347  }
void parseSMTLIBFile ( String  fileName,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
) throws Z3Exception
inline

Parse the given file using the SMT-LIB parser.

See also
ParseSMTLIBString

Definition at line 2215 of file Context.java.

2218  {
2219  int csn = Symbol.arrayLength(sortNames);
2220  int cs = Sort.arrayLength(sorts);
2221  int cdn = Symbol.arrayLength(declNames);
2222  int cd = AST.arrayLength(decls);
2223  if (csn != cs || cdn != cd)
2224  throw new Z3Exception("Argument size mismatch");
2225  Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
2226  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2227  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2228  AST.arrayToNative(decls));
2229  }
void parseSMTLIBString ( String  str,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
) throws Z3Exception
inline

Parse the given string using the SMT-LIB parser.

The symbol table of the parser can be initialized using the given sorts and declarations. The symbols in the arrays sortNames and declNames don't need to match the names of the sorts and declarations in the arrays sorts and decls . This is a useful feature since we can use arbitrary names to reference sorts and declarations.

Definition at line 2196 of file Context.java.

2198  {
2199  int csn = Symbol.arrayLength(sortNames);
2200  int cs = Sort.arrayLength(sorts);
2201  int cdn = Symbol.arrayLength(declNames);
2202  int cd = AST.arrayLength(decls);
2203  if (csn != cs || cdn != cd)
2204  throw new Z3Exception("Argument size mismatch");
2205  Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
2206  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2207  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2208  AST.arrayToNative(decls));
2209  }
Tactic repeat ( Tactic  t,
int  max 
) throws Z3Exception
inline

Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.

Definition at line 2538 of file Context.java.

2539  {
2540 
2541  checkContextMatch(t);
2542  return new Tactic(this, Native.tacticRepeat(nCtx(),
2543  t.getNativeObject(), max));
2544  }
void setPrintMode ( Z3_ast_print_mode  value) throws Z3Exception
inline

Selects the format used for pretty-printing expressions.

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

See also
AST.ToString(), Pattern.ToString(), FuncDecl.ToString(), Sort.ToString()

Definition at line 2160 of file Context.java.

2161  {
2162  Native.setAstPrintMode(nCtx(), value.toInt());
2163  }
String SimplifyHelp ( ) throws Z3Exception
inline

Return a string describing all available parameters to Expr.Simplify.

Definition at line 2888 of file Context.java.

2889  {
2890 
2891  return Native.simplifyGetHelp(nCtx());
2892  }
Tactic skip ( ) throws Z3Exception
inline

Create a tactic that just returns the given goal.

Definition at line 2549 of file Context.java.

2550  {
2551 
2552  return new Tactic(this, Native.tacticSkip(nCtx()));
2553  }
Tactic then ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
) throws Z3Exception
inline

Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .

Shorthand for

.

Definition at line 2470 of file Context.java.

2471  {
2472  return andThen(t1, t2, ts);
2473  }
Tactic andThen(Tactic t1, Tactic t2, Tactic...ts)
Definition: Context.java:2440
static void ToggleWarningMessages ( boolean  enabled) throws Z3Exception
inlinestatic

Enable/disable printing of warning messages to the console.

Note that this function is static and effects the behaviour of all contexts globally.

Definition at line 2907 of file Context.java.

2909  {
2910  Native.toggleWarningMessages((enabled) ? true : false);
2911  }
Tactic tryFor ( Tactic  t,
int  ms 
) throws Z3Exception
inline

Create a tactic that applies t to a goal for ms milliseconds.

If t does not terminate within ms milliseconds, then it fails.

Definition at line 2495 of file Context.java.

2496  {
2497 
2498  checkContextMatch(t);
2499  return new Tactic(this, Native.tacticTryFor(nCtx(),
2500  t.getNativeObject(), ms));
2501  }
long unwrapAST ( AST  a)
inline

Unwraps an AST.

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

See also
Native.Z3_inc_ref

).

See also
WrapAST
Parameters
aThe AST to unwrap.

Definition at line 2879 of file Context.java.

2880  {
2881  return a.getNativeObject();
2882  }
void updateParamValue ( String  id,
String  value 
) throws Z3Exception
inline

Update a mutable configuration parameter.

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 2920 of file Context.java.

2921  {
2922  Native.updateParamValue(nCtx(), id, value);
2923  }
Tactic usingParams ( Tactic  t,
Params  p 
) throws Z3Exception
inline

Create a tactic that applies t using the given set of parameters p .

Definition at line 2589 of file Context.java.

Referenced by Context.with().

2590  {
2591  checkContextMatch(t);
2592  checkContextMatch(p);
2593  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2594  t.getNativeObject(), p.getNativeObject()));
2595  }
Tactic when ( Probe  p,
Tactic  t 
) throws Z3Exception
inline

Create a tactic that applies t to a given goal if the probe p evaluates to true.

If p evaluates to false, then the new tactic behaves like the

tactic.

Definition at line 2509 of file Context.java.

2510  {
2511 
2512  checkContextMatch(t);
2513  checkContextMatch(p);
2514  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2515  t.getNativeObject()));
2516  }
Tactic with ( Tactic  t,
Params  p 
) throws Z3Exception
inline

Create a tactic that applies t using the given set of parameters p .

Alias for

UsingParams

Definition at line 2602 of file Context.java.

2603  {
2604  return usingParams(t, p);
2605  }
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2589
AST wrapAST ( long  nativeObject) throws Z3Exception
inline

Wraps an AST.

This function is used for transitions between native and managed objects. Note that nativeObject must be a native object obtained from Z3 (e.g., through

See also
UnwrapAST, Native.Z3_inc_ref

) and that it must have a correct reference count (see e.g., .

See also
UnwrapAST
Parameters
nativeObjectThe native pointer to wrap.

Definition at line 2864 of file Context.java.

2865  {
2866 
2867  return AST.create(this, nativeObject);
2868  }

Field Documentation

long m_refCount = 0
protected

Definition at line 3042 of file Context.java.

Referenced by Z3Object.dispose().