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)
 
Expr MkUpdateField (FuncDecl field, Expr t, Expr v) throws Z3Exception
 
FuncDecl mkFuncDecl (Symbol name, Sort[] domain, Sort range)
 
FuncDecl mkFuncDecl (Symbol name, Sort domain, Sort range)
 
FuncDecl mkFuncDecl (String name, Sort[] domain, Sort range)
 
FuncDecl mkFuncDecl (String name, Sort domain, Sort range)
 
FuncDecl mkFreshFuncDecl (String prefix, Sort[] domain, Sort range)
 
FuncDecl mkConstDecl (Symbol name, Sort range)
 
FuncDecl mkConstDecl (String name, Sort range)
 
FuncDecl mkFreshConstDecl (String prefix, Sort range)
 
Expr mkBound (int index, Sort ty)
 
Pattern mkPattern (Expr...terms)
 
Expr mkConst (Symbol name, Sort range)
 
Expr mkConst (String name, Sort range)
 
Expr mkFreshConst (String prefix, Sort range)
 
Expr mkConst (FuncDecl f)
 
BoolExpr mkBoolConst (Symbol name)
 
BoolExpr mkBoolConst (String name)
 
IntExpr mkIntConst (Symbol name)
 
IntExpr mkIntConst (String name)
 
RealExpr mkRealConst (Symbol name)
 
RealExpr mkRealConst (String name)
 
BitVecExpr mkBVConst (Symbol name, int size)
 
BitVecExpr mkBVConst (String name, int size)
 
Expr mkApp (FuncDecl f, Expr...args)
 
BoolExpr mkTrue ()
 
BoolExpr mkFalse ()
 
BoolExpr mkBool (boolean value)
 
BoolExpr mkEq (Expr x, Expr y)
 
BoolExpr mkDistinct (Expr...args)
 
BoolExpr mkNot (BoolExpr a)
 
Expr mkITE (BoolExpr t1, Expr t2, Expr t3)
 
