Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | Package Functions | Package Attributes
Context Class Reference
+ Inheritance diagram for Context:

Public Member Functions

 Context () throws Z3Exception
 Context (Map< String, String > settings) throws Z3Exception
IntSymbol mkSymbol (int i) throws Z3Exception
StringSymbol mkSymbol (String name) throws Z3Exception
BoolSort getBoolSort () throws Z3Exception
IntSort getIntSort () throws Z3Exception
RealSort getRealSort () throws Z3Exception
BoolSort mkBoolSort () throws Z3Exception
UninterpretedSort mkUninterpretedSort (Symbol s) throws Z3Exception
UninterpretedSort mkUninterpretedSort (String str) throws Z3Exception
IntSort mkIntSort () throws Z3Exception
RealSort mkRealSort () throws Z3Exception
BitVecSort mkBitVecSort (int size) throws Z3Exception
ArraySort mkArraySort (Sort domain, Sort range) throws Z3Exception
TupleSort mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts) throws Z3Exception
EnumSort mkEnumSort (Symbol name, Symbol...enumNames) throws Z3Exception
EnumSort mkEnumSort (String name, String...enumNames) throws Z3Exception
ListSort mkListSort (Symbol name, Sort elemSort) throws Z3Exception
ListSort mkListSort (String name, Sort elemSort) throws Z3Exception
FiniteDomainSort mkFiniteDomainSort (Symbol name, long size) throws Z3Exception
FiniteDomainSort mkFiniteDomainSort (String name, long size) throws Z3Exception
Constructor mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception
Constructor mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception
DatatypeSort mkDatatypeSort (Symbol name, Constructor[] constructors) throws Z3Exception
DatatypeSort mkDatatypeSort (String name, Constructor[] constructors) throws Z3Exception
DatatypeSort[] mkDatatypeSorts (Symbol[] names, Constructor[][] c) throws Z3Exception
DatatypeSort[] mkDatatypeSorts (String[] names, Constructor[][] c) throws Z3Exception
FuncDecl mkFuncDecl (Symbol name, Sort[] domain, Sort range) throws Z3Exception
FuncDecl mkFuncDecl (Symbol name, Sort domain, Sort range) throws Z3Exception
FuncDecl mkFuncDecl (String name, Sort[] domain, Sort range) throws Z3Exception
FuncDecl mkFuncDecl (String name, Sort domain, Sort range) throws Z3Exception
FuncDecl mkFreshFuncDecl (String prefix, Sort[] domain, Sort range) throws Z3Exception
FuncDecl mkConstDecl (Symbol name, Sort range) throws Z3Exception
FuncDecl mkConstDecl (String name, Sort range) throws Z3Exception
FuncDecl mkFreshConstDecl (String prefix, Sort range) throws Z3Exception
Expr mkBound (int index, Sort ty) throws Z3Exception
Pattern mkPattern (Expr...terms) throws Z3Exception
Expr mkConst (Symbol name, Sort range) throws Z3Exception
Expr mkConst (String name, Sort range) throws Z3Exception
Expr mkFreshConst (String prefix, Sort range) throws Z3Exception
Expr mkConst (FuncDecl f) throws Z3Exception
BoolExpr mkBoolConst (Symbol name) throws Z3Exception
BoolExpr mkBoolConst (String name) throws Z3Exception
IntExpr mkIntConst (Symbol name) throws Z3Exception
IntExpr mkIntConst (String name) throws Z3Exception
RealExpr mkRealConst (Symbol name) throws Z3Exception
RealExpr mkRealConst (String name) throws Z3Exception
BitVecExpr mkBVConst (Symbol name, int size) throws Z3Exception
BitVecExpr mkBVConst (String name, int size) throws Z3Exception
Expr mkApp (FuncDecl f, Expr...args) throws Z3Exception
BoolExpr mkTrue () throws Z3Exception
BoolExpr mkFalse () throws Z3Exception
BoolExpr mkBool (boolean value) throws Z3Exception
BoolExpr mkEq (Expr x, Expr y) throws Z3Exception
BoolExpr mkDistinct (Expr...args) throws Z3Exception
BoolExpr mkNot (BoolExpr a) throws Z3Exception
Expr mkITE (BoolExpr t1, Expr t2, Expr t3) throws Z3Exception
BoolExpr mkIff (BoolExpr t1, BoolExpr t2) throws Z3Exception
BoolExpr mkImplies (BoolExpr t1, BoolExpr t2) throws Z3Exception
BoolExpr mkXor (BoolExpr t1, BoolExpr t2) throws Z3Exception
BoolExpr mkAnd (BoolExpr...t) throws Z3Exception
BoolExpr mkOr (BoolExpr...t) throws Z3Exception
ArithExpr mkAdd (ArithExpr...t) throws Z3Exception
ArithExpr mkMul (ArithExpr...t) throws Z3Exception
ArithExpr mkSub (ArithExpr...t) throws Z3Exception
ArithExpr mkUnaryMinus (ArithExpr t) throws Z3Exception
ArithExpr mkDiv (ArithExpr t1, ArithExpr t2) throws Z3Exception
IntExpr mkMod (IntExpr t1, IntExpr t2) throws Z3Exception
IntExpr mkRem (IntExpr t1, IntExpr t2) throws Z3Exception
ArithExpr mkPower (ArithExpr t1, ArithExpr t2) throws Z3Exception
BoolExpr mkLt (ArithExpr t1, ArithExpr t2) throws Z3Exception
BoolExpr mkLe (ArithExpr t1, ArithExpr t2) throws Z3Exception
BoolExpr mkGt (ArithExpr t1, ArithExpr t2) throws Z3Exception
BoolExpr mkGe (ArithExpr t1, ArithExpr t2) throws Z3Exception
RealExpr mkInt2Real (IntExpr t) throws Z3Exception
IntExpr mkReal2Int (RealExpr t) throws Z3Exception
BoolExpr mkIsInteger (RealExpr t) throws Z3Exception
BitVecExpr mkBVNot (BitVecExpr t) throws Z3Exception
BitVecExpr mkBVRedAND (BitVecExpr t) throws Z3Exception
BitVecExpr mkBVRedOR (BitVecExpr t) throws Z3Exception
BitVecExpr mkBVAND (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVXOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVNAND (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVNOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVXNOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVNeg (BitVecExpr t) throws Z3Exception
BitVecExpr mkBVAdd (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVSub (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVMul (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVUDiv (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVSDiv (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVURem (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVSRem (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVSMod (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVULT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVSLT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVULE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVSLE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVUGE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVSGE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVUGT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVSGT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkConcat (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkExtract (int high, int low, BitVecExpr t) throws Z3Exception
BitVecExpr mkSignExt (int i, BitVecExpr t) throws Z3Exception
BitVecExpr mkZeroExt (int i, BitVecExpr t) throws Z3Exception
BitVecExpr mkRepeat (int i, BitVecExpr t) throws Z3Exception
BitVecExpr mkBVSHL (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVLSHR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVASHR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVRotateLeft (int i, BitVecExpr t) throws Z3Exception
BitVecExpr mkBVRotateRight (int i, BitVecExpr t) throws Z3Exception
BitVecExpr mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkBVRotateRight (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BitVecExpr mkInt2BV (int n, IntExpr t) throws Z3Exception
IntExpr mkBV2Int (BitVecExpr t, boolean signed) throws Z3Exception
BoolExpr mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception
BoolExpr mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception
BoolExpr mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
BoolExpr mkBVNegNoOverflow (BitVecExpr t) throws Z3Exception
BoolExpr mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception
BoolExpr mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception
ArrayExpr mkArrayConst (Symbol name, Sort domain, Sort range) throws Z3Exception
ArrayExpr mkArrayConst (String name, Sort domain, Sort range) throws Z3Exception
Expr mkSelect (ArrayExpr a, Expr i) throws Z3Exception
ArrayExpr mkStore (ArrayExpr a, Expr i, Expr v) throws Z3Exception
ArrayExpr mkConstArray (Sort domain, Expr v) throws Z3Exception
ArrayExpr mkMap (FuncDecl f, ArrayExpr...args) throws Z3Exception
Expr mkTermArray (ArrayExpr array) throws Z3Exception
SetSort mkSetSort (Sort ty) throws Z3Exception
Expr mkEmptySet (Sort domain) throws Z3Exception
Expr mkFullSet (Sort domain) throws Z3Exception
Expr mkSetAdd (Expr set, Expr element) throws Z3Exception
Expr mkSetDel (Expr set, Expr element) throws Z3Exception
Expr mkSetUnion (Expr...args) throws Z3Exception
Expr mkSetIntersection (Expr...args) throws Z3Exception
Expr mkSetDifference (Expr arg1, Expr arg2) throws Z3Exception
Expr mkSetComplement (Expr arg) throws Z3Exception
Expr mkSetMembership (Expr elem, Expr set) throws Z3Exception
Expr mkSetSubset (Expr arg1, Expr arg2) throws Z3Exception
Expr mkNumeral (String v, Sort ty) throws Z3Exception
Expr mkNumeral (int v, Sort ty) throws Z3Exception
Expr mkNumeral (long v, Sort ty) throws Z3Exception
RatNum mkReal (int num, int den) throws Z3Exception
RatNum mkReal (String v) throws Z3Exception
RatNum mkReal (int v) throws Z3Exception
RatNum mkReal (long v) throws Z3Exception
IntNum mkInt (String v) throws Z3Exception
IntNum mkInt (int v) throws Z3Exception
IntNum mkInt (long v) throws Z3Exception
BitVecNum mkBV (String v, int size) throws Z3Exception
BitVecNum mkBV (int v, int size) throws Z3Exception
BitVecNum mkBV (long v, int size) throws Z3Exception
Quantifier mkForall (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
Quantifier mkForall (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
Quantifier mkExists (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
Quantifier mkExists (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
Quantifier mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
Quantifier mkQuantifier (boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception
void setPrintMode (Z3_ast_print_mode value) throws Z3Exception
String benchmarkToSMTString (String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula) throws Z3Exception
void parseSMTLIBString (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception
void parseSMTLIBFile (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception
int getNumSMTLIBFormulas () throws Z3Exception
BoolExpr[] getSMTLIBFormulas () throws Z3Exception
int getNumSMTLIBAssumptions () throws Z3Exception
BoolExpr[] getSMTLIBAssumptions () throws Z3Exception
int getNumSMTLIBDecls () throws Z3Exception
FuncDecl[] getSMTLIBDecls () throws Z3Exception
int getNumSMTLIBSorts () throws Z3Exception
Sort[] getSMTLIBSorts () throws Z3Exception
BoolExpr parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception
BoolExpr parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception
Goal mkGoal (boolean models, boolean unsatCores, boolean proofs) throws Z3Exception
Params mkParams () throws Z3Exception
int getNumTactics () throws Z3Exception
String[] getTacticNames () throws Z3Exception
String getTacticDescription (String name) throws Z3Exception
Tactic mkTactic (String name) throws Z3Exception
Tactic andThen (Tactic t1, Tactic t2, Tactic...ts) throws Z3Exception
Tactic then (Tactic t1, Tactic t2, Tactic...ts) throws Z3Exception
Tactic orElse (Tactic t1, Tactic t2) throws Z3Exception
Tactic tryFor (Tactic t, int ms) throws Z3Exception
Tactic when (Probe p, Tactic t) throws Z3Exception
Tactic cond (Probe p, Tactic t1, Tactic t2) throws Z3Exception
Tactic repeat (Tactic t, int max) throws Z3Exception
Tactic skip () throws Z3Exception
Tactic fail () throws Z3Exception
Tactic failIf (Probe p) throws Z3Exception
Tactic failIfNotDecided () throws Z3Exception
Tactic usingParams (Tactic t, Params p) throws Z3Exception
Tactic with (Tactic t, Params p) throws Z3Exception
Tactic parOr (Tactic...t) throws Z3Exception
Tactic parAndThen (Tactic t1, Tactic t2) throws Z3Exception
void interrupt () throws Z3Exception
int getNumProbes () throws Z3Exception
String[] getProbeNames () throws Z3Exception
String getProbeDescription (String name) throws Z3Exception
Probe mkProbe (String name) throws Z3Exception
Probe constProbe (double val) throws Z3Exception
Probe lt (Probe p1, Probe p2) throws Z3Exception
Probe gt (Probe p1, Probe p2) throws Z3Exception
Probe le (Probe p1, Probe p2) throws Z3Exception
Probe ge (Probe p1, Probe p2) throws Z3Exception
Probe eq (Probe p1, Probe p2) throws Z3Exception
Probe and (Probe p1, Probe p2) throws Z3Exception
Probe or (Probe p1, Probe p2) throws Z3Exception
Probe not (Probe p) throws Z3Exception
Solver mkSolver () throws Z3Exception
Solver mkSolver (Symbol logic) throws Z3Exception
Solver mkSolver (String logic) throws Z3Exception
Solver mkSimpleSolver () throws Z3Exception
Solver mkSolver (Tactic t) throws Z3Exception
Fixedpoint mkFixedpoint () throws Z3Exception
AST wrapAST (long nativeObject) throws Z3Exception
long unwrapAST (AST a)
String SimplifyHelp () throws Z3Exception
ParamDescrs getSimplifyParameterDescriptions () throws Z3Exception
void updateParamValue (String id, String value) throws Z3Exception
void dispose ()

Static Public Member Functions

static void ToggleWarningMessages (boolean enabled) throws Z3Exception

Protected Member Functions

void finalize ()

Protected Attributes

long m_refCount = 0

Package Functions

Symbol[] MkSymbols (String[] names) throws Z3Exception
long nCtx ()
void initContext () throws Z3Exception
void checkContextMatch (Z3Object other) throws Z3Exception
void checkContextMatch (Z3Object[] arr) throws Z3Exception
ASTDecRefQueue ast_DRQ ()
ASTMapDecRefQueue astmap_DRQ ()
ASTVectorDecRefQueue astvector_DRQ ()
ApplyResultDecRefQueue applyResult_DRQ ()
FuncInterpEntryDecRefQueue funcEntry_DRQ ()
FuncInterpDecRefQueue funcInterp_DRQ ()
GoalDecRefQueue goal_DRQ ()
ModelDecRefQueue model_DRQ ()
ParamsDecRefQueue params_DRQ ()
ParamDescrsDecRefQueue paramDescrs_DRQ ()
ProbeDecRefQueue probe_DRQ ()
SolverDecRefQueue solver_DRQ ()
StatisticsDecRefQueue statistics_DRQ ()
TacticDecRefQueue tactic_DRQ ()
FixedpointDecRefQueue fixedpoint_DRQ ()

Package Attributes

long m_ctx = 0

Detailed Description

The main interaction with Z3 happens via the Context.

Definition at line 27 of file Context.java.


Constructor & Destructor Documentation

Context ( ) throws Z3Exception [inline]

Constructor.

Definition at line 32 of file Context.java.

    {
        super();
        m_ctx = Native.mkContextRc(0);
        initContext();
    }
Context ( Map< String, String >  settings) throws Z3Exception [inline]

Constructor.

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

    {
        super();
        long cfg = Native.mkConfig();
        for (Map.Entry<String, String> kv : settings.entrySet())
            Native.setParamValue(cfg, kv.getKey(), kv.getValue());
        m_ctx = Native.mkContextRc(cfg);
        Native.delConfig(cfg);
        initContext();
    }

Member Function Documentation

Probe and ( Probe  p1,
Probe  p2 
) throws Z3Exception [inline]

Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".

Definition at line 2758 of file Context.java.

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }
Tactic andThen ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
) throws Z3Exception [inline]

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

Definition at line 2440 of file Context.java.

Referenced by Context.then().

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        checkContextMatch(ts);

        long last = 0;
        if (ts != null && ts.length > 0)
        {
            last = ts[ts.length - 1].getNativeObject();
            for (int i = ts.length - 2; i >= 0; i--)
                last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
                        last);
        }
        if (last != 0)
        {
            last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
            return new Tactic(this, Native.tacticAndThen(nCtx(),
                    t1.getNativeObject(), last));
        } else
            return new Tactic(this, Native.tacticAndThen(nCtx(),
                    t1.getNativeObject(), t2.getNativeObject()));
    }
ApplyResultDecRefQueue applyResult_DRQ ( ) [inline, package]

Definition at line 2982 of file Context.java.

Referenced by ApplyResult.decRef(), and ApplyResult.incRef().

    {
        return m_ApplyResult_DRQ;
    }
ASTDecRefQueue ast_DRQ ( ) [inline, package]

Definition at line 2967 of file Context.java.

Referenced by AST.decRef(), and AST.incRef().

    {
        return m_AST_DRQ;
    }
ASTMapDecRefQueue astmap_DRQ ( ) [inline, package]

Definition at line 2972 of file Context.java.

Referenced by ASTMap.decRef(), and ASTMap.incRef().

    {
        return m_ASTMap_DRQ;
    }
ASTVectorDecRefQueue astvector_DRQ ( ) [inline, package]

Definition at line 2977 of file Context.java.

Referenced by ASTVector.decRef(), and ASTVector.incRef().

    {
        return m_ASTVector_DRQ;
    }
String benchmarkToSMTString ( String  name,
String  logic,
String  status,
String  attributes,
BoolExpr[]  assumptions,
BoolExpr  formula 
) throws Z3Exception [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 2177 of file Context.java.

    {

        return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
                attributes, (int) assumptions.length,
                AST.arrayToNative(assumptions), formula.getNativeObject());
    }
void checkContextMatch ( Z3Object  other) throws Z3Exception [inline, package]

Definition at line 2938 of file Context.java.

Referenced by Fixedpoint.add(), Goal.add(), Solver.add(), Fixedpoint.addFact(), Fixedpoint.addRule(), Context.and(), Context.andThen(), Probe.apply(), Tactic.apply(), FuncDecl.apply(), Solver.assertAndTrack(), Context.checkContextMatch(), InterpolationContext.ComputeInterpolant(), Context.cond(), Context.eq(), Context.failIf(), Context.ge(), Model.getConstInterp(), Model.getFuncInterp(), InterpolationContext.GetInterpolant(), Context.gt(), Context.le(), Context.lt(), Context.mkAdd(), Context.mkAnd(), Context.mkApp(), Context.mkArraySort(), Context.mkBV2Int(), Context.mkBVAdd(), Context.mkBVAddNoOverflow(), Context.mkBVAddNoUnderflow(), Context.mkBVAND(), Context.mkBVASHR(), Context.mkBVLSHR(), Context.mkBVMul(), Context.mkBVMulNoOverflow(), Context.mkBVMulNoUnderflow(), Context.mkBVNAND(), Context.mkBVNeg(), Context.mkBVNegNoOverflow(), Context.mkBVNOR(), Context.mkBVNot(), Context.mkBVOR(), Context.mkBVRedAND(), Context.mkBVRedOR(), Context.mkBVRotateLeft(), Context.mkBVRotateRight(), Context.mkBVSDiv(), Context.mkBVSDivNoOverflow(), Context.mkBVSGE(), Context.mkBVSGT(), Context.mkBVSHL(), Context.mkBVSLE(), Context.mkBVSLT(), Context.mkBVSMod(), Context.mkBVSRem(), Context.mkBVSub(), Context.mkBVSubNoOverflow(), Context.mkBVSubNoUnderflow(), Context.mkBVUDiv(), Context.mkBVUGE(), Context.mkBVUGT(), Context.mkBVULE(), Context.mkBVULT(), Context.mkBVURem(), Context.mkBVXNOR(), Context.mkBVXOR(), Context.mkConcat(), Context.mkConst(), Context.mkConstArray(), Context.mkConstDecl(), Context.mkDatatypeSort(), Context.mkDatatypeSorts(), Context.mkDistinct(), Context.mkDiv(), Context.mkEmptySet(), Context.mkEnumSort(), Context.mkEq(), Context.mkExtract(), Context.mkFiniteDomainSort(), Context.mkFreshConst(), Context.mkFreshConstDecl(), Context.mkFreshFuncDecl(), Context.mkFullSet(), Context.mkFuncDecl(), Context.mkGe(), Context.mkGt(), Context.mkIff(), Context.mkImplies(), Context.mkInt2BV(), Context.mkInt2Real(), InterpolationContext.MkInterpolant(), Context.mkIsInteger(), Context.mkITE(), Context.mkLe(), Context.mkListSort(), Context.mkLt(), Context.mkMap(), Context.mkMod(), Context.mkMul(), Context.mkNot(), Context.mkNumeral(), Context.mkOr(), Context.mkPower(), Context.mkReal2Int(), Context.mkRem(), Context.mkRepeat(), Context.mkSelect(), Context.mkSetAdd(), Context.mkSetComplement(), Context.mkSetDel(), Context.mkSetDifference(), Context.mkSetIntersection(), Context.mkSetMembership(), Context.mkSetSort(), Context.mkSetSubset(), Context.mkSetUnion(), Context.mkSignExt(), Context.mkStore(), Context.mkSub(), Context.mkTermArray(), Context.mkTupleSort(), Context.mkUnaryMinus(), Context.mkUninterpretedSort(), Context.mkXor(), Context.mkZeroExt(), Context.not(), Context.or(), Context.orElse(), Context.parAndThen(), Context.parOr(), Quantifier.Quantifier(), Fixedpoint.query(), Fixedpoint.registerRelation(), Context.repeat(), Solver.setParameters(), Fixedpoint.setParameters(), Expr.substitute(), Expr.substituteVars(), Context.tryFor(), Expr.update(), Fixedpoint.updateRule(), Context.usingParams(), and Context.when().

    {
        if (this != other.getContext())
            throw new Z3Exception("Context mismatch");
    }
void checkContextMatch ( Z3Object[]  arr) throws Z3Exception [inline, package]

Definition at line 2944 of file Context.java.

    {
        if (arr != null)
            for (Z3Object a : arr)
                checkContextMatch(a);
    }
Tactic cond ( Probe  p,
Tactic  t1,
Tactic  t2 
) throws Z3Exception [inline]

Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise.

Definition at line 2523 of file Context.java.

    {

        checkContextMatch(p);
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
Probe constProbe ( double  val) throws Z3Exception [inline]

Create a probe that always evaluates to val .

Definition at line 2681 of file Context.java.

    {
        return new Probe(this, Native.probeConst(nCtx(), val));
    }
void dispose ( ) [inline]

Disposes of the context.

Reimplemented from IDisposable.

Definition at line 3070 of file Context.java.

Referenced by Context.finalize().

    {
        m_AST_DRQ.clear(this);
        m_ASTMap_DRQ.clear(this);
        m_ASTVector_DRQ.clear(this);
        m_ApplyResult_DRQ.clear(this);
        m_FuncEntry_DRQ.clear(this);
        m_FuncInterp_DRQ.clear(this);
        m_Goal_DRQ.clear(this);
        m_Model_DRQ.clear(this);
        m_Params_DRQ.clear(this);
        m_Probe_DRQ.clear(this);
        m_Solver_DRQ.clear(this);
        m_Statistics_DRQ.clear(this);
        m_Tactic_DRQ.clear(this);
        m_Fixedpoint_DRQ.clear(this);

        m_boolSort = null;
        m_intSort = null;
        m_realSort = null;
    }
Probe eq ( Probe  p1,
Probe  p2 
) throws Z3Exception [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 2746 of file Context.java.

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

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }
Tactic fail ( ) throws Z3Exception [inline]

Create a tactic always fails.

Definition at line 2558 of file Context.java.

    {

        return new Tactic(this, Native.tacticFail(nCtx()));
    }
Tactic failIf ( Probe  p) throws Z3Exception [inline]

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

Definition at line 2568 of file Context.java.

    {

        checkContextMatch(p);
        return new Tactic(this,
                Native.tacticFailIf(nCtx(), p.getNativeObject()));
    }
Tactic failIfNotDecided ( ) throws Z3Exception [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 2580 of file Context.java.

    {
        return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
    }
void finalize ( ) [inline, protected]

Finalizer.

Definition at line 3047 of file Context.java.

    {
        dispose();

        if (m_refCount == 0)
        {
            try
            {
                Native.delContext(m_ctx);
            } catch (Z3Exception e)
            {
                // OK.
            }
            m_ctx = 0;
        } 
        /*
        else
            CMW: re-queue the finalizer? */
    }
FixedpointDecRefQueue fixedpoint_DRQ ( ) [inline, package]

Definition at line 3037 of file Context.java.

Referenced by Fixedpoint.decRef(), and Fixedpoint.incRef().

    {
        return m_Fixedpoint_DRQ;
    }

Definition at line 2987 of file Context.java.

Referenced by FuncInterp.Entry.decRef(), and FuncInterp.Entry.incRef().

    {
        return m_FuncEntry_DRQ;
    }
FuncInterpDecRefQueue funcInterp_DRQ ( ) [inline, package]

Definition at line 2992 of file Context.java.

Referenced by FuncInterp.decRef(), and FuncInterp.incRef().

    {
        return m_FuncInterp_DRQ;
    }
Probe ge ( Probe  p1,
Probe  p2 
) throws Z3Exception [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 2733 of file Context.java.

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }
BoolSort getBoolSort ( ) throws Z3Exception [inline]

Retrieves the Boolean sort of the context.

Definition at line 106 of file Context.java.

Referenced by Context.mkBoolConst().

    {
        if (m_boolSort == null)
            m_boolSort = new BoolSort(this);
        return m_boolSort;
    }
IntSort getIntSort ( ) throws Z3Exception [inline]

Retrieves the Integer sort of the context.

Definition at line 116 of file Context.java.

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

    {
        if (m_intSort == null)
            m_intSort = new IntSort(this);
        return m_intSort;
    }
int getNumProbes ( ) throws Z3Exception [inline]

The number of supported Probes.

Definition at line 2643 of file Context.java.

Referenced by Context.getProbeNames().

    {
        return Native.getNumProbes(nCtx());
    }
int getNumSMTLIBAssumptions ( ) throws Z3Exception [inline]

The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2259 of file Context.java.

Referenced by Context.getSMTLIBAssumptions().

    {
        return Native.getSmtlibNumAssumptions(nCtx());
    }
int getNumSMTLIBDecls ( ) throws Z3Exception [inline]

The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2283 of file Context.java.

Referenced by Context.getSMTLIBDecls().

    {
        return Native.getSmtlibNumDecls(nCtx());
    }
int getNumSMTLIBFormulas ( ) throws Z3Exception [inline]

The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2235 of file Context.java.

Referenced by Context.getSMTLIBFormulas().

    {
        return Native.getSmtlibNumFormulas(nCtx());
    }
int getNumSMTLIBSorts ( ) throws Z3Exception [inline]

The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2306 of file Context.java.

Referenced by Context.getSMTLIBSorts().

    {
        return Native.getSmtlibNumSorts(nCtx());
    }
int getNumTactics ( ) throws Z3Exception [inline]

The number of supported tactics.

Definition at line 2399 of file Context.java.

Referenced by Context.getTacticNames().

    {
        return Native.getNumTactics(nCtx());
    }
String getProbeDescription ( String  name) throws Z3Exception [inline]

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

Definition at line 2665 of file Context.java.

    {
        return Native.probeGetDescr(nCtx(), name);
    }
String [] getProbeNames ( ) throws Z3Exception [inline]

The names of all supported Probes.

Definition at line 2651 of file Context.java.

    {

        int n = getNumProbes();
        String[] res = new String[n];
        for (int i = 0; i < n; i++)
            res[i] = Native.getProbeName(nCtx(), i);
        return res;
    }
RealSort getRealSort ( ) throws Z3Exception [inline]

Retrieves the Real sort of the context.

Definition at line 126 of file Context.java.

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

    {
        if (m_realSort == null)
            m_realSort = new RealSort(this);
        return m_realSort;
    }

Retrieves parameter descriptions for simplifier.

Definition at line 2897 of file Context.java.

    {
        return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
    }
BoolExpr [] getSMTLIBAssumptions ( ) throws Z3Exception [inline]

The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2268 of file Context.java.

    {

        int n = getNumSMTLIBAssumptions();
        BoolExpr[] res = new BoolExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (BoolExpr) Expr.create(this,
                    Native.getSmtlibAssumption(nCtx(), i));
        return res;
    }
FuncDecl [] getSMTLIBDecls ( ) throws Z3Exception [inline]

The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2292 of file Context.java.

    {

        int n = getNumSMTLIBDecls();
        FuncDecl[] res = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
        return res;
    }
BoolExpr [] getSMTLIBFormulas ( ) throws Z3Exception [inline]

The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2244 of file Context.java.

    {

        int n = getNumSMTLIBFormulas();
        BoolExpr[] res = new BoolExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (BoolExpr) Expr.create(this,
                    Native.getSmtlibFormula(nCtx(), i));
        return res;
    }
Sort [] getSMTLIBSorts ( ) throws Z3Exception [inline]

The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 2315 of file Context.java.

    {

        int n = getNumSMTLIBSorts();
        Sort[] res = new Sort[n];
        for (int i = 0; i < n; i++)
            res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
        return res;
    }
String getTacticDescription ( String  name) throws Z3Exception [inline]

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

Definition at line 2421 of file Context.java.

    {

        return Native.tacticGetDescr(nCtx(), name);
    }
String [] getTacticNames ( ) throws Z3Exception [inline]

The names of all supported tactics.

Definition at line 2407 of file Context.java.

    {

        int n = getNumTactics();
        String[] res = new String[n];
        for (int i = 0; i < n; i++)
            res[i] = Native.getTacticName(nCtx(), i);
        return res;
    }
GoalDecRefQueue goal_DRQ ( ) [inline, package]

Definition at line 2997 of file Context.java.

Referenced by Goal.decRef(), and Goal.incRef().

    {
        return m_Goal_DRQ;
    }
Probe gt ( Probe  p1,
Probe  p2 
) throws Z3Exception [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 2705 of file Context.java.

    {

        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }
void initContext ( ) throws Z3Exception [inline, package]

Definition at line 2932 of file Context.java.

Referenced by Context.Context(), and InterpolationContext.InterpolationContext().

    {
        setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
        Native.setInternalErrorHandler(nCtx());
    }
void interrupt ( ) throws Z3Exception [inline]

Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics.

Definition at line 2635 of file Context.java.

    {
        Native.interrupt(nCtx());
    }
Probe le ( Probe  p1,
Probe  p2 
) throws Z3Exception [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 2719 of file Context.java.

    {

        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }
Probe lt ( Probe  p1,
Probe  p2 
) throws Z3Exception [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 2691 of file Context.java.

    {

        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }
ArithExpr mkAdd ( ArithExpr...  t) throws Z3Exception [inline]

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

Definition at line 763 of file Context.java.

    {

        checkContextMatch(t);
        return (ArithExpr) Expr.create(this,
                Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t)));
    }
BoolExpr mkAnd ( BoolExpr...  t) throws Z3Exception [inline]

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

Definition at line 741 of file Context.java.

    {

        checkContextMatch(t);
        return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length,
                AST.arrayToNative(t)));
    }
Expr mkApp ( FuncDecl  f,
Expr...  args 
) throws Z3Exception [inline]

Create a new function application.

Definition at line 624 of file Context.java.

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

    {
        checkContextMatch(f);
        checkContextMatch(args);
        return Expr.create(this, f, args);
    }
ArrayExpr mkArrayConst ( Symbol  name,
Sort  domain,
Sort  range 
) throws Z3Exception [inline]

Create an array constant.

Definition at line 1633 of file Context.java.

    {

        return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
    }
ArrayExpr mkArrayConst ( String  name,
Sort  domain,
Sort  range 
) throws Z3Exception [inline]

Create an array constant.

Definition at line 1643 of file Context.java.

    {

        return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
    }
ArraySort mkArraySort ( Sort  domain,
Sort  range 
) throws Z3Exception [inline]

Create a new array sort.

Definition at line 191 of file Context.java.

Referenced by Context.mkArrayConst().

    {

        checkContextMatch(domain);
        checkContextMatch(range);
        return new ArraySort(this, domain, range);
    }
BitVecSort mkBitVecSort ( int  size) throws Z3Exception [inline]

Create a new bit-vector sort.

Definition at line 182 of file Context.java.

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

    {

        return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
    }
BoolExpr mkBool ( boolean  value) throws Z3Exception [inline]

Creates a Boolean value.

Definition at line 650 of file Context.java.

    {
        return value ? mkTrue() : mkFalse();
    }
BoolExpr mkBoolConst ( Symbol  name) throws Z3Exception [inline]

Create a Boolean constant.

Definition at line 552 of file Context.java.

    {

        return (BoolExpr) mkConst(name, getBoolSort());
    }
BoolExpr mkBoolConst ( String  name) throws Z3Exception [inline]

Create a Boolean constant.

Definition at line 561 of file Context.java.

    {

        return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
    }
BoolSort mkBoolSort ( ) throws Z3Exception [inline]

Create a new Boolean sort.

Definition at line 136 of file Context.java.

Referenced by Expr.isBool().

    {

        return new BoolSort(this);
    }
Expr mkBound ( int  index,
Sort  ty 
) throws Z3Exception [inline]

Creates a new bound variable.

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

Definition at line 482 of file Context.java.

    {
        return Expr.create(this,
                Native.mkBound(nCtx(), index, ty.getNativeObject()));
    }
BitVecNum mkBV ( String  v,
int  size 
) throws Z3Exception [inline]

Create a bit-vector numeral.

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

Definition at line 2025 of file Context.java.

    {

        return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
    }
BitVecNum mkBV ( int  v,
int  size 
) throws Z3Exception [inline]

Create a bit-vector numeral.

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

Definition at line 2035 of file Context.java.

    {

        return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
    }
BitVecNum mkBV ( long  v,
int  size 
) throws Z3Exception [inline]

Create a bit-vector numeral.

Parameters:
vvalue of the numeral.

*

Parameters:
sizethe size of the bit-vector

Definition at line 2045 of file Context.java.

    {

        return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
    }
IntExpr mkBV2Int ( BitVecExpr  t,
boolean  signed 
) throws Z3Exception [inline]

Create an integer from the bit-vector argument t . 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 1509 of file Context.java.

    {

        checkContextMatch(t);
        return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
                (signed) ? true : false));
    }
BitVecExpr mkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1071 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvadd(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BoolExpr mkBVAddNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
) throws Z3Exception [inline]

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

Definition at line 1521 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
                : false));
    }
BoolExpr mkBVAddNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1536 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 982 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvand(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVASHR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

Arithmetic shift right 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 1416 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvashr(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVConst ( Symbol  name,
int  size 
) throws Z3Exception [inline]

Creates a bit-vector constant.

Definition at line 606 of file Context.java.

    {

        return (BitVecExpr) mkConst(name, mkBitVecSort(size));
    }
BitVecExpr mkBVConst ( String  name,
int  size 
) throws Z3Exception [inline]

Creates a bit-vector constant.

Definition at line 615 of file Context.java.

    {

        return (BitVecExpr) mkConst(name, mkBitVecSort(size));
    }
BitVecExpr mkBVLSHR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

Logical shift right 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 1396 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1097 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvmul(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BoolExpr mkBVMulNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
) throws Z3Exception [inline]

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

Definition at line 1605 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
                : false));
    }
BoolExpr mkBVMulNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1620 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1021 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvnand(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVNeg ( BitVecExpr  t) throws Z3Exception [inline]

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

Definition at line 1060 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
    }

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

Definition at line 1593 of file Context.java.

    {

        checkContextMatch(t);
        return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
                t.getNativeObject()));
    }
BitVecExpr mkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1034 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvnor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVNot ( BitVecExpr  t) throws Z3Exception [inline]

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

Definition at line 947 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
    }
BitVecExpr mkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 995 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BitVecExpr mkBVRedAND ( BitVecExpr  t) throws Z3Exception [inline]

Take conjunction of bits in a vector, return vector of length 1. The argument must have a bit-vector sort.

Definition at line 958 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvredand(nCtx(),
                t.getNativeObject()));
    }
BitVecExpr mkBVRedOR ( BitVecExpr  t) throws Z3Exception [inline]

Take disjunction of bits in a vector, return vector of length 1. The argument must have a bit-vector sort.

Definition at line 970 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvredor(nCtx(),
                t.getNativeObject()));
    }
BitVecExpr mkBVRotateLeft ( int  i,
BitVecExpr  t 
) throws Z3Exception [inline]

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

Definition at line 1429 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
                t.getNativeObject()));
    }
BitVecExpr mkBVRotateLeft ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1454 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVRotateRight ( int  i,
BitVecExpr  t 
) throws Z3Exception [inline]

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

Definition at line 1441 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
                t.getNativeObject()));
    }
