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< BitVecSort > | getStringSort ()
UninterpretedSort | mkUninterpretedSort (Symbol s)
UninterpretedSort | mkUninterpretedSort (String str)
IntSort | mkIntSort ()
RealSort | mkRealSort ()
BitVecSort | mkBitVecSort (int size)
SeqSort< BitVecSort > | mkStringSort ()
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, BoolSort > | mkSetUnion (Expr< ArraySort< D, BoolSort > >... args)
final< D extends Sort > ArrayExpr< D, BoolSort > | mkSetIntersection (Expr< ArraySort< D, BoolSort > >... args)
SeqExpr< BitVecSort > | mkString (String s)
SeqExpr< BitVecSort > | intToString (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< AST > | getASTDRQ ()
IDecRefQueue< ASTMap > | getASTMapDRQ ()
IDecRefQueue< ASTVector > | getASTVectorDRQ ()
IDecRefQueue< ApplyResult > | getApplyResultDRQ ()
IDecRefQueue< FuncInterp.Entry<?> > | getFuncEntryDRQ ()
IDecRefQueue< FuncInterp<?> > | getFuncInterpDRQ ()
IDecRefQueue< Goal > | getGoalDRQ ()
IDecRefQueue< Model > | getModelDRQ ()
IDecRefQueue< Params > | getParamsDRQ ()
IDecRefQueue< ParamDescrs > | getParamDescrsDRQ ()
IDecRefQueue< Probe > | getProbeDRQ ()
IDecRefQueue< Solver > | getSolverDRQ ()
IDecRefQueue< Statistics > | getStatisticsDRQ ()
IDecRefQueue< Tactic > | getTacticDRQ ()
IDecRefQueue< Fixedpoint > | getFixedpointDRQ ()
IDecRefQueue< Optimize > | getOptimizeDRQ ()
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 | ) |
| inline protected

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 }
z3py.Map
def Map(f, *args)
Definition: z3py.py:4757
z3py.String
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 }
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008

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

  name | Name of the benchmark. The argument is optional.
  logic | The benchmark logic.
  status | The status string (sat, unsat, or unknown)
  attributes | Other attributes, such as source, difficulty or category.
  assumptions | Auxiliary assumptions.
  formula | Formula 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 }
z3py.BoolSort
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 }
z3py.IntSort
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 }
com.microsoft.z3.Context.getNumProbes
int getNumProbes()
Definition: Context.java:2962

## ◆ getRealSort()

RealSort getRealSort | ( |  | ) |
| inline

Retrieves the Real sort of the context.

Definition at line 150 of file Context.java.

151 {
152 if (m_realSort == null) {
153 m_realSort = new RealSort(this);
154 }
155 return m_realSort;
156 }
z3py.RealSort
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 }
com.microsoft.z3.Context.mkStringSort
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 }
com.microsoft.z3.Context.getNumTactics
int getNumTactics()
Definition: Context.java:2727

## ◆ gt()

Probe gt | ( | Probe | p1,
|  | Probe | p2
| ) |  |
| inline

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

Definition at line 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 }
z3py.BitVecSort
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 }
com.microsoft.z3.Context.mkTrue
BoolExpr mkTrue()
Definition: Context.java:702
com.microsoft.z3.Context.mkFalse
BoolExpr mkFalse()
Definition: Context.java:710

## ◆ 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 }
com.microsoft.z3.Context.getBoolSort
BoolSort getBoolSort()
Definition: Context.java:128
com.microsoft.z3.Context.mkSymbol
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

  v | value of the numeral.
  size | the size of the bit-vector

Definition at line 2456 of file Context.java.

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

## ◆ mkBV() [2/3]

BitVecNum mkBV | ( | long | v,
|  | int | size
| ) |  |
| inline

Create a bit-vector numeral.

Parameters

  v | value of the numeral. *
  size | the 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

  v | A string representing the value in decimal notation.
  size | the 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 right`t2` 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 }
com.microsoft.z3.Context.mkDatatypeSorts
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

  names | names of datatype sorts
  c | list 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

  sorts | the sorts of the bound variables.
  names | names of the bound variables
  body | the body of the quantifier.
  weight | quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
  patterns | array containing the patterns created using `MkPattern`.
  noPatterns | array containing the anti-patterns created using `MkPattern`.
  quantifierID | optional symbol to track quantifier.
  skolemID | optional 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

  sgn | the sign.
  exp | the exponent.
  sig | the significand.
  s | FloatingPoint sort.

Exceptions

  Z3Exception |

Definition at line 3490 of file Context.java.

