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

Public Member Functions

 Context ()
 
 Context (Map< String, String > settings)
 
IntSymbol mkSymbol (int i)
 
StringSymbol mkSymbol (String name)
 
BoolSort getBoolSort ()
 
IntSort getIntSort ()
 
RealSort getRealSort ()
 
BoolSort mkBoolSort ()
 
SeqSort getStringSort ()
 
UninterpretedSort mkUninterpretedSort (Symbol s)
 
UninterpretedSort mkUninterpretedSort (String str)
 
IntSort mkIntSort ()
 
RealSort mkRealSort ()
 
BitVecSort mkBitVecSort (int size)
 
ArraySort mkArraySort (Sort domain, Sort range)
 
ArraySort mkArraySort (Sort[] domains, Sort range)
 
SeqSort mkStringSort ()
 
SeqSort mkSeqSort (Sort s)
 
ReSort mkReSort (Sort s)
 
TupleSort mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
 
EnumSort mkEnumSort (Symbol name, Symbol... enumNames)
 
EnumSort mkEnumSort (String name, String... enumNames)
 
ListSort mkListSort (Symbol name, Sort elemSort)
 
ListSort mkListSort (String name, Sort elemSort)
 
FiniteDomainSort mkFiniteDomainSort (Symbol name, long size)
 
FiniteDomainSort mkFiniteDomainSort (String name, long size)
 
Constructor mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
 
Constructor mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
 
DatatypeSort mkDatatypeSort (Symbol name, Constructor[] constructors)
 
DatatypeSort mkDatatypeSort (String name, Constructor[] constructors)
 
DatatypeSort[] mkDatatypeSorts (Symbol[] names, Constructor[][] c)
 
DatatypeSort[] mkDatatypeSorts (String[] names, Constructor[][] c)
 
Expr mkUpdateField (FuncDecl field, Expr t, Expr v) throws Z3Exception
 
FuncDecl mkFuncDecl (Symbol name, Sort[] domain, Sort range)
 
FuncDecl mkFuncDecl (Symbol name, Sort domain, Sort range)
 
FuncDecl mkFuncDecl (String name, Sort[] domain, Sort range)
 
FuncDecl mkFuncDecl (String name, Sort domain, Sort range)
 
FuncDecl mkFreshFuncDecl (String prefix, Sort[] domain, Sort range)
 
FuncDecl mkConstDecl (Symbol name, Sort range)
 
FuncDecl mkConstDecl (String name, Sort range)
 
FuncDecl mkFreshConstDecl (String prefix, Sort range)
 
Expr mkBound (int index, Sort ty)
 
Pattern mkPattern (Expr... terms)
 
Expr mkConst (Symbol name, Sort range)
 
Expr mkConst (String name, Sort range)
 
Expr mkFreshConst (String prefix, Sort range)
 
Expr mkConst (FuncDecl f)
 
BoolExpr mkBoolConst (Symbol name)
 
BoolExpr mkBoolConst (String name)
 
IntExpr mkIntConst (Symbol name)
 
IntExpr mkIntConst (String name)
 
RealExpr mkRealConst (Symbol name)
 
RealExpr mkRealConst (String name)
 
BitVecExpr mkBVConst (Symbol name, int size)
 
BitVecExpr mkBVConst (String name, int size)
 
Expr mkApp (FuncDecl f, Expr... args)
 
BoolExpr mkTrue ()
 
BoolExpr mkFalse ()
 
BoolExpr mkBool (boolean value)
 
BoolExpr mkEq (Expr x, Expr y)
 
BoolExpr mkDistinct (Expr... args)
 
BoolExpr mkNot (BoolExpr a)
 
Expr mkITE (BoolExpr t1, Expr t2, Expr t3)
 
