Solver.cs

Go to the documentation of this file.

/*++
Copyright (c) 2012 Microsoft Corporation
 
Module Name:
 
    Solver.cs
 
Abstract:
 
    Z3 Managed API: Solvers
 
Author:
 
    Christoph Wintersteiger (cwinter) 2012-03-22
 
Notes:
    
--*/
 
using System;
using System.Diagnostics;
using System.Linq;
using System.Collections.Generic;
 
namespace Microsoft.Z3
{
    public class Solver : Z3Object
    {
        public string Help
        {
            get
            {
 
                return Native.Z3_solver_get_help(Context.nCtx, NativeObject);
            }
        }
 
        public Params Parameters
        {
            set
            {
                Debug.Assert(value != null);
 
                Context.CheckContextMatch(value);
                Native.Z3_solver_set_params(Context.nCtx, NativeObject, value.NativeObject);
            }
        }
 
        public void Set(string name, bool value) 
    { 
        using var parameters = Context.MkParams().Add(name, value);
        Parameters = parameters; 
    }
 
        public void Set(string name, uint value)
    { 
        using var parameters = Context.MkParams().Add(name, value);
        Parameters = parameters; 
    }
 
        public void Set(string name, double value)
    { 
        using var parameters = Context.MkParams().Add(name, value);
        Parameters = parameters; 
    }
 
        public void Set(string name, string value)
    {
        using var parameters = Context.MkParams().Add(name, value);
        Parameters = parameters; 
    }
 
        public void Set(string name, Symbol value)
    {
        using var parameters = Context.MkParams().Add(name, value);
        Parameters = parameters; 
    }
 
        public void Set(Symbol name, bool value)
    { 
        using var parameters = Context.MkParams().Add(name, value);
        Parameters = parameters; 
    }
 
        public void Set(Symbol name, uint value)
    { 
        using var parameters = Context.MkParams().Add(name, value);
        Parameters = parameters; 
    }
 
        public void Set(Symbol name, double value)
    { 
        using var parameters = Context.MkParams().Add(name, value);
        Parameters = parameters; 
    }
 
        public void Set(Symbol name, string value)
    { 
        using var parameters = Context.MkParams().Add(name, value);
        Parameters = parameters; 
    }
 
        public void Set(Symbol name, Symbol value) 
    { 
        using var parameters = Context.MkParams().Add(name, value);
        Parameters = parameters; 
    }
 
 
 
