add simplifiers to .net API

src/api/dotnet/CMakeLists.txt

@@ -103,6 +103,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
     SeqExpr.cs
     SeqSort.cs
     SetSort.cs
+    Simplifiers.cs
     Solver.cs
     Sort.cs
     Statistics.cs

src/api/dotnet/Context.cs

@@ -3726,6 +3726,110 @@ public void Interrupt()
         }
         #endregion
 
+        #region Simplifiers
+        /// <summary>
+        /// The number of supported simplifiers.
+        /// </summary>
+        public uint NumSimplifiers
+        {
+            get { return Native.Z3_get_num_simplifiers(nCtx); }
+        }
+
+        /// <summary>
+        /// The names of all supported tactics.
+        /// </summary>
+        public string[] SimplifierNames
+        {
+            get
+            {
+
+                uint n = NumSimplifiers;
+                string[] res = new string[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = Native.Z3_get_simplifier_name(nCtx, i);
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// Returns a string containing a description of the simplifier with the given name.
+        /// </summary>
+        public string SimplifierDescription(string name)
+        {
+
+            return Native.Z3_simplifier_get_descr(nCtx, name);
+        }
+
+        /// <summary>
+        /// Creates a new Tactic.
+        /// </summary>
+        public Simplifier MkSimplifier(string name)
+        {
+
+            return new Simplifier(this, name);
+        }
+
+        /// <summary>
+        /// Create a simplifie that applies <paramref name="t1"/> and
+        /// then <paramref name="t2"/>.
+        /// </summary>
+        public Simplifier AndThen(Simplifier t1, Simplifier t2, params Simplifier[] ts)
+        {
+            Debug.Assert(t1 != null);
+            Debug.Assert(t2 != null);
+            // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
+
+
+            CheckContextMatch(t1);
+            CheckContextMatch(t2);
+            CheckContextMatch<Simplifier>(ts);
+
+            IntPtr last = IntPtr.Zero;
+            if (ts != null && ts.Length > 0)
+            {
+                last = ts[ts.Length - 1].NativeObject;
+                for (int i = ts.Length - 2; i >= 0; i--)
+                    last = Native.Z3_simplifier_and_then(nCtx, ts[i].NativeObject, last);
+            }
+            if (last != IntPtr.Zero)
+            {
+                last = Native.Z3_simplifier_and_then(nCtx, t2.NativeObject, last);
+                return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, last));
+            }
+            else
+                return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, t2.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a simplifier that applies <paramref name="t1"/> and then
+        /// then <paramref name="t2"/>.
+        /// </summary>
+        /// <remarks>
+        /// Shorthand for <c>AndThen</c>.
+        /// </remarks>
+        public Simplifier Then(Simplifier t1, Simplifier t2, params Simplifier[] ts)
+        {
+            Debug.Assert(t1 != null);
+            Debug.Assert(t2 != null);
+            //  Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
+
+            return AndThen(t1, t2, ts);
+        }
+
+        /// <summary>
+        /// Create a tactic that applies <paramref name="t"/> using the given set of parameters <paramref name="p"/>.
+        /// </summary>
+        public Simplifier UsingParams(Simplifier t, Params p)
+        {
+            Debug.Assert(t != null);
+            Debug.Assert(p != null);
+
+            CheckContextMatch(t);
+            CheckContextMatch(p);
+            return new Simplifier(this, Native.Z3_simplifier_using_params(nCtx, t.NativeObject, p.NativeObject));
+        }
+        #endregion
+
         #region Probes
         /// <summary>
         /// The number of supported Probes.
@@ -3926,6 +4030,16 @@ public Solver MkSimpleSolver()
             return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
         }
 
+        /// <summary>
+        /// Creates a solver that uses an incremental simplifier.
+        /// </summary>
+        public Solver MkSolver(Solver s, Simplifier t)
+        {
+            Debug.Assert(t != null);
+            Debug.Assert(s != null);
+            return new Solver(this, Native.Z3_solver_add_simplifier(nCtx, s.NativeObject, t.NativeObject));
+        }
+
         /// <summary>
         /// Creates a solver that is implemented using the given tactic.
         /// </summary>
@@ -3939,6 +4053,8 @@ public Solver MkSolver(Tactic t)
 
             return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
         }
+
+
         #endregion
 
         #region Fixedpoints

src/api/dotnet/Simplifiers.cs

@@ -0,0 +1,78 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    Tactic.cs
+
+Abstract:
+
+    Z3 Managed API: Simplifiers
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-21
+
+--*/
+
+using System;
+using System.Diagnostics;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Simplifiers are the basic building block for creating custom solvers with incremental pre-processing.
+    /// The complete list of simplifiers may be obtained using <c>Context.NumSimplifiers</c> 
+    /// and <c>Context.SimplifierNames</c>.
+    /// It may also be obtained using the command <c>(help-simplifier)</c> in the SMT 2.0 front-end.
+    /// </summary>
+    public class Simplifier : Z3Object
+    {
+        /// <summary>
+        /// A string containing a description of parameters accepted by the tactic.
+        /// </summary>
+        public string Help
+        {
+            get
+            {
+
+                return Native.Z3_simplifier_get_help(Context.nCtx, NativeObject);
+            }
+        }
+
+        /// <summary>
+        /// Retrieves parameter descriptions for Simplifiers.
+        /// </summary>
+        public ParamDescrs ParameterDescriptions
+        {
+            get { return new ParamDescrs(Context, Native.Z3_simplifier_get_param_descrs(Context.nCtx, NativeObject)); }
+        }
+
+        #region Internal
+        internal Simplifier(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Debug.Assert(ctx != null);
+        }
+        internal Simplifier(Context ctx, string name)
+            : base(ctx, Native.Z3_mk_simplifier(ctx.nCtx, name))
+        {
+            Debug.Assert(ctx != null);
+        }
+
+        internal override void IncRef(IntPtr o)
+        {
+            Native.Z3_simplifier_inc_ref(Context.nCtx, o);
+        }
+
+        internal override void DecRef(IntPtr o)
+        {
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_simplifier_dec_ref(Context.nCtx, o);
+            }
+        }
+        #endregion
+    }
+}

src/ast/simplifiers/dependent_expr_state.h

@@ -90,7 +90,8 @@ class dependent_expr_state {
     * Freeze internal functions
     */
     void freeze(expr* term);
-    bool frozen(func_decl* f) const { return m_frozen.is_marked(f); }
+    void freeze(expr_ref_vector const& terms) { for (expr* t : terms) freeze(t); }
+    bool frozen(func_decl* f) const { return m_frozen.is_marked(f); }    
     bool frozen(expr* f) const { return is_app(f) && m_frozen.is_marked(to_app(f)->get_decl()); }
     void freeze_suffix();
 

src/solver/simplifier_solver.cpp

@@ -110,10 +110,9 @@ class simplifier_solver : public solver {
         expr_ref_vector orig_assumptions(assumptions);
         m_core_replace.reset();
         if (qhead < m_fmls.size() || !assumptions.empty()) {
-            for (expr* a : assumptions)
-                m_preprocess_state.freeze(a);
             TRACE("solver", tout << "qhead " << qhead << "\n");
-            m_preprocess_state.replay(qhead, assumptions);
+            m_preprocess_state.replay(qhead, assumptions);   
+            m_preprocess_state.freeze(assumptions);
             m_preprocess.reduce();
             if (!m.inc())
                 return;