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)
 
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)
 
ArrayExpr mkStore (ArrayExpr a, Expr i, 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 MPlus (ReExpr re)
 
ReExpr MOption (ReExpr re)
 
ReExpr MkConcat (ReExpr... t)
 
ReExpr MkUnion (ReExpr... t)
 
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)
 
void parseSMTLIBString (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
 
void parseSMTLIBFile (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
 
int getNumSMTLIBFormulas ()
 
BoolExpr [] getSMTLIBFormulas ()
 
int getNumSMTLIBAssumptions ()
 
BoolExpr [] getSMTLIBAssumptions ()
 
int getNumSMTLIBDecls ()
 
FuncDecl [] getSMTLIBDecls ()
 
int getNumSMTLIBSorts ()
 
Sort [] getSMTLIBSorts ()
 
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.

Definition at line 29 of file Context.java.

Constructor & Destructor Documentation

§ Context() [1/3]

Context ( )
inline

Definition at line 33 of file Context.java.

33  {
34  m_ctx = Native.mkContextRc(0);
35  init();
36  }

§ Context() [2/3]

Context ( long  m_ctx)
inlineprotected

Definition at line 38 of file Context.java.

38  {
39  this.m_ctx = m_ctx;
40  init();
41  }

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

61  {
62  long cfg = Native.mkConfig();
63  for (Map.Entry<String, String> kv : settings.entrySet()) {
64  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
65  }
66  m_ctx = Native.mkContextRc(cfg);
67  Native.delConfig(cfg);
68  init();
69  }
def Map(f, args)
Definition: z3py.py:4207
def String(name, ctx=None)
Definition: z3py.py:9443

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

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

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

Referenced by Context.then().

2634  {
2635  checkContextMatch(t1);
2636  checkContextMatch(t2);
2637  checkContextMatch(ts);
2638 
2639  long last = 0;
2640  if (ts != null && ts.length > 0)
2641  {
2642  last = ts[ts.length - 1].getNativeObject();
2643  for (int i = ts.length - 2; i >= 0; i--) {
2644  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2645  last);
2646  }
2647  }
2648  if (last != 0)
2649  {
2650  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2651  return new Tactic(this, Native.tacticAndThen(nCtx(),
2652  t1.getNativeObject(), last));
2653  } else
2654  return new Tactic(this, Native.tacticAndThen(nCtx(),
2655  t1.getNativeObject(), t2.getNativeObject()));
2656  }

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

2375  {
2376 
2377  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2378  attributes, assumptions.length,
2379  AST.arrayToNative(assumptions), formula.getNativeObject());
2380  }

§ close()

void close ( )
inline

Disposes of the context.

Definition at line 4018 of file Context.java.

4019  {
4020  m_AST_DRQ.forceClear(this);
4021  m_ASTMap_DRQ.forceClear(this);
4022  m_ASTVector_DRQ.forceClear(this);
4023  m_ApplyResult_DRQ.forceClear(this);
4024  m_FuncEntry_DRQ.forceClear(this);
4025  m_FuncInterp_DRQ.forceClear(this);
4026  m_Goal_DRQ.forceClear(this);
4027  m_Model_DRQ.forceClear(this);
4028  m_Params_DRQ.forceClear(this);
4029  m_Probe_DRQ.forceClear(this);
4030  m_Solver_DRQ.forceClear(this);
4031  m_Optimize_DRQ.forceClear(this);
4032  m_Statistics_DRQ.forceClear(this);
4033  m_Tactic_DRQ.forceClear(this);
4034  m_Fixedpoint_DRQ.forceClear(this);
4035 
4036  m_boolSort = null;
4037  m_intSort = null;
4038  m_realSort = null;
4039  m_stringSort = null;
4040 
4041  Native.delContext(m_ctx);
4042  }

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

2715  {
2716  checkContextMatch(p);
2717  checkContextMatch(t1);
2718  checkContextMatch(t2);
2719  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2720  t1.getNativeObject(), t2.getNativeObject()));
2721  }

§ constProbe()

Probe constProbe ( double  val)
inline

Create a probe that always evaluates to

val

.

Definition at line 2866 of file Context.java.

2867  {
2868  return new Probe(this, Native.probeConst(nCtx(), val));
2869  }

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

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

2926  {
2927  checkContextMatch(p1);
2928  checkContextMatch(p2);
2929  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2930  p2.getNativeObject()));
2931  }

§ fail()

Tactic fail ( )
inline

Create a tactic always fails.

Definition at line 2745 of file Context.java.

2746  {
2747  return new Tactic(this, Native.tacticFail(nCtx()));
2748  }

§ failIf()

Tactic failIf ( Probe  p)
inline

Create a tactic that fails if the probe

p

evaluates to false.

Definition at line 2754 of file Context.java.

2755  {
2756  checkContextMatch(p);
2757  return new Tactic(this,
2758  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2759  }

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

2766  {
2767  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2768  }

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

2914  {
2915  checkContextMatch(p1);
2916  checkContextMatch(p2);
2917  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2918  p2.getNativeObject()));
2919  }

§ getApplyResultDRQ()

IDecRefQueue<ApplyResult> getApplyResultDRQ ( )
inline

Definition at line 3949 of file Context.java.

Referenced by ApplyResult.toString().

3950  {
3951  return m_ApplyResult_DRQ;
3952  }

§ getASTDRQ()

IDecRefQueue<AST> getASTDRQ ( )
inline

Definition at line 3934 of file Context.java.

Referenced by AST.getSExpr().

3935  {
3936  return m_AST_DRQ;
3937  }

§ getASTMapDRQ()

IDecRefQueue<ASTMap> getASTMapDRQ ( )
inline

Definition at line 3939 of file Context.java.

3940  {
3941  return m_ASTMap_DRQ;
3942  }

§ getASTVectorDRQ()

IDecRefQueue<ASTVector> getASTVectorDRQ ( )
inline

Definition at line 3944 of file Context.java.

Referenced by ASTVector.toString().

3945  {
3946  return m_ASTVector_DRQ;
3947  }

§ getBoolSort()

BoolSort getBoolSort ( )
inline

Retrieves the Boolean sort of the context.

Definition at line 115 of file Context.java.

Referenced by Context.mkBoolConst().

116  {
117  if (m_boolSort == null) {
118  m_boolSort = new BoolSort(this);
119  }
120  return m_boolSort;
121  }
def BoolSort(ctx=None)
Definition: z3py.py:1407

§ getConstructorDRQ()

IDecRefQueue<Constructor> getConstructorDRQ ( )
inline

Definition at line 3926 of file Context.java.

Referenced by Constructor.getAccessorDecls().

3926  {
3927  return m_Constructor_DRQ;
3928  }

§ getConstructorListDRQ()

IDecRefQueue<ConstructorList> getConstructorListDRQ ( )
inline

Definition at line 3930 of file Context.java.

3930  {
3931  return m_ConstructorList_DRQ;
3932  }

§ getFixedpointDRQ()

IDecRefQueue<Fixedpoint> getFixedpointDRQ ( )
inline

Definition at line 4004 of file Context.java.

Referenced by Fixedpoint.ParseString().

4005  {
4006  return m_Fixedpoint_DRQ;
4007  }

§ getFuncEntryDRQ()

IDecRefQueue<FuncInterp.Entry> getFuncEntryDRQ ( )
inline

Definition at line 3954 of file Context.java.

3955  {
3956  return m_FuncEntry_DRQ;
3957  }

§ getFuncInterpDRQ()

IDecRefQueue<FuncInterp> getFuncInterpDRQ ( )
inline

Definition at line 3959 of file Context.java.

Referenced by FuncInterp.toString().

3960  {
3961  return m_FuncInterp_DRQ;
3962  }

§ getGoalDRQ()

IDecRefQueue<Goal> getGoalDRQ ( )
inline

Definition at line 3964 of file Context.java.

Referenced by Goal.AsBoolExpr().

3965  {
3966  return m_Goal_DRQ;
3967  }

§ getIntSort()

IntSort getIntSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 126 of file Context.java.

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

127  {
128  if (m_intSort == null) {
129  m_intSort = new IntSort(this);
130  }
131  return m_intSort;
132  }
def IntSort(ctx=None)
Definition: z3py.py:2705

§ getModelDRQ()