BoolExpr mkIff (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkImplies (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkXor (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkAnd (BoolExpr...t)
 
BoolExpr mkOr (BoolExpr...t)
 
ArithExpr mkAdd (ArithExpr...t)
 
ArithExpr mkMul (ArithExpr...t)
 
ArithExpr mkSub (ArithExpr...t)
 
ArithExpr mkUnaryMinus (ArithExpr t)
 
ArithExpr mkDiv (ArithExpr t1, ArithExpr t2)
 
IntExpr mkMod (IntExpr t1, IntExpr t2)
 
IntExpr mkRem (IntExpr t1, IntExpr t2)
 
ArithExpr mkPower (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkLt (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkLe (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkGt (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkGe (ArithExpr t1, ArithExpr t2)
 
RealExpr mkInt2Real (IntExpr t)
 
IntExpr mkReal2Int (RealExpr t)
 
BoolExpr mkIsInteger (RealExpr t)
 
BitVecExpr mkBVNot (BitVecExpr t)
 
BitVecExpr mkBVRedAND (BitVecExpr t)
 
BitVecExpr mkBVRedOR (BitVecExpr t)
 
BitVecExpr mkBVAND (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVXOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNAND (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVXNOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNeg (BitVecExpr t)
 
BitVecExpr mkBVAdd (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSub (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVMul (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVUDiv (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSDiv (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVURem (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSRem (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSMod (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVULT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSLT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVULE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSLE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVUGE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSGE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVUGT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSGT (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkConcat (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkExtract (int high, int low, BitVecExpr t)
 
BitVecExpr mkSignExt (int i, BitVecExpr t)
 
BitVecExpr mkZeroExt (int i, BitVecExpr t)
 
BitVecExpr mkRepeat (int i, BitVecExpr t)
 
BitVecExpr mkBVSHL (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVLSHR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVASHR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVRotateLeft (int i, BitVecExpr t)
 
BitVecExpr mkBVRotateRight (int i, BitVecExpr t)
 
BitVecExpr mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVRotateRight (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkInt2BV (int n, IntExpr t)
 
IntExpr mkBV2Int (BitVecExpr t, boolean signed)
 
BoolExpr mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVNegNoOverflow (BitVecExpr t)
 
BoolExpr mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 
ArrayExpr mkArrayConst (Symbol name, Sort domain, Sort range)
 
ArrayExpr mkArrayConst (String name, Sort domain, Sort range)
 
Expr mkSelect (ArrayExpr a, Expr i)
 
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)
 
ArrayExpr mkEmptySet (Sort domain)
 
ArrayExpr mkFullSet (Sort domain)
 
ArrayExpr mkSetAdd (ArrayExpr set, Expr element)
 
ArrayExpr mkSetDel (ArrayExpr set, Expr element)
 
ArrayExpr mkSetUnion (ArrayExpr...args)
 
ArrayExpr mkSetIntersection (ArrayExpr...args)
 
ArrayExpr mkSetDifference (ArrayExpr arg1, ArrayExpr arg2)
 
ArrayExpr mkSetComplement (ArrayExpr arg)
 
BoolExpr mkSetMembership (Expr elem, ArrayExpr set)
 
BoolExpr mkSetSubset (ArrayExpr arg1, ArrayExpr arg2)
 
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 ()
 
Optimize mkOptimize ()
 
FPRMSort mkFPRoundingModeSort ()
 
FPRMExpr mkFPRoundNearestTiesToEven ()
 
FPRMNum mkFPRNE ()
 
FPRMNum mkFPRoundNearestTiesToAway ()
 
FPRMNum mkFPRNA ()
 
FPRMNum mkFPRoundTowardPositive ()
 
FPRMNum mkFPRTP ()
 
FPRMNum mkFPRoundTowardNegative ()
 
FPRMNum mkFPRTN ()
 
FPRMNum mkFPRoundTowardZero ()
 
FPRMNum mkFPRTZ ()
 
FPSort mkFPSort (int ebits, int sbits)
 
FPSort mkFPSortHalf ()
 
FPSort mkFPSort16 ()
 
FPSort mkFPSortSingle ()
 
FPSort mkFPSort32 ()
 
FPSort mkFPSortDouble ()
 
FPSort mkFPSort64 ()
 
FPSort mkFPSortQuadruple ()
 
FPSort mkFPSort128 ()
 
FPNum mkFPNaN (FPSort s)
 
FPNum mkFPInf (FPSort s, boolean negative)
 
FPNum mkFPZero (FPSort s, boolean negative)
 
FPNum mkFPNumeral (float v, FPSort s)
 
FPNum mkFPNumeral (double v, FPSort s)
 
FPNum mkFPNumeral (int v, FPSort s)
 
FPNum mkFPNumeral (boolean sgn, int exp, int sig, FPSort s)
 
FPNum mkFPNumeral (boolean sgn, long exp, long sig, FPSort s)
 
FPNum mkFP (float v, FPSort s)
 
FPNum mkFP (double v, FPSort s)
 
FPNum mkFP (int v, FPSort s)
 
FPNum mkFP (boolean sgn, int exp, int sig, FPSort s)
 
FPNum mkFP (boolean sgn, long exp, long sig, FPSort s)
 
FPExpr mkFPAbs (FPExpr t)
 
FPExpr mkFPNeg (FPExpr t)
 
FPExpr mkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
 
FPExpr mkFPSqrt (FPRMExpr rm, FPExpr t)
 
FPExpr mkFPRem (FPExpr t1, FPExpr t2)
 
FPExpr mkFPRoundToIntegral (FPRMExpr rm, FPExpr t)
 
FPExpr mkFPMin (FPExpr t1, FPExpr t2)
 
FPExpr mkFPMax (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPLEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPLt (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPGEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPGt (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPIsNormal (FPExpr t)
 
BoolExpr mkFPIsSubnormal (FPExpr t)
 
BoolExpr mkFPIsZero (FPExpr t)
 
BoolExpr mkFPIsInfinite (FPExpr t)
 
BoolExpr mkFPIsNaN (FPExpr t)
 
BoolExpr mkFPIsNegative (FPExpr t)
 
BoolExpr mkFPIsPositive (FPExpr t)
 
FPExpr mkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
 
FPExpr mkFPToFP (BitVecExpr bv, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, FPExpr t, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, RealExpr t, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
 
FPExpr mkFPToFP (FPSort s, FPRMExpr rm, FPExpr t)
 
BitVecExpr mkFPToBV (FPRMExpr rm, FPExpr t, int sz, boolean signed)
 
RealExpr mkFPToReal (FPExpr t)
 
BitVecExpr mkFPToIEEEBV (FPExpr t)
 
BitVecExpr mkFPToFP (FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
 
AST wrapAST (long nativeObject)
 
long unwrapAST (AST a)
 
String SimplifyHelp ()
 
ParamDescrs getSimplifyParameterDescriptions ()
 
void updateParamValue (String id, String value)
 
IDecRefQueue 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 ()
 
IDecRefQueue getOptimizeDRQ ()
 
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:4100

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

2705  {
2706  checkContextMatch(p1);
2707  checkContextMatch(p2);
2708  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
2709  p2.getNativeObject()));
2710  }
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 2401 of file Context.java.

Referenced by Context.then().

2403  {
2404  checkContextMatch(t1);
2405  checkContextMatch(t2);
2406  checkContextMatch(ts);
2407 
2408  long last = 0;
2409  if (ts != null && ts.length > 0)
2410  {
2411  last = ts[ts.length - 1].getNativeObject();
2412  for (int i = ts.length - 2; i >= 0; i--)
2413  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2414  last);
2415  }
2416  if (last != 0)
2417  {
2418  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2419  return new Tactic(this, Native.tacticAndThen(nCtx(),
2420  t1.getNativeObject(), last));
2421  } else
2422  return new Tactic(this, Native.tacticAndThen(nCtx(),
2423  t1.getNativeObject(), t2.getNativeObject()));
2424  }
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 2141 of file Context.java.

2144  {
2145 
2146  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2147  attributes, (int) assumptions.length,
2148  AST.arrayToNative(assumptions), formula.getNativeObject());
2149  }
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 2482 of file Context.java.

2483  {
2484  checkContextMatch(p);
2485  checkContextMatch(t1);
2486  checkContextMatch(t2);
2487  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2488  t1.getNativeObject(), t2.getNativeObject()));
2489  }
Probe constProbe ( double  val)
inline

Create a probe that always evaluates to

val

.

Definition at line 2634 of file Context.java.

2635  {
2636  return new Probe(this, Native.probeConst(nCtx(), val));
2637  }
void dispose ( )
inline

Disposes of the context.

Definition at line 3792 of file Context.java.

Referenced by Context.finalize().

3793  {
3794  m_AST_DRQ.clear(this);
3795  m_ASTMap_DRQ.clear(this);
3796  m_ASTVector_DRQ.clear(this);
3797  m_ApplyResult_DRQ.clear(this);
3798  m_FuncEntry_DRQ.clear(this);
3799  m_FuncInterp_DRQ.clear(this);
3800  m_Goal_DRQ.clear(this);
3801  m_Model_DRQ.clear(this);
3802  m_Params_DRQ.clear(this);
3803  m_Probe_DRQ.clear(this);
3804  m_Solver_DRQ.clear(this);
3805  m_Statistics_DRQ.clear(this);
3806  m_Tactic_DRQ.clear(this);
3807  m_Fixedpoint_DRQ.clear(this);
3808 
3809  m_boolSort = null;
3810  m_intSort = null;
3811  m_realSort = null;
3812  }
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 2693 of file Context.java.

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

2694  {
2695  checkContextMatch(p1);
2696  checkContextMatch(p2);
2697  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2698  p2.getNativeObject()));
2699  }
Tactic fail ( )
inline

Create a tactic always fails.

Definition at line 2513 of file Context.java.

2514  {
2515  return new Tactic(this, Native.tacticFail(nCtx()));
2516  }
Tactic failIf ( Probe  p)
inline

Create a tactic that fails if the probe

p

evaluates to false.

Definition at line 2522 of file Context.java.

2523  {
2524  checkContextMatch(p);
2525  return new Tactic(this,
2526  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2527  }
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 2533 of file Context.java.

2534  {
2535  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2536  }
void finalize ( )
inlineprotected

Finalizer.

Definition at line 3769 of file Context.java.

3770  {
3771  dispose();
3772 
3773  if (m_refCount == 0)
3774  {
3775  try
3776  {
3777  Native.delContext(m_ctx);
3778  } catch (Z3Exception e)
3779  {
3780  // OK.
3781  }
3782  m_ctx = 0;
3783  }
3784  /*
3785  else
3786  CMW: re-queue the finalizer? */
3787  }
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 2681 of file Context.java.

2682  {
2683  checkContextMatch(p1);
2684  checkContextMatch(p2);
2685  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2686  p2.getNativeObject()));
2687  }
IDecRefQueue getApplyResultDRQ ( )
inline

Definition at line 3699 of file Context.java.

Referenced by ApplyResult.toString().

3700  {
3701  return m_ApplyResult_DRQ;
3702  }
IDecRefQueue getASTDRQ ( )
inline

Definition at line 3684 of file Context.java.

Referenced by AST.getSExpr().

3685  {
3686  return m_AST_DRQ;
3687  }
IDecRefQueue getASTMapDRQ ( )
inline

Definition at line 3689 of file Context.java.

3690  {
3691  return m_ASTMap_DRQ;
3692  }
IDecRefQueue getASTVectorDRQ ( )
inline

Definition at line 3694 of file Context.java.

Referenced by ASTVector.toString().

3695  {
3696  return m_ASTVector_DRQ;
3697  }
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(ctx=None)
Definition: z3py.py:1346
IDecRefQueue getFixedpointDRQ ( )
inline

Definition at line 3754 of file Context.java.

Referenced by Fixedpoint.ParseString().

3755  {
3756  return m_Fixedpoint_DRQ;
3757  }
IDecRefQueue getFuncEntryDRQ ( )
inline

Definition at line 3704 of file Context.java.

Referenced by FuncInterp.Entry.toString().

3705  {
3706  return m_FuncEntry_DRQ;
3707  }
IDecRefQueue getFuncInterpDRQ ( )
inline

Definition at line 3709 of file Context.java.

Referenced by FuncInterp.toString().

3710  {
3711  return m_FuncInterp_DRQ;
3712  }
IDecRefQueue getGoalDRQ ( )
inline

Definition at line 3714 of file Context.java.

Referenced by Goal.AsBoolExpr().

3715  {
3716  return m_Goal_DRQ;
3717  }
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(ctx=None)
Definition: z3py.py:2639
IDecRefQueue getModelDRQ ( )
inline

Definition at line 3719 of file Context.java.

Referenced by Model.toString().

3720  {
3721  return m_Model_DRQ;
3722  }
int getNumProbes ( )
inline

The number of supported Probes.

Definition at line 2596 of file Context.java.

Referenced by Context.getProbeNames().

2597  {
2598  return Native.getNumProbes(nCtx());
2599  }
int getNumSMTLIBAssumptions ( )
inline

The number of SMTLIB assumptions parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2223 of file Context.java.

Referenced by Context.getSMTLIBAssumptions().

2224  {
2225  return Native.getSmtlibNumAssumptions(nCtx());
2226  }
int getNumSMTLIBDecls ( )
inline

The number of SMTLIB declarations parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2247 of file Context.java.

Referenced by Context.getSMTLIBDecls().

2248  {
2249  return Native.getSmtlibNumDecls(nCtx());
2250  }
int getNumSMTLIBFormulas ( )
inline

The number of SMTLIB formulas parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2199 of file Context.java.

Referenced by Context.getSMTLIBFormulas().

2200  {
2201  return Native.getSmtlibNumFormulas(nCtx());
2202  }
int getNumSMTLIBSorts ( )
inline

The number of SMTLIB sorts parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2270 of file Context.java.

Referenced by Context.getSMTLIBSorts().

2271  {
2272  return Native.getSmtlibNumSorts(nCtx());
2273  }
int getNumTactics ( )
inline

The number of supported tactics.

Definition at line 2362 of file Context.java.

Referenced by Context.getTacticNames().

2363  {
2364  return Native.getNumTactics(nCtx());
2365  }
IDecRefQueue getOptimizeDRQ ( )
inline

Definition at line 3759 of file Context.java.

3760  {
3761  return m_Optimize_DRQ;
3762  }
IDecRefQueue getParamDescrsDRQ ( )
inline

Definition at line 3729 of file Context.java.

Referenced by ParamDescrs.toString().

3730  {
3731  return m_ParamDescrs_DRQ;
3732  }
IDecRefQueue getParamsDRQ ( )
inline

Definition at line 3724 of file Context.java.

Referenced by Params.toString().

3725  {
3726  return m_Params_DRQ;
3727  }
String getProbeDescription ( String  name)
inline

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

Definition at line 2618 of file Context.java.

2619  {
2620  return Native.probeGetDescr(nCtx(), name);
2621  }
IDecRefQueue getProbeDRQ ( )
inline

Definition at line 3734 of file Context.java.

Referenced by Probe.apply().

3735  {
3736  return m_Probe_DRQ;
3737  }
String [] getProbeNames ( )
inline

The names of all supported Probes.

Definition at line 2604 of file Context.java.

2605  {
2606 
2607  int n = getNumProbes();
2608  String[] res = new String[n];
2609  for (int i = 0; i < n; i++)
2610  res[i] = Native.getProbeName(nCtx(), i);
2611  return res;
2612  }
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(ctx=None)
Definition: z3py.py:2655
ParamDescrs getSimplifyParameterDescriptions ( )
inline

Retrieves parameter descriptions for simplifier.

Definition at line 3623 of file Context.java.

3624  {
3625  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3626  }
BoolExpr [] getSMTLIBAssumptions ( )
inline

The assumptions parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2232 of file Context.java.

2233  {
2234 
2235  int n = getNumSMTLIBAssumptions();
2236  BoolExpr[] res = new BoolExpr[n];
2237  for (int i = 0; i < n; i++)
2238  res[i] = (BoolExpr) Expr.create(this,
2239  Native.getSmtlibAssumption(nCtx(), i));
2240  return res;
2241  }
FuncDecl [] getSMTLIBDecls ( )
inline

The declarations parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2256 of file Context.java.

2257  {
2258 
2259  int n = getNumSMTLIBDecls();
2260  FuncDecl[] res = new FuncDecl[n];
2261  for (int i = 0; i < n; i++)
2262  res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
2263  return res;
2264  }
BoolExpr [] getSMTLIBFormulas ( )
inline

The formulas parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2208 of file Context.java.

2209  {
2210 
2211  int n = getNumSMTLIBFormulas();
2212  BoolExpr[] res = new BoolExpr[n];
2213  for (int i = 0; i < n; i++)
2214  res[i] = (BoolExpr) Expr.create(this,
2215  Native.getSmtlibFormula(nCtx(), i));
2216  return res;
2217  }
Sort [] getSMTLIBSorts ( )
inline

The declarations parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2279 of file Context.java.

2280  {
2281 
2282  int n = getNumSMTLIBSorts();
2283  Sort[] res = new Sort[n];
2284  for (int i = 0; i < n; i++)
2285  res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
2286  return res;
2287  }
IDecRefQueue getSolverDRQ ( )
inline

Definition at line 3739 of file Context.java.

Referenced by Solver.toString().

3740  {
3741  return m_Solver_DRQ;
3742  }
IDecRefQueue getStatisticsDRQ ( )
inline

Definition at line 3744 of file Context.java.

3745  {
3746  return m_Statistics_DRQ;
3747  }
String getTacticDescription ( String  name)
inline

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

Definition at line 2384 of file Context.java.

2385  {
2386  return Native.tacticGetDescr(nCtx(), name);
2387  }
IDecRefQueue getTacticDRQ ( )
inline

Definition at line 3749 of file Context.java.

Referenced by Tactic.getSolver().

3750  {
3751  return m_Tactic_DRQ;
3752  }
String [] getTacticNames ( )
inline

The names of all supported tactics.

Definition at line 2370 of file Context.java.

2371  {
2372 
2373  int n = getNumTactics();
2374  String[] res = new String[n];
2375  for (int i = 0; i < n; i++)
2376  res[i] = Native.getTacticName(nCtx(), i);
2377  return res;
2378  }
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 2655 of file Context.java.

2656  {
2657  checkContextMatch(p1);
2658  checkContextMatch(p2);
2659  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2660  p2.getNativeObject()));
2661  }
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 2588 of file Context.java.

2589  {
2590  Native.interrupt(nCtx());
2591  }
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 2668 of file Context.java.

2669  {
2670  checkContextMatch(p1);
2671  checkContextMatch(p2);
2672  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2673  p2.getNativeObject()));
2674  }
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 2643 of file Context.java.

2644  {
2645  checkContextMatch(p1);
2646  checkContextMatch(p2);
2647  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2648  p2.getNativeObject()));
2649  }
ArithExpr mkAdd ( ArithExpr...  t)
inline

Create an expression representing

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

.

Definition at line 743 of file Context.java.

744  {
745  checkContextMatch(t);
746  return (ArithExpr) Expr.create(this,
747  Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t)));
748  }
BoolExpr mkAnd ( BoolExpr...  t)
inline

Create an expression representing

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

.

Definition at line 723 of file Context.java.

Referenced by Goal.AsBoolExpr().

724  {
725  checkContextMatch(t);
726  return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length,
727  AST.arrayToNative(t)));
728  }
Expr mkApp ( FuncDecl  f,
Expr...  args 
)
inline

Create a new function application.

Definition at line 610 of file Context.java.

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

611  {
612  checkContextMatch(f);
613  checkContextMatch(args);
614  return Expr.create(this, f, args);
615  }
ArrayExpr mkArrayConst ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1601 of file Context.java.

1603  {
1604  return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1605  }
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:184
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:503
ArrayExpr mkArrayConst ( String  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1610 of file Context.java.

1612  {
1613  return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1614  }
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:503
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:4004
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(sz, ctx=None)
Definition: z3py.py:3460
BoolExpr mkBool ( boolean  value)
inline

Creates a Boolean value.

Definition at line 636 of file Context.java.

637  {
638  return value ? mkTrue() : mkFalse();
639  }
BoolExpr mkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 546 of file Context.java.

547  {
548  return (BoolExpr) mkConst(name, getBoolSort());
549  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:503
BoolExpr mkBoolConst ( String  name)
inline

Create a Boolean constant.

Definition at line 554 of file Context.java.

555  {
556  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
557  }
IntSymbol mkSymbol(int i)
Definition: Context.java:72
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:503
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(ctx=None)
Definition: z3py.py:1346
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 480 of file Context.java.

481  {
482  return Expr.create(this,
483  Native.mkBound(nCtx(), index, ty.getNativeObject()));
484  }
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 1986 of file Context.java.

1987  {
1988  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
1989  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1848
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 1996 of file Context.java.

1997  {
1998  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
1999  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1848
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 2006 of file Context.java.

2007  {
2008  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2009  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1848
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 1478 of file Context.java.

1479  {
1480  checkContextMatch(t);
1481  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1482  (signed) ? true : false));
1483  }
BitVecExpr mkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1041 of file Context.java.

1042  {
1043  checkContextMatch(t1);
1044  checkContextMatch(t2);
1045  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1046  t1.getNativeObject(), t2.getNativeObject()));
1047  }
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 1490 of file Context.java.

1492  {
1493  checkContextMatch(t1);
1494  checkContextMatch(t2);
1495  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1496  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1497  : false));
1498  }
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 1505 of file Context.java.

1507  {
1508  checkContextMatch(t1);
1509  checkContextMatch(t2);
1510  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1511  t1.getNativeObject(), t2.getNativeObject()));
1512  }
BitVecExpr mkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 952 of file Context.java.

953  {
954  checkContextMatch(t1);
955  checkContextMatch(t2);
956  return new BitVecExpr(this, Native.mkBvand(nCtx(),
957  t1.getNativeObject(), t2.getNativeObject()));
958  }
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 1386 of file Context.java.

1387  {
1388  checkContextMatch(t1);
1389  checkContextMatch(t2);
1390  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1391  t1.getNativeObject(), t2.getNativeObject()));
1392  }
BitVecExpr mkBVConst ( Symbol  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 594 of file Context.java.

595  {
596  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
597  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:176
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:503
BitVecExpr mkBVConst ( String  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 602 of file Context.java.

603  {
604  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
605  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:176
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:503
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 1366 of file Context.java.

1367  {
1368  checkContextMatch(t1);
1369  checkContextMatch(t2);
1370  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1371  t1.getNativeObject(), t2.getNativeObject()));
1372  }
BitVecExpr mkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1067 of file Context.java.

1068  {
1069  checkContextMatch(t1);
1070  checkContextMatch(t2);
1071  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1072  t1.getNativeObject(), t2.getNativeObject()));
1073  }
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 1574 of file Context.java.

1576  {
1577  checkContextMatch(t1);
1578  checkContextMatch(t2);
1579  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1580  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1581  : false));
1582  }
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 1589 of file Context.java.

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

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