BitVecExpr mkBVRotateRight ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1469 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVSDiv ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

Signed division. 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 < 0.

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

Definition at line 1133 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BoolExpr mkBVSDivNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1579 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BoolExpr mkBVSGE ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1258 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BoolExpr mkBVSGT ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1284 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BitVecExpr mkBVSHL ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

Shift left. 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 1377 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvshl(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BoolExpr mkBVSLE ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1232 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BoolExpr mkBVSLT ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1206 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BitVecExpr mkBVSMod ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1180 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVSRem ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

Signed remainder. 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 1166 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1084 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsub(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BoolExpr mkBVSubNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1550 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BoolExpr mkBVSubNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2,
boolean  isSigned 
) throws Z3Exception [inline]

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

Definition at line 1564 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
                : false));
    }
BitVecExpr mkBVUDiv ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

Unsigned division. 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 1112 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BoolExpr mkBVUGE ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1245 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BoolExpr mkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1271 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BoolExpr mkBVULE ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1219 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BoolExpr mkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1193 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BitVecExpr mkBVURem ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

Unsigned remainder. 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 1148 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvurem(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1047 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 1008 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvxor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
BitVecExpr mkConcat ( BitVecExpr  t1,
BitVecExpr  t2 
) throws Z3Exception [inline]

Bit-vector concatenation. 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 1302 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkConcat(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
Expr mkConst ( Symbol  name,
Sort  range 
) throws Z3Exception [inline]

Creates a new Constant of sort range and named name .

Definition at line 505 of file Context.java.

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

    {

        checkContextMatch(name);
        checkContextMatch(range);

        return Expr.create(
                this,
                Native.mkConst(nCtx(), name.getNativeObject(),
                        range.getNativeObject()));
    }
Expr mkConst ( String  name,
Sort  range 
) throws Z3Exception [inline]

Creates a new Constant of sort range and named name .

Definition at line 521 of file Context.java.

    {

        return mkConst(mkSymbol(name), range);
    }
Expr mkConst ( FuncDecl  f) throws Z3Exception [inline]

Creates a fresh constant from the FuncDecl f .

Parameters:
fA decl of a 0-arity function

Definition at line 543 of file Context.java.

    {

        return mkApp(f, (Expr[]) null);
    }
ArrayExpr mkConstArray ( Sort  domain,
Expr  v 
) throws Z3Exception [inline]

Create a constant array. The resulting term is an array, such that a selecton an arbitrary index produces the value v.

See also:
MkArraySort, MkSelect

Definition at line 1699 of file Context.java.

    {

        checkContextMatch(domain);
        checkContextMatch(v);
        return new ArrayExpr(this, Native.mkConstArray(nCtx(),
                domain.getNativeObject(), v.getNativeObject()));
    }
FuncDecl mkConstDecl ( Symbol  name,
Sort  range 
) throws Z3Exception [inline]

Creates a new constant function declaration.

Definition at line 447 of file Context.java.

    {

        checkContextMatch(name);
        checkContextMatch(range);
        return new FuncDecl(this, name, null, range);
    }
FuncDecl mkConstDecl ( String  name,
Sort  range 
) throws Z3Exception [inline]

Creates a new constant function declaration.

Definition at line 458 of file Context.java.

    {

        checkContextMatch(range);
        return new FuncDecl(this, mkSymbol(name), null, range);
    }
Constructor mkConstructor ( Symbol  name,
Symbol  recognizer,
Symbol[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
) throws Z3Exception [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 287 of file Context.java.

    {

        return new Constructor(this, name, recognizer, fieldNames, sorts,
                sortRefs);
    }
Constructor mkConstructor ( String  name,
String  recognizer,
String[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
) throws Z3Exception [inline]

Create a datatype constructor.

Parameters:
name
recognizer
fieldNames
sorts
sortRefs
Returns:

Definition at line 303 of file Context.java.

    {

        return new Constructor(this, mkSymbol(name), mkSymbol(recognizer),
                MkSymbols(fieldNames), sorts, sortRefs);
    }
DatatypeSort mkDatatypeSort ( Symbol  name,
Constructor[]  constructors 
) throws Z3Exception [inline]

Create a new datatype sort.

Definition at line 315 of file Context.java.

    {

        checkContextMatch(name);
        checkContextMatch(constructors);
        return new DatatypeSort(this, name, constructors);
    }
DatatypeSort mkDatatypeSort ( String  name,
Constructor[]  constructors 
) throws Z3Exception [inline]

Create a new datatype sort.

Definition at line 327 of file Context.java.

    {

        checkContextMatch(constructors);
        return new DatatypeSort(this, mkSymbol(name), constructors);
    }
DatatypeSort [] mkDatatypeSorts ( Symbol[]  names,
Constructor  c[][] 
) throws Z3Exception [inline]

Create mutually recursive datatypes.

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

Definition at line 340 of file Context.java.

Referenced by Context.mkDatatypeSorts().

    {

        checkContextMatch(names);
        int n = (int) names.length;
        ConstructorList[] cla = new ConstructorList[n];
        long[] n_constr = new long[n];
        for (int i = 0; i < n; i++)
        {
            Constructor[] constructor = c[i];

            checkContextMatch(constructor);
            cla[i] = new ConstructorList(this, constructor);
            n_constr[i] = cla[i].getNativeObject();
        }
        long[] n_res = new long[n];
        Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
                n_constr);
        DatatypeSort[] res = new DatatypeSort[n];
        for (int i = 0; i < n; i++)
            res[i] = new DatatypeSort(this, n_res[i]);
        return res;
    }
DatatypeSort [] mkDatatypeSorts ( String[]  names,
Constructor  c[][] 
) throws Z3Exception [inline]

Create mutually recursive data-types.

Parameters:
names
c
Returns:

Definition at line 371 of file Context.java.

    {

        return mkDatatypeSorts(MkSymbols(names), c);
    }
BoolExpr mkDistinct ( Expr...  args) throws Z3Exception [inline]

Creates a distinct term.

Definition at line 669 of file Context.java.

    {
        checkContextMatch(args);
        return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length,
                AST.arrayToNative(args)));
    }
ArithExpr mkDiv ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception [inline]

Create an expression representing t1 / t2.

Definition at line 807 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
Expr mkEmptySet ( Sort  domain) throws Z3Exception [inline]

Create an empty set.

Definition at line 1753 of file Context.java.

    {

        checkContextMatch(domain);
        return Expr.create(this,
                Native.mkEmptySet(nCtx(), domain.getNativeObject()));
    }
EnumSort mkEnumSort ( Symbol  name,
Symbol...  enumNames 
) throws Z3Exception [inline]

Create a new enumeration sort.

Definition at line 216 of file Context.java.

    {

        checkContextMatch(name);
        checkContextMatch(enumNames);
        return new EnumSort(this, name, enumNames);
    }
EnumSort mkEnumSort ( String  name,
String...  enumNames 
) throws Z3Exception [inline]

Create a new enumeration sort.

Definition at line 228 of file Context.java.

    {
        return new EnumSort(this, mkSymbol(name), MkSymbols(enumNames));
    }
BoolExpr mkEq ( Expr  x,
Expr  y 
) throws Z3Exception [inline]

Creates the equality x = y .

Definition at line 658 of file Context.java.

    {
        checkContextMatch(x);
        checkContextMatch(y);
        return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
                y.getNativeObject()));
    }
