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 ()
 
CharSort mkCharSort ()
 
SeqSort< CharSort > getStringSort ()
 
UninterpretedSort mkUninterpretedSort (Symbol s)
 
UninterpretedSort mkUninterpretedSort (String str)
 
IntSort mkIntSort ()
 
RealSort mkRealSort ()
 
BitVecSort mkBitVecSort (int size)
 
SeqSort< CharSort > 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< CharSort > mkString (String s)
 
SeqExpr< CharSort > intToString (Expr< IntSort > e)
 
SeqExpr< CharSort > ubvToString (Expr< BitVecSort > e)
 
SeqExpr< CharSort > sbvToString (Expr< BitVecSort > e)
 
IntExpr stringToInt (Expr< SeqSort< CharSort >> e)
 
final< R extends Sort > SeqExpr< R > mkConcat (Expr< SeqSort< R >>... t)
 
BoolExpr MkStringLt (SeqSort< CharSort > s1, SeqSort< CharSort > s2)
 
BoolExpr MkStringLe (SeqSort< CharSort > s1, SeqSort< CharSort > s2)
 
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 mkCharLe (Expr< CharSort > ch1, Expr< CharSort > ch2)
 
IntExpr charToInt (Expr< CharSort > ch)
 
BitVecExpr charToBv (Expr< CharSort > ch)
 
Expr< CharSort > charFromBv (BitVecExpr bv)
 
BoolExpr mkIsDigit (Expr< CharSort > ch)
 
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)
inlineprotected

Definition at line 47 of file Context.java.

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

◆ Context() [3/3]

Context ( Map< String, String >  settings)
inline

Constructor. Remarks: The following parameters can be set:

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

Definition at line 72 of file Context.java.

72  {
73  synchronized (creation_lock) {
74  long cfg = Native.mkConfig();
75  for (Map.Entry<String, String> kv : settings.entrySet()) {
76  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
77  }
78  m_ctx = Native.mkContextRc(cfg);
79  Native.delConfig(cfg);
80  init();
81  }
82  }
z3py.Map
def Map(f, *args)
Definition: z3py.py:4823
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10928

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

3196  {
3197  checkContextMatch(p1);
3198  checkContextMatch(p2);
3199  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
3200  p2.getNativeObject()));
3201  }

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

2893  {
2894  checkContextMatch(t1);
2895  checkContextMatch(t2);
2896  checkContextMatch(ts);
2897 
2898  long last = 0;
2899  if (ts != null && ts.length > 0)
2900  {
2901  last = ts[ts.length - 1].getNativeObject();
2902  for (int i = ts.length - 2; i >= 0; i--) {
2903  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2904  last);
2905  }
2906  }
2907  if (last != 0)
2908  {
2909  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2910  return new Tactic(this, Native.tacticAndThen(nCtx(),
2911  t1.getNativeObject(), last));
2912  } else
2913  return new Tactic(this, Native.tacticAndThen(nCtx(),
2914  t1.getNativeObject(), t2.getNativeObject()));
2915  }

◆ benchmarkToSMTString()

String benchmarkToSMTString ( String  name,
String  logic,
String  status,
String  attributes,
Expr< BoolSort >[]  assumptions,
Expr< BoolSort >  formula 
)
inline

Convert a benchmark into an SMT-LIB formatted string.

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

Definition at line 2769 of file Context.java.

2772  {
2773 
2774  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2775  attributes, assumptions.length,
2776  AST.arrayToNative(assumptions), formula.getNativeObject());
2777  }

◆ charFromBv()

Expr<CharSort> charFromBv ( BitVecExpr  bv)
inline

Create a character from a bit-vector (code point).

Definition at line 2361 of file Context.java.

2362  {
2363  checkContextMatch(bv);
2364  return (Expr<CharSort>) Expr.create(this, Native.mkCharFromBv(nCtx(), bv.getNativeObject()));
2365  }

◆ charToBv()

BitVecExpr charToBv ( Expr< CharSort >  ch)
inline

Create a bit-vector (code point) from character.

Definition at line 2352 of file Context.java.

2353  {
2354  checkContextMatch(ch);
2355  return (BitVecExpr) Expr.create(this, Native.mkCharToBv(nCtx(), ch.getNativeObject()));
2356  }

◆ charToInt()

IntExpr charToInt ( Expr< CharSort >  ch)
inline

Create an integer (code point) from character.

Definition at line 2343 of file Context.java.

2344  {
2345  checkContextMatch(ch);
2346  return (IntExpr) Expr.create(this, Native.mkCharToInt(nCtx(), ch.getNativeObject()));
2347  }

◆ close()

void close ( )
inline

Disposes of the context.

Definition at line 4310 of file Context.java.

4311  {
4312  m_AST_DRQ.forceClear(this);
4313  m_ASTMap_DRQ.forceClear(this);
4314  m_ASTVector_DRQ.forceClear(this);
4315  m_ApplyResult_DRQ.forceClear(this);
4316  m_FuncEntry_DRQ.forceClear(this);
4317  m_FuncInterp_DRQ.forceClear(this);
4318  m_Goal_DRQ.forceClear(this);
4319  m_Model_DRQ.forceClear(this);
4320  m_Params_DRQ.forceClear(this);
4321  m_Probe_DRQ.forceClear(this);
4322  m_Solver_DRQ.forceClear(this);
4323  m_Optimize_DRQ.forceClear(this);
4324  m_Statistics_DRQ.forceClear(this);
4325  m_Tactic_DRQ.forceClear(this);
4326  m_Fixedpoint_DRQ.forceClear(this);
4327 
4328  m_boolSort = null;
4329  m_intSort = null;
4330  m_realSort = null;
4331  m_stringSort = null;
4332 
4333  synchronized (creation_lock) {
4334  Native.delContext(m_ctx);
4335  }
4336  m_ctx = 0;
4337  }

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

2974  {
2975  checkContextMatch(p);
2976  checkContextMatch(t1);
2977  checkContextMatch(t2);
2978  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2979  t1.getNativeObject(), t2.getNativeObject()));
2980  }

◆ constProbe()

Probe constProbe ( double  val)
inline

Create a probe that always evaluates to

val

.

Definition at line 3125 of file Context.java.

3126  {
3127  return new Probe(this, Native.probeConst(nCtx(), val));
3128  }

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

3185  {
3186  checkContextMatch(p1);
3187  checkContextMatch(p2);
3188  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
3189  p2.getNativeObject()));
3190  }

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

◆ fail()

Tactic fail ( )
inline

Create a tactic always fails.

Definition at line 3004 of file Context.java.

3005  {
3006  return new Tactic(this, Native.tacticFail(nCtx()));
3007  }

◆ failIf()

Tactic failIf ( Probe  p)
inline

Create a tactic that fails if the probe

p

evaluates to false.

Definition at line 3013 of file Context.java.

3014  {
3015  checkContextMatch(p);
3016  return new Tactic(this,
3017  Native.tacticFailIf(nCtx(), p.getNativeObject()));
3018  }

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

3025  {
3026  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
3027  }

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

3173  {
3174  checkContextMatch(p1);
3175  checkContextMatch(p2);
3176  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
3177  p2.getNativeObject()));
3178  }

◆ getApplyResultDRQ()

IDecRefQueue<ApplyResult> getApplyResultDRQ ( )
inline

Definition at line 4241 of file Context.java.

4242  {
4243  return m_ApplyResult_DRQ;
4244  }

◆ getASTDRQ()

IDecRefQueue<AST> getASTDRQ ( )
inline

Definition at line 4226 of file Context.java.

4227  {
4228  return m_AST_DRQ;
4229  }