Definition at line 991 of file Context.java.

992  {
993  checkContextMatch(t1);
994  checkContextMatch(t2);
995  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
996  t1.getNativeObject(), t2.getNativeObject()));
997  }
BitVecExpr mkBVNeg ( BitVecExpr  t)
inline

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

Definition at line 1030 of file Context.java.

1031  {
1032  checkContextMatch(t);
1033  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1034  }
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 1562 of file Context.java.

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

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

Definition at line 1004 of file Context.java.

1005  {
1006  checkContextMatch(t1);
1007  checkContextMatch(t2);
1008  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1009  t1.getNativeObject(), t2.getNativeObject()));
1010  }
BitVecExpr mkBVNot ( BitVecExpr  t)
inline

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

Definition at line 917 of file Context.java.

918  {
919  checkContextMatch(t);
920  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
921  }
BitVecExpr mkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 965 of file Context.java.

966  {
967  checkContextMatch(t1);
968  checkContextMatch(t2);
969  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
970  t2.getNativeObject()));
971  }
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 928 of file Context.java.

929  {
930  checkContextMatch(t);
931  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
932  t.getNativeObject()));
933  }
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 940 of file Context.java.

941  {
942  checkContextMatch(t);
943  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
944  t.getNativeObject()));
945  }
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 1399 of file Context.java.