BoolExpr mkIff (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkImplies (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkXor (BoolExpr t1, BoolExpr t2)
 
BoolExpr mkAnd (BoolExpr... t)
 
BoolExpr mkOr (BoolExpr... t)
 
ArithExpr mkAdd (ArithExpr... t)
 
ArithExpr mkMul (ArithExpr... t)
 
ArithExpr mkSub (ArithExpr... t)
 
ArithExpr mkUnaryMinus (ArithExpr t)
 
ArithExpr mkDiv (ArithExpr t1, ArithExpr t2)
 
IntExpr mkMod (IntExpr t1, IntExpr t2)
 
IntExpr mkRem (IntExpr t1, IntExpr t2)
 
ArithExpr mkPower (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkLt (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkLe (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkGt (ArithExpr t1, ArithExpr t2)
 
BoolExpr mkGe (ArithExpr t1, ArithExpr t2)
 
RealExpr mkInt2Real (IntExpr t)
 
IntExpr mkReal2Int (RealExpr t)
 
BoolExpr mkIsInteger (RealExpr t)
 
BitVecExpr mkBVNot (BitVecExpr t)
 
BitVecExpr mkBVRedAND (BitVecExpr t)
 
BitVecExpr mkBVRedOR (BitVecExpr t)
 
BitVecExpr mkBVAND (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVXOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNAND (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVXNOR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVNeg (BitVecExpr t)
 
BitVecExpr mkBVAdd (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSub (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVMul (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVUDiv (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSDiv (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVURem (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSRem (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVSMod (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVULT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSLT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVULE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSLE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVUGE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSGE (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVUGT (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSGT (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkConcat (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkExtract (int high, int low, BitVecExpr t)
 
BitVecExpr mkSignExt (int i, BitVecExpr t)
 
BitVecExpr mkZeroExt (int i, BitVecExpr t)
 
BitVecExpr mkRepeat (int i, BitVecExpr t)
 
BitVecExpr mkBVSHL (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVLSHR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVASHR (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVRotateLeft (int i, BitVecExpr t)
 
BitVecExpr mkBVRotateRight (int i, BitVecExpr t)
 
BitVecExpr mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkBVRotateRight (BitVecExpr t1, BitVecExpr t2)
 
BitVecExpr mkInt2BV (int n, IntExpr t)
 
IntExpr mkBV2Int (BitVecExpr t, boolean signed)
 
BoolExpr mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2)
 
BoolExpr mkBVNegNoOverflow (BitVecExpr t)
 
BoolExpr mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)
 
BoolExpr mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 
ArrayExpr mkArrayConst (Symbol name, Sort domain, Sort range)
 
ArrayExpr mkArrayConst (String name, Sort domain, Sort range)
 
Expr mkSelect (ArrayExpr a, Expr i)
 
Expr mkSelect (ArrayExpr a, Expr[] args)
 
ArrayExpr mkStore (ArrayExpr a, Expr i, Expr v)
 
ArrayExpr mkStore (ArrayExpr a, Expr[] args, Expr v)
 
ArrayExpr mkConstArray (Sort domain, Expr v)
 
ArrayExpr mkMap (FuncDecl f, ArrayExpr... args)
 
Expr mkTermArray (ArrayExpr array)
 
Expr mkArrayExt (ArrayExpr arg1, ArrayExpr arg2)
 
SetSort mkSetSort (Sort ty)
 
ArrayExpr mkEmptySet (Sort domain)
 
ArrayExpr mkFullSet (Sort domain)
 
ArrayExpr mkSetAdd (ArrayExpr set, Expr element)
 
ArrayExpr mkSetDel (ArrayExpr set, Expr element)
 
ArrayExpr mkSetUnion (ArrayExpr... args)
 
ArrayExpr mkSetIntersection (ArrayExpr... args)
 
ArrayExpr mkSetDifference (ArrayExpr arg1, ArrayExpr arg2)
 
ArrayExpr mkSetComplement (ArrayExpr arg)
 
BoolExpr mkSetMembership (Expr elem, ArrayExpr set)
 
BoolExpr mkSetSubset (ArrayExpr arg1, ArrayExpr arg2)
 
SeqExpr mkEmptySeq (Sort s)
 
SeqExpr mkUnit (Expr elem)
 
SeqExpr mkString (String s)
 
SeqExpr intToString (Expr e)
 
IntExpr stringToInt (Expr e)
 
SeqExpr mkConcat (SeqExpr... t)
 
IntExpr mkLength (SeqExpr s)
 
BoolExpr mkPrefixOf (SeqExpr s1, SeqExpr s2)
 
BoolExpr mkSuffixOf (SeqExpr s1, SeqExpr s2)
 
BoolExpr mkContains (SeqExpr s1, SeqExpr s2)
 
SeqExpr mkAt (SeqExpr s, IntExpr index)
 
SeqExpr mkExtract (SeqExpr s, IntExpr offset, IntExpr length)
 
IntExpr mkIndexOf (SeqExpr s, SeqExpr substr, ArithExpr offset)
 
SeqExpr mkReplace (SeqExpr s, SeqExpr src, SeqExpr dst)
 
ReExpr mkToRe (SeqExpr s)
 
BoolExpr mkInRe (SeqExpr s, ReExpr re)
 
ReExpr mkStar (ReExpr re)
 
ReExpr mkLoop (ReExpr re, int lo, int hi)
 
ReExpr mkLoop (ReExpr re, int lo)
 
ReExpr mkPlus (ReExpr re)
 
ReExpr mkOption (ReExpr re)
 
ReExpr mkComplement (ReExpr re)
 
ReExpr mkConcat (ReExpr... t)
 
ReExpr mkUnion (ReExpr... t)
 
ReExpr mkIntersect (ReExpr... t)
 
ReExpr mkEmptyRe (Sort s)
 
ReExpr mkFullRe (Sort s)
 
ReExpr mkRange (SeqExpr lo, SeqExpr hi)
 
BoolExpr mkAtMost (BoolExpr[] args, int k)
 
BoolExpr mkAtLeast (BoolExpr[] args, int k)
 
BoolExpr mkPBLe (int[] coeffs, BoolExpr[] args, int k)
 
BoolExpr mkPBGe (int[] coeffs, BoolExpr[] args, int k)
 
BoolExpr mkPBEq (int[] coeffs, BoolExpr[] args, int k)
 
Expr mkNumeral (String v, Sort ty)
 
Expr mkNumeral (int v, Sort ty)
 
Expr mkNumeral (long v, Sort ty)
 
RatNum mkReal (int num, int den)
 
RatNum mkReal (String v)
 
RatNum mkReal (int v)
 
RatNum mkReal (long v)
 
IntNum mkInt (String v)
 
IntNum mkInt (int v)
 
IntNum mkInt (long v)
 
BitVecNum mkBV (String v, int size)
 
BitVecNum mkBV (int v, int size)
 
BitVecNum mkBV (long v, int size)
 
Quantifier mkForall (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkForall (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkExists (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkExists (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkQuantifier (boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Lambda mkLambda (Sort[] sorts, Symbol[] names, Expr body)
 
Lambda mkLambda (Expr[] boundConstants, Expr body)
 
void setPrintMode (Z3_ast_print_mode value)
 
String benchmarkToSMTString (String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr 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 (FPExpr t)
 
FPExpr mkFPNeg (FPExpr t)
 
FPExpr mkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2)
 
FPExpr mkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
 
FPExpr mkFPSqrt (FPRMExpr rm, FPExpr t)
 
FPExpr mkFPRem (FPExpr t1, FPExpr t2)
 
FPExpr mkFPRoundToIntegral (FPRMExpr rm, FPExpr t)
 
FPExpr mkFPMin (FPExpr t1, FPExpr t2)
 
FPExpr mkFPMax (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPLEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPLt (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPGEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPGt (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPEq (FPExpr t1, FPExpr t2)
 
BoolExpr mkFPIsNormal (FPExpr t)
 
BoolExpr mkFPIsSubnormal (FPExpr t)
 
BoolExpr mkFPIsZero (FPExpr t)
 
BoolExpr mkFPIsInfinite (FPExpr t)
 
BoolExpr mkFPIsNaN (FPExpr t)
 
BoolExpr mkFPIsNegative (FPExpr t)
 
BoolExpr mkFPIsPositive (FPExpr t)
 
FPExpr mkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
 
FPExpr mkFPToFP (BitVecExpr bv, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, FPExpr t, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, RealExpr t, FPSort s)
 
FPExpr mkFPToFP (FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
 
FPExpr mkFPToFP (FPSort s, FPRMExpr rm, FPExpr t)
 
BitVecExpr mkFPToBV (FPRMExpr rm, FPExpr t, int sz, boolean signed)
 
RealExpr mkFPToReal (FPExpr t)
 
BitVecExpr mkFPToIEEEBV (FPExpr t)
 
BitVecExpr mkFPToFP (FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
 
AST wrapAST (long nativeObject)
 
long unwrapAST (AST a)
 
String SimplifyHelp ()
 
ParamDescrs getSimplifyParameterDescriptions ()
 
void updateParamValue (String id, String value)
 
IDecRefQueue< ConstructorgetConstructorDRQ ()
 
IDecRefQueue< ConstructorListgetConstructorListDRQ ()
 
IDecRefQueue< ASTgetASTDRQ ()
 
IDecRefQueue< ASTMap > getASTMapDRQ ()
 
IDecRefQueue< ASTVectorgetASTVectorDRQ ()
 
IDecRefQueue< ApplyResultgetApplyResultDRQ ()
 
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ ()
 
IDecRefQueue< FuncInterpgetFuncInterpDRQ ()
 
IDecRefQueue< GoalgetGoalDRQ ()
 
IDecRefQueue< ModelgetModelDRQ ()
 
IDecRefQueue< ParamsgetParamsDRQ ()
 
IDecRefQueue< ParamDescrsgetParamDescrsDRQ ()
 
IDecRefQueue< ProbegetProbeDRQ ()
 
IDecRefQueue< SolvergetSolverDRQ ()
 
IDecRefQueue< StatisticsgetStatisticsDRQ ()
 
IDecRefQueue< TacticgetTacticDRQ ()
 
IDecRefQueue< FixedpointgetFixedpointDRQ ()
 
IDecRefQueue< OptimizegetOptimizeDRQ ()
 
void close ()
 

Protected Member Functions

 Context (long m_ctx)
 

Detailed Description

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

Definition at line 35 of file Context.java.

Constructor & Destructor Documentation

◆ Context() [1/3]

Context ( )
inline

Definition at line 39 of file Context.java.

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

◆ Context() [2/3]

Context ( long  m_ctx)
inlineprotected

Definition at line 46 of file Context.java.

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

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

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

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

3029 {
3030 checkContextMatch(p1);
3031 checkContextMatch(p2);
3032 return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
3033 p2.getNativeObject()));
3034 }

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

2726 {
2727 checkContextMatch(t1);
2728 checkContextMatch(t2);
2729 checkContextMatch(ts);
2730
2731 long last = 0;
2732 if (ts != null && ts.length > 0)
2733 {
2734 last = ts[ts.length - 1].getNativeObject();
2735 for (int i = ts.length - 2; i >= 0; i--) {
2736 last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2737 last);
2738 }
2739 }
2740 if (last != 0)
2741 {
2742 last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2743 return new Tactic(this, Native.tacticAndThen(nCtx(),
2744 t1.getNativeObject(), last));
2745 } else
2746 return new Tactic(this, Native.tacticAndThen(nCtx(),
2747 t1.getNativeObject(), t2.getNativeObject()));
2748 }

Referenced by Context.then().

◆ benchmarkToSMTString()

String benchmarkToSMTString ( String  name,
String  logic,
String  status,
String  attributes,
BoolExpr[]  assumptions,
BoolExpr  formula 
)
inline

Convert a benchmark into an SMT-LIB formatted string.

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

Definition at line 2599 of file Context.java.

2602 {
2603
2604 return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2605 attributes, assumptions.length,
2606 AST.arrayToNative(assumptions), formula.getNativeObject());
2607 }

◆ close()

void close ( )
inline

Disposes of the context.

Definition at line 4112 of file Context.java.

4113 {
4114 m_AST_DRQ.forceClear(this);
4115 m_ASTMap_DRQ.forceClear(this);
4116 m_ASTVector_DRQ.forceClear(this);
4117 m_ApplyResult_DRQ.forceClear(this);
4118 m_FuncEntry_DRQ.forceClear(this);
4119 m_FuncInterp_DRQ.forceClear(this);
4120 m_Goal_DRQ.forceClear(this);
4121 m_Model_DRQ.forceClear(this);
4122 m_Params_DRQ.forceClear(this);
4123 m_Probe_DRQ.forceClear(this);
4124 m_Solver_DRQ.forceClear(this);
4125 m_Optimize_DRQ.forceClear(this);
4126 m_Statistics_DRQ.forceClear(this);
4127 m_Tactic_DRQ.forceClear(this);
4128 m_Fixedpoint_DRQ.forceClear(this);
4129
4130 m_boolSort = null;
4131 m_intSort = null;
4132 m_realSort = null;
4133 m_stringSort = null;
4134
4135 synchronized (creation_lock) {
4136 Native.delContext(m_ctx);
4137 }
4138 m_ctx = 0;
4139 }

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

2807 {
2808 checkContextMatch(p);
2809 checkContextMatch(t1);
2810 checkContextMatch(t2);
2811 return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2812 t1.getNativeObject(), t2.getNativeObject()));
2813 }

◆ constProbe()

Probe constProbe ( double  val)
inline

Create a probe that always evaluates to val.

Definition at line 2958 of file Context.java.

2959 {
2960 return new Probe(this, Native.probeConst(nCtx(), val));
2961 }

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

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

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

◆ fail()

Tactic fail ( )
inline

Create a tactic always fails.

Definition at line 2837 of file Context.java.

2838 {
2839 return new Tactic(this, Native.tacticFail(nCtx()));
2840 }

◆ failIf()

Tactic failIf ( Probe  p)
inline

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

Definition at line 2846 of file Context.java.

2847 {
2848 checkContextMatch(p);
2849 return new Tactic(this,
2850 Native.tacticFailIf(nCtx(), p.getNativeObject()));
2851 }

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

2858 {
2859 return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2860 }

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

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

◆ getApplyResultDRQ()

IDecRefQueue< ApplyResult > getApplyResultDRQ ( )
inline

Definition at line 4043 of file Context.java.

4044 {
4045 return m_ApplyResult_DRQ;
4046 }

◆ getASTDRQ()

IDecRefQueue< AST > getASTDRQ ( )
inline

Definition at line 4028 of file Context.java.

4029 {
4030 return m_AST_DRQ;
4031 }

◆ getASTMapDRQ()

IDecRefQueue< ASTMap > getASTMapDRQ ( )
inline

Definition at line 4033 of file Context.java.

4034 {
4035 return m_ASTMap_DRQ;
4036 }

◆ getASTVectorDRQ()

IDecRefQueue< ASTVector > getASTVectorDRQ ( )
inline

Definition at line 4038 of file Context.java.

4039 {
4040 return m_ASTVector_DRQ;
4041 }

◆ getBoolSort()

BoolSort getBoolSort ( )
inline

Retrieves the Boolean sort of the context.

Definition at line 127 of file Context.java.

128 {
129 if (m_boolSort == null) {
130 m_boolSort = new BoolSort(this);
131 }
132 return m_boolSort;
133 }
def BoolSort(ctx=None)
Definition: z3py.py:1533

Referenced by Context.mkBoolConst().

◆ getConstructorDRQ()

IDecRefQueue< Constructor > getConstructorDRQ ( )
inline

Definition at line 4020 of file Context.java.

4020 {
4021 return m_Constructor_DRQ;
4022 }

◆ getConstructorListDRQ()

IDecRefQueue< ConstructorList > getConstructorListDRQ ( )
inline

Definition at line 4024 of file Context.java.

4024 {
4025 return m_ConstructorList_DRQ;
4026 }

◆ getFixedpointDRQ()

IDecRefQueue< Fixedpoint > getFixedpointDRQ ( )
inline

Definition at line 4098 of file Context.java.

4099 {
4100 return m_Fixedpoint_DRQ;
4101 }

◆ getFuncEntryDRQ()

IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ ( )
inline

Definition at line 4048 of file Context.java.

4049 {
4050 return m_FuncEntry_DRQ;
4051 }

◆ getFuncInterpDRQ()

IDecRefQueue< FuncInterp > getFuncInterpDRQ ( )
inline

Definition at line 4053 of file Context.java.

4054 {
4055 return m_FuncInterp_DRQ;
4056 }

◆ getGoalDRQ()

IDecRefQueue< Goal > getGoalDRQ ( )
inline

Definition at line 4058 of file Context.java.

4059 {
4060 return m_Goal_DRQ;
4061 }

◆ getIntSort()

IntSort getIntSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 138 of file Context.java.

139 {
140 if (m_intSort == null) {
141 m_intSort = new IntSort(this);
142 }
143 return m_intSort;
144 }
def IntSort(ctx=None)
Definition: z3py.py:2907

Referenced by Context.mkInt(), and Context.mkIntConst().

◆ getModelDRQ()

IDecRefQueue< Model > getModelDRQ ( )
inline

Definition at line 4063 of file Context.java.

4064 {
4065 return m_Model_DRQ;
4066 }

◆ getNumProbes()

int getNumProbes ( )
inline

The number of supported Probes.

Definition at line 2920 of file Context.java.

2921 {
2922 return Native.getNumProbes(nCtx());
2923 }

Referenced by Context.getProbeNames().

◆ getNumTactics()

int getNumTactics ( )
inline

The number of supported tactics.

Definition at line 2685 of file Context.java.

2686 {
2687 return Native.getNumTactics(nCtx());
2688 }

Referenced by Context.getTacticNames().

◆ getOptimizeDRQ()

IDecRefQueue< Optimize > getOptimizeDRQ ( )
inline

Definition at line 4103 of file Context.java.

4104 {
4105 return m_Optimize_DRQ;
4106 }

◆ getParamDescrsDRQ()

IDecRefQueue< ParamDescrs > getParamDescrsDRQ ( )
inline

Definition at line 4073 of file Context.java.

4074 {
4075 return m_ParamDescrs_DRQ;
4076 }

◆ getParamsDRQ()

IDecRefQueue< Params > getParamsDRQ ( )
inline

Definition at line 4068 of file Context.java.

4069 {
4070 return m_Params_DRQ;
4071 }

◆ getProbeDescription()

String getProbeDescription ( String  name)
inline

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

Definition at line 2942 of file Context.java.

2943 {
2944 return Native.probeGetDescr(nCtx(), name);
2945 }

◆ getProbeDRQ()

IDecRefQueue< Probe > getProbeDRQ ( )
inline

Definition at line 4078 of file Context.java.

4079 {
4080 return m_Probe_DRQ;
4081 }

◆ getProbeNames()

String[] getProbeNames ( )
inline

The names of all supported Probes.

Definition at line 2928 of file Context.java.

2929 {
2930
2931 int n = getNumProbes();
2932 String[] res = new String[n];
2933 for (int i = 0; i < n; i++)
2934 res[i] = Native.getProbeName(nCtx(), i);
2935 return res;
2936 }

◆ getRealSort()

RealSort getRealSort ( )
inline

Retrieves the Real sort of the context.

Definition at line 149 of file Context.java.

150 {
151 if (m_realSort == null) {
152 m_realSort = new RealSort(this);
153 }
154 return m_realSort;
155 }
def RealSort(ctx=None)
Definition: z3py.py:2923

Referenced by Context.mkReal(), and Context.mkRealConst().

◆ getSimplifyParameterDescriptions()

ParamDescrs getSimplifyParameterDescriptions ( )
inline

Retrieves parameter descriptions for simplifier.

Definition at line 3947 of file Context.java.

3948 {
3949 return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3950 }

◆ getSolverDRQ()

IDecRefQueue< Solver > getSolverDRQ ( )
inline

Definition at line 4083 of file Context.java.

4084 {
4085 return m_Solver_DRQ;
4086 }

◆ getStatisticsDRQ()

IDecRefQueue< Statistics > getStatisticsDRQ ( )
inline

Definition at line 4088 of file Context.java.

4089 {
4090 return m_Statistics_DRQ;
4091 }

◆ getStringSort()

SeqSort getStringSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 168 of file Context.java.

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

◆ getTacticDescription()

String getTacticDescription ( String  name)
inline

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

Definition at line 2707 of file Context.java.

2708 {
2709 return Native.tacticGetDescr(nCtx(), name);
2710 }

◆ getTacticDRQ()

IDecRefQueue< Tactic > getTacticDRQ ( )
inline

Definition at line 4093 of file Context.java.

4094 {
4095 return m_Tactic_DRQ;
4096 }

◆ getTacticNames()

String[] getTacticNames ( )
inline

The names of all supported tactics.

Definition at line 2693 of file Context.java.

2694 {
2695
2696 int n = getNumTactics();
2697 String[] res = new String[n];
2698 for (int i = 0; i < n; i++)
2699 res[i] = Native.getTacticName(nCtx(), i);
2700 return res;
2701 }

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

2980 {
2981 checkContextMatch(p1);
2982 checkContextMatch(p2);
2983 return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2984 p2.getNativeObject()));
2985 }

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

2913 {
2914 Native.interrupt(nCtx());
2915 }

◆ intToString()

SeqExpr intToString ( Expr  e)
inline

Convert an integer expression to a string.

Definition at line 1983 of file Context.java.

1984 {
1985 return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
1986 }

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

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

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

2968 {
2969 checkContextMatch(p1);
2970 checkContextMatch(p2);
2971 return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2972 p2.getNativeObject()));
2973 }

◆ mkAdd()

ArithExpr mkAdd ( ArithExpr...  t)
inline

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

Definition at line 800 of file Context.java.

801 {
802 checkContextMatch(t);
803 return (ArithExpr) Expr.create(this,
804 Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
805 }

◆ mkAnd()

BoolExpr mkAnd ( BoolExpr...  t)
inline

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

Definition at line 780 of file Context.java.

781 {
782 checkContextMatch(t);
783 return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
784 AST.arrayToNative(t)));
785 }

Referenced by Goal.AsBoolExpr().

◆ mkApp()

Expr mkApp ( FuncDecl  f,
Expr...  args 
)
inline

Create a new function application.

Definition at line 667 of file Context.java.

668 {
669 checkContextMatch(f);
670 checkContextMatch(args);
671 return Expr.create(this, f, args);
672 }

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

◆ mkArrayConst() [1/2]

ArrayExpr mkArrayConst ( String  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1664 of file Context.java.

1666 {
1667 return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1668 }
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:220
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
IntSymbol mkSymbol(int i)
Definition: Context.java:93
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431

◆ mkArrayConst() [2/2]

ArrayExpr mkArrayConst ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1655 of file Context.java.

1657 {
1658 return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1659 }

◆ mkArrayExt()

Expr mkArrayExt ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.

Definition at line 1820 of file Context.java.

1821 {
1822 checkContextMatch(arg1);
1823 checkContextMatch(arg2);
1824 return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
1825 }

◆ mkArraySort() [1/2]

ArraySort mkArraySort ( Sort  domain,
Sort  range 
)
inline

Create a new array sort.

Definition at line 220 of file Context.java.

221 {
222 checkContextMatch(domain);
223 checkContextMatch(range);
224 return new ArraySort(this, domain, range);
225 }
def ArraySort(*sig)
Definition: z3py.py:4371

Referenced by Context.mkArrayConst().

◆ mkArraySort() [2/2]

ArraySort mkArraySort ( Sort[]  domains,
Sort  range 
)
inline

Create a new array sort.

Definition at line 231 of file Context.java.

232 {
233 checkContextMatch(domains);
234 checkContextMatch(range);
235 return new ArraySort(this, domains, range);
236 }

◆ mkAt()

SeqExpr mkAt ( SeqExpr  s,
IntExpr  index 
)
inline

Retrieve sequence of length one at index.

Definition at line 2045 of file Context.java.

2046 {
2047 checkContextMatch(s, index);
2048 return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
2049 }

◆ mkAtLeast()

BoolExpr mkAtLeast ( BoolExpr[]  args,
int  k 
)
inline

Create an at-least-k constraint.

Definition at line 2216 of file Context.java.

2217 {
2218 checkContextMatch(args);
2219 return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
2220 }

◆ mkAtMost()

BoolExpr mkAtMost ( BoolExpr[]  args,
int  k 
)
inline

Create an at-most-k constraint.

Definition at line 2207 of file Context.java.

2208 {
2209 checkContextMatch(args);
2210 return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
2211 }

◆ mkBitVecSort()

BitVecSort mkBitVecSort ( int  size)
inline

Create a new bit-vector sort.

Definition at line 212 of file Context.java.

213 {
214 return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
215 }
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3740

Referenced by Context.mkBV(), and Context.mkBVConst().

◆ mkBool()

BoolExpr mkBool ( boolean  value)
inline

Creates a Boolean value.

Definition at line 693 of file Context.java.

694 {
695 return value ? mkTrue() : mkFalse();
696 }

◆ mkBoolConst() [1/2]

BoolExpr mkBoolConst ( String  name)
inline

Create a Boolean constant.

Definition at line 611 of file Context.java.

612 {
613 return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
614 }

◆ mkBoolConst() [2/2]

BoolExpr mkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 603 of file Context.java.

604 {
605 return (BoolExpr) mkConst(name, getBoolSort());
606 }

◆ mkBoolSort()

BoolSort mkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 160 of file Context.java.

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

◆ mkBound()

Expr mkBound ( int  index,
Sort  ty 
)
inline

Creates a new bound variable.

Parameters
indexThe de-Bruijn index of the variable
tyThe sort of the variable

Definition at line 537 of file Context.java.

538 {
539 return Expr.create(this,
540 Native.mkBound(nCtx(), index, ty.getNativeObject()));
541 }

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

2411 {
2412 return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2413 }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2261
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212

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

2421 {
2422 return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2423 }

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

2401 {
2402 return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2403 }

◆ mkBV2Int()

IntExpr mkBV2Int ( BitVecExpr  t,
boolean signed   
)
inline

Create an integer from the bit-vector argument t. Remarks: If is_signed is false, then the bit-vector t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in t. If is_signed is true, t1 is treated as a signed bit-vector.

NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The argument must be of bit-vector sort.

Definition at line 1535 of file Context.java.

1536 {
1537 checkContextMatch(t);
1538 return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1539 (signed)));
1540 }

◆ mkBVAdd()

BitVecExpr mkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1098 of file Context.java.

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

◆ mkBVAddNoOverflow()

BoolExpr mkBVAddNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
)
inline

Create a predicate that checks that the bit-wise addition does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1547 of file Context.java.

1549 {
1550 checkContextMatch(t1);
1551 checkContextMatch(t2);
1552 return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1553 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1554 }

◆ mkBVAddNoUnderflow()

BoolExpr mkBVAddNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Create a predicate that checks that the bit-wise addition does not underflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1561 of file Context.java.

1563 {
1564 checkContextMatch(t1);
1565 checkContextMatch(t2);
1566 return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1567 t1.getNativeObject(), t2.getNativeObject()));
1568 }

◆ mkBVAND()

BitVecExpr mkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1009 of file Context.java.

1010 {
1011 checkContextMatch(t1);
1012 checkContextMatch(t2);
1013 return new BitVecExpr(this, Native.mkBvand(nCtx(),
1014 t1.getNativeObject(), t2.getNativeObject()));
1015 }

◆ mkBVASHR()

BitVecExpr mkBVASHR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Arithmetic shift right Remarks: It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The arguments must have a bit-vector sort.

Definition at line 1443 of file Context.java.

1444 {
1445 checkContextMatch(t1);
1446 checkContextMatch(t2);
1447 return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1448 t1.getNativeObject(), t2.getNativeObject()));
1449 }

◆ mkBVConst() [1/2]

BitVecExpr mkBVConst ( String  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 659 of file Context.java.

660 {
661 return (BitVecExpr) mkConst(name, mkBitVecSort(size));
662 }

◆ mkBVConst() [2/2]

BitVecExpr mkBVConst ( Symbol  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 651 of file Context.java.

652 {
653 return (BitVecExpr) mkConst(name, mkBitVecSort(size));
654 }

◆ mkBVLSHR()

BitVecExpr mkBVLSHR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Logical shift right Remarks: It is equivalent to unsigned division by 2^x where x is the value of t2.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The arguments must have a bit-vector sort.

Definition at line 1423 of file Context.java.

1424 {
1425 checkContextMatch(t1);
1426 checkContextMatch(t2);
1427 return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1428 t1.getNativeObject(), t2.getNativeObject()));
1429 }

◆ mkBVMul()

BitVecExpr mkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1124 of file Context.java.

1125 {
1126 checkContextMatch(t1);
1127 checkContextMatch(t2);
1128 return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1129 t1.getNativeObject(), t2.getNativeObject()));
1130 }

◆ mkBVMulNoOverflow()

BoolExpr mkBVMulNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
)
inline

Create a predicate that checks that the bit-wise multiplication does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1629 of file Context.java.

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

◆ mkBVMulNoUnderflow()

BoolExpr mkBVMulNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Create a predicate that checks that the bit-wise multiplication does not underflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1643 of file Context.java.

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

◆ mkBVNAND()

BitVecExpr mkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1048 of file Context.java.

1049 {
1050 checkContextMatch(t1);
1051 checkContextMatch(t2);
1052 return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1053 t1.getNativeObject(), t2.getNativeObject()));
1054 }

◆ mkBVNeg()

BitVecExpr mkBVNeg ( BitVecExpr  t)
inline

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

Definition at line 1087 of file Context.java.

1088 {
1089 checkContextMatch(t);
1090 return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1091 }

◆ mkBVNegNoOverflow()

BoolExpr mkBVNegNoOverflow ( BitVecExpr  t)
inline

Create a predicate that checks that the bit-wise negation does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1617 of file Context.java.

1618 {
1619 checkContextMatch(t);
1620 return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1621 t.getNativeObject()));
1622 }

◆ mkBVNOR()

BitVecExpr mkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1061 of file Context.java.

1062 {
1063 checkContextMatch(t1);
1064 checkContextMatch(t2);
1065 return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1066 t1.getNativeObject(), t2.getNativeObject()));
1067 }

◆ mkBVNot()

BitVecExpr mkBVNot ( BitVecExpr  t)
inline

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

Definition at line 974 of file Context.java.

975 {
976 checkContextMatch(t);
977 return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
978 }

◆ mkBVOR()

BitVecExpr mkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1022 of file Context.java.

1023 {
1024 checkContextMatch(t1);
1025 checkContextMatch(t2);
1026 return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1027 t2.getNativeObject()));
1028 }

◆ mkBVRedAND()

BitVecExpr mkBVRedAND ( BitVecExpr  t)
inline

Take conjunction of bits in a vector, return vector of length 1.

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

Definition at line 985 of file Context.java.

986 {
987 checkContextMatch(t);
988 return new BitVecExpr(this, Native.mkBvredand(nCtx(),
989 t.getNativeObject()));
990 }

◆ mkBVRedOR()

BitVecExpr mkBVRedOR ( BitVecExpr  t)
inline

Take disjunction of bits in a vector, return vector of length 1.

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

Definition at line 997 of file Context.java.

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

◆ mkBVRotateLeft() [1/2]

BitVecExpr mkBVRotateLeft ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Rotate Left. Remarks: Rotate bits of t1 to the left t2 times. The arguments must have the same bit-vector sort.

Definition at line 1481 of file Context.java.

1483 {
1484 checkContextMatch(t1);
1485 checkContextMatch(t2);
1486 return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1487 t1.getNativeObject(), t2.getNativeObject()));
1488 }