Quantifier mkExists ( Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception [inline]

Create an existential Quantifier.

See also:
MkForall(Sort[],Symbol[],Expr,uint,Pattern[],Expr[],Symbol,Symbol)

Definition at line 2095 of file Context.java.

Referenced by Context.mkQuantifier().

    {

        return new Quantifier(this, false, sorts, names, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }
Quantifier mkExists ( Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception [inline]

Create an existential Quantifier.

Definition at line 2107 of file Context.java.

    {

        return new Quantifier(this, false, boundConstants, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }
BitVecExpr mkExtract ( int  high,
int  low,
BitVecExpr  t 
) throws Z3Exception [inline]

Bit-vector extraction. 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 1318 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
                t.getNativeObject()));
    }
BoolExpr mkFalse ( ) throws Z3Exception [inline]

The false Term.

Definition at line 642 of file Context.java.

Referenced by Context.mkBool().

    {
        return new BoolExpr(this, Native.mkFalse(nCtx()));
    }
FiniteDomainSort mkFiniteDomainSort ( Symbol  name,
long  size 
) throws Z3Exception [inline]

Create a new finite domain sort.

Definition at line 258 of file Context.java.

    {

        checkContextMatch(name);
        return new FiniteDomainSort(this, name, size);
    }
FiniteDomainSort mkFiniteDomainSort ( String  name,
long  size 
) throws Z3Exception [inline]

Create a new finite domain sort.

Definition at line 269 of file Context.java.

    {

        return new FiniteDomainSort(this, mkSymbol(name), size);
    }
Fixedpoint mkFixedpoint ( ) throws Z3Exception [inline]

Create a Fixedpoint context.

Definition at line 2849 of file Context.java.

    {

        return new Fixedpoint(this);
    }
Quantifier mkForall ( Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception [inline]

Create a universal Quantifier. 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.

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.

Definition at line 2070 of file Context.java.

Referenced by Context.mkQuantifier().

    {

        return new Quantifier(this, true, sorts, names, body, weight, patterns,
                noPatterns, quantifierID, skolemID);
    }
Quantifier mkForall ( Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception [inline]

Create a universal Quantifier.

Definition at line 2082 of file Context.java.

    {

        return new Quantifier(this, true, boundConstants, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }
Expr mkFreshConst ( String  prefix,
Sort  range 
) throws Z3Exception [inline]

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

Definition at line 531 of file Context.java.

    {

        checkContextMatch(range);
        return Expr.create(this,
                Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
    }
FuncDecl mkFreshConstDecl ( String  prefix,
Sort  range 
) throws Z3Exception [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 470 of file Context.java.

    {

        checkContextMatch(range);
        return new FuncDecl(this, prefix, null, range);
    }
FuncDecl mkFreshFuncDecl ( String  prefix,
Sort[]  domain,
Sort  range 
) throws Z3Exception [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 435 of file Context.java.

    {

        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl(this, prefix, domain, range);
    }
Expr mkFullSet ( Sort  domain) throws Z3Exception [inline]

Create the full set.

Definition at line 1764 of file Context.java.

    {

        checkContextMatch(domain);
        return Expr.create(this,
                Native.mkFullSet(nCtx(), domain.getNativeObject()));
    }
FuncDecl mkFuncDecl ( Symbol  name,
Sort[]  domain,
Sort  range 
) throws Z3Exception [inline]

Creates a new function declaration.

Definition at line 381 of file Context.java.

    {

        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl(this, name, domain, range);
    }
FuncDecl mkFuncDecl ( Symbol  name,
Sort  domain,
Sort  range 
) throws Z3Exception [inline]

Creates a new function declaration.

Definition at line 394 of file Context.java.

    {

        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        Sort[] q = new Sort[] { domain };
        return new FuncDecl(this, name, q, range);
    }
FuncDecl mkFuncDecl ( String  name,
Sort[]  domain,
Sort  range 
) throws Z3Exception [inline]

Creates a new function declaration.

Definition at line 408 of file Context.java.

    {

        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl(this, mkSymbol(name), domain, range);
    }
FuncDecl mkFuncDecl ( String  name,
Sort  domain,
Sort  range 
) throws Z3Exception [inline]

Creates a new function declaration.

Definition at line 420 of file Context.java.

    {

        checkContextMatch(domain);
        checkContextMatch(range);
        Sort[] q = new Sort[] { domain };
        return new FuncDecl(this, mkSymbol(name), q, range);
    }
BoolExpr mkGe ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception [inline]

Create an expression representing t1 >= t2

Definition at line 895 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
Goal mkGoal ( boolean  models,
boolean  unsatCores,
boolean  proofs 
) throws Z3Exception [inline]

Creates a new Goal. 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 2380 of file Context.java.

    {

        return new Goal(this, models, unsatCores, proofs);
    }
BoolExpr mkGt ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception [inline]

Create an expression representing t1 > t2

Definition at line 883 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BoolExpr mkIff ( BoolExpr  t1,
BoolExpr  t2 
) throws Z3Exception [inline]

Create an expression representing t1 iff t2.

Definition at line 705 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BoolExpr mkImplies ( BoolExpr  t1,
BoolExpr  t2 
) throws Z3Exception [inline]

Create an expression representing t1 -> t2.

Definition at line 717 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkImplies(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
IntNum mkInt ( String  v) throws Z3Exception [inline]

Create an integer numeral.

Parameters:
vA string representing the Term value in decimal notation.

Definition at line 1989 of file Context.java.

    {

        return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
                .getNativeObject()));
    }
IntNum mkInt ( int  v) throws Z3Exception [inline]

Create an integer numeral.

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

Definition at line 2001 of file Context.java.

    {

        return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
                .getNativeObject()));
    }
IntNum mkInt ( long  v) throws Z3Exception [inline]

Create an integer numeral.

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

Definition at line 2013 of file Context.java.

    {

        return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
                .getNativeObject()));
    }
BitVecExpr mkInt2BV ( int  n,
IntExpr  t 
) throws Z3Exception [inline]

Create an n bit bit-vector from the integer argument t . 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 1487 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
                t.getNativeObject()));
    }