IDecRefQueue<Model> getModelDRQ ( )
inline

Definition at line 3969 of file Context.java.

Referenced by Model.toString().

3970  {
3971  return m_Model_DRQ;
3972  }

§ getNumProbes()

int getNumProbes ( )
inline

The number of supported Probes.

Definition at line 2828 of file Context.java.

Referenced by Context.getProbeNames().

2829  {
2830  return Native.getNumProbes(nCtx());
2831  }

§ getNumSMTLIBAssumptions()

int getNumSMTLIBAssumptions ( )
inline

The number of SMTLIB assumptions parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2454 of file Context.java.

Referenced by Context.getSMTLIBAssumptions().

2455  {
2456  return Native.getSmtlibNumAssumptions(nCtx());
2457  }

§ getNumSMTLIBDecls()

int getNumSMTLIBDecls ( )
inline

The number of SMTLIB declarations parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2478 of file Context.java.

Referenced by Context.getSMTLIBDecls().

2479  {
2480  return Native.getSmtlibNumDecls(nCtx());
2481  }

§ getNumSMTLIBFormulas()

int getNumSMTLIBFormulas ( )
inline

The number of SMTLIB formulas parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2430 of file Context.java.

Referenced by Context.getSMTLIBFormulas().

2431  {
2432  return Native.getSmtlibNumFormulas(nCtx());
2433  }

§ getNumSMTLIBSorts()

int getNumSMTLIBSorts ( )
inline

The number of SMTLIB sorts parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2501 of file Context.java.

Referenced by Context.getSMTLIBSorts().

2502  {
2503  return Native.getSmtlibNumSorts(nCtx());
2504  }

§ getNumTactics()

int getNumTactics ( )
inline

The number of supported tactics.

Definition at line 2593 of file Context.java.

Referenced by Context.getTacticNames().

2594  {
2595  return Native.getNumTactics(nCtx());
2596  }

§ getOptimizeDRQ()

IDecRefQueue<Optimize> getOptimizeDRQ ( )
inline

Definition at line 4009 of file Context.java.

4010  {
4011  return m_Optimize_DRQ;
4012  }

§ getParamDescrsDRQ()

IDecRefQueue<ParamDescrs> getParamDescrsDRQ ( )
inline

Definition at line 3979 of file Context.java.

Referenced by ParamDescrs.toString().

3980  {
3981  return m_ParamDescrs_DRQ;
3982  }

§ getParamsDRQ()

IDecRefQueue<Params> getParamsDRQ ( )
inline

Definition at line 3974 of file Context.java.

Referenced by Params.toString().

3975  {
3976  return m_Params_DRQ;
3977  }

§ getProbeDescription()

String getProbeDescription ( String  name)
inline

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

Definition at line 2850 of file Context.java.

2851  {
2852  return Native.probeGetDescr(nCtx(), name);
2853  }

§ getProbeDRQ()

IDecRefQueue<Probe> getProbeDRQ ( )
inline

Definition at line 3984 of file Context.java.

Referenced by Probe.apply().

3985  {
3986  return m_Probe_DRQ;
3987  }

§ getProbeNames()

String [] getProbeNames ( )
inline

The names of all supported Probes.

Definition at line 2836 of file Context.java.

2837  {
2838 
2839  int n = getNumProbes();
2840  String[] res = new String[n];
2841  for (int i = 0; i < n; i++)
2842  res[i] = Native.getProbeName(nCtx(), i);
2843  return res;
2844  }
def String(name, ctx=None)
Definition: z3py.py:9443

§ getRealSort()

RealSort getRealSort ( )
inline

Retrieves the Real sort of the context.

Definition at line 137 of file Context.java.

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

138  {
139  if (m_realSort == null) {
140  m_realSort = new RealSort(this);
141  }
142  return m_realSort;
143  }
def RealSort(ctx=None)
Definition: z3py.py:2721

§ getSimplifyParameterDescriptions()

ParamDescrs getSimplifyParameterDescriptions ( )
inline

Retrieves parameter descriptions for simplifier.

Definition at line 3855 of file Context.java.

3856  {
3857  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3858  }

§ getSMTLIBAssumptions()

BoolExpr [] getSMTLIBAssumptions ( )
inline

The assumptions parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2463 of file Context.java.

2464  {
2465 
2466  int n = getNumSMTLIBAssumptions();
2467  BoolExpr[] res = new BoolExpr[n];
2468  for (int i = 0; i < n; i++)
2469  res[i] = (BoolExpr) Expr.create(this,
2470  Native.getSmtlibAssumption(nCtx(), i));
2471  return res;
2472  }

§ getSMTLIBDecls()

FuncDecl [] getSMTLIBDecls ( )
inline

The declarations parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2487 of file Context.java.

2488  {
2489 
2490  int n = getNumSMTLIBDecls();
2491  FuncDecl[] res = new FuncDecl[n];
2492  for (int i = 0; i < n; i++)
2493  res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
2494  return res;
2495  }

§ getSMTLIBFormulas()

BoolExpr [] getSMTLIBFormulas ( )
inline

The formulas parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2439 of file Context.java.

2440  {
2441 
2442  int n = getNumSMTLIBFormulas();
2443  BoolExpr[] res = new BoolExpr[n];
2444  for (int i = 0; i < n; i++)
2445  res[i] = (BoolExpr) Expr.create(this,
2446  Native.getSmtlibFormula(nCtx(), i));
2447  return res;
2448  }

§ getSMTLIBSorts()

Sort [] getSMTLIBSorts ( )
inline

The declarations parsed by the last call to

ParseSMTLIBString

or

ParseSMTLIBFile

.

Definition at line 2510 of file Context.java.

2511  {
2512 
2513  int n = getNumSMTLIBSorts();
2514  Sort[] res = new Sort[n];
2515  for (int i = 0; i < n; i++)
2516  res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
2517  return res;
2518  }

§ getSolverDRQ()

IDecRefQueue<Solver> getSolverDRQ ( )
inline

Definition at line 3989 of file Context.java.

Referenced by Solver.toString().

3990  {
3991  return m_Solver_DRQ;
3992  }

§ getStatisticsDRQ()

IDecRefQueue<Statistics> getStatisticsDRQ ( )
inline

Definition at line 3994 of file Context.java.

3995  {
3996  return m_Statistics_DRQ;
3997  }

§ getStringSort()

SeqSort getStringSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 156 of file Context.java.

157  {
158  if (m_stringSort == null) {
159  m_stringSort = mkStringSort();
160  }
161  return m_stringSort;
162  }

§ getTacticDescription()

String getTacticDescription ( String  name)
inline

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

Definition at line 2615 of file Context.java.

2616  {
2617  return Native.tacticGetDescr(nCtx(), name);
2618  }

§ getTacticDRQ()

IDecRefQueue<Tactic> getTacticDRQ ( )
inline

Definition at line 3999 of file Context.java.

Referenced by Tactic.getSolver().

4000  {
4001  return m_Tactic_DRQ;
4002  }

§ getTacticNames()

String [] getTacticNames ( )
inline

The names of all supported tactics.

Definition at line 2601 of file Context.java.

2602  {
2603 
2604  int n = getNumTactics();
2605  String[] res = new String[n];
2606  for (int i = 0; i < n; i++)
2607  res[i] = Native.getTacticName(nCtx(), i);
2608  return res;
2609  }
def String(name, ctx=None)
Definition: z3py.py:9443

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

2888  {
2889  checkContextMatch(p1);
2890  checkContextMatch(p2);
2891  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2892  p2.getNativeObject()));
2893  }

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

2821  {
2822  Native.interrupt(nCtx());
2823  }

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

2901  {
2902  checkContextMatch(p1);
2903  checkContextMatch(p2);
2904  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2905  p2.getNativeObject()));
2906  }

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

2876  {
2877  checkContextMatch(p1);
2878  checkContextMatch(p2);
2879  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2880  p2.getNativeObject()));
2881  }

§ mkAdd()

ArithExpr mkAdd ( ArithExpr...  t)
inline

Create an expression representing

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

.

Definition at line 777 of file Context.java.

778  {
779  checkContextMatch(t);
780  return (ArithExpr) Expr.create(this,
781  Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
782  }

§ mkAnd()

BoolExpr mkAnd ( BoolExpr...  t)
inline

Create an expression representing

t[0] and t[1] and ...

.

Definition at line 757 of file Context.java.

Referenced by Goal.AsBoolExpr().

758  {
759  checkContextMatch(t);
760  return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
761  AST.arrayToNative(t)));
762  }

