Goal.cs

Go to the documentation of this file.

/*++
Copyright (c) 2012 Microsoft Corporation
 
Module Name:
 
    Goal.cs
 
Abstract:
 
    Z3 Managed API: Goal
 
Author:
 
    Christoph Wintersteiger (cwinter) 2012-03-21
 
Notes:
    
--*/
 
using System;
using System.Diagnostics;
using System.Linq;
 
namespace Microsoft.Z3
{
    public class Goal : Z3Object
    {
        public Z3_goal_prec Precision
        {
            get { return (Z3_goal_prec)Native.Z3_goal_precision(Context.nCtx, NativeObject); }
        }
 
        public bool IsPrecise
        {
            get { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; }
        }
        public bool IsUnderApproximation
        {
            get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
        }
 
        public bool IsOverApproximation
        {
            get { return Precision == Z3_goal_prec.Z3_GOAL_OVER; }
        }
 
        public bool IsGarbage
        {
            get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
        }
 
        public void Assert(params BoolExpr[] constraints)
        {
            Debug.Assert(constraints != null);
            Debug.Assert(constraints.All(c => c != null));
 
            Context.CheckContextMatch<BoolExpr>(constraints);
            foreach (BoolExpr c in constraints)
            {
                Debug.Assert(c != null); // It was an assume, now made an assert just to be sure we do not regress
                Native.Z3_goal_assert(Context.nCtx, NativeObject, c.NativeObject);
            }
        }
 
        public void Add(params BoolExpr[] constraints)
        {
            Assert(constraints);
        }
 
        public bool Inconsistent
        {
            get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; }
        }
 
        public uint Depth
        {
            get { return Native.Z3_goal_depth(Context.nCtx, NativeObject); }
        }
 
        public void Reset()
        {
            Native.Z3_goal_reset(Context.nCtx, NativeObject);
        }
 
        public uint Size
        {
            get { return Native.Z3_goal_size(Context.nCtx, NativeObject); }
        }
 
        public BoolExpr[] Formulas
        {
            get
            {
 
                uint n = Size;
                BoolExpr[] res = new BoolExpr[n];
                for (uint i = 0; i < n; i++)
                    res[i] = (BoolExpr)Expr.Create(Context, Native.Z3_goal_formula(Context.nCtx, NativeObject, i));
                return res;
            }
        }
 
        public uint NumExprs
        {
            get { return Native.Z3_goal_num_exprs(Context.nCtx, NativeObject); }
        }
 
        public bool IsDecidedSat
        {
            get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; }
        }
 
        public bool IsDecidedUnsat
        {
            get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
        }
 
        public Model ConvertModel(Model m)
        {
            if (m != null)
               return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, m.NativeObject));
            else
               return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, IntPtr.Zero));
        }
 
 
        public Goal Translate(Context ctx)
        {
            Debug.Assert(ctx != null);
 
            return new Goal(ctx, Native.Z3_goal_translate(Context.nCtx, NativeObject, ctx.nCtx));
        }
 
        public Goal Simplify(Params p = null)
        {
            using Tactic t = Context.MkTactic("simplify");
            using ApplyResult res = t.Apply(this, p);
 
            if (res.NumSubgoals == 0)
                throw new Z3Exception("No subgoals");
            else
                return res.Subgoals[0];
        }
 
        public override string ToString()
        {
            return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
        }
 
        public string ToDimacs(bool include_names = true)
        {
            return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject, (byte)(include_names ? 1 : 0));
        }
 
        public BoolExpr AsBoolExpr() {
            uint n = Size;
            if (n == 0) 
                return Context.MkTrue();
            else if (n == 1)                
                return Formulas[0];
            else {
                return Context.MkAnd(Formulas);
            }
        }
 
        #region Internal
        internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
 
        internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
            : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (byte)(models ? 1 : 0), (byte)(unsatCores ? 1 : 0), (byte)(proofs ? 1 : 0)))
        {
            Debug.Assert(ctx != null);
        }      
 
        internal override void IncRef(IntPtr o)
        {
            Native.Z3_goal_inc_ref(Context.nCtx, o);
        }
 
        internal override void DecRef(IntPtr o)
        {
            lock (Context)
            {
                if (Context.nCtx != IntPtr.Zero)
                    Native.Z3_goal_dec_ref(Context.nCtx, o);
            }
        }
 
        #endregion
    }
}