Context.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import static com.microsoft.z3.Constructor.of;
 
import com.microsoft.z3.enumerations.Z3_ast_print_mode;
 
import java.util.Map;
 
@SuppressWarnings("unchecked")
public class Context implements AutoCloseable {
    private long m_ctx;
    static final Object creation_lock = new Object();
 
    public Context () {
        synchronized (creation_lock) {
            m_ctx = Native.mkContextRc(0);
            init();
        }
    }
 
    protected Context (long m_ctx) {
        synchronized (creation_lock) {
            this.m_ctx = m_ctx;
            init();
        }
    }
 
 
    public Context(Map<String, String> settings) {
        synchronized (creation_lock) {
            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);
            init();
        }
    }
 
    private void init() {
        setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
        Native.setInternalErrorHandler(m_ctx);
    }
 
    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 new Symbol[0];
        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;
    private SeqSort<CharSort> m_stringSort = 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 CharSort mkCharSort()
    {
        return new CharSort(this);
    }
 
    public SeqSort<CharSort> getStringSort()
    {
        if (m_stringSort == null) {
            m_stringSort = mkStringSort();
        }
        return m_stringSort;
    }
 
    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 final <D extends Sort, R extends Sort> ArraySort<D, R> mkArraySort(D domain, R range)
    {
        checkContextMatch(domain);
        checkContextMatch(range);
        return new ArraySort<>(this, domain, range);
    }
 
 
    public final <R extends Sort> ArraySort<Sort, R> mkArraySort(Sort[] domains, R range)
    {
        checkContextMatch(domains);
        checkContextMatch(range);
        return new ArraySort<>(this, domains, range);
    }
 
    public SeqSort<CharSort> mkStringSort()
    {
        return new SeqSort<>(this, Native.mkStringSort(nCtx()));
    }
 
    public final <R extends Sort> SeqSort<R> mkSeqSort(R s)
    {
        return new SeqSort<>(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
    }
 
    public final <R extends Sort> ReSort<R> mkReSort(R s)
    {
        return new ReSort<>(this, Native.mkReSort(nCtx(), s.getNativeObject()));
    }
 
 
    public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames,
            Sort[] fieldSorts)
    {
        checkContextMatch(name);
        checkContextMatch(fieldNames);
        checkContextMatch(fieldSorts);
        return new TupleSort(this, name, fieldNames.length, fieldNames,
                fieldSorts);
    }
 
    public final <R> EnumSort<R> mkEnumSort(Symbol name, Symbol... enumNames)
 
    {
        checkContextMatch(name);
        checkContextMatch(enumNames);
        return new EnumSort<>(this, name, enumNames);
    }
 
    public final <R> EnumSort<R> mkEnumSort(String name, String... enumNames)
 
    {
        return new EnumSort<>(this, mkSymbol(name), mkSymbols(enumNames));
    }
 
    public final <R extends Sort> ListSort<R> mkListSort(Symbol name, R elemSort)
    {
        checkContextMatch(name);
        checkContextMatch(elemSort);
        return new ListSort<>(this, name, elemSort);
    }
 
    public final <R extends Sort> ListSort<R> mkListSort(String name, R elemSort)
    {
        checkContextMatch(elemSort);
        return new ListSort<>(this, mkSymbol(name), elemSort);
    }
 
    public final <R> FiniteDomainSort<R> mkFiniteDomainSort(Symbol name, long size)
 
    {
        checkContextMatch(name);
        return new FiniteDomainSort<>(this, name, size);
    }
 
    public final <R> FiniteDomainSort<R> mkFiniteDomainSort(String name, long size)
 
    {
        return new FiniteDomainSort<>(this, mkSymbol(name), size);
    }
 
    public final <R> Constructor<R> mkConstructor(Symbol name, Symbol recognizer,
            Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
 
    {
        return of(this, name, recognizer, fieldNames, sorts, sortRefs);
    }
 
    public final <R> Constructor<R> mkConstructor(String name, String recognizer,
            String[] fieldNames, Sort[] sorts, int[] sortRefs)
    {
        return of(this, mkSymbol(name), mkSymbol(recognizer), mkSymbols(fieldNames), sorts, sortRefs);
    }
 
    public final <R> DatatypeSort<R> mkDatatypeSort(Symbol name, Constructor<R>[] constructors)
    {
        checkContextMatch(name);
        checkContextMatch(constructors);
        return new DatatypeSort<>(this, name, constructors);
    }
 
    public final <R> DatatypeSort<R> mkDatatypeSort(String name, Constructor<R>[] constructors)
 
    {
        checkContextMatch(constructors);
        return new DatatypeSort<>(this, mkSymbol(name), constructors);
    }
 
    public <R> DatatypeSort<R> mkDatatypeSortRef(Symbol name, Sort[] params)
    {
        checkContextMatch(name);
        if (params != null)
            checkContextMatch(params);
        
        int numParams = (params == null) ? 0 : params.length;
        long[] paramsNative = (params == null) ? new long[0] : AST.arrayToNative(params);
        return new DatatypeSort<>(this, Native.mkDatatypeSort(nCtx(), name.getNativeObject(), numParams, paramsNative));
    }
 
    public <R> DatatypeSort<R> mkDatatypeSortRef(Symbol name)
    {
        return mkDatatypeSortRef(name, null);
    }
 
    public <R> DatatypeSort<R> mkDatatypeSortRef(String name, Sort[] params)
    {
        return mkDatatypeSortRef(mkSymbol(name), params);
    }
 
    public <R> DatatypeSort<R> mkDatatypeSortRef(String name)
    {
        return mkDatatypeSortRef(name, null);
    }
 
    public DatatypeSort<Object>[] mkDatatypeSorts(Symbol[] names, Constructor<Object>[][] c)
    {
        checkContextMatch(names);
        int n = names.length;
        ConstructorList<Object>[] cla = new ConstructorList[n];
        long[] n_constr = new long[n];
        for (int i = 0; i < n; i++)
        {
            Constructor<Object>[] 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<Object>[] res = new DatatypeSort[n];
        for (int i = 0; i < n; i++)
            res[i] = new DatatypeSort<>(this, n_res[i]);
        return res;
    }
 
    public DatatypeSort<Object>[] mkDatatypeSorts(String[] names, Constructor<Object>[][] c)
 
    {
        return mkDatatypeSorts(mkSymbols(names), c);
    }
 
    public final <F extends Sort, R extends Sort> Expr<R> mkUpdateField(FuncDecl<F> field, Expr<R> t, Expr<F> v)
        throws Z3Exception
    {
        return (Expr<R>) Expr.create(this,
                            Native.datatypeUpdateField
                            (nCtx(), field.getNativeObject(),
                             t.getNativeObject(), v.getNativeObject()));
    }
 
 
    public final <R extends Sort> FuncDecl<R> mkFuncDecl(Symbol name, Sort[] domain, R range)
    {
        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl<>(this, name, domain, range);
    }
 
    public final <R extends Sort> FuncDecl<R> mkPropagateFunction(Symbol name, Sort[] domain, R range)
    {
        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        long f = Native.solverPropagateDeclare(
            this.nCtx(), 
            name.getNativeObject(), 
            AST.arrayLength(domain), 
            AST.arrayToNative(domain),
            range.getNativeObject());
        return new FuncDecl<>(this, f);
    }
 
 
    public final <R extends Sort> FuncDecl<R> mkFuncDecl(Symbol name, Sort domain, R range)
 
    {
        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        Sort[] q = new Sort[] { domain };
        return new FuncDecl<>(this, name, q, range);
    }
 
    public final <R extends Sort> FuncDecl<R> mkFuncDecl(String name, Sort[] domain, R range)
 
    {
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl<>(this, mkSymbol(name), domain, range);
    }
 
    public final <R extends Sort> FuncDecl<R> mkFuncDecl(String name, Sort domain, R range)
 
    {
        checkContextMatch(domain);
        checkContextMatch(range);
        Sort[] q = new Sort[] { domain };
        return new FuncDecl<>(this, mkSymbol(name), q, range);
    }
 
    public final <R extends Sort> FuncDecl<R> mkRecFuncDecl(Symbol name, Sort[] domain, R range)
    {
        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl<>(this, name, domain, range, true);
    }
 
 
    public final <R extends Sort> void AddRecDef(FuncDecl<R> f, Expr<?>[] args, Expr<R> body)
    {
        checkContextMatch(f);
        checkContextMatch(args);
        checkContextMatch(body);
        long[] argsNative = AST.arrayToNative(args);
        Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject());
    }
 
    public final <R extends Sort> FuncDecl<R> mkFreshFuncDecl(String prefix, Sort[] domain, R range)
 
    {
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl<>(this, prefix, domain, range);
    }
 
    public final <R extends Sort> FuncDecl<R> mkConstDecl(Symbol name, R range)
    {
        checkContextMatch(name);
        checkContextMatch(range);
        return new FuncDecl<>(this, name, null, range);
    }
 
    public final <R extends Sort> FuncDecl<R> mkConstDecl(String name, R range)
    {
        checkContextMatch(range);
        return new FuncDecl<>(this, mkSymbol(name), null, range);
    }
 
    public final <R extends Sort> FuncDecl<R> mkFreshConstDecl(String prefix, R range)
 
    {
        checkContextMatch(range);
        return new FuncDecl<>(this, prefix, null, range);
    }
 
    public final <R extends Sort> Expr<R> mkBound(int index, R ty)
    {
        return (Expr<R>) Expr.create(this,
                Native.mkBound(nCtx(), index, ty.getNativeObject()));
    }
 
    @SafeVarargs
    public final 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(), terms.length,
                termsNative));
    }
 
    public final <R extends Sort> Expr<R> mkConst(Symbol name, R range)
    {
        checkContextMatch(name);
        checkContextMatch(range);
 
        return (Expr<R>) Expr.create(
                this,
                Native.mkConst(nCtx(), name.getNativeObject(),
                        range.getNativeObject()));
    }
 
    public final <R extends Sort> Expr<R> mkConst(String name, R range)
    {
        return mkConst(mkSymbol(name), range);
    }
 
    public final <R extends Sort> Expr<R> mkFreshConst(String prefix, R range)
    {
        checkContextMatch(range);
        return (Expr<R>) Expr.create(this,
                Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
    }
 
    public final <R extends Sort> Expr<R> mkConst(FuncDecl<R> 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));
    }
 
    @SafeVarargs
    public final <R extends Sort> Expr<R> mkApp(FuncDecl<R> 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()));
    }
 
    @SafeVarargs
    public final BoolExpr mkDistinct(Expr<?>... args)
    {
        checkContextMatch(args);
        return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
                AST.arrayToNative(args)));
    }
 
    public final BoolExpr mkNot(Expr<BoolSort> a)
    {
        checkContextMatch(a);
        return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
    }
 
    public final <R extends Sort> Expr<R> mkITE(Expr<BoolSort> t1, Expr<? extends R> t2, Expr<? extends R> t3)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        checkContextMatch(t3);
        return (Expr<R>) Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
                t2.getNativeObject(), t3.getNativeObject()));
    }
 
    public BoolExpr mkIff(Expr<BoolSort> t1, Expr<BoolSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkImplies(Expr<BoolSort> t1, Expr<BoolSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkImplies(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkXor(Expr<BoolSort> t1, Expr<BoolSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    @SafeVarargs
    public final BoolExpr mkAnd(Expr<BoolSort>... t)
    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
                AST.arrayToNative(t)));
    }
 
    @SafeVarargs
    public final BoolExpr mkOr(Expr<BoolSort>... t)
    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
                AST.arrayToNative(t)));
    }
 
    @SafeVarargs
    public final <R extends ArithSort> ArithExpr<R> mkAdd(Expr<? extends R>... t)
    {
        checkContextMatch(t);
        return (ArithExpr<R>) Expr.create(this,
                Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
    }
 
    @SafeVarargs
    public final <R extends ArithSort> ArithExpr<R> mkMul(Expr<? extends R>... t)
    {
        checkContextMatch(t);
        return (ArithExpr<R>) Expr.create(this,
                Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
    }
 
    @SafeVarargs
    public final <R extends ArithSort> ArithExpr<R> mkSub(Expr<? extends R>... t)
    {
        checkContextMatch(t);
        return (ArithExpr<R>) Expr.create(this,
                Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
    }
 
    public final <R extends ArithSort> ArithExpr<R> mkUnaryMinus(Expr<R> t)
    {
        checkContextMatch(t);
        return (ArithExpr<R>) Expr.create(this,
                Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
    }
 
    public final <R extends ArithSort> ArithExpr<R> mkDiv(Expr<? extends R> t1, Expr<? extends R> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return (ArithExpr<R>) Expr.create(this, Native.mkDiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public IntExpr mkMod(Expr<IntSort> t1, Expr<IntSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public IntExpr mkRem(Expr<IntSort> t1, Expr<IntSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public final <R extends ArithSort> ArithExpr<R> mkPower(Expr<? extends R> t1,
            Expr<? extends R> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return (ArithExpr<R>) Expr.create(
                this,
                Native.mkPower(nCtx(), t1.getNativeObject(),
                        t2.getNativeObject()));
    }
 
    public BoolExpr mkLt(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkLe(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkGt(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkGe(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public RealExpr mkInt2Real(Expr<IntSort> t)
    {
        checkContextMatch(t);
        return new RealExpr(this,
                Native.mkInt2real(nCtx(), t.getNativeObject()));
    }
 
    public IntExpr mkReal2Int(Expr<RealSort> t)
    {
        checkContextMatch(t);
        return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
    }
 
    public BoolExpr mkIsInteger(Expr<RealSort> t)
    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
    }
 
    public BitVecExpr mkBVNot(Expr<BitVecSort> t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
    }
 
    public BitVecExpr mkBVRedAND(Expr<BitVecSort> t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvredand(nCtx(),
                t.getNativeObject()));
    }
 
    public BitVecExpr mkBVRedOR(Expr<BitVecSort> t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvredor(nCtx(),
                t.getNativeObject()));
    }
 
    public BitVecExpr mkBVAND(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvand(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVXOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvxor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVNAND(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvnand(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVNOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvnor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVXNOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVNeg(Expr<BitVecSort> t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
    }
 
    public BitVecExpr mkBVAdd(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvadd(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVSub(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsub(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVMul(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvmul(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVUDiv(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVSDiv(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVURem(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvurem(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVSRem(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVSMod(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkBVULT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkBVSLT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkBVULE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkBVSLE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkBVUGE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkBVSGE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkBVUGT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BoolExpr mkBVSGT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }
 
    public BitVecExpr mkConcat(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkConcat(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkExtract(int high, int low, Expr<BitVecSort> t)
 
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
                t.getNativeObject()));
    }
 
    public BitVecExpr mkSignExt(int i, Expr<BitVecSort> t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
                t.getNativeObject()));
    }
 
    public BitVecExpr mkZeroExt(int i, Expr<BitVecSort> t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
                t.getNativeObject()));
    }
 
    public BitVecExpr mkRepeat(int i, Expr<BitVecSort> t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
                t.getNativeObject()));
    }
 
    public BitVecExpr mkBVSHL(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvshl(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVLSHR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVASHR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvashr(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVRotateLeft(int i, Expr<BitVecSort> t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
                t.getNativeObject()));
    }
 
    public BitVecExpr mkBVRotateRight(int i, Expr<BitVecSort> t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
                t.getNativeObject()));
    }
 
    public BitVecExpr mkBVRotateLeft(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkBVRotateRight(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BitVecExpr mkInt2BV(int n, Expr<IntSort> t)
    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
                t.getNativeObject()));
    }
 
    public IntExpr mkBV2Int(Expr<BitVecSort> t, boolean signed)
    {
        checkContextMatch(t);
        return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
            (signed)));
    }
 
    public BoolExpr mkBVAddNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2,
            boolean isSigned)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned)));
    }
 
    public BoolExpr mkBVAddNoUnderflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkBVSubNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkBVSubNoUnderflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2,
            boolean isSigned)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned)));
    }
 
    public BoolExpr mkBVSDivNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkBVNegNoOverflow(Expr<BitVecSort> t)
    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
                t.getNativeObject()));
    }
 
    public BoolExpr mkBVMulNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2,
            boolean isSigned)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned)));
    }
 
    public BoolExpr mkBVMulNoUnderflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public final <D extends Sort, R extends Sort> ArrayExpr<D, R> mkArrayConst(Symbol name, D domain, R range)
 
    {
        return (ArrayExpr<D, R>) mkConst(name, mkArraySort(domain, range));
    }
 
    public final <D extends Sort, R extends Sort> ArrayExpr<D, R> mkArrayConst(String name, D domain, R range)
 
    {
        return (ArrayExpr<D, R>) mkConst(mkSymbol(name), mkArraySort(domain, range));
    }
 
    public final <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
    {
        checkContextMatch(a);
        checkContextMatch(i);
        return (Expr<R>) Expr.create(
                this,
                Native.mkSelect(nCtx(), a.getNativeObject(),
                        i.getNativeObject()));
    }
 
    public final <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort, R>> a, Expr<?>[] args)
    {
        checkContextMatch(a);
        checkContextMatch(args);
        return (Expr<R>) Expr.create(
                this,
                Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
    }
 
    public final <D extends Sort, R extends Sort> ArrayExpr<D, R> mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)
    {
        checkContextMatch(a);
        checkContextMatch(i);
        checkContextMatch(v);
        return new ArrayExpr<>(this, Native.mkStore(nCtx(), a.getNativeObject(),
                i.getNativeObject(), v.getNativeObject()));
    }
 
    public final <R extends Sort> ArrayExpr<Sort, R> mkStore(Expr<ArraySort<Sort, R>> a, Expr<?>[] args, Expr<R> v)
    {
        checkContextMatch(a);
        checkContextMatch(args);
        checkContextMatch(v);
        return new ArrayExpr<>(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
                             args.length, AST.arrayToNative(args), v.getNativeObject()));
    }
 
    public final <D extends Sort, R extends Sort> ArrayExpr<D, R> mkConstArray(D domain, Expr<R> v)
    {
        checkContextMatch(domain);
        checkContextMatch(v);
        return new ArrayExpr<>(this, Native.mkConstArray(nCtx(),
                domain.getNativeObject(), v.getNativeObject()));
    }
 
    @SafeVarargs
    public final <D extends Sort, R1 extends Sort, R2 extends Sort> ArrayExpr<D, R2> mkMap(FuncDecl<R2> f, Expr<ArraySort<D, R1>>... args)
    {
        checkContextMatch(f);
        checkContextMatch(args);
        return (ArrayExpr<D, R2>) Expr.create(this, Native.mkMap(nCtx(),
                f.getNativeObject(), AST.arrayLength(args),
                AST.arrayToNative(args)));
    }
 
    public final <D extends Sort, R extends Sort> Expr<R> mkTermArray(Expr<ArraySort<D, R>> array)
    {
        checkContextMatch(array);
        return (Expr<R>) Expr.create(this,
                Native.mkArrayDefault(nCtx(), array.getNativeObject()));
    }
 
    public final <D extends Sort, R extends Sort> Expr<D> mkArrayExt(Expr<ArraySort<D, R>> arg1, Expr<ArraySort<D, R>> arg2)
    {
    checkContextMatch(arg1);
    checkContextMatch(arg2);
    return (Expr<D>) Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
    }
 
 
    public final <D extends Sort> SetSort<D> mkSetSort(D ty)
    {
        checkContextMatch(ty);
        return new SetSort<>(this, ty);
    }
 
    public final <D extends Sort> ArrayExpr<D, BoolSort> mkEmptySet(D domain)
    {
        checkContextMatch(domain);
        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                Native.mkEmptySet(nCtx(), domain.getNativeObject()));
    }
 
    public final <D extends Sort> ArrayExpr<D, BoolSort> mkFullSet(D domain)
    {
        checkContextMatch(domain);
        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                Native.mkFullSet(nCtx(), domain.getNativeObject()));
    }
 
    public final <D extends Sort> ArrayExpr<D, BoolSort> mkSetAdd(Expr<ArraySort<D, BoolSort>> set, Expr<D> element)
    {
        checkContextMatch(set);
        checkContextMatch(element);
        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                Native.mkSetAdd(nCtx(), set.getNativeObject(),
                        element.getNativeObject()));
    }
 
    public final <D extends Sort> ArrayExpr<D, BoolSort> mkSetDel(Expr<ArraySort<D, BoolSort>> set, Expr<D> element)
    {
        checkContextMatch(set);
        checkContextMatch(element);
        return (ArrayExpr<D, BoolSort>)Expr.create(this,
                Native.mkSetDel(nCtx(), set.getNativeObject(),
                        element.getNativeObject()));
    }
 
    @SafeVarargs
    public final <D extends Sort> ArrayExpr<D, BoolSort> mkSetUnion(Expr<ArraySort<D, BoolSort>>... args)
    {
        checkContextMatch(args);
        return (ArrayExpr<D, BoolSort>)Expr.create(this,
                Native.mkSetUnion(nCtx(), args.length,
                        AST.arrayToNative(args)));
    }
 
    @SafeVarargs
    public final <D extends Sort> ArrayExpr<D, BoolSort> mkSetIntersection(Expr<ArraySort<D, BoolSort>>... args)
    {
        checkContextMatch(args);
        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                Native.mkSetIntersect(nCtx(), args.length,
                        AST.arrayToNative(args)));
    }
 
    public final <D extends Sort> ArrayExpr<D, BoolSort> mkSetDifference(Expr<ArraySort<D, BoolSort>> arg1, Expr<ArraySort<D, BoolSort>> arg2)
    {
        checkContextMatch(arg1);
        checkContextMatch(arg2);
        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
                        arg2.getNativeObject()));
    }
 
    public final <D extends Sort> ArrayExpr<D, BoolSort> mkSetComplement(Expr<ArraySort<D, BoolSort>> arg)
    {
        checkContextMatch(arg);
        return (ArrayExpr<D, BoolSort>)Expr.create(this,
                Native.mkSetComplement(nCtx(), arg.getNativeObject()));
    }
 
    public final <D extends Sort> BoolExpr mkSetMembership(Expr<D> elem, Expr<ArraySort<D, BoolSort>> set)
    {
        checkContextMatch(elem);
        checkContextMatch(set);
        return (BoolExpr) Expr.create(this,
                Native.mkSetMember(nCtx(), elem.getNativeObject(),
                        set.getNativeObject()));
    }
 
    public final <D extends Sort> BoolExpr mkSetSubset(Expr<ArraySort<D, BoolSort>> arg1, Expr<ArraySort<D, BoolSort>> arg2)
    {
        checkContextMatch(arg1);
        checkContextMatch(arg2);
        return (BoolExpr) Expr.create(this,
                Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
                        arg2.getNativeObject()));
    }
 
 
    public final <R extends Sort> SeqExpr<R> mkEmptySeq(R s)
    {
        checkContextMatch(s);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
    }
 
    public final <R extends Sort> SeqExpr<R> mkUnit(Expr<R> elem)
    {
        checkContextMatch(elem);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
    }
 
    public SeqExpr<CharSort> mkString(String s)
    {
        StringBuilder buf = new StringBuilder();
        for (int i = 0; i < s.length(); i += Character.charCount(s.codePointAt(i))) {
            int code = s.codePointAt(i);
            if (code <= 32 || 127 < code) 
                buf.append(String.format("\\u{%x}", code));
            else
                buf.append(s.charAt(i));
        }
        return (SeqExpr<CharSort>) Expr.create(this, Native.mkString(nCtx(), buf.toString()));
    }
 
    public SeqExpr<CharSort> intToString(Expr<IntSort> e)
    {
        return (SeqExpr<CharSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
    }
 
    public SeqExpr<CharSort> ubvToString(Expr<BitVecSort> e)
    {
        return (SeqExpr<CharSort>) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
    }
    
    public SeqExpr<CharSort> sbvToString(Expr<BitVecSort> e)
    {
        return (SeqExpr<CharSort>) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject()));
    }
    
    public IntExpr stringToInt(Expr<SeqSort<CharSort>> e)
    {
        return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
    }
 
    @SafeVarargs
    public final <R extends Sort> SeqExpr<R> mkConcat(Expr<SeqSort<R>>... t)
    {
        checkContextMatch(t);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
    }
 
 
    public final <R extends Sort> IntExpr mkLength(Expr<SeqSort<R>> s)
    {
        checkContextMatch(s);
        return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
    }
 
    public final <R extends Sort> BoolExpr mkPrefixOf(Expr<SeqSort<R>> s1, Expr<SeqSort<R>> s2)
    {
        checkContextMatch(s1, s2);
        return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
    }
 
    public final <R extends Sort> BoolExpr mkSuffixOf(Expr<SeqSort<R>> s1, Expr<SeqSort<R>> s2)
    {
        checkContextMatch(s1, s2);
        return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
    }
 
    public final <R extends Sort> BoolExpr mkContains(Expr<SeqSort<R>> s1, Expr<SeqSort<R>> s2)
    {
        checkContextMatch(s1, s2);
        return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
    }
 
    public BoolExpr MkStringLt(Expr<SeqSort<CharSort>> s1, Expr<SeqSort<CharSort>> s2) 
    {
        checkContextMatch(s1, s2);
        return new BoolExpr(this, Native.mkStrLt(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
    }
 
    public BoolExpr MkStringLe(Expr<SeqSort<CharSort>> s1, Expr<SeqSort<CharSort>> s2)
    {
        checkContextMatch(s1, s2);
        return new BoolExpr(this, Native.mkStrLe(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
    }
 
 
    public final <R extends Sort> SeqExpr<R> mkAt(Expr<SeqSort<R>> s, Expr<IntSort> index)
    {
        checkContextMatch(s, index);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
    }
 
    public final <R extends Sort> Expr<R> mkNth(Expr<SeqSort<R>> s, Expr<IntSort> index)
    {
        checkContextMatch(s, index);
        return (Expr<R>) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
    }
 
 
    public final <R extends Sort> SeqExpr<R> mkExtract(Expr<SeqSort<R>> s, Expr<IntSort> offset, Expr<IntSort> length)
    {
        checkContextMatch(s, offset, length);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
    }
 
    public final <R extends Sort> IntExpr mkIndexOf(Expr<SeqSort<R>> s, Expr<SeqSort<R>> substr, Expr<IntSort> offset)
    {
        checkContextMatch(s, substr, offset);
        return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
    }
 
    public final <R extends Sort> IntExpr mkLastIndexOf(Expr<SeqSort<R>> s, Expr<SeqSort<R>> substr)
    {
        checkContextMatch(s, substr);
        return (IntExpr)Expr.create(this, Native.mkSeqLastIndex(nCtx(), s.getNativeObject(), substr.getNativeObject()));
    }
 
    public final <R extends Sort> SeqExpr<R> mkReplace(Expr<SeqSort<R>> s, Expr<SeqSort<R>> src, Expr<SeqSort<R>> dst)
    {
        checkContextMatch(s, src, dst);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
    }
 
    public final <R extends Sort> SeqExpr<R> mkReplaceAll(Expr<SeqSort<R>> s, Expr<SeqSort<R>> src, Expr<SeqSort<R>> dst)
    {
        checkContextMatch(s, src, dst);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplaceAll(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
    }
 
    public final <R extends Sort> SeqExpr<R> mkReplaceRe(Expr<SeqSort<R>> s, ReExpr<SeqSort<R>> re, Expr<SeqSort<R>> dst)
    {
        checkContextMatch(s, re, dst);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplaceRe(nCtx(), s.getNativeObject(), re.getNativeObject(), dst.getNativeObject()));
    }
 
    public final <R extends Sort> SeqExpr<R> mkReplaceReAll(Expr<SeqSort<R>> s, ReExpr<SeqSort<R>> re, Expr<SeqSort<R>> dst)
    {
        checkContextMatch(s, re, dst);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplaceReAll(nCtx(), s.getNativeObject(), re.getNativeObject(), dst.getNativeObject()));
    }
 
    public final <R extends Sort> ReExpr<SeqSort<R>> mkToRe(Expr<SeqSort<R>> s)
    {
        checkContextMatch(s);
        return (ReExpr<SeqSort<R>>) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
    }
 
 
    public final <R extends Sort> BoolExpr mkInRe(Expr<SeqSort<R>> s, ReExpr<SeqSort<R>> re)
    {
        checkContextMatch(s, re);
        return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
    }
 
    public final <R extends Sort> ReExpr<R> mkStar(Expr<ReSort<R>> re)
    {
        checkContextMatch(re);
        return (ReExpr<R>) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
    }
 
    public final <R extends Sort> ReExpr<R> mkPower(Expr<ReSort<R>> re, int n)
    {
        return (ReExpr<R>) Expr.create(this, Native.mkRePower(nCtx(), re.getNativeObject(), n));
    }
 
    public final <R extends Sort> ReExpr<R> mkLoop(Expr<ReSort<R>> re, int lo, int hi)
    {
        return (ReExpr<R>) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
    }
 
    public final <R extends Sort> ReExpr<R> mkLoop(Expr<ReSort<R>> re, int lo)
    {
        return (ReExpr<R>) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
    }
 
 
    public final <R extends Sort> ReExpr<R> mkPlus(Expr<ReSort<R>> re)
    {
        checkContextMatch(re);
        return (ReExpr<R>) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
    }
 
    public final <R extends Sort> ReExpr<R> mkOption(Expr<ReSort<R>> re)
    {
        checkContextMatch(re);
        return (ReExpr<R>) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
    }
 
    public final <R extends Sort> ReExpr<R> mkComplement(Expr<ReSort<R>> re)
    {
        checkContextMatch(re);
        return (ReExpr<R>) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
    }
 
    @SafeVarargs
    public final <R extends Sort> ReExpr<R> mkConcat(ReExpr<R>... t)
    {
        checkContextMatch(t);
        return (ReExpr<R>) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
    }
 
    @SafeVarargs
    public final <R extends Sort> ReExpr<R> mkUnion(Expr<ReSort<R>>... t)
    {
        checkContextMatch(t);
        return (ReExpr<R>) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
    }
 
    @SafeVarargs
    public final <R extends Sort> ReExpr<R> mkIntersect(Expr<ReSort<R>>... t)
    {
        checkContextMatch(t);
        return (ReExpr<R>) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
    }
 
    public final <R extends Sort> ReExpr<R> mkDiff(Expr<ReSort<R>> a, Expr<ReSort<R>> b)
    {
        checkContextMatch(a, b);
    return (ReExpr<R>) Expr.create(this, Native.mkReDiff(nCtx(), a.getNativeObject(), b.getNativeObject()));
    }
 
 
    public final <R extends Sort> ReExpr<R> mkEmptyRe(ReSort<R> s)
    {
        return (ReExpr<R>) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
    }
 
    public final <R extends Sort> ReExpr<R> mkFullRe(ReSort<R> s)
    {
        return (ReExpr<R>) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
    }
 
    public final <R extends Sort> ReExpr<R> mkAllcharRe(ReSort<R> s)
    {
        return (ReExpr<R>) Expr.create(this, Native.mkReAllchar(nCtx(), s.getNativeObject()));
    }
 
    public final ReExpr<SeqSort<CharSort>> mkRange(Expr<SeqSort<CharSort>> lo, Expr<SeqSort<CharSort>> hi)
    {
        checkContextMatch(lo, hi);
        return (ReExpr<SeqSort<CharSort>>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
    }
 
    public BoolExpr mkCharLe(Expr<CharSort> ch1, Expr<CharSort> ch2) 
    {
        checkContextMatch(ch1, ch2);
        return (BoolExpr) Expr.create(this, Native.mkCharLe(nCtx(), ch1.getNativeObject(), ch2.getNativeObject()));
    }
 
    public IntExpr charToInt(Expr<CharSort> ch) 
    {
        checkContextMatch(ch);
        return (IntExpr) Expr.create(this, Native.mkCharToInt(nCtx(), ch.getNativeObject()));
    }
 
    public BitVecExpr charToBv(Expr<CharSort> ch) 
    {
        checkContextMatch(ch);
        return (BitVecExpr) Expr.create(this, Native.mkCharToBv(nCtx(), ch.getNativeObject()));
    }
 
    public Expr<CharSort> charFromBv(BitVecExpr bv) 
    {
        checkContextMatch(bv);
        return (Expr<CharSort>) Expr.create(this, Native.mkCharFromBv(nCtx(), bv.getNativeObject()));
    }
 
    public BoolExpr mkIsDigit(Expr<CharSort> ch) 
    {
        checkContextMatch(ch);
        return (BoolExpr) Expr.create(this, Native.mkCharIsDigit(nCtx(), ch.getNativeObject()));
    }
 
    public BoolExpr mkAtMost(Expr<BoolSort>[] args, int k)
    {
        checkContextMatch(args);
        return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
    }
 
    public BoolExpr mkAtLeast(Expr<BoolSort>[] args, int k)
    {
        checkContextMatch(args);
        return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
    }
 
    public BoolExpr mkPBLe(int[] coeffs, Expr<BoolSort>[] args, int k)
    {
        checkContextMatch(args);
        return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
    }
 
    public BoolExpr mkPBGe(int[] coeffs, Expr<BoolSort>[] args, int k)
    {
        checkContextMatch(args);
        return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
    }
 
    public BoolExpr mkPBEq(int[] coeffs, Expr<BoolSort>[] args, int k)
    {
        checkContextMatch(args);
        return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
    }
 
    public final <R extends Sort> Expr<R> mkNumeral(String v, R ty)
    {
        checkContextMatch(ty);
        return (Expr<R>) Expr.create(this,
                Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
    }
 
    public final <R extends Sort> Expr<R> mkNumeral(int v, R ty)
    {
        checkContextMatch(ty);
        return (Expr<R>) Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
    }
 
    public final <R extends Sort> Expr<R> mkNumeral(long v, R ty)
    {
        checkContextMatch(ty);
        return (Expr<R>) 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<BoolSort> body,
                               int weight, Pattern[] patterns, Expr<?>[] noPatterns,
                               Symbol quantifierID, Symbol skolemID)
    {
        return Quantifier.of(this, true, sorts, names, body, weight, patterns,
                noPatterns, quantifierID, skolemID);
    }
 
    public Quantifier mkForall(Expr<?>[] boundConstants, Expr<BoolSort> body, int weight,
                               Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID,
                               Symbol skolemID)
    {
 
        return Quantifier.of(this, true, boundConstants, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }
 
    public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr<BoolSort> body,
                               int weight, Pattern[] patterns, Expr<?>[] noPatterns,
                               Symbol quantifierID, Symbol skolemID)
    {
 
        return Quantifier.of(this, false, sorts, names, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }
 
    public Quantifier mkExists(Expr<?>[] boundConstants, Expr<BoolSort> body, int weight,
                               Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID,
                               Symbol skolemID)
    {
 
        return Quantifier.of(this, false, boundConstants, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }
 
    public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
                                   Symbol[] names, Expr<BoolSort> 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<BoolSort> 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 final <R extends Sort> Lambda<R> mkLambda(Sort[] sorts, Symbol[] names, Expr<R> body)
     {
         return Lambda.of(this, sorts, names, body);
     }
 
     public final <R extends Sort> Lambda<R> mkLambda(Expr<?>[] boundConstants, Expr<R> body)
     {
         return Lambda.of(this, boundConstants, body);
     }
 
 
    public void setPrintMode(Z3_ast_print_mode value)
    {
        Native.setAstPrintMode(nCtx(), value.toInt());
    }
 
    public String benchmarkToSMTString(String name, String logic,
            String status, String attributes, Expr<BoolSort>[] assumptions,
                                       Expr<BoolSort> formula)
    {
 
        return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
                attributes, assumptions.length,
                AST.arrayToNative(assumptions), formula.getNativeObject());
    }
 
    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");
        }
        ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
                str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
                AST.arrayToNative(sorts), AST.arrayLength(decls),
                Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
        return v.ToBoolExprArray();
    }
 
    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");
        ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
                fileName, AST.arrayLength(sorts),
                Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
                AST.arrayLength(decls), Symbol.arrayToNative(declNames),
                AST.arrayToNative(decls)));
        return v.ToBoolExprArray();
    }
 
    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 getNumSimplifiers()
    {
        return Native.getNumSimplifiers(nCtx());
    }
 
    public String[] getSimplifierNames()
    {
 
        int n = getNumSimplifiers();
        String[] res = new String[n];
        for (int i = 0; i < n; i++)
            res[i] = Native.getSimplifierName(nCtx(), i);
        return res;
    }
 
    public String getSimplifierDescription(String name)
    {
        return Native.simplifierGetDescr(nCtx(), name);
    }
 
    public Simplifier mkSimplifier(String name)
    {
        return new Simplifier(this, name);
    }
 
    public Simplifier andThen(Simplifier t1, Simplifier t2, Simplifier... 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.simplifierAndThen(nCtx(), ts[i].getNativeObject(),
                    last);
            }
        }
        if (last != 0)
        {
            last = Native.simplifierAndThen(nCtx(), t2.getNativeObject(), last);
            return new Simplifier(this, Native.simplifierAndThen(nCtx(),
                    t1.getNativeObject(), last));
        } else
            return new Simplifier(this, Native.simplifierAndThen(nCtx(),
                    t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public Simplifier then(Simplifier t1, Simplifier t2, Simplifier... ts)
    {
        return andThen(t1, t2, ts);
    }
 
    public Simplifier usingParams(Simplifier t, Params p)
    {
        checkContextMatch(t);
        checkContextMatch(p);
        return new Simplifier(this, Native.simplifierUsingParams(nCtx(),
                t.getNativeObject(), p.getNativeObject()));
    }
 
    public Simplifier with(Simplifier t, Params p)
    {
        return usingParams(t, p);
    }
 
    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 Solver mkSolver(Solver s, Simplifier simp)
    {
        return new Solver(this, Native.solverAddSimplifier(nCtx(), s.getNativeObject(), simp.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, exp, sig, s);
    }
 
    public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
    {
        return mkFPNumeral(sgn, exp, sig, s);
    }
 
 
    public FPExpr mkFPAbs(Expr<FPSort> t)
    {
        return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
    }
 
    public FPExpr mkFPNeg(Expr<FPSort> t)
    {
        return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
    }
 
    public FPExpr mkFPAdd(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public FPExpr mkFPSub(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public FPExpr mkFPMul(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public FPExpr mkFPDiv(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public FPExpr mkFPFMA(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2, Expr<FPSort> t3)
    {
        return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
    }
 
    public FPExpr mkFPSqrt(Expr<FPRMSort> rm, Expr<FPSort> t)
    {
        return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
    }
 
    public FPExpr mkFPRem(Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public FPExpr mkFPRoundToIntegral(Expr<FPRMSort> rm, Expr<FPSort> t)
    {
        return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
    }
 
    public FPExpr mkFPMin(Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public FPExpr mkFPMax(Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkFPLEq(Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkFPLt(Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkFPGEq(Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkFPGt(Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkFPEq(Expr<FPSort> t1, Expr<FPSort> t2)
    {
        return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }
 
    public BoolExpr mkFPIsNormal(Expr<FPSort> t)
    {
        return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
    }
 
    public BoolExpr mkFPIsSubnormal(Expr<FPSort> t)
    {
        return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
    }
 
    public BoolExpr mkFPIsZero(Expr<FPSort> t)
    {
        return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
    }
 
    public BoolExpr mkFPIsInfinite(Expr<FPSort> t)
    {
        return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
    }
 
    public BoolExpr mkFPIsNaN(Expr<FPSort> t)
    {
        return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
    }
 
    public BoolExpr mkFPIsNegative(Expr<FPSort> t)
    {
        return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
    }
 
    public BoolExpr mkFPIsPositive(Expr<FPSort> t)
    {
        return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
    }
 
    public FPExpr mkFP(Expr<BitVecSort> sgn, Expr<BitVecSort> sig, Expr<BitVecSort> exp)
    {
        return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
    }
 
    public FPExpr mkFPToFP(Expr<BitVecSort> bv, FPSort s)
    {
        return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
    }
 
    public FPExpr mkFPToFP(Expr<FPRMSort> rm, FPExpr t, FPSort s)
    {
        return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
    }
 
    public FPExpr mkFPToFP(Expr<FPRMSort> rm, RealExpr t, FPSort s)
    {
        return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
    }
 
    public FPExpr mkFPToFP(Expr<FPRMSort> rm, Expr<BitVecSort> 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, Expr<FPRMSort> rm, Expr<FPSort> t)
    {
        return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
    }
 
    public BitVecExpr mkFPToBV(Expr<FPRMSort> rm, Expr<FPSort> 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(Expr<FPSort> t)
    {
        return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
    }
 
    public BitVecExpr mkFPToIEEEBV(Expr<FPSort> t)
    {
        return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
    }
 
    public BitVecExpr mkFPToFP(Expr<FPRMSort> rm, Expr<IntSort> exp, Expr<RealSort> sig, FPSort s)
    {
        return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
    }
 
    public final <R extends Sort> FuncDecl<BoolSort> mkLinearOrder(R sort, int index) {
        return (FuncDecl<BoolSort>) FuncDecl.create(
                this,
                Native.mkLinearOrder(
                        nCtx(),
                        sort.getNativeObject(),
                        index
                )
        );
    }
 
    public final <R extends Sort> FuncDecl<BoolSort> mkPartialOrder(R sort, int index) {
        return (FuncDecl<BoolSort>) FuncDecl.create(
                this,
                Native.mkPartialOrder(
                    nCtx(),
                    sort.getNativeObject(),
                    index
                )
        );
    }
 
    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);
    }
 
 
    public long nCtx()
    {
        if (m_ctx == 0)
            throw new Z3Exception("Context closed");
        return m_ctx;
    }
 
 
    void checkContextMatch(Z3Object other)
    {
        if (this != other.getContext())
            throw new Z3Exception("Context mismatch");
    }
 
    void checkContextMatch(Z3Object other1, Z3Object other2)
    {
        checkContextMatch(other1);
        checkContextMatch(other2);
    }
 
    void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
    {
        checkContextMatch(other1);
        checkContextMatch(other2);
        checkContextMatch(other3);
    }
 
    void checkContextMatch(Z3Object[] arr)
    {
        if (arr != null)
            for (Z3Object a : arr)
                checkContextMatch(a);
    }
 
    private Z3ReferenceQueue m_RefQueue = new Z3ReferenceQueue(this);
 
    Z3ReferenceQueue getReferenceQueue() { return m_RefQueue; }
 
    @Override
    public void close()
    {
        if (m_ctx == 0)
            return;
 
        m_RefQueue.forceClear();
 
        m_boolSort = null;
        m_intSort = null;
        m_realSort = null;
        m_stringSort = null;
        m_RefQueue = null;
 
        synchronized (creation_lock) {
            Native.delContext(m_ctx);
        }
        m_ctx = 0;
    }
}