§ mkApp()

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

Create a new function application.

Definition at line 644 of file Context.java.

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

645  {
646  checkContextMatch(f);
647  checkContextMatch(args);
648  return Expr.create(this, f, args);
649  }

§ mkArrayConst() [1/2]

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

Create an array constant.

Definition at line 1632 of file Context.java.

1634  {
1635  return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1636  }
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:208
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

§ mkArrayConst() [2/2]

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

Create an array constant.

Definition at line 1641 of file Context.java.

1643  {
1644  return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1645  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:208
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

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

1751  {
1752  checkContextMatch(arg1);
1753  checkContextMatch(arg2);
1754  return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
1755  }

§ mkArraySort()

ArraySort mkArraySort ( Sort  domain,
Sort  range 
)
inline

Create a new array sort.

Definition at line 208 of file Context.java.

Referenced by Context.mkArrayConst().

209  {
210  checkContextMatch(domain);
211  checkContextMatch(range);
212  return new ArraySort(this, domain, range);
213  }
def ArraySort(d, r)
Definition: z3py.py:4110

§ MkAt()

SeqExpr MkAt ( SeqExpr  s,
IntExpr  index 
)
inline

Retrieve sequence of length one at index.

Definition at line 1959 of file Context.java.

1960  {
1961  checkContextMatch(s, index);
1962  return new SeqExpr(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
1963  }

§ mkBitVecSort()

BitVecSort mkBitVecSort ( int  size)
inline

Create a new bit-vector sort.

Definition at line 200 of file Context.java.

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

201  {
202  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
203  }
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3530

§ mkBool()

BoolExpr mkBool ( boolean  value)
inline

Creates a Boolean value.

Definition at line 670 of file Context.java.

671  {
672  return value ? mkTrue() : mkFalse();
673  }

§ mkBoolConst() [1/2]

BoolExpr mkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 580 of file Context.java.

581  {
582  return (BoolExpr) mkConst(name, getBoolSort());
583  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

§ mkBoolConst() [2/2]

BoolExpr mkBoolConst ( String  name)
inline

Create a Boolean constant.

Definition at line 588 of file Context.java.

589  {
590  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
591  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

§ mkBoolSort()

BoolSort mkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 148 of file Context.java.

149  {
150  return new BoolSort(this);
151  }
def BoolSort(ctx=None)
Definition: z3py.py:1407

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

515  {
516  return Expr.create(this,
517  Native.mkBound(nCtx(), index, ty.getNativeObject()));
518  }

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

2208  {
2209  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2210  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2068
BitVecSort mkBitVecSort(int size)
Definition: Context.java:200

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

2218  {
2219  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2220  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2068
BitVecSort mkBitVecSort(int size)
Definition: Context.java:200

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

2228  {
2229  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2230  }
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2068
BitVecSort mkBitVecSort(int size)
Definition: Context.java:200

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

1513  {
1514  checkContextMatch(t);
1515  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1516  (signed)));
1517  }

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

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

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

1526  {
1527  checkContextMatch(t1);
1528  checkContextMatch(t2);
1529  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1530  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1531  }

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

1540  {
1541  checkContextMatch(t1);
1542  checkContextMatch(t2);
1543  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1544  t1.getNativeObject(), t2.getNativeObject()));
1545  }

§ mkBVAND()

BitVecExpr mkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 986 of file Context.java.

987  {
988  checkContextMatch(t1);
989  checkContextMatch(t2);
990  return new BitVecExpr(this, Native.mkBvand(nCtx(),
991  t1.getNativeObject(), t2.getNativeObject()));
992  }

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

1421  {
1422  checkContextMatch(t1);
1423  checkContextMatch(t2);
1424  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1425  t1.getNativeObject(), t2.getNativeObject()));
1426  }

§ mkBVConst() [1/2]

BitVecExpr mkBVConst ( Symbol  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 628 of file Context.java.

629  {
630  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
631  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:200
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

§ mkBVConst() [2/2]

BitVecExpr mkBVConst ( String  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 636 of file Context.java.

637  {
638  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
639  }
BitVecSort mkBitVecSort(int size)
Definition: Context.java:200
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

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

1401  {
1402  checkContextMatch(t1);
1403  checkContextMatch(t2);
1404  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1405  t1.getNativeObject(), t2.getNativeObject()));
1406  }

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

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

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

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

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

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

§ mkBVNAND()

BitVecExpr mkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1025 of file Context.java.

1026  {
1027  checkContextMatch(t1);
1028  checkContextMatch(t2);
1029  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1030  t1.getNativeObject(), t2.getNativeObject()));
1031  }

§ mkBVNeg()

BitVecExpr mkBVNeg ( BitVecExpr  t)
inline

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

Definition at line 1064 of file Context.java.

1065  {
1066  checkContextMatch(t);
1067  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1068  }

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

1595  {
1596  checkContextMatch(t);
1597  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1598  t.getNativeObject()));
1599  }

§ mkBVNOR()

BitVecExpr mkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1038 of file Context.java.

1039  {
1040  checkContextMatch(t1);
1041  checkContextMatch(t2);
1042  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1043  t1.getNativeObject(), t2.getNativeObject()));
1044  }

§ mkBVNot()

BitVecExpr mkBVNot ( BitVecExpr  t)
inline

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

Definition at line 951 of file Context.java.

952  {
953  checkContextMatch(t);
954  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
955  }

§ mkBVOR()

BitVecExpr mkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 999 of file Context.java.

1000  {
1001  checkContextMatch(t1);
1002  checkContextMatch(t2);
1003  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1004  t2.getNativeObject()));
1005  }

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

963  {
964  checkContextMatch(t);
965  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
966  t.getNativeObject()));
967  }

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

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

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

1434  {
1435  checkContextMatch(t);
1436  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1437  t.getNativeObject()));
1438  }

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

1460  {
1461  checkContextMatch(t1);
1462  checkContextMatch(t2);
1463  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1464  t1.getNativeObject(), t2.getNativeObject()));
1465  }

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

1446  {
1447  checkContextMatch(t);
1448  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1449  t.getNativeObject()));
1450  }

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

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

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

1138  {
1139  checkContextMatch(t1);
1140  checkContextMatch(t2);
1141  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1142  t1.getNativeObject(), t2.getNativeObject()));
1143  }

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

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

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

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

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

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

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

1382  {
1383  checkContextMatch(t1);
1384  checkContextMatch(t2);
1385  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1386  t1.getNativeObject(), t2.getNativeObject()));
1387  }

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

1237  {
1238  checkContextMatch(t1);
1239  checkContextMatch(t2);
1240  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1241  t2.getNativeObject()));
1242  }

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

1211  {
1212  checkContextMatch(t1);
1213  checkContextMatch(t2);
1214  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1215  t2.getNativeObject()));
1216  }

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

1185  {
1186  checkContextMatch(t1);
1187  checkContextMatch(t2);
1188  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1189  t1.getNativeObject(), t2.getNativeObject()));
1190  }

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

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

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

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

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

1554  {
1555  checkContextMatch(t1);
1556  checkContextMatch(t2);
1557  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1558  t1.getNativeObject(), t2.getNativeObject()));
1559  }

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

1568  {
1569  checkContextMatch(t1);
1570  checkContextMatch(t2);
1571  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1572  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1573  }

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

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

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

1250  {
1251  checkContextMatch(t1);
1252  checkContextMatch(t2);
1253  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1254  t2.getNativeObject()));
1255  }

§ mkBVUGT()

BoolExpr mkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1275 of file Context.java.

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

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

1224  {
1225  checkContextMatch(t1);
1226  checkContextMatch(t2);
1227  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1228  t2.getNativeObject()));
1229  }

§ mkBVULT()

BoolExpr mkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1197 of file Context.java.

1198  {
1199  checkContextMatch(t1);
1200  checkContextMatch(t2);
1201  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1202  t2.getNativeObject()));
1203  }

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

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

§ mkBVXNOR()

BitVecExpr mkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1051 of file Context.java.

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

§ mkBVXOR()

BitVecExpr mkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

Definition at line 1012 of file Context.java.