◆ getASTMapDRQ()

IDecRefQueue<ASTMap> getASTMapDRQ ( )
inline

Definition at line 4231 of file Context.java.

4232  {
4233  return m_ASTMap_DRQ;
4234  }

◆ getASTVectorDRQ()

IDecRefQueue<ASTVector> getASTVectorDRQ ( )
inline

Definition at line 4236 of file Context.java.

4237  {
4238  return m_ASTVector_DRQ;
4239  }

◆ 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:1691

◆ getConstructorDRQ()

IDecRefQueue<Constructor<?> > getConstructorDRQ ( )
inline

Definition at line 4218 of file Context.java.

4218  {
4219  return m_Constructor_DRQ;
4220  }

◆ getConstructorListDRQ()

IDecRefQueue<ConstructorList<?> > getConstructorListDRQ ( )
inline

Definition at line 4222 of file Context.java.

4222  {
4223  return m_ConstructorList_DRQ;
4224  }

◆ getFixedpointDRQ()

IDecRefQueue<Fixedpoint> getFixedpointDRQ ( )
inline

Definition at line 4296 of file Context.java.

4297  {
4298  return m_Fixedpoint_DRQ;
4299  }

◆ getFuncEntryDRQ()

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

Definition at line 4246 of file Context.java.

4247  {
4248  return m_FuncEntry_DRQ;
4249  }

◆ getFuncInterpDRQ()

IDecRefQueue<FuncInterp<?> > getFuncInterpDRQ ( )
inline

Definition at line 4251 of file Context.java.

4252  {
4253  return m_FuncInterp_DRQ;
4254  }

◆ getGoalDRQ()

IDecRefQueue<Goal> getGoalDRQ ( )
inline

Definition at line 4256 of file Context.java.

4257  {
4258  return m_Goal_DRQ;
4259  }

◆ 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:3138

◆ getModelDRQ()

IDecRefQueue<Model> getModelDRQ ( )
inline

Definition at line 4261 of file Context.java.

4262  {
4263  return m_Model_DRQ;
4264  }

◆ getNumProbes()

int getNumProbes ( )
inline

The number of supported Probes.

Definition at line 3087 of file Context.java.

3088  {
3089  return Native.getNumProbes(nCtx());
3090  }

◆ getNumTactics()

int getNumTactics ( )
inline

The number of supported tactics.

Definition at line 2852 of file Context.java.

2853  {
2854  return Native.getNumTactics(nCtx());
2855  }

◆ getOptimizeDRQ()

IDecRefQueue<Optimize> getOptimizeDRQ ( )
inline

Definition at line 4301 of file Context.java.

4302  {
4303  return m_Optimize_DRQ;
4304  }

◆ getParamDescrsDRQ()

IDecRefQueue<ParamDescrs> getParamDescrsDRQ ( )
inline

Definition at line 4271 of file Context.java.

4272  {
4273  return m_ParamDescrs_DRQ;
4274  }

◆ getParamsDRQ()

IDecRefQueue<Params> getParamsDRQ ( )
inline

Definition at line 4266 of file Context.java.

4267  {
4268  return m_Params_DRQ;
4269  }

◆ getProbeDescription()

String getProbeDescription ( String  name)
inline

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

Definition at line 3109 of file Context.java.

3110  {
3111  return Native.probeGetDescr(nCtx(), name);
3112  }

◆ getProbeDRQ()

IDecRefQueue<Probe> getProbeDRQ ( )
inline

Definition at line 4276 of file Context.java.

4277  {
4278  return m_Probe_DRQ;
4279  }

◆ getProbeNames()

String [] getProbeNames ( )
inline

The names of all supported Probes.

Definition at line 3095 of file Context.java.

3096  {
3097 
3098  int n = getNumProbes();
3099  String[] res = new String[n];
3100  for (int i = 0; i < n; i++)
3101  res[i] = Native.getProbeName(nCtx(), i);
3102  return res;
3103  }

◆ 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:3155

◆ getSimplifyParameterDescriptions()

ParamDescrs getSimplifyParameterDescriptions ( )
inline

Retrieves parameter descriptions for simplifier.

Definition at line 4145 of file Context.java.

4146  {
4147  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
4148  }

◆ getSolverDRQ()

IDecRefQueue<Solver> getSolverDRQ ( )
inline

Definition at line 4281 of file Context.java.

4282  {
4283  return m_Solver_DRQ;
4284  }

◆ getStatisticsDRQ()

IDecRefQueue<Statistics> getStatisticsDRQ ( )
inline

Definition at line 4286 of file Context.java.

4287  {
4288  return m_Statistics_DRQ;
4289  }

◆ getStringSort()

SeqSort<CharSort> getStringSort ( )
inline

Retrieves the String sort of the context.

Definition at line 178 of file Context.java.

179  {
180  if (m_stringSort == null) {
181  m_stringSort = mkStringSort();
182  }
183  return m_stringSort;
184  }
com.microsoft.z3.Context.mkStringSort
SeqSort< CharSort > mkStringSort()
Definition: Context.java:251

◆ getTacticDescription()

String getTacticDescription ( String  name)
inline

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

Definition at line 2874 of file Context.java.

2875  {
2876  return Native.tacticGetDescr(nCtx(), name);
2877  }

◆ getTacticDRQ()

IDecRefQueue<Tactic> getTacticDRQ ( )
inline

Definition at line 4291 of file Context.java.

4292  {
4293  return m_Tactic_DRQ;
4294  }

◆ getTacticNames()

String [] getTacticNames ( )
inline

The names of all supported tactics.

Definition at line 2860 of file Context.java.

2861  {
2862 
2863  int n = getNumTactics();
2864  String[] res = new String[n];
2865  for (int i = 0; i < n; i++)
2866  res[i] = Native.getTacticName(nCtx(), i);
2867  return res;
2868  }

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

3147  {
3148  checkContextMatch(p1);
3149  checkContextMatch(p2);
3150  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
3151  p2.getNativeObject()));
3152  }

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

3080  {
3081  Native.interrupt(nCtx());
3082  }

◆ intToString()

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

Convert an integer expression to a string.

Definition at line 2033 of file Context.java.

2034  {
2035  return (SeqExpr<CharSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
2036  }

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

3160  {
3161  checkContextMatch(p1);
3162  checkContextMatch(p2);
3163  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
3164  p2.getNativeObject()));
3165  }

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

3135  {
3136  checkContextMatch(p1);
3137  checkContextMatch(p2);
3138  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
3139  p2.getNativeObject()));
3140  }

◆ mkAdd()

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

Create an expression representing

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

.

Definition at line 838 of file Context.java.

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

◆ mkAnd()

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

Create an expression representing

t[0] and t[1] and ...
com.microsoft.z3.Context.and
Probe and(Probe p1, Probe p2)
Definition: Context.java:3195

.

Definition at line 816 of file Context.java.

817  {
818  checkContextMatch(t);
819  return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
820  AST.arrayToNative(t)));
821  }

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

702  {
703  checkContextMatch(f);
704  checkContextMatch(args);
705  return Expr.create(this, f, args);
706  }

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

2389  {
2390  checkContextMatch(args);
2391  return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
2392  }

◆ mkAtMost()

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

Create an at-most-k constraint.

Definition at line 2379 of file Context.java.

2380  {
2381  checkContextMatch(args);
2382  return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
2383  }

◆ mkBitVecSort()

BitVecSort mkBitVecSort ( int  size)
inline

Create a new bit-vector sort.

Definition at line 222 of file Context.java.

223  {
224  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
225  }
z3py.BitVecSort
def BitVecSort(sz, ctx=None)
Definition: z3py.py:4005