◆ mkBVRotateLeft() [2/2]

BitVecExpr mkBVRotateLeft ( int  i,
BitVecExpr  t 
)
inline

Rotate Left. Remarks: Rotate bits of t to the left i times. The argument t must have a bit-vector sort.

Definition at line 1456 of file Context.java.

1457 {
1458 checkContextMatch(t);
1459 return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1460 t.getNativeObject()));
1461 }

◆ mkBVRotateRight() [1/2]

BitVecExpr mkBVRotateRight ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1496 of file Context.java.

1498 {
1499 checkContextMatch(t1);
1500 checkContextMatch(t2);
1501 return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1502 t1.getNativeObject(), t2.getNativeObject()));
1503 }

◆ mkBVRotateRight() [2/2]

BitVecExpr mkBVRotateRight ( int  i,
BitVecExpr  t 
)
inline

Rotate Right. Remarks: Rotate bits of t to the right i times. The argument t must have a bit-vector sort.

Definition at line 1468 of file Context.java.

1469 {
1470 checkContextMatch(t);
1471 return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1472 t.getNativeObject()));
1473 }

◆ mkBVSDiv()

BitVecExpr mkBVSDiv ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

  • The floor of t1/t2 if t2 is different from zero, and t1*t2 >= 0.
  • The ceiling of t1/t2 if t2 is different from zero, and t1*t2 &lt; 0.

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