1013  {
1014  checkContextMatch(t1);
1015  checkContextMatch(t2);
1016  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1017  t1.getNativeObject(), t2.getNativeObject()));
1018  }

§ mkConcat()

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

1307  {
1308  checkContextMatch(t1);
1309  checkContextMatch(t2);
1310  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1311  t1.getNativeObject(), t2.getNativeObject()));
1312  }

§ MkConcat() [1/2]

SeqExpr MkConcat ( SeqExpr...  t)
inline

Concatentate sequences.

Definition at line 1913 of file Context.java.

1914  {
1915  checkContextMatch(t);
1916  return new SeqExpr(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
1917  }

§ MkConcat() [2/2]

ReExpr MkConcat ( ReExpr...  t)
inline

Create the concatenation of regular languages.

Definition at line 2041 of file Context.java.

2042  {
2043  checkContextMatch(t);
2044  return new ReExpr(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2045  }

§ mkConst() [1/3]

Expr mkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort

range

and named

name

.

Definition at line 537 of file Context.java.

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

538  {
539  checkContextMatch(name);
540  checkContextMatch(range);
541 
542  return Expr.create(
543  this,
544  Native.mkConst(nCtx(), name.getNativeObject(),
545  range.getNativeObject()));
546  }

§ mkConst() [2/3]

Expr mkConst ( String  name,
Sort  range 
)
inline

Creates a new Constant of sort

range

and named

name

.

Definition at line 552 of file Context.java.

553  {
554  return mkConst(mkSymbol(name), range);
555  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

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

573  {
574  return mkApp(f, (Expr[]) null);
575  }
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:644

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

1705  {
1706  checkContextMatch(domain);
1707  checkContextMatch(v);
1708  return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1709  domain.getNativeObject(), v.getNativeObject()));
1710  }

§ mkConstDecl() [1/2]

FuncDecl mkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 480 of file Context.java.

481  {
482  checkContextMatch(name);
483  checkContextMatch(range);
484  return new FuncDecl(this, name, null, range);
485  }

§ mkConstDecl() [2/2]

FuncDecl mkConstDecl ( String  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 490 of file Context.java.

491  {
492  checkContextMatch(range);
493  return new FuncDecl(this, mkSymbol(name), null, range);
494  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81

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

325  {
326  return of(this, name, recognizer, fieldNames, sorts,
327  sortRefs);
328  }

§ mkConstructor() [2/2]

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

Create a datatype constructor.

Definition at line 333 of file Context.java.

335  {
336  return of(this, mkSymbol(name), mkSymbol(recognizer),
337  mkSymbols(fieldNames), sorts, sortRefs);
338  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81

§ MkContains()

BoolExpr MkContains ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence containment of s2 in s1.

Definition at line 1950 of file Context.java.

1951  {
1952  checkContextMatch(s1, s2);
1953  return new BoolExpr(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
1954  }

§ mkDatatypeSort() [1/2]

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

Create a new datatype sort.

Definition at line 343 of file Context.java.

345  {
346  checkContextMatch(name);
347  checkContextMatch(constructors);
348  return new DatatypeSort(this, name, constructors);
349  }

§ mkDatatypeSort() [2/2]

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

Create a new datatype sort.

Definition at line 354 of file Context.java.

356  {
357  checkContextMatch(constructors);
358  return new DatatypeSort(this, mkSymbol(name), constructors);
359  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81

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

Referenced by Context.mkDatatypeSorts().

368  {
369  checkContextMatch(names);
370  int n = names.length;
371  ConstructorList[] cla = new ConstructorList[n];
372  long[] n_constr = new long[n];
373  for (int i = 0; i < n; i++)
374  {
375  Constructor[] constructor = c[i];
376 
377  checkContextMatch(constructor);
378  cla[i] = new ConstructorList(this, constructor);
379  n_constr[i] = cla[i].getNativeObject();
380  }
381  long[] n_res = new long[n];
382  Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
383  n_constr);
384  DatatypeSort[] res = new DatatypeSort[n];
385  for (int i = 0; i < n; i++)
386  res[i] = new DatatypeSort(this, n_res[i]);
387  return res;
388  }

§ mkDatatypeSorts() [2/2]

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

Create mutually recursive data-types.

Definition at line 393 of file Context.java.

395  {
396  return mkDatatypeSorts(mkSymbols(names), c);
397  }
DatatypeSort [] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:366

§ mkDistinct()

BoolExpr mkDistinct ( Expr...  args)
inline

Creates a

term.

Definition at line 689 of file Context.java.

690  {
691  checkContextMatch(args);
692  return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
693  AST.arrayToNative(args)));
694  }

§ mkDiv()

ArithExpr mkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 / t2

.

Definition at line 817 of file Context.java.

818  {
819  checkContextMatch(t1);
820  checkContextMatch(t2);
821  return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
822  t1.getNativeObject(), t2.getNativeObject()));
823  }

§ MkEmptySeq()

SeqExpr MkEmptySeq ( Sort  s)
inline

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

Definition at line 1887 of file Context.java.

1888  {
1889  checkContextMatch(s);
1890  return new SeqExpr(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
1891  }

§ mkEmptySet()

ArrayExpr mkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 1770 of file Context.java.

1771  {
1772  checkContextMatch(domain);
1773  return (ArrayExpr)Expr.create(this,
1774  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1775  }

§ mkEnumSort() [1/2]

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

Create a new enumeration sort.

Definition at line 256 of file Context.java.

258  {
259  checkContextMatch(name);
260  checkContextMatch(enumNames);
261  return new EnumSort(this, name, enumNames);
262  }
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4574

§ mkEnumSort() [2/2]

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

Create a new enumeration sort.

Definition at line 267 of file Context.java.

269  {
270  return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
271  }
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4574
IntSymbol mkSymbol(int i)
Definition: Context.java:81

§ mkEq()

BoolExpr mkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality

x"/> = <paramref name="y

.

Definition at line 678 of file Context.java.

679  {
680  checkContextMatch(x);
681  checkContextMatch(y);
682  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
683  y.getNativeObject()));
684  }

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

Referenced by Context.mkQuantifier().

2286  {
2287 
2288  return Quantifier.of(this, false, sorts, names, body, weight,
2289  patterns, noPatterns, quantifierID, skolemID);
2290  }

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

2299  {
2300 
2301  return Quantifier.of(this, false, boundConstants, body, weight,
2302  patterns, noPatterns, quantifierID, skolemID);
2303  }

§ mkExtract()

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

1324  {
1325  checkContextMatch(t);
1326  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1327  t.getNativeObject()));
1328  }

§ MkExtract()

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

Extract subsequence.

Definition at line 1968 of file Context.java.

1969  {
1970  checkContextMatch(s, offset, length);
1971  return new SeqExpr(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
1972  }

§ mkFalse()

BoolExpr mkFalse ( )
inline

The false Term.

Definition at line 662 of file Context.java.

Referenced by Context.mkBool().

663  {
664  return new BoolExpr(this, Native.mkFalse(nCtx()));
665  }

§ mkFiniteDomainSort() [1/2]

FiniteDomainSort mkFiniteDomainSort ( Symbol  name,
long  size 
)
inline

Create a new finite domain sort.

Definition at line 295 of file Context.java.

297  {
298  checkContextMatch(name);
299  return new FiniteDomainSort(this, name, size);
300  }
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6563

§ mkFiniteDomainSort() [2/2]

FiniteDomainSort mkFiniteDomainSort ( String  name,
long  size 
)
inline

Create a new finite domain sort.

Definition at line 305 of file Context.java.

307  {
308  return new FiniteDomainSort(this, mkSymbol(name), size);
309  }
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6563
IntSymbol mkSymbol(int i)
Definition: Context.java:81

§ mkFixedpoint()

Fixedpoint mkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3026 of file Context.java.

3027  {
3028  return new Fixedpoint(this);
3029  }

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

Referenced by Context.mkQuantifier().

2260  {
2261 
2262  return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2263  noPatterns, quantifierID, skolemID);
2264  }

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

2273  {
2274 
2275  return Quantifier.of(this, true, boundConstants, body, weight,
2276  patterns, noPatterns, quantifierID, skolemID);
2277  }

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

