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

Public Member Functions

 Context ()
 
 Context (Map< String, String > settings)
 
IntSymbol mkSymbol (int i)
 
StringSymbol mkSymbol (String name)
 
BoolSort getBoolSort ()
 
IntSort getIntSort ()
 
RealSort getRealSort ()
 
BoolSort mkBoolSort ()
 
SeqSort< BitVecSortgetStringSort ()
 
UninterpretedSort mkUninterpretedSort (Symbol s)
 
UninterpretedSort mkUninterpretedSort (String str)
 
IntSort mkIntSort ()
 
RealSort mkRealSort ()
 
BitVecSort mkBitVecSort (int size)
 
SeqSort< BitVecSortmkStringSort ()
 
TupleSort mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
 
DatatypeSort< Object >[] mkDatatypeSorts (Symbol[] names, Constructor< Object >[][] c)
 
DatatypeSort< Object >[] mkDatatypeSorts (String[] names, Constructor< Object >[][] c)
 
Pattern mkPattern (Expr<?>... terms)
 
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)
 
BoolExpr mkTrue ()
 
BoolExpr mkFalse ()
 
BoolExpr mkBool (boolean value)
 
BoolExpr mkNot (Expr< BoolSort > a)
 
BoolExpr mkIff (Expr< BoolSort > t1, Expr< BoolSort > t2)
 
BoolExpr mkImplies (Expr< BoolSort > t1, Expr< BoolSort > t2)
 
BoolExpr mkXor (Expr< BoolSort > t1, Expr< BoolSort > t2)
 
BoolExpr mkAnd (Expr< BoolSort >... t)
 
BoolExpr mkOr (Expr< BoolSort >... t)
 
IntExpr mkMod (Expr< IntSort > t1, Expr< IntSort > t2)
 
IntExpr mkRem (Expr< IntSort > t1, Expr< IntSort > t2)
 
RealExpr mkInt2Real (Expr< IntSort > t)
 
IntExpr mkReal2Int (Expr< RealSort > t)
 
BoolExpr mkIsInteger (Expr< RealSort > t)
 
BitVecExpr mkBVNot (Expr< BitVecSort > t)
 
BitVecExpr mkBVRedAND (Expr< BitVecSort > t)
 
BitVecExpr mkBVRedOR (Expr< BitVecSort > t)
 