Definition at line 1160 of file Context.java.

1161 {
1162 checkContextMatch(t1);
1163 checkContextMatch(t2);
1164 return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1165 t1.getNativeObject(), t2.getNativeObject()));
1166 }

◆ mkBVSDivNoOverflow()

BoolExpr mkBVSDivNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Create a predicate that checks that the bit-wise signed division does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1603 of file Context.java.

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

◆ mkBVSGE()

BoolExpr mkBVSGE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1285 of file Context.java.

1286 {
1287 checkContextMatch(t1);
1288 checkContextMatch(t2);
1289 return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1290 t2.getNativeObject()));
1291 }

◆ mkBVSGT()

BoolExpr mkBVSGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1311 of file Context.java.

1312 {
1313 checkContextMatch(t1);
1314 checkContextMatch(t2);
1315 return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1316 t2.getNativeObject()));
1317 }

◆ mkBVSHL()

BitVecExpr mkBVSHL ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Shift left. Remarks: It is equivalent to multiplication by 2^x where x is the value of t2.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The arguments must have a bit-vector sort.

Definition at line 1404 of file Context.java.

1405 {
1406 checkContextMatch(t1);
1407 checkContextMatch(t2);
1408 return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1409 t1.getNativeObject(), t2.getNativeObject()));
1410 }

◆ mkBVSLE()

BoolExpr mkBVSLE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1259 of file Context.java.

1260 {
1261 checkContextMatch(t1);
1262 checkContextMatch(t2);
1263 return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1264 t2.getNativeObject()));
1265 }

◆ mkBVSLT()

BoolExpr mkBVSLT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1233 of file Context.java.

1234 {
1235 checkContextMatch(t1);
1236 checkContextMatch(t2);
1237 return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1238 t2.getNativeObject()));
1239 }

◆ mkBVSMod()

BitVecExpr mkBVSMod ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed remainder (sign follows divisor). Remarks: If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1207 of file Context.java.

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

◆ mkBVSRem()

BitVecExpr mkBVSRem ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Signed remainder. Remarks: It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1.

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

Definition at line 1193 of file Context.java.

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

◆ mkBVSub()

BitVecExpr mkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1111 of file Context.java.

1112 {
1113 checkContextMatch(t1);
1114 checkContextMatch(t2);
1115 return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1116 t1.getNativeObject(), t2.getNativeObject()));
1117 }

◆ mkBVSubNoOverflow()

BoolExpr mkBVSubNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Create a predicate that checks that the bit-wise subtraction does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1575 of file Context.java.

1577 {
1578 checkContextMatch(t1);
1579 checkContextMatch(t2);
1580 return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1581 t1.getNativeObject(), t2.getNativeObject()));
1582 }

◆ mkBVSubNoUnderflow()

BoolExpr mkBVSubNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
)
inline

Create a predicate that checks that the bit-wise subtraction does not underflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1589 of file Context.java.

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

◆ mkBVUDiv()

BitVecExpr mkBVUDiv ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned division. Remarks: It is defined as the floor of t1/t2 if t2 is different from zero. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1139 of file Context.java.

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

◆ mkBVUGE()

BoolExpr mkBVUGE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1272 of file Context.java.

1273 {
1274 checkContextMatch(t1);
1275 checkContextMatch(t2);
1276 return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1277 t2.getNativeObject()));
1278 }

◆ mkBVUGT()

BoolExpr mkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1298 of file Context.java.

1299 {
1300 checkContextMatch(t1);
1301 checkContextMatch(t2);
1302 return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1303 t2.getNativeObject()));
1304 }

◆ mkBVULE()

BoolExpr mkBVULE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1246 of file Context.java.

1247 {
1248 checkContextMatch(t1);
1249 checkContextMatch(t2);
1250 return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1251 t2.getNativeObject()));
1252 }

◆ mkBVULT()

BoolExpr mkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1220 of file Context.java.

1221 {
1222 checkContextMatch(t1);
1223 checkContextMatch(t2);
1224 return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1225 t2.getNativeObject()));
1226 }

◆ mkBVURem()

BitVecExpr mkBVURem ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned remainder. Remarks: It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1175 of file Context.java.

1176 {
1177 checkContextMatch(t1);
1178 checkContextMatch(t2);
1179 return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1180 t1.getNativeObject(), t2.getNativeObject()));
1181 }

◆ mkBVXNOR()

BitVecExpr mkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1074 of file Context.java.

1075 {
1076 checkContextMatch(t1);
1077 checkContextMatch(t2);
1078 return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1079 t1.getNativeObject(), t2.getNativeObject()));
1080 }

◆ mkBVXOR()

BitVecExpr mkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1035 of file Context.java.

1036 {
1037 checkContextMatch(t1);
1038 checkContextMatch(t2);
1039 return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1040 t1.getNativeObject(), t2.getNativeObject()));
1041 }

◆ mkComplement()

ReExpr mkComplement ( ReExpr  re)
inline

Create the complement regular expression.

Definition at line 2145 of file Context.java.

2146 {
2147 checkContextMatch(re);
2148 return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
2149 }

◆ mkConcat() [1/3]

BitVecExpr mkConcat ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bit-vector concatenation. Remarks: The arguments must have a bit-vector sort.

Returns
The result is a bit-vector of size n1+n2, where n1 (n2) is the size of t1 (t2).

Definition at line 1329 of file Context.java.

1330 {
1331 checkContextMatch(t1);
1332 checkContextMatch(t2);
1333 return new BitVecExpr(this, Native.mkConcat(nCtx(),
1334 t1.getNativeObject(), t2.getNativeObject()));
1335 }

◆ mkConcat() [2/3]

ReExpr mkConcat ( ReExpr...  t)
inline

Create the concatenation of regular languages.

Definition at line 2154 of file Context.java.

2155 {
2156 checkContextMatch(t);
2157 return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2158 }

◆ mkConcat() [3/3]

SeqExpr mkConcat ( SeqExpr...  t)
inline

Concatenate sequences.

Definition at line 1999 of file Context.java.

2000 {
2001 checkContextMatch(t);
2002 return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
2003 }

◆ mkConst() [1/3]

Expr mkConst ( FuncDecl  f)
inline

Creates a fresh constant from the FuncDecl f.

Parameters
fA decl of a 0-arity function

Definition at line 595 of file Context.java.

596 {
597 return mkApp(f, (Expr[]) null);
598 }
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:667

◆ mkConst() [2/3]

Expr mkConst ( String  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name.

Definition at line 575 of file Context.java.

576 {
577 return mkConst(mkSymbol(name), range);
578 }

◆ mkConst() [3/3]

Expr mkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name.

Definition at line 560 of file Context.java.

561 {
562 checkContextMatch(name);
563 checkContextMatch(range);
564
565 return Expr.create(
566 this,
567 Native.mkConst(nCtx(), name.getNativeObject(),
568 range.getNativeObject()));
569 }

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

◆ mkConstArray()

ArrayExpr mkConstArray ( Sort  domain,
Expr  v 
)
inline

Create a constant array. Remarks: The resulting term is an array, such that a select on an arbitrary index produces the value v.

See also
mkArraySort
mkSelect

Definition at line 1774 of file Context.java.

1775 {
1776 checkContextMatch(domain);
1777 checkContextMatch(v);
1778 return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1779 domain.getNativeObject(), v.getNativeObject()));
1780 }

◆ mkConstDecl() [1/2]

FuncDecl mkConstDecl ( String  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 513 of file Context.java.

514 {
515 checkContextMatch(range);
516 return new FuncDecl(this, mkSymbol(name), null, range);
517 }

◆ mkConstDecl() [2/2]

FuncDecl mkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 503 of file Context.java.

504 {
505 checkContextMatch(name);
506 checkContextMatch(range);
507 return new FuncDecl(this, name, null, range);
508 }

◆ mkConstructor() [1/2]

Constructor mkConstructor ( String  name,
String  recognizer,
String[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
)
inline

Create a datatype constructor.

Definition at line 356 of file Context.java.

358 {
359 return of(this, mkSymbol(name), mkSymbol(recognizer),
360 mkSymbols(fieldNames), sorts, sortRefs);
361 }

◆ mkConstructor() [2/2]

Constructor mkConstructor ( Symbol  name,
Symbol  recognizer,
Symbol[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
)
inline

Create a datatype constructor.

Parameters
nameconstructor name
recognizername of recognizer function.
fieldNamesnames of the constructor fields.
sortsfield sorts, 0 if the field sort refers to a recursive sort.
sortRefsreference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared.

Definition at line 345 of file Context.java.

348 {
349 return of(this, name, recognizer, fieldNames, sorts,
350 sortRefs);
351 }

◆ mkContains()

BoolExpr mkContains ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence containment of s2 in s1.

Definition at line 2036 of file Context.java.

2037 {
2038 checkContextMatch(s1, s2);
2039 return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2040 }

◆ mkDatatypeSort() [1/2]

DatatypeSort mkDatatypeSort ( String  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 377 of file Context.java.

379 {
380 checkContextMatch(constructors);
381 return new DatatypeSort(this, mkSymbol(name), constructors);
382 }

◆ mkDatatypeSort() [2/2]

DatatypeSort mkDatatypeSort ( Symbol  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 366 of file Context.java.

368 {
369 checkContextMatch(name);
370 checkContextMatch(constructors);
371 return new DatatypeSort(this, name, constructors);
372 }

◆ mkDatatypeSorts() [1/2]

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

Create mutually recursive data-types.

Definition at line 416 of file Context.java.

418 {
419 return mkDatatypeSorts(mkSymbols(names), c);
420 }
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:389

◆ mkDatatypeSorts() [2/2]

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

Create mutually recursive datatypes.

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

Definition at line 389 of file Context.java.

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

Referenced by Context.mkDatatypeSorts().

◆ mkDistinct()

BoolExpr mkDistinct ( Expr...  args)
inline

Creates a distinct term.

Definition at line 712 of file Context.java.

713 {
714 checkContextMatch(args);
715 return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
716 AST.arrayToNative(args)));
717 }

◆ mkDiv()

ArithExpr mkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 / t2.

Definition at line 840 of file Context.java.

841 {
842 checkContextMatch(t1);
843 checkContextMatch(t2);
844 return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
845 t1.getNativeObject(), t2.getNativeObject()));
846 }

◆ mkEmptyRe()

ReExpr mkEmptyRe ( Sort  s)
inline

Create the empty regular expression.

Definition at line 2181 of file Context.java.

2182 {
2183 return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
2184 }

◆ mkEmptySeq()

SeqExpr mkEmptySeq ( Sort  s)
inline

Sequences, Strings and regular expressions. Create the empty sequence.

Definition at line 1957 of file Context.java.

1958 {
1959 checkContextMatch(s);
1960 return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
1961 }

◆ mkEmptySet()

ArrayExpr mkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 1840 of file Context.java.

1841 {
1842 checkContextMatch(domain);
1843 return (ArrayExpr)Expr.create(this,
1844 Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1845 }

◆ mkEnumSort() [1/2]

EnumSort mkEnumSort ( String  name,
String...  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 290 of file Context.java.

292 {
293 return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
294 }
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4994

◆ mkEnumSort() [2/2]

EnumSort mkEnumSort ( Symbol  name,
Symbol...  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 279 of file Context.java.

281 {
282 checkContextMatch(name);
283 checkContextMatch(enumNames);
284 return new EnumSort(this, name, enumNames);
285 }

◆ mkEq()

BoolExpr mkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality x = y

Definition at line 701 of file Context.java.

702 {
703 checkContextMatch(x);
704 checkContextMatch(y);
705 return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
706 y.getNativeObject()));
707 }

◆ mkExists() [1/2]

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

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

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

Definition at line 2489 of file Context.java.

2492 {
2493
2494 return Quantifier.of(this, false, boundConstants, body, weight,
2495 patterns, noPatterns, quantifierID, skolemID);
2496 }

◆ mkExists() [2/2]

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

Creates an existential quantifier using de-Bruijn indexed variables.

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

Definition at line 2476 of file Context.java.

2479 {
2480
2481 return Quantifier.of(this, false, sorts, names, body, weight,
2482 patterns, noPatterns, quantifierID, skolemID);
2483 }

Referenced by Context.mkQuantifier().

◆ mkExtract() [1/2]

BitVecExpr mkExtract ( int  high,
int  low,
BitVecExpr  t 
)
inline

Bit-vector extraction. Remarks: Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1. The argument t must have a bit-vector sort.

Definition at line 1345 of file Context.java.

1347 {
1348 checkContextMatch(t);
1349 return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1350 t.getNativeObject()));
1351 }

