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)
 
final 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)
 
final< R extends Sort > Expr< R > mkApp (FuncDecl< R > f, Expr<?>... args)
 
BoolExpr mkTrue ()
 
BoolExpr mkFalse ()
 
BoolExpr mkBool (boolean value)
 
BoolExpr mkEq (Expr<?> x, Expr<?> y)
 
final BoolExpr mkDistinct (Expr<?>... args)
 
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)
 
final BoolExpr mkAnd (Expr< BoolSort >... t)
 
final BoolExpr mkOr (Expr< BoolSort >... t)
 
final< R extends ArithSort > ArithExpr< R > mkAdd (Expr<? extends R >... t)
 
final< R extends ArithSort > ArithExpr< R > mkMul (Expr<? extends R >... t)
 
final< R extends ArithSort > ArithExpr< R > mkSub (Expr<? extends R >... t)
 
IntExpr mkMod (Expr< IntSort > t1, Expr< IntSort > t2)
 
IntExpr mkRem (Expr< IntSort > t1, Expr< IntSort > t2)
 
BoolExpr mkLt (Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
 
BoolExpr mkLe (Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
 
BoolExpr mkGt (Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
 
BoolExpr mkGe (Expr<? extends ArithSort > t1, Expr<? extends ArithSort > 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)
 
final< D extends Sort, R1 extends Sort, R2 extends Sort > ArrayExpr< D, R2 > mkMap (FuncDecl< R2 > f, Expr< ArraySort< D, R1 > >... args)
 
final< D extends Sort > ArrayExpr< D, BoolSortmkSetUnion (Expr< ArraySort< D, BoolSort > >... args)
 
final< D extends Sort > ArrayExpr< D, BoolSortmkSetIntersection (Expr< ArraySort< D, BoolSort > >... args)
 
SeqExpr< BitVecSortmkString (String s)
 
SeqExpr< BitVecSortintToString (Expr< IntSort > e)
 
IntExpr stringToInt (Expr< SeqSort< BitVecSort > > e)
 
final< R extends Sort > SeqExpr< R > mkConcat (Expr< SeqSort< R > >... t)
 
final< R extends Sort > ReExpr< R > mkConcat (ReExpr< R >... t)
 
final< R extends Sort > ReExpr< R > mkUnion (Expr< ReSort< R > >... t)
 
final< R extends Sort > ReExpr< R > mkIntersect (Expr< ReSort< R > >... t)
 
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 }
def Map(f, *args)
Definition: z3py.py:4757
def String(name, ctx=None)
Definition: z3py.py:10693

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

3071 {
3072 checkContextMatch(p1);
3073 checkContextMatch(p2);
3074 return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
3075 p2.getNativeObject()));
3076 }

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

2768 {
2769 checkContextMatch(t1);
2770 checkContextMatch(t2);
2771 checkContextMatch(ts);
2772
2773 long last = 0;
2774 if (ts != null && ts.length > 0)
2775 {
2776 last = ts[ts.length - 1].getNativeObject();
2777 for (int i = ts.length - 2; i >= 0; i--) {
2778 last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2779 last);
2780 }
2781 }
2782 if (last != 0)
2783 {
2784 last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2785 return new Tactic(this, Native.tacticAndThen(nCtx(),
2786 t1.getNativeObject(), last));
2787 } else
2788 return new Tactic(this, Native.tacticAndThen(nCtx(),
2789 t1.getNativeObject(), t2.getNativeObject()));
2790 }

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

2647 {
2648
2649 return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2650 attributes, assumptions.length,
2651 AST.arrayToNative(assumptions), formula.getNativeObject());
2652 }

◆ close()

void close ( )
inline

Disposes of the context.

Definition at line 4154 of file Context.java.

4155 {
4156 m_AST_DRQ.forceClear(this);
4157 m_ASTMap_DRQ.forceClear(this);
4158 m_ASTVector_DRQ.forceClear(this);
4159 m_ApplyResult_DRQ.forceClear(this);
4160 m_FuncEntry_DRQ.forceClear(this);
4161 m_FuncInterp_DRQ.forceClear(this);
4162 m_Goal_DRQ.forceClear(this);
4163 m_Model_DRQ.forceClear(this);
4164 m_Params_DRQ.forceClear(this);
4165 m_Probe_DRQ.forceClear(this);
4166 m_Solver_DRQ.forceClear(this);
4167 m_Optimize_DRQ.forceClear(this);
4168 m_Statistics_DRQ.forceClear(this);
4169 m_Tactic_DRQ.forceClear(this);
4170 m_Fixedpoint_DRQ.forceClear(this);
4171
4172 m_boolSort = null;
4173 m_intSort = null;
4174 m_realSort = null;
4175 m_stringSort = null;
4176
4177 synchronized (creation_lock) {
4178 Native.delContext(m_ctx);
4179 }
4180 m_ctx = 0;
4181 }

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

2849 {
2850 checkContextMatch(p);
2851 checkContextMatch(t1);
2852 checkContextMatch(t2);
2853 return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2854 t1.getNativeObject(), t2.getNativeObject()));
2855 }

◆ constProbe()

Probe constProbe ( double  val)
inline

Create a probe that always evaluates to val.

Definition at line 3000 of file Context.java.

3001 {
3002 return new Probe(this, Native.probeConst(nCtx(), val));
3003 }

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

3060 {
3061 checkContextMatch(p1);
3062 checkContextMatch(p2);
3063 return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
3064 p2.getNativeObject()));
3065 }

Referenced by AstRef.__eq__(), UserPropagateBase.add_eq(), SortRef.cast(), and BoolSortRef.cast().

◆ fail()

Tactic fail ( )
inline

Create a tactic always fails.

Definition at line 2879 of file Context.java.

2880 {
2881 return new Tactic(this, Native.tacticFail(nCtx()));
2882 }

◆ failIf()

Tactic failIf ( Probe  p)
inline

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

Definition at line 2888 of file Context.java.

