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

Public Member Functions

 Context ()
 
 Context (Map< String, String > settings)
 
IntSymbol mkSymbol (int i)
 
StringSymbol mkSymbol (String name)
 
BoolSort getBoolSort ()
 
IntSort getIntSort ()
 
RealSort getRealSort ()
 
BoolSort mkBoolSort ()
 
UninterpretedSort mkUninterpretedSort (Symbol s)
 
UninterpretedSort mkUninterpretedSort (String str)
 
IntSort mkIntSort ()
 
RealSort mkRealSort ()
 
BitVecSort mkBitVecSort (int size)
 
ArraySort mkArraySort (Sort domain, Sort range)
 
TupleSort mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
 
EnumSort mkEnumSort (Symbol name, Symbol...enumNames)
 
EnumSort mkEnumSort (String name, String...enumNames)
 
ListSort mkListSort (Symbol name, Sort elemSort)
 
ListSort mkListSort (String name, Sort elemSort)
 
FiniteDomainSort mkFiniteDomainSort (Symbol name, long size)
 
FiniteDomainSort mkFiniteDomainSort (String name, long size)
 
Constructor mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
 
Constructor mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
 
DatatypeSort mkDatatypeSort (Symbol name, Constructor[] constructors)
 
DatatypeSort mkDatatypeSort (String name, Constructor[] constructors)
 
DatatypeSort[] mkDatatypeSorts (Symbol[] names, Constructor[][] c)
 
DatatypeSort[] mkDatatypeSorts (String[] names, Constructor[][] c)
 
FuncDecl mkFuncDecl (Symbol name, Sort[] domain, Sort range)
 
FuncDecl mkFuncDecl (Symbol name, Sort domain, Sort range)
 
FuncDecl mkFuncDecl (String name, Sort[] domain, Sort range)
 
FuncDecl mkFuncDecl (String name, Sort domain, Sort range)
 
FuncDecl mkFreshFuncDecl (String prefix, Sort[] domain, Sort range)
 
FuncDecl mkConstDecl (Symbol name, Sort range)
 
FuncDecl mkConstDecl (String name, Sort range)
 
FuncDecl mkFreshConstDecl (String prefix, Sort range)
 
Expr mkBound (int index, Sort ty)
 
Pattern mkPattern (Expr...terms)
 
Expr mkConst (Symbol name, Sort range)
 
Expr mkConst (String name, Sort range)
 
Expr mkFreshConst (String prefix, Sort range)
 
Expr mkConst (FuncDecl f)
 
BoolExpr mkBoolConst (Symbol name)
 
BoolExpr mkBoolConst (String name)
 
IntExpr mkIntConst (Symbol name)
 
IntExpr mkIntConst (String name)
 
RealExpr mkRealConst (Symbol name)
 
RealExpr mkRealConst (String name)
 
BitVecExpr mkBVConst (Symbol name, int size)
 
BitVecExpr mkBVConst (String name, int size)
 
Expr mkApp (FuncDecl f, Expr...args)
 
BoolExpr mkTrue ()
 
BoolExpr mkFalse ()
 
BoolExpr mkBool (boolean value)
 
BoolExpr mkEq (Expr x, Expr y)
 
BoolExpr mkDistinct (Expr...args)
 
BoolExpr mkNot (BoolExpr a)
 
Expr mkITE (BoolExpr t1, Expr t2, Expr t3)
 