◆ mkExtract() [2/2]

SeqExpr mkExtract ( SeqExpr  s,
IntExpr  offset,
IntExpr  length 
)
inline

Extract subsequence.

Definition at line 2054 of file Context.java.

2055 {
2056 checkContextMatch(s, offset, length);
2057 return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
2058 }

◆ mkFalse()

BoolExpr mkFalse ( )
inline

The false Term.

Definition at line 685 of file Context.java.

686 {
687 return new BoolExpr(this, Native.mkFalse(nCtx()));
688 }

Referenced by Context.mkBool().

◆ mkFiniteDomainSort() [1/2]

FiniteDomainSort mkFiniteDomainSort ( String  name,
long  size 
)
inline

Create a new finite domain sort.

Definition at line 328 of file Context.java.

330 {
331 return new FiniteDomainSort(this, mkSymbol(name), size);
332 }
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7221

◆ mkFiniteDomainSort() [2/2]

FiniteDomainSort mkFiniteDomainSort ( Symbol  name,
long  size 
)
inline

Create a new finite domain sort.

Definition at line 318 of file Context.java.

320 {
321 checkContextMatch(name);
322 return new FiniteDomainSort(this, name, size);
323 }

◆ mkFixedpoint()

Fixedpoint mkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3118 of file Context.java.

3119 {
3120 return new Fixedpoint(this);
3121 }

◆ mkForall() [1/2]

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

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

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

Definition at line 2463 of file Context.java.

2466 {
2467
2468 return Quantifier.of(this, true, boundConstants, body, weight,
2469 patterns, noPatterns, quantifierID, skolemID);
2470 }

◆ mkForall() [2/2]

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

Create a universal Quantifier.

Parameters
sortsthe sorts of the bound variables.
namesnames of the bound variables
bodythe body of the quantifier.
weightquantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
patternsarray containing the patterns created using MkPattern.
noPatternsarray containing the anti-patterns created using MkPattern.
quantifierIDoptional symbol to track quantifier.
skolemIDoptional symbol to track skolem constants.
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 2450 of file Context.java.

2453 {
2454
2455 return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2456 noPatterns, quantifierID, skolemID);
2457 }

Referenced by Context.mkQuantifier().

◆ mkFP() [1/6]

FPExpr mkFP ( BitVecExpr  sgn,
BitVecExpr  sig,
BitVecExpr  exp 
)
inline

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

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

Definition at line 3746 of file Context.java.

3747 {
3748 return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3749 }

◆ mkFP() [2/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 3448 of file Context.java.

3449 {
3450 return mkFPNumeral(sgn, exp, sig, s);
3451 }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3353

◆ mkFP() [3/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 3461 of file Context.java.

3462 {
3463 return mkFPNumeral(sgn, exp, sig, s);
3464 }

◆ mkFP() [4/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 3423 of file Context.java.

3424 {
3425 return mkFPNumeral(v, s);
3426 }

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

3413 {
3414 return mkFPNumeral(v, s);
3415 }

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

3436 {
3437 return mkFPNumeral(v, s);
3438 }

◆ mkFPAbs()

FPExpr mkFPAbs ( FPExpr  t)
inline

Floating-point absolute value

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3472 of file Context.java.

3473 {
3474 return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3475 }

◆ mkFPAdd()

FPExpr mkFPAdd ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point addition

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

Definition at line 3494 of file Context.java.

3495 {
3496 return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3497 }

◆ mkFPDiv()

FPExpr mkFPDiv ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point division

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

Definition at line 3530 of file Context.java.

3531 {
3532 return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3533 }

◆ mkFPEq()

BoolExpr mkFPEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point equality.

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

Definition at line 3658 of file Context.java.

3659 {
3660 return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3661 }

◆ mkFPFMA()

FPExpr mkFPFMA ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2,
FPExpr  t3 
)
inline

Floating-point fused multiply-add

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

Definition at line 3545 of file Context.java.

3546 {
3547 return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3548 }

◆ mkFPGEq()

BoolExpr mkFPGEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3634 of file Context.java.

3635 {
3636 return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3637 }

◆ mkFPGt()

BoolExpr mkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3645 of file Context.java.

3646 {
3647 return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3648 }

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

3332 {
3333 return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3334 }

◆ mkFPIsInfinite()

BoolExpr mkFPIsInfinite ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3698 of file Context.java.

3699 {
3700 return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3701 }

◆ mkFPIsNaN()

BoolExpr mkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3708 of file Context.java.

3709 {
3710 return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3711 }

◆ mkFPIsNegative()

BoolExpr mkFPIsNegative ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3718 of file Context.java.

3719 {
3720 return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3721 }

◆ mkFPIsNormal()

BoolExpr mkFPIsNormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3668 of file Context.java.

3669 {
3670 return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3671 }

◆ mkFPIsPositive()

BoolExpr mkFPIsPositive ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3728 of file Context.java.

3729 {
3730 return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3731 }

◆ mkFPIsSubnormal()

BoolExpr mkFPIsSubnormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3678 of file Context.java.

3679 {
3680 return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3681 }

◆ mkFPIsZero()

BoolExpr mkFPIsZero ( FPExpr  t)
inline

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

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3688 of file Context.java.

3689 {
3690 return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3691 }

◆ mkFPLEq()

BoolExpr mkFPLEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3612 of file Context.java.

3613 {
3614 return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3615 }

◆ mkFPLt()

BoolExpr mkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3623 of file Context.java.

3624 {
3625 return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3626 }

◆ mkFPMax()

FPExpr mkFPMax ( FPExpr  t1,
FPExpr  t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3601 of file Context.java.

3602 {
3603 return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3604 }

◆ mkFPMin()

FPExpr mkFPMin ( FPExpr  t1,
FPExpr  t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3590 of file Context.java.

3591 {
3592 return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3593 }

◆ mkFPMul()

FPExpr mkFPMul ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point multiplication

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

Definition at line 3518 of file Context.java.

3519 {
3520 return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3521 }

◆ mkFPNaN()

FPNum mkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3320 of file Context.java.

3321 {
3322 return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3323 }

◆ mkFPNeg()

FPExpr mkFPNeg ( FPExpr  t)
inline

Floating-point negation

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3482 of file Context.java.

3483 {
3484 return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3485 }

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

3389 {
3390 return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3391 }

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

3402 {
3403 return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3404 }

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

3365 {
3366 return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3367 }

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

3354 {
3355 return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3356 }

Referenced by Context.mkFP().

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

3376 {
3377 return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3378 }

◆ mkFPRem()

FPExpr mkFPRem ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3567 of file Context.java.

3568 {
3569 return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3570 }

◆ mkFPRNA()

FPRMNum mkFPRNA ( )
inline

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

Exceptions
Z3Exception

Definition at line 3172 of file Context.java.

3173 {
3174 return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3175 }

◆ mkFPRNE()

FPRMNum mkFPRNE ( )
inline

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

Exceptions
Z3Exception

Definition at line 3154 of file Context.java.

3155 {
3156 return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3157 }

◆ mkFPRoundingModeSort()

FPRMSort mkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Exceptions
Z3Exception

Definition at line 3136 of file Context.java.

3137 {
3138 return new FPRMSort(this);
3139 }

◆ mkFPRoundNearestTiesToAway()

FPRMNum mkFPRoundNearestTiesToAway ( )
inline

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

Exceptions
Z3Exception

Definition at line 3163 of file Context.java.

3164 {
3165 return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3166 }

◆ mkFPRoundNearestTiesToEven()

FPRMExpr mkFPRoundNearestTiesToEven ( )
inline

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

Exceptions
Z3Exception

Definition at line 3145 of file Context.java.

3146 {
3147 return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3148 }

◆ mkFPRoundToIntegral()

FPExpr mkFPRoundToIntegral ( FPRMExpr  rm,
FPExpr  t 
)
inline

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

Parameters
rmterm of RoundingMode sort
tfloating-point term
Exceptions
Z3Exception

Definition at line 3579 of file Context.java.

3580 {
3581 return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3582 }

◆ mkFPRoundTowardNegative()

FPRMNum mkFPRoundTowardNegative ( )
inline

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

Exceptions
Z3Exception

Definition at line 3199 of file Context.java.

3200 {
3201 return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3202 }

◆ mkFPRoundTowardPositive()

FPRMNum mkFPRoundTowardPositive ( )
inline

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

Exceptions
Z3Exception

Definition at line 3181 of file Context.java.

3182 {
3183 return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3184 }

◆ mkFPRoundTowardZero()

FPRMNum mkFPRoundTowardZero ( )
inline

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

Exceptions
Z3Exception

Definition at line 3217 of file Context.java.

3218 {
3219 return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3220 }

◆ mkFPRTN()

FPRMNum mkFPRTN ( )
inline

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

Exceptions
Z3Exception

Definition at line 3208 of file Context.java.

3209 {
3210 return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3211 }

◆ mkFPRTP()

FPRMNum mkFPRTP ( )
inline

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

Exceptions
Z3Exception

Definition at line 3190 of file Context.java.

3191 {
3192 return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3193 }

◆ mkFPRTZ()

FPRMNum mkFPRTZ ( )
inline

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

Exceptions
Z3Exception

Definition at line 3226 of file Context.java.

3227 {
3228 return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3229 }

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

3238 {
3239 return new FPSort(this, ebits, sbits);
3240 }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9183

◆ mkFPSort128()

FPSort mkFPSort128 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3309 of file Context.java.

3310 {
3311 return new FPSort(this, Native.mkFpaSort128(nCtx()));
3312 }

◆ mkFPSort16()

FPSort mkFPSort16 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3255 of file Context.java.

3256 {
3257 return new FPSort(this, Native.mkFpaSort16(nCtx()));
3258 }

◆ mkFPSort32()

FPSort mkFPSort32 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3273 of file Context.java.

3274 {
3275 return new FPSort(this, Native.mkFpaSort32(nCtx()));
3276 }

◆ mkFPSort64()

FPSort mkFPSort64 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3291 of file Context.java.

3292 {
3293 return new FPSort(this, Native.mkFpaSort64(nCtx()));
3294 }

◆ mkFPSortDouble()

FPSort mkFPSortDouble ( )
inline

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

Exceptions
Z3Exception

Definition at line 3282 of file Context.java.

3283 {
3284 return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3285 }

◆ mkFPSortHalf()

FPSort mkFPSortHalf ( )
inline

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

Exceptions
Z3Exception

Definition at line 3246 of file Context.java.

3247 {
3248 return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3249 }

◆ mkFPSortQuadruple()

FPSort mkFPSortQuadruple ( )
inline

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

Exceptions
Z3Exception

Definition at line 3300 of file Context.java.

3301 {
3302 return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3303 }

◆ mkFPSortSingle()

FPSort mkFPSortSingle ( )
inline

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

Exceptions
Z3Exception

Definition at line 3264 of file Context.java.

3265 {
3266 return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3267 }

◆ mkFPSqrt()

FPExpr mkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term
Exceptions
Z3Exception

Definition at line 3556 of file Context.java.

3557 {
3558 return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3559 }

◆ mkFPSub()

FPExpr mkFPSub ( FPRMExpr  rm,
FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point subtraction

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

Definition at line 3506 of file Context.java.

3507 {
3508 return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3509 }

◆ mkFPToBV()

BitVecExpr mkFPToBV ( FPRMExpr  rm,
FPExpr  t,
int  sz,
boolean signed   
)
inline

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

Parameters
rmRoundingMode term.
tFloatingPoint term
szSize of the resulting bit-vector.
signedIndicates whether the result is a signed or unsigned bit-vector. Remarks: Produces a term that represents the conversion of the floating-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 3847 of file Context.java.

3848 {
3849 if (signed)
3850 return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3851 else
3852 return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3853 }

◆ mkFPToFP() [1/6]

FPExpr mkFPToFP ( BitVecExpr  bv,
FPSort  s 
)
inline

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

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

Definition at line 3762 of file Context.java.

3763 {
3764 return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3765 }

◆ mkFPToFP() [2/6]

FPExpr mkFPToFP ( FPRMExpr  rm,
BitVecExpr  t,
FPSort  s,
boolean signed   
)
inline

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

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

Definition at line 3812 of file Context.java.

3813 {
3814 if (signed)
3815 return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3816 else
3817 return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3818 }

◆ mkFPToFP() [3/6]

FPExpr mkFPToFP ( FPRMExpr  rm,
FPExpr  t,
FPSort  s 
)
inline

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

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

Definition at line 3778 of file Context.java.

3779 {
3780 return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3781 }

◆ mkFPToFP() [4/6]

BitVecExpr mkFPToFP ( FPRMExpr  rm,
IntExpr  exp,
RealExpr  sig,
FPSort  s 
)
inline

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

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

Definition at line 3897 of file Context.java.

3898 {
3899 return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3900 }

◆ mkFPToFP() [5/6]

FPExpr mkFPToFP ( FPRMExpr  rm,
RealExpr  t,
FPSort  s 
)
inline

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

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

Definition at line 3794 of file Context.java.

3795 {
3796 return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3797 }

◆ mkFPToFP() [6/6]

FPExpr mkFPToFP ( FPSort  s,
FPRMExpr  rm,
FPExpr  t 
)
inline

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

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

Definition at line 3830 of file Context.java.

3831 {
3832 return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3833 }

◆ mkFPToIEEEBV()

BitVecExpr mkFPToIEEEBV ( FPExpr  t)
inline

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

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

Definition at line 3879 of file Context.java.

3880 {
3881 return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3882 }

◆ mkFPToReal()

RealExpr mkFPToReal ( FPExpr  t)
inline

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

Parameters
tFloatingPoint term Remarks: Produces a term that represents the conversion of the floating-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 3864 of file Context.java.

3865 {
3866 return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3867 }

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

3343 {
3344 return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3345 }

◆ mkFreshConst()

Expr mkFreshConst ( String  prefix,
Sort  range 
)
inline

Creates a fresh Constant of sort range and a name prefixed with prefix.

Definition at line 584 of file Context.java.

585 {
586 checkContextMatch(range);
587 return Expr.create(this,
588 Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
589 }

◆ mkFreshConstDecl()

FuncDecl mkFreshConstDecl ( String  prefix,
Sort  range 
)
inline

Creates a fresh constant function declaration with a name prefixed with prefix.

See also
mkFuncDecl(String,Sort,Sort)
mkFuncDecl(String,Sort[],Sort)

Definition at line 525 of file Context.java.

527 {
528 checkContextMatch(range);
529 return new FuncDecl(this, prefix, null, range);
530 }

◆ mkFreshFuncDecl()

FuncDecl mkFreshFuncDecl ( String  prefix,
Sort[]  domain,
Sort  range 
)
inline

Creates a fresh function declaration with a name prefixed with prefix.

See also
mkFuncDecl(String,Sort,Sort)
mkFuncDecl(String,Sort[],Sort)

Definition at line 492 of file Context.java.

494 {
495 checkContextMatch(domain);
496 checkContextMatch(range);
497 return new FuncDecl(this, prefix, domain, range);
498 }

◆ mkFullRe()

ReExpr mkFullRe ( Sort  s)
inline

Create the full regular expression.

Definition at line 2189 of file Context.java.

2190 {
2191 return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
2192 }

◆ mkFullSet()

ArrayExpr mkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 1850 of file Context.java.

1851 {
1852 checkContextMatch(domain);
1853 return (ArrayExpr)Expr.create(this,
1854 Native.mkFullSet(nCtx(), domain.getNativeObject()));
1855 }

◆ mkFuncDecl() [1/4]

FuncDecl mkFuncDecl ( String  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 477 of file Context.java.

479 {
480 checkContextMatch(domain);
481 checkContextMatch(range);
482 Sort[] q = new Sort[] { domain };
483 return new FuncDecl(this, mkSymbol(name), q, range);
484 }

◆ mkFuncDecl() [2/4]

FuncDecl mkFuncDecl ( String  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 466 of file Context.java.

468 {
469 checkContextMatch(domain);
470 checkContextMatch(range);
471 return new FuncDecl(this, mkSymbol(name), domain, range);
472 }

◆ mkFuncDecl() [3/4]

FuncDecl mkFuncDecl ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 453 of file Context.java.

455 {
456 checkContextMatch(name);
457 checkContextMatch(domain);
458 checkContextMatch(range);
459 Sort[] q = new Sort[] { domain };
460 return new FuncDecl(this, name, q, range);
461 }

◆ mkFuncDecl() [4/4]

FuncDecl mkFuncDecl ( Symbol  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 441 of file Context.java.

443 {
444 checkContextMatch(name);
445 checkContextMatch(domain);
446 checkContextMatch(range);
447 return new FuncDecl(this, name, domain, range);
448 }

◆ mkGe()

BoolExpr mkGe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 &gt;= t2

Definition at line 923 of file Context.java.

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

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

2670 {
2671 return new Goal(this, models, unsatCores, proofs);
2672 }

◆ mkGt()

BoolExpr mkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 &gt; t2

Definition at line 912 of file Context.java.

913 {
914 checkContextMatch(t1);
915 checkContextMatch(t2);
916 return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
917 t2.getNativeObject()));
918 }

◆ mkIff()

BoolExpr mkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 iff t2.

Definition at line 747 of file Context.java.

748 {
749 checkContextMatch(t1);
750 checkContextMatch(t2);
751 return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
752 t2.getNativeObject()));
753 }

◆ mkImplies()

BoolExpr mkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 -> t2.

Definition at line 758 of file Context.java.

759 {
760 checkContextMatch(t1);
761 checkContextMatch(t2);
762 return new BoolExpr(this, Native.mkImplies(nCtx(),
763 t1.getNativeObject(), t2.getNativeObject()));
764 }

◆ mkIndexOf()

IntExpr mkIndexOf ( SeqExpr  s,
SeqExpr  substr,
ArithExpr  offset 
)
inline

Extract index of sub-string starting at offset.

Definition at line 2063 of file Context.java.

2064 {
2065 checkContextMatch(s, substr, offset);
2066 return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
2067 }

◆ mkInRe()

BoolExpr mkInRe ( SeqExpr  s,
ReExpr  re 
)
inline

Check for regular expression membership.

Definition at line 2091 of file Context.java.

2092 {
2093 checkContextMatch(s, re);
2094 return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
2095 }

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

2376 {
2377
2378 return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2379 .getNativeObject()));
2380 }

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

2389 {
2390
2391 return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2392 .getNativeObject()));
2393 }

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

2363 {
2364
2365 return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2366 .getNativeObject()));
2367 }