RealExpr mkInt2Real ( IntExpr  t) throws Z3Exception [inline]

Coerce an integer to a real. 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) <= t1 < MkInt2Real(k)+1. The argument must be of integer sort.

Definition at line 913 of file Context.java.

    {

        checkContextMatch(t);
        return new RealExpr(this,
                Native.mkInt2real(nCtx(), t.getNativeObject()));
    }
IntExpr mkIntConst ( Symbol  name) throws Z3Exception [inline]

Creates an integer constant.

Definition at line 570 of file Context.java.

    {

        return (IntExpr) mkConst(name, getIntSort());
    }
IntExpr mkIntConst ( String  name) throws Z3Exception [inline]

Creates an integer constant.

Definition at line 579 of file Context.java.

    {

        return (IntExpr) mkConst(name, getIntSort());
    }
IntSort mkIntSort ( ) throws Z3Exception [inline]

Create a new integer sort.

Definition at line 164 of file Context.java.

    {

        return new IntSort(this);
    }
BoolExpr mkIsInteger ( RealExpr  t) throws Z3Exception [inline]

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

Definition at line 936 of file Context.java.

    {

        checkContextMatch(t);
        return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
    }
Expr mkITE ( BoolExpr  t1,
Expr  t2,
Expr  t3 
) throws Z3Exception [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 692 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        checkContextMatch(t3);
        return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
                t2.getNativeObject(), t3.getNativeObject()));
    }