3321  {
3322  return mkFPNumeral(v, s);
3323  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3261

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

3332  {
3333  return mkFPNumeral(v, s);
3334  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3261

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

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

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

3357  {
3358  return mkFPNumeral(sgn, sig, exp, s);
3359  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3261

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

3370  {
3371  return mkFPNumeral(sgn, sig, exp, s);
3372  }
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3261

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

3655  {
3656  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3657  }

§ mkFPAbs()

FPExpr mkFPAbs ( FPExpr  t)
inline

Floating-point absolute value

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3380 of file Context.java.

3381  {
3382  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3383  }

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

3403  {
3404  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3405  }

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

3439  {
3440  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3441  }

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

3567  {
3568  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3569  }

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

3454  {
3455  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3456  }

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

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

§ mkFPGt()

BoolExpr mkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater 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.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3556  }

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

3240  {
3241  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3242  }

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

3607  {
3608  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3609  }

§ mkFPIsNaN()

BoolExpr mkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3616 of file Context.java.

3617  {
3618  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3619  }

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

3627  {
3628  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3629  }

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

3577  {
3578  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3579  }

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

3637  {
3638  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3639  }

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

3587  {
3588  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3589  }

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

3597  {
3598  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3599  }

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

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

§ mkFPLt()

BoolExpr mkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3531 of file Context.java.

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

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

3510  {
3511  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3512  }

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

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

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

3427  {
3428  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3429  }

§ mkFPNaN()

FPNum mkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3228 of file Context.java.

3229  {
3230  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3231  }

§ mkFPNeg()

FPExpr mkFPNeg ( FPExpr  t)
inline

Floating-point negation

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3390 of file Context.java.

3391  {
3392  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3393  }

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

Referenced by Context.mkFP().

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

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

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

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

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

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

3297  {
3298  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3299  }

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

3310  {
3311  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3312  }

§ mkFPRem()

FPExpr mkFPRem ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3475 of file Context.java.

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

§ mkFPRNA()

FPRMNum mkFPRNA ( )
inline

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

Exceptions
Z3Exception

Definition at line 3080 of file Context.java.

3081  {
3082  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3083  }

§ mkFPRNE()

FPRMNum mkFPRNE ( )
inline

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

Exceptions
Z3Exception

Definition at line 3062 of file Context.java.

3063  {
3064  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3065  }

§ mkFPRoundingModeSort()

FPRMSort mkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Exceptions
Z3Exception

Definition at line 3044 of file Context.java.

3045  {
3046  return new FPRMSort(this);
3047  }

§ mkFPRoundNearestTiesToAway()

FPRMNum mkFPRoundNearestTiesToAway ( )
inline

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

Exceptions
Z3Exception

Definition at line 3071 of file Context.java.

3072  {
3073  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3074  }

§ mkFPRoundNearestTiesToEven()

FPRMExpr mkFPRoundNearestTiesToEven ( )
inline

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

Exceptions
Z3Exception

Definition at line 3053 of file Context.java.

3054  {
3055  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3056  }

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

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

§ mkFPRoundTowardNegative()

FPRMNum mkFPRoundTowardNegative ( )
inline

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

Exceptions
Z3Exception

Definition at line 3107 of file Context.java.

3108  {
3109  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3110  }

§ mkFPRoundTowardPositive()

FPRMNum mkFPRoundTowardPositive ( )
inline

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

Exceptions
Z3Exception

Definition at line 3089 of file Context.java.

3090  {
3091  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3092  }

§ mkFPRoundTowardZero()

FPRMNum mkFPRoundTowardZero ( )
inline

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

Exceptions
Z3Exception

Definition at line 3125 of file Context.java.

3126  {
3127  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3128  }

§ mkFPRTN()

FPRMNum mkFPRTN ( )
inline

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

Exceptions
Z3Exception

Definition at line 3116 of file Context.java.

3117  {
3118  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3119  }

§ mkFPRTP()

FPRMNum mkFPRTP ( )
inline

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

Exceptions
Z3Exception

Definition at line 3098 of file Context.java.

3099  {
3100  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3101  }

§ mkFPRTZ()

FPRMNum mkFPRTZ ( )
inline

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

Exceptions
Z3Exception

Definition at line 3134 of file Context.java.

3135  {
3136  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3137  }

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

3146  {
3147  return new FPSort(this, ebits, sbits);
3148  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ mkFPSort128()

FPSort mkFPSort128 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3217 of file Context.java.

3218  {
3219  return new FPSort(this, Native.mkFpaSort128(nCtx()));
3220  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ mkFPSort16()

FPSort mkFPSort16 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3163 of file Context.java.

3164  {
3165  return new FPSort(this, Native.mkFpaSort16(nCtx()));
3166  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ mkFPSort32()

FPSort mkFPSort32 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3181 of file Context.java.

3182  {
3183  return new FPSort(this, Native.mkFpaSort32(nCtx()));
3184  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ mkFPSort64()

FPSort mkFPSort64 ( )
inline

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

Exceptions
Z3Exception

Definition at line 3199 of file Context.java.

3200  {
3201  return new FPSort(this, Native.mkFpaSort64(nCtx()));
3202  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ mkFPSortDouble()

FPSort mkFPSortDouble ( )
inline

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

Exceptions
Z3Exception

Definition at line 3190 of file Context.java.

3191  {
3192  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3193  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ mkFPSortHalf()

FPSort mkFPSortHalf ( )
inline

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

Exceptions
Z3Exception

Definition at line 3154 of file Context.java.

3155  {
3156  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3157  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ mkFPSortQuadruple()

FPSort mkFPSortQuadruple ( )
inline

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

Exceptions
Z3Exception

Definition at line 3208 of file Context.java.

3209  {
3210  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3211  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ mkFPSortSingle()

FPSort mkFPSortSingle ( )
inline

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

Exceptions
Z3Exception

Definition at line 3172 of file Context.java.

3173  {
3174  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3175  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ mkFPSqrt()

FPExpr mkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term
Exceptions
Z3Exception

Definition at line 3464 of file Context.java.

3465  {
3466  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3467  }

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

3415  {
3416  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3417  }

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

3756  {
3757  if (signed)
3758  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3759  else
3760  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3761  }

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

3671  {
3672  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3673  }

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

3687  {
3688  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3689  }

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

3703  {
3704  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3705  }

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

3721  {
3722  if (signed)
3723  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3724  else
3725  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3726  }

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

3739  {
3740  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3741  }

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

3806  {
3807  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3808  }

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

3788  {
3789  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3790  }

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

3773  {
3774  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3775  }

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

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

§ mkFreshConst()

Expr mkFreshConst ( String  prefix,
Sort  range 
)
inline

Creates a fresh Constant of sort

range

and a name prefixed with

prefix

.

Definition at line 561 of file Context.java.

562  {
563  checkContextMatch(range);
564  return Expr.create(this,
565  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
566  }

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

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

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

471  {
472  checkContextMatch(domain);
473  checkContextMatch(range);
474  return new FuncDecl(this, prefix, domain, range);
475  }

§ mkFullSet()

ArrayExpr mkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 1780 of file Context.java.

1781  {
1782  checkContextMatch(domain);
1783  return (ArrayExpr)Expr.create(this,
1784  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1785  }

§ mkFuncDecl() [1/4]

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

Creates a new function declaration.

Definition at line 418 of file Context.java.

420  {
421  checkContextMatch(name);
422  checkContextMatch(domain);
423  checkContextMatch(range);
424  return new FuncDecl(this, name, domain, range);
425  }

§ mkFuncDecl() [2/4]

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

Creates a new function declaration.

Definition at line 430 of file Context.java.

432  {
433  checkContextMatch(name);
434  checkContextMatch(domain);
435  checkContextMatch(range);
436  Sort[] q = new Sort[] { domain };
437  return new FuncDecl(this, name, q, range);
438  }

§ mkFuncDecl() [3/4]

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

Creates a new function declaration.

Definition at line 443 of file Context.java.

445  {
446  checkContextMatch(domain);
447  checkContextMatch(range);
448  return new FuncDecl(this, mkSymbol(name), domain, range);
449  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81

§ mkFuncDecl() [4/4]

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

Creates a new function declaration.

Definition at line 454 of file Context.java.

456  {
457  checkContextMatch(domain);
458  checkContextMatch(range);
459  Sort[] q = new Sort[] { domain };
460  return new FuncDecl(this, mkSymbol(name), q, range);
461  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81

§ mkGe()

BoolExpr mkGe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &gt;= t2

Definition at line 900 of file Context.java.

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

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

2578  {
2579  return new Goal(this, models, unsatCores, proofs);
2580  }

§ mkGt()

BoolExpr mkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &gt; t2

Definition at line 889 of file Context.java.

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

§ mkIff()

BoolExpr mkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 iff t2

.

Definition at line 724 of file Context.java.

725  {
726  checkContextMatch(t1);
727  checkContextMatch(t2);
728  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
729  t2.getNativeObject()));
730  }

§ mkImplies()

BoolExpr mkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 -> t2

.

Definition at line 735 of file Context.java.

736  {
737  checkContextMatch(t1);
738  checkContextMatch(t2);
739  return new BoolExpr(this, Native.mkImplies(nCtx(),
740  t1.getNativeObject(), t2.getNativeObject()));
741  }

§ MkIndexOf()

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

Extract index of sub-string starting at offset.

Definition at line 1977 of file Context.java.

1978  {
1979  checkContextMatch(s, substr, offset);
1980  return new IntExpr(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
1981  }

§ MkInRe()

BoolExpr MkInRe ( SeqExpr  s,
ReExpr  re 
)
inline

Check for regular expression membership.

Definition at line 2005 of file Context.java.

2006  {
2007  checkContextMatch(s, re);
2008  return new BoolExpr(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
2009  }

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

2170  {
2171 
2172  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2173  .getNativeObject()));
2174  }

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

2183  {
2184 
2185  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2186  .getNativeObject()));
2187  }

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

2196  {
2197 
2198  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2199  .getNativeObject()));
2200  }

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

1492  {
1493  checkContextMatch(t);
1494  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1495  t.getNativeObject()));
1496  }

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

919  {
920  checkContextMatch(t);
921  return new RealExpr(this,
922  Native.mkInt2real(nCtx(), t.getNativeObject()));
923  }

§ mkIntConst() [1/2]

IntExpr mkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 596 of file Context.java.

597  {
598  return (IntExpr) mkConst(name, getIntSort());
599  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

§ mkIntConst() [2/2]

IntExpr mkIntConst ( String  name)
inline

Creates an integer constant.

Definition at line 604 of file Context.java.

605  {
606  return (IntExpr) mkConst(name, getIntSort());
607  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

§ mkIntSort()

IntSort mkIntSort ( )
inline

Create a new integer sort.

Definition at line 184 of file Context.java.

185  {
186  return new IntSort(this);
187  }
def IntSort(ctx=None)
Definition: z3py.py:2705

§ mkIsInteger()

BoolExpr mkIsInteger ( RealExpr  t)
inline

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

Definition at line 940 of file Context.java.

941  {
942  checkContextMatch(t);
943  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
944  }

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

713  {
714  checkContextMatch(t1);
715  checkContextMatch(t2);
716  checkContextMatch(t3);
717  return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
718  t2.getNativeObject(), t3.getNativeObject()));
719  }

§ mkLe()

BoolExpr mkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &lt;= t2

Definition at line 878 of file Context.java.

879  {
880  checkContextMatch(t1);
881  checkContextMatch(t2);
882  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
883  t2.getNativeObject()));
884  }

§ MkLength()

IntExpr MkLength ( SeqExpr  s)
inline

Retrieve the length of a given sequence.

Definition at line 1923 of file Context.java.

1924  {
1925  checkContextMatch(s);
1926  return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
1927  }

§ mkListSort() [1/2]

ListSort mkListSort ( Symbol  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 276 of file Context.java.

277  {
278  checkContextMatch(name);
279  checkContextMatch(elemSort);
280  return new ListSort(this, name, elemSort);
281  }

§ mkListSort() [2/2]

ListSort mkListSort ( String  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 286 of file Context.java.

287  {
288  checkContextMatch(elemSort);
289  return new ListSort(this, mkSymbol(name), elemSort);
290  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81

§ mkLt()

BoolExpr mkLt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 &lt; t2

Definition at line 867 of file Context.java.

868  {
869  checkContextMatch(t1);
870  checkContextMatch(t2);
871  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
872  t2.getNativeObject()));
873  }

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

1726  {
1727  checkContextMatch(f);
1728  checkContextMatch(args);
1729  return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1730  f.getNativeObject(), AST.arrayLength(args),
1731  AST.arrayToNative(args)));
1732  }

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

831  {
832  checkContextMatch(t1);
833  checkContextMatch(t2);
834  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
835  t2.getNativeObject()));
836  }

§ mkMul()

ArithExpr mkMul ( ArithExpr...  t)
inline

Create an expression representing

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

.

Definition at line 787 of file Context.java.

788  {
789  checkContextMatch(t);
790  return (ArithExpr) Expr.create(this,
791  Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
792  }

§ mkNot()

BoolExpr mkNot ( BoolExpr  a)
inline

Mk an expression representing

not(a)

.

Definition at line 699 of file Context.java.

700  {
701  checkContextMatch(a);
702  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
703  }

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

Referenced by Context.mkBV().

2069  {
2070  checkContextMatch(ty);
2071  return Expr.create(this,
2072  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
2073  }

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

2086  {
2087  checkContextMatch(ty);
2088  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
2089  }

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

2102  {
2103  checkContextMatch(ty);
2104  return Expr.create(this,
2105  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
2106  }

§ mkOptimize()

Optimize mkOptimize ( )
inline

Create a Optimize context.

Definition at line 3034 of file Context.java.

3035  {
3036  return new Optimize(this);
3037  }

§ mkOr()

BoolExpr mkOr ( BoolExpr...  t)
inline

Create an expression representing

t[0] or t[1] or ...

.

Definition at line 767 of file Context.java.

768  {
769  checkContextMatch(t);
770  return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
771  AST.arrayToNative(t)));
772  }

§ mkParams()

Params mkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2585 of file Context.java.

2586  {
2587  return new Params(this);
2588  }

§ mkPattern()

Pattern mkPattern ( Expr...  terms)
inline

Create a quantifier pattern.

Definition at line 523 of file Context.java.

524  {
525  if (terms.length == 0)
526  throw new Z3Exception("Cannot create a pattern from zero terms");
527 
528  long[] termsNative = AST.arrayToNative(terms);
529  return new Pattern(this, Native.mkPattern(nCtx(), terms.length,
530  termsNative));
531  }

§ mkPower()

ArithExpr mkPower ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing

t1 ^ t2

.

Definition at line 854 of file Context.java.

855  {
856  checkContextMatch(t1);
857  checkContextMatch(t2);
858  return (ArithExpr) Expr.create(
859  this,
860  Native.mkPower(nCtx(), t1.getNativeObject(),
861  t2.getNativeObject()));
862  }

§ MkPrefixOf()

BoolExpr MkPrefixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence prefix.

Definition at line 1932 of file Context.java.

1933  {
1934  checkContextMatch(s1, s2);
1935  return new BoolExpr(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
1936  }

§ mkProbe()

Probe mkProbe ( String  name)
inline

Creates a new Probe.

Definition at line 2858 of file Context.java.

2859  {
2860  return new Probe(this, name);
2861  }

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

2313  {
2314 
2315  if (universal)
2316  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2317  quantifierID, skolemID);
2318  else
2319  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2320  quantifierID, skolemID);
2321  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2283
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2257

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

2330  {
2331 
2332  if (universal)
2333  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2334  quantifierID, skolemID);
2335  else
2336  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2337  quantifierID, skolemID);
2338  }
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2283
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2257

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

2118  {
2119  if (den == 0) {
2120  throw new Z3Exception("Denominator is zero");
2121  }
2122 
2123  return new RatNum(this, Native.mkReal(nCtx(), num, den));
2124  }

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

2133  {
2134 
2135  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2136  .getNativeObject()));
2137  }

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