BitVecExpr mkBVAND (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVOR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVXOR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVNAND (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVNOR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVXNOR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVNeg (Expr< BitVecSort > t)
 
BitVecExpr mkBVAdd (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVSub (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVMul (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVUDiv (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVSDiv (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVURem (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVSRem (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVSMod (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVULT (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSLT (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVULE (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSLE (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVUGE (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSGE (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVUGT (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSGT (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkConcat (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkExtract (int high, int low, Expr< BitVecSort > t)
 
BitVecExpr mkSignExt (int i, Expr< BitVecSort > t)
 
BitVecExpr mkZeroExt (int i, Expr< BitVecSort > t)
 
BitVecExpr mkRepeat (int i, Expr< BitVecSort > t)
 
BitVecExpr mkBVSHL (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVLSHR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVASHR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVRotateLeft (int i, Expr< BitVecSort > t)
 
BitVecExpr mkBVRotateRight (int i, Expr< BitVecSort > t)
 
BitVecExpr mkBVRotateLeft (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVRotateRight (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkInt2BV (int n, Expr< IntSort > t)
 
IntExpr mkBV2Int (Expr< BitVecSort > t, boolean signed)
 
BoolExpr mkBVAddNoOverflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
 
BoolExpr mkBVAddNoUnderflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSubNoOverflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSubNoUnderflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
 
BoolExpr mkBVSDivNoOverflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVNegNoOverflow (Expr< BitVecSort > t)
 
BoolExpr mkBVMulNoOverflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
 
BoolExpr mkBVMulNoUnderflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
SeqExpr< BitVecSortmkString (String s)
 
SeqExpr< BitVecSortintToString (Expr< IntSort > e)
 
IntExpr stringToInt (Expr< SeqSort< BitVecSort >> e)
 
BoolExpr mkAtMost (Expr< BoolSort >[] args, int k)
 
BoolExpr mkAtLeast (Expr< BoolSort >[] args, int k)
 
BoolExpr mkPBLe (int[] coeffs, Expr< BoolSort >[] args, int k)
 
BoolExpr mkPBGe (int[] coeffs, Expr< BoolSort >[] args, int k)
 
BoolExpr mkPBEq (int[] coeffs, Expr< BoolSort >[] args, int k)
 
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< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkForall (Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkExists (Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkExists (Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkQuantifier (boolean universal, Expr<?>[] boundConstants, Expr< BoolSort > 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, Expr< BoolSort >[] assumptions, Expr< BoolSort > formula)
 
BoolExpr[] parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
 
BoolExpr[] parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
 
Goal mkGoal (boolean models, boolean unsatCores, boolean proofs)
 
Params mkParams ()
 
int getNumTactics ()
 
String[] getTacticNames ()
 
String getTacticDescription (String name)
 
Tactic mkTactic (String name)
 
Tactic andThen (Tactic t1, Tactic t2, Tactic... ts)
 
Tactic then (Tactic t1, Tactic t2, Tactic... ts)
 
Tactic orElse (Tactic t1, Tactic t2)
 
Tactic tryFor (Tactic t, int ms)
 
Tactic when (Probe p, Tactic t)
 
Tactic cond (Probe p, Tactic t1, Tactic t2)
 
Tactic repeat (Tactic t, int max)
 
Tactic skip ()
 
Tactic fail ()
 
Tactic failIf (Probe p)
 
Tactic failIfNotDecided ()
 
Tactic usingParams (Tactic t, Params p)
 
Tactic with (Tactic t, Params p)
 
Tactic parOr (Tactic... t)
 
Tactic parAndThen (Tactic t1, Tactic t2)
 
void interrupt ()
 
int getNumProbes ()
 
String[] getProbeNames ()
 
String getProbeDescription (String name)
 
Probe mkProbe (String name)
 
Probe constProbe (double val)
 
Probe lt (Probe p1, Probe p2)
 
Probe gt (Probe p1, Probe p2)
 
Probe le (Probe p1, Probe p2)
 
Probe ge (Probe p1, Probe p2)
 
Probe eq (Probe p1, Probe p2)
 
Probe and (Probe p1, Probe p2)
 
Probe or (Probe p1, Probe p2)
 
Probe not (Probe p)
 
Solver mkSolver ()
 
Solver mkSolver (Symbol logic)
 
Solver mkSolver (String logic)
 
Solver mkSimpleSolver ()
 
Solver mkSolver (Tactic t)
 
Fixedpoint mkFixedpoint ()
 
Optimize mkOptimize ()
 
FPRMSort mkFPRoundingModeSort ()
 
FPRMExpr mkFPRoundNearestTiesToEven ()
 
FPRMNum mkFPRNE ()
 
FPRMNum mkFPRoundNearestTiesToAway ()
 
FPRMNum mkFPRNA ()
 
FPRMNum mkFPRoundTowardPositive ()
 
FPRMNum mkFPRTP ()
 
FPRMNum mkFPRoundTowardNegative ()
 
FPRMNum mkFPRTN ()
 
FPRMNum mkFPRoundTowardZero ()
 
FPRMNum mkFPRTZ ()
 
FPSort mkFPSort (int ebits, int sbits)
 
FPSort mkFPSortHalf ()
 
FPSort mkFPSort16 ()
 
FPSort mkFPSortSingle ()
 
FPSort mkFPSort32 ()
 
FPSort mkFPSortDouble ()
 
FPSort mkFPSort64 ()
 
FPSort mkFPSortQuadruple ()
 
FPSort mkFPSort128 ()
 
FPNum mkFPNaN (FPSort s)
 
FPNum mkFPInf (FPSort s, boolean negative)
 
FPNum mkFPZero (FPSort s, boolean negative)
 
FPNum mkFPNumeral (float v, FPSort s)
 
FPNum mkFPNumeral (double v, FPSort s)
 
FPNum mkFPNumeral (int v, FPSort s)
 
FPNum mkFPNumeral (boolean sgn, int exp, int sig, FPSort s)
 
FPNum mkFPNumeral (boolean sgn, long exp, long sig, FPSort s)
 
FPNum mkFP (float v, FPSort s)
 
FPNum mkFP (double v, FPSort s)
 
FPNum mkFP (int v, FPSort s)
 
FPNum mkFP (boolean sgn, int exp, int sig, FPSort s)
 
FPNum mkFP (boolean sgn, long exp, long sig, FPSort s)
 
FPExpr mkFPAbs (Expr< FPSort > t)
 
FPExpr mkFPNeg (Expr< FPSort > t)
 
FPExpr mkFPAdd (Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPSub (Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPMul (Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPDiv (Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPFMA (Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2, Expr< FPSort > t3)
 
FPExpr mkFPSqrt (Expr< FPRMSort > rm, Expr< FPSort > t)
 
FPExpr mkFPRem (Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPRoundToIntegral (Expr< FPRMSort > rm, Expr< FPSort > t)
 
FPExpr mkFPMin (Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPMax (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPLEq (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPLt (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPGEq (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPGt (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPEq (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPIsNormal (Expr< FPSort > t)
 
BoolExpr mkFPIsSubnormal (Expr< FPSort > t)
 
BoolExpr mkFPIsZero (Expr< FPSort > t)
 
BoolExpr mkFPIsInfinite (Expr< FPSort > t)
 
BoolExpr mkFPIsNaN (Expr< FPSort > t)
 
BoolExpr mkFPIsNegative (Expr< FPSort > t)
 
BoolExpr mkFPIsPositive (Expr< FPSort > t)
 
FPExpr mkFP (Expr< BitVecSort > sgn, Expr< BitVecSort > sig, Expr< BitVecSort > exp)
 
FPExpr mkFPToFP (Expr< BitVecSort > bv, FPSort s)
 
FPExpr mkFPToFP (Expr< FPRMSort > rm, FPExpr t, FPSort s)
 
FPExpr mkFPToFP (Expr< FPRMSort > rm, RealExpr t, FPSort s)
 
FPExpr mkFPToFP (Expr< FPRMSort > rm, Expr< BitVecSort > t, FPSort s, boolean signed)
 
FPExpr mkFPToFP (FPSort s, Expr< FPRMSort > rm, Expr< FPSort > t)
 
BitVecExpr mkFPToBV (Expr< FPRMSort > rm, Expr< FPSort > t, int sz, boolean signed)
 
RealExpr mkFPToReal (Expr< FPSort > t)
 
BitVecExpr mkFPToIEEEBV (Expr< FPSort > t)
 
BitVecExpr mkFPToFP (Expr< FPRMSort > rm, Expr< IntSort > exp, Expr< RealSort > sig, FPSort s)
 
AST wrapAST (long nativeObject)
 
long unwrapAST (AST a)
 
String SimplifyHelp ()
 
ParamDescrs getSimplifyParameterDescriptions ()
 
void updateParamValue (String id, String value)
 
long nCtx ()
 
IDecRefQueue< Constructor<?> > getConstructorDRQ ()
 
IDecRefQueue< ConstructorList<?> > getConstructorListDRQ ()
 
IDecRefQueue< ASTgetASTDRQ ()
 
IDecRefQueue< ASTMap > getASTMapDRQ ()
 
IDecRefQueue< ASTVectorgetASTVectorDRQ ()
 
IDecRefQueue< ApplyResultgetApplyResultDRQ ()
 
IDecRefQueue< FuncInterp.Entry<?> > getFuncEntryDRQ ()
 
IDecRefQueue< FuncInterp<?> > getFuncInterpDRQ ()
 
IDecRefQueue< GoalgetGoalDRQ ()
 
IDecRefQueue< ModelgetModelDRQ ()
 
IDecRefQueue< ParamsgetParamsDRQ ()
 
IDecRefQueue< ParamDescrsgetParamDescrsDRQ ()
 
IDecRefQueue< ProbegetProbeDRQ ()
 
IDecRefQueue< SolvergetSolverDRQ ()
 
IDecRefQueue< StatisticsgetStatisticsDRQ ()
 
IDecRefQueue< TacticgetTacticDRQ ()
 
IDecRefQueue< FixedpointgetFixedpointDRQ ()
 
IDecRefQueue< OptimizegetOptimizeDRQ ()
 
void close ()
 

Protected Member Functions

 Context (long m_ctx)
 

Detailed Description

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

Definition at line 36 of file Context.java.

Constructor & Destructor Documentation

◆ Context() [1/3]

Context ( )
inline

Definition at line 40 of file Context.java.

40  {
41  synchronized (creation_lock) {
42  m_ctx = Native.mkContextRc(0);
43  init();
44  }
45  }

◆ Context() [2/3]

Context ( long  m_ctx)
inlineprotected

Definition at line 47 of file Context.java.

47  {
48  synchronized (creation_lock) {
49  this.m_ctx = m_ctx;
50  init();
51  }
52  }

◆ Context() [3/3]

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

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

Member Function Documentation

◆ and()

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

3055  {
3056  checkContextMatch(p1);
3057  checkContextMatch(p2);
3058  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
3059  p2.getNativeObject()));
3060  }

◆ andThen()

Tactic andThen ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
)
inline

Create a tactic that applies

t1

to a Goal and then

t2

to every subgoal produced by

t1

Definition at line 2750 of file Context.java.

2752  {
2753  checkContextMatch(t1);
2754  checkContextMatch(t2);
2755  checkContextMatch(ts);
2756 
2757  long last = 0;
2758  if (ts != null && ts.length > 0)
2759  {
2760  last = ts[ts.length - 1].getNativeObject();
2761  for (int i = ts.length - 2; i >= 0; i--) {
2762  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2763  last);
2764  }
2765  }
2766  if (last != 0)
2767  {
2768  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2769  return new Tactic(this, Native.tacticAndThen(nCtx(),
2770  t1.getNativeObject(), last));
2771  } else
2772  return new Tactic(this, Native.tacticAndThen(nCtx(),
2773  t1.getNativeObject(), t2.getNativeObject()));
2774  }

◆ benchmarkToSMTString()

String benchmarkToSMTString ( String  name,
String  logic,
String  status,
String  attributes,
Expr< BoolSort >[]  assumptions,
Expr< BoolSort 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 2628 of file Context.java.

2631  {
2632 
2633  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2634  attributes, assumptions.length,
2635  AST.arrayToNative(assumptions), formula.getNativeObject());
2636  }

◆ close()

void close ( )
inline

Disposes of the context.

Definition at line 4138 of file Context.java.

4139  {
4140  m_AST_DRQ.forceClear(this);
4141  m_ASTMap_DRQ.forceClear(this);
4142  m_ASTVector_DRQ.forceClear(this);
4143  m_ApplyResult_DRQ.forceClear(this);
4144  m_FuncEntry_DRQ.forceClear(this);
4145  m_FuncInterp_DRQ.forceClear(this);
4146  m_Goal_DRQ.forceClear(this);
4147  m_Model_DRQ.forceClear(this);
4148  m_Params_DRQ.forceClear(this);
4149  m_Probe_DRQ.forceClear(this);
4150  m_Solver_DRQ.forceClear(this);
4151  m_Optimize_DRQ.forceClear(this);
4152  m_Statistics_DRQ.forceClear(this);
4153  m_Tactic_DRQ.forceClear(this);
4154  m_Fixedpoint_DRQ.forceClear(this);
4155 
4156  m_boolSort = null;
4157  m_intSort = null;
4158  m_realSort = null;
4159  m_stringSort = null;
4160 
4161  synchronized (creation_lock) {
4162  Native.delContext(m_ctx);
4163  }
4164  m_ctx = 0;
4165  }

◆ cond()

Tactic cond ( Probe  p,
Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that applies

t1

to a given goal if the probe

p

evaluates to true and

t2

otherwise.

Definition at line 2832 of file Context.java.

2833  {
2834  checkContextMatch(p);
2835  checkContextMatch(t1);
2836  checkContextMatch(t2);
2837  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2838  t1.getNativeObject(), t2.getNativeObject()));
2839  }

◆ constProbe()

Probe constProbe ( double  val)
inline

Create a probe that always evaluates to

val

.

Definition at line 2984 of file Context.java.

2985  {
2986  return new Probe(this, Native.probeConst(nCtx(), val));
2987  }

◆ eq()

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

3044  {
3045  checkContextMatch(p1);
3046  checkContextMatch(p2);
3047  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
3048  p2.getNativeObject()));
3049  }

◆ fail()

Tactic fail ( )
inline

Create a tactic always fails.

Definition at line 2863 of file Context.java.

2864  {
2865  return new Tactic(this, Native.tacticFail(nCtx()));
2866  }

◆ failIf()

Tactic failIf ( Probe  p)
inline

Create a tactic that fails if the probe

p

evaluates to false.

Definition at line 2872 of file Context.java.

2873  {
2874  checkContextMatch(p);
2875  return new Tactic(this,
2876  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2877  }

◆ failIfNotDecided()

Tactic failIfNotDecided ( )
inline

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

Definition at line 2883 of file Context.java.

2884  {
2885  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2886  }

◆ ge()

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

3032  {
3033  checkContextMatch(p1);
3034  checkContextMatch(p2);
3035  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
3036  p2.getNativeObject()));
3037  }

◆ getApplyResultDRQ()

IDecRefQueue<ApplyResult> getApplyResultDRQ ( )
inline

Definition at line 4069 of file Context.java.

4070  {
4071  return m_ApplyResult_DRQ;
4072  }

◆ getASTDRQ()

IDecRefQueue<AST> getASTDRQ ( )
inline

Definition at line 4054 of file Context.java.

4055  {
4056  return m_AST_DRQ;
4057  }

◆ getASTMapDRQ()

IDecRefQueue<ASTMap> getASTMapDRQ ( )
inline

Definition at line 4059 of file Context.java.

4060  {
4061  return m_ASTMap_DRQ;
4062  }

◆ getASTVectorDRQ()

IDecRefQueue<ASTVector> getASTVectorDRQ ( )
inline

Definition at line 4064 of file Context.java.

4065  {
4066  return m_ASTVector_DRQ;
4067  }

◆ getBoolSort()

BoolSort getBoolSort ( )
inline

Retrieves the Boolean sort of the context.

Definition at line 128 of file Context.java.

129  {
130  if (m_boolSort == null) {
131  m_boolSort = new BoolSort(this);
132  }
133  return m_boolSort;
134  }

◆ getConstructorDRQ()

IDecRefQueue<Constructor<?> > getConstructorDRQ ( )
inline

Definition at line 4046 of file Context.java.

4046  {
4047  return m_Constructor_DRQ;
4048  }

◆ getConstructorListDRQ()

IDecRefQueue<ConstructorList<?> > getConstructorListDRQ ( )
inline

Definition at line 4050 of file Context.java.

4050  {
4051  return m_ConstructorList_DRQ;
4052  }

◆ getFixedpointDRQ()

IDecRefQueue<Fixedpoint> getFixedpointDRQ ( )
inline

Definition at line 4124 of file Context.java.

4125  {
4126  return m_Fixedpoint_DRQ;
4127  }

◆ getFuncEntryDRQ()

IDecRefQueue<FuncInterp.Entry<?> > getFuncEntryDRQ ( )
inline

Definition at line 4074 of file Context.java.

4075  {
4076  return m_FuncEntry_DRQ;
4077  }

◆ getFuncInterpDRQ()

IDecRefQueue<FuncInterp<?> > getFuncInterpDRQ ( )
inline

Definition at line 4079 of file Context.java.

4080  {
4081  return m_FuncInterp_DRQ;
4082  }

◆ getGoalDRQ()

IDecRefQueue<Goal> getGoalDRQ ( )
inline

Definition at line 4084 of file Context.java.

4085  {
4086  return m_Goal_DRQ;
4087  }

◆ getIntSort()

IntSort getIntSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 139 of file Context.java.

140  {
141  if (m_intSort == null) {
142  m_intSort = new IntSort(this);
143  }
144  return m_intSort;
145  }

◆ getModelDRQ()

IDecRefQueue<Model> getModelDRQ ( )
inline

Definition at line 4089 of file Context.java.

4090  {
4091  return m_Model_DRQ;
4092  }

◆ getNumProbes()

int getNumProbes ( )
inline

The number of supported Probes.

Definition at line 2946 of file Context.java.

2947  {
2948  return Native.getNumProbes(nCtx());
2949  }

◆ getNumTactics()

int getNumTactics ( )
inline

The number of supported tactics.

Definition at line 2711 of file Context.java.

2712  {
2713  return Native.getNumTactics(nCtx());
2714  }

◆ getOptimizeDRQ()

IDecRefQueue<Optimize> getOptimizeDRQ ( )
inline

Definition at line 4129 of file Context.java.

4130  {
4131  return m_Optimize_DRQ;
4132  }

◆ getParamDescrsDRQ()

IDecRefQueue<ParamDescrs> getParamDescrsDRQ ( )
inline

Definition at line 4099 of file Context.java.

4100  {
4101  return m_ParamDescrs_DRQ;
4102  }

◆ getParamsDRQ()

IDecRefQueue<Params> getParamsDRQ ( )
inline

Definition at line 4094 of file Context.java.

4095  {
4096  return m_Params_DRQ;
4097  }

◆ getProbeDescription()

String getProbeDescription ( String  name)
inline

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

Definition at line 2968 of file Context.java.

2969  {
2970  return Native.probeGetDescr(nCtx(), name);
2971  }

◆ getProbeDRQ()

IDecRefQueue<Probe> getProbeDRQ ( )
inline

Definition at line 4104 of file Context.java.

4105  {
4106  return m_Probe_DRQ;
4107  }

◆ getProbeNames()

String [] getProbeNames ( )
inline

The names of all supported Probes.

Definition at line 2954 of file Context.java.

2955  {
2956 
2957  int n = getNumProbes();
2958  String[] res = new String[n];
2959  for (int i = 0; i < n; i++)
2960  res[i] = Native.getProbeName(nCtx(), i);
2961  return res;
2962  }

◆ getRealSort()

RealSort getRealSort ( )
inline

Retrieves the Real sort of the context.

Definition at line 150 of file Context.java.

151  {
152  if (m_realSort == null) {
153  m_realSort = new RealSort(this);
154  }
155  return m_realSort;
156  }

◆ getSimplifyParameterDescriptions()

ParamDescrs getSimplifyParameterDescriptions ( )
inline

Retrieves parameter descriptions for simplifier.

Definition at line 3973 of file Context.java.

3974  {
3975  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3976  }

◆ getSolverDRQ()

IDecRefQueue<Solver> getSolverDRQ ( )
inline

Definition at line 4109 of file Context.java.

4110  {
4111  return m_Solver_DRQ;
4112  }

◆ getStatisticsDRQ()

IDecRefQueue<Statistics> getStatisticsDRQ ( )
inline

Definition at line 4114 of file Context.java.

4115  {
4116  return m_Statistics_DRQ;
4117  }

◆ getStringSort()

SeqSort<BitVecSort> getStringSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 169 of file Context.java.

170  {
171  if (m_stringSort == null) {
172  m_stringSort = mkStringSort();
173  }
174  return m_stringSort;
175  }

◆ getTacticDescription()

String getTacticDescription ( String  name)
inline

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

Definition at line 2733 of file Context.java.

2734  {
2735  return Native.tacticGetDescr(nCtx(), name);
2736  }

◆ getTacticDRQ()

IDecRefQueue<Tactic> getTacticDRQ ( )
inline

Definition at line 4119 of file Context.java.

4120  {
4121  return m_Tactic_DRQ;
4122  }

◆ getTacticNames()

String [] getTacticNames ( )
inline

The names of all supported tactics.

Definition at line 2719 of file Context.java.

2720  {
2721 
2722  int n = getNumTactics();
2723  String[] res = new String[n];
2724  for (int i = 0; i < n; i++)
2725  res[i] = Native.getTacticName(nCtx(), i);
2726  return res;
2727  }

◆ gt()

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

3006  {
3007  checkContextMatch(p1);
3008  checkContextMatch(p2);
3009  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
3010  p2.getNativeObject()));
3011  }

◆ interrupt()

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

2939  {
2940  Native.interrupt(nCtx());
2941  }

◆ intToString()

SeqExpr<BitVecSort> intToString ( Expr< IntSort e)
inline

Convert an integer expression to a string.

Definition at line 2005 of file Context.java.

2006  {
2007  return (SeqExpr<BitVecSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
2008  }

◆ le()

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

3019  {
3020  checkContextMatch(p1);
3021  checkContextMatch(p2);
3022  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
3023  p2.getNativeObject()));
3024  }

◆ lt()

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

2994  {
2995  checkContextMatch(p1);
2996  checkContextMatch(p2);
2997  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2998  p2.getNativeObject()));
2999  }

◆ mkAnd()

BoolExpr mkAnd ( Expr< BoolSort >...  t)
inline

Create an expression representing

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

.

Definition at line 803 of file Context.java.

804  {
805  checkContextMatch(t);
806  return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
807  AST.arrayToNative(t)));
808  }

Referenced by Goal.AsBoolExpr().

◆ mkAtLeast()

BoolExpr mkAtLeast ( Expr< BoolSort >[]  args,
int  k 
)
inline

Create an at-least-k constraint.

Definition at line 2247 of file Context.java.

2248  {
2249  checkContextMatch(args);
2250  return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
2251  }

◆ mkAtMost()

BoolExpr mkAtMost ( Expr< BoolSort >[]  args,
int  k 
)
inline

Create an at-most-k constraint.

Definition at line 2238 of file Context.java.

2239  {
2240  checkContextMatch(args);
2241  return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
2242  }

◆ mkBitVecSort()

BitVecSort mkBitVecSort ( int  size)
inline

Create a new bit-vector sort.

Definition at line 213 of file Context.java.

214  {
215  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
216  }

◆ mkBool()

BoolExpr mkBool ( boolean  value)
inline

Creates a Boolean value.

Definition at line 716 of file Context.java.

717  {
718  return value ? mkTrue() : mkFalse();
719  }

◆ mkBoolConst() [1/2]

BoolExpr mkBoolConst ( String  name)
inline

Create a Boolean constant.

Definition at line 634 of file Context.java.

635  {
636  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
637  }

◆ mkBoolConst() [2/2]

BoolExpr mkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 626 of file Context.java.

627  {
628  return (BoolExpr) mkConst(name, getBoolSort());
629  }

◆ mkBoolSort()

BoolSort mkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 161 of file Context.java.

162  {
163  return new BoolSort(this);
164  }

◆ mkBV() [1/3]

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

2441  {
2442  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2443  }

◆ mkBV() [2/3]

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

2451  {
2452  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2453  }

◆ mkBV() [3/3]

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

2431  {
2432  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2433  }

◆ mkBV2Int()

IntExpr mkBV2Int ( Expr< BitVecSort 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 1558 of file Context.java.

1559  {
1560  checkContextMatch(t);
1561  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1562  (signed)));
1563  }

◆ mkBVAdd()

BitVecExpr mkBVAdd ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1121 of file Context.java.

1122  {
1123  checkContextMatch(t1);
1124  checkContextMatch(t2);
1125  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1126  t1.getNativeObject(), t2.getNativeObject()));
1127  }

◆ mkBVAddNoOverflow()

BoolExpr mkBVAddNoOverflow ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1570 of file Context.java.

1572  {
1573  checkContextMatch(t1);
1574  checkContextMatch(t2);
1575  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1576  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1577  }

◆ mkBVAddNoUnderflow()

BoolExpr mkBVAddNoUnderflow ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1584 of file Context.java.

1586  {
1587  checkContextMatch(t1);
1588  checkContextMatch(t2);
1589  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1590  t1.getNativeObject(), t2.getNativeObject()));
1591  }

◆ mkBVAND()

BitVecExpr mkBVAND ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1032 of file Context.java.

1033  {
1034  checkContextMatch(t1);
1035  checkContextMatch(t2);
1036  return new BitVecExpr(this, Native.mkBvand(nCtx(),
1037  t1.getNativeObject(), t2.getNativeObject()));
1038  }

◆ mkBVASHR()

BitVecExpr mkBVASHR ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1466 of file Context.java.

1467  {
1468  checkContextMatch(t1);
1469  checkContextMatch(t2);
1470  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1471  t1.getNativeObject(), t2.getNativeObject()));
1472  }

◆ mkBVConst() [1/2]

BitVecExpr mkBVConst ( String  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 682 of file Context.java.

683  {
684  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
685  }

◆ mkBVConst() [2/2]

BitVecExpr mkBVConst ( Symbol  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 674 of file Context.java.

675  {
676  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
677  }

◆ mkBVLSHR()

BitVecExpr mkBVLSHR ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1446 of file Context.java.

1447  {
1448  checkContextMatch(t1);
1449  checkContextMatch(t2);
1450  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1451  t1.getNativeObject(), t2.getNativeObject()));
1452  }

◆ mkBVMul()

BitVecExpr mkBVMul ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1147 of file Context.java.

1148  {
1149  checkContextMatch(t1);
1150  checkContextMatch(t2);
1151  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1152  t1.getNativeObject(), t2.getNativeObject()));
1153  }

◆ mkBVMulNoOverflow()

BoolExpr mkBVMulNoOverflow ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1652 of file Context.java.

1654  {
1655  checkContextMatch(t1);
1656  checkContextMatch(t2);
1657  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1658  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1659  }

◆ mkBVMulNoUnderflow()

BoolExpr mkBVMulNoUnderflow ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1666 of file Context.java.

1668  {
1669  checkContextMatch(t1);
1670  checkContextMatch(t2);
1671  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1672  t1.getNativeObject(), t2.getNativeObject()));
1673  }

◆ mkBVNAND()

BitVecExpr mkBVNAND ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1071 of file Context.java.

1072  {
1073  checkContextMatch(t1);
1074  checkContextMatch(t2);
1075  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1076  t1.getNativeObject(), t2.getNativeObject()));
1077  }

◆ mkBVNeg()

BitVecExpr mkBVNeg ( Expr< BitVecSort t)
inline

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

Definition at line 1110 of file Context.java.

1111  {
1112  checkContextMatch(t);
1113  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1114  }

◆ mkBVNegNoOverflow()

BoolExpr mkBVNegNoOverflow ( Expr< BitVecSort 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 1640 of file Context.java.

1641  {
1642  checkContextMatch(t);
1643  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1644  t.getNativeObject()));
1645  }

◆ mkBVNOR()

BitVecExpr mkBVNOR ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1084 of file Context.java.

1085  {
1086  checkContextMatch(t1);
1087  checkContextMatch(t2);
1088  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1089  t1.getNativeObject(), t2.getNativeObject()));
1090  }

◆ mkBVNot()

BitVecExpr mkBVNot ( Expr< BitVecSort t)
inline

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

Definition at line 997 of file Context.java.

998  {
999  checkContextMatch(t);
1000  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
1001  }

◆ mkBVOR()

BitVecExpr mkBVOR ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1045 of file Context.java.

1046  {
1047  checkContextMatch(t1);
1048  checkContextMatch(t2);
1049  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1050  t2.getNativeObject()));
1051  }

◆ mkBVRedAND()

BitVecExpr mkBVRedAND ( Expr< BitVecSort 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 1008 of file Context.java.

1009  {
1010  checkContextMatch(t);
1011  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
1012  t.getNativeObject()));
1013  }

◆ mkBVRedOR()

BitVecExpr mkBVRedOR ( Expr< BitVecSort 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 1020 of file Context.java.

1021  {
1022  checkContextMatch(t);
1023  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
1024  t.getNativeObject()));
1025  }

◆ mkBVRotateLeft() [1/2]

BitVecExpr mkBVRotateLeft ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1504 of file Context.java.

1506  {
1507  checkContextMatch(t1);
1508  checkContextMatch(t2);
1509  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1510  t1.getNativeObject(), t2.getNativeObject()));
1511  }