◆ mkInt2BV()

BitVecExpr mkInt2BV ( int  n,
IntExpr  t 
)
inline

Create an n bit bit-vector from the integer argument t. Remarks: NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The argument must be of integer sort.

Definition at line 1514 of file Context.java.

1515 {
1516 checkContextMatch(t);
1517 return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1518 t.getNativeObject()));
1519 }

◆ mkInt2Real()

RealExpr mkInt2Real ( IntExpr  t)
inline

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

You can take the floor of a real by creating an auxiliary integer Term k and asserting MakeInt2Real(k) &lt;= t1 &lt; MkInt2Real(k)+1. The argument must be of integer sort.

Definition at line 941 of file Context.java.

942 {
943 checkContextMatch(t);
944 return new RealExpr(this,
945 Native.mkInt2real(nCtx(), t.getNativeObject()));
946 }

◆ mkIntConst() [1/2]

IntExpr mkIntConst ( String  name)
inline

Creates an integer constant.

Definition at line 627 of file Context.java.

628 {
629 return (IntExpr) mkConst(name, getIntSort());
630 }

◆ mkIntConst() [2/2]

IntExpr mkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 619 of file Context.java.

620 {
621 return (IntExpr) mkConst(name, getIntSort());
622 }

◆ mkIntersect()

ReExpr mkIntersect ( ReExpr...  t)
inline

Create the intersection of regular languages.

Definition at line 2172 of file Context.java.

2173 {
2174 checkContextMatch(t);
2175 return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
2176 }

◆ mkIntSort()

IntSort mkIntSort ( )
inline

Create a new integer sort.

Definition at line 196 of file Context.java.

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

◆ mkIsInteger()

BoolExpr mkIsInteger ( RealExpr  t)
inline

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

Definition at line 963 of file Context.java.

964 {
965 checkContextMatch(t);
966 return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
967 }

◆ mkITE()

Expr mkITE ( BoolExpr  t1,
Expr  t2,
Expr  t3 
)
inline

Create an expression representing an if-then-else: ite(t1, t2, t3).

Parameters
t1An expression with Boolean sort
t2An expression
t3An expression with the same sort as t2

Definition at line 735 of file Context.java.

736 {
737 checkContextMatch(t1);
738 checkContextMatch(t2);
739 checkContextMatch(t3);
740 return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
741 t2.getNativeObject(), t3.getNativeObject()));
742 }

◆ mkLambda() [1/2]

Lambda mkLambda ( Expr[]  boundConstants,
Expr  body 
)
inline

Create a lambda expression.

Creates a lambda expression using a list of constants that will form the set of bound variables.

Definition at line 2561 of file Context.java.

2562 {
2563 return Lambda.of(this, boundConstants, body);
2564 }
def Lambda(vs, body)
Definition: z3py.py:2081

◆ mkLambda() [2/2]

Lambda mkLambda ( Sort[]  sorts,
Symbol[]  names,
Expr  body 
)
inline

Create a lambda expression.

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 lambda. 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.

Parameters
sortsthe sorts of the bound variables.
namesnames of the bound variables.
bodythe body of the quantifier.

Definition at line 2550 of file Context.java.

2551 {
2552 return Lambda.of(this, sorts, names, body);
2553 }

◆ mkLe()

BoolExpr mkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 &lt;= t2

Definition at line 901 of file Context.java.

902 {
903 checkContextMatch(t1);
904 checkContextMatch(t2);
905 return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
906 t2.getNativeObject()));
907 }

◆ mkLength()

IntExpr mkLength ( SeqExpr  s)
inline

Retrieve the length of a given sequence.

Definition at line 2009 of file Context.java.

2010 {
2011 checkContextMatch(s);
2012 return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
2013 }

◆ mkListSort() [1/2]

ListSort mkListSort ( String  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 309 of file Context.java.

310 {
311 checkContextMatch(elemSort);
312 return new ListSort(this, mkSymbol(name), elemSort);
313 }

◆ mkListSort() [2/2]

ListSort mkListSort ( Symbol  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 299 of file Context.java.

300 {
301 checkContextMatch(name);
302 checkContextMatch(elemSort);
303 return new ListSort(this, name, elemSort);
304 }

◆ mkLoop() [1/2]

ReExpr mkLoop ( ReExpr  re,
int  lo 
)
inline

Take the lower-bounded Kleene star of a regular expression.

Definition at line 2117 of file Context.java.

2118 {
2119 return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
2120 }

◆ mkLoop() [2/2]

ReExpr mkLoop ( ReExpr  re,
int  lo,
int  hi 
)
inline

Take the lower and upper-bounded Kleene star of a regular expression.

Definition at line 2109 of file Context.java.

2110 {
2111 return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
2112 }

◆ mkLt()

BoolExpr mkLt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 &lt; t2

Definition at line 890 of file Context.java.

891 {
892 checkContextMatch(t1);
893 checkContextMatch(t2);
894 return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
895 t2.getNativeObject()));
896 }

◆ mkMap()

ArrayExpr mkMap ( FuncDecl  f,
ArrayExpr...  args 
)
inline

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

See also
mkArraySort
mkSelect
mkStore

Definition at line 1795 of file Context.java.

1796 {
1797 checkContextMatch(f);
1798 checkContextMatch(args);
1799 return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1800 f.getNativeObject(), AST.arrayLength(args),
1801 AST.arrayToNative(args)));
1802 }

◆ mkMod()

IntExpr mkMod ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 mod t2. Remarks: The arguments must have int type.

Definition at line 853 of file Context.java.

854 {
855 checkContextMatch(t1);
856 checkContextMatch(t2);
857 return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
858 t2.getNativeObject()));
859 }

◆ mkMul()

ArithExpr mkMul ( ArithExpr...  t)
inline

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

Definition at line 810 of file Context.java.