1400  {
1401  checkContextMatch(t);
1402  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1403  t.getNativeObject()));
1404  }
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 1424 of file Context.java.

1426  {
1427  checkContextMatch(t1);
1428  checkContextMatch(t2);
1429  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1430  t1.getNativeObject(), t2.getNativeObject()));
1431  }
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 1411 of file Context.java.

1412  {
1413  checkContextMatch(t);
1414  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1415  t.getNativeObject()));
1416  }
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 1439 of file Context.java.

1441  {
1442  checkContextMatch(t1);
1443  checkContextMatch(t2);
1444  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1445  t1.getNativeObject(), t2.getNativeObject()));
1446  }
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 1103 of file Context.java.

1104  {
1105  checkContextMatch(t1);
1106  checkContextMatch(t2);
1107  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1108  t1.getNativeObject(), t2.getNativeObject()));
1109  }
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 1548 of file Context.java.

1550  {
1551  checkContextMatch(t1);
1552  checkContextMatch(t2);
1553  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1554  t1.getNativeObject(), t2.getNativeObject()));
1555  }
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 1228 of file Context.java.

1229  {
1230  checkContextMatch(t1);
1231  checkContextMatch(t2);
1232  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1233  t2.getNativeObject()));
1234  }
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 1254 of file Context.java.

1255  {
1256  checkContextMatch(t1);
1257  checkContextMatch(t2);
1258  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1259  t2.getNativeObject()));
1260  }
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 1347 of file Context.java.

1348  {
1349  checkContextMatch(t1);
1350  checkContextMatch(t2);
1351  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1352  t1.getNativeObject(), t2.getNativeObject()));
1353  }
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 1202 of file Context.java.

1203  {
1204  checkContextMatch(t1);
1205  checkContextMatch(t2);
1206  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1207  t2.getNativeObject()));
1208  }
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 1176 of file Context.java.

1177  {
1178  checkContextMatch(t1);
1179  checkContextMatch(t2);
1180  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1181  t2.getNativeObject()));
1182  }
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 1150 of file Context.java.

1151  {
1152  checkContextMatch(t1);
1153  checkContextMatch(t2);
1154  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1155  t1.getNativeObject(), t2.getNativeObject()));
1156  }
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 1136 of file Context.java.

1137  {
1138  checkContextMatch(t1);
1139  checkContextMatch(t2);
1140  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1141  t1.getNativeObject(), t2.getNativeObject()));
1142  }
BitVecExpr mkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1054 of file Context.java.

1055  {
1056  checkContextMatch(t1);
1057  checkContextMatch(t2);
1058  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1059  t1.getNativeObject(), t2.getNativeObject()));
1060  }
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 1519 of file Context.java.

1521  {
1522  checkContextMatch(t1);
1523  checkContextMatch(t2);
1524  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1525  t1.getNativeObject(), t2.getNativeObject()));
1526  }
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 1533 of file Context.java.

1535  {
1536  checkContextMatch(t1);
1537  checkContextMatch(t2);
1538  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1539  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1540  : false));
1541  }
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 1082 of file Context.java.

1083  {
1084  checkContextMatch(t1);
1085  checkContextMatch(t2);
1086  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1087  t1.getNativeObject(), t2.getNativeObject()));
1088  }
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 1215 of file Context.java.

1216  {
1217  checkContextMatch(t1);
1218  checkContextMatch(t2);
1219  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1220  t2.getNativeObject()));
1221  }
BoolExpr mkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1241 of file Context.java.

1242  {
1243  checkContextMatch(t1);
1244  checkContextMatch(t2);
1245  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1246  t2.getNativeObject()));
1247  }
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 1189 of file Context.java.

1190  {
1191  checkContextMatch(t1);
1192  checkContextMatch(t2);
1193  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1194  t2.getNativeObject()));
1195  }
BoolExpr mkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1163 of file Context.java.

1164  {
1165  checkContextMatch(t1);
1166  checkContextMatch(t2);
1167  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1168  t2.getNativeObject()));
1169  }
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 1118 of file Context.java.

1119  {
1120  checkContextMatch(t1);
1121  checkContextMatch(t2);
1122  return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1123  t1.getNativeObject(), t2.getNativeObject()));
1124  }
BitVecExpr mkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1017 of file Context.java.

1018  {
1019  checkContextMatch(t1);
1020  checkContextMatch(t2);
1021  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1022  t1.getNativeObject(), t2.getNativeObject()));
1023  }
BitVecExpr mkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 978 of file Context.java.