◆ mkBVRotateLeft() [2/2]

BitVecExpr mkBVRotateLeft ( int  i,
Expr< BitVecSort 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 1479 of file Context.java.

1480  {
1481  checkContextMatch(t);
1482  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1483  t.getNativeObject()));
1484  }

◆ mkBVRotateRight() [1/2]

BitVecExpr mkBVRotateRight ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1519 of file Context.java.

1521  {
1522  checkContextMatch(t1);
1523  checkContextMatch(t2);
1524  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1525  t1.getNativeObject(), t2.getNativeObject()));
1526  }

◆ mkBVRotateRight() [2/2]

BitVecExpr mkBVRotateRight ( int  i,
Expr< BitVecSort 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 1491 of file Context.java.

1492  {
1493  checkContextMatch(t);
1494  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1495  t.getNativeObject()));
1496  }

◆ mkBVSDiv()

BitVecExpr mkBVSDiv ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1183 of file Context.java.

1184  {
1185  checkContextMatch(t1);
1186  checkContextMatch(t2);
1187  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1188  t1.getNativeObject(), t2.getNativeObject()));
1189  }

◆ mkBVSDivNoOverflow()

BoolExpr mkBVSDivNoOverflow ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1626 of file Context.java.

1628  {
1629  checkContextMatch(t1);
1630  checkContextMatch(t2);
1631  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1632  t1.getNativeObject(), t2.getNativeObject()));
1633  }