811 {
812 checkContextMatch(t);
813 return (ArithExpr) Expr.create(this,
814 Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
815 }

◆ mkNot()

BoolExpr mkNot ( BoolExpr  a)
inline

Create an expression representing not(a).

Definition at line 722 of file Context.java.

723 {
724 checkContextMatch(a);
725 return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
726 }

◆ mkNumeral() [1/3]

Expr mkNumeral ( int  v,
Sort  ty 
)
inline

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.

Parameters
vValue of the numeral
tySort of the numeral
Returns
A Term with value v and type ty

Definition at line 2278 of file Context.java.

2279 {
2280 checkContextMatch(ty);
2281 return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
2282 }

◆ mkNumeral() [2/3]

Expr mkNumeral ( long  v,
Sort  ty 
)
inline

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.

Parameters
vValue of the numeral
tySort of the numeral
Returns
A Term with value v and type ty

Definition at line 2294 of file Context.java.

2295 {
2296 checkContextMatch(ty);
2297 return Expr.create(this,
2298 Native.mkInt64(nCtx(), v, ty.getNativeObject()));
2299 }

◆ mkNumeral() [3/3]

Expr mkNumeral ( String  v,
Sort  ty 
)
inline

Create a Term of a given sort.

Parameters
vA string representing the term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*.
tyThe sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size.
Returns
A Term with value v and sort ty

Definition at line 2261 of file Context.java.

2262 {
2263 checkContextMatch(ty);
2264 return Expr.create(this,
2265 Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
2266 }

Referenced by Context.mkBV().

◆ mkOptimize()

Optimize mkOptimize ( )
inline

Create a Optimize context.

Definition at line 3126 of file Context.java.

3127 {
3128 return new Optimize(this);
3129 }

◆ mkOption()

ReExpr mkOption ( ReExpr  re)
inline

Create the optional regular expression.

Definition at line 2135 of file Context.java.

2136 {
2137 checkContextMatch(re);
2138 return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
2139 }

◆ mkOr()

BoolExpr mkOr ( BoolExpr...  t)
inline

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

Definition at line 790 of file Context.java.

791 {
792 checkContextMatch(t);
793 return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
794 AST.arrayToNative(t)));
795 }

◆ mkParams()

Params mkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2677 of file Context.java.

2678 {
2679 return new Params(this);
2680 }

◆ mkPattern()

Pattern mkPattern ( Expr...  terms)
inline

Create a quantifier pattern.

Definition at line 546 of file Context.java.

547 {
548 if (terms.length == 0)
549 throw new Z3Exception("Cannot create a pattern from zero terms");
550
551 long[] termsNative = AST.arrayToNative(terms);
552 return new Pattern(this, Native.mkPattern(nCtx(), terms.length,
553 termsNative));
554 }

◆ mkPBEq()

BoolExpr mkPBEq ( int[]  coeffs,
BoolExpr[]  args,
int  k 
)
inline

Create a pseudo-Boolean equal constraint.

Definition at line 2243 of file Context.java.

2244 {
2245 checkContextMatch(args);
2246 return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2247 }

◆ mkPBGe()

BoolExpr mkPBGe ( int[]  coeffs,
BoolExpr[]  args,
int  k 
)
inline

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

Definition at line 2234 of file Context.java.

2235 {
2236 checkContextMatch(args);
2237 return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2238 }

◆ mkPBLe()

BoolExpr mkPBLe ( int[]  coeffs,
BoolExpr[]  args,
int  k 
)
inline

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

Definition at line 2225 of file Context.java.

2226 {
2227 checkContextMatch(args);
2228 return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2229 }

◆ mkPlus()

ReExpr mkPlus ( ReExpr  re)
inline

Take the Kleene plus of a regular expression.

Definition at line 2126 of file Context.java.

2127 {
2128 checkContextMatch(re);
2129 return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
2130 }

◆ mkPower()

ArithExpr mkPower ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 ^ t2.

Definition at line 877 of file Context.java.

878 {
879 checkContextMatch(t1);
880 checkContextMatch(t2);
881 return (ArithExpr) Expr.create(
882 this,
883 Native.mkPower(nCtx(), t1.getNativeObject(),
884 t2.getNativeObject()));
885 }

◆ mkPrefixOf()

BoolExpr mkPrefixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence prefix.

Definition at line 2018 of file Context.java.

2019 {
2020 checkContextMatch(s1, s2);
2021 return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2022 }

◆ mkProbe()

Probe mkProbe ( String  name)
inline

Creates a new Probe.

Definition at line 2950 of file Context.java.

2951 {
2952 return new Probe(this, name);
2953 }

◆ mkQuantifier() [1/2]

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

Create a Quantifier

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

Definition at line 2520 of file Context.java.

2523 {
2524
2525 if (universal)
2526 return mkForall(boundConstants, body, weight, patterns, noPatterns,
2527 quantifierID, skolemID);
2528 else
2529 return mkExists(boundConstants, body, weight, patterns, noPatterns,
2530 quantifierID, skolemID);
2531 }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2476
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2450

◆ mkQuantifier() [2/2]

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

Create a Quantifier.

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

Definition at line 2502 of file Context.java.

2506 {
2507
2508 if (universal)
2509 return mkForall(sorts, names, body, weight, patterns, noPatterns,
2510 quantifierID, skolemID);
2511 else
2512 return mkExists(sorts, names, body, weight, patterns, noPatterns,
2513 quantifierID, skolemID);
2514 }

◆ mkRange()

ReExpr mkRange ( SeqExpr  lo,
SeqExpr  hi 
)
inline

Create a range expression.

Definition at line 2197 of file Context.java.

2198 {
2199 checkContextMatch(lo, hi);
2200 return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
2201 }

◆ mkReal() [1/4]

RatNum mkReal ( int  num,
int  den 
)
inline

Create a real from a fraction.

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

Definition at line 2310 of file Context.java.

2311 {
2312 if (den == 0) {
2313 throw new Z3Exception("Denominator is zero");
2314 }
2315
2316 return new RatNum(this, Native.mkReal(nCtx(), num, den));
2317 }

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

2339 {
2340
2341 return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2342 .getNativeObject()));
2343 }

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

2352 {
2353
2354 return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2355 .getNativeObject()));
2356 }

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

2326 {
2327
2328 return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2329 .getNativeObject()));
2330 }

◆ mkReal2Int()

IntExpr mkReal2Int ( RealExpr  t)
inline

Coerce a real to an integer. Remarks: The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort.

Definition at line 954 of file Context.java.

955 {
956 checkContextMatch(t);
957 return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
958 }

◆ mkRealConst() [1/2]

RealExpr mkRealConst ( String  name)
inline

Creates a real constant.

Definition at line 643 of file Context.java.

644 {
645 return (RealExpr) mkConst(name, getRealSort());
646 }

◆ mkRealConst() [2/2]

RealExpr mkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 635 of file Context.java.

636 {
637 return (RealExpr) mkConst(name, getRealSort());
638 }

◆ mkRealSort()

RealSort mkRealSort ( )
inline

Create a real sort.

Definition at line 204 of file Context.java.

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

◆ mkRem()

IntExpr mkRem ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 rem t2. Remarks: The arguments must have int type.

Definition at line 866 of file Context.java.

867 {
868 checkContextMatch(t1);
869 checkContextMatch(t2);
870 return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
871 t2.getNativeObject()));
872 }

◆ mkRepeat()

BitVecExpr mkRepeat ( int  i,
BitVecExpr  t 
)
inline

Bit-vector repetition. Remarks: The argument t must have a bit-vector sort.

Definition at line 1386 of file Context.java.

1387 {
1388 checkContextMatch(t);
1389 return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1390 t.getNativeObject()));
1391 }

◆ mkReplace()

SeqExpr mkReplace ( SeqExpr  s,
SeqExpr  src,
SeqExpr  dst 
)
inline

Replace the first occurrence of src by dst in s.

Definition at line 2072 of file Context.java.

2073 {
2074 checkContextMatch(s, src, dst);
2075 return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
2076 }

◆ mkReSort()

ReSort mkReSort ( Sort  s)
inline

Create a new regular expression sort

Definition at line 257 of file Context.java.

258 {
259 return new ReSort(this, Native.mkReSort(nCtx(), s.getNativeObject()));
260 }
def ReSort(s)
Definition: z3py.py:10294

◆ mkSelect() [1/2]

Expr mkSelect ( ArrayExpr  a,
Expr  i 
)
inline

Array read. Remarks: The argument a is the array and i is the index of the array that gets read.

The node a must have an array sort [domain -> range], and i must have the sort domain. The sort of the result is range.

See also
mkArraySort
mkStore

Definition at line 1683 of file Context.java.

1684 {
1685 checkContextMatch(a);
1686 checkContextMatch(i);
1687 return Expr.create(
1688 this,
1689 Native.mkSelect(nCtx(), a.getNativeObject(),
1690 i.getNativeObject()));
1691 }

◆ mkSelect() [2/2]

Expr mkSelect ( ArrayExpr  a,
Expr[]  args 
)
inline

Array read. Remarks: The argument a is the array and args are the indices of the array that gets read.

The node a must have an array sort [domains -> range], and args must have the sorts domains. The sort of the result is range.

See also
mkArraySort
mkStore

Definition at line 1706 of file Context.java.

1707 {
1708 checkContextMatch(a);
1709 checkContextMatch(args);
1710 return Expr.create(
1711 this,
1712 Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
1713 }

◆ mkSeqSort()

SeqSort mkSeqSort ( Sort  s)
inline

Create a new sequence sort

Definition at line 249 of file Context.java.

250 {
251 return new SeqSort(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
252 }
def SeqSort(s)
Definition: z3py.py:9980

◆ mkSetAdd()

ArrayExpr mkSetAdd ( ArrayExpr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 1860 of file Context.java.

1861 {
1862 checkContextMatch(set);
1863 checkContextMatch(element);
1864 return (ArrayExpr)Expr.create(this,
1865 Native.mkSetAdd(nCtx(), set.getNativeObject(),
1866 element.getNativeObject()));
1867 }

◆ mkSetComplement()

ArrayExpr mkSetComplement ( ArrayExpr  arg)
inline

Take the complement of a set.

Definition at line 1918 of file Context.java.

1919 {
1920 checkContextMatch(arg);
1921 return (ArrayExpr)Expr.create(this,
1922 Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1923 }

◆ mkSetDel()

ArrayExpr mkSetDel ( ArrayExpr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 1872 of file Context.java.

1873 {
1874 checkContextMatch(set);
1875 checkContextMatch(element);
1876 return (ArrayExpr)Expr.create(this,
1877 Native.mkSetDel(nCtx(), set.getNativeObject(),
1878 element.getNativeObject()));
1879 }

◆ mkSetDifference()

ArrayExpr mkSetDifference ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Take the difference between two sets.

Definition at line 1906 of file Context.java.

1907 {
1908 checkContextMatch(arg1);
1909 checkContextMatch(arg2);
1910 return (ArrayExpr)Expr.create(this,
1911 Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1912 arg2.getNativeObject()));
1913 }

◆ mkSetIntersection()

ArrayExpr mkSetIntersection ( ArrayExpr...  args)
inline

Take the intersection of a list of sets.

Definition at line 1895 of file Context.java.

1896 {
1897 checkContextMatch(args);
1898 return (ArrayExpr)Expr.create(this,
1899 Native.mkSetIntersect(nCtx(), args.length,
1900 AST.arrayToNative(args)));
1901 }

◆ mkSetMembership()

BoolExpr mkSetMembership ( Expr  elem,
ArrayExpr  set 
)
inline

Check for set membership.

Definition at line 1928 of file Context.java.

1929 {
1930 checkContextMatch(elem);
1931 checkContextMatch(set);
1932 return (BoolExpr) Expr.create(this,
1933 Native.mkSetMember(nCtx(), elem.getNativeObject(),
1934 set.getNativeObject()));
1935 }

◆ mkSetSort()

SetSort mkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 1831 of file Context.java.

1832 {
1833 checkContextMatch(ty);
1834 return new SetSort(this, ty);
1835 }
def SetSort(s)
Sets.
Definition: z3py.py:4568

◆ mkSetSubset()

BoolExpr mkSetSubset ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 1940 of file Context.java.

1941 {
1942 checkContextMatch(arg1);
1943 checkContextMatch(arg2);
1944 return (BoolExpr) Expr.create(this,
1945 Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1946 arg2.getNativeObject()));
1947 }

◆ mkSetUnion()

ArrayExpr mkSetUnion ( ArrayExpr...  args)
inline

Take the union of a list of sets.

Definition at line 1884 of file Context.java.

1885 {
1886 checkContextMatch(args);
1887 return (ArrayExpr)Expr.create(this,
1888 Native.mkSetUnion(nCtx(), args.length,
1889 AST.arrayToNative(args)));
1890 }

◆ mkSignExt()

BitVecExpr mkSignExt ( int  i,
BitVecExpr  t 
)
inline

Bit-vector sign extension. Remarks: Sign-extends the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector. The argument t must have a bit-vector sort.

Definition at line 1360 of file Context.java.

1361 {
1362 checkContextMatch(t);
1363 return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1364 t.getNativeObject()));
1365 }

◆ mkSimpleSolver()

Solver mkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3097 of file Context.java.

3098 {
3099 return new Solver(this, Native.mkSimpleSolver(nCtx()));
3100 }

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

3064 {
3065 return mkSolver((Symbol) null);
3066 }

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

◆ mkSolver() [2/4]

Solver mkSolver ( String  logic)
inline

Creates a new (incremental) solver.

See also
mkSolver(Symbol)

Definition at line 3089 of file Context.java.

3090 {
3091 return mkSolver(mkSymbol(logic));
3092 }

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

3076 {
3077
3078 if (logic == null)
3079 return new Solver(this, Native.mkSolver(nCtx()));
3080 else
3081 return new Solver(this, Native.mkSolverForLogic(nCtx(),
3082 logic.getNativeObject()));
3083 }

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

3109 {
3110
3111 return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3112 t.getNativeObject()));
3113 }

◆ mkStar()

ReExpr mkStar ( ReExpr  re)
inline

Take the Kleene star of a regular expression.

Definition at line 2100 of file Context.java.

2101 {
2102 checkContextMatch(re);
2103 return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
2104 }

◆ mkStore() [1/2]

ArrayExpr mkStore ( ArrayExpr  a,
Expr  i,
Expr  v 
)
inline

Array update. Remarks: The node a must have an array sort [domain -> range], i must have sort domain, v must have sort range. The sort of the result is [domain -> range]. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to a (with respect to select) on all indices except for i, where it maps to v (and the select of a with respect to i may be a different value).

See also
mkArraySort
mkSelect

Definition at line 1731 of file Context.java.

1732 {
1733 checkContextMatch(a);
1734 checkContextMatch(i);
1735 checkContextMatch(v);
1736 return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1737 i.getNativeObject(), v.getNativeObject()));
1738 }

◆ mkStore() [2/2]

ArrayExpr mkStore ( ArrayExpr  a,
Expr[]  args,
Expr  v 
)
inline

Array update. Remarks: The node a must have an array sort [domains -> range], i must have sort domain, v must have sort range. The sort of the result is [domains -> range]. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to a (with respect to select) on all indices except for args, where it maps to v (and the select of a with respect to args may be a different value).

See also
mkArraySort
mkSelect

Definition at line 1756 of file Context.java.

1757 {
1758 checkContextMatch(a);
1759 checkContextMatch(args);
1760 checkContextMatch(v);
1761 return new ArrayExpr(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
1762 args.length, AST.arrayToNative(args), v.getNativeObject()));
1763 }

◆ mkString()

SeqExpr mkString ( String  s)
inline

Create a string constant.

Definition at line 1975 of file Context.java.

1976 {
1977 return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
1978 }

◆ mkStringSort()

SeqSort mkStringSort ( )
inline

Create a new string sort

Definition at line 241 of file Context.java.

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

Referenced by Context.getStringSort().

◆ mkSub()

ArithExpr mkSub ( ArithExpr...  t)
inline

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

Definition at line 820 of file Context.java.

821 {
822 checkContextMatch(t);
823 return (ArithExpr) Expr.create(this,
824 Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
825 }

◆ mkSuffixOf()

BoolExpr mkSuffixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence suffix.

Definition at line 2027 of file Context.java.

2028 {
2029 checkContextMatch(s1, s2);
2030 return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2031 }

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

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

Referenced by Optimize.AssertSoft(), Context.mkArrayConst(), Context.mkBoolConst(), Context.mkConst(), Context.mkConstDecl(), Context.mkConstructor(), Context.mkDatatypeSort(), Context.mkEnumSort(), Context.mkFiniteDomainSort(), Context.mkFuncDecl(), Context.mkListSort(), Context.mkSolver(), and Context.mkUninterpretedSort().

◆ mkSymbol() [2/2]

StringSymbol mkSymbol ( String  name)
inline

Create a symbol using a string.

Definition at line 101 of file Context.java.

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

◆ mkTactic()

Tactic mkTactic ( String  name)
inline

Creates a new Tactic.

Definition at line 2715 of file Context.java.

2716 {
2717 return new Tactic(this, name);
2718 }

Referenced by Goal.simplify().

◆ mkTermArray()

Expr mkTermArray ( ArrayExpr  array)
inline

Access the array default value. Remarks: Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Definition at line 1810 of file Context.java.

1811 {
1812 checkContextMatch(array);
1813 return Expr.create(this,
1814 Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1815 }

◆ mkToRe()

ReExpr mkToRe ( SeqExpr  s)
inline

Convert a regular expression that accepts sequence s.

Definition at line 2081 of file Context.java.

2082 {
2083 checkContextMatch(s);
2084 return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
2085 }

◆ mkTrue()

BoolExpr mkTrue ( )
inline

The true Term.

Definition at line 677 of file Context.java.

678 {
679 return new BoolExpr(this, Native.mkTrue(nCtx()));
680 }

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

◆ mkTupleSort()

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

Create a new tuple sort.

Definition at line 266 of file Context.java.

268 {
269 checkContextMatch(name);
270 checkContextMatch(fieldNames);
271 checkContextMatch(fieldSorts);
272 return new TupleSort(this, name, fieldNames.length, fieldNames,
273 fieldSorts);
274 }
def TupleSort(name, sorts, ctx=None)
Definition: z3py.py:4971

◆ mkUnaryMinus()

ArithExpr mkUnaryMinus ( ArithExpr  t)
inline

Create an expression representing -t.

Definition at line 830 of file Context.java.

831 {
832 checkContextMatch(t);
833 return (ArithExpr) Expr.create(this,
834 Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
835 }

◆ mkUninterpretedSort() [1/2]

UninterpretedSort mkUninterpretedSort ( String  str)
inline

Create a new uninterpreted sort.

Definition at line 188 of file Context.java.

189 {
190 return mkUninterpretedSort(mkSymbol(str));
191 }
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:179

◆ mkUninterpretedSort() [2/2]

UninterpretedSort mkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 179 of file Context.java.

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

Referenced by Context.mkUninterpretedSort().

◆ mkUnion()

ReExpr mkUnion ( ReExpr...  t)
inline

Create the union of regular languages.

Definition at line 2163 of file Context.java.

2164 {
2165 checkContextMatch(t);
2166 return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2167 }

◆ mkUnit()

SeqExpr mkUnit ( Expr  elem)
inline

Create the singleton sequence.

Definition at line 1966 of file Context.java.

1967 {
1968 checkContextMatch(elem);
1969 return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
1970 }

◆ mkUpdateField()

Expr mkUpdateField ( FuncDecl  field,
Expr  t,
Expr  v 
) throws Z3Exception
inline

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

Definition at line 428 of file Context.java.

430 {
431 return Expr.create (this,
432 Native.datatypeUpdateField
433 (nCtx(), field.getNativeObject(),
434 t.getNativeObject(), v.getNativeObject()));
435 }

◆ mkXor()

BoolExpr mkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 xor t2.

Definition at line 769 of file Context.java.

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

◆ mkZeroExt()

BitVecExpr mkZeroExt ( int  i,
BitVecExpr  t 
)
inline

Bit-vector zero extension. Remarks: Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector. The argument t must have a bit-vector sort.

Definition at line 1374 of file Context.java.

1375 {
1376 checkContextMatch(t);
1377 return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1378 t.getNativeObject()));
1379 }

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

3051 {
3052 checkContextMatch(p);
3053 return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
3054 }

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

3040 {
3041 checkContextMatch(p1);
3042 checkContextMatch(p2);
3043 return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
3044 p2.getNativeObject()));
3045 }

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

2767 {
2768 checkContextMatch(t1);
2769 checkContextMatch(t2);
2770 return new Tactic(this, Native.tacticOrElse(nCtx(),
2771 t1.getNativeObject(), t2.getNativeObject()));
2772 }

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

2900 {
2901 checkContextMatch(t1);
2902 checkContextMatch(t2);
2903 return new Tactic(this, Native.tacticParAndThen(nCtx(),
2904 t1.getNativeObject(), t2.getNativeObject()));
2905 }

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

2889 {
2890 checkContextMatch(t);
2891 return new Tactic(this, Native.tacticParOr(nCtx(),
2892 Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2893 }

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

2643 {
2644 int csn = Symbol.arrayLength(sortNames);
2645 int cs = Sort.arrayLength(sorts);
2646 int cdn = Symbol.arrayLength(declNames);
2647 int cd = AST.arrayLength(decls);
2648 if (csn != cs || cdn != cd)
2649 throw new Z3Exception("Argument size mismatch");
2650 ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
2651 fileName, AST.arrayLength(sorts),
2652 Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2653 AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2654 AST.arrayToNative(decls)));
2655 return v.ToBoolExprArray();
2656 }

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

2621 {
2622 int csn = Symbol.arrayLength(sortNames);
2623 int cs = Sort.arrayLength(sorts);
2624 int cdn = Symbol.arrayLength(declNames);
2625 int cd = AST.arrayLength(decls);
2626 if (csn != cs || cdn != cd) {
2627 throw new Z3Exception("Argument size mismatch");
2628 }
2629 ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
2630 str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2631 AST.arrayToNative(sorts), AST.arrayLength(decls),
2632 Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2633 return v.ToBoolExprArray();
2634 }

◆ repeat()

Tactic repeat ( Tactic  t,
int  max 
)
inline

Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.

Definition at line 2819 of file Context.java.

2820 {
2821 checkContextMatch(t);
2822 return new Tactic(this, Native.tacticRepeat(nCtx(),
2823 t.getNativeObject(), max));
2824 }
expr max(expr const &a, expr const &b)
Definition: z3++.h:1591

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

2582 {
2583 Native.setAstPrintMode(nCtx(), value.toInt());
2584 }

◆ SimplifyHelp()

String SimplifyHelp ( )
inline

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

Definition at line 3939 of file Context.java.

3940 {
3941 return Native.simplifyGetHelp(nCtx());
3942 }

◆ skip()

Tactic skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 2829 of file Context.java.

2830 {
2831 return new Tactic(this, Native.tacticSkip(nCtx()));
2832 }

◆ stringToInt()

IntExpr stringToInt ( Expr  e)
inline

Convert an integer expression to a string.

Definition at line 1991 of file Context.java.

1992 {
1993 return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
1994 }

◆ then()

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

Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1

Remarks: Shorthand for AndThen.

Definition at line 2756 of file Context.java.

2757 {
2758 return andThen(t1, t2, ts);
2759 }
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2724

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

2781 {
2782 checkContextMatch(t);
2783 return new Tactic(this, Native.tacticTryFor(nCtx(),
2784 t.getNativeObject(), ms));
2785 }

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

3931 {
3932 return a.getNativeObject();
3933 }

◆ updateParamValue()

void updateParamValue ( String  id,
String  value 
)
inline

Update a mutable configuration parameter. Remarks: The list of all configuration parameters can be obtained using the Z3 executable: z3.exe -ini? Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.

Definition at line 3960 of file Context.java.

3961 {
3962 Native.updateParamValue(nCtx(), id, value);
3963 }

◆ usingParams()

Tactic usingParams ( Tactic  t,
Params  p 
)
inline

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

Definition at line 2866 of file Context.java.

2867 {
2868 checkContextMatch(t);
2869 checkContextMatch(p);
2870 return new Tactic(this, Native.tacticUsingParams(nCtx(),
2871 t.getNativeObject(), p.getNativeObject()));
2872 }

Referenced by Context.with().

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

2794 {
2795 checkContextMatch(t);
2796 checkContextMatch(p);
2797 return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2798 t.getNativeObject()));
2799 }

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

2881 {
2882 return usingParams(t, p);
2883 }
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2866

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

3914 {
3915 return AST.create(this, nativeObject);
3916 }