979  {
980  checkContextMatch(t1);
981  checkContextMatch(t2);
982  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
983  t1.getNativeObject(), t2.getNativeObject()));
984  }
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 1272 of file Context.java.

1273  {
1274  checkContextMatch(t1);
1275  checkContextMatch(t2);
1276  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1277  t1.getNativeObject(), t2.getNativeObject()));
1278  }
Expr mkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort

range

and named

name

.

Definition at line 503 of file Context.java.

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

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

Creates a new Constant of sort

range

and named

name

.

Definition at line 518 of file Context.java.

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

Creates a fresh constant from the FuncDecl

f

.

Parameters
fA decl of a 0-arity function

Definition at line 538 of file Context.java.

539  {
540  return mkApp(f, (Expr[]) null);
541  }
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:610
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 1673 of file Context.java.

1674  {
1675  checkContextMatch(domain);
1676  checkContextMatch(v);
1677  return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1678  domain.getNativeObject(), v.getNativeObject()));
1679  }
FuncDecl mkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 446 of file Context.java.

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

Creates a new constant function declaration.

Definition at line 456 of file Context.java.

457  {
458  checkContextMatch(range);
459  return new FuncDecl(this, mkSymbol(name), null, range);
460  }
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 655 of file Context.java.

656  {
657  checkContextMatch(args);
658  return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length,
659  AST.arrayToNative(args)));
660  }
ArithExpr mkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 / t2

.

Definition at line 783 of file Context.java.

784  {
785  checkContextMatch(t1);
786  checkContextMatch(t2);
787  return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
788  t1.getNativeObject(), t2.getNativeObject()));
789  }
ArrayExpr mkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 1728 of file Context.java.

1729  {
1730  checkContextMatch(domain);
1731  return (ArrayExpr)Expr.create(this,
1732  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1733  }
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(name, values, ctx=None)
Definition: z3py.py:4458
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(name, values, ctx=None)
Definition: z3py.py:4458
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 644 of file Context.java.

645  {
646  checkContextMatch(x);
647  checkContextMatch(y);
648  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
649  y.getNativeObject()));
650  }
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 2055 of file Context.java.

Referenced by Context.mkQuantifier().

2058  {
2059 
2060  return new Quantifier(this, false, sorts, names, body, weight,
2061  patterns, noPatterns, quantifierID, skolemID);
2062  }
Quantifier mkExists ( Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create an existential Quantifier.

Definition at line 2067 of file Context.java.

2070  {
2071 
2072  return new Quantifier(this, false, boundConstants, body, weight,
2073  patterns, noPatterns, quantifierID, skolemID);
2074  }
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 1288 of file Context.java.

1290  {
1291  checkContextMatch(t);
1292  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1293  t.getNativeObject()));
1294  }
BoolExpr mkFalse ( )
inline

The false Term.

Definition at line 628 of file Context.java.

Referenced by Context.mkBool().

629  {
630  return new BoolExpr(this, Native.mkFalse(nCtx()));
631  }
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  }
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6389
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  }
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6389
IntSymbol mkSymbol(int i)
Definition: Context.java:72
Fixedpoint mkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 2794 of file Context.java.

2795  {
2796  return new Fixedpoint(this);
2797  }
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 2030 of file Context.java.

Referenced by Context.mkQuantifier().

