src/api/java/Context.java

Go to the documentation of this file.

package com.microsoft.z3;

import java.util.Map;

import com.microsoft.z3.enumerations.Z3_ast_print_mode;

public class Context extends IDisposable
{
    public Context()
    {
        super();
        m_ctx = Native.mkContextRc(0);
        initContext();
    }

    public Context(Map<String, String> settings)
    {
        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();
    }

    public IntSymbol mkSymbol(int i)
    {
        return new IntSymbol(this, i);
    }

    public StringSymbol mkSymbol(String name)
    {
        return new StringSymbol(this, name);
    }

    Symbol[] mkSymbols(String[] names)
    {
        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;
    }

    private BoolSort m_boolSort = null;
    private IntSort m_intSort = null;
    private RealSort m_realSort = null;

    public BoolSort getBoolSort()
    {
        if (m_boolSort == null)
            m_boolSort = new BoolSort(this);
        return m_boolSort;
    }

    public IntSort getIntSort()
    {
        if (m_intSort == null)
            m_intSort = new IntSort(this);
        return m_intSort;
    }

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

    public BoolSort mkBoolSort()
    {
        return new BoolSort(this);
    }

    public UninterpretedSort mkUninterpretedSort(Symbol s)
    {
        checkContextMatch(s);
        return new UninterpretedSort(this, s);
    }

    public UninterpretedSort mkUninterpretedSort(String str)
    {
        return mkUninterpretedSort(mkSymbol(str));
    }

    public IntSort mkIntSort()
    {
        return new IntSort(this);
    }

    public RealSort mkRealSort()
    {
        return new RealSort(this);
    }

    public BitVecSort mkBitVecSort(int size)
    {
        return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
    }

    public ArraySort mkArraySort(Sort domain, Sort range)
    {
        checkContextMatch(domain);
        checkContextMatch(range);
        return new ArraySort(this, domain, range);
    }