BoolExpr mkLe ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception [inline]

Create an expression representing t1 <= t2

Definition at line 871 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
ListSort mkListSort ( Symbol  name,
Sort  elemSort 
) throws Z3Exception [inline]

Create a new list sort.

Definition at line 237 of file Context.java.

    {

        checkContextMatch(name);
        checkContextMatch(elemSort);
        return new ListSort(this, name, elemSort);
    }
ListSort mkListSort ( String  name,
Sort  elemSort 
) throws Z3Exception [inline]

Create a new list sort.

Definition at line 248 of file Context.java.

    {

        checkContextMatch(elemSort);
        return new ListSort(this, mkSymbol(name), elemSort);
    }
BoolExpr mkLt ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception [inline]

Create an expression representing t1 < t2

Definition at line 859 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
ArrayExpr mkMap ( FuncDecl  f,
ArrayExpr...  args 
) throws Z3Exception [inline]

Maps f on the argument arrays. Eeach 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 1717 of file Context.java.

    {

        checkContextMatch(f);
        checkContextMatch(args);
        return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
                f.getNativeObject(), AST.arrayLength(args),
                AST.arrayToNative(args)));
    }
IntExpr mkMod ( IntExpr  t1,
IntExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 820 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
ArithExpr mkMul ( ArithExpr...  t) throws Z3Exception [inline]

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

Definition at line 774 of file Context.java.

    {

        checkContextMatch(t);
        return (ArithExpr) Expr.create(this,
                Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t)));
    }