2033  {
2034 
2035  return new Quantifier(this, true, sorts, names, body, weight, patterns,
2036  noPatterns, quantifierID, skolemID);
2037  }
Quantifier mkForall ( Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a universal Quantifier.

Definition at line 2042 of file Context.java.

2045  {
2046 
2047  return new Quantifier(this, true, boundConstants, body, weight,
2048  patterns, noPatterns, quantifierID, skolemID);
2049  }
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 3088 of file Context.java.

3089  {
3090  return mkFPNumeral(v, s);
3091  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3029
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 3099 of file Context.java.

3100  {
3101  return mkFPNumeral(v, s);
3102  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3029
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 3111 of file Context.java.

3112  {
3113  return mkFPNumeral(v, s);
3114  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3029
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 3124 of file Context.java.

3125  {
3126  return mkFPNumeral(sgn, sig, exp, s);
3127  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3029
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 3137 of file Context.java.

3138  {
3139  return mkFPNumeral(sgn, sig, exp, s);
3140  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3029
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 3422 of file Context.java.

3423  {
3424  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3425  }
FPExpr mkFPAbs ( FPExpr  t)
inline

Floating-point absolute value

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3148 of file Context.java.

3149  {
3150  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3151  }
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 3170 of file Context.java.

3171  {
3172  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3173  }
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 3206 of file Context.java.

3207  {
3208  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3209  }
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 3334 of file Context.java.

3335  {
3336  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3337  }
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 3221 of file Context.java.

3222  {
3223  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3224  }
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 3310 of file Context.java.

3311  {
3312  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3313  }
BoolExpr mkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3321 of file Context.java.

3322  {
3323  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3324  }
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 3007 of file Context.java.

3008  {
3009  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3010  }
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 3374 of file Context.java.

3375  {
3376  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3377  }
BoolExpr mkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3384 of file Context.java.

3385  {
3386  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3387  }
BoolExpr mkFPIsNegative ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3394 of file Context.java.

3395  {
3396  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3397  }
BoolExpr mkFPIsNormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3344 of file Context.java.

3345  {
3346  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3347  }
BoolExpr mkFPIsPositive ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3404 of file Context.java.

3405  {
3406  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3407  }
BoolExpr mkFPIsSubnormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3354 of file Context.java.

3355  {
3356  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3357  }
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 3364 of file Context.java.

3365  {
3366  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3367  }
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 3288 of file Context.java.

3289  {
3290  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3291  }
BoolExpr mkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3299 of file Context.java.

3300  {
3301  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3302  }
FPExpr mkFPMax ( FPExpr  t1,
FPExpr  t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3277 of file Context.java.

3278  {
3279  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3280  }
FPExpr mkFPMin ( FPExpr  t1,
FPExpr  t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3266 of file Context.java.

3267  {
3268  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3269  }
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 3194 of file Context.java.

3195  {
3196  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3197  }
FPNum mkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 2996 of file Context.java.

2997  {
2998  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
2999  }
FPExpr mkFPNeg ( FPExpr  t)
inline

Floating-point negation

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3158 of file Context.java.

3159  {
3160  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3161  }
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 3029 of file Context.java.

Referenced by Context.mkFP().

3030  {
3031  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3032  }
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 3040 of file Context.java.

3041  {
3042  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3043  }
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 3051 of file Context.java.

3052  {
3053  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3054  }
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 3064 of file Context.java.

3065  {
3066  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3067  }
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 3077 of file Context.java.

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

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3243 of file Context.java.

3244  {
3245  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3246  }
FPRMNum mkFPRNA ( )
inline

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

Exceptions
Z3Exception

Definition at line 2848 of file Context.java.

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

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

Exceptions
Z3Exception

Definition at line 2830 of file Context.java.

2831  {
2832  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
2833  }
FPRMSort mkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Exceptions
Z3Exception

Definition at line 2812 of file Context.java.

2813  {
2814  return new FPRMSort(this);
2815  }
FPRMNum mkFPRoundNearestTiesToAway ( )
inline

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

Exceptions
Z3Exception

Definition at line 2839 of file Context.java.

2840  {
2841  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
2842  }
FPRMExpr mkFPRoundNearestTiesToEven ( )
inline

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

Exceptions
Z3Exception

Definition at line 2821 of file Context.java.

2822  {
2823  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
2824  }
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 3255 of file Context.java.

3256  {
3257  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3258  }
FPRMNum mkFPRoundTowardNegative ( )
inline

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

Exceptions
Z3Exception

Definition at line 2875 of file Context.java.

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

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

Exceptions
Z3Exception

Definition at line 2857 of file Context.java.

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

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

Exceptions
Z3Exception

Definition at line 2893 of file Context.java.

2894  {
2895  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
2896  }
FPRMNum mkFPRTN ( )
inline

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

Exceptions
Z3Exception

Definition at line 2884 of file Context.java.

2885  {
2886  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
2887  }
FPRMNum mkFPRTP ( )
inline

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

Exceptions
Z3Exception

Definition at line 2866 of file Context.java.

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

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

Exceptions
Z3Exception

Definition at line 2902 of file Context.java.

2903  {
2904  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
2905  }
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 2913 of file Context.java.

2914  {
2915  return new FPSort(this, ebits, sbits);
2916  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort mkFPSort128 ( )
inline

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

Exceptions
Z3Exception

Definition at line 2985 of file Context.java.

2986  {
2987  return new FPSort(this, Native.mkFpaSort128(nCtx()));
2988  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort mkFPSort16 ( )
inline

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

Exceptions
Z3Exception

Definition at line 2931 of file Context.java.

2932  {
2933  return new FPSort(this, Native.mkFpaSort16(nCtx()));
2934  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort mkFPSort32 ( )
inline

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

Exceptions
Z3Exception

Definition at line 2949 of file Context.java.

2950  {
2951  return new FPSort(this, Native.mkFpaSort32(nCtx()));
2952  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort mkFPSort64 ( )
inline

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

Exceptions
Z3Exception

Definition at line 2967 of file Context.java.

2968  {
2969  return new FPSort(this, Native.mkFpaSort64(nCtx()));
2970  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort mkFPSortDouble ( )
inline

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

Exceptions
Z3Exception

Definition at line 2958 of file Context.java.

2959  {
2960  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
2961  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort mkFPSortHalf ( )
inline

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

Exceptions
Z3Exception

Definition at line 2922 of file Context.java.

2923  {
2924  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
2925  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort mkFPSortQuadruple ( )
inline

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

Exceptions
Z3Exception

Definition at line 2976 of file Context.java.

2977  {
2978  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
2979  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort mkFPSortSingle ( )
inline

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

Exceptions
Z3Exception

Definition at line 2940 of file Context.java.

2941  {
2942  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
2943  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPExpr mkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term
Exceptions
Z3Exception

Definition at line 3232 of file Context.java.

3233  {
3234  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3235  }
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 3182 of file Context.java.

3183  {
3184  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3185  }
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 3523 of file Context.java.

3524  {
3525  if (signed)
3526  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3527  else
3528  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3529  }
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 3438 of file Context.java.

3439  {
3440  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3441  }
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 3454 of file Context.java.

3455  {
3456  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3457  }
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 3470 of file Context.java.

3471  {
3472  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3473  }
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 3488 of file Context.java.

3489  {
3490  if (signed)
3491  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3492  else
3493  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3494  }
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 3506 of file Context.java.

3507  {
3508  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3509  }
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 3573 of file Context.java.

3574  {
3575  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3576  }
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 3555 of file Context.java.

3556  {
3557  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3558  }
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 3540 of file Context.java.

3541  {
3542  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3543  }
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 3018 of file Context.java.

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

Creates a fresh Constant of sort

range

and a name prefixed with

prefix

.

Definition at line 527 of file Context.java.

528  {
529  checkContextMatch(range);
530  return Expr.create(this,
531  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
532  }
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 468 of file Context.java.

470  {
471  checkContextMatch(range);
472  return new FuncDecl(this, prefix, null, range);
473  }
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 435 of file Context.java.

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

Create the full set.

Definition at line 1738 of file Context.java.

1739  {
1740  checkContextMatch(domain);
1741  return (ArrayExpr)Expr.create(this,
1742  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1743  }
FuncDecl mkFuncDecl ( Symbol  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 384 of file Context.java.

386  {
387  checkContextMatch(name);
388  checkContextMatch(domain);
389  checkContextMatch(range);
390  return new FuncDecl(this, name, domain, range);
391  }
FuncDecl mkFuncDecl ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 396 of file Context.java.

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

Creates a new function declaration.

Definition at line 409 of file Context.java.

411  {
412  checkContextMatch(domain);
413  checkContextMatch(range);
414  return new FuncDecl(this, mkSymbol(name), domain, range);
415  }
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 420 of file Context.java.

422  {
423  checkContextMatch(domain);
424  checkContextMatch(range);
425  Sort[] q = new Sort[] { domain };
426  return new FuncDecl(this, mkSymbol(name), q, range);
427  }
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 866 of file Context.java.

867  {
868  checkContextMatch(t1);
869  checkContextMatch(t2);
870  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
871  t2.getNativeObject()));
872  }
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 2345 of file Context.java.

2347  {
2348  return new Goal(this, models, unsatCores, proofs);
2349  }
BoolExpr mkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &gt; t2

Definition at line 855 of file Context.java.

856  {
857  checkContextMatch(t1);
858  checkContextMatch(t2);
859  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
860  t2.getNativeObject()));
861  }
BoolExpr mkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 iff t2

.

Definition at line 690 of file Context.java.

691  {
692  checkContextMatch(t1);
693  checkContextMatch(t2);
694  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
695  t2.getNativeObject()));
696  }
BoolExpr mkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 -> t2

.

Definition at line 701 of file Context.java.

702  {
703  checkContextMatch(t1);
704  checkContextMatch(t2);
705  return new BoolExpr(this, Native.mkImplies(nCtx(),
706  t1.getNativeObject(), t2.getNativeObject()));
707  }
IntNum mkInt ( String  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 1948 of file Context.java.

1949  {
1950 
1951  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
1952  .getNativeObject()));
1953  }
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 1961 of file Context.java.

1962  {
1963 
1964  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
1965  .getNativeObject()));
1966  }
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 1974 of file Context.java.

1975  {
1976 
1977  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
1978  .getNativeObject()));
1979  }
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 1457 of file Context.java.

1458  {
1459  checkContextMatch(t);
1460  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1461  t.getNativeObject()));
1462  }
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 884 of file Context.java.

885  {
886  checkContextMatch(t);
887  return new RealExpr(this,
888  Native.mkInt2real(nCtx(), t.getNativeObject()));
889  }
IntExpr mkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 562 of file Context.java.

563  {
564  return (IntExpr) mkConst(name, getIntSort());
565  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:503
IntExpr mkIntConst ( String  name)
inline

Creates an integer constant.

Definition at line 570 of file Context.java.

571  {
572  return (IntExpr) mkConst(name, getIntSort());
573  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:503
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(ctx=None)
Definition: z3py.py:2639
BoolExpr mkIsInteger ( RealExpr  t)
inline

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

Definition at line 906 of file Context.java.

907  {
908  checkContextMatch(t);
909  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
910  }
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 678 of file Context.java.

679  {
680  checkContextMatch(t1);
681  checkContextMatch(t2);
682  checkContextMatch(t3);
683  return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
684  t2.getNativeObject(), t3.getNativeObject()));
685  }
BoolExpr mkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &lt;= t2

Definition at line 844 of file Context.java.

845  {
846  checkContextMatch(t1);
847  checkContextMatch(t2);
848  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
849  t2.getNativeObject()));
850  }
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 833 of file Context.java.

834  {
835  checkContextMatch(t1);
836  checkContextMatch(t2);
837  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
838  t2.getNativeObject()));
839  }
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 1694 of file Context.java.

1695  {
1696  checkContextMatch(f);
1697  checkContextMatch(args);
1698  return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1699  f.getNativeObject(), AST.arrayLength(args),
1700  AST.arrayToNative(args)));
1701  }
IntExpr mkMod ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing

t1 mod t2

. Remarks: The arguments must have int type.

Definition at line 796 of file Context.java.

797  {
798  checkContextMatch(t1);
799  checkContextMatch(t2);
800  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
801  t2.getNativeObject()));
802  }
ArithExpr mkMul ( ArithExpr...  t)
inline