2889 {
2890 checkContextMatch(p);
2891 return new Tactic(this,
2892 Native.tacticFailIf(nCtx(), p.getNativeObject()));
2893 }

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

2900 {
2901 return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2902 }

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

3048 {
3049 checkContextMatch(p1);
3050 checkContextMatch(p2);
3051 return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
3052 p2.getNativeObject()));
3053 }

◆ getApplyResultDRQ()

IDecRefQueue< ApplyResult > getApplyResultDRQ ( )
inline

Definition at line 4085 of file Context.java.

4086 {
4087 return m_ApplyResult_DRQ;
4088 }

◆ getASTDRQ()

IDecRefQueue< AST > getASTDRQ ( )
inline

Definition at line 4070 of file Context.java.

4071 {
4072 return m_AST_DRQ;
4073 }

◆ getASTMapDRQ()

IDecRefQueue< ASTMap > getASTMapDRQ ( )
inline

Definition at line 4075 of file Context.java.

4076 {
4077 return m_ASTMap_DRQ;
4078 }

◆ getASTVectorDRQ()

IDecRefQueue< ASTVector > getASTVectorDRQ ( )
inline

Definition at line 4080 of file Context.java.

4081 {
4082 return m_ASTVector_DRQ;
4083 }

◆ 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 }
def BoolSort(ctx=None)
Definition: z3py.py:1655

◆ getConstructorDRQ()

IDecRefQueue< Constructor<?> > getConstructorDRQ ( )
inline

Definition at line 4062 of file Context.java.

4062 {
4063 return m_Constructor_DRQ;
4064 }

◆ getConstructorListDRQ()

IDecRefQueue< ConstructorList<?> > getConstructorListDRQ ( )
inline

Definition at line 4066 of file Context.java.

4066 {
4067 return m_ConstructorList_DRQ;
4068 }

◆ getFixedpointDRQ()

IDecRefQueue< Fixedpoint > getFixedpointDRQ ( )
inline

Definition at line 4140 of file Context.java.

4141 {
4142 return m_Fixedpoint_DRQ;
4143 }

◆ getFuncEntryDRQ()

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

Definition at line 4090 of file Context.java.

4091 {
4092 return m_FuncEntry_DRQ;
4093 }

◆ getFuncInterpDRQ()

IDecRefQueue< FuncInterp<?> > getFuncInterpDRQ ( )
inline

Definition at line 4095 of file Context.java.

4096 {
4097 return m_FuncInterp_DRQ;
4098 }

◆ getGoalDRQ()

IDecRefQueue< Goal > getGoalDRQ ( )
inline

Definition at line 4100 of file Context.java.

4101 {
4102 return m_Goal_DRQ;
4103 }

◆ 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 }
def IntSort(ctx=None)
Definition: z3py.py:3100

◆ getModelDRQ()

IDecRefQueue< Model > getModelDRQ ( )
inline

Definition at line 4105 of file Context.java.

4106 {
4107 return m_Model_DRQ;
4108 }

◆ getNumProbes()

int getNumProbes ( )
inline

The number of supported Probes.

Definition at line 2962 of file Context.java.

2963 {
2964 return Native.getNumProbes(nCtx());
2965 }

◆ getNumTactics()

int getNumTactics ( )
inline

The number of supported tactics.

Definition at line 2727 of file Context.java.

2728 {
2729 return Native.getNumTactics(nCtx());
2730 }

◆ getOptimizeDRQ()

IDecRefQueue< Optimize > getOptimizeDRQ ( )
inline

Definition at line 4145 of file Context.java.

4146 {
4147 return m_Optimize_DRQ;
4148 }

◆ getParamDescrsDRQ()

IDecRefQueue< ParamDescrs > getParamDescrsDRQ ( )
inline

Definition at line 4115 of file Context.java.

4116 {
4117 return m_ParamDescrs_DRQ;
4118 }

◆ getParamsDRQ()

IDecRefQueue< Params > getParamsDRQ ( )
inline

Definition at line 4110 of file Context.java.

4111 {
4112 return m_Params_DRQ;
4113 }

◆ getProbeDescription()

String getProbeDescription ( String  name)
inline

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

Definition at line 2984 of file Context.java.

2985 {
2986 return Native.probeGetDescr(nCtx(), name);
2987 }

◆ getProbeDRQ()

IDecRefQueue< Probe > getProbeDRQ ( )
inline

Definition at line 4120 of file Context.java.

4121 {
4122 return m_Probe_DRQ;
4123 }

◆ getProbeNames()

String[] getProbeNames ( )
inline

The names of all supported Probes.

Definition at line 2970 of file Context.java.

2971 {
2972
2973 int n = getNumProbes();
2974 String[] res = new String[n];
2975 for (int i = 0; i < n; i++)
2976 res[i] = Native.getProbeName(nCtx(), i);
2977 return res;
2978 }

◆ 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 }
def RealSort(ctx=None)
Definition: z3py.py:3117

◆ getSimplifyParameterDescriptions()

ParamDescrs getSimplifyParameterDescriptions ( )
inline

Retrieves parameter descriptions for simplifier.

Definition at line 3989 of file Context.java.

3990 {
3991 return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3992 }

◆ getSolverDRQ()

IDecRefQueue< Solver > getSolverDRQ ( )
inline

Definition at line 4125 of file Context.java.

4126 {
4127 return m_Solver_DRQ;
4128 }

◆ getStatisticsDRQ()

IDecRefQueue< Statistics > getStatisticsDRQ ( )
inline

Definition at line 4130 of file Context.java.

4131 {
4132 return m_Statistics_DRQ;
4133 }

◆ 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 }
SeqSort< BitVecSort > mkStringSort()
Definition: Context.java:242

◆ getTacticDescription()

String getTacticDescription ( String  name)
inline

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

Definition at line 2749 of file Context.java.

2750 {
2751 return Native.tacticGetDescr(nCtx(), name);
2752 }

◆ getTacticDRQ()

IDecRefQueue< Tactic > getTacticDRQ ( )
inline

Definition at line 4135 of file Context.java.

4136 {
4137 return m_Tactic_DRQ;
4138 }

◆ getTacticNames()

String[] getTacticNames ( )
inline

The names of all supported tactics.

Definition at line 2735 of file Context.java.

2736 {
2737
2738 int n = getNumTactics();
2739 String[] res = new String[n];
2740 for (int i = 0; i < n; i++)
2741 res[i] = Native.getTacticName(nCtx(), i);
2742 return res;
2743 }

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

3022 {
3023 checkContextMatch(p1);
3024 checkContextMatch(p2);
3025 return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
3026 p2.getNativeObject()));
3027 }

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

2955 {
2956 Native.interrupt(nCtx());
2957 }

◆ intToString()

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

Convert an integer expression to a string.

Definition at line 2017 of file Context.java.

2018 {
2019 return (SeqExpr<BitVecSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
2020 }

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

3035 {
3036 checkContextMatch(p1);
3037 checkContextMatch(p2);
3038 return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
3039 p2.getNativeObject()));
3040 }

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

3010 {
3011 checkContextMatch(p1);
3012 checkContextMatch(p2);
3013 return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
3014 p2.getNativeObject()));
3015 }

◆ mkAdd()

final< R extends ArithSort > ArithExpr< R > mkAdd ( Expr<? extends R >...  t)
inline

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

Definition at line 829 of file Context.java.

830 {
831 checkContextMatch(t);
832 return (ArithExpr<R>) Expr.create(this,
833 Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
834 }

◆ mkAnd()

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

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

Definition at line 807 of file Context.java.

808 {
809 checkContextMatch(t);
810 return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
811 AST.arrayToNative(t)));
812 }

Referenced by Goal.AsBoolExpr().

◆ mkApp()

final< R extends Sort > Expr< R > mkApp ( FuncDecl< R >  f,
Expr<?>...  args 
)
inline

Create a new function application.

Definition at line 692 of file Context.java.

693 {
694 checkContextMatch(f);
695 checkContextMatch(args);
696 return Expr.create(this, f, args);
697 }

Referenced by ListSort< R extends Sort >.getNil().

◆ mkAtLeast()

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

Create an at-least-k constraint.

Definition at line 2263 of file Context.java.

2264 {
2265 checkContextMatch(args);
2266 return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
2267 }

◆ mkAtMost()

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

Create an at-most-k constraint.

Definition at line 2254 of file Context.java.

2255 {
2256 checkContextMatch(args);
2257 return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
2258 }

◆ 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 }
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3967

◆ mkBool()

BoolExpr mkBool ( boolean  value)
inline

Creates a Boolean value.

Definition at line 718 of file Context.java.

719 {
720 return value ? mkTrue() : mkFalse();
721 }

◆ mkBoolConst() [1/2]

BoolExpr mkBoolConst ( String  name)
inline

Create a Boolean constant.

Definition at line 635 of file Context.java.

636 {
637 return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
638 }
IntSymbol mkSymbol(int i)
Definition: Context.java:94

◆ mkBoolConst() [2/2]

BoolExpr mkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 627 of file Context.java.

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

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

2457 {
2458 return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2459 }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:213

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

2467 {
2468 return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2469 }

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

2447 {
2448 return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2449 }

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

1568 {
1569 checkContextMatch(t);
1570 return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1571 (signed)));
1572 }

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

1131 {
1132 checkContextMatch(t1);
1133 checkContextMatch(t2);
1134 return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1135 t1.getNativeObject(), t2.getNativeObject()));
1136 }

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

1581 {
1582 checkContextMatch(t1);
1583 checkContextMatch(t2);
1584 return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1585 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1586 }

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

1595 {
1596 checkContextMatch(t1);
1597 checkContextMatch(t2);
1598 return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1599 t1.getNativeObject(), t2.getNativeObject()));
1600 }

◆ mkBVAND()

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

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

Definition at line 1041 of file Context.java.

1042 {
1043 checkContextMatch(t1);
1044 checkContextMatch(t2);
1045 return new BitVecExpr(this, Native.mkBvand(nCtx(),
1046 t1.getNativeObject(), t2.getNativeObject()));
1047 }

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

1476 {
1477 checkContextMatch(t1);
1478 checkContextMatch(t2);
1479 return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1480 t1.getNativeObject(), t2.getNativeObject()));
1481 }

◆ mkBVConst() [1/2]

BitVecExpr mkBVConst ( String  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 683 of file Context.java.

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

◆ mkBVConst() [2/2]

BitVecExpr mkBVConst ( Symbol  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 675 of file Context.java.

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

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

1456 {
1457 checkContextMatch(t1);
1458 checkContextMatch(t2);
1459 return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1460 t1.getNativeObject(), t2.getNativeObject()));
1461 }

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

1157 {
1158 checkContextMatch(t1);
1159 checkContextMatch(t2);
1160 return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1161 t1.getNativeObject(), t2.getNativeObject()));
1162 }

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

1663 {
1664 checkContextMatch(t1);
1665 checkContextMatch(t2);
1666 return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1667 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1668 }

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

1677 {
1678 checkContextMatch(t1);
1679 checkContextMatch(t2);
1680 return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1681 t1.getNativeObject(), t2.getNativeObject()));
1682 }

◆ mkBVNAND()

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

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

Definition at line 1080 of file Context.java.

1081 {
1082 checkContextMatch(t1);
1083 checkContextMatch(t2);
1084 return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1085 t1.getNativeObject(), t2.getNativeObject()));
1086 }

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

1120 {
1121 checkContextMatch(t);
1122 return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1123 }

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

1650 {
1651 checkContextMatch(t);
1652 return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1653 t.getNativeObject()));
1654 }

◆ mkBVNOR()

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

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

Definition at line 1093 of file Context.java.

1094 {
1095 checkContextMatch(t1);
1096 checkContextMatch(t2);
1097 return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1098 t1.getNativeObject(), t2.getNativeObject()));
1099 }

◆ mkBVNot()

BitVecExpr mkBVNot ( Expr< BitVecSort t)
inline

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

Definition at line 1006 of file Context.java.

1007 {
1008 checkContextMatch(t);
1009 return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
1010 }

◆ mkBVOR()

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

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

Definition at line 1054 of file Context.java.

1055 {
1056 checkContextMatch(t1);
1057 checkContextMatch(t2);
1058 return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1059 t2.getNativeObject()));
1060 }

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

1018 {
1019 checkContextMatch(t);
1020 return new BitVecExpr(this, Native.mkBvredand(nCtx(),
1021 t.getNativeObject()));
1022 }

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

1030 {
1031 checkContextMatch(t);
1032 return new BitVecExpr(this, Native.mkBvredor(nCtx(),
1033 t.getNativeObject()));
1034 }

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

1515 {
1516 checkContextMatch(t1);
1517 checkContextMatch(t2);
1518 return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1519 t1.getNativeObject(), t2.getNativeObject()));
1520 }

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

1489 {
1490 checkContextMatch(t);
1491 return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1492 t.getNativeObject()));
1493 }

◆ mkBVRotateRight() [1/2]

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

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

Definition at line 1528 of file Context.java.

1530 {
1531 checkContextMatch(t1);
1532 checkContextMatch(t2);
1533 return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1534 t1.getNativeObject(), t2.getNativeObject()));
1535 }

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

1501 {
1502 checkContextMatch(t);
1503 return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1504 t.getNativeObject()));
1505 }

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

1193 {
1194 checkContextMatch(t1);
1195 checkContextMatch(t2);
1196 return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1197 t1.getNativeObject(), t2.getNativeObject()));
1198 }

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

1637 {
1638 checkContextMatch(t1);
1639 checkContextMatch(t2);
1640 return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1641 t1.getNativeObject(), t2.getNativeObject()));
1642 }

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

1318 {
1319 checkContextMatch(t1);
1320 checkContextMatch(t2);
1321 return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1322 t2.getNativeObject()));
1323 }

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

1344 {
1345 checkContextMatch(t1);
1346 checkContextMatch(t2);
1347 return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1348 t2.getNativeObject()));
1349 }

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

1437 {
1438 checkContextMatch(t1);
1439 checkContextMatch(t2);
1440 return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1441 t1.getNativeObject(), t2.getNativeObject()));
1442 }

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

1292 {
1293 checkContextMatch(t1);
1294 checkContextMatch(t2);
1295 return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1296 t2.getNativeObject()));
1297 }

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

1266 {
1267 checkContextMatch(t1);
1268 checkContextMatch(t2);
1269 return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1270 t2.getNativeObject()));
1271 }

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

1240 {
1241 checkContextMatch(t1);
1242 checkContextMatch(t2);
1243 return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1244 t1.getNativeObject(), t2.getNativeObject()));
1245 }

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

1226 {
1227 checkContextMatch(t1);
1228 checkContextMatch(t2);
1229 return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1230 t1.getNativeObject(), t2.getNativeObject()));
1231 }

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

1144 {
1145 checkContextMatch(t1);
1146 checkContextMatch(t2);
1147 return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1148 t1.getNativeObject(), t2.getNativeObject()));
1149 }

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

1609 {
1610 checkContextMatch(t1);
1611 checkContextMatch(t2);
1612 return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1613 t1.getNativeObject(), t2.getNativeObject()));
1614 }

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

1623 {
1624 checkContextMatch(t1);
1625 checkContextMatch(t2);
1626 return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1627 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1628 }

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

1172 {
1173 checkContextMatch(t1);
1174 checkContextMatch(t2);
1175 return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1176 t1.getNativeObject(), t2.getNativeObject()));
1177 }

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

1305 {
1306 checkContextMatch(t1);
1307 checkContextMatch(t2);
1308 return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1309 t2.getNativeObject()));
1310 }

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

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

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

1279 {
1280 checkContextMatch(t1);
1281 checkContextMatch(t2);
1282 return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1283 t2.getNativeObject()));
1284 }

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

1253 {
1254 checkContextMatch(t1);
1255 checkContextMatch(t2);
1256 return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1257 t2.getNativeObject()));
1258 }

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

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

◆ mkBVXNOR()

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

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

Definition at line 1106 of file Context.java.

1107 {
1108 checkContextMatch(t1);
1109 checkContextMatch(t2);
1110 return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1111 t1.getNativeObject(), t2.getNativeObject()));
1112 }

◆ mkBVXOR()

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

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

Definition at line 1067 of file Context.java.

1068 {
1069 checkContextMatch(t1);
1070 checkContextMatch(t2);
1071 return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1072 t1.getNativeObject(), t2.getNativeObject()));
1073 }

◆ mkConcat() [1/3]

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

1362 {
1363 checkContextMatch(t1);
1364 checkContextMatch(t2);
1365 return new BitVecExpr(this, Native.mkConcat(nCtx(),
1366 t1.getNativeObject(), t2.getNativeObject()));
1367 }

◆ mkConcat() [2/3]

final< R extends Sort > SeqExpr< R > mkConcat ( Expr< SeqSort< R > >...  t)
inline

Concatenate sequences.

Definition at line 2034 of file Context.java.

2035 {
2036 checkContextMatch(t);
2037 return (SeqExpr<R>) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
2038 }

◆ mkConcat() [3/3]

final< R extends Sort > ReExpr< R > mkConcat ( ReExpr< R >...  t)
inline

Create the concatenation of regular languages.

Definition at line 2199 of file Context.java.

2200 {
2201 checkContextMatch(t);
2202 return (ReExpr<R>) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2203 }

◆ 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 }
DatatypeSort< Object >[] mkDatatypeSorts(Symbol[] names, Constructor< Object >[][] c)
Definition: Context.java:387

◆ 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 }

◆ mkDistinct()

final BoolExpr mkDistinct ( Expr<?>...  args)
inline

Creates a distinct term.

Definition at line 738 of file Context.java.

739 {
740 checkContextMatch(args);
741 return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
742 AST.arrayToNative(args)));
743 }

◆ mkEq()

BoolExpr mkEq ( Expr<?>  x,
Expr<?>  y 
)
inline

Creates the equality x = y

Definition at line 726 of file Context.java.

727 {
728 checkContextMatch(x);
729 checkContextMatch(y);
730 return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
731 y.getNativeObject()));
732 }

◆ 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<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol)

Definition at line 2534 of file Context.java.

2537 {
2538
2539 return Quantifier.of(this, false, boundConstants, body, weight,
2540 patterns, noPatterns, quantifierID, skolemID);
2541 }

◆ 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<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol)

Definition at line 2521 of file Context.java.

2524 {
2525
2526 return Quantifier.of(this, false, sorts, names, body, weight,
2527 patterns, noPatterns, quantifierID, skolemID);
2528 }

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

1379 {
1380 checkContextMatch(t);
1381 return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1382 t.getNativeObject()));
1383 }

◆ mkFalse()

BoolExpr mkFalse ( )
inline

The false Term.

Definition at line 710 of file Context.java.

711 {
712 return new BoolExpr(this, Native.mkFalse(nCtx()));
713 }

◆ mkFixedpoint()

Fixedpoint mkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3160 of file Context.java.

3161 {
3162 return new Fixedpoint(this);
3163 }

◆ 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<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol)

Definition at line 2508 of file Context.java.

2511 {
2512
2513 return Quantifier.of(this, true, boundConstants, body, weight,
2514 patterns, noPatterns, quantifierID, skolemID);
2515 }

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

2499 {
2500 return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2501 noPatterns, quantifierID, skolemID);
2502 }

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

3491 {
3492 return mkFPNumeral(sgn, exp, sig, s);
3493 }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3395

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

3504 {
3505 return mkFPNumeral(sgn, exp, sig, s);
3506 }

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

3466 {
3467 return mkFPNumeral(v, s);
3468 }

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

3789 {
3790 return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3791 }

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

3455 {
3456 return mkFPNumeral(v, s);
3457 }

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

3478 {
3479 return mkFPNumeral(v, s);
3480 }

◆ mkFPAbs()

FPExpr mkFPAbs ( Expr< FPSort t)
inline

Floating-point absolute value

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3514 of file Context.java.

3515 {
3516 return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3517 }

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

3537 {
3538 return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3539 }

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

3573 {
3574 return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3575 }

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

3701 {
3702 return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3703 }

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

3588 {
3589 return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3590 }

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

3677 {
3678 return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3679 }

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

3688 {
3689 return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3690 }

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

3374 {
3375 return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3376 }

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

3741 {
3742 return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3743 }

◆ mkFPIsNaN()

BoolExpr mkFPIsNaN ( Expr< FPSort t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3750 of file Context.java.

3751 {
3752 return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3753 }

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

3761 {
3762 return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3763 }

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

3711 {
3712 return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3713 }

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

3771 {
3772 return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3773 }

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

3721 {
3722 return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3723 }

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

3731 {
3732 return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3733 }

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

3655 {
3656 return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3657 }

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

3666 {
3667 return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3668 }

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

3644 {
3645 return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3646 }

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

3633 {
3634 return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3635 }

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

3561 {
3562 return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3563 }

◆ mkFPNaN()

FPNum mkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3362 of file Context.java.

3363 {
3364 return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3365 }

◆ mkFPNeg()

FPExpr mkFPNeg ( Expr< FPSort t)
inline

Floating-point negation

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3524 of file Context.java.

3525 {
3526 return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3527 }

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

3431 {
3432 return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3433 }

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

3444 {
3445 return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3446 }

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

3407 {
3408 return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3409 }

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

3396 {
3397 return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3398 }

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

3418 {
3419 return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3420 }

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

3610 {
3611 return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3612 }

◆ mkFPRNA()

FPRMNum mkFPRNA ( )
inline

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

Exceptions
Z3Exception

Definition at line 3214 of file Context.java.

3215 {
3216 return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3217 }

◆ mkFPRNE()

FPRMNum mkFPRNE ( )
inline

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

Exceptions
Z3Exception

Definition at line 3196 of file Context.java.

3197 {
3198 return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3199 }

◆ mkFPRoundingModeSort()

FPRMSort mkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Exceptions
Z3Exception

Definition at line 3178 of file Context.java.

3179 {
3180 return new FPRMSort(this);
3181 }

◆ mkFPRoundNearestTiesToAway()

FPRMNum mkFPRoundNearestTiesToAway ( )
inline

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

Exceptions
Z3Exception

Definition at line 3205 of file Context.java.

3206 {
3207 return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3208 }

◆ mkFPRoundNearestTiesToEven()

FPRMExpr mkFPRoundNearestTiesToEven ( )
inline

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

Exceptions
Z3Exception

Definition at line 3187 of file Context.java.

3188 {
3189 return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3190 }

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

3622 {
3623 return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3624 }

◆ mkFPRoundTowardNegative()

FPRMNum mkFPRoundTowardNegative ( )
inline

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

Exceptions
Z3Exception

Definition at line 3241 of file Context.java.

3242 {
3243 return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3244 }

◆ mkFPRoundTowardPositive()

FPRMNum mkFPRoundTowardPositive ( )
inline

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

Exceptions
Z3Exception

Definition at line 3223 of file Context.java.

3224 {
3225 return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3226 }

◆ mkFPRoundTowardZero()

FPRMNum mkFPRoundTowardZero ( )
inline

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

Exceptions
Z3Exception

Definition at line 3259 of file Context.java.

3260 {
3261 return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3262 }

◆ mkFPRTN()

FPRMNum mkFPRTN ( )
inline

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

Exceptions
Z3Exception

Definition at line 3250 of file Context.java.

3251 {
3252 return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3253 }

◆ mkFPRTP()

FPRMNum mkFPRTP ( )
inline

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

Exceptions
Z3Exception

Definition at line 3232 of file Context.java.

3233 {
3234 return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3235 }

◆ mkFPRTZ()

FPRMNum mkFPRTZ ( )
inline

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

Exceptions
Z3Exception

Definition at line 3268 of file Context.java.

3269 {
3270 return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3271 }

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

3280 {
3281 return new FPSort(this, ebits, sbits);
3282 }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9727

◆ mkFPSort128()

FPSort mkFPSort128 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3351 of file Context.java.

3352 {
3353 return new FPSort(this, Native.mkFpaSort128(nCtx()));
3354 }

◆ mkFPSort16()

FPSort mkFPSort16 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3297 of file Context.java.

3298 {
3299 return new FPSort(this, Native.mkFpaSort16(nCtx()));
3300 }

◆ mkFPSort32()

FPSort mkFPSort32 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3315 of file Context.java.

3316 {
3317 return new FPSort(this, Native.mkFpaSort32(nCtx()));
3318 }

◆ mkFPSort64()

FPSort mkFPSort64 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3333 of file Context.java.

3334 {
3335 return new FPSort(this, Native.mkFpaSort64(nCtx()));
3336 }

◆ mkFPSortDouble()

FPSort mkFPSortDouble ( )
inline

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

Exceptions
Z3Exception

Definition at line 3324 of file Context.java.

3325 {
3326 return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3327 }

◆ mkFPSortHalf()

FPSort mkFPSortHalf ( )
inline

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

Exceptions
Z3Exception

Definition at line 3288 of file Context.java.

3289 {
3290 return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3291 }

◆ mkFPSortQuadruple()

FPSort mkFPSortQuadruple ( )
inline

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

Exceptions
Z3Exception

Definition at line 3342 of file Context.java.

3343 {
3344 return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3345 }

◆ mkFPSortSingle()

FPSort mkFPSortSingle ( )
inline

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

Exceptions
Z3Exception

Definition at line 3306 of file Context.java.

3307 {
3308 return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3309 }

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

3599 {
3600 return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3601 }

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

3549 {
3550 return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3551 }

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

3890 {
3891 if (signed)
3892 return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3893 else
3894 return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3895 }

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

3805 {
3806 return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3807 }

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

3855 {
3856 if (signed)
3857 return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3858 else
3859 return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3860 }

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

3940 {
3941 return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3942 }

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

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

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

3837 {
3838 return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3839 }

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

3873 {
3874 return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3875 }

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

3922 {
3923 return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3924 }

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

3907 {
3908 return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3909 }

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

3385 {
3386 return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3387 }

◆ mkGe()

BoolExpr mkGe ( Expr<? extends ArithSort t1,
Expr<? extends ArithSort t2 
)
inline

Create an expression representing t1 &gt;= t2

Definition at line 955 of file Context.java.

956 {
957 checkContextMatch(t1);
958 checkContextMatch(t2);
959 return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
960 t2.getNativeObject()));
961 }

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

2712 {
2713 return new Goal(this, models, unsatCores, proofs);
2714 }

◆ mkGt()

BoolExpr mkGt ( Expr<? extends ArithSort t1,
Expr<? extends ArithSort t2 
)
inline

Create an expression representing t1 &gt; t2

Definition at line 944 of file Context.java.

945 {
946 checkContextMatch(t1);
947 checkContextMatch(t2);
948 return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
949 t2.getNativeObject()));
950 }

◆ mkIff()

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

Create an expression representing t1 iff t2.

Definition at line 773 of file Context.java.

774 {
775 checkContextMatch(t1);
776 checkContextMatch(t2);
777 return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
778 t2.getNativeObject()));
779 }

◆ mkImplies()

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

Create an expression representing t1 -> t2.

Definition at line 784 of file Context.java.

785 {
786 checkContextMatch(t1);
787 checkContextMatch(t2);
788 return new BoolExpr(this, Native.mkImplies(nCtx(),
789 t1.getNativeObject(), t2.getNativeObject()));
790 }

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

2422 {
2423
2424 return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2425 .getNativeObject()));
2426 }

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

2435 {
2436
2437 return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2438 .getNativeObject()));
2439 }

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

2409 {
2410
2411 return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2412 .getNativeObject()));
2413 }

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

1547 {
1548 checkContextMatch(t);
1549 return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1550 t.getNativeObject()));
1551 }

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

974 {
975 checkContextMatch(t);
976 return new RealExpr(this,
977 Native.mkInt2real(nCtx(), t.getNativeObject()));
978 }

◆ mkIntConst() [1/2]

IntExpr mkIntConst ( String  name)
inline

Creates an integer constant.

Definition at line 651 of file Context.java.

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

◆ mkIntConst() [2/2]

IntExpr mkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 643 of file Context.java.

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

◆ mkIntersect()

final< R extends Sort > ReExpr< R > mkIntersect ( Expr< ReSort< R > >...  t)
inline

Create the intersection of regular languages.

Definition at line 2219 of file Context.java.

2220 {
2221 checkContextMatch(t);
2222 return (ReExpr<R>) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
2223 }

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

996 {
997 checkContextMatch(t);
998 return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
999 }

◆ mkLe()

BoolExpr mkLe ( Expr<? extends ArithSort t1,
Expr<? extends ArithSort t2 
)
inline

Create an expression representing t1 &lt;= t2

Definition at line 933 of file Context.java.

934 {
935 checkContextMatch(t1);
936 checkContextMatch(t2);
937 return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
938 t2.getNativeObject()));
939 }

◆ mkLt()

BoolExpr mkLt ( Expr<? extends ArithSort t1,
Expr<? extends ArithSort t2 
)
inline

Create an expression representing t1 &lt; t2

Definition at line 922 of file Context.java.

923 {
924 checkContextMatch(t1);
925 checkContextMatch(t2);
926 return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
927 t2.getNativeObject()));
928 }

◆ mkMap()

final< D extends Sort, R1 extends Sort, R2 extends Sort > ArrayExpr< D, R2 > mkMap ( FuncDecl< R2 >  f,
Expr< ArraySort< D, R1 > >...  args 
)
inline

Maps f on the argument arrays. Remarks: Each element of args must be of an array sort [domain_i -> range_i]. The function declaration f must have type range_1 .. range_n -> range. v must have sort range. The sort of the result is [domain_i -> range].

See also
#mkArraySort
#mkSelect
#mkStore

Definition at line 1827 of file Context.java.

1828 {
1829 checkContextMatch(f);
1830 checkContextMatch(args);
1831 return (ArrayExpr<D, R2>) Expr.create(this, Native.mkMap(nCtx(),
1832 f.getNativeObject(), AST.arrayLength(args),
1833 AST.arrayToNative(args)));
1834 }

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

885 {
886 checkContextMatch(t1);
887 checkContextMatch(t2);
888 return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
889 t2.getNativeObject()));
890 }

◆ mkMul()

final< R extends ArithSort > ArithExpr< R > mkMul ( Expr<? extends R >...  t)
inline

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

Definition at line 840 of file Context.java.

841 {
842 checkContextMatch(t);
843 return (ArithExpr<R>) Expr.create(this,
844 Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
845 }

◆ mkNot()

BoolExpr mkNot ( Expr< BoolSort a)
inline

Create an expression representing not(a).

Definition at line 748 of file Context.java.

749 {
750 checkContextMatch(a);
751 return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
752 }

◆ mkOptimize()

Optimize mkOptimize ( )
inline

Create a Optimize context.

Definition at line 3168 of file Context.java.

3169 {
3170 return new Optimize(this);
3171 }

◆ mkOr()

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

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

Definition at line 818 of file Context.java.

819 {
820 checkContextMatch(t);
821 return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
822 AST.arrayToNative(t)));
823 }

◆ mkParams()

Params mkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2719 of file Context.java.

2720 {
2721 return new Params(this);
2722 }

◆ mkPattern()

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

Create a quantifier pattern.

Definition at line 570 of file Context.java.

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

◆ mkPBEq()

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

Create a pseudo-Boolean equal constraint.

Definition at line 2290 of file Context.java.

2291 {
2292 checkContextMatch(args);
2293 return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2294 }

◆ mkPBGe()

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

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

Definition at line 2281 of file Context.java.

2282 {
2283 checkContextMatch(args);
2284 return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2285 }

◆ mkPBLe()

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

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

Definition at line 2272 of file Context.java.

2273 {
2274 checkContextMatch(args);
2275 return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2276 }

◆ mkProbe()

Probe mkProbe ( String  name)
inline

Creates a new Probe.

Definition at line 2992 of file Context.java.

2993 {
2994 return new Probe(this, name);
2995 }

◆ 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<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol)

Definition at line 2565 of file Context.java.

2568 {
2569
2570 if (universal)
2571 return mkForall(boundConstants, body, weight, patterns, noPatterns,
2572 quantifierID, skolemID);
2573 else
2574 return mkExists(boundConstants, body, weight, patterns, noPatterns,
2575 quantifierID, skolemID);
2576 }
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2496
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2521

◆ 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<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol)

Definition at line 2547 of file Context.java.

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

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

2357 {
2358 if (den == 0) {
2359 throw new Z3Exception("Denominator is zero");
2360 }
2361
2362 return new RatNum(this, Native.mkReal(nCtx(), num, den));
2363 }

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

2385 {
2386
2387 return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2388 .getNativeObject()));
2389 }

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

2398 {
2399
2400 return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2401 .getNativeObject()));
2402 }

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

2372 {
2373
2374 return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2375 .getNativeObject()));
2376 }

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

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

◆ mkRealConst() [1/2]

RealExpr mkRealConst ( String  name)
inline

Creates a real constant.

Definition at line 667 of file Context.java.

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

◆ mkRealConst() [2/2]

RealExpr mkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 659 of file Context.java.

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

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

898 {
899 checkContextMatch(t1);
900 checkContextMatch(t2);
901 return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
902 t2.getNativeObject()));
903 }

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

1419 {
1420 checkContextMatch(t);
1421 return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1422 t.getNativeObject()));
1423 }

◆ mkSetIntersection()

final< D extends Sort > ArrayExpr< D, BoolSort > mkSetIntersection ( Expr< ArraySort< D, BoolSort > >...  args)
inline

Take the intersection of a list of sets.

Definition at line 1929 of file Context.java.

1930 {
1931 checkContextMatch(args);
1932 return (ArrayExpr<D, BoolSort>) Expr.create(this,
1933 Native.mkSetIntersect(nCtx(), args.length,
1934 AST.arrayToNative(args)));
1935 }

◆ mkSetUnion()

final< D extends Sort > ArrayExpr< D, BoolSort > mkSetUnion ( Expr< ArraySort< D, BoolSort > >...  args)
inline

Take the union of a list of sets.

Definition at line 1917 of file Context.java.

1918 {
1919 checkContextMatch(args);
1920 return (ArrayExpr<D, BoolSort>)Expr.create(this,
1921 Native.mkSetUnion(nCtx(), args.length,
1922 AST.arrayToNative(args)));
1923 }

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

1393 {
1394 checkContextMatch(t);
1395 return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1396 t.getNativeObject()));
1397 }

◆ mkSimpleSolver()

Solver mkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3139 of file Context.java.

3140 {
3141 return new Solver(this, Native.mkSimpleSolver(nCtx()));
3142 }

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

3106 {
3107 return mkSolver((Symbol) null);
3108 }

Referenced by Tactic.getSolver().

◆ mkSolver() [2/4]

Solver mkSolver ( String  logic)
inline

Creates a new (incremental) solver.

See also
mkSolver(Symbol)

Definition at line 3131 of file Context.java.

3132 {
3133 return mkSolver(mkSymbol(logic));
3134 }

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

3118 {
3119
3120 if (logic == null)
3121 return new Solver(this, Native.mkSolver(nCtx()));
3122 else
3123 return new Solver(this, Native.mkSolverForLogic(nCtx(),
3124 logic.getNativeObject()));
3125 }

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

3151 {
3152
3153 return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3154 t.getNativeObject()));
3155 }

◆ mkString()

SeqExpr< BitVecSort > mkString ( String  s)
inline

Create a string constant.

Definition at line 2009 of file Context.java.

2010 {
2011 return (SeqExpr<BitVecSort>) Expr.create(this, Native.mkString(nCtx(), s));
2012 }

◆ 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 }

◆ mkSub()

final< R extends ArithSort > ArithExpr< R > mkSub ( Expr<? extends R >...  t)
inline

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

Definition at line 851 of file Context.java.

852 {
853 checkContextMatch(t);
854 return (ArithExpr<R>) Expr.create(this,
855 Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
856 }

◆ 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 }

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

2758 {
2759 return new Tactic(this, name);
2760 }

Referenced by Goal.simplify().

◆ mkTrue()

BoolExpr mkTrue ( )
inline

The true Term.

Definition at line 702 of file Context.java.

703 {
704 return new BoolExpr(this, Native.mkTrue(nCtx()));
705 }

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 }
def TupleSort(name, sorts, ctx=None)
Definition: z3py.py:5293

◆ 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 }
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:180

◆ 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 }

◆ mkUnion()

final< R extends Sort > ReExpr< R > mkUnion ( Expr< ReSort< R > >...  t)
inline

Create the union of regular languages.

Definition at line 2209 of file Context.java.

2210 {
2211 checkContextMatch(t);
2212 return (ReExpr<R>) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2213 }

◆ mkXor()

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

Create an expression representing t1 xor t2.

Definition at line 795 of file Context.java.

796 {
797 checkContextMatch(t1);
798 checkContextMatch(t2);
799 return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
800 t2.getNativeObject()));
801 }

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

1407 {
1408 checkContextMatch(t);
1409 return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1410 t.getNativeObject()));
1411 }

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

3093 {
3094 checkContextMatch(p);
3095 return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
3096 }

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

3082 {
3083 checkContextMatch(p1);
3084 checkContextMatch(p2);
3085 return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
3086 p2.getNativeObject()));
3087 }

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

2809 {
2810 checkContextMatch(t1);
2811 checkContextMatch(t2);
2812 return new Tactic(this, Native.tacticOrElse(nCtx(),
2813 t1.getNativeObject(), t2.getNativeObject()));
2814 }

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

2942 {
2943 checkContextMatch(t1);
2944 checkContextMatch(t2);
2945 return new Tactic(this, Native.tacticParAndThen(nCtx(),
2946 t1.getNativeObject(), t2.getNativeObject()));
2947 }

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

2931 {
2932 checkContextMatch(t);
2933 return new Tactic(this, Native.tacticParOr(nCtx(),
2934 Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2935 }

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

2686 {
2687 int csn = Symbol.arrayLength(sortNames);
2688 int cs = Sort.arrayLength(sorts);
2689 int cdn = Symbol.arrayLength(declNames);
2690 int cd = AST.arrayLength(decls);
2691 if (csn != cs || cdn != cd)
2692 throw new Z3Exception("Argument size mismatch");
2693 ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
2694 fileName, AST.arrayLength(sorts),
2695 Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2696 AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2697 AST.arrayToNative(decls)));
2698 return v.ToBoolExprArray();
2699 }

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

2665 {
2666 int csn = Symbol.arrayLength(sortNames);
2667 int cs = Sort.arrayLength(sorts);
2668 int cdn = Symbol.arrayLength(declNames);
2669 int cd = AST.arrayLength(decls);
2670 if (csn != cs || cdn != cd) {
2671 throw new Z3Exception("Argument size mismatch");
2672 }
2673 ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
2674 str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2675 AST.arrayToNative(sorts), AST.arrayLength(decls),
2676 Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2677 return v.ToBoolExprArray();
2678 }

◆ 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 max is reached.

Definition at line 2861 of file Context.java.

2862 {
2863 checkContextMatch(t);
2864 return new Tactic(this, Native.tacticRepeat(nCtx(),
2865 t.getNativeObject(), max));
2866 }
expr max(expr const &a, expr const &b)
Definition: z3++.h:1836

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

2627 {
2628 Native.setAstPrintMode(nCtx(), value.toInt());
2629 }

◆ SimplifyHelp()

String SimplifyHelp ( )
inline

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

Definition at line 3981 of file Context.java.

3982 {
3983 return Native.simplifyGetHelp(nCtx());
3984 }

◆ skip()

Tactic skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 2871 of file Context.java.

2872 {
2873 return new Tactic(this, Native.tacticSkip(nCtx()));
2874 }

◆ stringToInt()

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

Convert an integer expression to a string.

Definition at line 2025 of file Context.java.

2026 {
2027 return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
2028 }

◆ 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 AndThen.

Definition at line 2798 of file Context.java.

2799 {
2800 return andThen(t1, t2, ts);
2801 }
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2766

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

2823 {
2824 checkContextMatch(t);
2825 return new Tactic(this, Native.tacticTryFor(nCtx(),
2826 t.getNativeObject(), ms));
2827 }

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

3973 {
3974 return a.getNativeObject();
3975 }

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

4003 {
4004 Native.updateParamValue(nCtx(), id, value);
4005 }

◆ usingParams()

Tactic usingParams ( Tactic  t,
Params  p 
)
inline

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

Definition at line 2908 of file Context.java.

2909 {
2910 checkContextMatch(t);
2911 checkContextMatch(p);
2912 return new Tactic(this, Native.tacticUsingParams(nCtx(),
2913 t.getNativeObject(), p.getNativeObject()));
2914 }

◆ 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 skip tactic.

Definition at line 2835 of file Context.java.

2836 {
2837 checkContextMatch(t);
2838 checkContextMatch(p);
2839 return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2840 t.getNativeObject()));
2841 }

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

2923 {
2924 return usingParams(t, p);
2925 }
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2908

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

3956 {
3957 return AST.create(this, nativeObject);
3958 }