◆ mkBVSGE()

BoolExpr mkBVSGE ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1308 of file Context.java.

1309  {
1310  checkContextMatch(t1);
1311  checkContextMatch(t2);
1312  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1313  t2.getNativeObject()));
1314  }

◆ mkBVSGT()

BoolExpr mkBVSGT ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1334 of file Context.java.

1335  {
1336  checkContextMatch(t1);
1337  checkContextMatch(t2);
1338  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1339  t2.getNativeObject()));
1340  }

◆ mkBVSHL()

BitVecExpr mkBVSHL ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1427 of file Context.java.

1428  {
1429  checkContextMatch(t1);
1430  checkContextMatch(t2);
1431  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1432  t1.getNativeObject(), t2.getNativeObject()));
1433  }

◆ mkBVSLE()

BoolExpr mkBVSLE ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1282 of file Context.java.

1283  {
1284  checkContextMatch(t1);
1285  checkContextMatch(t2);
1286  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1287  t2.getNativeObject()));
1288  }

◆ mkBVSLT()

BoolExpr mkBVSLT ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1256 of file Context.java.

1257  {
1258  checkContextMatch(t1);
1259  checkContextMatch(t2);
1260  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1261  t2.getNativeObject()));
1262  }

◆ mkBVSMod()

BitVecExpr mkBVSMod ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1230 of file Context.java.

1231  {
1232  checkContextMatch(t1);
1233  checkContextMatch(t2);
1234  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1235  t1.getNativeObject(), t2.getNativeObject()));
1236  }

◆ mkBVSRem()

BitVecExpr mkBVSRem ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1216 of file Context.java.

1217  {
1218  checkContextMatch(t1);
1219  checkContextMatch(t2);
1220  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1221  t1.getNativeObject(), t2.getNativeObject()));
1222  }

◆ mkBVSub()

BitVecExpr mkBVSub ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1134 of file Context.java.

1135  {
1136  checkContextMatch(t1);
1137  checkContextMatch(t2);
1138  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1139  t1.getNativeObject(), t2.getNativeObject()));
1140  }

◆ mkBVSubNoOverflow()

BoolExpr mkBVSubNoOverflow ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1598 of file Context.java.

1600  {
1601  checkContextMatch(t1);
1602  checkContextMatch(t2);
1603  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1604  t1.getNativeObject(), t2.getNativeObject()));
1605  }

◆ mkBVSubNoUnderflow()

BoolExpr mkBVSubNoUnderflow ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1612 of file Context.java.

1614  {
1615  checkContextMatch(t1);
1616  checkContextMatch(t2);
1617  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1618  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1619  }

◆ mkBVUDiv()

BitVecExpr mkBVUDiv ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1162 of file Context.java.

1163  {
1164  checkContextMatch(t1);
1165  checkContextMatch(t2);
1166  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1167  t1.getNativeObject(), t2.getNativeObject()));
1168  }

◆ mkBVUGE()

BoolExpr mkBVUGE ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1295 of file Context.java.

1296  {
1297  checkContextMatch(t1);
1298  checkContextMatch(t2);
1299  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1300  t2.getNativeObject()));
1301  }

◆ mkBVUGT()

BoolExpr mkBVUGT ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1321 of file Context.java.

1322  {
1323  checkContextMatch(t1);
1324  checkContextMatch(t2);
1325  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1326  t2.getNativeObject()));
1327  }

◆ mkBVULE()

BoolExpr mkBVULE ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1269 of file Context.java.

1270  {
1271  checkContextMatch(t1);
1272  checkContextMatch(t2);
1273  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1274  t2.getNativeObject()));
1275  }

◆ mkBVULT()

BoolExpr mkBVULT ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1243 of file Context.java.

1244  {
1245  checkContextMatch(t1);
1246  checkContextMatch(t2);
1247  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1248  t2.getNativeObject()));
1249  }

◆ mkBVURem()

BitVecExpr mkBVURem ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1198 of file Context.java.

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

◆ mkBVXNOR()

BitVecExpr mkBVXNOR ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1097 of file Context.java.

1098  {
1099  checkContextMatch(t1);
1100  checkContextMatch(t2);
1101  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1102  t1.getNativeObject(), t2.getNativeObject()));
1103  }

◆ mkBVXOR()

BitVecExpr mkBVXOR ( Expr< BitVecSort t1,
Expr< BitVecSort t2 
)
inline

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

Definition at line 1058 of file Context.java.

1059  {
1060  checkContextMatch(t1);
1061  checkContextMatch(t2);
1062  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1063  t1.getNativeObject(), t2.getNativeObject()));
1064  }

◆ mkConcat()

BitVecExpr mkConcat ( Expr< BitVecSort t1,
Expr< BitVecSort 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 1352 of file Context.java.

1353  {
1354  checkContextMatch(t1);
1355  checkContextMatch(t2);
1356  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1357  t1.getNativeObject(), t2.getNativeObject()));
1358  }

◆ mkDatatypeSorts() [1/2]

DatatypeSort<Object> [] mkDatatypeSorts ( String[]  names,
Constructor< Object >  c[][] 
)
inline

Create mutually recursive data-types.

Definition at line 413 of file Context.java.

415  {
416  return mkDatatypeSorts(mkSymbols(names), c);
417  }

◆ mkDatatypeSorts() [2/2]

DatatypeSort<Object> [] mkDatatypeSorts ( Symbol[]  names,
Constructor< Object >  c[][] 
)
inline

Create mutually recursive datatypes.

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

Definition at line 387 of file Context.java.

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

◆ mkExists() [1/2]

Quantifier mkExists ( Expr<?>[]  boundConstants,
Expr< BoolSort body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

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

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

Definition at line 2518 of file Context.java.

2521  {
2522 
2523  return Quantifier.of(this, false, boundConstants, body, weight,
2524  patterns, noPatterns, quantifierID, skolemID);
2525  }

◆ mkExists() [2/2]

Quantifier mkExists ( Sort[]  sorts,
Symbol[]  names,
Expr< BoolSort body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Creates an existential quantifier using de-Bruijn indexed variables.

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

Definition at line 2505 of file Context.java.

2508  {
2509 
2510  return Quantifier.of(this, false, sorts, names, body, weight,
2511  patterns, noPatterns, quantifierID, skolemID);
2512  }

◆ mkExtract()

BitVecExpr mkExtract ( int  high,
int  low,
Expr< BitVecSort 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 1368 of file Context.java.

1370  {
1371  checkContextMatch(t);
1372  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1373  t.getNativeObject()));
1374  }

◆ mkFalse()

BoolExpr mkFalse ( )
inline

The false Term.

Definition at line 708 of file Context.java.

709  {
710  return new BoolExpr(this, Native.mkFalse(nCtx()));
711  }

◆ mkFixedpoint()

Fixedpoint mkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3144 of file Context.java.

3145  {
3146  return new Fixedpoint(this);
3147  }

◆ mkForall() [1/2]

Quantifier mkForall ( Expr<?>[]  boundConstants,
Expr< BoolSort body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

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

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

Definition at line 2492 of file Context.java.

2495  {
2496 
2497  return Quantifier.of(this, true, boundConstants, body, weight,
2498  patterns, noPatterns, quantifierID, skolemID);
2499  }

◆ mkForall() [2/2]

Quantifier mkForall ( Sort[]  sorts,
Symbol[]  names,
Expr< BoolSort body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a universal Quantifier.

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

Definition at line 2480 of file Context.java.

2483  {
2484  return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2485  noPatterns, quantifierID, skolemID);
2486  }

◆ mkFP() [1/6]

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

3475  {
3476  return mkFPNumeral(sgn, exp, sig, s);
3477  }

◆ mkFP() [2/6]

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

3488  {
3489  return mkFPNumeral(sgn, exp, sig, s);
3490  }

◆ mkFP() [3/6]

FPNum mkFP ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a double.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3449 of file Context.java.

3450  {
3451  return mkFPNumeral(v, s);
3452  }

◆ mkFP() [4/6]

FPExpr mkFP ( Expr< BitVecSort sgn,
Expr< BitVecSort sig,
Expr< BitVecSort 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 3772 of file Context.java.

3773  {
3774  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3775  }

◆ mkFP() [5/6]

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

3439  {
3440  return mkFPNumeral(v, s);
3441  }

◆ mkFP() [6/6]

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

3462  {
3463  return mkFPNumeral(v, s);
3464  }

◆ mkFPAbs()

FPExpr mkFPAbs ( Expr< FPSort t)
inline

Floating-point absolute value

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3498 of file Context.java.

3499  {
3500  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3501  }

◆ mkFPAdd()

FPExpr mkFPAdd ( Expr< FPRMSort rm,
Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Floating-point addition

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

Definition at line 3520 of file Context.java.

3521  {
3522  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3523  }

◆ mkFPDiv()

FPExpr mkFPDiv ( Expr< FPRMSort rm,
Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Floating-point division

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

Definition at line 3556 of file Context.java.

3557  {
3558  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3559  }

◆ mkFPEq()

BoolExpr mkFPEq ( Expr< FPSort t1,
Expr< FPSort 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 3684 of file Context.java.

3685  {
3686  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3687  }

◆ mkFPFMA()

FPExpr mkFPFMA ( Expr< FPRMSort rm,
Expr< FPSort t1,
Expr< FPSort t2,
Expr< FPSort 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 3571 of file Context.java.

3572  {
3573  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3574  }

◆ mkFPGEq()

BoolExpr mkFPGEq ( Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3660 of file Context.java.

3661  {
3662  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3663  }

◆ mkFPGt()

BoolExpr mkFPGt ( Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3671 of file Context.java.

3672  {
3673  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3674  }

◆ mkFPInf()

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

3358  {
3359  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3360  }

◆ mkFPIsInfinite()

BoolExpr mkFPIsInfinite ( Expr< FPSort t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3724 of file Context.java.

3725  {
3726  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3727  }

◆ mkFPIsNaN()

BoolExpr mkFPIsNaN ( Expr< FPSort t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3734 of file Context.java.

3735  {
3736  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3737  }

◆ mkFPIsNegative()

BoolExpr mkFPIsNegative ( Expr< FPSort t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3744 of file Context.java.

3745  {
3746  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3747  }

◆ mkFPIsNormal()

BoolExpr mkFPIsNormal ( Expr< FPSort t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3694 of file Context.java.

3695  {
3696  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3697  }

◆ mkFPIsPositive()

BoolExpr mkFPIsPositive ( Expr< FPSort t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3754 of file Context.java.

3755  {
3756  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3757  }

◆ mkFPIsSubnormal()

BoolExpr mkFPIsSubnormal ( Expr< FPSort t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3704 of file Context.java.

3705  {
3706  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3707  }

◆ mkFPIsZero()

BoolExpr mkFPIsZero ( Expr< FPSort 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 3714 of file Context.java.

3715  {
3716  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3717  }

◆ mkFPLEq()

BoolExpr mkFPLEq ( Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3638 of file Context.java.

3639  {
3640  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3641  }

◆ mkFPLt()

BoolExpr mkFPLt ( Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3649 of file Context.java.

3650  {
3651  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3652  }

◆ mkFPMax()

FPExpr mkFPMax ( Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3627 of file Context.java.

3628  {
3629  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3630  }

◆ mkFPMin()

FPExpr mkFPMin ( Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3616 of file Context.java.

3617  {
3618  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3619  }

◆ mkFPMul()

FPExpr mkFPMul ( Expr< FPRMSort rm,
Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Floating-point multiplication

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

Definition at line 3544 of file Context.java.

3545  {
3546  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3547  }

◆ mkFPNaN()

FPNum mkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3346 of file Context.java.

3347  {
3348  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3349  }

◆ mkFPNeg()

FPExpr mkFPNeg ( Expr< FPSort t)
inline

Floating-point negation

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3508 of file Context.java.

3509  {
3510  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3511  }

◆ mkFPNumeral() [1/5]

FPNum mkFPNumeral ( boolean  sgn,
int  exp,
int  sig,
FPSort  s 
)
inline

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

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

Definition at line 3414 of file Context.java.

3415  {
3416  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3417  }

◆ mkFPNumeral() [2/5]

FPNum mkFPNumeral ( boolean  sgn,
long  exp,
long  sig,
FPSort  s 
)
inline

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

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

Definition at line 3427 of file Context.java.

3428  {
3429  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3430  }

◆ mkFPNumeral() [3/5]

FPNum mkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a double.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3390 of file Context.java.

3391  {
3392  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3393  }

◆ mkFPNumeral() [4/5]

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

3380  {
3381  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3382  }

◆ mkFPNumeral() [5/5]

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

3402  {
3403  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3404  }

◆ mkFPRem()

FPExpr mkFPRem ( Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3593 of file Context.java.

3594  {
3595  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3596  }

◆ mkFPRNA()

FPRMNum mkFPRNA ( )
inline

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

Exceptions
Z3Exception

Definition at line 3198 of file Context.java.

3199  {
3200  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3201  }

◆ mkFPRNE()

FPRMNum mkFPRNE ( )
inline

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

Exceptions
Z3Exception

Definition at line 3180 of file Context.java.

3181  {
3182  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3183  }

◆ mkFPRoundingModeSort()

FPRMSort mkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Exceptions
Z3Exception

Definition at line 3162 of file Context.java.

3163  {
3164  return new FPRMSort(this);
3165  }

◆ mkFPRoundNearestTiesToAway()

FPRMNum mkFPRoundNearestTiesToAway ( )
inline

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

Exceptions
Z3Exception

Definition at line 3189 of file Context.java.

3190  {
3191  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3192  }

◆ mkFPRoundNearestTiesToEven()

FPRMExpr mkFPRoundNearestTiesToEven ( )
inline

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

Exceptions
Z3Exception

Definition at line 3171 of file Context.java.

3172  {
3173  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3174  }

◆ mkFPRoundToIntegral()

FPExpr mkFPRoundToIntegral ( Expr< FPRMSort rm,
Expr< FPSort 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 3605 of file Context.java.

3606  {
3607  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3608  }

◆ mkFPRoundTowardNegative()

FPRMNum mkFPRoundTowardNegative ( )
inline

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

Exceptions
Z3Exception

Definition at line 3225 of file Context.java.

3226  {
3227  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3228  }

◆ mkFPRoundTowardPositive()

FPRMNum mkFPRoundTowardPositive ( )
inline

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

Exceptions
Z3Exception

Definition at line 3207 of file Context.java.

3208  {
3209  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3210  }

◆ mkFPRoundTowardZero()

FPRMNum mkFPRoundTowardZero ( )
inline

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

Exceptions
Z3Exception

Definition at line 3243 of file Context.java.

3244  {
3245  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3246  }

◆ mkFPRTN()

FPRMNum mkFPRTN ( )
inline

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

Exceptions
Z3Exception

Definition at line 3234 of file Context.java.

3235  {
3236  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3237  }

◆ mkFPRTP()

FPRMNum mkFPRTP ( )
inline

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

Exceptions
Z3Exception

Definition at line 3216 of file Context.java.

3217  {
3218  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3219  }

◆ mkFPRTZ()

FPRMNum mkFPRTZ ( )
inline

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

Exceptions
Z3Exception

Definition at line 3252 of file Context.java.

3253  {
3254  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3255  }

◆ mkFPSort()

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

3264  {
3265  return new FPSort(this, ebits, sbits);
3266  }

◆ mkFPSort128()

FPSort mkFPSort128 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3335 of file Context.java.

3336  {
3337  return new FPSort(this, Native.mkFpaSort128(nCtx()));
3338  }

◆ mkFPSort16()

FPSort mkFPSort16 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3281 of file Context.java.

3282  {
3283  return new FPSort(this, Native.mkFpaSort16(nCtx()));
3284  }

◆ mkFPSort32()

FPSort mkFPSort32 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3299 of file Context.java.

3300  {
3301  return new FPSort(this, Native.mkFpaSort32(nCtx()));
3302  }

◆ mkFPSort64()

FPSort mkFPSort64 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3317 of file Context.java.

3318  {
3319  return new FPSort(this, Native.mkFpaSort64(nCtx()));
3320  }

◆ mkFPSortDouble()

FPSort mkFPSortDouble ( )
inline

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

Exceptions
Z3Exception

Definition at line 3308 of file Context.java.

3309  {
3310  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3311  }

◆ mkFPSortHalf()

FPSort mkFPSortHalf ( )
inline

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

Exceptions
Z3Exception

Definition at line 3272 of file Context.java.

3273  {
3274  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3275  }

◆ mkFPSortQuadruple()

FPSort mkFPSortQuadruple ( )
inline

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

Exceptions
Z3Exception

Definition at line 3326 of file Context.java.

3327  {
3328  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3329  }

◆ mkFPSortSingle()

FPSort mkFPSortSingle ( )
inline

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

Exceptions
Z3Exception

Definition at line 3290 of file Context.java.

3291  {
3292  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3293  }

◆ mkFPSqrt()

FPExpr mkFPSqrt ( Expr< FPRMSort rm,
Expr< FPSort t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term
Exceptions
Z3Exception

Definition at line 3582 of file Context.java.

3583  {
3584  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3585  }

◆ mkFPSub()

FPExpr mkFPSub ( Expr< FPRMSort rm,
Expr< FPSort t1,
Expr< FPSort t2 
)
inline

Floating-point subtraction

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

Definition at line 3532 of file Context.java.

3533  {
3534  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3535  }

◆ mkFPToBV()

BitVecExpr mkFPToBV ( Expr< FPRMSort rm,
Expr< FPSort t,
int  sz,
boolean signed   
)
inline

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

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

Definition at line 3873 of file Context.java.

3874  {
3875  if (signed)
3876  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3877  else
3878  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3879  }

◆ mkFPToFP() [1/6]

FPExpr mkFPToFP ( Expr< BitVecSort 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 3788 of file Context.java.

3789  {
3790  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3791  }

◆ mkFPToFP() [2/6]

FPExpr mkFPToFP ( Expr< FPRMSort rm,
Expr< BitVecSort 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 3838 of file Context.java.

3839  {
3840  if (signed)
3841  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3842  else
3843  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3844  }

◆ mkFPToFP() [3/6]

BitVecExpr mkFPToFP ( Expr< FPRMSort rm,
Expr< IntSort exp,
Expr< RealSort 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 3923 of file Context.java.

3924  {
3925  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3926  }

◆ mkFPToFP() [4/6]

FPExpr mkFPToFP ( Expr< FPRMSort 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 3804 of file Context.java.

3805  {
3806  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3807  }

◆ mkFPToFP() [5/6]

FPExpr mkFPToFP ( Expr< FPRMSort 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 3820 of file Context.java.

3821  {
3822  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3823  }

◆ mkFPToFP() [6/6]

FPExpr mkFPToFP ( FPSort  s,
Expr< FPRMSort rm,
Expr< FPSort 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 3856 of file Context.java.

3857  {
3858  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3859  }

◆ mkFPToIEEEBV()

BitVecExpr mkFPToIEEEBV ( Expr< FPSort t)
inline

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

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

Definition at line 3905 of file Context.java.

3906  {
3907  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3908  }

◆ mkFPToReal()

RealExpr mkFPToReal ( Expr< FPSort t)
inline

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

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

Definition at line 3890 of file Context.java.

3891  {
3892  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3893  }

◆ mkFPZero()

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

3369  {
3370  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3371  }

◆ mkGoal()

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

2696  {
2697  return new Goal(this, models, unsatCores, proofs);
2698  }

◆ mkIff()

BoolExpr mkIff ( Expr< BoolSort t1,
Expr< BoolSort t2 
)
inline

Create an expression representing

t1 iff t2

.

Definition at line 770 of file Context.java.

771  {
772  checkContextMatch(t1);
773  checkContextMatch(t2);
774  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
775  t2.getNativeObject()));
776  }

◆ mkImplies()

BoolExpr mkImplies ( Expr< BoolSort t1,
Expr< BoolSort t2 
)
inline

Create an expression representing

t1 -> t2

.

Definition at line 781 of file Context.java.

782  {
783  checkContextMatch(t1);
784  checkContextMatch(t2);
785  return new BoolExpr(this, Native.mkImplies(nCtx(),
786  t1.getNativeObject(), t2.getNativeObject()));
787  }

◆ mkInt() [1/3]

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

2406  {
2407 
2408  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2409  .getNativeObject()));
2410  }

◆ mkInt() [2/3]

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

2419  {
2420 
2421  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2422  .getNativeObject()));
2423  }

◆ mkInt() [3/3]

IntNum mkInt ( String  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 2392 of file Context.java.

2393  {
2394 
2395  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2396  .getNativeObject()));
2397  }

◆ mkInt2BV()

BitVecExpr mkInt2BV ( int  n,
Expr< IntSort 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 1537 of file Context.java.

1538  {
1539  checkContextMatch(t);
1540  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1541  t.getNativeObject()));
1542  }

◆ mkInt2Real()

RealExpr mkInt2Real ( Expr< IntSort t)
inline

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

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

k

and asserting

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

. The argument must be of integer sort.

Definition at line 964 of file Context.java.

965  {
966  checkContextMatch(t);
967  return new RealExpr(this,
968  Native.mkInt2real(nCtx(), t.getNativeObject()));
969  }

◆ mkIntConst() [1/2]

IntExpr mkIntConst ( String  name)
inline

Creates an integer constant.

Definition at line 650 of file Context.java.

651  {
652  return (IntExpr) mkConst(name, getIntSort());
653  }

◆ mkIntConst() [2/2]

IntExpr mkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 642 of file Context.java.

643  {
644  return (IntExpr) mkConst(name, getIntSort());
645  }

◆ mkIntSort()

IntSort mkIntSort ( )
inline

Create a new integer sort.

Definition at line 197 of file Context.java.

198  {
199  return new IntSort(this);
200  }

◆ mkIsInteger()

BoolExpr mkIsInteger ( Expr< RealSort t)
inline

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

Definition at line 986 of file Context.java.

987  {
988  checkContextMatch(t);
989  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
990  }

◆ mkMod()

IntExpr mkMod ( Expr< IntSort t1,
Expr< IntSort t2 
)
inline

Create an expression representing

t1 mod t2

. Remarks: The arguments must have int type.

Definition at line 876 of file Context.java.

877  {
878  checkContextMatch(t1);
879  checkContextMatch(t2);
880  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
881  t2.getNativeObject()));
882  }

◆ mkNot()

BoolExpr mkNot ( Expr< BoolSort a)
inline

Create an expression representing

not(a)

.

Definition at line 745 of file Context.java.

746  {
747  checkContextMatch(a);
748  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
749  }

◆ mkOptimize()

Optimize mkOptimize ( )
inline

Create a Optimize context.

Definition at line 3152 of file Context.java.

3153  {
3154  return new Optimize(this);
3155  }

◆ mkOr()

BoolExpr mkOr ( Expr< BoolSort >...  t)
inline

Create an expression representing

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

.

Definition at line 813 of file Context.java.

814  {
815  checkContextMatch(t);
816  return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
817  AST.arrayToNative(t)));
818  }

◆ mkParams()

Params mkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2703 of file Context.java.

2704  {
2705  return new Params(this);
2706  }

◆ mkPattern()

Pattern mkPattern ( Expr<?>...  terms)
inline

Create a quantifier pattern.

Definition at line 569 of file Context.java.

570  {
571  if (terms.length == 0)
572  throw new Z3Exception("Cannot create a pattern from zero terms");
573 
574  long[] termsNative = AST.arrayToNative(terms);
575  return new Pattern(this, Native.mkPattern(nCtx(), terms.length,
576  termsNative));
577  }

◆ mkPBEq()

BoolExpr mkPBEq ( int[]  coeffs,
Expr< BoolSort >[]  args,
int  k 
)
inline

Create a pseudo-Boolean equal constraint.

Definition at line 2274 of file Context.java.

2275  {
2276  checkContextMatch(args);
2277  return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2278  }

◆ mkPBGe()

BoolExpr mkPBGe ( int[]  coeffs,
Expr< BoolSort >[]  args,
int  k 
)
inline

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

Definition at line 2265 of file Context.java.

2266  {
2267  checkContextMatch(args);
2268  return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2269  }

◆ mkPBLe()

BoolExpr mkPBLe ( int[]  coeffs,
Expr< BoolSort >[]  args,
int  k 
)
inline

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

Definition at line 2256 of file Context.java.

2257  {
2258  checkContextMatch(args);
2259  return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2260  }

◆ mkProbe()

Probe mkProbe ( String  name)
inline

Creates a new Probe.

Definition at line 2976 of file Context.java.

2977  {
2978  return new Probe(this, name);
2979  }

◆ mkQuantifier() [1/2]

Quantifier mkQuantifier ( boolean  universal,
Expr<?>[]  boundConstants,
Expr< BoolSort body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a Quantifier

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

Definition at line 2549 of file Context.java.

2552  {
2553 
2554  if (universal)
2555  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2556  quantifierID, skolemID);
2557  else
2558  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2559  quantifierID, skolemID);
2560  }

◆ mkQuantifier() [2/2]

Quantifier mkQuantifier ( boolean  universal,
Sort[]  sorts,
Symbol[]  names,
Expr< BoolSort body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a Quantifier.

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

Definition at line 2531 of file Context.java.

2535  {
2536 
2537  if (universal)
2538  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2539  quantifierID, skolemID);
2540  else
2541  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2542  quantifierID, skolemID);
2543  }

◆ mkReal() [1/4]

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

2341  {
2342  if (den == 0) {
2343  throw new Z3Exception("Denominator is zero");
2344  }
2345 
2346  return new RatNum(this, Native.mkReal(nCtx(), num, den));
2347  }

◆ mkReal() [2/4]

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

2369  {
2370 
2371  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2372  .getNativeObject()));
2373  }

◆ mkReal() [3/4]

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

2382  {
2383 
2384  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2385  .getNativeObject()));
2386  }

◆ mkReal() [4/4]

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

2356  {
2357 
2358  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2359  .getNativeObject()));
2360  }

◆ mkReal2Int()

IntExpr mkReal2Int ( Expr< RealSort 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 977 of file Context.java.

978  {
979  checkContextMatch(t);
980  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
981  }

◆ mkRealConst() [1/2]

RealExpr mkRealConst ( String  name)
inline

Creates a real constant.

Definition at line 666 of file Context.java.

667  {
668  return (RealExpr) mkConst(name, getRealSort());
669  }

◆ mkRealConst() [2/2]

RealExpr mkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 658 of file Context.java.

659  {
660  return (RealExpr) mkConst(name, getRealSort());
661  }

◆ mkRealSort()

RealSort mkRealSort ( )
inline

Create a real sort.

Definition at line 205 of file Context.java.

206  {
207  return new RealSort(this);
208  }

◆ mkRem()

IntExpr mkRem ( Expr< IntSort t1,
Expr< IntSort t2 
)
inline

Create an expression representing

t1 rem t2

. Remarks: The arguments must have int type.

Definition at line 889 of file Context.java.

890  {
891  checkContextMatch(t1);
892  checkContextMatch(t2);
893  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
894  t2.getNativeObject()));
895  }

◆ mkRepeat()

BitVecExpr mkRepeat ( int  i,
Expr< BitVecSort t 
)
inline

Bit-vector repetition. Remarks: The argument

t

must have a bit-vector sort.

Definition at line 1409 of file Context.java.

1410  {
1411  checkContextMatch(t);
1412  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1413  t.getNativeObject()));
1414  }

◆ mkSignExt()

BitVecExpr mkSignExt ( int  i,
Expr< BitVecSort 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 1383 of file Context.java.

1384  {
1385  checkContextMatch(t);
1386  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1387  t.getNativeObject()));
1388  }

◆ mkSimpleSolver()

Solver mkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3123 of file Context.java.

3124  {
3125  return new Solver(this, Native.mkSimpleSolver(nCtx()));
3126  }

◆ mkSolver() [1/4]

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

3090  {
3091  return mkSolver((Symbol) null);
3092  }

Referenced by Tactic.getSolver().

◆ mkSolver() [2/4]

Solver mkSolver ( String  logic)
inline

Creates a new (incremental) solver.

See also
mkSolver(Symbol)

Definition at line 3115 of file Context.java.

3116  {
3117  return mkSolver(mkSymbol(logic));
3118  }

◆ mkSolver() [3/4]

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

3102  {
3103 
3104  if (logic == null)
3105  return new Solver(this, Native.mkSolver(nCtx()));
3106  else
3107  return new Solver(this, Native.mkSolverForLogic(nCtx(),
3108  logic.getNativeObject()));
3109  }

◆ mkSolver() [4/4]

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

3135  {
3136 
3137  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3138  t.getNativeObject()));
3139  }

◆ mkString()

SeqExpr<BitVecSort> mkString ( String  s)
inline

Create a string constant.

Definition at line 1997 of file Context.java.

1998  {
1999  return (SeqExpr<BitVecSort>) Expr.create(this, Native.mkString(nCtx(), s));
2000  }

◆ mkStringSort()

SeqSort<BitVecSort> mkStringSort ( )
inline

Create a new string sort

Definition at line 242 of file Context.java.

243  {
244  return new SeqSort<>(this, Native.mkStringSort(nCtx()));
245  }

◆ mkSymbol() [1/2]

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

95  {
96  return new IntSymbol(this, i);
97  }

Referenced by Params.add().

◆ mkSymbol() [2/2]

StringSymbol mkSymbol ( String  name)
inline

Create a symbol using a string.

Definition at line 102 of file Context.java.

103  {
104  return new StringSymbol(this, name);
105  }

◆ mkTactic()

Tactic mkTactic ( String  name)
inline

Creates a new Tactic.

Definition at line 2741 of file Context.java.

2742  {
2743  return new Tactic(this, name);
2744  }

Referenced by Goal.simplify().

◆ mkTrue()

BoolExpr mkTrue ( )
inline

The true Term.

Definition at line 700 of file Context.java.

701  {
702  return new BoolExpr(this, Native.mkTrue(nCtx()));
703  }

Referenced by Goal.AsBoolExpr().

◆ mkTupleSort()

TupleSort mkTupleSort ( Symbol  name,
Symbol[]  fieldNames,
Sort[]  fieldSorts 
)
inline

Create a new tuple sort.

Definition at line 267 of file Context.java.

269  {
270  checkContextMatch(name);
271  checkContextMatch(fieldNames);
272  checkContextMatch(fieldSorts);
273  return new TupleSort(this, name, fieldNames.length, fieldNames,
274  fieldSorts);
275  }

◆ mkUninterpretedSort() [1/2]

UninterpretedSort mkUninterpretedSort ( String  str)
inline

Create a new uninterpreted sort.

Definition at line 189 of file Context.java.

190  {
191  return mkUninterpretedSort(mkSymbol(str));
192  }

◆ mkUninterpretedSort() [2/2]

UninterpretedSort mkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 180 of file Context.java.

181  {
182  checkContextMatch(s);
183  return new UninterpretedSort(this, s);
184  }

◆ mkXor()

BoolExpr mkXor ( Expr< BoolSort t1,
Expr< BoolSort t2 
)
inline

Create an expression representing

t1 xor t2

.

Definition at line 792 of file Context.java.

793  {
794  checkContextMatch(t1);
795  checkContextMatch(t2);
796  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
797  t2.getNativeObject()));
798  }

◆ mkZeroExt()

BitVecExpr mkZeroExt ( int  i,
Expr< BitVecSort 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 1397 of file Context.java.

1398  {
1399  checkContextMatch(t);
1400  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1401  t.getNativeObject()));
1402  }

◆ nCtx()

long nCtx ( )
inline

◆ not()

Probe not ( Probe  p)
inline

Create a probe that evaluates to

true

when the value

p

does not evaluate to

true

.

Definition at line 3076 of file Context.java.

3077  {
3078  checkContextMatch(p);
3079  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
3080  }

◆ or()

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

3066  {
3067  checkContextMatch(p1);
3068  checkContextMatch(p2);
3069  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
3070  p2.getNativeObject()));
3071  }