        public ParamDescrs ParameterDescriptions
        {
            get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); }
        }
 
 
        public uint NumScopes
        {
            get { return Native.Z3_solver_get_num_scopes(Context.nCtx, NativeObject); }
        }
 
        public void Push()
        {
            Native.Z3_solver_push(Context.nCtx, NativeObject);
        }
 
        public void Pop(uint n = 1)
        {
            Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
        }
 
        public void Reset()
        {
            Native.Z3_solver_reset(Context.nCtx, NativeObject);
        }
 
        public void Assert(params BoolExpr[] constraints)
        {
            Debug.Assert(constraints != null);
            Debug.Assert(constraints.All(c => c != null));
 
            Context.CheckContextMatch<BoolExpr>(constraints);
            foreach (BoolExpr a in constraints)
            {
                Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
            }
        }
 
        public void Add(params BoolExpr[] constraints)
        {
            Assert(constraints);
        }
 
        public void Add(IEnumerable<BoolExpr> constraints)
        {
            Assert(constraints.ToArray());
        }
 
        public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
        {
            Debug.Assert(constraints != null);
            Debug.Assert(constraints.All(c => c != null));
            Debug.Assert(ps.All(c => c != null));
            Context.CheckContextMatch<BoolExpr>(constraints);
            Context.CheckContextMatch<BoolExpr>(ps);
            if (constraints.Length != ps.Length)
                throw new Z3Exception("Argument size mismatch");
            
            for (int i = 0 ; i < constraints.Length; i++)
                Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
        }
 
        public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
        {
            Debug.Assert(constraint != null);
            Debug.Assert(p != null);
            Context.CheckContextMatch(constraint);
            Context.CheckContextMatch(p);
                        
            Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
        }
 
        public void FromFile(string file) 
        {
             Native.Z3_solver_from_file(Context.nCtx, NativeObject, file);      
        }
 
        public void FromString(string str) 
        {
             Native.Z3_solver_from_string(Context.nCtx, NativeObject, str);     
        }
 
        public uint NumAssertions
        {
            get
            {
                using ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
                return assertions.Size;
            }
        }
 
        public BoolExpr[] Assertions
        {
            get
            {
 
                using ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
                return assertions.ToBoolExprArray();
            }
        }
 
        public BoolExpr[] Units
        {
            get
            {
 
                using ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_units(Context.nCtx, NativeObject));
                return assertions.ToBoolExprArray();
            }
        }
 
        public BoolExpr[] NonUnits
        {
            get
            {
                using ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_non_units(Context.nCtx, NativeObject));
                return assertions.ToBoolExprArray();
            }
        }
 
        public BoolExpr[] Trail
        {
            get
            {
                using ASTVector trail = new ASTVector(Context, Native.Z3_solver_get_trail(Context.nCtx, NativeObject));
                return trail.ToBoolExprArray();
            }
        }
 
        public Expr CongruenceRoot(Expr t)
        {
            Debug.Assert(t != null);
            Context.CheckContextMatch(t);
            return Expr.Create(Context, Native.Z3_solver_congruence_root(Context.nCtx, NativeObject, t.NativeObject));
        }
 
        public Expr CongruenceNext(Expr t)
        {
            Debug.Assert(t != null);
            Context.CheckContextMatch(t);
            return Expr.Create(Context, Native.Z3_solver_congruence_next(Context.nCtx, NativeObject, t.NativeObject));
        }
 
        public Expr CongruenceExplain(Expr a, Expr b)
        {
            Debug.Assert(a != null);
            Debug.Assert(b != null);
            Context.CheckContextMatch(a);
            Context.CheckContextMatch(b);
            return Expr.Create(Context, Native.Z3_solver_congruence_explain(Context.nCtx, NativeObject, a.NativeObject, b.NativeObject));
        }
 
        public Status Check(params Expr[] assumptions)
        {
            Z3_lbool r;
            if (assumptions == null || assumptions.Length == 0)
                r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
            else
                r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
            return lboolToStatus(r);
        }
 
        public Status Check(IEnumerable<BoolExpr> assumptions)
        {
            Z3_lbool r;
            BoolExpr[] asms = assumptions.ToArray();
            if (asms.Length == 0)
                r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
            else
                r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)asms.Length, AST.ArrayToNative(asms));
            return lboolToStatus(r);
        }
 
        public Status Consequences(IEnumerable<BoolExpr> assumptions, IEnumerable<Expr> variables, out BoolExpr[] consequences) 
        {
            using ASTVector result = new ASTVector(Context);
            using ASTVector asms = new ASTVector(Context);
            using ASTVector vars = new ASTVector(Context);
            foreach (var asm in assumptions) asms.Push(asm);
            foreach (var v in variables) vars.Push(v);
            Z3_lbool r = (Z3_lbool)Native.Z3_solver_get_consequences(Context.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, result.NativeObject);
            consequences = result.ToBoolExprArray();
            return lboolToStatus(r);
        }
 
        public Model Model
        {
            get
            {
                IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject);
                if (x == IntPtr.Zero)
                    return null;
                else
                    return new Model(Context, x);
            }
        }
 
        public Expr Proof
        {
            get
            {
                IntPtr x = Native.Z3_solver_get_proof(Context.nCtx, NativeObject);
                if (x == IntPtr.Zero)
                    return null;
                else
                    return Expr.Create(Context, x);
            }
        }
 
        public BoolExpr[] UnsatCore
        {
            get
            {
 
                using ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));                
                return core.ToBoolExprArray();
            }
        }
 
        public string ReasonUnknown
        {
            get
            {
 
                return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
            }
        }
 
        public uint BacktrackLevel { get; set; }
 
        public BoolExpr[] CubeVariables { get; set; }
        
 
        public IEnumerable<BoolExpr[]> Cube()
        {
             using ASTVector cv = new ASTVector(Context);
             if (CubeVariables != null) 
                foreach (var b in CubeVariables) cv.Push(b);
 
             while (true) {
                var lvl = BacktrackLevel;
                BacktrackLevel = uint.MaxValue;
                using ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, cv.NativeObject, lvl));
                var v = r.ToBoolExprArray();
                CubeVariables = cv.ToBoolExprArray();
                if (v.Length == 1 && v[0].IsFalse) {
                   break;
                }
                yield return v; 
                if (v.Length == 0) {
                   break;
                }
             }
        }
 
        public Solver Translate(Context ctx) 
        {
             Debug.Assert(ctx != null);
             return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
        }
 
        public void ImportModelConverter(Solver src) 
        {
             Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject);
        }
 
        public Statistics Statistics
        {
            get
            {
 
                return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject));
            }
        }
 
        public override string ToString()
        {
            return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
        }
 
        #region Internal
        internal Solver(Context ctx, IntPtr obj)
            : base(ctx, obj)
        {
            Debug.Assert(ctx != null);
            this.BacktrackLevel = uint.MaxValue;
        }
 
        internal override void IncRef(IntPtr o)
        {
            Native.Z3_solver_inc_ref(Context.nCtx, o);
        }
 
        internal override void DecRef(IntPtr o)
        {
            lock (Context)
            {
                if (Context.nCtx != IntPtr.Zero)
                    Native.Z3_solver_dec_ref(Context.nCtx, o);
            }
        }
 
        private Status lboolToStatus(Z3_lbool r) 
        {
            switch (r)
            {
                case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
                case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
                default: return Status.UNKNOWN;
            }
        }
 
        #endregion
    }
}