2146  {
2147 
2148  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2149  .getNativeObject()));
2150  }

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

2159  {
2160 
2161  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2162  .getNativeObject()));
2163  }

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

932  {
933  checkContextMatch(t);
934  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
935  }

§ mkRealConst() [1/2]

RealExpr mkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 612 of file Context.java.

613  {
614  return (RealExpr) mkConst(name, getRealSort());
615  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

§ mkRealConst() [2/2]

RealExpr mkRealConst ( String  name)
inline

Creates a real constant.

Definition at line 620 of file Context.java.

621  {
622  return (RealExpr) mkConst(name, getRealSort());
623  }
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537

§ mkRealSort()

RealSort mkRealSort ( )
inline

Create a real sort.

Definition at line 192 of file Context.java.

193  {
194  return new RealSort(this);
195  }
def RealSort(ctx=None)
Definition: z3py.py:2721

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

844  {
845  checkContextMatch(t1);
846  checkContextMatch(t2);
847  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
848  t2.getNativeObject()));
849  }

§ mkRepeat()

BitVecExpr mkRepeat ( int  i,
BitVecExpr  t 
)
inline

Bit-vector repetition. Remarks: The argument

t

must have a bit-vector sort.

Definition at line 1363 of file Context.java.

1364  {
1365  checkContextMatch(t);
1366  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1367  t.getNativeObject()));
1368  }