◆ orElse()

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

2793  {
2794  checkContextMatch(t1);
2795  checkContextMatch(t2);
2796  return new Tactic(this, Native.tacticOrElse(nCtx(),
2797  t1.getNativeObject(), t2.getNativeObject()));
2798  }

◆ parAndThen()

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

2926  {
2927  checkContextMatch(t1);
2928  checkContextMatch(t2);
2929  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2930  t1.getNativeObject(), t2.getNativeObject()));
2931  }

◆ parOr()

Tactic parOr ( Tactic...  t)
inline

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

Definition at line 2914 of file Context.java.

2915  {
2916  checkContextMatch(t);
2917  return new Tactic(this, Native.tacticParOr(nCtx(),
2918  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2919  }

◆ parseSMTLIB2File()

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

2670  {
2671  int csn = Symbol.arrayLength(sortNames);
2672  int cs = Sort.arrayLength(sorts);
2673  int cdn = Symbol.arrayLength(declNames);
2674  int cd = AST.arrayLength(decls);
2675  if (csn != cs || cdn != cd)
2676  throw new Z3Exception("Argument size mismatch");
2677  ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
2678  fileName, AST.arrayLength(sorts),
2679  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2680  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2681  AST.arrayToNative(decls)));
2682  return v.ToBoolExprArray();
2683  }