◆ mkBool()

BoolExpr mkBool ( boolean  value)
inline

Creates a Boolean value.

Definition at line 727 of file Context.java.

728  {
729  return value ? mkTrue() : mkFalse();
730  }

◆ mkBoolConst() [1/2]

BoolExpr mkBoolConst ( String  name)
inline

Create a Boolean constant.

Definition at line 644 of file Context.java.

645  {
646  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
647  }
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 636 of file Context.java.

637  {
638  return (BoolExpr) mkConst(name, getBoolSort());
639  }

◆ mkBoolSort()

BoolSort mkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 161 of file Context.java.

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

◆ mkBV() [1/3]

BitVecNum mkBV ( int  v,
int  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2581 of file Context.java.

2582  {
2583  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2584  }
com.microsoft.z3.Context.mkBitVecSort
BitVecSort mkBitVecSort(int size)
Definition: Context.java:222

◆ mkBV() [2/3]

BitVecNum mkBV ( long  v,
int  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2591 of file Context.java.

2592  {
2593  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2594  }

◆ mkBV() [3/3]

BitVecNum mkBV ( String  v,
int  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2571 of file Context.java.

2572  {
2573  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2574  }

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

1577  {
1578  checkContextMatch(t);
1579  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1580  (signed)));
1581  }

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

1140  {
1141  checkContextMatch(t1);
1142  checkContextMatch(t2);
1143  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1144  t1.getNativeObject(), t2.getNativeObject()));
1145  }

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

1590  {
1591  checkContextMatch(t1);
1592  checkContextMatch(t2);
1593  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1594  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1595  }

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

1604  {
1605  checkContextMatch(t1);
1606  checkContextMatch(t2);
1607  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1608  t1.getNativeObject(), t2.getNativeObject()));
1609  }

◆ mkBVAND()

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

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

Definition at line 1050 of file Context.java.

1051  {
1052  checkContextMatch(t1);
1053  checkContextMatch(t2);
1054  return new BitVecExpr(this, Native.mkBvand(nCtx(),
1055  t1.getNativeObject(), t2.getNativeObject()));
1056  }

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

1485  {
1486  checkContextMatch(t1);
1487  checkContextMatch(t2);
1488  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1489  t1.getNativeObject(), t2.getNativeObject()));
1490  }

◆ mkBVConst() [1/2]

BitVecExpr mkBVConst ( String  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 692 of file Context.java.

693  {
694  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
695  }

◆ mkBVConst() [2/2]

BitVecExpr mkBVConst ( Symbol  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 684 of file Context.java.

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

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

1465  {
1466  checkContextMatch(t1);
1467  checkContextMatch(t2);
1468  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1469  t1.getNativeObject(), t2.getNativeObject()));
1470  }

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

1166  {
1167  checkContextMatch(t1);
1168  checkContextMatch(t2);
1169  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1170  t1.getNativeObject(), t2.getNativeObject()));
1171  }

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

1672  {
1673  checkContextMatch(t1);
1674  checkContextMatch(t2);
1675  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1676  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1677  }

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

1686  {
1687  checkContextMatch(t1);
1688  checkContextMatch(t2);
1689  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1690  t1.getNativeObject(), t2.getNativeObject()));
1691  }

◆ mkBVNAND()

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

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

Definition at line 1089 of file Context.java.

1090  {
1091  checkContextMatch(t1);
1092  checkContextMatch(t2);
1093  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1094  t1.getNativeObject(), t2.getNativeObject()));
1095  }

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

1129  {
1130  checkContextMatch(t);
1131  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1132  }

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

1659  {
1660  checkContextMatch(t);
1661  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1662  t.getNativeObject()));
1663  }

◆ mkBVNOR()

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

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

Definition at line 1102 of file Context.java.

1103  {
1104  checkContextMatch(t1);
1105  checkContextMatch(t2);
1106  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1107  t1.getNativeObject(), t2.getNativeObject()));
1108  }

◆ mkBVNot()

BitVecExpr mkBVNot ( Expr< BitVecSort >  t)
inline

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

Definition at line 1015 of file Context.java.

1016  {
1017  checkContextMatch(t);
1018  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
1019  }

◆ mkBVOR()

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

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

Definition at line 1063 of file Context.java.

1064  {
1065  checkContextMatch(t1);
1066  checkContextMatch(t2);
1067  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1068  t2.getNativeObject()));
1069  }

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

1027  {
1028  checkContextMatch(t);
1029  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
1030  t.getNativeObject()));
1031  }

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

1039  {
1040  checkContextMatch(t);
1041  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
1042  t.getNativeObject()));
1043  }

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

1524  {
1525  checkContextMatch(t1);
1526  checkContextMatch(t2);
1527  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1528  t1.getNativeObject(), t2.getNativeObject()));
1529  }

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

1498  {
1499  checkContextMatch(t);
1500  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1501  t.getNativeObject()));
1502  }

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

1539  {
1540  checkContextMatch(t1);
1541  checkContextMatch(t2);
1542  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1543  t1.getNativeObject(), t2.getNativeObject()));
1544  }

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

1510  {
1511  checkContextMatch(t);
1512  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1513  t.getNativeObject()));
1514  }

◆ mkBVSDiv()

BitVecExpr mkBVSDiv ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

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

If

t2

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

Definition at line 1201 of file Context.java.

1202  {
1203  checkContextMatch(t1);
1204  checkContextMatch(t2);
1205  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1206  t1.getNativeObject(), t2.getNativeObject()));
1207  }

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

1646  {
1647  checkContextMatch(t1);
1648  checkContextMatch(t2);
1649  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1650  t1.getNativeObject(), t2.getNativeObject()));
1651  }

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

1327  {
1328  checkContextMatch(t1);
1329  checkContextMatch(t2);
1330  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1331  t2.getNativeObject()));
1332  }

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

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

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

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

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

1301  {
1302  checkContextMatch(t1);
1303  checkContextMatch(t2);
1304  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1305  t2.getNativeObject()));
1306  }

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

1275  {
1276  checkContextMatch(t1);
1277  checkContextMatch(t2);
1278  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1279  t2.getNativeObject()));
1280  }

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

1249  {
1250  checkContextMatch(t1);
1251  checkContextMatch(t2);
1252  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1253  t1.getNativeObject(), t2.getNativeObject()));
1254  }

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

1235  {
1236  checkContextMatch(t1);
1237  checkContextMatch(t2);
1238  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1239  t1.getNativeObject(), t2.getNativeObject()));
1240  }

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

1153  {
1154  checkContextMatch(t1);
1155  checkContextMatch(t2);
1156  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1157  t1.getNativeObject(), t2.getNativeObject()));
1158  }

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

1618  {
1619  checkContextMatch(t1);
1620  checkContextMatch(t2);
1621  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1622  t1.getNativeObject(), t2.getNativeObject()));
1623  }

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

1632  {
1633  checkContextMatch(t1);
1634  checkContextMatch(t2);
1635  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1636  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1637  }

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

1181  {
1182  checkContextMatch(t1);
1183  checkContextMatch(t2);
1184  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1185  t1.getNativeObject(), t2.getNativeObject()));
1186  }

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

1314  {
1315  checkContextMatch(t1);
1316  checkContextMatch(t2);
1317  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1318  t2.getNativeObject()));
1319  }

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

1340  {
1341  checkContextMatch(t1);
1342  checkContextMatch(t2);
1343  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1344  t2.getNativeObject()));
1345  }

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

1288  {
1289  checkContextMatch(t1);
1290  checkContextMatch(t2);
1291  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1292  t2.getNativeObject()));
1293  }

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

