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.Contracts;

namespace Microsoft.Z3
{
    [ContractVerification(true)]
    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)
        {
            Contract.Requires(constraints != null);
            Contract.Requires(Contract.ForAll(constraints, c => c != null));

            Context.CheckContextMatch<BoolExpr>(constraints);
            foreach (BoolExpr c in constraints)
            {
                Contract.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
            {
                Contract.Ensures(Contract.Result<BoolExpr[]>() != null);

                uint n = Size;
                BoolExpr[] res = new BoolExpr[n];
                for (uint i = 0; i < n; i++)
                    res[i] = new BoolExpr(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 Goal Translate(Context ctx)
        {
            Contract.Requires(ctx != null);

            return new Goal(ctx, Native.Z3_goal_translate(Context.nCtx, NativeObject, ctx.nCtx));
        }

        public Goal Simplify(Params p = null)
        {
            Tactic t = Context.MkTactic("simplify");
            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 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) { Contract.Requires(ctx != null); }

        internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
            : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
        {
            Contract.Requires(ctx != null);
        }

        internal class DecRefQueue : IDecRefQueue
        {
            public DecRefQueue() : base() { }
            public DecRefQueue(uint move_limit) : base(move_limit) { }
            internal override void IncRef(Context ctx, IntPtr obj)
            {
                Native.Z3_goal_inc_ref(ctx.nCtx, obj);
            }

            internal override void DecRef(Context ctx, IntPtr obj)
            {
                Native.Z3_goal_dec_ref(ctx.nCtx, obj);
            }
        };        

        internal override void IncRef(IntPtr o)
        {
            Context.Goal_DRQ.IncAndClear(Context, o);
            base.IncRef(o);
        }

        internal override void DecRef(IntPtr o)
        {
            Context.Goal_DRQ.Add(o);
            base.DecRef(o);
        }

        #endregion
    }
}