3491 {
3492 return mkFPNumeral(sgn, exp, sig, s);
3493 }
com.microsoft.z3.Context.mkFPNumeral
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

  sgn | the sign.
  exp | the exponent.
  sig | the significand.
  s | FloatingPoint 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

  v | numeral value.
  s | FloatingPoint 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

  sgn | bit-vector term (of size 1) representing the sign.
  sig | bit-vector term representing the significand.
  exp | bit-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

  v | numeral value.
  s | FloatingPoint 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

  v | numeral value.
  s | FloatingPoint 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

  t | floating-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

  rm | rounding mode term
  t1 | floating-point term
  t2 | floating-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

  rm | rounding mode term
  t1 | floating-point term
  t2 | floating-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

  t1 | floating-point term
  t2 | floating-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

  rm | rounding mode term
  t1 | floating-point term
  t2 | floating-point term
  t3 | floating-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

  t1 | floating-point term
  t2 | floating-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

  t1 | floating-point term
  t2 | floating-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

  s | FloatingPoint sort.
  negative | indicates 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

  t | floating-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

  t | floating-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

  t | floating-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

  t | floating-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

  t | floating-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

  t | floating-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

  t | floating-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

  t1 | floating-point term
  t2 | floating-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

  t1 | floating-point term
  t2 | floating-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

  t1 | floating-point term
  t2 | floating-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

  t1 | floating-point term
  t2 | floating-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

  rm | rounding mode term
  t1 | floating-point term
  t2 | floating-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

  s | FloatingPoint 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

  t | floating-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

  sgn | the sign.
  exp | the exponent.
  sig | the significand.
  s | FloatingPoint 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

  sgn | the sign.
  exp | the exponent.
  sig | the significand.
  s | FloatingPoint 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

  v | numeral value.
  s | FloatingPoint 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

  v | numeral value.
  s | FloatingPoint 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

  v | numeral value.
  s | FloatingPoint 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

  t1 | floating-point term
  t2 | floating-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

  rm | term of RoundingMode sort
  t | floating-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

  ebits | exponent bits in the FloatingPoint sort.
  sbits | significand bits in the FloatingPoint sort.

Exceptions

  Z3Exception |

Definition at line 3279 of file Context.java.

3280 {
3281 return new FPSort(this, ebits, sbits);
3282 }
z3py.FPSort
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

  rm | rounding mode term
  t | floating-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

  rm | rounding mode term
  t1 | floating-point term
  t2 | floating-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

  rm | RoundingMode term.
  t | FloatingPoint term
  sz | Size of the resulting bit-vector.
  signed | Indicates 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

  bv | bit-vector value (of size m).
  s | FloatingPoint 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

  rm | RoundingMode term.
  t | term of bit-vector sort.
  s | FloatingPoint sort.
  signed | flag 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

  rm | RoundingMode term.
  exp | Exponent term of Int sort.
  sig | Significand term of Real sort.
  s | FloatingPoint 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

  rm | RoundingMode term.
  t | FloatingPoint term.
  s | FloatingPoint 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

  rm | RoundingMode term.
  t | term of Real sort.
  s | FloatingPoint 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

  s | FloatingPoint sort
  rm | floating-point rounding mode term
  t | floating-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

  t | FloatingPoint 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

  t | FloatingPoint 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

  s | FloatingPoint sort.
  negative | indicates 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

  models | Indicates whether model generation should be enabled.
  unsatCores | Indicates whether unsat core generation should be enabled.
  proofs | Indicates 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

  v | value 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 }
com.microsoft.z3.Context.getIntSort
IntSort getIntSort()
Definition: Context.java:139

## ◆ mkInt() [2/3]

IntNum mkInt | ( | long | v | ) |
| inline

Create an integer numeral.

Parameters

  v | value 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

  v | A 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 }
com.microsoft.z3.Context.mkForall
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2496
com.microsoft.z3.Context.mkExists
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java: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

  num | numerator of rational.
  den | denominator 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

  v | value 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 }
com.microsoft.z3.Context.getRealSort
RealSort getRealSort()
Definition: Context.java:150

## ◆ mkReal() [3/4]

RatNum mkReal | ( | long | v | ) |
| inline

Create a real numeral.

Parameters

  v | value 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

  v | A 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 }
com.microsoft.z3.Context.mkSolver
Solver mkSolver()
Definition: Context.java:3105

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 }
z3py.TupleSort
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 }
com.microsoft.z3.Context.mkUninterpretedSort
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

Definition at line 4008 of file Context.java.

4009 {
4010 if (m_ctx == 0)
4011 throw new Z3Exception("Context closed");
4012 return m_ctx;
4013 }

Referenced by ASTVector.ASTVector(), ConstructorDecRefQueue.decRef(), ConstructorListDecRefQueue.decRef(), AST.equals(), FuncDecl< R extends Sort >.equals(), Sort.equals(), FPRMSort.FPRMSort(), FPSort.FPSort(), Quantifier.of(), Lambda< R extends Sort >.of(), ASTVector.set(), AST.translate(), ASTVector.translate(), Goal.translate(), and Solver.translate().

## ◆ 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 }
z3::max
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 }
com.microsoft.z3.Context.andThen
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

  a | The 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 }
com.microsoft.z3.Context.usingParams
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

  nativeObject | The native pointer to wrap.

Definition at line 3955 of file Context.java.

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