BoolExpr mkNot ( BoolExpr  a) throws Z3Exception [inline]

Mk an expression representing not(a).

Definition at line 679 of file Context.java.

    {

        checkContextMatch(a);
        return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
    }
Expr mkNumeral ( String  v,
Sort  ty 
) throws Z3Exception [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 1890 of file Context.java.

Referenced by Context.mkBV().

    {

        checkContextMatch(ty);
        return Expr.create(this,
                Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
    }
Expr mkNumeral ( int  v,
Sort  ty 
) throws Z3Exception [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 1908 of file Context.java.

    {

        checkContextMatch(ty);
        return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
    }
Expr mkNumeral ( long  v,
Sort  ty 
) throws Z3Exception [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 1925 of file Context.java.

    {

        checkContextMatch(ty);
        return Expr.create(this,
                Native.mkInt64(nCtx(), v, ty.getNativeObject()));
    }
BoolExpr mkOr ( BoolExpr...  t) throws Z3Exception [inline]

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

Definition at line 752 of file Context.java.

    {

        checkContextMatch(t);
        return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length,
                AST.arrayToNative(t)));
    }
Params mkParams ( ) throws Z3Exception [inline]

Creates a new ParameterSet.

Definition at line 2390 of file Context.java.

    {

        return new Params(this);
    }
Pattern mkPattern ( Expr...  terms) throws Z3Exception [inline]

Create a quantifier pattern.

Definition at line 491 of file Context.java.

    {
        if (terms.length == 0)
            throw new Z3Exception("Cannot create a pattern from zero terms");

        long[] termsNative = AST.arrayToNative(terms);
        return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length,
                termsNative));
    }
ArithExpr mkPower ( ArithExpr  t1,
ArithExpr  t2 
) throws Z3Exception [inline]

Create an expression representing t1 ^ t2.

Definition at line 845 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return (ArithExpr) Expr.create(
                this,
                Native.mkPower(nCtx(), t1.getNativeObject(),
                        t2.getNativeObject()));
    }
Probe mkProbe ( String  name) throws Z3Exception [inline]

Creates a new Probe.

Definition at line 2673 of file Context.java.

    {
        return new Probe(this, name);
    }
Quantifier mkQuantifier ( boolean  universal,
Sort[]  sorts,
Symbol[]  names,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception [inline]

Create a Quantifier.

Definition at line 2119 of file Context.java.

    {

        if (universal)
            return mkForall(sorts, names, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
        else
            return mkExists(sorts, names, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
    }
Quantifier mkQuantifier ( boolean  universal,
Expr[]  boundConstants,
Expr  body,
int  weight,
Pattern[]  patterns,
Expr[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
) throws Z3Exception [inline]

Create a Quantifier.

Definition at line 2136 of file Context.java.

    {

        if (universal)
            return mkForall(boundConstants, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
        else
            return mkExists(boundConstants, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
    }
RatNum mkReal ( int  num,
int  den 
) throws Z3Exception [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 1940 of file Context.java.

    {
        if (den == 0)
            throw new Z3Exception("Denominator is zero");

        return new RatNum(this, Native.mkReal(nCtx(), num, den));
    }
RatNum mkReal ( String  v) throws Z3Exception [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 1954 of file Context.java.

    {

        return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
                .getNativeObject()));
    }
RatNum mkReal ( int  v) throws Z3Exception [inline]

Create a real numeral.

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

Definition at line 1966 of file Context.java.

    {

        return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
                .getNativeObject()));
    }
RatNum mkReal ( long  v) throws Z3Exception [inline]

Create a real numeral.

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

Definition at line 1978 of file Context.java.

    {

        return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
                .getNativeObject()));
    }
IntExpr mkReal2Int ( RealExpr  t) throws Z3Exception [inline]

Coerce a real to an integer. 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 926 of file Context.java.

    {

        checkContextMatch(t);
        return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
    }
RealExpr mkRealConst ( Symbol  name) throws Z3Exception [inline]

Creates a real constant.

Definition at line 588 of file Context.java.

    {

        return (RealExpr) mkConst(name, getRealSort());
    }
RealExpr mkRealConst ( String  name) throws Z3Exception [inline]

Creates a real constant.

Definition at line 597 of file Context.java.

    {

        return (RealExpr) mkConst(name, getRealSort());
    }
RealSort mkRealSort ( ) throws Z3Exception [inline]

Create a real sort.

Definition at line 173 of file Context.java.

    {

        return new RealSort(this);
    }
IntExpr mkRem ( IntExpr  t1,
IntExpr  t2 
) throws Z3Exception [inline]

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

Definition at line 833 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BitVecExpr mkRepeat ( int  i,
BitVecExpr  t 
) throws Z3Exception [inline]

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

Definition at line 1359 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
                t.getNativeObject()));
    }
Expr mkSelect ( ArrayExpr  a,
Expr  i 
) throws Z3Exception [inline]

Array read. 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 1659 of file Context.java.

    {

        checkContextMatch(a);
        checkContextMatch(i);
        return Expr.create(
                this,
                Native.mkSelect(nCtx(), a.getNativeObject(),
                        i.getNativeObject()));
    }
Expr mkSetAdd ( Expr  set,
Expr  element 
) throws Z3Exception [inline]

Add an element to the set.

Definition at line 1775 of file Context.java.

    {

        checkContextMatch(set);
        checkContextMatch(element);
        return Expr.create(
                this,
                Native.mkSetAdd(nCtx(), set.getNativeObject(),
                        element.getNativeObject()));
    }
Expr mkSetComplement ( Expr  arg) throws Z3Exception [inline]

Take the complement of a set.

Definition at line 1843 of file Context.java.

    {

        checkContextMatch(arg);
        return Expr.create(this,
                Native.mkSetComplement(nCtx(), arg.getNativeObject()));
    }
Expr mkSetDel ( Expr  set,
Expr  element 
) throws Z3Exception [inline]

Remove an element from a set.

Definition at line 1789 of file Context.java.

    {

        checkContextMatch(set);
        checkContextMatch(element);
        return Expr.create(
                this,
                Native.mkSetDel(nCtx(), set.getNativeObject(),
                        element.getNativeObject()));
    }
Expr mkSetDifference ( Expr  arg1,
Expr  arg2 
) throws Z3Exception [inline]

Take the difference between two sets.

Definition at line 1829 of file Context.java.

    {

        checkContextMatch(arg1);
        checkContextMatch(arg2);
        return Expr.create(
                this,
                Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
                        arg2.getNativeObject()));
    }
Expr mkSetIntersection ( Expr...  args) throws Z3Exception [inline]

Take the intersection of a list of sets.

Definition at line 1816 of file Context.java.

    {

        checkContextMatch(args);
        return Expr.create(
                this,
                Native.mkSetIntersect(nCtx(), (int) args.length,
                        AST.arrayToNative(args)));
    }
Expr mkSetMembership ( Expr  elem,
Expr  set 
) throws Z3Exception [inline]

Check for set membership.

Definition at line 1854 of file Context.java.

    {

        checkContextMatch(elem);
        checkContextMatch(set);
        return Expr.create(
                this,
                Native.mkSetMember(nCtx(), elem.getNativeObject(),
                        set.getNativeObject()));
    }
SetSort mkSetSort ( Sort  ty) throws Z3Exception [inline]

Create a set type.

Definition at line 1743 of file Context.java.

    {

        checkContextMatch(ty);
        return new SetSort(this, ty);
    }
Expr mkSetSubset ( Expr  arg1,
Expr  arg2 
) throws Z3Exception [inline]

Check for subsetness of sets.

Definition at line 1868 of file Context.java.

    {

        checkContextMatch(arg1);
        checkContextMatch(arg2);
        return Expr.create(
                this,
                Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
                        arg2.getNativeObject()));
    }
Expr mkSetUnion ( Expr...  args) throws Z3Exception [inline]

Take the union of a list of sets.