BoolExpr mkIff (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkImplies (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkXor (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkAnd (BoolExpr...t)
 
BoolExpr mkOr (BoolExpr...t)
 
ArithExpr mkAdd (ArithExpr...t)
 
ArithExpr mkMul (ArithExpr...t)
 
ArithExpr mkSub (ArithExpr...t)
 
ArithExpr mkUnaryMinus (ArithExpr t)
 
ArithExpr mkDiv (ArithExpr t1, ArithExpr t2)
 
IntExpr mkMod (IntExpr t1, IntExpr t2)
 
IntExpr mkRem (IntExpr t1, IntExpr t2)
 
ArithExpr mkPower (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkLt (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkLe (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkGt (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkGe (ArithExpr t1, ArithExpr t2)
 
RealExpr mkInt2Real (IntExpr t)
 
IntExpr mkReal2Int (RealExpr t)
 
BoolExpr mkIsInteger (RealExpr t)
 
BitVecExpr mkBVNot (BitVecExpr t)
 
BitVecExpr mkBVRedAND (BitVecExpr t)
 
BitVecExpr mkBVRedOR (BitVecExpr t)
 
BitVecExpr mkBVAND (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVXOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNAND (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVXNOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNeg (BitVecExpr t)
 
BitVecExpr mkBVAdd (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSub (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVMul (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVUDiv (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSDiv (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVURem (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSRem (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSMod (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVULT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSLT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVULE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSLE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVUGE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSGE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVUGT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSGT (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkConcat (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkExtract (int high, int low, BitVecExpr t)
 
BitVecExpr mkSignExt (int i, BitVecExpr t)
 
BitVecExpr mkZeroExt (int i, BitVecExpr t)
 
BitVecExpr mkRepeat (int i, BitVecExpr t)
 
BitVecExpr mkBVSHL (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVLSHR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVASHR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVRotateLeft (int i, BitVecExpr t)
 
BitVecExpr mkBVRotateRight (int i, BitVecExpr t)
 
BitVecExpr mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVRotateRight (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkInt2BV (int n, IntExpr t)
 
IntExpr mkBV2Int (BitVecExpr t, boolean signed)
 
BoolExpr mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVNegNoOverflow (BitVecExpr t)
 
BoolExpr mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 
ArrayExpr mkArrayConst (Symbol name, Sort domain, Sort range)
 
ArrayExpr mkArrayConst (String name, Sort domain, Sort range)
 
Expr mkSelect (ArrayExpr a, Expr i)
 
ArrayExpr mkStore (ArrayExpr a, Expr i, Expr v)
 
ArrayExpr mkConstArray (Sort domain, Expr v)
 
ArrayExpr mkMap (FuncDecl f, ArrayExpr...args)
 
Expr mkTermArray (ArrayExpr array)
 
SetSort mkSetSort (Sort ty)
 
Expr mkEmptySet (Sort domain)
 
Expr mkFullSet (Sort domain)
 
Expr mkSetAdd (Expr set, Expr element)
 
Expr mkSetDel (Expr set, Expr element)
 
Expr mkSetUnion (Expr...args)
 
Expr mkSetIntersection (Expr...args)
 
Expr mkSetDifference (Expr arg1, Expr arg2)
 
Expr mkSetComplement (Expr arg)
 
Expr mkSetMembership (Expr elem, Expr set)
 
Expr mkSetSubset (Expr arg1, Expr arg2)
 
Expr mkNumeral (String v, Sort ty)
 
Expr mkNumeral (int v, Sort ty)
 
Expr mkNumeral (long v, Sort ty)
 
RatNum mkReal (int num, int den)
 
RatNum mkReal (String v)
 
RatNum mkReal (int v)
 
RatNum mkReal (long v)
 
IntNum mkInt (String v)
 
IntNum mkInt (int v)
 
IntNum mkInt (long v)
 
BitVecNum mkBV (String v, int size)
 
BitVecNum mkBV (int v, int size)
 
BitVecNum mkBV (long v, int size)
 
Quantifier mkForall (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkForall (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkExists (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkExists (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkQuantifier (boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
void setPrintMode (Z3_ast_print_mode value)
 
String benchmarkToSMTString (String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
 
void parseSMTLIBString (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
 
void parseSMTLIBFile (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
 
int getNumSMTLIBFormulas ()
 
BoolExpr[] getSMTLIBFormulas ()
 
int getNumSMTLIBAssumptions ()
 
BoolExpr[] getSMTLIBAssumptions ()
 
int getNumSMTLIBDecls ()
 
FuncDecl[] getSMTLIBDecls ()
 
int getNumSMTLIBSorts ()
 
Sort[] getSMTLIBSorts ()
 
BoolExpr parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
 
BoolExpr parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
 
Goal mkGoal (boolean models, boolean unsatCores, boolean proofs)
 
Params mkParams ()
 
int getNumTactics ()
 
String[] getTacticNames ()
 
String getTacticDescription (String name)
 
Tactic mkTactic (String name)
 
Tactic andThen (Tactic t1, Tactic t2, Tactic...ts)
 
Tactic then (Tactic t1, Tactic t2, Tactic...ts)
 
Tactic orElse (Tactic t1, Tactic t2)
 
Tactic tryFor (Tactic t, int ms)
 
Tactic when (Probe p, Tactic t)
 
Tactic cond (Probe p, Tactic t1, Tactic t2)
 
Tactic repeat (Tactic t, int max)
 
Tactic skip ()
 
Tactic fail ()
 
Tactic failIf (Probe p)
 
Tactic failIfNotDecided ()
 
Tactic usingParams (Tactic t, Params p)
 
Tactic with (Tactic t, Params p)
 
Tactic parOr (Tactic...t)
 
Tactic parAndThen (Tactic t1, Tactic t2)
 
void interrupt ()
 
int getNumProbes ()
 
String[] getProbeNames ()
 
String getProbeDescription (String name)
 
Probe mkProbe (String name)
 
Probe constProbe (double val)
 
Probe lt (Probe p1, Probe p2)
 
Probe gt (Probe p1, Probe p2)
 
Probe le (Probe p1, Probe p2)
 
Probe ge (Probe p1, Probe p2)
 
Probe eq (Probe p1, Probe p2)
 
Probe and (Probe p1, Probe p2)
 
Probe or (Probe p1, Probe p2)
 
Probe not (Probe p)
 
Solver mkSolver ()
 
Solver mkSolver (Symbol logic)
 
Solver mkSolver (String logic)
 
Solver mkSimpleSolver ()
 
Solver mkSolver (Tactic t)
 
Fixedpoint mkFixedpoint ()
 
FPRMSort mkFPRoundingModeSort ()
 
FPRMExpr mkFPRoundNearestTiesToEven ()
 
FPRMNum mkFPRNE ()
 
FPRMNum mkFPRoundNearestTiesToAway ()
 
FPRMNum mkFPRNA ()
 
FPRMNum mkFPRoundTowardPositive ()
 
FPRMNum mkFPRTP ()
 
FPRMNum mkFPRoundTowardNegative ()
 
FPRMNum mkFPRTN ()
 
FPRMNum mkFPRoundTowardZero ()
 
FPRMNum mkFPRTZ ()
 
FPSort mkFPSort (int ebits, int sbits)
 
FPSort mkFPSortHalf ()
 
FPSort mkFPSort16 ()
 
FPSort mkFPSortSingle ()
 
FPSort mkFPSort32 ()
 
FPSort mkFPSortDouble ()
 
FPSort mkFPSort64 ()
 
FPSort mkFPSortQuadruple ()
 
FPSort mkFPSort128 ()
 
FPNum mkFPNaN (FPSort s)
 
FPNum mkFPInf (FPSort s, boolean negative)
 
FPNum mkFPZero (FPSort s, boolean negative)
 
FPNum mkFPNumeral (float v, FPSort s)
 
FPNum mkFPNumeral (double v, FPSort s)
 
FPNum mkFPNumeral (int v, FPSort s)
 
FPNum mkFPNumeral (boolean sgn, int exp, int sig, FPSort s)
 
FPNum mkFPNumeral (boolean sgn, long exp, long sig, FPSort s)
 
FPNum mkFP (float v, FPSort s)
 
FPNum mkFP (double v, FPSort s)
 
FPNum mkFP (int v, FPSort s)
 
FPNum mkFP (boolean sgn, int exp, int sig, FPSort s)
 
FPNum mkFP (boolean sgn, long exp, long sig, FPSort s)
 
FPExpr mkFPAbs (FPExpr t)
 
FPExpr mkFPNeg (FPExpr t)
 
FPExpr mkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
 
FPExpr mkFPSqrt (FPRMExpr rm, FPExpr t)
 
FPExpr mkFPRem (FPExpr t1, FPExpr t2)
 
FPExpr mkFPRoundToIntegral (FPRMExpr rm, FPExpr t)
 
FPExpr mkFPMin (FPExpr t1, FPExpr t2)
 
FPExpr mkFPMax (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPLEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPLt (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPGEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPGt (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPIsNormal (FPExpr t)
 
BoolExpr mkFPIsSubnormal (FPExpr t)
 
BoolExpr mkFPIsZero (FPExpr t)
 
BoolExpr mkFPIsInfinite (FPExpr t)
 
BoolExpr mkFPIsNaN (FPExpr t)
 
BoolExpr mkFPIsNegative (FPExpr t)
 
BoolExpr mkFPIsPositive (FPExpr t)
 
FPExpr mkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
 
FPExpr mkFPToFP (BitVecExpr bv, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, FPExpr t, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, RealExpr t, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
 
FPExpr mkFPToFP (FPSort s, FPRMExpr rm, FPExpr t)
 
BitVecExpr mkFPToBV (FPRMExpr rm, FPExpr t, int sz, boolean signed)
 
RealExpr mkFPToReal (FPExpr t)
 
BitVecExpr mkFPToIEEEBV (FPExpr t)
 
BitVecExpr mkFPToFP (FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
 
AST wrapAST (long nativeObject)
 
long unwrapAST (AST a)
 
String SimplifyHelp ()
 
ParamDescrs getSimplifyParameterDescriptions ()
 
void updateParamValue (String id, String value)
 
IDecRefQueue getASTDRQ ()
 
IDecRefQueue getASTMapDRQ ()
 
IDecRefQueue getASTVectorDRQ ()
 
IDecRefQueue getApplyResultDRQ ()
 
IDecRefQueue getFuncEntryDRQ ()
 
IDecRefQueue getFuncInterpDRQ ()
 
IDecRefQueue getGoalDRQ ()
 
IDecRefQueue getModelDRQ ()
 
IDecRefQueue getParamsDRQ ()
 
IDecRefQueue getParamDescrsDRQ ()
 
IDecRefQueue getProbeDRQ ()
 
IDecRefQueue getSolverDRQ ()
 
IDecRefQueue getStatisticsDRQ ()
 
IDecRefQueue getTacticDRQ ()
 
IDecRefQueue getFixedpointDRQ ()
 
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

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 ( )
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)
inline

Constructor. Remarks: The following parameters can be set:

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

Definition at line 56 of file Context.java.

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

Member Function Documentation

Probe and ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to "true" when the value

p1

and

p2

evaluate to "true".

Definition at line 2694 of file Context.java.

2695  {
2696  checkContextMatch(p1);
2697  checkContextMatch(p2);
2698  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
2699  p2.getNativeObject()));
2700  }
Tactic andThen ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
)
inline

Create a tactic that applies

t1

to a Goal and then

t2"/> to every subgoal produced by <paramref name="t1

.

Definition at line 2391 of file Context.java.

Referenced by Context.then().

2393  {
2394  checkContextMatch(t1);
2395  checkContextMatch(t2);
2396  checkContextMatch(ts);
2397 
2398  long last = 0;
2399  if (ts != null && ts.length > 0)
2400  {
2401  last = ts[ts.length - 1].getNativeObject();
2402  for (int i = ts.length - 2; i >= 0; i--)
2403  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2404  last);
2405  }
2406  if (last != 0)
2407  {
2408  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2409  return new Tactic(this, Native.tacticAndThen(nCtx(),
2410  t1.getNativeObject(), last));
2411  } else
2412  return new Tactic(this, Native.tacticAndThen(nCtx(),
2413  t1.getNativeObject(), t2.getNativeObject()));
2414  }
String benchmarkToSMTString ( String  name,
String  logic,
String  status,
String  attributes,
BoolExpr[]  assumptions,
BoolExpr  formula 
)
inline

Convert a benchmark into an SMT-LIB formatted string.

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

Definition at line 2131 of file Context.java.

2134  {
2135 
2136  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2137  attributes, (int) assumptions.length,
2138  AST.arrayToNative(assumptions), formula.getNativeObject());
2139  }
Tactic cond ( Probe  p,
Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that applies

t1

to a given goal if the probe

p"/> evaluates to true and <paramref name="t2

otherwise.

Definition at line 2472 of file Context.java.

2473  {
2474  checkContextMatch(p);
2475  checkContextMatch(t1);
2476  checkContextMatch(t2);
2477  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2478  t1.getNativeObject(), t2.getNativeObject()));
2479  }
Probe constProbe ( double  val)
inline

Create a probe that always evaluates to

val

.

Definition at line 2624 of file Context.java.

2625  {
2626  return new Probe(this, Native.probeConst(nCtx(), val));
2627  }
void dispose ( )
inline

Disposes of the context.

Definition at line 3768 of file Context.java.

Referenced by Context.finalize().

3769  {
3770  m_AST_DRQ.clear(this);
3771  m_ASTMap_DRQ.clear(this);
3772  m_ASTVector_DRQ.clear(this);
3773  m_ApplyResult_DRQ.clear(this);
3774  m_FuncEntry_DRQ.clear(this);
3775  m_FuncInterp_DRQ.clear(this);
3776  m_Goal_DRQ.clear(this);
3777  m_Model_DRQ.clear(this);
3778  m_Params_DRQ.clear(this);
3779  m_Probe_DRQ.clear(this);
3780  m_Solver_DRQ.clear(this);
3781  m_Statistics_DRQ.clear(this);
3782  m_Tactic_DRQ.clear(this);
3783  m_Fixedpoint_DRQ.clear(this);
3784 
3785  m_boolSort = null;
3786  m_intSort = null;
3787  m_realSort = null;
3788  }
Probe eq ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to "true" when the value returned by

p1

is equal to the value returned by

p2

Definition at line 2683 of file Context.java.

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

2684  {
2685  checkContextMatch(p1);
2686  checkContextMatch(p2);
2687  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2688  p2.getNativeObject()));
2689  }
Tactic fail ( )
inline

Create a tactic always fails.

Definition at line 2503 of file Context.java.

2504  {
2505  return new Tactic(this, Native.tacticFail(nCtx()));
2506  }
Tactic failIf ( Probe  p)
inline

Create a tactic that fails if the probe

p

evaluates to false.

Definition at line 2512 of file Context.java.

2513  {
2514  checkContextMatch(p);
2515  return new Tactic(this,
2516  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2517  }
Tactic failIfNotDecided ( )
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 2523 of file Context.java.

2524  {
2525  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2526  }
void finalize ( )
inlineprotected

Finalizer.

Definition at line 3745 of file Context.java.

3746  {
3747  dispose();
3748 
3749  if (m_refCount == 0)
3750  {
3751  try
3752  {
3753  Native.delContext(m_ctx);
3754  } catch (Z3Exception e)
3755  {
3756  // OK.
3757  }
3758  m_ctx = 0;
3759  }
3760  /*
3761  else
3762  CMW: re-queue the finalizer? */
3763  }
Probe ge ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to "true" when the value returned by

p1

is greater than or equal the value returned by

p2

Definition at line 2671 of file Context.java.

2672  {
2673  checkContextMatch(p1);
2674  checkContextMatch(p2);
2675  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2676  p2.getNativeObject()));
2677  }
IDecRefQueue getApplyResultDRQ ( )
inline

Definition at line 3680 of file Context.java.

3681  {
3682  return m_ApplyResult_DRQ;
3683  }
IDecRefQueue getASTDRQ ( )
inline

Definition at line 3665 of file Context.java.

3666  {
3667  return m_AST_DRQ;
3668  }
IDecRefQueue getASTMapDRQ ( )
inline

Definition at line 3670 of file Context.java.

3671  {
3672  return m_ASTMap_DRQ;
3673  }
IDecRefQueue getASTVectorDRQ ( )
inline

Definition at line 3675 of file Context.java.

3676  {
3677  return m_ASTVector_DRQ;
3678  }
BoolSort getBoolSort ( )
inline

Retrieves the Boolean sort of the context.

Definition at line 105 of file Context.java.

Referenced by Context.mkBoolConst().

106  {
107  if (m_boolSort == null)
108  m_boolSort = new BoolSort(this);
109  return m_boolSort;
110  }
def BoolSort
Definition: z3py.py:1336
IDecRefQueue getFixedpointDRQ ( )
inline

Definition at line 3735 of file Context.java.

3736  {
3737  return m_Fixedpoint_DRQ;
3738  }
IDecRefQueue getFuncEntryDRQ ( )
inline

Definition at line 3685 of file Context.java.

3686  {
3687  return m_FuncEntry_DRQ;
3688  }
IDecRefQueue getFuncInterpDRQ ( )
inline

Definition at line 3690 of file Context.java.

3691  {
3692  return m_FuncInterp_DRQ;
3693  }
IDecRefQueue getGoalDRQ ( )
inline

Definition at line 3695 of file Context.java.

3696  {
3697  return m_Goal_DRQ;
3698  }
IntSort getIntSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 115 of file Context.java.

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

116  {
117  if (m_intSort == null)
118  m_intSort = new IntSort(this);
119  return m_intSort;
120  }
def IntSort
Definition: z3py.py:2625
IDecRefQueue getModelDRQ ( )
inline

Definition at line 3700 of file Context.java.

3701  {
3702  return m_Model_DRQ;
3703  }
int getNumProbes ( )
inline

The number of supported Probes.

Definition at line 2586 of file Context.java.

Referenced by Context.getProbeNames().

2587  {
2588  return Native.getNumProbes(nCtx());
2589  }
int getNumSMTLIBAssumptions ( )
inline

The number of SMTLIB assumptions parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2213 of file Context.java.

Referenced by Context.getSMTLIBAssumptions().

2214  {
2215  return Native.getSmtlibNumAssumptions(nCtx());
2216  }
int getNumSMTLIBDecls ( )
inline

The number of SMTLIB declarations parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2237 of file Context.java.

Referenced by Context.getSMTLIBDecls().

2238  {
2239  return Native.getSmtlibNumDecls(nCtx());
2240  }
int getNumSMTLIBFormulas ( )
inline

The number of SMTLIB formulas parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2189 of file Context.java.

Referenced by Context.getSMTLIBFormulas().

2190  {
2191  return Native.getSmtlibNumFormulas(nCtx());
2192  }
int getNumSMTLIBSorts ( )
inline

The number of SMTLIB sorts parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2260 of file Context.java.

Referenced by Context.getSMTLIBSorts().

2261  {
2262  return Native.getSmtlibNumSorts(nCtx());
2263  }
int getNumTactics ( )
inline

The number of supported tactics.

Definition at line 2352 of file Context.java.

Referenced by Context.getTacticNames().

2353  {
2354  return Native.getNumTactics(nCtx());
2355  }
IDecRefQueue getParamDescrsDRQ ( )
inline

Definition at line 3710 of file Context.java.

3711  {
3712  return m_ParamDescrs_DRQ;
3713  }
IDecRefQueue getParamsDRQ ( )
inline

Definition at line 3705 of file Context.java.

3706  {
3707  return m_Params_DRQ;
3708  }
String getProbeDescription ( String  name)
inline

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

Definition at line 2608 of file Context.java.

2609  {
2610  return Native.probeGetDescr(nCtx(), name);
2611  }
IDecRefQueue getProbeDRQ ( )
inline

Definition at line 3715 of file Context.java.

3716  {
3717  return m_Probe_DRQ;
3718  }
String [] getProbeNames ( )
inline

The names of all supported Probes.

Definition at line 2594 of file Context.java.

2595  {
2596 
2597  int n = getNumProbes();
2598  String[] res = new String[n];
2599  for (int i = 0; i < n; i++)
2600  res[i] = Native.getProbeName(nCtx(), i);
2601  return res;
2602  }
RealSort getRealSort ( )
inline

Retrieves the Real sort of the context.

Definition at line 125 of file Context.java.

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

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

Retrieves parameter descriptions for simplifier.

Definition at line 3605 of file Context.java.

3606  {
3607  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3608  }
BoolExpr [] getSMTLIBAssumptions ( )
inline

The assumptions parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2222 of file Context.java.

2223  {
2224 
2225  int n = getNumSMTLIBAssumptions();
2226  BoolExpr[] res = new BoolExpr[n];
2227  for (int i = 0; i < n; i++)
2228  res[i] = (BoolExpr) Expr.create(this,
2229  Native.getSmtlibAssumption(nCtx(), i));
2230  return res;
2231  }
FuncDecl [] getSMTLIBDecls ( )
inline

The declarations parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2246 of file Context.java.

2247  {
2248 
2249  int n = getNumSMTLIBDecls();
2250  FuncDecl[] res = new FuncDecl[n];
2251  for (int i = 0; i < n; i++)
2252  res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
2253  return res;
2254  }
BoolExpr [] getSMTLIBFormulas ( )
inline

The formulas parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2198 of file Context.java.

2199  {
2200 
2201  int n = getNumSMTLIBFormulas();
2202  BoolExpr[] res = new BoolExpr[n];
2203  for (int i = 0; i < n; i++)
2204  res[i] = (BoolExpr) Expr.create(this,
2205  Native.getSmtlibFormula(nCtx(), i));
2206  return res;
2207  }
Sort [] getSMTLIBSorts ( )
inline

The declarations parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2269 of file Context.java.

2270  {
2271 
2272  int n = getNumSMTLIBSorts();
2273  Sort[] res = new Sort[n];
2274  for (int i = 0; i < n; i++)
2275  res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
2276  return res;
2277  }
IDecRefQueue getSolverDRQ ( )
inline

Definition at line 3720 of file Context.java.

3721  {
3722  return m_Solver_DRQ;
3723  }
IDecRefQueue getStatisticsDRQ ( )
inline

Definition at line 3725 of file Context.java.

3726  {
3727  return m_Statistics_DRQ;
3728  }
String getTacticDescription ( String  name)
inline

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

Definition at line 2374 of file Context.java.

2375  {
2376  return Native.tacticGetDescr(nCtx(), name);
2377  }
IDecRefQueue getTacticDRQ ( )
inline

Definition at line 3730 of file Context.java.

3731  {
3732  return m_Tactic_DRQ;
3733  }
String [] getTacticNames ( )
inline

The names of all supported tactics.

Definition at line 2360 of file Context.java.

2361  {
2362 
2363  int n = getNumTactics();
2364  String[] res = new String[n];
2365  for (int i = 0; i < n; i++)
2366  res[i] = Native.getTacticName(nCtx(), i);
2367  return res;
2368  }
Probe gt ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to "true" when the value returned by

p1

is greater than the value returned by

p2

Definition at line 2645 of file Context.java.

2646  {
2647  checkContextMatch(p1);
2648  checkContextMatch(p2);
2649  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2650  p2.getNativeObject()));
2651  }
void interrupt ( )
inline

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

Definition at line 2578 of file Context.java.

2579  {
2580  Native.interrupt(nCtx());
2581  }
Probe le ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to "true" when the value returned by

p1

is less than or equal the value returned by

p2

Definition at line 2658 of file Context.java.

2659  {
2660  checkContextMatch(p1);
2661  checkContextMatch(p2);
2662  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2663  p2.getNativeObject()));
2664  }
Probe lt ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to "true" when the value returned by

p1

is less than the value returned by

p2

Definition at line 2633 of file Context.java.

2634  {
2635  checkContextMatch(p1);
2636  checkContextMatch(p2);
2637  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2638  p2.getNativeObject()));
2639  }
ArithExpr mkAdd ( ArithExpr...  t)
inline

Create an expression representing

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

.

Definition at line 726 of file Context.java.

727  {
728  checkContextMatch(t);
729  return (ArithExpr) Expr.create(this,
730  Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t)));
731  }
BoolExpr mkAnd ( BoolExpr...  t)
inline

Create an expression representing

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

.

Definition at line 706 of file Context.java.

707  {
708  checkContextMatch(t);
709  return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length,
710  AST.arrayToNative(t)));
711  }
Expr mkApp ( FuncDecl  f,
Expr...  args 
)
inline

Create a new function application.

Definition at line 593 of file Context.java.

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

594  {
595  checkContextMatch(f);
596  checkContextMatch(args);
597  return Expr.create(this, f, args);
598  }
ArrayExpr mkArrayConst ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1584 of file Context.java.

1586  {
1587  return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1588  }
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:184
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
ArrayExpr mkArrayConst ( String  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1593 of file Context.java.

1595  {
1596  return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1597  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:184
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
ArraySort mkArraySort ( Sort  domain,
Sort  range 
)
inline

Create a new array sort.

Definition at line 184 of file Context.java.

Referenced by Context.mkArrayConst().

185  {
186  checkContextMatch(domain);
187  checkContextMatch(range);
188  return new ArraySort(this, domain, range);
189  }
def ArraySort(d, r)
Definition: z3py.py:3978
BitVecSort mkBitVecSort ( int  size)
inline

Create a new bit-vector sort.

Definition at line 176 of file Context.java.

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

177  {
178  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
179  }
def BitVecSort
Definition: z3py.py:3446
BoolExpr mkBool ( boolean  value)
inline

Creates a Boolean value.

Definition at line 619 of file Context.java.

620  {
621  return value ? mkTrue() : mkFalse();
622  }
BoolExpr mkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 529 of file Context.java.

530  {
531  return (BoolExpr) mkConst(name, getBoolSort());
532  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
BoolExpr mkBoolConst ( String  name)
inline

Create a Boolean constant.

Definition at line 537 of file Context.java.

538  {
539  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
540  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
BoolSort mkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 135 of file Context.java.

136  {
137  return new BoolSort(this);
138  }
def BoolSort
Definition: z3py.py:1336
Expr mkBound ( int  index,
Sort  ty 
)
inline

Creates a new bound variable.

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

Definition at line 463 of file Context.java.

464  {
465  return Expr.create(this,
466  Native.mkBound(nCtx(), index, ty.getNativeObject()));
467  }
BitVecNum mkBV ( String  v,
int  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 1976 of file Context.java.

1977  {
1978  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
1979  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1838
BitVecSort mkBitVecSort(int size)
Definition: Context.java:176
BitVecNum mkBV ( int  v,
int  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 1986 of file Context.java.

1987  {
1988  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
1989  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1838
BitVecSort mkBitVecSort(int size)
Definition: Context.java:176
BitVecNum mkBV ( long  v,
int  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 1996 of file Context.java.

1997  {
1998  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
1999  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1838
BitVecSort mkBitVecSort(int size)
Definition: Context.java:176
IntExpr mkBV2Int ( BitVecExpr  t,
boolean  signed 
)
inline

Create an integer from the bit-vector argument

t

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

[0..2^N-1]

, where N are the number of bits in

t

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

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

The argument must be of bit-vector sort.

Definition at line 1461 of file Context.java.

1462  {
1463  checkContextMatch(t);
1464  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1465  (signed) ? true : false));
1466  }
BitVecExpr mkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1024 of file Context.java.

1025  {
1026  checkContextMatch(t1);
1027  checkContextMatch(t2);
1028  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1029  t1.getNativeObject(), t2.getNativeObject()));
1030  }
BoolExpr mkBVAddNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
)
inline

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

Definition at line 1473 of file Context.java.

1475  {
1476  checkContextMatch(t1);
1477  checkContextMatch(t2);
1478  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1479  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1480  : false));
1481  }
BoolExpr mkBVAddNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1488 of file Context.java.

1490  {
1491  checkContextMatch(t1);
1492  checkContextMatch(t2);
1493  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1494  t1.getNativeObject(), t2.getNativeObject()));
1495  }
BitVecExpr mkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 935 of file Context.java.

936  {
937  checkContextMatch(t1);
938  checkContextMatch(t2);
939  return new BitVecExpr(this, Native.mkBvand(nCtx(),
940  t1.getNativeObject(), t2.getNativeObject()));
941  }
BitVecExpr mkBVASHR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

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

The arguments must have a bit-vector sort.

Definition at line 1369 of file Context.java.

1370  {
1371  checkContextMatch(t1);
1372  checkContextMatch(t2);
1373  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1374  t1.getNativeObject(), t2.getNativeObject()));
1375  }
BitVecExpr mkBVConst ( Symbol  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 577 of file Context.java.

578  {
579  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
580  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:176
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
BitVecExpr mkBVConst ( String  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 585 of file Context.java.

586  {
587  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
588  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:176
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
BitVecExpr mkBVLSHR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

2^x

where x is the value of

t2

.

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

The arguments must have a bit-vector sort.

Definition at line 1349 of file Context.java.

1350  {
1351  checkContextMatch(t1);
1352  checkContextMatch(t2);
1353  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1354  t1.getNativeObject(), t2.getNativeObject()));
1355  }
BitVecExpr mkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1050 of file Context.java.

1051  {
1052  checkContextMatch(t1);
1053  checkContextMatch(t2);
1054  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1055  t1.getNativeObject(), t2.getNativeObject()));
1056  }
BoolExpr mkBVMulNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
)
inline

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

Definition at line 1557 of file Context.java.

1559  {
1560  checkContextMatch(t1);
1561  checkContextMatch(t2);
1562  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1563  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1564  : false));
1565  }
BoolExpr mkBVMulNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1572 of file Context.java.

1574  {
1575  checkContextMatch(t1);
1576  checkContextMatch(t2);
1577  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1578  t1.getNativeObject(), t2.getNativeObject()));
1579  }
BitVecExpr mkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 974 of file Context.java.

975  {
976  checkContextMatch(t1);
977  checkContextMatch(t2);
978  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
979  t1.getNativeObject(), t2.getNativeObject()));
980  }
BitVecExpr mkBVNeg ( BitVecExpr  t)
inline

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

Definition at line 1013 of file Context.java.

1014  {
1015  checkContextMatch(t);
1016  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1017  }
BoolExpr mkBVNegNoOverflow ( BitVecExpr  t)
inline

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

Definition at line 1545 of file Context.java.

1546  {
1547  checkContextMatch(t);
1548  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1549  t.getNativeObject()));
1550  }
BitVecExpr mkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 987 of file Context.java.

988  {
989  checkContextMatch(t1);
990  checkContextMatch(t2);
991  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
992  t1.getNativeObject(), t2.getNativeObject()));
993  }
BitVecExpr mkBVNot ( BitVecExpr  t)
inline

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

Definition at line 900 of file Context.java.

901  {
902  checkContextMatch(t);
903  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
904  }
BitVecExpr mkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 948 of file Context.java.

949  {
950  checkContextMatch(t1);
951  checkContextMatch(t2);
952  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
953  t2.getNativeObject()));
954  }
BitVecExpr mkBVRedAND ( BitVecExpr  t)
inline

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

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

Definition at line 911 of file Context.java.

912  {
913  checkContextMatch(t);
914  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
915  t.getNativeObject()));
916  }
BitVecExpr mkBVRedOR ( BitVecExpr  t)
inline

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

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

Definition at line 923 of file Context.java.

924  {
925  checkContextMatch(t);
926  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
927  t.getNativeObject()));
928  }
BitVecExpr mkBVRotateLeft ( int  i,
BitVecExpr  t 
)
inline

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

t

must have a bit-vector sort.

Definition at line 1382 of file Context.java.

1383  {
1384  checkContextMatch(t);
1385  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1386  t.getNativeObject()));
1387  }
BitVecExpr mkBVRotateLeft ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Rotate Left. Remarks: Rotate bits of

t1

to the left

t2

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

Definition at line 1407 of file Context.java.

1409  {
1410  checkContextMatch(t1);
1411  checkContextMatch(t2);
1412  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1413  t1.getNativeObject(), t2.getNativeObject()));
1414  }
BitVecExpr mkBVRotateRight ( int  i,
BitVecExpr  t 
)
inline

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

t

must have a bit-vector sort.

Definition at line 1394 of file Context.java.

1395  {
1396  checkContextMatch(t);
1397  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1398  t.getNativeObject()));
1399  }
BitVecExpr mkBVRotateRight ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Rotate Right. Remarks: Rotate bits of

t1

to the right

t2

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

Definition at line 1422 of file Context.java.

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

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

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

If

t2

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

Definition at line 1086 of file Context.java.

1087  {
1088  checkContextMatch(t1);
1089  checkContextMatch(t2);
1090  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1091  t1.getNativeObject(), t2.getNativeObject()));
1092  }
BoolExpr mkBVSDivNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1531 of file Context.java.

1533  {
1534  checkContextMatch(t1);
1535  checkContextMatch(t2);
1536  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1537  t1.getNativeObject(), t2.getNativeObject()));
1538  }
BoolExpr mkBVSGE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1211 of file Context.java.

1212  {
1213  checkContextMatch(t1);
1214  checkContextMatch(t2);
1215  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1216  t2.getNativeObject()));
1217  }
BoolExpr mkBVSGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1237 of file Context.java.

1238  {
1239  checkContextMatch(t1);
1240  checkContextMatch(t2);
1241  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1242  t2.getNativeObject()));
1243  }
BitVecExpr mkBVSHL ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Shift left. Remarks: It is equivalent to multiplication by

2^x

where x is the value of

t2

.

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

The arguments must have a bit-vector sort.

Definition at line 1330 of file Context.java.

1331  {
1332  checkContextMatch(t1);
1333  checkContextMatch(t2);
1334  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1335  t1.getNativeObject(), t2.getNativeObject()));
1336  }
BoolExpr mkBVSLE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1185 of file Context.java.

1186  {
1187  checkContextMatch(t1);
1188  checkContextMatch(t2);
1189  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1190  t2.getNativeObject()));
1191  }
BoolExpr mkBVSLT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1159 of file Context.java.

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

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

t2

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

Definition at line 1133 of file Context.java.

1134  {
1135  checkContextMatch(t1);
1136  checkContextMatch(t2);
1137  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1138  t1.getNativeObject(), t2.getNativeObject()));
1139  }
BitVecExpr mkBVSRem ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Signed remainder. Remarks: It is defined as

t1 - (t1 /s t2) * t2

, where

/s

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

If

t2

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

Definition at line 1119 of file Context.java.

1120  {
1121  checkContextMatch(t1);
1122  checkContextMatch(t2);
1123  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1124  t1.getNativeObject(), t2.getNativeObject()));
1125  }
BitVecExpr mkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1037 of file Context.java.

1038  {
1039  checkContextMatch(t1);
1040  checkContextMatch(t2);
1041  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1042  t1.getNativeObject(), t2.getNativeObject()));
1043  }
BoolExpr mkBVSubNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1502 of file Context.java.

1504  {
1505  checkContextMatch(t1);
1506  checkContextMatch(t2);
1507  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1508  t1.getNativeObject(), t2.getNativeObject()));
1509  }
BoolExpr mkBVSubNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
)
inline

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

Definition at line 1516 of file Context.java.

1518  {
1519  checkContextMatch(t1);
1520  checkContextMatch(t2);
1521  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1522  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1523  : false));
1524  }
BitVecExpr mkBVUDiv ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

t1/t2

if t2 is different from zero. If

t2

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

Definition at line 1065 of file Context.java.

1066  {
1067  checkContextMatch(t1);
1068  checkContextMatch(t2);
1069  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1070  t1.getNativeObject(), t2.getNativeObject()));
1071  }
BoolExpr mkBVUGE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1198 of file Context.java.

1199  {
1200  checkContextMatch(t1);
1201  checkContextMatch(t2);
1202  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1203  t2.getNativeObject()));
1204  }
BoolExpr mkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1224 of file Context.java.

1225  {
1226  checkContextMatch(t1);
1227  checkContextMatch(t2);
1228  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1229  t2.getNativeObject()));
1230  }
BoolExpr mkBVULE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1172 of file Context.java.

1173  {
1174  checkContextMatch(t1);
1175  checkContextMatch(t2);
1176  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1177  t2.getNativeObject()));
1178  }
BoolExpr mkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1146 of file Context.java.

1147  {
1148  checkContextMatch(t1);
1149  checkContextMatch(t2);
1150  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1151  t2.getNativeObject()));
1152  }
BitVecExpr mkBVURem ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned remainder. Remarks: It is defined as

t1 - (t1 /u t2) * t2

, where

/u

represents unsigned division. If

t2

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

Definition at line 1101 of file Context.java.

1102  {
1103  checkContextMatch(t1);
1104  checkContextMatch(t2);
1105  return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1106  t1.getNativeObject(), t2.getNativeObject()));
1107  }
BitVecExpr mkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1000 of file Context.java.

1001  {
1002  checkContextMatch(t1);
1003  checkContextMatch(t2);
1004  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1005  t1.getNativeObject(), t2.getNativeObject()));
1006  }
BitVecExpr mkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 961 of file Context.java.

962  {
963  checkContextMatch(t1);
964  checkContextMatch(t2);
965  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
966  t1.getNativeObject(), t2.getNativeObject()));
967  }
BitVecExpr mkConcat ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

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

Definition at line 1255 of file Context.java.

1256  {
1257  checkContextMatch(t1);
1258  checkContextMatch(t2);
1259  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1260  t1.getNativeObject(), t2.getNativeObject()));
1261  }
Expr mkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort

range

and named

name

.

Definition at line 486 of file Context.java.

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

487  {
488  checkContextMatch(name);
489  checkContextMatch(range);
490 
491  return Expr.create(
492  this,
493  Native.mkConst(nCtx(), name.getNativeObject(),
494  range.getNativeObject()));
495  }
Expr mkConst ( String  name,
Sort  range 
)
inline

Creates a new Constant of sort

range

and named

name

.

Definition at line 501 of file Context.java.

502  {
503  return mkConst(mkSymbol(name), range);
504  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
Expr mkConst ( FuncDecl  f)
inline

Creates a fresh constant from the FuncDecl

f

.

Parameters
fA decl of a 0-arity function

Definition at line 521 of file Context.java.

522  {
523  return mkApp(f, (Expr[]) null);
524  }
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:593
ArrayExpr mkConstArray ( Sort  domain,
Expr  v 
)
inline

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

on an arbitrary index produces the value

v

.

See also
mkArraySort
mkSelect

Definition at line 1656 of file Context.java.

1657  {
1658  checkContextMatch(domain);
1659  checkContextMatch(v);
1660  return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1661  domain.getNativeObject(), v.getNativeObject()));
1662  }
FuncDecl mkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 429 of file Context.java.

430  {
431  checkContextMatch(name);
432  checkContextMatch(range);
433  return new FuncDecl(this, name, null, range);
434  }
FuncDecl mkConstDecl ( String  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 439 of file Context.java.

440  {
441  checkContextMatch(range);
442  return new FuncDecl(this, mkSymbol(name), null, range);
443  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
Constructor mkConstructor ( Symbol  name,
Symbol  recognizer,
Symbol[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
)
inline

Create a datatype constructor.

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

Definition at line 273 of file Context.java.

276  {
277 
278  return new Constructor(this, name, recognizer, fieldNames, sorts,
279  sortRefs);
280  }
Constructor mkConstructor ( String  name,
String  recognizer,
String[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
)
inline

Create a datatype constructor.

Parameters
name
recognizer
fieldNames
sorts
sortRefs
Returns

Definition at line 292 of file Context.java.

295  {
296 
297  return new Constructor(this, mkSymbol(name), mkSymbol(recognizer),
298  mkSymbols(fieldNames), sorts, sortRefs);
299  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
DatatypeSort mkDatatypeSort ( Symbol  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 304 of file Context.java.

306  {
307  checkContextMatch(name);
308  checkContextMatch(constructors);
309  return new DatatypeSort(this, name, constructors);
310  }
DatatypeSort mkDatatypeSort ( String  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 315 of file Context.java.

317  {
318  checkContextMatch(constructors);
319  return new DatatypeSort(this, mkSymbol(name), constructors);
320  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
DatatypeSort [] mkDatatypeSorts ( Symbol[]  names,
Constructor  c[][] 
)
inline

Create mutually recursive datatypes.

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

Definition at line 327 of file Context.java.

Referenced by Context.mkDatatypeSorts().

329  {
330  checkContextMatch(names);
331  int n = (int) names.length;
332  ConstructorList[] cla = new ConstructorList[n];
333  long[] n_constr = new long[n];
334  for (int i = 0; i < n; i++)
335  {
336  Constructor[] constructor = c[i];
337 
338  checkContextMatch(constructor);
339  cla[i] = new ConstructorList(this, constructor);
340  n_constr[i] = cla[i].getNativeObject();
341  }
342  long[] n_res = new long[n];
343  Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
344  n_constr);
345  DatatypeSort[] res = new DatatypeSort[n];
346  for (int i = 0; i < n; i++)
347  res[i] = new DatatypeSort(this, n_res[i]);
348  return res;
349  }
DatatypeSort [] mkDatatypeSorts ( String[]  names,
Constructor  c[][] 
)
inline

Create mutually recursive data-types.

Parameters
names
c
Returns

Definition at line 358 of file Context.java.

360  {
361  return mkDatatypeSorts(mkSymbols(names), c);
362  }
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:327
BoolExpr mkDistinct ( Expr...  args)
inline

Creates a

term.

Definition at line 638 of file Context.java.

639  {
640  checkContextMatch(args);
641  return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length,
642  AST.arrayToNative(args)));
643  }
ArithExpr mkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 / t2

.

Definition at line 766 of file Context.java.

767  {
768  checkContextMatch(t1);
769  checkContextMatch(t2);
770  return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
771  t1.getNativeObject(), t2.getNativeObject()));
772  }
Expr mkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 1711 of file Context.java.

1712  {
1713  checkContextMatch(domain);
1714  return Expr.create(this,
1715  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1716  }
EnumSort mkEnumSort ( Symbol  name,
Symbol...  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 207 of file Context.java.

209  {
210  checkContextMatch(name);
211  checkContextMatch(enumNames);
212  return new EnumSort(this, name, enumNames);
213  }
def EnumSort
Definition: z3py.py:4421
EnumSort mkEnumSort ( String  name,
String...  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 218 of file Context.java.

220  {
221  return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
222  }
def EnumSort
Definition: z3py.py:4421
IntSymbol mkSymbol(int i)
Definition: Context.java:72
BoolExpr mkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality

x"/> = <paramref name="y

.

Definition at line 627 of file Context.java.

628  {
629  checkContextMatch(x);
630  checkContextMatch(y);
631  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
632  y.getNativeObject()));
633  }
Quantifier mkExists ( Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create an existential Quantifier.

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

Definition at line 2045 of file Context.java.

Referenced by Context.mkQuantifier().

2048  {
2049 
2050  return new Quantifier(this, false, sorts, names, body, weight,
2051  patterns, noPatterns, quantifierID, skolemID);
2052  }
Quantifier mkExists ( Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create an existential Quantifier.

Definition at line 2057 of file Context.java.

2060  {
2061 
2062  return new Quantifier(this, false, boundConstants, body, weight,
2063  patterns, noPatterns, quantifierID, skolemID);
2064  }
BitVecExpr mkExtract ( int  high,
int  low,
BitVecExpr  t 
)
inline

Bit-vector extraction. Remarks: Extract the bits

high

down to

low

from a bitvector of size

m

to yield a new bitvector of size

n

, where

n = high - low + 1

. The argument

t

must have a bit-vector sort.

Definition at line 1271 of file Context.java.

1273  {
1274  checkContextMatch(t);
1275  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1276  t.getNativeObject()));
1277  }
BoolExpr mkFalse ( )
inline

The false Term.

Definition at line 611 of file Context.java.

Referenced by Context.mkBool().

612  {
613  return new BoolExpr(this, Native.mkFalse(nCtx()));
614  }
FiniteDomainSort mkFiniteDomainSort ( Symbol  name,
long  size 
)
inline

Create a new finite domain sort.

Definition at line 246 of file Context.java.

248  {
249  checkContextMatch(name);
250  return new FiniteDomainSort(this, name, size);
251  }
FiniteDomainSort mkFiniteDomainSort ( String  name,
long  size 
)
inline

Create a new finite domain sort.

Definition at line 256 of file Context.java.

258  {
259  return new FiniteDomainSort(this, mkSymbol(name), size);
260  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
Fixedpoint mkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 2784 of file Context.java.

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

Create a universal Quantifier.

Parameters
sortsthe sorts of the bound variables.
namesnames of the bound variables
bodythe body of the quantifier.
weightquantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
patternsarray containing the patterns created using
MkPattern
.
noPatternsarray containing the anti-patterns created using
MkPattern
.
quantifierIDoptional symbol to track quantifier.
skolemIDoptional symbol to track skolem constants.

Remarks: Creates a forall formula, where

weight"/> is the weight, <paramref name="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.

Definition at line 2020 of file Context.java.

Referenced by Context.mkQuantifier().

2023  {
2024 
2025  return new Quantifier(this, true, sorts, names, body, weight, patterns,
2026  noPatterns, quantifierID, skolemID);
2027  }
Quantifier mkForall ( Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a universal Quantifier.

Definition at line 2032 of file Context.java.

2035  {
2036 
2037  return new Quantifier(this, true, boundConstants, body, weight,
2038  patterns, noPatterns, quantifierID, skolemID);
2039  }
FPNum mkFP ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3070 of file Context.java.

3071  {
3072  return mkFPNumeral(v, s);
3073  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3011
FPNum mkFP ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3081 of file Context.java.

3082  {
3083  return mkFPNumeral(v, s);
3084  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3011
FPNum mkFP ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3093 of file Context.java.

3094  {
3095  return mkFPNumeral(v, s);
3096  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3011
FPNum mkFP ( boolean  sgn,
int  exp,
int  sig,
FPSort  s 
)
inline

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

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

Definition at line 3106 of file Context.java.

3107  {
3108  return mkFPNumeral(sgn, sig, exp, s);
3109  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3011
FPNum mkFP ( boolean  sgn,
long  exp,
long  sig,
FPSort  s 
)
inline

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

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

Definition at line 3119 of file Context.java.

3120  {
3121  return mkFPNumeral(sgn, sig, exp, s);
3122  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3011
FPExpr mkFP ( BitVecExpr  sgn,
BitVecExpr  sig,
BitVecExpr  exp 
)
inline

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

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

Definition at line 3404 of file Context.java.

3405  {
3406  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3407  }
FPExpr mkFPAbs ( FPExpr  t)
inline

Floating-point absolute value

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3130 of file Context.java.

3131  {
3132  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3133  }
FPExpr mkFPAdd ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point addition

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

Definition at line 3152 of file Context.java.

3153  {
3154  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3155  }
FPExpr mkFPDiv ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point division

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

Definition at line 3188 of file Context.java.

3189  {
3190  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3191  }
BoolExpr mkFPEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point equality.

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

Definition at line 3316 of file Context.java.

3317  {
3318  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3319  }
FPExpr mkFPFMA ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2,
FPExpr  t3 
)
inline

Floating-point fused multiply-add

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

Definition at line 3203 of file Context.java.

3204  {
3205  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3206  }
BoolExpr mkFPGEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3292 of file Context.java.

3293  {
3294  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3295  }
BoolExpr mkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3303 of file Context.java.

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

Create a floating-point infinity of sort s.

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

Definition at line 2989 of file Context.java.

2990  {
2991  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
2992  }
BoolExpr mkFPIsInfinite ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3356 of file Context.java.

3357  {
3358  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3359  }
BoolExpr mkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3366 of file Context.java.

3367  {
3368  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3369  }
BoolExpr mkFPIsNegative ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3376 of file Context.java.

3377  {
3378  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3379  }
BoolExpr mkFPIsNormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3326 of file Context.java.

3327  {
3328  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3329  }
BoolExpr mkFPIsPositive ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3386 of file Context.java.

3387  {
3388  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3389  }
BoolExpr mkFPIsSubnormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3336 of file Context.java.

3337  {
3338  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3339  }
BoolExpr mkFPIsZero ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3346 of file Context.java.

3347  {
3348  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3349  }
BoolExpr mkFPLEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3270 of file Context.java.

3271  {
3272  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3273  }
BoolExpr mkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3281 of file Context.java.

3282  {
3283  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3284  }
FPExpr mkFPMax ( FPExpr  t1,
FPExpr  t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3259 of file Context.java.

3260  {
3261  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3262  }
FPExpr mkFPMin ( FPExpr  t1,
FPExpr  t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3248 of file Context.java.

3249  {
3250  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3251  }
FPExpr mkFPMul ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point multiplication

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

Definition at line 3176 of file Context.java.

3177  {
3178  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3179  }
FPNum mkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 2978 of file Context.java.

2979  {
2980  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
2981  }
FPExpr mkFPNeg ( FPExpr  t)
inline

Floating-point negation

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3140 of file Context.java.

3141  {
3142  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3143  }
FPNum mkFPNumeral ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3011 of file Context.java.

Referenced by Context.mkFP().

3012  {
3013  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3014  }
FPNum mkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3022 of file Context.java.

3023  {
3024  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3025  }
FPNum mkFPNumeral ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

  • Parameters
    vnumeral value.
    sFloatingPoint sort.
    Exceptions
    Z3Exception

Definition at line 3033 of file Context.java.

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

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

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

Definition at line 3046 of file Context.java.

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

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

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

Definition at line 3059 of file Context.java.

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

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3225 of file Context.java.

3226  {
3227  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3228  }
FPRMNum mkFPRNA ( )
inline

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

Exceptions
Z3Exception

Definition at line 2830 of file Context.java.

2831  {
2832  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
2833  }
FPRMNum mkFPRNE ( )
inline

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

Exceptions
Z3Exception

Definition at line 2812 of file Context.java.

2813  {
2814  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
2815  }
FPRMSort mkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Exceptions
Z3Exception

Definition at line 2794 of file Context.java.

2795  {
2796  return new FPRMSort(this);
2797  }
FPRMNum mkFPRoundNearestTiesToAway ( )
inline

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

Exceptions
Z3Exception

Definition at line 2821 of file Context.java.

2822  {
2823  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
2824  }
FPRMExpr mkFPRoundNearestTiesToEven ( )
inline

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

Exceptions
Z3Exception

Definition at line 2803 of file Context.java.

2804  {
2805  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
2806  }
FPExpr mkFPRoundToIntegral ( FPRMExpr  rm,
FPExpr  t 
)
inline

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

Parameters
rmterm of RoundingMode sort
tfloating-point term
Exceptions
Z3Exception

Definition at line 3237 of file Context.java.

3238  {
3239  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3240  }
FPRMNum mkFPRoundTowardNegative ( )
inline

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

Exceptions
Z3Exception

Definition at line 2857 of file Context.java.

2858  {
2859  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
2860  }
FPRMNum mkFPRoundTowardPositive ( )
inline

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

Exceptions
Z3Exception

Definition at line 2839 of file Context.java.

2840  {
2841  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
2842  }
FPRMNum mkFPRoundTowardZero ( )
inline

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

Exceptions
Z3Exception

Definition at line 2875 of file Context.java.

2876  {
2877  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
2878  }
FPRMNum mkFPRTN ( )
inline

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

Exceptions
Z3Exception

Definition at line 2866 of file Context.java.

2867  {
2868  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
2869  }
FPRMNum mkFPRTP ( )
inline

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

Exceptions
Z3Exception

Definition at line 2848 of file Context.java.

2849  {
2850  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
2851  }
FPRMNum mkFPRTZ ( )
inline

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

Exceptions
Z3Exception

Definition at line 2884 of file Context.java.

2885  {
2886  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
2887  }
FPSort mkFPSort ( int  ebits,
int  sbits 
)
inline

Create a FloatingPoint sort.

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

Definition at line 2895 of file Context.java.

2896  {
2897  return new FPSort(this, ebits, sbits);
2898  }
def FPSort
Definition: z3py.py:7920
FPSort mkFPSort128 ( )
inline

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

Exceptions
Z3Exception

Definition at line 2967 of file Context.java.

2968  {
2969  return new FPSort(this, Native.mkFpaSort128(nCtx()));
2970  }
def FPSort
Definition: z3py.py:7920
FPSort mkFPSort16 ( )
inline

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

Exceptions
Z3Exception

Definition at line 2913 of file Context.java.

2914  {
2915  return new FPSort(this, Native.mkFpaSort16(nCtx()));
2916  }
def FPSort
Definition: z3py.py:7920
FPSort mkFPSort32 ( )
inline

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

Exceptions
Z3Exception

Definition at line 2931 of file Context.java.

2932  {
2933  return new FPSort(this, Native.mkFpaSort32(nCtx()));
2934  }
def FPSort
Definition: z3py.py:7920
FPSort mkFPSort64 ( )
inline

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

Exceptions
Z3Exception

Definition at line 2949 of file Context.java.

2950  {
2951  return new FPSort(this, Native.mkFpaSort64(nCtx()));
2952  }
def FPSort
Definition: z3py.py:7920
FPSort mkFPSortDouble ( )
inline

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

Exceptions
Z3Exception

Definition at line 2940 of file Context.java.

2941  {
2942  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
2943  }
def FPSort
Definition: z3py.py:7920
FPSort mkFPSortHalf ( )
inline

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

Exceptions
Z3Exception

Definition at line 2904 of file Context.java.

2905  {
2906  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
2907  }
def FPSort
Definition: z3py.py:7920
FPSort mkFPSortQuadruple ( )
inline

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

Exceptions
Z3Exception

Definition at line 2958 of file Context.java.

2959  {
2960  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
2961  }
def FPSort
Definition: z3py.py:7920
FPSort mkFPSortSingle ( )
inline

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

Exceptions
Z3Exception

Definition at line 2922 of file Context.java.

2923  {
2924  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
2925  }
def FPSort
Definition: z3py.py:7920
FPExpr mkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term
Exceptions
Z3Exception

Definition at line 3214 of file Context.java.

3215  {
3216  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3217  }
FPExpr mkFPSub ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point subtraction

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

Definition at line 3164 of file Context.java.

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

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

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

Definition at line 3505 of file Context.java.

3506  {
3507  if (signed)
3508  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3509  else
3510  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3511  }
FPExpr mkFPToFP ( BitVecExpr  bv,
FPSort  s 
)
inline

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

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

Definition at line 3420 of file Context.java.

3421  {
3422  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3423  }
FPExpr mkFPToFP ( FPRMExpr  rm,
FPExpr  t,
FPSort  s 
)
inline

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

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

Definition at line 3436 of file Context.java.

3437  {
3438  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3439  }
FPExpr mkFPToFP ( FPRMExpr  rm,
RealExpr  t,
FPSort  s 
)
inline

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

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

Definition at line 3452 of file Context.java.

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

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

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

Definition at line 3470 of file Context.java.

3471  {
3472  if (signed)
3473  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3474  else
3475  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3476  }
FPExpr mkFPToFP ( FPSort  s,
FPRMExpr  rm,
FPExpr  t 
)
inline

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

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

Definition at line 3488 of file Context.java.

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

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

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

Definition at line 3555 of file Context.java.

3556  {
3557  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3558  }
BitVecExpr mkFPToIEEEBV ( FPExpr  t)
inline

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

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

Definition at line 3537 of file Context.java.

3538  {
3539  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3540  }
RealExpr mkFPToReal ( FPExpr  t)
inline

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

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

Definition at line 3522 of file Context.java.

3523  {
3524  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3525  }
FPNum mkFPZero ( FPSort  s,
boolean  negative 
)
inline

Create a floating-point zero of sort s.

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

Definition at line 3000 of file Context.java.

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

Creates a fresh Constant of sort

range

and a name prefixed with

prefix

.

Definition at line 510 of file Context.java.

511  {
512  checkContextMatch(range);
513  return Expr.create(this,
514  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
515  }
FuncDecl mkFreshConstDecl ( String  prefix,
Sort  range 
)
inline

Creates a fresh constant function declaration with a name prefixed with

prefix"

.

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

Definition at line 451 of file Context.java.

453  {
454  checkContextMatch(range);
455  return new FuncDecl(this, prefix, null, range);
456  }
FuncDecl mkFreshFuncDecl ( String  prefix,
Sort[]  domain,
Sort  range 
)
inline

Creates a fresh function declaration with a name prefixed with

prefix

.

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

Definition at line 418 of file Context.java.

420  {
421  checkContextMatch(domain);
422  checkContextMatch(range);
423  return new FuncDecl(this, prefix, domain, range);
424  }
Expr mkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 1721 of file Context.java.

1722  {
1723  checkContextMatch(domain);
1724  return Expr.create(this,
1725  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1726  }
FuncDecl mkFuncDecl ( Symbol  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 367 of file Context.java.

369  {
370  checkContextMatch(name);
371  checkContextMatch(domain);
372  checkContextMatch(range);
373  return new FuncDecl(this, name, domain, range);
374  }
FuncDecl mkFuncDecl ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 379 of file Context.java.

381  {
382  checkContextMatch(name);
383  checkContextMatch(domain);
384  checkContextMatch(range);
385  Sort[] q = new Sort[] { domain };
386  return new FuncDecl(this, name, q, range);
387  }
FuncDecl mkFuncDecl ( String  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 392 of file Context.java.

394  {
395  checkContextMatch(domain);
396  checkContextMatch(range);
397  return new FuncDecl(this, mkSymbol(name), domain, range);
398  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
FuncDecl mkFuncDecl ( String  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 403 of file Context.java.

405  {
406  checkContextMatch(domain);
407  checkContextMatch(range);
408  Sort[] q = new Sort[] { domain };
409  return new FuncDecl(this, mkSymbol(name), q, range);
410  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
BoolExpr mkGe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &gt;= t2

Definition at line 849 of file Context.java.

850  {
851  checkContextMatch(t1);
852  checkContextMatch(t2);
853  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
854  t2.getNativeObject()));
855  }
Goal mkGoal ( boolean  models,
boolean  unsatCores,
boolean  proofs 
)
inline

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

proofs

is set to true here.

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

Definition at line 2335 of file Context.java.

2337  {
2338  return new Goal(this, models, unsatCores, proofs);
2339  }
BoolExpr mkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &gt; t2

Definition at line 838 of file Context.java.

839  {
840  checkContextMatch(t1);
841  checkContextMatch(t2);
842  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
843  t2.getNativeObject()));
844  }
BoolExpr mkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 iff t2

.

Definition at line 673 of file Context.java.

674  {
675  checkContextMatch(t1);
676  checkContextMatch(t2);
677  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
678  t2.getNativeObject()));
679  }
BoolExpr mkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 -> t2

.

Definition at line 684 of file Context.java.

685  {
686  checkContextMatch(t1);
687  checkContextMatch(t2);
688  return new BoolExpr(this, Native.mkImplies(nCtx(),
689  t1.getNativeObject(), t2.getNativeObject()));
690  }
IntNum mkInt ( String  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 1938 of file Context.java.

1939  {
1940 
1941  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
1942  .getNativeObject()));
1943  }
IntNum mkInt ( int  v)
inline

Create an integer numeral.

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

Definition at line 1951 of file Context.java.

1952  {
1953 
1954  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
1955  .getNativeObject()));
1956  }
IntNum mkInt ( long  v)
inline

Create an integer numeral.

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

Definition at line 1964 of file Context.java.

1965  {
1966 
1967  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
1968  .getNativeObject()));
1969  }
BitVecExpr mkInt2BV ( int  n,
IntExpr  t 
)
inline

Create an

n

bit bit-vector from the integer argument

t

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

The argument must be of integer sort.

Definition at line 1440 of file Context.java.

1441  {
1442  checkContextMatch(t);
1443  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1444  t.getNativeObject()));
1445  }
RealExpr mkInt2Real ( IntExpr  t)
inline

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

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

k

and and asserting

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

. The argument must be of integer sort.

Definition at line 867 of file Context.java.

868  {
869  checkContextMatch(t);
870  return new RealExpr(this,
871  Native.mkInt2real(nCtx(), t.getNativeObject()));
872  }
IntExpr mkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 545 of file Context.java.

546  {
547  return (IntExpr) mkConst(name, getIntSort());
548  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
IntExpr mkIntConst ( String  name)
inline

Creates an integer constant.

Definition at line 553 of file Context.java.

554  {
555  return (IntExpr) mkConst(name, getIntSort());
556  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
IntSort mkIntSort ( )
inline

Create a new integer sort.

Definition at line 160 of file Context.java.

161  {
162  return new IntSort(this);
163  }
def IntSort
Definition: z3py.py:2625
BoolExpr mkIsInteger ( RealExpr  t)
inline

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

Definition at line 889 of file Context.java.

890  {
891  checkContextMatch(t);
892  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
893  }
Expr mkITE ( BoolExpr  t1,
Expr  t2,
Expr  t3 
)
inline

Create an expression representing an if-then-else:

ite(t1, t2, t3)

.

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

Definition at line 661 of file Context.java.

662  {
663  checkContextMatch(t1);
664  checkContextMatch(t2);
665  checkContextMatch(t3);
666  return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
667  t2.getNativeObject(), t3.getNativeObject()));
668  }
BoolExpr mkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &lt;= t2

Definition at line 827 of file Context.java.

828  {
829  checkContextMatch(t1);
830  checkContextMatch(t2);
831  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
832  t2.getNativeObject()));
833  }
ListSort mkListSort ( Symbol  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 227 of file Context.java.

228  {
229  checkContextMatch(name);
230  checkContextMatch(elemSort);
231  return new ListSort(this, name, elemSort);
232  }
ListSort mkListSort ( String  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 237 of file Context.java.

238  {
239  checkContextMatch(elemSort);
240  return new ListSort(this, mkSymbol(name), elemSort);
241  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
BoolExpr mkLt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &lt; t2

Definition at line 816 of file Context.java.

817  {
818  checkContextMatch(t1);
819  checkContextMatch(t2);
820  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
821  t2.getNativeObject()));
822  }
ArrayExpr mkMap ( FuncDecl  f,
ArrayExpr...  args 
)
inline

Maps f on the argument arrays. Remarks: 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 1677 of file Context.java.

1678  {
1679  checkContextMatch(f);
1680  checkContextMatch(args);
1681  return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1682  f.getNativeObject(), AST.arrayLength(args),
1683  AST.arrayToNative(args)));
1684  }
IntExpr mkMod ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing

t1 mod t2

. Remarks: The arguments must have int type.

Definition at line 779 of file Context.java.

780  {
781  checkContextMatch(t1);
782  checkContextMatch(t2);
783  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
784  t2.getNativeObject()));
785  }
ArithExpr mkMul ( ArithExpr...  t)
inline

Create an expression representing

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

.

Definition at line 736 of file Context.java.

737  {
738  checkContextMatch(t);
739  return (ArithExpr) Expr.create(this,
740  Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t)));
741  }
BoolExpr mkNot ( BoolExpr  a)
inline

Mk an expression representing

not(a)

.

Definition at line 648 of file Context.java.

649  {
650  checkContextMatch(a);
651  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
652  }
Expr mkNumeral ( String  v,
Sort  ty 
)
inline

Create a Term of a given sort.

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

Definition at line 1838 of file Context.java.

Referenced by Context.mkBV().

1839  {
1840  checkContextMatch(ty);
1841  return Expr.create(this,
1842  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
1843  }
Expr mkNumeral ( int  v,
Sort  ty 
)
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 1855 of file Context.java.

1856  {
1857  checkContextMatch(ty);
1858  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
1859  }
Expr mkNumeral ( long  v,
Sort  ty 
)
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 1871 of file Context.java.

1872  {
1873  checkContextMatch(ty);
1874  return Expr.create(this,
1875  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
1876  }
BoolExpr mkOr ( BoolExpr...  t)
inline

Create an expression representing

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

.

Definition at line 716 of file Context.java.

717  {
718  checkContextMatch(t);
719  return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length,
720  AST.arrayToNative(t)));
721  }
Params mkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2344 of file Context.java.

2345  {
2346  return new Params(this);
2347  }
Pattern mkPattern ( Expr...  terms)
inline

Create a quantifier pattern.

Definition at line 472 of file Context.java.

473  {
474  if (terms.length == 0)
475  throw new Z3Exception("Cannot create a pattern from zero terms");
476 
477  long[] termsNative = AST.arrayToNative(terms);
478  return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length,
479  termsNative));
480  }
ArithExpr mkPower ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 ^ t2

.

Definition at line 803 of file Context.java.

804  {
805  checkContextMatch(t1);
806  checkContextMatch(t2);
807  return (ArithExpr) Expr.create(
808  this,
809  Native.mkPower(nCtx(), t1.getNativeObject(),
810  t2.getNativeObject()));
811  }
Probe mkProbe ( String  name)
inline

Creates a new Probe.

Definition at line 2616 of file Context.java.

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

Create a Quantifier.

Definition at line 2069 of file Context.java.

2073  {
2074 
2075  if (universal)
2076  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2077  quantifierID, skolemID);
2078  else
2079  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2080  quantifierID, skolemID);
2081  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2045
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2020
Quantifier mkQuantifier ( boolean  universal,
Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a Quantifier.

Definition at line 2086 of file Context.java.

2089  {
2090 
2091  if (universal)
2092  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2093  quantifierID, skolemID);
2094  else
2095  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2096  quantifierID, skolemID);
2097  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2045
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2020
RatNum mkReal ( int  num,
int  den 
)
inline

Create a real from a fraction.

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

Definition at line 1887 of file Context.java.

1888  {
1889  if (den == 0)
1890  throw new Z3Exception("Denominator is zero");
1891 
1892  return new RatNum(this, Native.mkReal(nCtx(), num, den));
1893  }
RatNum mkReal ( String  v)
inline

Create a real numeral.

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

Definition at line 1901 of file Context.java.

1902  {
1903 
1904  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
1905  .getNativeObject()));
1906  }
RatNum mkReal ( int  v)
inline

Create a real numeral.

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

Definition at line 1914 of file Context.java.

1915  {
1916 
1917  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
1918  .getNativeObject()));
1919  }
RatNum mkReal ( long  v)
inline

Create a real numeral.

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

Definition at line 1927 of file Context.java.

1928  {
1929 
1930  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
1931  .getNativeObject()));
1932  }
IntExpr mkReal2Int ( RealExpr  t)
inline

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

Definition at line 880 of file Context.java.

881  {
882  checkContextMatch(t);
883  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
884  }
RealExpr mkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 561 of file Context.java.

562  {
563  return (RealExpr) mkConst(name, getRealSort());
564  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
RealExpr mkRealConst ( String  name)
inline

Creates a real constant.

Definition at line 569 of file Context.java.

570  {
571  return (RealExpr) mkConst(name, getRealSort());
572  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
RealSort mkRealSort ( )
inline

Create a real sort.

Definition at line 168 of file Context.java.

169  {
170  return new RealSort(this);
171  }
def RealSort
Definition: z3py.py:2641
IntExpr mkRem ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing

t1 rem t2

. Remarks: The arguments must have int type.

Definition at line 792 of file Context.java.

793  {
794  checkContextMatch(t1);
795  checkContextMatch(t2);
796  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
797  t2.getNativeObject()));
798  }
BitVecExpr mkRepeat ( int  i,
BitVecExpr  t 
)
inline

Bit-vector repetition. Remarks: The argument

t

must have a bit-vector sort.

Definition at line 1312 of file Context.java.

1313  {
1314  checkContextMatch(t);
1315  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1316  t.getNativeObject()));
1317  }
Expr mkSelect ( ArrayExpr  a,
Expr  i 
)
inline

Array read. Remarks: The argument

a

is the array and

i

is the index of the array that gets read.

The node

a

must have an array sort

[domain -> range]

, and

i

must have the sort

domain

. The sort of the result is

range

.

See also
mkArraySort
mkStore

Definition at line 1612 of file Context.java.

1613  {
1614  checkContextMatch(a);
1615  checkContextMatch(i);
1616  return Expr.create(
1617  this,
1618  Native.mkSelect(nCtx(), a.getNativeObject(),
1619  i.getNativeObject()));
1620  }
Expr mkSetAdd ( Expr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 1731 of file Context.java.

1732  {
1733  checkContextMatch(set);
1734  checkContextMatch(element);
1735  return Expr.create(
1736  this,
1737  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1738  element.getNativeObject()));
1739  }
Expr mkSetComplement ( Expr  arg)
inline

Take the complement of a set.

Definition at line 1794 of file Context.java.

1795  {
1796  checkContextMatch(arg);
1797  return Expr.create(this,
1798  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1799  }
Expr mkSetDel ( Expr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 1744 of file Context.java.

1745  {
1746  checkContextMatch(set);
1747  checkContextMatch(element);
1748  return Expr.create(
1749  this,
1750  Native.mkSetDel(nCtx(), set.getNativeObject(),
1751  element.getNativeObject()));
1752  }
Expr mkSetDifference ( Expr  arg1,
Expr  arg2 
)
inline

Take the difference between two sets.

Definition at line 1781 of file Context.java.

1782  {
1783  checkContextMatch(arg1);
1784  checkContextMatch(arg2);
1785  return Expr.create(
1786  this,
1787  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1788  arg2.getNativeObject()));
1789  }
Expr mkSetIntersection ( Expr...  args)
inline

Take the intersection of a list of sets.

Definition at line 1769 of file Context.java.

1770  {
1771  checkContextMatch(args);
1772  return Expr.create(
1773  this,
1774  Native.mkSetIntersect(nCtx(), (int) args.length,
1775  AST.arrayToNative(args)));
1776  }
Expr mkSetMembership ( Expr  elem,
Expr  set 
)
inline

Check for set membership.

Definition at line 1804 of file Context.java.

1805  {
1806  checkContextMatch(elem);
1807  checkContextMatch(set);
1808  return Expr.create(
1809  this,
1810  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1811  set.getNativeObject()));
1812  }
SetSort mkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 1702 of file Context.java.

1703  {
1704  checkContextMatch(ty);
1705  return new SetSort(this, ty);
1706  }
Expr mkSetSubset ( Expr  arg1,
Expr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 1817 of file Context.java.

1818  {
1819  checkContextMatch(arg1);
1820  checkContextMatch(arg2);
1821  return Expr.create(
1822  this,
1823  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1824  arg2.getNativeObject()));
1825  }
Expr mkSetUnion ( Expr...  args)
inline

Take the union of a list of sets.

Definition at line 1757 of file Context.java.

1758  {
1759  checkContextMatch(args);
1760  return Expr.create(
1761  this,
1762  Native.mkSetUnion(nCtx(), (int) args.length,
1763  AST.arrayToNative(args)));
1764  }
BitVecExpr mkSignExt ( int  i,
BitVecExpr  t 
)
inline

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

m+i

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

t

must have a bit-vector sort.

Definition at line 1286 of file Context.java.

1287  {
1288  checkContextMatch(t);
1289  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1290  t.getNativeObject()));
1291  }
Solver mkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 2763 of file Context.java.

2764  {
2765  return new Solver(this, Native.mkSimpleSolver(nCtx()));
2766  }
Solver mkSolver ( )
inline

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

Definition at line 2729 of file Context.java.

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

2730  {
2731  return mkSolver((Symbol) null);
2732  }
Solver mkSolver ( Symbol  logic)
inline

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

Definition at line 2741 of file Context.java.

2742  {
2743 
2744  if (logic == null)
2745  return new Solver(this, Native.mkSolver(nCtx()));
2746  else
2747  return new Solver(this, Native.mkSolverForLogic(nCtx(),
2748  logic.getNativeObject()));
2749  }
Solver mkSolver ( String  logic)
inline

Creates a new (incremental) solver.

See also
mkSolver(Symbol)

Definition at line 2755 of file Context.java.

2756  {
2757  return mkSolver(mkSymbol(logic));
2758  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
Solver mkSolver ( Tactic  t)
inline

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

Push

and

Pop

, but it will always solve each check from scratch.

Definition at line 2774 of file Context.java.

2775  {
2776 
2777  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
2778  t.getNativeObject()));
2779  }
ArrayExpr mkStore ( ArrayExpr  a,
Expr  i,
Expr  v 
)
inline

Array update. Remarks: The node

a

must have an array sort

[domain -> range]

,

i

must have sort

domain

,

v

must have sort range. The sort of the result is

[domain -> range]

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

a

(with respect to

) on all indices except for

i

, where it maps to

v

(and the

of

a

with respect to

i

may be a different value).

See also
mkArraySort
mkSelect

Definition at line 1638 of file Context.java.

1639  {
1640  checkContextMatch(a);
1641  checkContextMatch(i);
1642  checkContextMatch(v);
1643  return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1644  i.getNativeObject(), v.getNativeObject()));
1645  }
ArithExpr mkSub ( ArithExpr...  t)
inline

Create an expression representing

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

.

Definition at line 746 of file Context.java.

747  {
748  checkContextMatch(t);
749  return (ArithExpr) Expr.create(this,
750  Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t)));
751  }
IntSymbol mkSymbol ( int  i)
inline

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

Definition at line 72 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().

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

Create a symbol using a string.

Definition at line 80 of file Context.java.

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

Creates a new Tactic.

Definition at line 2382 of file Context.java.

Referenced by Goal.simplify().

2383  {
2384  return new Tactic(this, name);
2385  }
Expr mkTermArray ( ArrayExpr  array)
inline

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

Definition at line 1692 of file Context.java.

1693  {
1694  checkContextMatch(array);
1695  return Expr.create(this,
1696  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1697  }
BoolExpr mkTrue ( )
inline

The true Term.

Definition at line 603 of file Context.java.

Referenced by Context.mkBool().

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

Create a new tuple sort.

Definition at line 194 of file Context.java.

196  {
197  checkContextMatch(name);
198  checkContextMatch(fieldNames);
199  checkContextMatch(fieldSorts);
200  return new TupleSort(this, name, (int) fieldNames.length, fieldNames,
201  fieldSorts);
202  }
ArithExpr mkUnaryMinus ( ArithExpr  t)
inline

Create an expression representing

-t

.

Definition at line 756 of file Context.java.

757  {
758  checkContextMatch(t);
759  return (ArithExpr) Expr.create(this,
760  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
761  }
UninterpretedSort mkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 143 of file Context.java.

Referenced by Context.mkUninterpretedSort().

144  {
145  checkContextMatch(s);
146  return new UninterpretedSort(this, s);
147  }
UninterpretedSort mkUninterpretedSort ( String  str)
inline

Create a new uninterpreted sort.

Definition at line 152 of file Context.java.

153  {
154  return mkUninterpretedSort(mkSymbol(str));
155  }
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:143
IntSymbol mkSymbol(int i)
Definition: Context.java:72
BoolExpr mkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 xor t2

.

Definition at line 695 of file Context.java.

696  {
697  checkContextMatch(t1);
698  checkContextMatch(t2);
699  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
700  t2.getNativeObject()));
701  }
BitVecExpr mkZeroExt ( int  i,
BitVecExpr  t 
)
inline

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

m+i

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

t

must have a bit-vector sort.

Definition at line 1300 of file Context.java.

1301  {
1302  checkContextMatch(t);
1303  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1304  t.getNativeObject()));
1305  }
Probe not ( Probe  p)
inline

Create a probe that evaluates to "true" when the value

p

does not evaluate to "true".

Definition at line 2716 of file Context.java.

2717  {
2718  checkContextMatch(p);
2719  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2720  }
Probe or ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to "true" when the value

p1

or

p2

evaluate to "true".

Definition at line 2705 of file Context.java.

2706  {
2707  checkContextMatch(p1);
2708  checkContextMatch(p2);
2709  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
2710  p2.getNativeObject()));
2711  }
Tactic orElse ( Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that first applies

t1

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

t2

applied to the Goal.

Definition at line 2432 of file Context.java.

2433  {
2434  checkContextMatch(t1);
2435  checkContextMatch(t2);
2436  return new Tactic(this, Native.tacticOrElse(nCtx(),
2437  t1.getNativeObject(), t2.getNativeObject()));
2438  }
Tactic parAndThen ( Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that applies

t1

to a given goal and then

t2

to every subgoal produced by

t1

. The subgoals are processed in parallel.

Definition at line 2565 of file Context.java.

2566  {
2567  checkContextMatch(t1);
2568  checkContextMatch(t2);
2569  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2570  t1.getNativeObject(), t2.getNativeObject()));
2571  }
Tactic parOr ( Tactic...  t)
inline

Create a tactic that applies the given tactics in parallel.

Definition at line 2554 of file Context.java.

2555  {
2556  checkContextMatch(t);
2557  return new Tactic(this, Native.tacticParOr(nCtx(),
2558  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2559  }
BoolExpr parseSMTLIB2File ( String  fileName,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
)
inline

Parse the given file using the SMT-LIB2 parser.

See also
parseSMTLIB2String

Definition at line 2307 of file Context.java.

2310  {
2311 
2312  int csn = Symbol.arrayLength(sortNames);
2313  int cs = Sort.arrayLength(sorts);
2314  int cdn = Symbol.arrayLength(declNames);
2315  int cd = AST.arrayLength(decls);
2316  if (csn != cs || cdn != cd)
2317  throw new Z3Exception("Argument size mismatch");
2318  return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
2319  fileName, AST.arrayLength(sorts),
2320  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2321  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2322  AST.arrayToNative(decls)));
2323  }
BoolExpr parseSMTLIB2String ( String  str,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
)
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 2286 of file Context.java.

2289  {
2290 
2291  int csn = Symbol.arrayLength(sortNames);
2292  int cs = Sort.arrayLength(sorts);
2293  int cdn = Symbol.arrayLength(declNames);
2294  int cd = AST.arrayLength(decls);
2295  if (csn != cs || cdn != cd)
2296  throw new Z3Exception("Argument size mismatch");
2297  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2298  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2299  AST.arrayToNative(sorts), AST.arrayLength(decls),
2300  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2301  }
void parseSMTLIBFile ( String  fileName,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
)
inline

Parse the given file using the SMT-LIB parser.

See also
parseSMTLIBString

Definition at line 2169 of file Context.java.

2172  {
2173  int csn = Symbol.arrayLength(sortNames);
2174  int cs = Sort.arrayLength(sorts);
2175  int cdn = Symbol.arrayLength(declNames);
2176  int cd = AST.arrayLength(decls);
2177  if (csn != cs || cdn != cd)
2178  throw new Z3Exception("Argument size mismatch");
2179  Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
2180  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2181  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2182  AST.arrayToNative(decls));
2183  }
void parseSMTLIBString ( String  str,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
)
inline

Parse the given string using the SMT-LIB parser. Remarks: 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 2150 of file Context.java.

2152  {
2153  int csn = Symbol.arrayLength(sortNames);
2154  int cs = Sort.arrayLength(sorts);
2155  int cdn = Symbol.arrayLength(declNames);
2156  int cd = AST.arrayLength(decls);
2157  if (csn != cs || cdn != cd)
2158  throw new Z3Exception("Argument size mismatch");
2159  Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
2160  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2161  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2162  AST.arrayToNative(decls));
2163  }
Tactic repeat ( Tactic  t,
int  max 
)
inline

Create a tactic that keeps applying

t

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

max

is reached.

Definition at line 2485 of file Context.java.

2486  {
2487  checkContextMatch(t);
2488  return new Tactic(this, Native.tacticRepeat(nCtx(),
2489  t.getNativeObject(), max));
2490  }
void setPrintMode ( Z3_ast_print_mode  value)
inline

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

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

Definition at line 2113 of file Context.java.

2114  {
2115  Native.setAstPrintMode(nCtx(), value.toInt());
2116  }
String SimplifyHelp ( )
inline

Return a string describing all available parameters to

Expr.Simplify

.

Definition at line 3597 of file Context.java.

3598  {
3599  return Native.simplifyGetHelp(nCtx());
3600  }
Tactic skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 2495 of file Context.java.

2496  {
2497  return new Tactic(this, Native.tacticSkip(nCtx()));
2498  }
Tactic then ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
)
inline

Create a tactic that applies

t1

to a Goal and then

t2"/> to every subgoal produced by <paramref name="t1

.

Remarks: Shorthand for

.

Definition at line 2422 of file Context.java.

2423  {
2424  return andThen(t1, t2, ts);
2425  }
Tactic andThen(Tactic t1, Tactic t2, Tactic...ts)
Definition: Context.java:2391
Tactic tryFor ( Tactic  t,
int  ms 
)
inline

Create a tactic that applies

t

to a goal for

ms

milliseconds. Remarks: If

t

does not terminate within

ms

milliseconds, then it fails.

Definition at line 2446 of file Context.java.

2447  {
2448  checkContextMatch(t);
2449  return new Tactic(this, Native.tacticTryFor(nCtx(),
2450  t.getNativeObject(), ms));
2451  }
long unwrapAST ( AST  a)
inline

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

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

Definition at line 3588 of file Context.java.

3589  {
3590  return a.getNativeObject();
3591  }
void updateParamValue ( String  id,
String  value 
)
inline

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

z3.exe -ini?

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

Definition at line 3618 of file Context.java.

3619  {
3620  Native.updateParamValue(nCtx(), id, value);
3621  }
Tactic usingParams ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

.

Definition at line 2532 of file Context.java.

Referenced by Context.with().

2533  {
2534  checkContextMatch(t);
2535  checkContextMatch(p);
2536  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2537  t.getNativeObject(), p.getNativeObject()));
2538  }
Tactic when ( Probe  p,
Tactic  t 
)
inline

Create a tactic that applies

t

to a given goal if the probe

p

evaluates to true. Remarks: If

p

evaluates to false, then the new tactic behaves like the

tactic.

Definition at line 2459 of file Context.java.

2460  {
2461  checkContextMatch(t);
2462  checkContextMatch(p);
2463  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2464  t.getNativeObject()));
2465  }
Tactic with ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

. Remarks: Alias for

UsingParams

Definition at line 2546 of file Context.java.

2547  {
2548  return usingParams(t, p);
2549  }
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2532
AST wrapAST ( long  nativeObject)
inline

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

nativeObject

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

UnwrapAST

) and that it must have a correct reference count.

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

Definition at line 3571 of file Context.java.

3572  {
3573  return AST.create(this, nativeObject);
3574  }

Field Documentation

long m_refCount = 0
protected

Definition at line 3740 of file Context.java.

Referenced by Z3Object.dispose().