Create an expression representing

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

.

Definition at line 753 of file Context.java.

754  {
755  checkContextMatch(t);
756  return (ArithExpr) Expr.create(this,
757  Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t)));
758  }
BoolExpr mkNot ( BoolExpr  a)
inline

Mk an expression representing

not(a)

.

Definition at line 665 of file Context.java.

666  {
667  checkContextMatch(a);
668  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
669  }
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 1848 of file Context.java.

Referenced by Context.mkBV().

1849  {
1850  checkContextMatch(ty);
1851  return Expr.create(this,
1852  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
1853  }
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 1865 of file Context.java.

1866  {
1867  checkContextMatch(ty);
1868  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
1869  }
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 1881 of file Context.java.

1882  {
1883  checkContextMatch(ty);
1884  return Expr.create(this,
1885  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
1886  }
Optimize mkOptimize ( )
inline

Create a Optimize context.

Definition at line 2802 of file Context.java.

2803  {
2804  return new Optimize(this);
2805  }
BoolExpr mkOr ( BoolExpr...  t)
inline

Create an expression representing

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

.

Definition at line 733 of file Context.java.

734  {
735  checkContextMatch(t);
736  return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length,
737  AST.arrayToNative(t)));
738  }
Params mkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2354 of file Context.java.

2355  {
2356  return new Params(this);
2357  }
Pattern mkPattern ( Expr...  terms)
inline

Create a quantifier pattern.

Definition at line 489 of file Context.java.

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

Create an expression representing

t1 ^ t2

.

Definition at line 820 of file Context.java.

821  {
822  checkContextMatch(t1);
823  checkContextMatch(t2);
824  return (ArithExpr) Expr.create(
825  this,
826  Native.mkPower(nCtx(), t1.getNativeObject(),
827  t2.getNativeObject()));
828  }
Probe mkProbe ( String  name)
inline

Creates a new Probe.

Definition at line 2626 of file Context.java.

2627  {
2628  return new Probe(this, name);
2629  }
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 2079 of file Context.java.

2083  {
2084 
2085  if (universal)
2086  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2087  quantifierID, skolemID);
2088  else
2089  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2090  quantifierID, skolemID);
2091  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2055
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2030
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 2096 of file Context.java.

2099  {
2100 
2101  if (universal)
2102  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2103  quantifierID, skolemID);
2104  else
2105  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2106  quantifierID, skolemID);
2107  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2055
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2030
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 1897 of file Context.java.

1898  {
1899  if (den == 0)
1900  throw new Z3Exception("Denominator is zero");
1901 
1902  return new RatNum(this, Native.mkReal(nCtx(), num, den));
1903  }
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 1911 of file Context.java.

1912  {
1913 
1914  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
1915  .getNativeObject()));
1916  }
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 1924 of file Context.java.

1925  {
1926 
1927  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
1928  .getNativeObject()));
1929  }
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 1937 of file Context.java.

1938  {
1939 
1940  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
1941  .getNativeObject()));
1942  }
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 897 of file Context.java.

898  {
899  checkContextMatch(t);
900  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
901  }
RealExpr mkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 578 of file Context.java.

579  {
580  return (RealExpr) mkConst(name, getRealSort());
581  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:503
RealExpr mkRealConst ( String  name)
inline

Creates a real constant.

Definition at line 586 of file Context.java.

587  {
588  return (RealExpr) mkConst(name, getRealSort());
589  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:503
RealSort mkRealSort ( )
inline

Create a real sort.

Definition at line 168 of file Context.java.

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

Create an expression representing

t1 rem t2

. Remarks: The arguments must have int type.

Definition at line 809 of file Context.java.

810  {
811  checkContextMatch(t1);
812  checkContextMatch(t2);
813  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
814  t2.getNativeObject()));
815  }
BitVecExpr mkRepeat ( int  i,
BitVecExpr  t 
)
inline

Bit-vector repetition. Remarks: The argument

t

must have a bit-vector sort.

Definition at line 1329 of file Context.java.

1330  {
1331  checkContextMatch(t);
1332  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1333  t.getNativeObject()));
1334  }
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 1629 of file Context.java.

1630  {
1631  checkContextMatch(a);
1632  checkContextMatch(i);
1633  return Expr.create(
1634  this,
1635  Native.mkSelect(nCtx(), a.getNativeObject(),
1636  i.getNativeObject()));
1637  }
ArrayExpr mkSetAdd ( ArrayExpr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 1748 of file Context.java.

1749  {
1750  checkContextMatch(set);
1751  checkContextMatch(element);
1752  return (ArrayExpr)Expr.create(this,
1753  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1754  element.getNativeObject()));
1755  }
ArrayExpr mkSetComplement ( ArrayExpr  arg)
inline

Take the complement of a set.

Definition at line 1806 of file Context.java.

1807  {
1808  checkContextMatch(arg);
1809  return (ArrayExpr)Expr.create(this,
1810  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1811  }
ArrayExpr mkSetDel ( ArrayExpr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 1760 of file Context.java.

1761  {
1762  checkContextMatch(set);
1763  checkContextMatch(element);
1764  return (ArrayExpr)Expr.create(this,
1765  Native.mkSetDel(nCtx(), set.getNativeObject(),
1766  element.getNativeObject()));
1767  }
ArrayExpr mkSetDifference ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Take the difference between two sets.

Definition at line 1794 of file Context.java.

1795  {
1796  checkContextMatch(arg1);
1797  checkContextMatch(arg2);
1798  return (ArrayExpr)Expr.create(this,
1799  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1800  arg2.getNativeObject()));
1801  }
ArrayExpr mkSetIntersection ( ArrayExpr...  args)
inline

Take the intersection of a list of sets.

Definition at line 1783 of file Context.java.

1784  {
1785  checkContextMatch(args);
1786  return (ArrayExpr)Expr.create(this,
1787  Native.mkSetIntersect(nCtx(), (int) args.length,
1788  AST.arrayToNative(args)));
1789  }
BoolExpr mkSetMembership ( Expr  elem,
ArrayExpr  set 
)
inline

Check for set membership.

Definition at line 1816 of file Context.java.

1817  {
1818  checkContextMatch(elem);
1819  checkContextMatch(set);
1820  return (BoolExpr) Expr.create(this,
1821  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1822  set.getNativeObject()));
1823  }
SetSort mkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 1719 of file Context.java.

1720  {
1721  checkContextMatch(ty);
1722  return new SetSort(this, ty);
1723  }
BoolExpr mkSetSubset ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 1828 of file Context.java.

1829  {
1830  checkContextMatch(arg1);
1831  checkContextMatch(arg2);
1832  return (BoolExpr) Expr.create(this,
1833  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1834  arg2.getNativeObject()));
1835  }
ArrayExpr mkSetUnion ( ArrayExpr...  args)
inline

Take the union of a list of sets.

Definition at line 1772 of file Context.java.

1773  {
1774  checkContextMatch(args);
1775  return (ArrayExpr)Expr.create(this,
1776  Native.mkSetUnion(nCtx(), (int) args.length,
1777  AST.arrayToNative(args)));
1778  }
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 1303 of file Context.java.

1304  {
1305  checkContextMatch(t);
1306  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1307  t.getNativeObject()));
1308  }
Solver mkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 2773 of file Context.java.

2774  {
2775  return new Solver(this, Native.mkSimpleSolver(nCtx()));
2776  }
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 2739 of file Context.java.

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

2740  {
2741  return mkSolver((Symbol) null);
2742  }
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 2751 of file Context.java.