Definition at line 1803 of file Context.java.

    {

        checkContextMatch(args);
        return Expr.create(
                this,
                Native.mkSetUnion(nCtx(), (int) args.length,
                        AST.arrayToNative(args)));
    }
BitVecExpr mkSignExt ( int  i,
BitVecExpr  t 
) throws Z3Exception [inline]

Bit-vector sign extension. 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 1333 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
                t.getNativeObject()));
    }
Solver mkSimpleSolver ( ) throws Z3Exception [inline]

Creates a new (incremental) solver.

Definition at line 2828 of file Context.java.

    {

        return new Solver(this, Native.mkSimpleSolver(nCtx()));
    }
Solver mkSolver ( ) throws Z3Exception [inline]

Creates a new (incremental) solver. 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 2795 of file Context.java.

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

    {
        return mkSolver((Symbol) null);
    }
Solver mkSolver ( Symbol  logic) throws Z3Exception [inline]

Creates a new (incremental) solver. 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 2806 of file Context.java.

    {

        if (logic == null)
            return new Solver(this, Native.mkSolver(nCtx()));
        else
            return new Solver(this, Native.mkSolverForLogic(nCtx(),
                    logic.getNativeObject()));
    }
Solver mkSolver ( String  logic) throws Z3Exception [inline]

Creates a new (incremental) solver.

See also:
MkSolver(Symbol)

Definition at line 2819 of file Context.java.

    {

        return mkSolver(mkSymbol(logic));
    }
Solver mkSolver ( Tactic  t) throws Z3Exception [inline]

Creates a solver that is implemented using the given tactic. The solver supports the commands Push and Pop, but it will always solve each check from scratch.

Definition at line 2839 of file Context.java.

    {

        return new Solver(this, Native.mkSolverFromTactic(nCtx(),
                t.getNativeObject()));
    }
ArrayExpr mkStore ( ArrayExpr  a,
Expr  i,
Expr  v 
) throws Z3Exception [inline]

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

See also:
MkArraySort, MkSelect

Definition at line 1683 of file Context.java.

    {

        checkContextMatch(a);
        checkContextMatch(i);
        checkContextMatch(v);
        return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
                i.getNativeObject(), v.getNativeObject()));
    }
ArithExpr mkSub ( ArithExpr...  t) throws Z3Exception [inline]

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

Definition at line 785 of file Context.java.

    {

        checkContextMatch(t);
        return (ArithExpr) Expr.create(this,
                Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t)));
    }
IntSymbol mkSymbol ( int  i) throws Z3Exception [inline]

Creates a new symbol using an integer. Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.

Definition at line 73 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.MkSymbols(), and Context.mkUninterpretedSort().

    {
        return new IntSymbol(this, i);
    }
StringSymbol mkSymbol ( String  name) throws Z3Exception [inline]

Create a symbol using a string.

Definition at line 81 of file Context.java.

    {
        return new StringSymbol(this, name);
    }
Symbol [] MkSymbols ( String[]  names) throws Z3Exception [inline, package]

Create an array of symbols.

Definition at line 89 of file Context.java.

Referenced by Context.mkConstructor(), Context.mkDatatypeSorts(), and Context.mkEnumSort().

    {
        if (names == null)
            return null;
        Symbol[] result = new Symbol[names.length];
        for (int i = 0; i < names.length; ++i)
            result[i] = mkSymbol(names[i]);
        return result;
    }
Tactic mkTactic ( String  name) throws Z3Exception [inline]

Creates a new Tactic.

Definition at line 2430 of file Context.java.

Referenced by Goal.simplify().

    {

        return new Tactic(this, name);
    }
Expr mkTermArray ( ArrayExpr  array) throws Z3Exception [inline]

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

Definition at line 1732 of file Context.java.

    {

        checkContextMatch(array);
        return Expr.create(this,
                Native.mkArrayDefault(nCtx(), array.getNativeObject()));
    }
BoolExpr mkTrue ( ) throws Z3Exception [inline]

The true Term.

Definition at line 634 of file Context.java.

Referenced by Context.mkBool().

    {
        return new BoolExpr(this, Native.mkTrue(nCtx()));
    }
TupleSort mkTupleSort ( Symbol  name,
Symbol[]  fieldNames,
Sort[]  fieldSorts 
) throws Z3Exception [inline]

Create a new tuple sort.

Definition at line 202 of file Context.java.

    {

        checkContextMatch(name);
        checkContextMatch(fieldNames);
        checkContextMatch(fieldSorts);
        return new TupleSort(this, name, (int) fieldNames.length, fieldNames,
                fieldSorts);
    }
ArithExpr mkUnaryMinus ( ArithExpr  t) throws Z3Exception [inline]

Create an expression representing -t.

Definition at line 796 of file Context.java.

    {

        checkContextMatch(t);
        return (ArithExpr) Expr.create(this,
                Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
    }

Create a new uninterpreted sort.

Definition at line 145 of file Context.java.

Referenced by Context.mkUninterpretedSort().

    {

        checkContextMatch(s);
        return new UninterpretedSort(this, s);
    }
UninterpretedSort mkUninterpretedSort ( String  str) throws Z3Exception [inline]

Create a new uninterpreted sort.

Definition at line 155 of file Context.java.

    {

        return mkUninterpretedSort(mkSymbol(str));
    }
BoolExpr mkXor ( BoolExpr  t1,
BoolExpr  t2 
) throws Z3Exception [inline]

Create an expression representing t1 xor t2.

Definition at line 729 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
BitVecExpr mkZeroExt ( int  i,
BitVecExpr  t 
) throws Z3Exception [inline]

Bit-vector zero extension. 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 1347 of file Context.java.

    {

        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
                t.getNativeObject()));
    }
ModelDecRefQueue model_DRQ ( ) [inline, package]

Definition at line 3002 of file Context.java.

Referenced by Model.decRef(), and Model.incRef().

    {
        return m_Model_DRQ;
    }
long nCtx ( ) [inline, package]

Definition at line 2927 of file Context.java.

Referenced by Context.and(), Context.andThen(), Context.benchmarkToSMTString(), InterpolationContext.CheckInterpolant(), InterpolationContext.ComputeInterpolant(), Context.cond(), Context.constProbe(), ASTVectorDecRefQueue.decRef(), ASTDecRefQueue.decRef(), FixedpointDecRefQueue.decRef(), FuncInterpDecRefQueue.decRef(), FuncInterpEntryDecRefQueue.decRef(), GoalDecRefQueue.decRef(), ModelDecRefQueue.decRef(), ParamDescrsDecRefQueue.decRef(), ParamsDecRefQueue.decRef(), ProbeDecRefQueue.decRef(), SolverDecRefQueue.decRef(), StatisticsDecRefQueue.decRef(), TacticDecRefQueue.decRef(), ASTMapDecRefQueue.decRef(), ApplyResultDecRefQueue.decRef(), Context.eq(), Context.fail(), Context.failIf(), Context.failIfNotDecided(), Context.ge(), InterpolationContext.GetInterpolant(), Context.getNumProbes(), Context.getNumSMTLIBAssumptions(), Context.getNumSMTLIBDecls(), Context.getNumSMTLIBFormulas(), Context.getNumSMTLIBSorts(), Context.getNumTactics(), Context.getProbeDescription(), Context.getProbeNames(), Context.getSimplifyParameterDescriptions(), Context.getSMTLIBAssumptions(), Context.getSMTLIBDecls(), Context.getSMTLIBFormulas(), Context.getSMTLIBSorts(), Context.getTacticDescription(), Context.getTacticNames(), Context.gt(), ApplyResultDecRefQueue.incRef(), FixedpointDecRefQueue.incRef(), FuncInterpDecRefQueue.incRef(), FuncInterpEntryDecRefQueue.incRef(), GoalDecRefQueue.incRef(), ASTMapDecRefQueue.incRef(), ModelDecRefQueue.incRef(), ParamDescrsDecRefQueue.incRef(), ParamsDecRefQueue.incRef(), ProbeDecRefQueue.incRef(), SolverDecRefQueue.incRef(), StatisticsDecRefQueue.incRef(), TacticDecRefQueue.incRef(), ASTDecRefQueue.incRef(), ASTVectorDecRefQueue.incRef(), Context.initContext(), InterpolationContext.InterpolationProfile(), Context.interrupt(), Context.le(), Context.lt(), Context.mkAdd(), Context.mkAnd(), Context.mkBitVecSort(), Context.mkBound(), Context.mkBV2Int(), Context.mkBVAdd(), Context.mkBVAddNoOverflow(), Context.mkBVAddNoUnderflow(), Context.mkBVAND(), Context.mkBVASHR(), Context.mkBVLSHR(), Context.mkBVMul(), Context.mkBVMulNoOverflow(), Context.mkBVMulNoUnderflow(), Context.mkBVNAND(), Context.mkBVNeg(), Context.mkBVNegNoOverflow(), Context.mkBVNOR(), Context.mkBVNot(), Context.mkBVOR(), Context.mkBVRedAND(), Context.mkBVRedOR(), Context.mkBVRotateLeft(), Context.mkBVRotateRight(), Context.mkBVSDiv(), Context.mkBVSDivNoOverflow(), Context.mkBVSGE(), Context.mkBVSGT(), Context.mkBVSHL(), Context.mkBVSLE(), Context.mkBVSLT(), Context.mkBVSMod(), Context.mkBVSRem(), Context.mkBVSub(), Context.mkBVSubNoOverflow(), Context.mkBVSubNoUnderflow(), Context.mkBVUDiv(), Context.mkBVUGE(), Context.mkBVUGT(), Context.mkBVULE(), Context.mkBVULT(), Context.mkBVURem(), Context.mkBVXNOR(), Context.mkBVXOR(), Context.mkConcat(), Context.mkConst(), Context.mkConstArray(), Context.mkDatatypeSorts(), Context.mkDistinct(), Context.mkDiv(), Context.mkEmptySet(), Context.mkEq(), Context.mkExtract(), Context.mkFalse(), Context.mkFreshConst(), Context.mkFullSet(), Context.mkGe(), Context.mkGt(), Context.mkIff(), Context.mkImplies(), Context.mkInt(), Context.mkInt2BV(), Context.mkInt2Real(), InterpolationContext.MkInterpolant(), Context.mkIsInteger(), Context.mkITE(), Context.mkLe(), Context.mkLt(), Context.mkMap(), Context.mkMod(), Context.mkMul(), Context.mkNot(), Context.mkNumeral(), Context.mkOr(), Context.mkPattern(), Context.mkPower(), Context.mkReal(), Context.mkReal2Int(), Context.mkRem(), Context.mkRepeat(), Context.mkSelect(), Context.mkSetAdd(), Context.mkSetComplement(), Context.mkSetDel(), Context.mkSetDifference(), Context.mkSetIntersection(), Context.mkSetMembership(), Context.mkSetSubset(), Context.mkSetUnion(), Context.mkSignExt(), Context.mkSimpleSolver(), Context.mkSolver(), Context.mkStore(), Context.mkSub(), Context.mkTermArray(), Context.mkTrue(), Context.mkUnaryMinus(), Context.mkXor(), Context.mkZeroExt(), Context.not(), Context.or(), Context.orElse(), Context.parAndThen(), Context.parOr(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), Context.parseSMTLIBFile(), Context.parseSMTLIBString(), InterpolationContext.ReadInterpolationProblem(), Context.repeat(), Context.setPrintMode(), Context.SimplifyHelp(), Context.skip(), Context.tryFor(), Context.updateParamValue(), Context.usingParams(), Context.when(), and InterpolationContext.WriteInterpolationProblem().

    {
        return m_ctx;
    }