    public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames,
            Sort[] fieldSorts)
    {
        checkContextMatch(name);
        checkContextMatch(fieldNames);
        checkContextMatch(fieldSorts);
        return new TupleSort(this, name, (int) fieldNames.length, fieldNames,
                fieldSorts);
    }

    public EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
           
    {
        checkContextMatch(name);
        checkContextMatch(enumNames);
        return new EnumSort(this, name, enumNames);
    }

    public EnumSort mkEnumSort(String name, String... enumNames)
           
    {
        return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
    }

    public ListSort mkListSort(Symbol name, Sort elemSort)
    {
        checkContextMatch(name);
        checkContextMatch(elemSort);
        return new ListSort(this, name, elemSort);
    }

    public ListSort mkListSort(String name, Sort elemSort)
    {
        checkContextMatch(elemSort);
        return new ListSort(this, mkSymbol(name), elemSort);
    }

    public FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
           
    {
        checkContextMatch(name);
        return new FiniteDomainSort(this, name, size);
    }

    public FiniteDomainSort mkFiniteDomainSort(String name, long size)
           
    {
        return new FiniteDomainSort(this, mkSymbol(name), size);
    }

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

        return new Constructor(this, name, recognizer, fieldNames, sorts,
                sortRefs);
    }

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

        return new Constructor(this, mkSymbol(name), mkSymbol(recognizer),
                mkSymbols(fieldNames), sorts, sortRefs);
    }

    public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
           
    {
        checkContextMatch(name);
        checkContextMatch(constructors);
        return new DatatypeSort(this, name, constructors);
    }

    public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
           
    {
        checkContextMatch(constructors);
        return new DatatypeSort(this, mkSymbol(name), constructors);
    }

    public DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
           
    {
        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;
    }

    public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
           
    {
        return mkDatatypeSorts(mkSymbols(names), c);
    }

    public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) 
            throws Z3Exception
    {
        return Expr.create
            (this, 
             Native.datatypeUpdateField
             (nCtx(), field.getNativeObject(),
              t.getNativeObject(), v.getNativeObject()));               
    }


    public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
           
    {
        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl(this, name, domain, range);
    }

    public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
           
    {
        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        Sort[] q = new Sort[] { domain };
        return new FuncDecl(this, name, q, range);
    }

    public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
           
    {
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl(this, mkSymbol(name), domain, range);
    }

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

    public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
           
    {
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl(this, prefix, domain, range);
    }

    public FuncDecl mkConstDecl(Symbol name, Sort range)
    {
        checkContextMatch(name);
        checkContextMatch(range);
        return new FuncDecl(this, name, null, range);
    }

    public FuncDecl mkConstDecl(String name, Sort range)
    {
        checkContextMatch(range);
        return new FuncDecl(this, mkSymbol(name), null, range);
    }

    public FuncDecl mkFreshConstDecl(String prefix, Sort range)
           
    {
        checkContextMatch(range);
        return new FuncDecl(this, prefix, null, range);
    }

    public Expr mkBound(int index, Sort ty)
    {
        return Expr.create(this,
                Native.mkBound(nCtx(), index, ty.getNativeObject()));
    }

    public Pattern mkPattern(Expr... terms)
    {
        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));
    }

    public Expr mkConst(Symbol name, Sort range)
    {
        checkContextMatch(name);
        checkContextMatch(range);

        return Expr.create(
                this,
                Native.mkConst(nCtx(), name.getNativeObject(),
                        range.getNativeObject()));
    }

    public Expr mkConst(String name, Sort range)
    {
        return mkConst(mkSymbol(name), range);
    }

    public Expr mkFreshConst(String prefix, Sort range)
    {
        checkContextMatch(range);
        return Expr.create(this,
                Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
    }

    public Expr mkConst(FuncDecl f)
    {
        return mkApp(f, (Expr[]) null);
    }

    public BoolExpr mkBoolConst(Symbol name)
    {
        return (BoolExpr) mkConst(name, getBoolSort());
    }

    public BoolExpr mkBoolConst(String name)
    {
        return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
    }

    public IntExpr mkIntConst(Symbol name)
    {
        return (IntExpr) mkConst(name, getIntSort());
    }

    public IntExpr mkIntConst(String name)
    {
        return (IntExpr) mkConst(name, getIntSort());
    }

    public RealExpr mkRealConst(Symbol name)
    {
        return (RealExpr) mkConst(name, getRealSort());
    }

    public RealExpr mkRealConst(String name)
    {
        return (RealExpr) mkConst(name, getRealSort());
    }

    public BitVecExpr mkBVConst(Symbol name, int size)
    {
        return (BitVecExpr) mkConst(name, mkBitVecSort(size));
    }

    public BitVecExpr mkBVConst(String name, int size)
    {
        return (BitVecExpr) mkConst(name, mkBitVecSort(size));
    }

    public Expr mkApp(FuncDecl f, Expr... args)
    {
        checkContextMatch(f);
        checkContextMatch(args);
        return Expr.create(this, f, args);
    }

    public BoolExpr mkTrue()
    {
        return new BoolExpr(this, Native.mkTrue(nCtx()));
    }

    public BoolExpr mkFalse()
    {
        return new BoolExpr(this, Native.mkFalse(nCtx()));
    }

    public BoolExpr mkBool(boolean value)
    {
        return value ? mkTrue() : mkFalse();
    }

    public BoolExpr mkEq(Expr x, Expr y)
    {
        checkContextMatch(x);
        checkContextMatch(y);
        return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
                y.getNativeObject()));
    }

    public BoolExpr mkDistinct(Expr... args)
    {
        checkContextMatch(args);
        return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length,
                AST.arrayToNative(args)));
    }

    public BoolExpr mkNot(BoolExpr a)
    {
        checkContextMatch(a);
        return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
    }

    public Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        checkContextMatch(t3);
        return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
                t2.getNativeObject(), t3.getNativeObject()));
    }

    public BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkImplies(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkAnd(BoolExpr... t)
    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length,
                AST.arrayToNative(t)));
    }

    public BoolExpr mkOr(BoolExpr... t)
    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length,
                AST.arrayToNative(t)));
    }

    public ArithExpr mkAdd(ArithExpr... t)
    {
        checkContextMatch(t);
        return (ArithExpr) Expr.create(this,
                Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t)));
    }

    public ArithExpr mkMul(ArithExpr... t)
    {
        checkContextMatch(t);
        return (ArithExpr) Expr.create(this,
                Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t)));
    }

    public ArithExpr mkSub(ArithExpr... t)
    {
        checkContextMatch(t);
        return (ArithExpr) Expr.create(this,
                Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t)));
    }

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

    public ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public IntExpr mkMod(IntExpr t1, IntExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public IntExpr mkRem(IntExpr t1, IntExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return (ArithExpr) Expr.create(
                this,
                Native.mkPower(nCtx(), t1.getNativeObject(),
                        t2.getNativeObject()));
    }

    public BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public RealExpr mkInt2Real(IntExpr t)
    {
        checkContextMatch(t);
        return new RealExpr(this,
                Native.mkInt2real(nCtx(), t.getNativeObject()));
    }

    public IntExpr mkReal2Int(RealExpr t)
    {
        checkContextMatch(t);
        return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
    }

    public BoolExpr mkIsInteger(RealExpr t)
    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
    }

    public BitVecExpr mkBVNot(BitVecExpr t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
    }

    public BitVecExpr mkBVRedAND(BitVecExpr t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvredand(nCtx(),
                t.getNativeObject()));
    }

    public BitVecExpr mkBVRedOR(BitVecExpr t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvredor(nCtx(),
                t.getNativeObject()));
    }

    public BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvand(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvxor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvnand(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvnor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

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

    public BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvadd(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsub(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvmul(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvurem(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

    public BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkConcat(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkExtract(int high, int low, BitVecExpr t)
           
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
                t.getNativeObject()));
    }

    public BitVecExpr mkSignExt(int i, BitVecExpr t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
                t.getNativeObject()));
    }

    public BitVecExpr mkZeroExt(int i, BitVecExpr t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
                t.getNativeObject()));
    }

    public BitVecExpr mkRepeat(int i, BitVecExpr t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
                t.getNativeObject()));
    }

    public BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvshl(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvashr(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
                t.getNativeObject()));
    }

    public BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
                t.getNativeObject()));
    }

    public BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
           
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
           
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BitVecExpr mkInt2BV(int n, IntExpr t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
                t.getNativeObject()));
    }

    public IntExpr mkBV2Int(BitVecExpr t, boolean signed)
    {
        checkContextMatch(t);
        return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
                (signed) ? true : false));
    }

    public BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2,
            boolean isSigned)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
                : false));
    }

    public BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
           
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
           
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2,
            boolean isSigned)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
                : false));
    }

    public BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
           
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public BoolExpr mkBVNegNoOverflow(BitVecExpr t)
    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
                t.getNativeObject()));
    }

    public BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2,
            boolean isSigned)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
                : false));
    }

    public BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
           
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
           
    {
        return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
    }

    public ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
           
    {
        return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
    }

    public Expr mkSelect(ArrayExpr a, Expr i)
    {
        checkContextMatch(a);
        checkContextMatch(i);
        return Expr.create(
                this,
                Native.mkSelect(nCtx(), a.getNativeObject(),
                        i.getNativeObject()));
    }

    public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
    {
        checkContextMatch(a);
        checkContextMatch(i);
        checkContextMatch(v);
        return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
                i.getNativeObject(), v.getNativeObject()));
    }

    public ArrayExpr mkConstArray(Sort domain, Expr v)
    {
        checkContextMatch(domain);
        checkContextMatch(v);
        return new ArrayExpr(this, Native.mkConstArray(nCtx(),
                domain.getNativeObject(), v.getNativeObject()));
    }

    public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
    {
        checkContextMatch(f);
        checkContextMatch(args);
        return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
                f.getNativeObject(), AST.arrayLength(args),
                AST.arrayToNative(args)));
    }

    public Expr mkTermArray(ArrayExpr array)
    {
        checkContextMatch(array);
        return Expr.create(this,
                Native.mkArrayDefault(nCtx(), array.getNativeObject()));
    }

    public SetSort mkSetSort(Sort ty)
    {
        checkContextMatch(ty);
        return new SetSort(this, ty);
    }

    public ArrayExpr mkEmptySet(Sort domain)
    {
        checkContextMatch(domain);
        return (ArrayExpr)Expr.create(this,
                Native.mkEmptySet(nCtx(), domain.getNativeObject()));
    }

    public ArrayExpr mkFullSet(Sort domain)
    {
        checkContextMatch(domain);
        return (ArrayExpr)Expr.create(this,
                Native.mkFullSet(nCtx(), domain.getNativeObject()));
    }

    public ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
    {
        checkContextMatch(set);
        checkContextMatch(element);
        return (ArrayExpr)Expr.create(this,
                Native.mkSetAdd(nCtx(), set.getNativeObject(),
                        element.getNativeObject()));
    }

    public ArrayExpr mkSetDel(ArrayExpr set, Expr element)
    {
        checkContextMatch(set);
        checkContextMatch(element);
        return (ArrayExpr)Expr.create(this,
                Native.mkSetDel(nCtx(), set.getNativeObject(),
                        element.getNativeObject()));
    }

    public ArrayExpr mkSetUnion(ArrayExpr... args)
    {
        checkContextMatch(args);
        return (ArrayExpr)Expr.create(this,
                Native.mkSetUnion(nCtx(), (int) args.length,
                        AST.arrayToNative(args)));
    }

    public ArrayExpr mkSetIntersection(ArrayExpr... args)
    {
        checkContextMatch(args);
        return (ArrayExpr)Expr.create(this,
                Native.mkSetIntersect(nCtx(), (int) args.length,
                        AST.arrayToNative(args)));
    }

    public ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
    {
        checkContextMatch(arg1);
        checkContextMatch(arg2);
        return (ArrayExpr)Expr.create(this,
                Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
                        arg2.getNativeObject()));
    }

    public ArrayExpr mkSetComplement(ArrayExpr arg)
    {
        checkContextMatch(arg);
        return (ArrayExpr)Expr.create(this,
                Native.mkSetComplement(nCtx(), arg.getNativeObject()));
    }

    public BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
    {
        checkContextMatch(elem);
        checkContextMatch(set);
        return (BoolExpr) Expr.create(this,
                Native.mkSetMember(nCtx(), elem.getNativeObject(),
                        set.getNativeObject()));
    }

    public BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
    {
        checkContextMatch(arg1);
        checkContextMatch(arg2);
        return (BoolExpr) Expr.create(this,
                Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
                        arg2.getNativeObject()));
    }

    public Expr mkNumeral(String v, Sort ty)
    {
        checkContextMatch(ty);
        return Expr.create(this,
                Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
    }

    public Expr mkNumeral(int v, Sort ty)
    {
        checkContextMatch(ty);
        return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
    }

    public Expr mkNumeral(long v, Sort ty)
    {
        checkContextMatch(ty);
        return Expr.create(this,
                Native.mkInt64(nCtx(), v, ty.getNativeObject()));
    }

    public RatNum mkReal(int num, int den)
    {
        if (den == 0)
            throw new Z3Exception("Denominator is zero");

        return new RatNum(this, Native.mkReal(nCtx(), num, den));
    }

    public RatNum mkReal(String v)
    {

        return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
                .getNativeObject()));
    }

    public RatNum mkReal(int v)
    {

        return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
                .getNativeObject()));
    }

    public RatNum mkReal(long v)
    {

        return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
                .getNativeObject()));
    }

    public IntNum mkInt(String v)
    {

        return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
                .getNativeObject()));
    }

    public IntNum mkInt(int v)
    {

        return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
                .getNativeObject()));
    }

    public IntNum mkInt(long v)
    {

        return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
                .getNativeObject()));
    }

    public BitVecNum mkBV(String v, int size)
    {
        return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
    }

    public BitVecNum mkBV(int v, int size)
    {
        return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
    }

    public BitVecNum mkBV(long v, int size)
    {
        return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
    }

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

        return new Quantifier(this, true, sorts, names, body, weight, patterns,
                noPatterns, quantifierID, skolemID);
    }

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

        return new Quantifier(this, true, boundConstants, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }

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

        return new Quantifier(this, false, sorts, names, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }

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

        return new Quantifier(this, false, boundConstants, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }

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

        if (universal)
            return mkForall(sorts, names, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
        else
            return mkExists(sorts, names, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
    }

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

        if (universal)
            return mkForall(boundConstants, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
        else
            return mkExists(boundConstants, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
    }

    public void setPrintMode(Z3_ast_print_mode value)
    {
        Native.setAstPrintMode(nCtx(), value.toInt());
    }

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

        return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
                attributes, (int) assumptions.length,
                AST.arrayToNative(assumptions), formula.getNativeObject());
    }

    public void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts,
            Symbol[] declNames, FuncDecl[] decls)
    {
        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));
    }

    public void parseSMTLIBFile(String fileName, Symbol[] sortNames,
            Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
           
    {
        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));
    }

    public int getNumSMTLIBFormulas()
    {
        return Native.getSmtlibNumFormulas(nCtx());
    }

    public BoolExpr[] getSMTLIBFormulas()
    {

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

    public int getNumSMTLIBAssumptions()
    {
        return Native.getSmtlibNumAssumptions(nCtx());
    }

    public BoolExpr[] getSMTLIBAssumptions()
    {

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

    public int getNumSMTLIBDecls()
    {
        return Native.getSmtlibNumDecls(nCtx());
    }

    public FuncDecl[] getSMTLIBDecls()
    {

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

    public int getNumSMTLIBSorts()
    {
        return Native.getSmtlibNumSorts(nCtx());
    }

    public Sort[] getSMTLIBSorts()
    {

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

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

        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)));
    }

    public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
            Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
           
    {

        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)));
    }

    public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
           
    {
        return new Goal(this, models, unsatCores, proofs);
    }

    public Params mkParams()
    {
        return new Params(this);
    }

    public int getNumTactics()
    {
        return Native.getNumTactics(nCtx());
    }

    public String[] getTacticNames()
    {

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

    public String getTacticDescription(String name)
    {
        return Native.tacticGetDescr(nCtx(), name);
    }

    public Tactic mkTactic(String name)
    {
        return new Tactic(this, name);
    }

    public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
           
    {
        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()));
    }

    public Tactic then(Tactic t1, Tactic t2, Tactic... ts)
    {
        return andThen(t1, t2, ts);
    }

    public Tactic orElse(Tactic t1, Tactic t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new Tactic(this, Native.tacticOrElse(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public Tactic tryFor(Tactic t, int ms)
    {
        checkContextMatch(t);
        return new Tactic(this, Native.tacticTryFor(nCtx(),
                t.getNativeObject(), ms));
    }

    public Tactic when(Probe p, Tactic t)
    {
        checkContextMatch(t);
        checkContextMatch(p);
        return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
                t.getNativeObject()));
    }

    public Tactic cond(Probe p, Tactic t1, Tactic t2)
    {
        checkContextMatch(p);
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public Tactic repeat(Tactic t, int max)
    {
        checkContextMatch(t);
        return new Tactic(this, Native.tacticRepeat(nCtx(),
                t.getNativeObject(), max));
    }

    public Tactic skip()
    {
        return new Tactic(this, Native.tacticSkip(nCtx()));
    }

    public Tactic fail()
    {
        return new Tactic(this, Native.tacticFail(nCtx()));
    }

    public Tactic failIf(Probe p)
    {
        checkContextMatch(p);
        return new Tactic(this,
                Native.tacticFailIf(nCtx(), p.getNativeObject()));
    }

    public Tactic failIfNotDecided()
    {
        return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
    }

    public Tactic usingParams(Tactic t, Params p)
    {
        checkContextMatch(t);
        checkContextMatch(p);
        return new Tactic(this, Native.tacticUsingParams(nCtx(),
                t.getNativeObject(), p.getNativeObject()));
    }

    public Tactic with(Tactic t, Params p)
    {
        return usingParams(t, p);
    }

    public Tactic parOr(Tactic... t)
    {
        checkContextMatch(t);
        return new Tactic(this, Native.tacticParOr(nCtx(),
                Tactic.arrayLength(t), Tactic.arrayToNative(t)));
    }

    public Tactic parAndThen(Tactic t1, Tactic t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new Tactic(this, Native.tacticParAndThen(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    public void interrupt()
    {
        Native.interrupt(nCtx());
    }

    public int getNumProbes()
    {
        return Native.getNumProbes(nCtx());
    }

    public String[] getProbeNames()
    {

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

    public String getProbeDescription(String name)
    {
        return Native.probeGetDescr(nCtx(), name);
    }

    public Probe mkProbe(String name)
    {
        return new Probe(this, name);
    }

    public Probe constProbe(double val)
    {
        return new Probe(this, Native.probeConst(nCtx(), val));
    }

    public Probe lt(Probe p1, Probe p2)
    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

    public Probe gt(Probe p1, Probe p2)
    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

    public Probe le(Probe p1, Probe p2)
    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

    public Probe ge(Probe p1, Probe p2)
    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

    public Probe eq(Probe p1, Probe p2)
    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

    public Probe and(Probe p1, Probe p2)
    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

    public Probe or(Probe p1, Probe p2)
    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

    public Probe not(Probe p)
    {
        checkContextMatch(p);
        return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
    }

    public Solver mkSolver()
    {
        return mkSolver((Symbol) null);
    }

    public Solver mkSolver(Symbol logic)
    {

        if (logic == null)
            return new Solver(this, Native.mkSolver(nCtx()));
        else
            return new Solver(this, Native.mkSolverForLogic(nCtx(),
                    logic.getNativeObject()));
    }

    public Solver mkSolver(String logic)
    {
        return mkSolver(mkSymbol(logic));
    }

    public Solver mkSimpleSolver()
    {
        return new Solver(this, Native.mkSimpleSolver(nCtx()));
    }

    public Solver mkSolver(Tactic t)
    {

        return new Solver(this, Native.mkSolverFromTactic(nCtx(),
                t.getNativeObject()));
    }

    public Fixedpoint mkFixedpoint()
    {
        return new Fixedpoint(this);
    }

    public Optimize mkOptimize()
    {
        return new Optimize(this);
    }

    
    public FPRMSort mkFPRoundingModeSort()
    {
        return new FPRMSort(this);
    }

    public FPRMExpr mkFPRoundNearestTiesToEven()
    {
        return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
    }

    public FPRMNum mkFPRNE()
    {
        return new FPRMNum(this, Native.mkFpaRne(nCtx()));
    }

    public FPRMNum mkFPRoundNearestTiesToAway()
    {
        return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
    }

    public FPRMNum mkFPRNA()
    {
        return new FPRMNum(this, Native.mkFpaRna(nCtx()));
    }

    public FPRMNum mkFPRoundTowardPositive()
    {
        return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
    }

    public FPRMNum mkFPRTP()
    {
        return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
    }

    public FPRMNum mkFPRoundTowardNegative()
    {
        return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
    }

    public FPRMNum mkFPRTN()
    {
        return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
    }

    public FPRMNum mkFPRoundTowardZero()
    {
        return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
    }

    public FPRMNum mkFPRTZ()
    {
        return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
    }        

    public FPSort mkFPSort(int ebits, int sbits)
    {
        return new FPSort(this, ebits, sbits);
    }

    public FPSort mkFPSortHalf()
    {
        return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
    }

    public FPSort mkFPSort16()
    {
        return new FPSort(this, Native.mkFpaSort16(nCtx()));
    }

    public FPSort mkFPSortSingle()
    {
        return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
    }

    public FPSort mkFPSort32()
    {
        return new FPSort(this, Native.mkFpaSort32(nCtx()));
    }

    public FPSort mkFPSortDouble()
    {
        return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
    }

    public FPSort mkFPSort64()
    {
        return new FPSort(this, Native.mkFpaSort64(nCtx()));
    }

    public FPSort mkFPSortQuadruple()
    {        
        return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
    }

    public FPSort mkFPSort128()
    {
        return new FPSort(this, Native.mkFpaSort128(nCtx()));
    }


    public FPNum mkFPNaN(FPSort s)
    {
        return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
    }

    public FPNum mkFPInf(FPSort s, boolean negative)
    {
        return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
    }

    public FPNum mkFPZero(FPSort s, boolean negative)
    {
        return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
    }

    public FPNum mkFPNumeral(float v, FPSort s)
    {
        return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
    }

    public FPNum mkFPNumeral(double v, FPSort s)
    {
        return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
    }

    public FPNum mkFPNumeral(int v, FPSort s)
    {
        return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
    }

    public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
    {
        return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));    
    }

    public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
    {
        return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
    }

    public FPNum mkFP(float v, FPSort s)
    {
        return mkFPNumeral(v, s);
    }

    public FPNum mkFP(double v, FPSort s)
    {
        return mkFPNumeral(v, s);
    }

    public FPNum mkFP(int v, FPSort s)
    {
        return mkFPNumeral(v, s);
    }

    public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
    {
        return mkFPNumeral(sgn, sig, exp, s);
    }

    public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
    {
        return mkFPNumeral(sgn, sig, exp, s);
    }


    public FPExpr mkFPAbs(FPExpr t) 
    {
        return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
    }

    public FPExpr mkFPNeg(FPExpr t) 
    {
        return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
    }

    public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2) 
    {
        return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2) 
    {
        return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2) 
    {
        return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2) 
    {
        return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) 
    {
        return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
    }

    public FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t) 
    {
        return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
    }

    public FPExpr mkFPRem(FPExpr t1, FPExpr t2) 
    {
        return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
    {            
        return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
    }

    public FPExpr mkFPMin(FPExpr t1, FPExpr t2)
    {
        return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public FPExpr mkFPMax(FPExpr t1, FPExpr t2)
    {
        return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }   
    
    public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2) 
    {            
        return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public BoolExpr mkFPLt(FPExpr t1, FPExpr t2) 
    {                    
        return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2) 
    {                    
        return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public BoolExpr mkFPGt(FPExpr t1, FPExpr t2) 
    {            
        return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
    {
        return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }

    public BoolExpr mkFPIsNormal(FPExpr t) 
    {
        return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
    }

    public BoolExpr mkFPIsSubnormal(FPExpr t) 
    {                   
        return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
    }

    public BoolExpr mkFPIsZero(FPExpr t)
    {
        return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
    }

    public BoolExpr mkFPIsInfinite(FPExpr t)
    {    
        return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
    }

    public BoolExpr mkFPIsNaN(FPExpr t) 
    {                   
        return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
    }

    public BoolExpr mkFPIsNegative(FPExpr t)
    {     
        return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
    }

    public BoolExpr mkFPIsPositive(FPExpr t)
    {
        return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
    }        

    public FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
    {
        return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
    }

    public FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
    {
        return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
    }

    public FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
    {
        return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
    }

    public FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
    {
        return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
    }

    public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
    {
        if (signed)
            return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
        else
            return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
    }

    public FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
    {
        return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
    }

    public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
    {
        if (signed)
            return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
        else
            return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
    }

    public RealExpr mkFPToReal(FPExpr t)
    {
        return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
    }

    public BitVecExpr mkFPToIEEEBV(FPExpr t)
    {
        return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
    }

    public BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
    {
        return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
    }
    
    
    public AST wrapAST(long nativeObject)
    {
        return AST.create(this, nativeObject);
    }

    public long unwrapAST(AST a)
    {
        return a.getNativeObject();
    }

    public String SimplifyHelp()
    {
        return Native.simplifyGetHelp(nCtx());
    }

    public ParamDescrs getSimplifyParameterDescriptions()
    {
        return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
    }

    public void updateParamValue(String id, String value)
    {
        Native.updateParamValue(nCtx(), id, value);
    }

    long m_ctx = 0;

    long nCtx()
    {
        return m_ctx;
    }

    void initContext()
    {
        setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
        Native.setInternalErrorHandler(nCtx());
    }

    void checkContextMatch(Z3Object other)
    {
        if (this != other.getContext())
            throw new Z3Exception("Context mismatch");
    }

    void checkContextMatch(Z3Object[] arr)
    {
        if (arr != null)
            for (Z3Object a : arr)
                checkContextMatch(a);
    }

    private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
    private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(10);
    private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(10);
    private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(10);
    private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(10);
    private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(10);
    private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(10);
    private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(10);
    private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(10);
    private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(10);
    private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(10);
    private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(10);
    private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(10);
    private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10);
    private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10);
    private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(10);

    public IDecRefQueue getASTDRQ()
    {
        return m_AST_DRQ;
    }

    public IDecRefQueue getASTMapDRQ()
    {
        return m_ASTMap_DRQ;
    }

    public IDecRefQueue getASTVectorDRQ()
    {
        return m_ASTVector_DRQ;
    }

    public IDecRefQueue getApplyResultDRQ()
    {
        return m_ApplyResult_DRQ;
    }

    public IDecRefQueue getFuncEntryDRQ()
    {
        return m_FuncEntry_DRQ;
    }

    public IDecRefQueue getFuncInterpDRQ()
    {
        return m_FuncInterp_DRQ;
    }

    public IDecRefQueue getGoalDRQ()
    {
        return m_Goal_DRQ;
    }

    public IDecRefQueue getModelDRQ()
    {
        return m_Model_DRQ;
    }

    public IDecRefQueue getParamsDRQ()
    {
        return m_Params_DRQ;
    }

    public IDecRefQueue getParamDescrsDRQ()
    {
        return m_ParamDescrs_DRQ;
    }

    public IDecRefQueue getProbeDRQ()
    {
        return m_Probe_DRQ;
    }

    public IDecRefQueue getSolverDRQ()
    {
        return m_Solver_DRQ;
    }

    public IDecRefQueue getStatisticsDRQ()
    {
        return m_Statistics_DRQ;
    }

    public IDecRefQueue getTacticDRQ()
    {
        return m_Tactic_DRQ;
    }

    public IDecRefQueue getFixedpointDRQ()
    {
        return m_Fixedpoint_DRQ;
    }

    public IDecRefQueue getOptimizeDRQ()
    {
        return m_Optimize_DRQ;
    }

    protected long m_refCount = 0;

    protected void finalize()
    {
        dispose();

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

    public void dispose()
    {
        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;
    }
}