1262  {
1263  checkContextMatch(t1);
1264  checkContextMatch(t2);
1265  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1266  t2.getNativeObject()));
1267  }

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

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

◆ mkBVXNOR()

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

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

Definition at line 1115 of file Context.java.

1116  {
1117  checkContextMatch(t1);
1118  checkContextMatch(t2);
1119  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1120  t1.getNativeObject(), t2.getNativeObject()));
1121  }

◆ mkBVXOR()

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

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

Definition at line 1076 of file Context.java.

1077  {
1078  checkContextMatch(t1);
1079  checkContextMatch(t2);
1080  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1081  t1.getNativeObject(), t2.getNativeObject()));
1082  }

◆ mkCharLe()

BoolExpr mkCharLe ( Expr< CharSort >  ch1,
Expr< CharSort >  ch2 
)
inline

Create less than or equal to between two characters.

Definition at line 2334 of file Context.java.

2335  {
2336  checkContextMatch(ch1, ch2);
2337  return (BoolExpr) Expr.create(this, Native.mkCharLe(nCtx(), ch1.getNativeObject(), ch2.getNativeObject()));
2338  }

◆ mkCharSort()

CharSort mkCharSort ( )
inline

Creates character sort object.

Definition at line 170 of file Context.java.

171  {
172  return new CharSort(this);
173  }
z3py.CharSort
def CharSort(ctx=None)
Definition: z3py.py:10755

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

1371  {
1372  checkContextMatch(t1);
1373  checkContextMatch(t2);
1374  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1375  t1.getNativeObject(), t2.getNativeObject()));
1376  }

◆ mkConcat() [2/3]

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

Concatenate sequences.

Definition at line 2066 of file Context.java.

2067  {
2068  checkContextMatch(t);
2069  return (SeqExpr<R>) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
2070  }

◆ mkConcat() [3/3]

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

Create the concatenation of regular languages.

Definition at line 2259 of file Context.java.

2260  {
2261  checkContextMatch(t);
2262  return (ReExpr<R>) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2263  }

◆ mkDatatypeSorts() [1/2]

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

Create mutually recursive data-types.

Definition at line 422 of file Context.java.

424  {
425  return mkDatatypeSorts(mkSymbols(names), c);
426  }
com.microsoft.z3.Context.mkDatatypeSorts
DatatypeSort< Object >[] mkDatatypeSorts(Symbol[] names, Constructor< Object >[][] c)
Definition: Context.java:396

◆ mkDatatypeSorts() [2/2]

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

Create mutually recursive datatypes.

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

Definition at line 396 of file Context.java.

397  {
398  checkContextMatch(names);
399  int n = names.length;
400  ConstructorList<Object>[] cla = new ConstructorList[n];
401  long[] n_constr = new long[n];
402  for (int i = 0; i < n; i++)
403  {
404  Constructor<Object>[] constructor = c[i];
405 
406  checkContextMatch(constructor);
407  cla[i] = new ConstructorList<>(this, constructor);
408  n_constr[i] = cla[i].getNativeObject();
409  }
410  long[] n_res = new long[n];
411  Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
412  n_constr);
413  DatatypeSort<Object>[] res = new DatatypeSort[n];
414  for (int i = 0; i < n; i++)
415  res[i] = new DatatypeSort<>(this, n_res[i]);
416  return res;
417  }
z3py.DatatypeSort
def DatatypeSort(name, ctx=None)
Definition: z3py.py:5358

◆ mkDistinct()

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

Creates a

distinct
z3::distinct
expr distinct(expr_vector const &args)
Definition: z3++.h:2433

term.

Definition at line 747 of file Context.java.

748  {
749  checkContextMatch(args);
750  return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
751  AST.arrayToNative(args)));
752  }

◆ mkEq()

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

Creates the equality

x = y

Definition at line 735 of file Context.java.

736  {
737  checkContextMatch(x);
738  checkContextMatch(y);
739  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
740  y.getNativeObject()));
741  }

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

2662  {
2663 
2664  return Quantifier.of(this, false, boundConstants, body, weight,
2665  patterns, noPatterns, quantifierID, skolemID);
2666  }

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

2649  {
2650 
2651  return Quantifier.of(this, false, sorts, names, body, weight,
2652  patterns, noPatterns, quantifierID, skolemID);
2653  }

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

1388  {
1389  checkContextMatch(t);
1390  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1391  t.getNativeObject()));
1392  }

◆ mkFalse()

BoolExpr mkFalse ( )
inline

The false Term.

Definition at line 719 of file Context.java.

720  {
721  return new BoolExpr(this, Native.mkFalse(nCtx()));
722  }

◆ mkFixedpoint()

Fixedpoint mkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3285 of file Context.java.

3286  {
3287  return new Fixedpoint(this);
3288  }

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

2636  {
2637 
2638  return Quantifier.of(this, true, boundConstants, body, weight,
2639  patterns, noPatterns, quantifierID, skolemID);
2640  }

◆ mkForall() [2/2]

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

Create a universal Quantifier.

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

Definition at line 2621 of file Context.java.

2624  {
2625  return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2626  noPatterns, quantifierID, skolemID);
2627  }

◆ mkFP() [1/6]

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

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

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

Definition at line 3615 of file Context.java.

3616  {
3617  return mkFPNumeral(sgn, exp, sig, s);
3618  }
com.microsoft.z3.Context.mkFPNumeral
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3520

◆ mkFP() [2/6]

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

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

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

Definition at line 3628 of file Context.java.

3629  {
3630  return mkFPNumeral(sgn, exp, sig, s);
3631  }

◆ mkFP() [3/6]

FPNum mkFP ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a double.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3590 of file Context.java.

3591  {
3592  return mkFPNumeral(v, s);
3593  }

◆ mkFP() [4/6]

FPExpr mkFP ( Expr< BitVecSort >  sgn,
Expr< BitVecSort >  sig,
Expr< BitVecSort >  exp 
)
inline

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

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

Definition at line 3913 of file Context.java.

3914  {
3915  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3916  }

◆ mkFP() [5/6]

FPNum mkFP ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3579 of file Context.java.

3580  {
3581  return mkFPNumeral(v, s);
3582  }

◆ mkFP() [6/6]

FPNum mkFP ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3602 of file Context.java.

3603  {
3604  return mkFPNumeral(v, s);
3605  }

◆ mkFPAbs()

FPExpr mkFPAbs ( Expr< FPSort >  t)
inline

Floating-point absolute value

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3639 of file Context.java.

3640  {
3641  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3642  }

◆ mkFPAdd()

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

Floating-point addition

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

Definition at line 3661 of file Context.java.

3662  {
3663  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3664  }

◆ mkFPDiv()

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

Floating-point division

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

Definition at line 3697 of file Context.java.

3698  {
3699  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3700  }

◆ mkFPEq()

