Solver.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import com.microsoft.z3.enumerations.Z3_lbool;
 
import java.lang.ref.ReferenceQueue;
import java.util.*;
 
@SuppressWarnings("unchecked")
public class Solver extends Z3Object {
    public String getHelp()
    {
        return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
    }
 
    public void setParameters(Params value)
    {
        getContext().checkContextMatch(value);
        Native.solverSetParams(getContext().nCtx(), getNativeObject(),
                value.getNativeObject());
    }
 
    public ParamDescrs getParameterDescriptions()
    {
        return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
                getContext().nCtx(), getNativeObject()));
    }
 
    public int getNumScopes()
    {
        return Native
                .solverGetNumScopes(getContext().nCtx(), getNativeObject());
    }
 
    public void push()
    {
        Native.solverPush(getContext().nCtx(), getNativeObject());
    }
 
    public void pop()
    {
        pop(1);
    }
 
    public void pop(int n)
    {
        Native.solverPop(getContext().nCtx(), getNativeObject(), n);
    }
 
    public void reset()
    {
        Native.solverReset(getContext().nCtx(), getNativeObject());
    }
 
    public void interrupt()
    {
        Native.solverInterrupt(getContext().nCtx(), getNativeObject());
    }
 
    public void add(Expr<BoolSort>... constraints)
    {
        getContext().checkContextMatch(constraints);
        for (Expr<BoolSort> a : constraints)
        {
            Native.solverAssert(getContext().nCtx(), getNativeObject(),
                    a.getNativeObject());
        }
    }
 
 
    public void assertAndTrack(Expr<BoolSort>[] constraints, Expr<BoolSort>[] ps)
    {
        getContext().checkContextMatch(constraints);
        getContext().checkContextMatch(ps);
        if (constraints.length != ps.length) {
            throw new Z3Exception("Argument size mismatch");
        }
 
        for (int i = 0; i < constraints.length; i++) {
            Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
                constraints[i].getNativeObject(), ps[i].getNativeObject());
        }
    }
 
    public void assertAndTrack(Expr<BoolSort> constraint, Expr<BoolSort> p)
    {
        getContext().checkContextMatch(constraint);
        getContext().checkContextMatch(p);
 
        Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
                constraint.getNativeObject(), p.getNativeObject());
    }
 
    public void fromFile(String file) 
    {
        Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);    
    }
 
    public void fromString(String str) 
    {
        Native.solverFromString(getContext().nCtx(), getNativeObject(), str);   
    }
 
 
    public int getNumAssertions()
    {
        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
        return assrts.size();
    }
 
    public BoolExpr[] getAssertions()
    {
        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
        return assrts.ToBoolExprArray();
    }
 
    @SafeVarargs
    public final Status check(Expr<BoolSort>... assumptions)
    {
        Z3_lbool r;
        if (assumptions == null) {
            r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
                getNativeObject()));
        } else {
            r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
                .nCtx(), getNativeObject(), assumptions.length, AST
                .arrayToNative(assumptions)));
        }
        return lboolToStatus(r);
    }
 
    @SuppressWarnings("rawtypes")
    public Status check()
    {
        return check((Expr[]) null);
    }
 
    public Status getConsequences(Expr<BoolSort>[] assumptions, Expr<?>[] variables, List<Expr<BoolSort>> consequences)
    {
        ASTVector result = new ASTVector(getContext());
        ASTVector asms = new ASTVector(getContext());
        ASTVector vars = new ASTVector(getContext());
        for (Expr<BoolSort> asm : assumptions) asms.push(asm);
        for (Expr<?> v : variables) vars.push(v);
        int r = Native.solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject());
        for (int i = 0; i < result.size(); ++i) consequences.add((BoolExpr) Expr.create(getContext(), result.get(i).getNativeObject()));
        return lboolToStatus(Z3_lbool.fromInt(r));
    }
 
 
    public Model getModel()
    {
        long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
        if (x == 0) {
            return null;
        } else {
            return new Model(getContext(), x);
        }
    }
 
    public Expr<?> getProof()
    {
        long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
        if (x == 0) {
            return null;
        } else {
            return Expr.create(getContext(), x);
        }
    }
 
    public BoolExpr[] getUnsatCore()
    {
 
        ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));        
        return core.ToBoolExprArray();
    }
 
    public BoolExpr[] getUnits()
    {
        ASTVector units = new ASTVector(getContext(), Native.solverGetUnits(getContext().nCtx(), getNativeObject()));
        return units.ToBoolExprArray();
    }
 
    public BoolExpr[] getNonUnits()
    {
        ASTVector nonUnits = new ASTVector(getContext(), Native.solverGetNonUnits(getContext().nCtx(), getNativeObject()));
        return nonUnits.ToBoolExprArray();
    }
 
    public BoolExpr[] getTrail()
    {
        ASTVector trail = new ASTVector(getContext(), Native.solverGetTrail(getContext().nCtx(), getNativeObject()));
        return trail.ToBoolExprArray();
    }
 
    public String getReasonUnknown()
    {
        return Native.solverGetReasonUnknown(getContext().nCtx(),
                getNativeObject());
    }
 
    public int[] getTrailLevels()
    {
        ASTVector trailVector = new ASTVector(getContext(), Native.solverGetTrail(getContext().nCtx(), getNativeObject()));
        int[] levels = new int[trailVector.size()];
        Native.solverGetLevels(getContext().nCtx(), getNativeObject(), trailVector.getNativeObject(), trailVector.size(), levels);
        return levels;
    }
 
    public java.util.Iterator<BoolExpr[]> cube(Expr<?>[] vars, int cutoff)
    {
        ASTVector cubeVars = new ASTVector(getContext());
        if (vars != null) {
            for (Expr<?> v : vars) {
                cubeVars.push(v);
            }
        }
        
        return new java.util.Iterator<BoolExpr[]>() {
            private BoolExpr[] nextCube = computeNext();
            
            private BoolExpr[] computeNext() {
                ASTVector result = new ASTVector(getContext(), 
                    Native.solverCube(getContext().nCtx(), getNativeObject(), 
                                     cubeVars.getNativeObject(), cutoff));
                BoolExpr[] cube = result.ToBoolExprArray();
                
                // Check for termination conditions
                if (cube.length == 1 && cube[0].isFalse()) {
                    return null; // No more cubes
                }
                if (cube.length == 0) {
                    return null; // Search space exhausted
                }
                return cube;
            }
            
            @Override
            public boolean hasNext() {
                return nextCube != null;
            }
            
            @Override
            public BoolExpr[] next() {
                if (nextCube == null) {
                    throw new java.util.NoSuchElementException();
                }
                BoolExpr[] current = nextCube;
                nextCube = computeNext();
                return current;
            }
        };
    }
 
    public Expr<?> congruenceRoot(Expr<?> t)
    {
        getContext().checkContextMatch(t);
        return Expr.create(getContext(),
            Native.solverCongruenceRoot(getContext().nCtx(), getNativeObject(), t.getNativeObject()));
    }
 
    public Expr<?> congruenceNext(Expr<?> t)
    {
        getContext().checkContextMatch(t);
        return Expr.create(getContext(),
            Native.solverCongruenceNext(getContext().nCtx(), getNativeObject(), t.getNativeObject()));
    }
 
    public Expr<?> congruenceExplain(Expr<?> a, Expr<?> b)
    {
        getContext().checkContextMatch(a);
        getContext().checkContextMatch(b);
        return Expr.create(getContext(),
            Native.solverCongruenceExplain(getContext().nCtx(), getNativeObject(),
                a.getNativeObject(), b.getNativeObject()));
    }
 
    public void solveFor(Expr<?>[] variables, Expr<?>[] terms, BoolExpr[] guards)
    {
        ASTVector vars = new ASTVector(getContext());
        ASTVector termVec = new ASTVector(getContext());
        ASTVector guardVec = new ASTVector(getContext());
        for (Expr<?> v : variables) vars.push(v);
        for (Expr<?> t : terms) termVec.push(t);
        for (BoolExpr g : guards) guardVec.push(g);
        Native.solverSolveFor(getContext().nCtx(), getNativeObject(),
            vars.getNativeObject(), termVec.getNativeObject(), guardVec.getNativeObject());
    }
 
    public void setInitialValue(Expr<?> var, Expr<?> value)
    {
        getContext().checkContextMatch(var);
        getContext().checkContextMatch(value);
        Native.solverSetInitialValue(getContext().nCtx(), getNativeObject(), 
                                     var.getNativeObject(), value.getNativeObject());
    }
 
    public void importModelConverter(Solver src)
    {
        Native.solverImportModelConverter(getContext().nCtx(), src.getNativeObject(), getNativeObject());
    }
 
    public Solver translate(Context ctx) 
    {
        return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
    }
 
    public Solver addSimplifier(Simplifier simplifier)
    {
        return new Solver(getContext(), Native.solverAddSimplifier(
                getContext().nCtx(), getNativeObject(), simplifier.getNativeObject()));
    }
 
    public String toDimacs(boolean includeNames)
    {
        return Native.solverToDimacsString(getContext().nCtx(), getNativeObject(), includeNames);
    }
 
    public Statistics getStatistics()
    {
        return new Statistics(getContext(), Native.solverGetStatistics(
                getContext().nCtx(), getNativeObject()));
    }
 
    @Override
    public String toString()
    {
        return Native
                .solverToString(getContext().nCtx(), getNativeObject());
    }
 
    private Status lboolToStatus(Z3_lbool r) 
    {
        switch (r)
        {
        case Z3_L_TRUE:
            return Status.SATISFIABLE;
        case Z3_L_FALSE:
            return Status.UNSATISFIABLE;
        default:
            return Status.UNKNOWN;
        }
    }
 
    Solver(Context ctx, long obj)
    {
        super(ctx, obj);
    }
 
    @Override
    void incRef() {
        Native.solverIncRef(getContext().nCtx(), getNativeObject());
    }
 
    @Override
    void addToReferenceQueue() {
        getContext().getReferenceQueue().storeReference(this, SolverRef::new);
    }
 
    private static class SolverRef extends Z3ReferenceQueue.Reference<Solver> {
 
        private SolverRef(Solver referent, ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }
 
        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.solverDecRef(ctx.nCtx(), z3Obj);
        }
    }
}