§ MkReplace()

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

Replace the first occurrence of src by dst in s.

Definition at line 1986 of file Context.java.

1987  {
1988  checkContextMatch(s, src, dst);
1989  return new SeqExpr(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
1990  }

§ mkReSort()

ReSort mkReSort ( Sort  s)
inline

Create a new regular expression sort

Definition at line 234 of file Context.java.

235  {
236  return new ReSort(this, Native.mkReSort(nCtx(), s.getNativeObject()));
237  }
def ReSort(s)
Definition: z3py.py:9584

§ mkSelect()

Expr mkSelect ( ArrayExpr  a,
Expr  i 
)
inline

Array read. Remarks: The argument

a

is the array and

i

is the index of the array that gets read.

The node

a

must have an array sort

[domain -> range]

, and

i

must have the sort

domain

. The sort of the result is

range

.

See also
mkArraySort
mkStore

Definition at line 1660 of file Context.java.

1661  {
1662  checkContextMatch(a);
1663  checkContextMatch(i);
1664  return Expr.create(
1665  this,
1666  Native.mkSelect(nCtx(), a.getNativeObject(),
1667  i.getNativeObject()));
1668  }

§ mkSeqSort()

SeqSort mkSeqSort ( Sort  s)
inline

Create a new sequence sort

Definition at line 226 of file Context.java.

227  {
228  return new SeqSort(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
229  }
def SeqSort(s)
Definition: z3py.py:9357

§ mkSetAdd()

ArrayExpr mkSetAdd ( ArrayExpr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 1790 of file Context.java.

1791  {
1792  checkContextMatch(set);
1793  checkContextMatch(element);
1794  return (ArrayExpr)Expr.create(this,
1795  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1796  element.getNativeObject()));
1797  }

§ mkSetComplement()

ArrayExpr mkSetComplement ( ArrayExpr  arg)
inline

Take the complement of a set.

Definition at line 1848 of file Context.java.

1849  {
1850  checkContextMatch(arg);
1851  return (ArrayExpr)Expr.create(this,
1852  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1853  }

§ mkSetDel()

ArrayExpr mkSetDel ( ArrayExpr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 1802 of file Context.java.

1803  {
1804  checkContextMatch(set);
1805  checkContextMatch(element);
1806  return (ArrayExpr)Expr.create(this,
1807  Native.mkSetDel(nCtx(), set.getNativeObject(),
1808  element.getNativeObject()));
1809  }

§ mkSetDifference()

ArrayExpr mkSetDifference ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Take the difference between two sets.

Definition at line 1836 of file Context.java.

1837  {
1838  checkContextMatch(arg1);
1839  checkContextMatch(arg2);
1840  return (ArrayExpr)Expr.create(this,
1841  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1842  arg2.getNativeObject()));
1843  }

§ mkSetIntersection()

ArrayExpr mkSetIntersection ( ArrayExpr...  args)
inline

Take the intersection of a list of sets.

Definition at line 1825 of file Context.java.

1826  {
1827  checkContextMatch(args);
1828  return (ArrayExpr)Expr.create(this,
1829  Native.mkSetIntersect(nCtx(), args.length,
1830  AST.arrayToNative(args)));
1831  }

§ mkSetMembership()

BoolExpr mkSetMembership ( Expr  elem,
ArrayExpr  set 
)
inline

Check for set membership.

Definition at line 1858 of file Context.java.

1859  {
1860  checkContextMatch(elem);
1861  checkContextMatch(set);
1862  return (BoolExpr) Expr.create(this,
1863  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1864  set.getNativeObject()));
1865  }

§ mkSetSort()

SetSort mkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 1761 of file Context.java.

1762  {
1763  checkContextMatch(ty);
1764  return new SetSort(this, ty);
1765  }

§ mkSetSubset()

BoolExpr mkSetSubset ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 1870 of file Context.java.

1871  {
1872  checkContextMatch(arg1);
1873  checkContextMatch(arg2);
1874  return (BoolExpr) Expr.create(this,
1875  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1876  arg2.getNativeObject()));
1877  }

§ mkSetUnion()

ArrayExpr mkSetUnion ( ArrayExpr...  args)
inline

Take the union of a list of sets.

Definition at line 1814 of file Context.java.

1815  {
1816  checkContextMatch(args);
1817  return (ArrayExpr)Expr.create(this,
1818  Native.mkSetUnion(nCtx(), args.length,
1819  AST.arrayToNative(args)));
1820  }

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

1338  {
1339  checkContextMatch(t);
1340  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1341  t.getNativeObject()));
1342  }

§ mkSimpleSolver()

Solver mkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3005 of file Context.java.

3006  {
3007  return new Solver(this, Native.mkSimpleSolver(nCtx()));
3008  }

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

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

2972  {
2973  return mkSolver((Symbol) null);
2974  }

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

2984  {
2985 
2986  if (logic == null)
2987  return new Solver(this, Native.mkSolver(nCtx()));
2988  else
2989  return new Solver(this, Native.mkSolverForLogic(nCtx(),
2990  logic.getNativeObject()));
2991  }

§ mkSolver() [3/4]

Solver mkSolver ( String  logic)
inline

Creates a new (incremental) solver.

See also
mkSolver(Symbol)

Definition at line 2997 of file Context.java.

2998  {
2999  return mkSolver(mkSymbol(logic));
3000  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81

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

3017  {
3018 
3019  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3020  t.getNativeObject()));
3021  }

§ MkStar()

ReExpr MkStar ( ReExpr  re)
inline

Take the Kleene star of a regular expression.

Definition at line 2014 of file Context.java.

2015  {
2016  checkContextMatch(re);
2017  return new ReExpr(this, Native.mkReStar(nCtx(), re.getNativeObject()));
2018  }

§ mkStore()

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

1687  {
1688  checkContextMatch(a);
1689  checkContextMatch(i);
1690  checkContextMatch(v);
1691  return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1692  i.getNativeObject(), v.getNativeObject()));
1693  }

§ MkString()

SeqExpr MkString ( String  s)
inline

Create a string constant.

Definition at line 1905 of file Context.java.

1906  {
1907  return new SeqExpr(this, Native.mkString(nCtx(), s));
1908  }

§ mkStringSort()

SeqSort mkStringSort ( )
inline

Create a new string sort

Definition at line 218 of file Context.java.

Referenced by Context.getStringSort().

219  {
220  return new SeqSort(this, Native.mkStringSort(nCtx()));
221  }
def SeqSort(s)
Definition: z3py.py:9357

§ mkSub()

ArithExpr mkSub ( ArithExpr...  t)
inline

Create an expression representing

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

.

Definition at line 797 of file Context.java.

798  {
799  checkContextMatch(t);
800  return (ArithExpr) Expr.create(this,
801  Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
802  }

§ MkSuffixOf()

BoolExpr MkSuffixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence suffix.

Definition at line 1941 of file Context.java.

1942  {
1943  checkContextMatch(s1, s2);
1944  return new BoolExpr(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
1945  }

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

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

82  {
83  return new IntSymbol(this, i);
84  }

§ mkSymbol() [2/2]

StringSymbol mkSymbol ( String  name)
inline

Create a symbol using a string.

Definition at line 89 of file Context.java.

90  {
91  return new StringSymbol(this, name);
92  }

§ mkTactic()

Tactic mkTactic ( String  name)
inline

Creates a new Tactic.

Definition at line 2623 of file Context.java.

Referenced by Goal.simplify().

2624  {
2625  return new Tactic(this, name);
2626  }

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

1741  {
1742  checkContextMatch(array);
1743  return Expr.create(this,
1744  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1745  }

§ MkToRe()

ReExpr MkToRe ( SeqExpr  s)
inline

Convert a regular expression that accepts sequence s.

Definition at line 1995 of file Context.java.

1996  {
1997  checkContextMatch(s);
1998  return new ReExpr(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
1999  }

§ mkTrue()

BoolExpr mkTrue ( )
inline

The true Term.

Definition at line 654 of file Context.java.

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

655  {
656  return new BoolExpr(this, Native.mkTrue(nCtx()));
657  }

§ mkTupleSort()

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

Create a new tuple sort.

Definition at line 243 of file Context.java.

245  {
246  checkContextMatch(name);
247  checkContextMatch(fieldNames);
248  checkContextMatch(fieldSorts);
249  return new TupleSort(this, name, fieldNames.length, fieldNames,
250  fieldSorts);
251  }

§ mkUnaryMinus()

ArithExpr mkUnaryMinus ( ArithExpr  t)
inline

Create an expression representing

-t

.

Definition at line 807 of file Context.java.

808  {
809  checkContextMatch(t);
810  return (ArithExpr) Expr.create(this,
811  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
812  }

§ mkUninterpretedSort() [1/2]

UninterpretedSort mkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 167 of file Context.java.

Referenced by Context.mkUninterpretedSort().

168  {
169  checkContextMatch(s);
170  return new UninterpretedSort(this, s);
171  }

§ mkUninterpretedSort() [2/2]

UninterpretedSort mkUninterpretedSort ( String  str)
inline

Create a new uninterpreted sort.

Definition at line 176 of file Context.java.

177  {
178  return mkUninterpretedSort(mkSymbol(str));
179  }
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:167
IntSymbol mkSymbol(int i)
Definition: Context.java:81

§ MkUnion()

ReExpr MkUnion ( ReExpr...  t)
inline

Create the union of regular languages.

Definition at line 2050 of file Context.java.

2051  {
2052  checkContextMatch(t);
2053  return new ReExpr(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2054  }

§ MkUnit()

SeqExpr MkUnit ( Expr  elem)
inline

Create the singleton sequence.

Definition at line 1896 of file Context.java.

1897  {
1898  checkContextMatch(elem);
1899  return new SeqExpr(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
1900  }

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

407  {
408  return Expr.create (this,
409  Native.datatypeUpdateField
410  (nCtx(), field.getNativeObject(),
411  t.getNativeObject(), v.getNativeObject()));
412  }

§ mkXor()

BoolExpr mkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing

t1 xor t2

.

Definition at line 746 of file Context.java.

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

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

1352  {
1353  checkContextMatch(t);
1354  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1355  t.getNativeObject()));
1356  }

§ MOption()

ReExpr MOption ( ReExpr  re)
inline

Create the optional regular expression.

Definition at line 2032 of file Context.java.

2033  {
2034  checkContextMatch(re);
2035  return new ReExpr(this, Native.mkReOption(nCtx(), re.getNativeObject()));
2036  }

§ MPlus()

ReExpr MPlus ( ReExpr  re)
inline

Take the Kleene plus of a regular expression.

Definition at line 2023 of file Context.java.

2024  {
2025  checkContextMatch(re);
2026  return new ReExpr(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
2027  }

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

2959  {
2960  checkContextMatch(p);
2961  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2962  }

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

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

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

2675  {
2676  checkContextMatch(t1);
2677  checkContextMatch(t2);
2678  return new Tactic(this, Native.tacticOrElse(nCtx(),
2679  t1.getNativeObject(), t2.getNativeObject()));
2680  }

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

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

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

2797  {
2798  checkContextMatch(t);
2799  return new Tactic(this, Native.tacticParOr(nCtx(),
2800  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2801  }

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

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

§ parseSMTLIB2String()

BoolExpr parseSMTLIB2String ( String  str,
Symbol []  sortNames,
Sort []  sorts,
Symbol []  declNames,
FuncDecl []  decls 
)
inline

Parse the given string using the SMT-LIB2 parser.

See also
parseSMTLIBString
Returns
A conjunction of assertions in the scope (up to push/pop) at the end of the string.

Definition at line 2527 of file Context.java.

2530  {
2531 
2532  int csn = Symbol.arrayLength(sortNames);
2533  int cs = Sort.arrayLength(sorts);
2534  int cdn = Symbol.arrayLength(declNames);
2535  int cd = AST.arrayLength(decls);
2536  if (csn != cs || cdn != cd) {
2537  throw new Z3Exception("Argument size mismatch");
2538  }
2539  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2540  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2541  AST.arrayToNative(sorts), AST.arrayLength(decls),
2542  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2543  }

§ parseSMTLIBFile()

void parseSMTLIBFile ( String  fileName,
Symbol []  sortNames,
Sort []  sorts,
Symbol []  declNames,
FuncDecl []  decls 
)
inline

Parse the given file using the SMT-LIB parser.

See also
parseSMTLIBString

Definition at line 2410 of file Context.java.

2413  {
2414  int csn = Symbol.arrayLength(sortNames);
2415  int cs = Sort.arrayLength(sorts);
2416  int cdn = Symbol.arrayLength(declNames);
2417  int cd = AST.arrayLength(decls);
2418  if (csn != cs || cdn != cd)
2419  throw new Z3Exception("Argument size mismatch");
2420  Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
2421  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2422  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2423  AST.arrayToNative(decls));
2424  }

§ parseSMTLIBString()

void parseSMTLIBString ( String  str,
Symbol []  sortNames,
Sort []  sorts,
Symbol []  declNames,
FuncDecl []  decls 
)
inline

Parse the given string using the SMT-LIB parser. Remarks: The symbol table of the parser can be initialized using the given sorts and declarations. The symbols in the arrays

sortNames

and

declNames

don't need to match the names of the sorts and declarations in the arrays

sorts

and

decls

. This is a useful feature since we can use arbitrary names to reference sorts and declarations.

Definition at line 2391 of file Context.java.

2393  {
2394  int csn = Symbol.arrayLength(sortNames);
2395  int cs = Sort.arrayLength(sorts);
2396  int cdn = Symbol.arrayLength(declNames);
2397  int cd = AST.arrayLength(decls);
2398  if (csn != cs || cdn != cd)
2399  throw new Z3Exception("Argument size mismatch");
2400  Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
2401  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2402  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2403  AST.arrayToNative(decls));
2404  }

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

2728  {
2729  checkContextMatch(t);
2730  return new Tactic(this, Native.tacticRepeat(nCtx(),
2731  t.getNativeObject(), max));
2732  }

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

Referenced by Context.Context().

2355  {
2356  Native.setAstPrintMode(nCtx(), value.toInt());
2357  }

§ SimplifyHelp()

String SimplifyHelp ( )
inline

Return a string describing all available parameters to

Expr.Simplify

.

Definition at line 3847 of file Context.java.

3848  {
3849  return Native.simplifyGetHelp(nCtx());
3850  }

§ skip()

Tactic skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 2737 of file Context.java.

2738  {
2739  return new Tactic(this, Native.tacticSkip(nCtx()));
2740  }

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

2665  {
2666  return andThen(t1, t2, ts);
2667  }
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2632

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

2689  {
2690  checkContextMatch(t);
2691  return new Tactic(this, Native.tacticTryFor(nCtx(),
2692  t.getNativeObject(), ms));
2693  }

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

3839  {
3840  return a.getNativeObject();
3841  }

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

3869  {
3870  Native.updateParamValue(nCtx(), id, value);
3871  }

§ usingParams()

Tactic usingParams ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

.

Definition at line 2774 of file Context.java.

Referenced by Context.with().

2775  {
2776  checkContextMatch(t);
2777  checkContextMatch(p);
2778  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2779  t.getNativeObject(), p.getNativeObject()));
2780  }

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

2702  {
2703  checkContextMatch(t);
2704  checkContextMatch(p);
2705  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2706  t.getNativeObject()));
2707  }

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

2789  {
2790  return usingParams(t, p);
2791  }
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2774

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

3822  {
3823  return AST.create(this, nativeObject);
3824  }