2752  {
2753 
2754  if (logic == null)
2755  return new Solver(this, Native.mkSolver(nCtx()));
2756  else
2757  return new Solver(this, Native.mkSolverForLogic(nCtx(),
2758  logic.getNativeObject()));
2759  }
Solver mkSolver ( String  logic)
inline

Creates a new (incremental) solver.

See also
mkSolver(Symbol)

Definition at line 2765 of file Context.java.

2766  {
2767  return mkSolver(mkSymbol(logic));
2768  }
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 2784 of file Context.java.

2785  {
2786 
2787  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
2788  t.getNativeObject()));
2789  }
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 1655 of file Context.java.

1656  {
1657  checkContextMatch(a);
1658  checkContextMatch(i);
1659  checkContextMatch(v);
1660  return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1661  i.getNativeObject(), v.getNativeObject()));
1662  }
ArithExpr mkSub ( ArithExpr...  t)
inline

Create an expression representing

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

.

Definition at line 763 of file Context.java.

764  {
765  checkContextMatch(t);
766  return (ArithExpr) Expr.create(this,
767  Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t)));
768  }
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(), Context.mkSymbol(), 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 2392 of file Context.java.

Referenced by Goal.simplify().

2393  {
2394  return new Tactic(this, name);
2395  }
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 1709 of file Context.java.

1710  {
1711  checkContextMatch(array);
1712  return Expr.create(this,
1713  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1714  }
BoolExpr mkTrue ( )
inline

The true Term.

Definition at line 620 of file Context.java.

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

621  {
622  return new BoolExpr(this, Native.mkTrue(nCtx()));
623  }
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 773 of file Context.java.

774  {
775  checkContextMatch(t);
776  return (ArithExpr) Expr.create(this,
777  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
778  }
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
Expr MkUpdateField ( FuncDecl  field,
Expr  t,
Expr  v 
) throws Z3Exception
inline

Update a datatype field at expression t with value v. The function performs a record update at t. The field that is passed in as argument is updated with value v, the remainig fields of t are unchanged.

Definition at line 370 of file Context.java.

372  {
373  return Expr.create
374  (this,
375  Native.datatypeUpdateField
376  (nCtx(), field.getNativeObject(),
377  t.getNativeObject(), v.getNativeObject()));
378  }
BoolExpr mkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 xor t2

.

Definition at line 712 of file Context.java.

713  {
714  checkContextMatch(t1);
715  checkContextMatch(t2);
716  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
717  t2.getNativeObject()));
718  }
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 1317 of file Context.java.

1318  {
1319  checkContextMatch(t);
1320  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1321  t.getNativeObject()));
1322  }
Probe not ( Probe  p)
inline

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

p

does not evaluate to "true".

Definition at line 2726 of file Context.java.

2727  {
2728  checkContextMatch(p);
2729  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2730  }
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 2715 of file Context.java.

2716  {
2717  checkContextMatch(p1);
2718  checkContextMatch(p2);
2719  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
2720  p2.getNativeObject()));
2721  }
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 2442 of file Context.java.

2443  {
2444  checkContextMatch(t1);
2445  checkContextMatch(t2);
2446  return new Tactic(this, Native.tacticOrElse(nCtx(),
2447  t1.getNativeObject(), t2.getNativeObject()));
2448  }
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 2575 of file Context.java.

2576  {
2577  checkContextMatch(t1);
2578  checkContextMatch(t2);
2579  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2580  t1.getNativeObject(), t2.getNativeObject()));
2581  }
Tactic parOr ( Tactic...  t)
inline

Create a tactic that applies the given tactics in parallel.

Definition at line 2564 of file Context.java.

2565  {
2566  checkContextMatch(t);
2567  return new Tactic(this, Native.tacticParOr(nCtx(),
2568  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2569  }
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 2317 of file Context.java.

2320  {
2321 
2322  int csn = Symbol.arrayLength(sortNames);
2323  int cs = Sort.arrayLength(sorts);
2324  int cdn = Symbol.arrayLength(declNames);
2325  int cd = AST.arrayLength(decls);
2326  if (csn != cs || cdn != cd)
2327  throw new Z3Exception("Argument size mismatch");
2328  return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
2329  fileName, AST.arrayLength(sorts),
2330  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2331  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2332  AST.arrayToNative(decls)));
2333  }
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 2296 of file Context.java.

2299  {
2300 
2301  int csn = Symbol.arrayLength(sortNames);
2302  int cs = Sort.arrayLength(sorts);
2303  int cdn = Symbol.arrayLength(declNames);
2304  int cd = AST.arrayLength(decls);
2305  if (csn != cs || cdn != cd)
2306  throw new Z3Exception("Argument size mismatch");
2307  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2308  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2309  AST.arrayToNative(sorts), AST.arrayLength(decls),
2310  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2311  }
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 2179 of file Context.java.

2182  {
2183  int csn = Symbol.arrayLength(sortNames);
2184  int cs = Sort.arrayLength(sorts);
2185  int cdn = Symbol.arrayLength(declNames);
2186  int cd = AST.arrayLength(decls);
2187  if (csn != cs || cdn != cd)
2188  throw new Z3Exception("Argument size mismatch");
2189  Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
2190  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2191  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2192  AST.arrayToNative(decls));
2193  }
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 2160 of file Context.java.

2162  {
2163  int csn = Symbol.arrayLength(sortNames);
2164  int cs = Sort.arrayLength(sorts);
2165  int cdn = Symbol.arrayLength(declNames);
2166  int cd = AST.arrayLength(decls);
2167  if (csn != cs || cdn != cd)
2168  throw new Z3Exception("Argument size mismatch");
2169  Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
2170  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2171  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2172  AST.arrayToNative(decls));
2173  }
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 2495 of file Context.java.

2496  {
2497  checkContextMatch(t);
2498  return new Tactic(this, Native.tacticRepeat(nCtx(),
2499  t.getNativeObject(), max));
2500  }
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 2123 of file Context.java.

Referenced by Context.updateParamValue().

2124  {
2125  Native.setAstPrintMode(nCtx(), value.toInt());
2126  }
String SimplifyHelp ( )
inline

Return a string describing all available parameters to

Expr.Simplify

.

Definition at line 3615 of file Context.java.

3616  {
3617  return Native.simplifyGetHelp(nCtx());
3618  }
Tactic skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 2505 of file Context.java.

2506  {
2507  return new Tactic(this, Native.tacticSkip(nCtx()));
2508  }
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 2432 of file Context.java.

2433  {
2434  return andThen(t1, t2, ts);
2435  }
Tactic andThen(Tactic t1, Tactic t2, Tactic...ts)
Definition: Context.java:2401
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 2456 of file Context.java.

2457  {
2458  checkContextMatch(t);
2459  return new Tactic(this, Native.tacticTryFor(nCtx(),
2460  t.getNativeObject(), ms));
2461  }
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 3606 of file Context.java.

3607  {
3608  return a.getNativeObject();
3609  }
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 3636 of file Context.java.

3637  {
3638  Native.updateParamValue(nCtx(), id, value);
3639  }
Tactic usingParams ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

.

Definition at line 2542 of file Context.java.

Referenced by Context.with().

2543  {
2544  checkContextMatch(t);
2545  checkContextMatch(p);
2546  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2547  t.getNativeObject(), p.getNativeObject()));
2548  }
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 2469 of file Context.java.

2470  {
2471  checkContextMatch(t);
2472  checkContextMatch(p);
2473  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2474  t.getNativeObject()));
2475  }
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 2556 of file Context.java.

2557  {
2558  return usingParams(t, p);
2559  }
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2542
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 3589 of file Context.java.

3590  {
3591  return AST.create(this, nativeObject);
3592  }

Field Documentation

long m_refCount = 0
protected

Definition at line 3764 of file Context.java.

Referenced by Z3Object.dispose().