BoolExpr mkFPEq ( Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point equality.

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

Definition at line 3825 of file Context.java.

3826  {
3827  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3828  }

◆ mkFPFMA()

FPExpr mkFPFMA ( Expr< FPRMSort >  rm,
Expr< FPSort >  t1,
Expr< FPSort >  t2,
Expr< FPSort >  t3 
)
inline

Floating-point fused multiply-add

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

Definition at line 3712 of file Context.java.

3713  {
3714  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3715  }

◆ mkFPGEq()

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

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3801 of file Context.java.

3802  {
3803  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3804  }

◆ mkFPGt()

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

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3812 of file Context.java.

3813  {
3814  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3815  }

◆ mkFPInf()

FPNum mkFPInf ( FPSort  s,
boolean  negative 
)
inline

Create a floating-point infinity of sort s.

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

Definition at line 3498 of file Context.java.

3499  {
3500  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3501  }

◆ mkFPIsInfinite()

BoolExpr mkFPIsInfinite ( Expr< FPSort >  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3865 of file Context.java.

3866  {
3867  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3868  }

◆ mkFPIsNaN()

BoolExpr mkFPIsNaN ( Expr< FPSort >  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3875 of file Context.java.

3876  {
3877  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3878  }

◆ mkFPIsNegative()

BoolExpr mkFPIsNegative ( Expr< FPSort >  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3885 of file Context.java.

3886  {
3887  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3888  }

◆ mkFPIsNormal()

BoolExpr mkFPIsNormal ( Expr< FPSort >  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3835 of file Context.java.

3836  {
3837  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3838  }

◆ mkFPIsPositive()

BoolExpr mkFPIsPositive ( Expr< FPSort >  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3895 of file Context.java.

3896  {
3897  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3898  }

◆ mkFPIsSubnormal()

BoolExpr mkFPIsSubnormal ( Expr< FPSort >  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3845 of file Context.java.

3846  {
3847  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3848  }

◆ mkFPIsZero()

BoolExpr mkFPIsZero ( Expr< FPSort >  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3855 of file Context.java.

3856  {
3857  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3858  }

◆ mkFPLEq()

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

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3779 of file Context.java.

3780  {
3781  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3782  }

◆ mkFPLt()

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

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3790 of file Context.java.

3791  {
3792  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3793  }

◆ mkFPMax()

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

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3768 of file Context.java.

3769  {
3770  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3771  }

◆ mkFPMin()

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

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3757 of file Context.java.

3758  {
3759  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3760  }

◆ mkFPMul()

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

Floating-point multiplication

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

Definition at line 3685 of file Context.java.

3686  {
3687  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3688  }

◆ mkFPNaN()

FPNum mkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3487 of file Context.java.

3488  {
3489  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3490  }

◆ mkFPNeg()

FPExpr mkFPNeg ( Expr< FPSort >  t)
inline

Floating-point negation

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3649 of file Context.java.

3650  {
3651  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3652  }

◆ mkFPNumeral() [1/5]

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

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

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

Definition at line 3555 of file Context.java.

3556  {
3557  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3558  }

◆ mkFPNumeral() [2/5]

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

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

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

Definition at line 3568 of file Context.java.

3569  {
3570  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3571  }

◆ mkFPNumeral() [3/5]

FPNum mkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a double.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3531 of file Context.java.

3532  {
3533  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3534  }

◆ mkFPNumeral() [4/5]

FPNum mkFPNumeral ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3520 of file Context.java.

3521  {
3522  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3523  }

◆ mkFPNumeral() [5/5]

FPNum mkFPNumeral ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3542 of file Context.java.

3543  {
3544  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3545  }

◆ mkFPRem()

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

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3734 of file Context.java.

3735  {
3736  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3737  }

◆ mkFPRNA()

FPRMNum mkFPRNA ( )
inline

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

Exceptions
Z3Exception

Definition at line 3339 of file Context.java.

3340  {
3341  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3342  }

◆ mkFPRNE()

FPRMNum mkFPRNE ( )
inline

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

Exceptions
Z3Exception

Definition at line 3321 of file Context.java.

3322  {
3323  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3324  }

◆ mkFPRoundingModeSort()

FPRMSort mkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Exceptions
Z3Exception

Definition at line 3303 of file Context.java.

3304  {
3305  return new FPRMSort(this);
3306  }

◆ mkFPRoundNearestTiesToAway()

FPRMNum mkFPRoundNearestTiesToAway ( )
inline

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

Exceptions
Z3Exception

Definition at line 3330 of file Context.java.

3331  {
3332  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3333  }

◆ mkFPRoundNearestTiesToEven()

FPRMExpr mkFPRoundNearestTiesToEven ( )
inline

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

Exceptions
Z3Exception

Definition at line 3312 of file Context.java.

3313  {
3314  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3315  }

◆ mkFPRoundToIntegral()

FPExpr mkFPRoundToIntegral ( Expr< FPRMSort >  rm,
Expr< FPSort >  t 
)
inline

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

Parameters
rmterm of RoundingMode sort
tfloating-point term
Exceptions
Z3Exception

Definition at line 3746 of file Context.java.

3747  {
3748  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3749  }

◆ mkFPRoundTowardNegative()

FPRMNum mkFPRoundTowardNegative ( )
inline

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

Exceptions
Z3Exception

Definition at line 3366 of file Context.java.

3367  {
3368  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3369  }

◆ mkFPRoundTowardPositive()

FPRMNum mkFPRoundTowardPositive ( )
inline

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

Exceptions
Z3Exception

Definition at line 3348 of file Context.java.

3349  {
3350  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3351  }

◆ mkFPRoundTowardZero()

FPRMNum mkFPRoundTowardZero ( )
inline

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

Exceptions
Z3Exception

Definition at line 3384 of file Context.java.

3385  {
3386  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3387  }

◆ mkFPRTN()

FPRMNum mkFPRTN ( )
inline

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

Exceptions
Z3Exception

Definition at line 3375 of file Context.java.

3376  {
3377  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3378  }

◆ mkFPRTP()

FPRMNum mkFPRTP ( )
inline

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

Exceptions
Z3Exception

Definition at line 3357 of file Context.java.

3358  {
3359  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3360  }

◆ mkFPRTZ()

FPRMNum mkFPRTZ ( )
inline

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

Exceptions
Z3Exception

Definition at line 3393 of file Context.java.

3394  {
3395  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3396  }

◆ mkFPSort()

FPSort mkFPSort ( int  ebits,
int  sbits 
)
inline

Create a FloatingPoint sort.

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

Definition at line 3404 of file Context.java.

3405  {
3406  return new FPSort(this, ebits, sbits);
3407  }
z3py.FPSort
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9901

◆ mkFPSort128()

FPSort mkFPSort128 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3476 of file Context.java.

3477  {
3478  return new FPSort(this, Native.mkFpaSort128(nCtx()));
3479  }

◆ mkFPSort16()

FPSort mkFPSort16 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3422 of file Context.java.

3423  {
3424  return new FPSort(this, Native.mkFpaSort16(nCtx()));
3425  }

◆ mkFPSort32()

FPSort mkFPSort32 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3440 of file Context.java.

3441  {
3442  return new FPSort(this, Native.mkFpaSort32(nCtx()));
3443  }

◆ mkFPSort64()

FPSort mkFPSort64 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3458 of file Context.java.

3459  {
3460  return new FPSort(this, Native.mkFpaSort64(nCtx()));
3461  }

◆ mkFPSortDouble()

FPSort mkFPSortDouble ( )
inline

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

Exceptions
Z3Exception

Definition at line 3449 of file Context.java.

3450  {
3451  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3452  }

◆ mkFPSortHalf()

FPSort mkFPSortHalf ( )
inline

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

Exceptions
Z3Exception

Definition at line 3413 of file Context.java.

3414  {
3415  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3416  }

◆ mkFPSortQuadruple()

FPSort mkFPSortQuadruple ( )
inline

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

Exceptions
Z3Exception

Definition at line 3467 of file Context.java.

3468  {
3469  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3470  }

◆ mkFPSortSingle()

FPSort mkFPSortSingle ( )
inline

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

Exceptions
Z3Exception

Definition at line 3431 of file Context.java.

3432  {
3433  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3434  }

◆ mkFPSqrt()

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

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term
Exceptions
Z3Exception

Definition at line 3723 of file Context.java.

3724  {
3725  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3726  }

◆ mkFPSub()

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

Floating-point subtraction

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

Definition at line 3673 of file Context.java.

3674  {
3675  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3676  }

◆ mkFPToBV()

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

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

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

Definition at line 4014 of file Context.java.

4015  {
4016  if (signed)
4017  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
4018  else
4019  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
4020  }

◆ mkFPToFP() [1/6]

FPExpr mkFPToFP ( Expr< BitVecSort >  bv,
FPSort  s 
)
inline

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

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

Definition at line 3929 of file Context.java.

3930  {
3931  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3932  }

◆ mkFPToFP() [2/6]

FPExpr mkFPToFP ( Expr< FPRMSort >  rm,
Expr< BitVecSort >  t,
FPSort  s,
boolean signed   
)
inline

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

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

Definition at line 3979 of file Context.java.

3980  {
3981  if (signed)
3982  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3983  else
3984  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3985  }

◆ mkFPToFP() [3/6]

BitVecExpr mkFPToFP ( Expr< FPRMSort >  rm,
Expr< IntSort >  exp,
Expr< RealSort >  sig,
FPSort  s 
)
inline

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

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

Definition at line 4064 of file Context.java.

4065  {
4066  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
4067  }

◆ mkFPToFP() [4/6]

FPExpr mkFPToFP ( Expr< FPRMSort >  rm,
FPExpr  t,
FPSort  s 
)
inline

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

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

Definition at line 3945 of file Context.java.

3946  {
3947  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3948  }

◆ mkFPToFP() [5/6]

FPExpr mkFPToFP ( Expr< FPRMSort >  rm,
RealExpr  t,
FPSort  s 
)
inline

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

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

Definition at line 3961 of file Context.java.

3962  {
3963  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3964  }

◆ mkFPToFP() [6/6]

FPExpr mkFPToFP ( FPSort  s,
Expr< FPRMSort >  rm,
Expr< FPSort >  t 
)
inline

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

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

Definition at line 3997 of file Context.java.

3998  {
3999  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
4000  }

◆ mkFPToIEEEBV()

BitVecExpr mkFPToIEEEBV ( Expr< FPSort >  t)
inline

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

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

Definition at line 4046 of file Context.java.

4047  {
4048  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
4049  }

◆ mkFPToReal()

RealExpr mkFPToReal ( Expr< FPSort >  t)
inline

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

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

Definition at line 4031 of file Context.java.

4032  {
4033  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
4034  }

◆ mkFPZero()

FPNum mkFPZero ( FPSort  s,
boolean  negative 
)
inline

Create a floating-point zero of sort s.

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

Definition at line 3509 of file Context.java.

3510  {
3511  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3512  }

◆ mkGe()

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

Create an expression representing

t1 &gt;= t2
com.microsoft.z3.Context.gt
Probe gt(Probe p1, Probe p2)
Definition: Context.java:3146

Definition at line 964 of file Context.java.

965  {
966  checkContextMatch(t1);
967  checkContextMatch(t2);
968  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
969  t2.getNativeObject()));
970  }

◆ mkGoal()

Goal mkGoal ( boolean  models,
boolean  unsatCores,
boolean  proofs 
)
inline

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

proofs

is set to true here.

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

Definition at line 2836 of file Context.java.

2837  {
2838  return new Goal(this, models, unsatCores, proofs);
2839  }

◆ mkGt()

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

Create an expression representing

t1 &gt; t2

Definition at line 953 of file Context.java.

954  {
955  checkContextMatch(t1);
956  checkContextMatch(t2);
957  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
958  t2.getNativeObject()));
959  }

◆ mkIff()

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

Create an expression representing

t1 iff t2

.

Definition at line 782 of file Context.java.

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

◆ mkImplies()

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

Create an expression representing

t1 -> t2

.

Definition at line 793 of file Context.java.

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

◆ mkInt() [1/3]

IntNum mkInt ( int  v)
inline

Create an integer numeral.

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

Definition at line 2546 of file Context.java.

2547  {
2548 
2549  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2550  .getNativeObject()));
2551  }

◆ mkInt() [2/3]

IntNum mkInt ( long  v)
inline

Create an integer numeral.

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

Definition at line 2559 of file Context.java.

2560  {
2561 
2562  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2563  .getNativeObject()));
2564  }

◆ mkInt() [3/3]

IntNum mkInt ( String  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 2533 of file Context.java.

2534  {
2535 
2536  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2537  .getNativeObject()));
2538  }

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

1556  {
1557  checkContextMatch(t);
1558  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1559  t.getNativeObject()));
1560  }

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

983  {
984  checkContextMatch(t);
985  return new RealExpr(this,
986  Native.mkInt2real(nCtx(), t.getNativeObject()));
987  }

◆ mkIntConst() [1/2]

IntExpr mkIntConst ( String  name)
inline

Creates an integer constant.

Definition at line 660 of file Context.java.

661  {
662  return (IntExpr) mkConst(name, getIntSort());
663  }

◆ mkIntConst() [2/2]

IntExpr mkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 652 of file Context.java.

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

◆ mkIntersect()

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

Create the intersection of regular languages.

Definition at line 2279 of file Context.java.

2280  {
2281  checkContextMatch(t);
2282  return (ReExpr<R>) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
2283  }

◆ mkIntSort()

IntSort mkIntSort ( )
inline

Create a new integer sort.

Definition at line 206 of file Context.java.

207  {
208  return new IntSort(this);
209  }

◆ mkIsDigit()

BoolExpr mkIsDigit ( Expr< CharSort >  ch)
inline

Create a check if the character is a digit.

Definition at line 2370 of file Context.java.

2371  {
2372  checkContextMatch(ch);
2373  return (BoolExpr) Expr.create(this, Native.mkCharIsDigit(nCtx(), ch.getNativeObject()));
2374  }

◆ mkIsInteger()

BoolExpr mkIsInteger ( Expr< RealSort >  t)
inline

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

Definition at line 1004 of file Context.java.

1005  {
1006  checkContextMatch(t);
1007  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
1008  }

◆ mkLe()

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

Create an expression representing

t1 &lt;= t2

Definition at line 942 of file Context.java.

943  {
944  checkContextMatch(t1);
945  checkContextMatch(t2);
946  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
947  t2.getNativeObject()));
948  }

◆ mkLt()

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

Create an expression representing

t1 &lt; t2

Definition at line 931 of file Context.java.

932  {
933  checkContextMatch(t1);
934  checkContextMatch(t2);
935  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
936  t2.getNativeObject()));
937  }

◆ 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
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3970

.

v

must have sort range. The sort of the result is

[domain_i -> range]

.

See also
#mkArraySort(Sort[], R)
#mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
#mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)

Definition at line 1835 of file Context.java.

1836  {
1837  checkContextMatch(f);
1838  checkContextMatch(args);
1839  return (ArrayExpr<D, R2>) Expr.create(this, Native.mkMap(nCtx(),
1840  f.getNativeObject(), AST.arrayLength(args),
1841  AST.arrayToNative(args)));
1842  }

◆ mkMod()

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

Create an expression representing

t1 mod t2
z3::mod
expr mod(expr const &a, expr const &b)
Definition: z3++.h:1627

. Remarks: The arguments must have int type.

Definition at line 893 of file Context.java.

894  {
895  checkContextMatch(t1);
896  checkContextMatch(t2);
897  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
898  t2.getNativeObject()));
899  }

◆ mkMul()

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

Create an expression representing

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

.

Definition at line 849 of file Context.java.

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

◆ mkNot()

BoolExpr mkNot ( Expr< BoolSort >  a)
inline

Create an expression representing

not(a)
com.microsoft.z3.Context.not
Probe not(Probe p)
Definition: Context.java:3217

.

Definition at line 757 of file Context.java.

758  {
759  checkContextMatch(a);
760  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
761  }

◆ mkOptimize()

Optimize mkOptimize ( )
inline

Create a Optimize context.

Definition at line 3293 of file Context.java.

3294  {
3295  return new Optimize(this);
3296  }

◆ mkOr()

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

Create an expression representing

t[0] or t[1] or ...
com.microsoft.z3.Context.or
Probe or(Probe p1, Probe p2)
Definition: Context.java:3206

.

Definition at line 827 of file Context.java.

828  {
829  checkContextMatch(t);
830  return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
831  AST.arrayToNative(t)));
832  }

◆ mkParams()

Params mkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2844 of file Context.java.

2845  {
2846  return new Params(this);
2847  }

◆ mkPattern()

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

Create a quantifier pattern.

Definition at line 579 of file Context.java.

580  {
581  if (terms.length == 0)
582  throw new Z3Exception("Cannot create a pattern from zero terms");
583 
584  long[] termsNative = AST.arrayToNative(terms);
585  return new Pattern(this, Native.mkPattern(nCtx(), terms.length,
586  termsNative));
587  }

◆ mkPBEq()

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

Create a pseudo-Boolean equal constraint.

Definition at line 2415 of file Context.java.

2416  {
2417  checkContextMatch(args);
2418  return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2419  }

◆ mkPBGe()

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

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

Definition at line 2406 of file Context.java.

2407  {
2408  checkContextMatch(args);
2409  return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2410  }

◆ mkPBLe()

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

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

Definition at line 2397 of file Context.java.

2398  {
2399  checkContextMatch(args);
2400  return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2401  }

◆ mkProbe()

Probe mkProbe ( String  name)
inline

Creates a new Probe.

Definition at line 3117 of file Context.java.

3118  {
3119  return new Probe(this, name);
3120  }

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

2693  {
2694 
2695  if (universal)
2696  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2697  quantifierID, skolemID);
2698  else
2699  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2700  quantifierID, skolemID);
2701  }
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:2621
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:2646

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

2676  {
2677 
2678  if (universal)
2679  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2680  quantifierID, skolemID);
2681  else
2682  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2683  quantifierID, skolemID);
2684  }

◆ mkReal() [1/4]

RatNum mkReal ( int  num,
int  den 
)
inline

Create a real from a fraction.

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

Definition at line 2481 of file Context.java.

2482  {
2483  if (den == 0) {
2484  throw new Z3Exception("Denominator is zero");
2485  }
2486 
2487  return new RatNum(this, Native.mkReal(nCtx(), num, den));
2488  }

◆ mkReal() [2/4]

RatNum mkReal ( int  v)
inline

Create a real numeral.

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

Definition at line 2509 of file Context.java.

2510  {
2511 
2512  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2513  .getNativeObject()));
2514  }

◆ mkReal() [3/4]

RatNum mkReal ( long  v)
inline

Create a real numeral.

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

Definition at line 2522 of file Context.java.

2523  {
2524 
2525  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2526  .getNativeObject()));
2527  }

◆ mkReal() [4/4]

RatNum mkReal ( String  v)
inline

Create a real numeral.

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

Definition at line 2496 of file Context.java.

2497  {
2498 
2499  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2500  .getNativeObject()));
2501  }

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

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

◆ mkRealConst() [1/2]

RealExpr mkRealConst ( String  name)
inline

Creates a real constant.

Definition at line 676 of file Context.java.

677  {
678  return (RealExpr) mkConst(name, getRealSort());
679  }

◆ mkRealConst() [2/2]

RealExpr mkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 668 of file Context.java.

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

◆ mkRealSort()

RealSort mkRealSort ( )
inline

Create a real sort.

Definition at line 214 of file Context.java.

215  {
216  return new RealSort(this);
217  }

◆ mkRem()

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

Create an expression representing

t1 rem t2
z3::rem
expr rem(expr const &a, expr const &b)
Definition: z3++.h:1643

. Remarks: The arguments must have int type.

Definition at line 906 of file Context.java.

907  {
908  checkContextMatch(t1);
909  checkContextMatch(t2);
910  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
911  t2.getNativeObject()));
912  }

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

1428  {
1429  checkContextMatch(t);
1430  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1431  t.getNativeObject()));
1432  }

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

1938  {
1939  checkContextMatch(args);
1940  return (ArrayExpr<D, BoolSort>) Expr.create(this,
1941  Native.mkSetIntersect(nCtx(), args.length,
1942  AST.arrayToNative(args)));
1943  }

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

1926  {
1927  checkContextMatch(args);
1928  return (ArrayExpr<D, BoolSort>)Expr.create(this,
1929  Native.mkSetUnion(nCtx(), args.length,
1930  AST.arrayToNative(args)));
1931  }

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

1402  {
1403  checkContextMatch(t);
1404  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1405  t.getNativeObject()));
1406  }

◆ mkSimpleSolver()

Solver mkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3264 of file Context.java.

3265  {
3266  return new Solver(this, Native.mkSimpleSolver(nCtx()));
3267  }

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

3231  {
3232  return mkSolver((Symbol) null);
3233  }

Referenced by Tactic.getSolver().

◆ mkSolver() [2/4]

Solver mkSolver ( String  logic)
inline

Creates a new (incremental) solver.

See also
mkSolver(Symbol)

Definition at line 3256 of file Context.java.

3257  {
3258  return mkSolver(mkSymbol(logic));
3259  }

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

3243  {
3244 
3245  if (logic == null)
3246  return new Solver(this, Native.mkSolver(nCtx()));
3247  else
3248  return new Solver(this, Native.mkSolverForLogic(nCtx(),
3249  logic.getNativeObject()));
3250  }

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

3276  {
3277 
3278  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3279  t.getNativeObject()));
3280  }

◆ mkString()

SeqExpr<CharSort> mkString ( String  s)
inline

Create a string constant.

Definition at line 2017 of file Context.java.

2018  {
2019  StringBuilder buf = new StringBuilder();
2020  for (int i = 0; i < s.length(); ++i) {
2021  int code = s.codePointAt(i);
2022  if (code <= 32 || 127 < code)
2023  buf.append(String.format("\\u{%x}", code));
2024  else
2025  buf.append(s.charAt(i));
2026  }
2027  return (SeqExpr<CharSort>) Expr.create(this, Native.mkString(nCtx(), buf.toString()));
2028  }

◆ MkStringLe()

BoolExpr MkStringLe ( SeqSort< CharSort >  s1,
SeqSort< CharSort >  s2 
)
inline

Check if the string s1 is lexicographically less or equal to s2.

Definition at line 2122 of file Context.java.

2123  {
2124  checkContextMatch(s1, s2);
2125  return new BoolExpr(this, Native.mkStrLe(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2126  }

◆ MkStringLt()

BoolExpr MkStringLt ( SeqSort< CharSort >  s1,
SeqSort< CharSort >  s2 
)
inline

Check if the string s1 is lexicographically strictly less than s2.

Definition at line 2113 of file Context.java.

2114  {
2115  checkContextMatch(s1, s2);
2116  return new BoolExpr(this, Native.mkStrLt(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2117  }

◆ mkStringSort()

SeqSort<CharSort> mkStringSort ( )
inline

Create a new string sort

Definition at line 251 of file Context.java.

252  {
253  return new SeqSort<>(this, Native.mkStringSort(nCtx()));
254  }

◆ mkSub()

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

Create an expression representing

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

.

Definition at line 860 of file Context.java.

861  {
862  checkContextMatch(t);
863  return (ArithExpr<R>) Expr.create(this,
864  Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
865  }

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

2883  {
2884  return new Tactic(this, name);
2885  }

Referenced by Goal.simplify().

◆ mkTrue()

BoolExpr mkTrue ( )
inline

The true Term.

Definition at line 711 of file Context.java.

712  {
713  return new BoolExpr(this, Native.mkTrue(nCtx()));
714  }

Referenced by Goal.AsBoolExpr().

◆ mkTupleSort()

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

Create a new tuple sort.

Definition at line 276 of file Context.java.

278  {
279  checkContextMatch(name);
280  checkContextMatch(fieldNames);
281  checkContextMatch(fieldSorts);
282  return new TupleSort(this, name, fieldNames.length, fieldNames,
283  fieldSorts);
284  }
z3py.TupleSort
def TupleSort(name, sorts, ctx=None)
Definition: z3py.py:5363

◆ mkUninterpretedSort() [1/2]

UninterpretedSort mkUninterpretedSort ( String  str)
inline

Create a new uninterpreted sort.

Definition at line 198 of file Context.java.

199  {
200  return mkUninterpretedSort(mkSymbol(str));
201  }
com.microsoft.z3.Context.mkUninterpretedSort
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:189

◆ mkUninterpretedSort() [2/2]

UninterpretedSort mkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 189 of file Context.java.

190  {
191  checkContextMatch(s);
192  return new UninterpretedSort(this, s);
193  }

◆ mkUnion()

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

Create the union of regular languages.

Definition at line 2269 of file Context.java.

2270  {
2271  checkContextMatch(t);
2272  return (ReExpr<R>) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2273  }

◆ mkXor()

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

Create an expression representing

t1 xor t2

.

Definition at line 804 of file Context.java.

805  {
806  checkContextMatch(t1);
807  checkContextMatch(t2);
808  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
809  t2.getNativeObject()));
810  }

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

1416  {
1417  checkContextMatch(t);
1418  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1419  t.getNativeObject()));
1420  }

◆ nCtx()

long nCtx ( )
inline

Definition at line 4164 of file Context.java.

4165  {
4166  if (m_ctx == 0)
4167  throw new Z3Exception("Context closed");
4168  return m_ctx;
4169  }

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

3218  {
3219  checkContextMatch(p);
3220  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
3221  }

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

3207  {
3208  checkContextMatch(p1);
3209  checkContextMatch(p2);
3210  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
3211  p2.getNativeObject()));
3212  }

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

2934  {
2935  checkContextMatch(t1);
2936  checkContextMatch(t2);
2937  return new Tactic(this, Native.tacticOrElse(nCtx(),
2938  t1.getNativeObject(), t2.getNativeObject()));
2939  }

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

3067  {
3068  checkContextMatch(t1);
3069  checkContextMatch(t2);
3070  return new Tactic(this, Native.tacticParAndThen(nCtx(),
3071  t1.getNativeObject(), t2.getNativeObject()));
3072  }

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

3056  {
3057  checkContextMatch(t);
3058  return new Tactic(this, Native.tacticParOr(nCtx(),
3059  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
3060  }

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

2811  {
2812  int csn = Symbol.arrayLength(sortNames);
2813  int cs = Sort.arrayLength(sorts);
2814  int cdn = Symbol.arrayLength(declNames);
2815  int cd = AST.arrayLength(decls);
2816  if (csn != cs || cdn != cd)
2817  throw new Z3Exception("Argument size mismatch");
2818  ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
2819  fileName, AST.arrayLength(sorts),
2820  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2821  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2822  AST.arrayToNative(decls)));
2823  return v.ToBoolExprArray();
2824  }

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

2790  {
2791  int csn = Symbol.arrayLength(sortNames);
2792  int cs = Sort.arrayLength(sorts);
2793  int cdn = Symbol.arrayLength(declNames);
2794  int cd = AST.arrayLength(decls);
2795  if (csn != cs || cdn != cd) {
2796  throw new Z3Exception("Argument size mismatch");
2797  }
2798  ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
2799  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2800  AST.arrayToNative(sorts), AST.arrayLength(decls),
2801  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2802  return v.ToBoolExprArray();
2803  }

◆ 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
z3::max
expr max(expr const &a, expr const &b)
Definition: z3++.h:1953

is reached.

Definition at line 2986 of file Context.java.

2987  {
2988  checkContextMatch(t);
2989  return new Tactic(this, Native.tacticRepeat(nCtx(),
2990  t.getNativeObject(), max));
2991  }

◆ sbvToString()

SeqExpr<CharSort> sbvToString ( Expr< BitVecSort >  e)
inline

Convert an signed bitvector expression to a string.

Definition at line 2049 of file Context.java.

2050  {
2051  return (SeqExpr<CharSort>) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject()));
2052  }

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

2752  {
2753  Native.setAstPrintMode(nCtx(), value.toInt());
2754  }

◆ SimplifyHelp()

String SimplifyHelp ( )
inline

Return a string describing all available parameters to

Expr.Simplify

.

Definition at line 4137 of file Context.java.

4138  {
4139  return Native.simplifyGetHelp(nCtx());
4140  }

◆ skip()

Tactic skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 2996 of file Context.java.

2997  {
2998  return new Tactic(this, Native.tacticSkip(nCtx()));
2999  }

◆ stringToInt()

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

Convert an integer expression to a string.

Definition at line 2057 of file Context.java.

2058  {
2059  return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
2060  }

◆ 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
z3py.AndThen
def AndThen(*ts, **ks)
Definition: z3py.py:8297

.

Definition at line 2923 of file Context.java.

2924  {
2925  return andThen(t1, t2, ts);
2926  }
com.microsoft.z3.Context.andThen
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2891

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

2948  {
2949  checkContextMatch(t);
2950  return new Tactic(this, Native.tacticTryFor(nCtx(),
2951  t.getNativeObject(), ms));
2952  }

◆ ubvToString()

SeqExpr<CharSort> ubvToString ( Expr< BitVecSort >  e)
inline

Convert an unsigned bitvector expression to a string.

Definition at line 2041 of file Context.java.

2042  {
2043  return (SeqExpr<CharSort>) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
2044  }

◆ unwrapAST()

long unwrapAST ( AST  a)
inline

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

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

Definition at line 4128 of file Context.java.

4129  {
4130  return a.getNativeObject();
4131  }

◆ 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?
z3
Z3 C++ namespace.
Definition: z3++.h:49

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

4159  {
4160  Native.updateParamValue(nCtx(), id, value);
4161  }

◆ usingParams()

Tactic usingParams ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

.

Definition at line 3033 of file Context.java.

3034  {
3035  checkContextMatch(t);
3036  checkContextMatch(p);
3037  return new Tactic(this, Native.tacticUsingParams(nCtx(),
3038  t.getNativeObject(), p.getNativeObject()));
3039  }

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

2961  {
2962  checkContextMatch(t);
2963  checkContextMatch(p);
2964  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2965  t.getNativeObject()));
2966  }

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

3048  {
3049  return usingParams(t, p);
3050  }
com.microsoft.z3.Context.usingParams
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:3033

◆ wrapAST()

AST wrapAST ( long  nativeObject)
inline

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

nativeObject

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

UnwrapAST

) and that it must have a correct reference count.

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

Definition at line 4111 of file Context.java.

4112  {
4113  return AST.create(this, nativeObject);
4114  }
Generated on Sat Jan 14 2023 14:44:09 for Z3 by doxygen 1.9.1