Probe not ( Probe  p) throws Z3Exception [inline]

Create a probe that evaluates to "true" when the value p does not evaluate to "true".

Definition at line 2782 of file Context.java.

    {

        checkContextMatch(p);
        return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
    }
Probe or ( Probe  p1,
Probe  p2 
) throws Z3Exception [inline]

Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".

Definition at line 2770 of file Context.java.

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }
Tactic orElse ( Tactic  t1,
Tactic  t2 
) throws Z3Exception [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 2480 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new Tactic(this, Native.tacticOrElse(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
ParamDescrsDecRefQueue paramDescrs_DRQ ( ) [inline, package]

Definition at line 3012 of file Context.java.

Referenced by ParamDescrs.decRef(), and ParamDescrs.incRef().

    {
        return m_ParamDescrs_DRQ;
    }
ParamsDecRefQueue params_DRQ ( ) [inline, package]

Definition at line 3007 of file Context.java.

Referenced by Params.decRef(), and Params.incRef().

    {
        return m_Params_DRQ;
    }
Tactic parAndThen ( Tactic  t1,
Tactic  t2 
) throws Z3Exception [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 2622 of file Context.java.

    {

        checkContextMatch(t1);
        checkContextMatch(t2);
        return new Tactic(this, Native.tacticParAndThen(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
Tactic parOr ( Tactic...  t) throws Z3Exception [inline]

Create a tactic that applies the given tactics in parallel.

Definition at line 2610 of file Context.java.

    {
        checkContextMatch(t);
        return new Tactic(this, Native.tacticParOr(nCtx(),
                Tactic.arrayLength(t), Tactic.arrayToNative(t)));
    }
BoolExpr parseSMTLIB2File ( String  fileName,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
) throws Z3Exception [inline]

Parse the given file using the SMT-LIB2 parser.

See also:
ParseSMTLIB2String

Definition at line 2353 of file Context.java.

    {

        int csn = Symbol.arrayLength(sortNames);
        int cs = Sort.arrayLength(sorts);
        int cdn = Symbol.arrayLength(declNames);
        int cd = AST.arrayLength(decls);
        if (csn != cs || cdn != cd)
            throw new Z3Exception("Argument size mismatch");
        return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
                fileName, AST.arrayLength(sorts),
                Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
                AST.arrayLength(decls), Symbol.arrayToNative(declNames),
                AST.arrayToNative(decls)));
    }
BoolExpr parseSMTLIB2String ( String  str,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
) throws Z3Exception [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 2332 of file Context.java.

    {

        int csn = Symbol.arrayLength(sortNames);
        int cs = Sort.arrayLength(sorts);
        int cdn = Symbol.arrayLength(declNames);
        int cd = AST.arrayLength(decls);
        if (csn != cs || cdn != cd)
            throw new Z3Exception("Argument size mismatch");
        return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
                str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
                AST.arrayToNative(sorts), AST.arrayLength(decls),
                Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
    }
void parseSMTLIBFile ( String  fileName,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
) throws Z3Exception [inline]

Parse the given file using the SMT-LIB parser.

See also:
ParseSMTLIBString

Definition at line 2215 of file Context.java.

    {
        int csn = Symbol.arrayLength(sortNames);
        int cs = Sort.arrayLength(sorts);
        int cdn = Symbol.arrayLength(declNames);
        int cd = AST.arrayLength(decls);
        if (csn != cs || cdn != cd)
            throw new Z3Exception("Argument size mismatch");
        Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
                Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
                AST.arrayLength(decls), Symbol.arrayToNative(declNames),
                AST.arrayToNative(decls));
    }
void parseSMTLIBString ( String  str,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl[]  decls 
) throws Z3Exception [inline]

Parse the given string using the SMT-LIB parser. 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 2196 of file Context.java.

    {
        int csn = Symbol.arrayLength(sortNames);
        int cs = Sort.arrayLength(sorts);
        int cdn = Symbol.arrayLength(declNames);
        int cd = AST.arrayLength(decls);
        if (csn != cs || cdn != cd)
            throw new Z3Exception("Argument size mismatch");
        Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
                Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
                AST.arrayLength(decls), Symbol.arrayToNative(declNames),
                AST.arrayToNative(decls));
    }
ProbeDecRefQueue probe_DRQ ( ) [inline, package]

Definition at line 3017 of file Context.java.

Referenced by Probe.decRef(), and Probe.incRef().

    {
        return m_Probe_DRQ;
    }
Tactic repeat ( Tactic  t,
int  max 
) throws Z3Exception [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 2538 of file Context.java.

    {

        checkContextMatch(t);
        return new Tactic(this, Native.tacticRepeat(nCtx(),
                t.getNativeObject(), max));
    }
void setPrintMode ( Z3_ast_print_mode  value) throws Z3Exception [inline]

Selects the format used for pretty-printing expressions. 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 2160 of file Context.java.

Referenced by Context.initContext().

    {
        Native.setAstPrintMode(nCtx(), value.toInt());
    }
String SimplifyHelp ( ) throws Z3Exception [inline]

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

Definition at line 2888 of file Context.java.

    {

        return Native.simplifyGetHelp(nCtx());
    }
Tactic skip ( ) throws Z3Exception [inline]

Create a tactic that just returns the given goal.

Definition at line 2549 of file Context.java.

    {

        return new Tactic(this, Native.tacticSkip(nCtx()));
    }
SolverDecRefQueue solver_DRQ ( ) [inline, package]

Definition at line 3022 of file Context.java.

Referenced by Solver.decRef(), and Solver.incRef().

    {
        return m_Solver_DRQ;
    }
StatisticsDecRefQueue statistics_DRQ ( ) [inline, package]

Definition at line 3027 of file Context.java.

Referenced by Statistics.decRef(), and Statistics.incRef().

    {
        return m_Statistics_DRQ;
    }
TacticDecRefQueue tactic_DRQ ( ) [inline, package]

Definition at line 3032 of file Context.java.

Referenced by Tactic.decRef(), and Tactic.incRef().

    {
        return m_Tactic_DRQ;
    }
Tactic then ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
) throws Z3Exception [inline]

Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 . Shorthand for AndThen.

Definition at line 2470 of file Context.java.

    {
        return andThen(t1, t2, ts);
    }
static void ToggleWarningMessages ( boolean  enabled) throws Z3Exception [inline, static]

Enable/disable printing of warning messages to the console. Note that this function is static and effects the behaviour of all contexts globally.

Definition at line 2907 of file Context.java.

    {
        Native.toggleWarningMessages((enabled) ? true : false);
    }
Tactic tryFor ( Tactic  t,
int  ms 
) throws Z3Exception [inline]

Create a tactic that applies t to a goal for ms milliseconds. If t does not terminate within ms milliseconds, then it fails.

Definition at line 2495 of file Context.java.

    {

        checkContextMatch(t);
        return new Tactic(this, Native.tacticTryFor(nCtx(),
                t.getNativeObject(), ms));
    }
long unwrapAST ( AST  a) [inline]

Unwraps an AST. 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.Z3_inc_ref, WrapAST

).

Parameters:
aThe AST to unwrap.

Definition at line 2879 of file Context.java.

    {
        return a.getNativeObject();
    }
void updateParamValue ( String  id,
String  value 
) throws Z3Exception [inline]

Update a mutable configuration parameter. 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 2920 of file Context.java.

    {
        Native.updateParamValue(nCtx(), id, value);
    }
Tactic usingParams ( Tactic  t,
Params  p 
) throws Z3Exception [inline]

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

Definition at line 2589 of file Context.java.

Referenced by Context.with().

    {
        checkContextMatch(t);
        checkContextMatch(p);
        return new Tactic(this, Native.tacticUsingParams(nCtx(),
                t.getNativeObject(), p.getNativeObject()));
    }
Tactic when ( Probe  p,
Tactic  t 
) throws Z3Exception [inline]

Create a tactic that applies t to a given goal if the probe p evaluates to true. If p evaluates to false, then the new tactic behaves like the skip tactic.

Definition at line 2509 of file Context.java.

    {

        checkContextMatch(t);
        checkContextMatch(p);
        return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
                t.getNativeObject()));
    }
Tactic with ( Tactic  t,
Params  p 
) throws Z3Exception [inline]

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

Definition at line 2602 of file Context.java.

    {
        return usingParams(t, p);
    }
AST wrapAST ( long  nativeObject) throws Z3Exception [inline]

Wraps an AST. 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

See also:
UnwrapAST, Native.Z3_inc_ref, UnwrapAST

) and that it must have a correct reference count (see e.g., .

Parameters:
nativeObjectThe native pointer to wrap.

Definition at line 2864 of file Context.java.

    {

        return AST.create(this, nativeObject);
    }

Field Documentation

long m_ctx = 0 [package]
long m_refCount = 0 [protected]

Definition at line 3042 of file Context.java.

Referenced by Z3Object.dispose(), Context.finalize(), and Z3Object.Z3Object().

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines