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 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 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)
 
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:4296
def String(name, ctx=None)
Definition: z3py.py:9738

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

2959  {
2960  checkContextMatch(p1);
2961  checkContextMatch(p2);
2962  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
2963  p2.getNativeObject()));
2964  }

◆ 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 <paramref name="t1

.

Definition at line 2654 of file Context.java.

Referenced by Context.then().

2656  {
2657  checkContextMatch(t1);
2658  checkContextMatch(t2);
2659  checkContextMatch(ts);
2660 
2661  long last = 0;
2662  if (ts != null && ts.length > 0)
2663  {
2664  last = ts[ts.length - 1].getNativeObject();
2665  for (int i = ts.length - 2; i >= 0; i--) {
2666  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2667  last);
2668  }
2669  }
2670  if (last != 0)
2671  {
2672  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2673  return new Tactic(this, Native.tacticAndThen(nCtx(),
2674  t1.getNativeObject(), last));
2675  } else
2676  return new Tactic(this, Native.tacticAndThen(nCtx(),
2677  t1.getNativeObject(), t2.getNativeObject()));
2678  }

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

2536  {
2537 
2538  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2539  attributes, assumptions.length,
2540  AST.arrayToNative(assumptions), formula.getNativeObject());
2541  }

◆ close()

void close ( )
inline

Disposes of the context.

Definition at line 4040 of file Context.java.

4041  {
4042  m_AST_DRQ.forceClear(this);
4043  m_ASTMap_DRQ.forceClear(this);
4044  m_ASTVector_DRQ.forceClear(this);
4045  m_ApplyResult_DRQ.forceClear(this);
4046  m_FuncEntry_DRQ.forceClear(this);
4047  m_FuncInterp_DRQ.forceClear(this);
4048  m_Goal_DRQ.forceClear(this);
4049  m_Model_DRQ.forceClear(this);
4050  m_Params_DRQ.forceClear(this);
4051  m_Probe_DRQ.forceClear(this);
4052  m_Solver_DRQ.forceClear(this);
4053  m_Optimize_DRQ.forceClear(this);
4054  m_Statistics_DRQ.forceClear(this);
4055  m_Tactic_DRQ.forceClear(this);
4056  m_Fixedpoint_DRQ.forceClear(this);
4057 
4058  m_boolSort = null;
4059  m_intSort = null;
4060  m_realSort = null;
4061  m_stringSort = null;
4062 
4063  synchronized (creation_lock) {
4064  Native.delContext(m_ctx);
4065  }
4066  }

◆ 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 <paramref name="t2

otherwise.

Definition at line 2736 of file Context.java.

2737  {
2738  checkContextMatch(p);
2739  checkContextMatch(t1);
2740  checkContextMatch(t2);
2741  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2742  t1.getNativeObject(), t2.getNativeObject()));
2743  }

◆ constProbe()

Probe constProbe ( double  val)
inline

Create a probe that always evaluates to

val

.

Definition at line 2888 of file Context.java.

2889  {
2890  return new Probe(this, Native.probeConst(nCtx(), val));
2891  }

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

2948  {
2949  checkContextMatch(p1);
2950  checkContextMatch(p2);
2951  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2952  p2.getNativeObject()));
2953  }

◆ fail()

Tactic fail ( )
inline

Create a tactic always fails.

Definition at line 2767 of file Context.java.

2768  {
2769  return new Tactic(this, Native.tacticFail(nCtx()));
2770  }

◆ failIf()

Tactic failIf ( Probe  p)
inline

Create a tactic that fails if the probe

p

evaluates to false.

Definition at line 2776 of file Context.java.

2777  {
2778  checkContextMatch(p);
2779  return new Tactic(this,
2780  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2781  }

◆ failIfNotDecided()

Tactic failIfNotDecided ( )
inline

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

Definition at line 2787 of file Context.java.

2788  {
2789  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2790  }

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

2936  {
2937  checkContextMatch(p1);
2938  checkContextMatch(p2);
2939  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2940  p2.getNativeObject()));
2941  }

◆ getApplyResultDRQ()

IDecRefQueue<ApplyResult> getApplyResultDRQ ( )
inline

Definition at line 3971 of file Context.java.

3972  {
3973  return m_ApplyResult_DRQ;
3974  }

◆ getASTDRQ()

IDecRefQueue<AST> getASTDRQ ( )
inline

Definition at line 3956 of file Context.java.

3957  {
3958  return m_AST_DRQ;
3959  }

◆ getASTMapDRQ()

IDecRefQueue<ASTMap> getASTMapDRQ ( )
inline

Definition at line 3961 of file Context.java.

3962  {
3963  return m_ASTMap_DRQ;
3964  }

◆ getASTVectorDRQ()

IDecRefQueue<ASTVector> getASTVectorDRQ ( )
inline

Definition at line 3966 of file Context.java.

3967  {
3968  return m_ASTVector_DRQ;
3969  }

◆ getBoolSort()

BoolSort getBoolSort ( )
inline

Retrieves the Boolean sort of the context.

Definition at line 127 of file Context.java.

Referenced by Context.mkBoolConst().

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:1435

◆ getConstructorDRQ()

IDecRefQueue<Constructor> getConstructorDRQ ( )
inline

Definition at line 3948 of file Context.java.

3948  {
3949  return m_Constructor_DRQ;
3950  }

◆ getConstructorListDRQ()

IDecRefQueue<ConstructorList> getConstructorListDRQ ( )
inline

Definition at line 3952 of file Context.java.

3952  {
3953  return m_ConstructorList_DRQ;
3954  }

◆ getFixedpointDRQ()

IDecRefQueue<Fixedpoint> getFixedpointDRQ ( )
inline

Definition at line 4026 of file Context.java.

4027  {
4028  return m_Fixedpoint_DRQ;
4029  }

◆ getFuncEntryDRQ()

IDecRefQueue<FuncInterp.Entry> getFuncEntryDRQ ( )
inline

Definition at line 3976 of file Context.java.

3977  {
3978  return m_FuncEntry_DRQ;
3979  }

◆ getFuncInterpDRQ()

IDecRefQueue<FuncInterp> getFuncInterpDRQ ( )
inline

Definition at line 3981 of file Context.java.

3982  {
3983  return m_FuncInterp_DRQ;
3984  }

◆ getGoalDRQ()

IDecRefQueue<Goal> getGoalDRQ ( )
inline

Definition at line 3986 of file Context.java.

3987  {
3988  return m_Goal_DRQ;
3989  }

◆ getIntSort()

IntSort getIntSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 138 of file Context.java.

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

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:2746

◆ getModelDRQ()

IDecRefQueue<Model> getModelDRQ ( )
inline

Definition at line 3991 of file Context.java.

3992  {
3993  return m_Model_DRQ;
3994  }

◆ getNumProbes()

int getNumProbes ( )
inline

The number of supported Probes.

Definition at line 2850 of file Context.java.

Referenced by Context.getProbeNames().

2851  {
2852  return Native.getNumProbes(nCtx());
2853  }

◆ getNumTactics()

int getNumTactics ( )
inline

The number of supported tactics.

Definition at line 2615 of file Context.java.

Referenced by Context.getTacticNames().

2616  {
2617  return Native.getNumTactics(nCtx());
2618  }

◆ getOptimizeDRQ()

IDecRefQueue<Optimize> getOptimizeDRQ ( )
inline

Definition at line 4031 of file Context.java.

4032  {
4033  return m_Optimize_DRQ;
4034  }

◆ getParamDescrsDRQ()

IDecRefQueue<ParamDescrs> getParamDescrsDRQ ( )
inline

Definition at line 4001 of file Context.java.

4002  {
4003  return m_ParamDescrs_DRQ;
4004  }

◆ getParamsDRQ()

IDecRefQueue<Params> getParamsDRQ ( )
inline

Definition at line 3996 of file Context.java.

3997  {
3998  return m_Params_DRQ;
3999  }

◆ getProbeDescription()

String getProbeDescription ( String  name)
inline

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

Definition at line 2872 of file Context.java.

2873  {
2874  return Native.probeGetDescr(nCtx(), name);
2875  }

◆ getProbeDRQ()

IDecRefQueue<Probe> getProbeDRQ ( )
inline

Definition at line 4006 of file Context.java.

4007  {
4008  return m_Probe_DRQ;
4009  }

◆ getProbeNames()

String [] getProbeNames ( )
inline

The names of all supported Probes.

Definition at line 2858 of file Context.java.

2859  {
2860 
2861  int n = getNumProbes();
2862  String[] res = new String[n];
2863  for (int i = 0; i < n; i++)
2864  res[i] = Native.getProbeName(nCtx(), i);
2865  return res;
2866  }
def String(name, ctx=None)
Definition: z3py.py:9738

◆ getRealSort()

RealSort getRealSort ( )
inline

Retrieves the Real sort of the context.

Definition at line 149 of file Context.java.

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

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:2762

◆ getSimplifyParameterDescriptions()

ParamDescrs getSimplifyParameterDescriptions ( )
inline

Retrieves parameter descriptions for simplifier.

Definition at line 3877 of file Context.java.

3878  {
3879  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3880  }

◆ getSolverDRQ()

IDecRefQueue<Solver> getSolverDRQ ( )
inline

Definition at line 4011 of file Context.java.

4012  {
4013  return m_Solver_DRQ;
4014  }

◆ getStatisticsDRQ()

IDecRefQueue<Statistics> getStatisticsDRQ ( )
inline

Definition at line 4016 of file Context.java.

4017  {
4018  return m_Statistics_DRQ;
4019  }

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

2638  {
2639  return Native.tacticGetDescr(nCtx(), name);
2640  }

◆ getTacticDRQ()

IDecRefQueue<Tactic> getTacticDRQ ( )
inline

Definition at line 4021 of file Context.java.

4022  {
4023  return m_Tactic_DRQ;
4024  }

◆ getTacticNames()

String [] getTacticNames ( )
inline

The names of all supported tactics.

Definition at line 2623 of file Context.java.

2624  {
2625 
2626  int n = getNumTactics();
2627  String[] res = new String[n];
2628  for (int i = 0; i < n; i++)
2629  res[i] = Native.getTacticName(nCtx(), i);
2630  return res;
2631  }
def String(name, ctx=None)
Definition: z3py.py:9738

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

2910  {
2911  checkContextMatch(p1);
2912  checkContextMatch(p2);
2913  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2914  p2.getNativeObject()));
2915  }

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

2843  {
2844  Native.interrupt(nCtx());
2845  }

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

2923  {
2924  checkContextMatch(p1);
2925  checkContextMatch(p2);
2926  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2927  p2.getNativeObject()));
2928  }

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

2898  {
2899  checkContextMatch(p1);
2900  checkContextMatch(p2);
2901  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2902  p2.getNativeObject()));
2903  }

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

Referenced by Goal.AsBoolExpr().

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

◆ mkApp()

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

Create a new function application.

Definition at line 667 of file Context.java.

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

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

◆ mkArrayConst() [1/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  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:220
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

◆ mkArrayConst() [2/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  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
IntSymbol mkSymbol(int i)
Definition: Context.java:93
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:220
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

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

Referenced by Context.mkArrayConst().

221  {
222  checkContextMatch(domain);
223  checkContextMatch(range);
224  return new ArraySort(this, domain, range);
225  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
def ArraySort(d, r)
Definition: z3py.py:4199

◆ 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  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
def ArraySort(d, r)
Definition: z3py.py:4199

◆ mkAt()

SeqExpr mkAt ( SeqExpr  s,
IntExpr  index 
)
inline

Retrieve sequence of length one at index.

Definition at line 2029 of file Context.java.

2030  {
2031  checkContextMatch(s, index);
2032  return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
2033  }

◆ mkAtLeast()

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

Create an at-least-k constraint.

Definition at line 2184 of file Context.java.

2185  {
2186  checkContextMatch(args);
2187  return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
2188  }

◆ mkAtMost()

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

Create an at-most-k constraint.

Definition at line 2175 of file Context.java.

2176  {
2177  checkContextMatch(args);
2178  return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
2179  }

◆ mkBitVecSort()

BitVecSort mkBitVecSort ( int  size)
inline

Create a new bit-vector sort.

Definition at line 212 of file Context.java.

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

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

◆ 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 ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 603 of file Context.java.

604  {
605  return (BoolExpr) mkConst(name, getBoolSort());
606  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

◆ mkBoolConst() [2/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  }
IntSymbol mkSymbol(int i)
Definition: Context.java:93
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

◆ mkBoolSort()

BoolSort mkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 160 of file Context.java.

161  {
162  return new BoolSort(this);
163  }
def BoolSort(ctx=None)
Definition: z3py.py:1435

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

2369  {
2370  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2371  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2229
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212

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

2379  {
2380  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2381  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2229
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212

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

2389  {
2390  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2391  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2229
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212

◆ 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 ( 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  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

◆ mkBVConst() [2/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  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

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

◆ mkBVRotateLeft() [2/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  }

◆ mkBVRotateRight() [1/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  }

◆ mkBVRotateRight() [2/2]

BitVecExpr mkBVRotateRight ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Rotate Right. Remarks: Rotate bits of

t1

to the right

t2

times. The arguments must have the same bit-vector sort.

Definition at line 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  }

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

2130  {
2131  checkContextMatch(re);
2132  return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
2133  }

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

SeqExpr mkConcat ( SeqExpr...  t)
inline

Concatentate sequences.

Definition at line 1983 of file Context.java.

1984  {
1985  checkContextMatch(t);
1986  return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
1987  }

◆ mkConcat() [3/3]

ReExpr mkConcat ( ReExpr...  t)
inline

Create the concatenation of regular languages.

Definition at line 2138 of file Context.java.

2139  {
2140  checkContextMatch(t);
2141  return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2142  }

◆ mkConst() [1/3]

Expr mkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort

and named

name

.

Definition at line 560 of file Context.java.

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

561  {
562  checkContextMatch(name);
563  checkContextMatch(range);
564 
565  return Expr.create(
566  this,
567  Native.mkConst(nCtx(), name.getNativeObject(),
568  range.getNativeObject()));
569  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813

◆ mkConst() [2/3]

Expr mkConst ( String  name,
Sort  range 
)
inline

Creates a new Constant of sort

and named

name

.

Definition at line 575 of file Context.java.

576  {
577  return mkConst(mkSymbol(name), range);
578  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
IntSymbol mkSymbol(int i)
Definition: Context.java:93
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

◆ mkConst() [3/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

◆ mkConstArray()

ArrayExpr mkConstArray ( Sort  domain,
Expr  v 
)
inline

Create a constant array. Remarks: The resulting term is an array, such that a

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

◆ mkConstDecl() [2/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  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
IntSymbol mkSymbol(int i)
Definition: Context.java:93

◆ mkConstructor() [1/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  }

◆ mkConstructor() [2/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  }
IntSymbol mkSymbol(int i)
Definition: Context.java:93

◆ mkContains()

BoolExpr mkContains ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence containment of s2 in s1.

Definition at line 2020 of file Context.java.

2021  {
2022  checkContextMatch(s1, s2);
2023  return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2024  }

◆ mkDatatypeSort() [1/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  }

◆ mkDatatypeSort() [2/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  }
IntSymbol mkSymbol(int i)
Definition: Context.java:93

◆ mkDatatypeSorts() [1/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.

Referenced by Context.mkDatatypeSorts().

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  }

◆ mkDatatypeSorts() [2/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

◆ mkDistinct()

BoolExpr mkDistinct ( Expr...  args)
inline

Creates a

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  }

◆ 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 ( 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  }
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4668

◆ mkEnumSort() [2/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:4668
IntSymbol mkSymbol(int i)
Definition: Context.java:93

◆ mkEq()

BoolExpr mkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality

x"/> = <paramref name="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 ( Sort []  sorts,
Symbol []  names,
Expr  body,
int  weight,
Pattern []  patterns,
Expr []  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Creates an existential quantifier using de-Brujin indexed variables.

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

Definition at line 2444 of file Context.java.

Referenced by Context.mkQuantifier().

2447  {
2448 
2449  return Quantifier.of(this, false, sorts, names, body, weight,
2450  patterns, noPatterns, quantifierID, skolemID);
2451  }

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

2460  {
2461 
2462  return Quantifier.of(this, false, boundConstants, body, weight,
2463  patterns, noPatterns, quantifierID, skolemID);
2464  }

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

2039  {
2040  checkContextMatch(s, offset, length);
2041  return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
2042  }

◆ mkFalse()

BoolExpr mkFalse ( )
inline

The false Term.

Definition at line 685 of file Context.java.

Referenced by Context.mkBool().

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

◆ mkFiniteDomainSort() [1/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  }
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6767

◆ mkFiniteDomainSort() [2/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:6767
IntSymbol mkSymbol(int i)
Definition: Context.java:93

◆ mkFixedpoint()

Fixedpoint mkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3048 of file Context.java.

3049  {
3050  return new Fixedpoint(this);
3051  }

◆ mkForall() [1/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 2418 of file Context.java.

Referenced by Context.mkQuantifier().

2421  {
2422 
2423  return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2424  noPatterns, quantifierID, skolemID);
2425  }

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

2434  {
2435 
2436  return Quantifier.of(this, true, boundConstants, body, weight,
2437  patterns, noPatterns, quantifierID, skolemID);
2438  }

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

3343  {
3344  return mkFPNumeral(v, s);
3345  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3283

◆ mkFP() [2/6]

FPNum mkFP ( double  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 mkFPNumeral(v, s);
3356  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3283

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

3366  {
3367  return mkFPNumeral(v, s);
3368  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3283

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

3379  {
3380  return mkFPNumeral(sgn, sig, exp, s);
3381  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3283

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

3392  {
3393  return mkFPNumeral(sgn, sig, exp, s);
3394  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3283

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

3677  {
3678  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3679  }

◆ mkFPAbs()

FPExpr mkFPAbs ( FPExpr  t)
inline

Floating-point absolute value

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3402 of file Context.java.

3403  {
3404  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3405  }

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

3425  {
3426  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3427  }

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

3461  {
3462  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3463  }

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

3589  {
3590  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3591  }

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

3476  {
3477  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3478  }

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

3565  {
3566  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3567  }

◆ mkFPGt()

BoolExpr mkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3575 of file Context.java.

3576  {
3577  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3578  }

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

3262  {
3263  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3264  }

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

3629  {
3630  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3631  }

◆ mkFPIsNaN()

BoolExpr mkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3638 of file Context.java.

3639  {
3640  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3641  }

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

3649  {
3650  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3651  }

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

3599  {
3600  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3601  }

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

3659  {
3660  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3661  }

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

3609  {
3610  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3611  }

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

3619  {
3620  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3621  }

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

3543  {
3544  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3545  }

◆ mkFPLt()

BoolExpr mkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3553 of file Context.java.

3554  {
3555  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3556  }

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

3532  {
3533  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3534  }

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

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

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

3449  {
3450  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3451  }

◆ mkFPNaN()

FPNum mkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3250 of file Context.java.

3251  {
3252  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3253  }

◆ mkFPNeg()

FPExpr mkFPNeg ( FPExpr  t)
inline

Floating-point negation

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3412 of file Context.java.

3413  {
3414  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3415  }

◆ mkFPNumeral() [1/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 3283 of file Context.java.

Referenced by Context.mkFP().

3284  {
3285  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3286  }

◆ mkFPNumeral() [2/5]

FPNum mkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3294 of file Context.java.

3295  {
3296  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3297  }

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

3306  {
3307  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3308  }

◆ mkFPNumeral() [4/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.
sigthe significand.
expthe exponent.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3318 of file Context.java.

3319  {
3320  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3321  }

◆ mkFPNumeral() [5/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.
sigthe significand.
expthe exponent.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3331 of file Context.java.

3332  {
3333  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3334  }

◆ mkFPRem()

FPExpr mkFPRem ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3497 of file Context.java.

3498  {
3499  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3500  }

◆ mkFPRNA()

FPRMNum mkFPRNA ( )
inline

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

Exceptions
Z3Exception

Definition at line 3102 of file Context.java.

3103  {
3104  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3105  }

◆ mkFPRNE()

FPRMNum mkFPRNE ( )
inline

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

Exceptions
Z3Exception

Definition at line 3084 of file Context.java.

3085  {
3086  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3087  }

◆ mkFPRoundingModeSort()

FPRMSort mkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Exceptions
Z3Exception

Definition at line 3066 of file Context.java.

3067  {
3068  return new FPRMSort(this);
3069  }

◆ mkFPRoundNearestTiesToAway()

FPRMNum mkFPRoundNearestTiesToAway ( )
inline

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

Exceptions
Z3Exception

Definition at line 3093 of file Context.java.

3094  {
3095  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3096  }

◆ mkFPRoundNearestTiesToEven()

FPRMExpr mkFPRoundNearestTiesToEven ( )
inline

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

Exceptions
Z3Exception

Definition at line 3075 of file Context.java.

3076  {
3077  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3078  }

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

3510  {
3511  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3512  }

◆ mkFPRoundTowardNegative()

FPRMNum mkFPRoundTowardNegative ( )
inline

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

Exceptions
Z3Exception

Definition at line 3129 of file Context.java.

3130  {
3131  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3132  }

◆ mkFPRoundTowardPositive()

FPRMNum mkFPRoundTowardPositive ( )
inline

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

Exceptions
Z3Exception

Definition at line 3111 of file Context.java.

3112  {
3113  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3114  }

◆ mkFPRoundTowardZero()

FPRMNum mkFPRoundTowardZero ( )
inline

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

Exceptions
Z3Exception

Definition at line 3147 of file Context.java.

3148  {
3149  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3150  }

◆ mkFPRTN()

FPRMNum mkFPRTN ( )
inline

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

Exceptions
Z3Exception

Definition at line 3138 of file Context.java.

3139  {
3140  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3141  }

◆ mkFPRTP()

FPRMNum mkFPRTP ( )
inline

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

Exceptions
Z3Exception

Definition at line 3120 of file Context.java.

3121  {
3122  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3123  }

◆ mkFPRTZ()

FPRMNum mkFPRTZ ( )
inline

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

Exceptions
Z3Exception

Definition at line 3156 of file Context.java.

3157  {
3158  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3159  }

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

3168  {
3169  return new FPSort(this, ebits, sbits);
3170  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8850

◆ mkFPSort128()

FPSort mkFPSort128 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3239 of file Context.java.

3240  {
3241  return new FPSort(this, Native.mkFpaSort128(nCtx()));
3242  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8850

◆ mkFPSort16()

FPSort mkFPSort16 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3185 of file Context.java.

3186  {
3187  return new FPSort(this, Native.mkFpaSort16(nCtx()));
3188  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8850

◆ mkFPSort32()

FPSort mkFPSort32 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3203 of file Context.java.

3204  {
3205  return new FPSort(this, Native.mkFpaSort32(nCtx()));
3206  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8850

◆ mkFPSort64()

FPSort mkFPSort64 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3221 of file Context.java.

3222  {
3223  return new FPSort(this, Native.mkFpaSort64(nCtx()));
3224  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8850

◆ mkFPSortDouble()

FPSort mkFPSortDouble ( )
inline

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

Exceptions
Z3Exception

Definition at line 3212 of file Context.java.

3213  {
3214  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3215  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8850

◆ mkFPSortHalf()

FPSort mkFPSortHalf ( )
inline

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

Exceptions
Z3Exception

Definition at line 3176 of file Context.java.

3177  {
3178  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3179  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8850

◆ mkFPSortQuadruple()

FPSort mkFPSortQuadruple ( )
inline

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

Exceptions
Z3Exception

Definition at line 3230 of file Context.java.

3231  {
3232  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3233  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8850

◆ mkFPSortSingle()

FPSort mkFPSortSingle ( )
inline

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

Exceptions
Z3Exception

Definition at line 3194 of file Context.java.

3195  {
3196  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3197  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8850

◆ mkFPSqrt()

FPExpr mkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term
Exceptions
Z3Exception

Definition at line 3486 of file Context.java.

3487  {
3488  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3489  }

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

3437  {
3438  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3439  }

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

3778  {
3779  if (signed)
3780  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3781  else
3782  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3783  }

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

3693  {
3694  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3695  }

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

3709  {
3710  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3711  }

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

3725  {
3726  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3727  }

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

3743  {
3744  if (signed)
3745  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3746  else
3747  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3748  }

◆ mkFPToFP() [5/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 3760 of file Context.java.

3761  {
3762  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3763  }

◆ mkFPToFP() [6/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 3827 of file Context.java.

3828  {
3829  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3830  }

◆ 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 represenatation of that NaN.
Exceptions
Z3Exception

Definition at line 3809 of file Context.java.

3810  {
3811  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3812  }

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

3795  {
3796  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3797  }

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

3273  {
3274  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3275  }

◆ mkFreshConst()

Expr mkFreshConst ( String  prefix,
Sort  range 
)
inline

Creates a fresh Constant of sort

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

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

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

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

◆ mkFuncDecl() [2/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  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813

◆ mkFuncDecl() [3/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  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
IntSymbol mkSymbol(int i)
Definition: Context.java:93

◆ mkFuncDecl() [4/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  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
IntSymbol mkSymbol(int i)
Definition: Context.java:93

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

2600  {
2601  return new Goal(this, models, unsatCores, proofs);
2602  }

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

2048  {
2049  checkContextMatch(s, substr, offset);
2050  return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
2051  }

◆ mkInRe()

BoolExpr mkInRe ( SeqExpr  s,
ReExpr  re 
)
inline

Check for regular expression membership.

Definition at line 2075 of file Context.java.

2076  {
2077  checkContextMatch(s, re);
2078  return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
2079  }

◆ mkInt() [1/3]

IntNum mkInt ( String  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 2330 of file Context.java.

2331  {
2332 
2333  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2334  .getNativeObject()));
2335  }

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

2344  {
2345 
2346  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2347  .getNativeObject()));
2348  }

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

2357  {
2358 
2359  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2360  .getNativeObject()));
2361  }

◆ 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 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 ( Symbol  name)
inline

Creates an integer constant.

Definition at line 619 of file Context.java.

620  {
621  return (IntExpr) mkConst(name, getIntSort());
622  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

◆ mkIntConst() [2/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  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

◆ mkIntersect()

ReExpr mkIntersect ( ReExpr...  t)
inline

Create the intersection of regular languages.

Definition at line 2156 of file Context.java.

2157  {
2158  checkContextMatch(t);
2159  return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
2160  }

◆ mkIntSort()

IntSort mkIntSort ( )
inline

Create a new integer sort.

Definition at line 196 of file Context.java.

197  {
198  return new IntSort(this);
199  }
def IntSort(ctx=None)
Definition: z3py.py:2746

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

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

1994  {
1995  checkContextMatch(s);
1996  return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
1997  }

◆ mkListSort() [1/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  }

◆ mkListSort() [2/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  }
IntSymbol mkSymbol(int i)
Definition: Context.java:93

◆ mkLoop() [1/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 2093 of file Context.java.

2094  {
2095  return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
2096  }

◆ mkLoop() [2/2]

ReExpr mkLoop ( ReExpr  re,
int  lo 
)
inline

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

Definition at line 2101 of file Context.java.

2102  {
2103  return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
2104  }

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

Referenced by Context.mkBV().

2230  {
2231  checkContextMatch(ty);
2232  return Expr.create(this,
2233  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
2234  }

◆ mkNumeral() [2/3]

Expr mkNumeral ( int  v,
Sort  ty 
)
inline

Create a Term of a given sort. This function can be use 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 2246 of file Context.java.

2247  {
2248  checkContextMatch(ty);
2249  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
2250  }

◆ mkNumeral() [3/3]

Expr mkNumeral ( long  v,
Sort  ty 
)
inline

Create a Term of a given sort. This function can be use 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 2262 of file Context.java.

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

◆ mkOptimize()

Optimize mkOptimize ( )
inline

Create a Optimize context.

Definition at line 3056 of file Context.java.

3057  {
3058  return new Optimize(this);
3059  }

◆ mkOption()

ReExpr mkOption ( ReExpr  re)
inline

Create the optional regular expression.

Definition at line 2119 of file Context.java.

2120  {
2121  checkContextMatch(re);
2122  return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
2123  }

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

2608  {
2609  return new Params(this);
2610  }

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

2212  {
2213  checkContextMatch(args);
2214  return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2215  }

◆ mkPBGe()

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

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

Definition at line 2202 of file Context.java.

2203  {
2204  checkContextMatch(args);
2205  return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2206  }

◆ mkPBLe()

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

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

Definition at line 2193 of file Context.java.

2194  {
2195  checkContextMatch(args);
2196  return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2197  }

◆ mkPlus()

ReExpr mkPlus ( ReExpr  re)
inline

Take the Kleene plus of a regular expression.

Definition at line 2110 of file Context.java.

2111  {
2112  checkContextMatch(re);
2113  return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
2114  }

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

2003  {
2004  checkContextMatch(s1, s2);
2005  return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2006  }

◆ mkProbe()

Probe mkProbe ( String  name)
inline

Creates a new Probe.

Definition at line 2880 of file Context.java.

2881  {
2882  return new Probe(this, name);
2883  }

◆ mkQuantifier() [1/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 2470 of file Context.java.

2474  {
2475 
2476  if (universal)
2477  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2478  quantifierID, skolemID);
2479  else
2480  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2481  quantifierID, skolemID);
2482  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2444
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2418

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

2491  {
2492 
2493  if (universal)
2494  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2495  quantifierID, skolemID);
2496  else
2497  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2498  quantifierID, skolemID);
2499  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2444
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2418

◆ mkRange()

ReExpr mkRange ( SeqExpr  lo,
SeqExpr  hi 
)
inline

Create a range expression.

Definition at line 2165 of file Context.java.

2166  {
2167  checkContextMatch(lo, hi);
2168  return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
2169  }

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

2279  {
2280  if (den == 0) {
2281  throw new Z3Exception("Denominator is zero");
2282  }
2283 
2284  return new RatNum(this, Native.mkReal(nCtx(), num, den));
2285  }

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

2294  {
2295 
2296  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2297  .getNativeObject()));
2298  }

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

2307  {
2308 
2309  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2310  .getNativeObject()));
2311  }

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

2320  {
2321 
2322  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2323  .getNativeObject()));
2324  }

◆ 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 ( Symbol  name)
inline

Creates a real constant.

Definition at line 635 of file Context.java.

636  {
637  return (RealExpr) mkConst(name, getRealSort());
638  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

◆ mkRealConst() [2/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  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560

◆ mkRealSort()

RealSort mkRealSort ( )
inline

Create a real sort.

Definition at line 204 of file Context.java.

205  {
206  return new RealSort(this);
207  }
def RealSort(ctx=None)
Definition: z3py.py:2762

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

2057  {
2058  checkContextMatch(s, src, dst);
2059  return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
2060  }

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

◆ 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

.

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

.

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:9652

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

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

3028  {
3029  return new Solver(this, Native.mkSimpleSolver(nCtx()));
3030  }

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

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

2994  {
2995  return mkSolver((Symbol) null);
2996  }

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

3006  {
3007 
3008  if (logic == null)
3009  return new Solver(this, Native.mkSolver(nCtx()));
3010  else
3011  return new Solver(this, Native.mkSolverForLogic(nCtx(),
3012  logic.getNativeObject()));
3013  }

◆ mkSolver() [3/4]

Solver mkSolver ( String  logic)
inline

Creates a new (incremental) solver.

See also
mkSolver(Symbol)

Definition at line 3019 of file Context.java.

3020  {
3021  return mkSolver(mkSymbol(logic));
3022  }
IntSymbol mkSymbol(int i)
Definition: Context.java:93

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

3039  {
3040 
3041  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3042  t.getNativeObject()));
3043  }

◆ mkStar()

ReExpr mkStar ( ReExpr  re)
inline

Take the Kleene star of a regular expression.

Definition at line 2084 of file Context.java.

2085  {
2086  checkContextMatch(re);
2087  return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
2088  }

◆ 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

) on all indices except for

i

, where it maps to

v

(and the

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

) on all indices except for

args

, where it maps to

v

(and the

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.

Referenced by Context.getStringSort().

242  {
243  return new SeqSort(this, Native.mkStringSort(nCtx()));
244  }
def SeqSort(s)
Definition: z3py.py:9652

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

2012  {
2013  checkContextMatch(s1, s2);
2014  return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2015  }

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

Referenced by Params.add(), 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().

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

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

Referenced by Goal.simplify().

2646  {
2647  return new Tactic(this, name);
2648  }

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

2066  {
2067  checkContextMatch(s);
2068  return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
2069  }

◆ mkTrue()

BoolExpr mkTrue ( )
inline

The true Term.

Definition at line 677 of file Context.java.

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

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

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

◆ 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 ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 179 of file Context.java.

Referenced by Context.mkUninterpretedSort().

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

◆ mkUninterpretedSort() [2/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
IntSymbol mkSymbol(int i)
Definition: Context.java:93

◆ mkUnion()

ReExpr mkUnion ( ReExpr...  t)
inline

Create the union of regular languages.

Definition at line 2147 of file Context.java.

2148  {
2149  checkContextMatch(t);
2150  return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2151  }

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

2981  {
2982  checkContextMatch(p);
2983  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2984  }

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

2970  {
2971  checkContextMatch(p1);
2972  checkContextMatch(p2);
2973  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
2974  p2.getNativeObject()));
2975  }

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

2697  {
2698  checkContextMatch(t1);
2699  checkContextMatch(t2);
2700  return new Tactic(this, Native.tacticOrElse(nCtx(),
2701  t1.getNativeObject(), t2.getNativeObject()));
2702  }

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

2830  {
2831  checkContextMatch(t1);
2832  checkContextMatch(t2);
2833  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2834  t1.getNativeObject(), t2.getNativeObject()));
2835  }

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

2819  {
2820  checkContextMatch(t);
2821  return new Tactic(this, Native.tacticParOr(nCtx(),
2822  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2823  }

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

2574  {
2575  int csn = Symbol.arrayLength(sortNames);
2576  int cs = Sort.arrayLength(sorts);
2577  int cdn = Symbol.arrayLength(declNames);
2578  int cd = AST.arrayLength(decls);
2579  if (csn != cs || cdn != cd)
2580  throw new Z3Exception("Argument size mismatch");
2581  return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
2582  fileName, AST.arrayLength(sorts),
2583  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2584  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2585  AST.arrayToNative(decls)));
2586  }

◆ 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 in the scope (up to push/pop) at the end of the string.

Definition at line 2549 of file Context.java.

2552  {
2553 
2554  int csn = Symbol.arrayLength(sortNames);
2555  int cs = Sort.arrayLength(sorts);
2556  int cdn = Symbol.arrayLength(declNames);
2557  int cd = AST.arrayLength(decls);
2558  if (csn != cs || cdn != cd) {
2559  throw new Z3Exception("Argument size mismatch");
2560  }
2561  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2562  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2563  AST.arrayToNative(sorts), AST.arrayLength(decls),
2564  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2565  }

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

2750  {
2751  checkContextMatch(t);
2752  return new Tactic(this, Native.tacticRepeat(nCtx(),
2753  t.getNativeObject(), max));
2754  }

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

2516  {
2517  Native.setAstPrintMode(nCtx(), value.toInt());
2518  }

◆ SimplifyHelp()

String SimplifyHelp ( )
inline

Return a string describing all available parameters to

Expr.Simplify

.

Definition at line 3869 of file Context.java.

3870  {
3871  return Native.simplifyGetHelp(nCtx());
3872  }

◆ skip()

Tactic skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 2759 of file Context.java.

2760  {
2761  return new Tactic(this, Native.tacticSkip(nCtx()));
2762  }

◆ then()

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

Create a tactic that applies

t1

to a Goal and then

t2

to every subgoal produced by

t1

Remarks: Shorthand for

.

Definition at line 2686 of file Context.java.

2687  {
2688  return andThen(t1, t2, ts);
2689  }
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2654

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

2711  {
2712  checkContextMatch(t);
2713  return new Tactic(this, Native.tacticTryFor(nCtx(),
2714  t.getNativeObject(), ms));
2715  }

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

3861  {
3862  return a.getNativeObject();
3863  }

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

3891  {
3892  Native.updateParamValue(nCtx(), id, value);
3893  }

◆ usingParams()

Tactic usingParams ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

.

Definition at line 2796 of file Context.java.

Referenced by Context.with().

2797  {
2798  checkContextMatch(t);
2799  checkContextMatch(p);
2800  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2801  t.getNativeObject(), p.getNativeObject()));
2802  }

◆ when()

Tactic when ( Probe  p,
Tactic  t 
)
inline

Create a tactic that applies

t

to a given goal if the probe

p

evaluates to true. Remarks: If

p

evaluates to false, then the new tactic behaves like the

tactic.

Definition at line 2723 of file Context.java.

2724  {
2725  checkContextMatch(t);
2726  checkContextMatch(p);
2727  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2728  t.getNativeObject()));
2729  }

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

2811  {
2812  return usingParams(t, p);
2813  }
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2796

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

3844  {
3845  return AST.create(this, nativeObject);
3846  }