◆ parseSMTLIB2String()

BoolExpr [] parseSMTLIB2String ( String  str,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl<?>[]  decls 
)
inline

Parse the given string using the SMT-LIB2 parser.

Returns
A conjunction of assertions.

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

Definition at line 2647 of file Context.java.

2649  {
2650  int csn = Symbol.arrayLength(sortNames);
2651  int cs = Sort.arrayLength(sorts);
2652  int cdn = Symbol.arrayLength(declNames);
2653  int cd = AST.arrayLength(decls);
2654  if (csn != cs || cdn != cd) {
2655  throw new Z3Exception("Argument size mismatch");
2656  }
2657  ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
2658  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2659  AST.arrayToNative(sorts), AST.arrayLength(decls),
2660  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2661  return v.ToBoolExprArray();
2662  }

◆ repeat()

Tactic repeat ( Tactic  t,
int  max 
)
inline

Create a tactic that keeps applying

t

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

is reached.

Definition at line 2845 of file Context.java.

2846  {
2847  checkContextMatch(t);
2848  return new Tactic(this, Native.tacticRepeat(nCtx(),
2849  t.getNativeObject(), max));
2850  }

◆ setPrintMode()

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

2611  {
2612  Native.setAstPrintMode(nCtx(), value.toInt());
2613  }

◆ SimplifyHelp()

String SimplifyHelp ( )
inline

Return a string describing all available parameters to

Expr.Simplify

.

Definition at line 3965 of file Context.java.

3966  {
3967  return Native.simplifyGetHelp(nCtx());
3968  }

◆ skip()

Tactic skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 2855 of file Context.java.

2856  {
2857  return new Tactic(this, Native.tacticSkip(nCtx()));
2858  }

◆ stringToInt()

IntExpr stringToInt ( Expr< SeqSort< BitVecSort >>  e)
inline

Convert an integer expression to a string.

Definition at line 2013 of file Context.java.

2014  {
2015  return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
2016  }

◆ then()

Tactic then ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
)
inline

Create a tactic that applies

t1

to a Goal and then

t2

to every subgoal produced by

t1

Remarks: Shorthand for

.

Definition at line 2782 of file Context.java.

2783  {
2784  return andThen(t1, t2, ts);
2785  }

◆ tryFor()

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

2807  {
2808  checkContextMatch(t);
2809  return new Tactic(this, Native.tacticTryFor(nCtx(),
2810  t.getNativeObject(), ms));
2811  }

◆ unwrapAST()

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

3957  {
3958  return a.getNativeObject();
3959  }

◆ updateParamValue()

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

3987  {
3988  Native.updateParamValue(nCtx(), id, value);
3989  }

◆ usingParams()

Tactic usingParams ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

.

Definition at line 2892 of file Context.java.

2893  {
2894  checkContextMatch(t);
2895  checkContextMatch(p);
2896  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2897  t.getNativeObject(), p.getNativeObject()));
2898  }

◆ when()

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

2820  {
2821  checkContextMatch(t);
2822  checkContextMatch(p);
2823  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2824  t.getNativeObject()));
2825  }

◆ with()

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

2907  {
2908  return usingParams(t, p);
2909  }

◆ wrapAST()

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

3940  {
3941  return AST.create(this, nativeObject);
3942  }
com.microsoft.z3.Context.mkFalse
BoolExpr mkFalse()
Definition: Context.java:708
com.microsoft.z3.Context.getBoolSort
BoolSort getBoolSort()
Definition: Context.java:128
z3py.TupleSort
def TupleSort(name, sorts, ctx=None)
Definition: z3py.py:5012
com.microsoft.z3.Context.not
Probe not(Probe p)
Definition: Context.java:3076
z3py.RealSort
def RealSort(ctx=None)
Definition: z3py.py:2958
com.microsoft.z3.Context.or
Probe or(Probe p1, Probe p2)
Definition: Context.java:3065
com.microsoft.z3.Context.mkFPNumeral
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3379
com.microsoft.z3.Context.mkSymbol
IntSymbol mkSymbol(int i)
Definition: Context.java:94
com.microsoft.z3.Context.mkBitVecSort
BitVecSort mkBitVecSort(int size)
Definition: Context.java:213
com.microsoft.z3.Context.mkSolver
Solver mkSolver()
Definition: Context.java:3089
com.microsoft.z3.Context.andThen
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2750
com.microsoft.z3.Context.getIntSort
IntSort getIntSort()
Definition: Context.java:139
com.microsoft.z3.Context.lt
Probe lt(Probe p1, Probe p2)
Definition: Context.java:2993
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:3992
z3::mod
expr mod(expr const &a, expr const &b)
Definition: z3++.h:1399
com.microsoft.z3.Context.mkDatatypeSorts
DatatypeSort< Object >[] mkDatatypeSorts(Symbol[] names, Constructor< Object >[][] c)
Definition: Context.java:387
com.microsoft.z3.Context.getNumProbes
int getNumProbes()
Definition: Context.java:2946
com.microsoft.z3.Context.skip
Tactic skip()
Definition: Context.java:2855
z3py.FPSort
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9225
com.microsoft.z3.Context.and
Probe and(Probe p1, Probe p2)
Definition: Context.java:3054
com.microsoft.z3.Context.getRealSort
RealSort getRealSort()
Definition: Context.java:150
z3::max
expr max(expr const &a, expr const &b)
Definition: z3++.h:1724
z3py.BitVecSort
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3781
z3::rem
expr rem(expr const &a, expr const &b)
Definition: z3++.h:1415
z3
Z3 C++ namespace.
Definition: z3++.h:48
z3py.AndThen
def AndThen(*ts, **ks)
Definition: z3py.py:7789
z3py.IntSort
def IntSort(ctx=None)
Definition: z3py.py:2942
com.microsoft.z3.Context.getNumTactics
int getNumTactics()
Definition: Context.java:2711
com.microsoft.z3.Context.mkForall
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2480
z3py.Map
def Map(f, *args)
Definition: z3py.py:4520
com.microsoft.z3.Context.mkTrue
BoolExpr mkTrue()
Definition: Context.java:700
com.microsoft.z3.Context.mkExists
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2505
com.microsoft.z3.Context.mkUninterpretedSort
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:180
z3py.BoolSort
def BoolSort(ctx=None)
Definition: z3py.py:1553
com.microsoft.z3.Context.usingParams
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2892
com.microsoft.z3.Context.mkStringSort
SeqSort< BitVecSort > mkStringSort()
Definition: Context.java:242
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10130