Merge branch 'master' of https://github.com/z3prover/z3

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 @@ namespace Microsoft.Z3
         }
         #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 @@ namespace Microsoft.Z3
             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 @@ namespace Microsoft.Z3
 
             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:
+
+    Simplifiers.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/api/java/CMakeLists.txt

@@ -165,6 +165,8 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   SeqExpr.java
   SeqSort.java
   SetSort.java
+  Simplifier.java
+  SimplifierDecRefQueue.java
   SolverDecRefQueue.java
   Solver.java
   Sort.java

src/api/java/Context.java

@@ -3081,6 +3081,106 @@ public class Context implements AutoCloseable {
         Native.interrupt(nCtx());
     }
 
+    /**
+     * The number of supported simplifiers.
+     **/
+    public int getNumSimplifiers()
+    {
+        return Native.getNumSimplifiers(nCtx());
+    }
+
+    /**
+     * The names of all supported simplifiers.
+     **/
+    public String[] getSimplifierNames()
+    {
+
+        int n = getNumSimplifiers();
+        String[] res = new String[n];
+        for (int i = 0; i < n; i++)
+            res[i] = Native.getSimplifierName(nCtx(), i);
+        return res;
+    }
+
+    /**
+     * Returns a string containing a description of the simplifier with the given
+     * name.
+     **/
+    public String getSimplifierDescription(String name)
+    {
+        return Native.simplifierGetDescr(nCtx(), name);
+    }
+
+    /**
+     * Creates a new Simplifier.
+     **/
+    public Simplifier mkSimplifier(String name)
+    {
+        return new Simplifier(this, name);
+    }
+
+    /**
+     * Create a simplifier that applies {@code t1} and then {@code t1}
+     **/
+    public Simplifier andThen(Simplifier t1, Simplifier t2, Simplifier... ts)
+
+    {
+        checkContextMatch(t1);
+        checkContextMatch(t2);
+        checkContextMatch(ts);
+
+        long last = 0;
+        if (ts != null && ts.length > 0)
+        {
+            last = ts[ts.length - 1].getNativeObject();
+            for (int i = ts.length - 2; i >= 0; i--) {
+                last = Native.simplifierAndThen(nCtx(), ts[i].getNativeObject(),
+                    last);
+            }
+        }
+        if (last != 0)
+        {
+            last = Native.simplifierAndThen(nCtx(), t2.getNativeObject(), last);
+            return new Simplifier(this, Native.simplifierAndThen(nCtx(),
+                    t1.getNativeObject(), last));
+        } else
+            return new Simplifier(this, Native.simplifierAndThen(nCtx(),
+                    t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Create a simplifier that applies {@code t1} and then {@code t2}
+     *
+     * Remarks:  Shorthand for {@code AndThen}. 
+     **/
+    public Simplifier then(Simplifier t1, Simplifier t2, Simplifier... ts)
+    {
+        return andThen(t1, t2, ts);
+    }
+
+    /**
+     * Create a simplifier that applies {@code t} using the given set of
+     * parameters {@code p}.
+     **/
+    public Simplifier usingParams(Simplifier t, Params p)
+    {
+        checkContextMatch(t);
+        checkContextMatch(p);
+        return new Simplifier(this, Native.simplifierUsingParams(nCtx(),
+                t.getNativeObject(), p.getNativeObject()));
+    }
+
+    /**
+     * Create a simplifier that applies {@code t} using the given set of
+     * parameters {@code p}.
+     * Remarks: Alias for
+     * {@code UsingParams}
+     **/
+    public Simplifier with(Simplifier t, Params p)
+    {
+        return usingParams(t, p);
+    }
+
     /**
      * The number of supported Probes.
      **/
@@ -3279,6 +3379,14 @@ public class Context implements AutoCloseable {
                 t.getNativeObject()));
     }
 
+    /**
+     * Creates a solver that is uses the simplifier pre-processing.
+     **/
+    public Solver mkSolver(Solver s, Simplifier simp)
+    {
+        return new Solver(this, Native.solverAddSimplifier(nCtx(), s.getNativeObject(), simp.getNativeObject()));
+    }
+
     /**
      * Create a Fixedpoint context.
      **/
@@ -4209,6 +4317,7 @@ public class Context implements AutoCloseable {
     private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
     private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
     private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
+    private SimplifierDecRefQueue m_Simplifier_DRQ = new SimplifierDecRefQueue();
     private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
     private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
     private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
@@ -4293,6 +4402,11 @@ public class Context implements AutoCloseable {
         return m_Tactic_DRQ;
     }
 
+    public IDecRefQueue<Simplifier> getSimplifierDRQ()
+    {
+        return m_Simplifier_DRQ;
+    }
+
     public IDecRefQueue<Fixedpoint> getFixedpointDRQ()
     {
         return m_Fixedpoint_DRQ;
@@ -4323,6 +4437,7 @@ public class Context implements AutoCloseable {
         m_Optimize_DRQ.forceClear(this);
         m_Statistics_DRQ.forceClear(this);
         m_Tactic_DRQ.forceClear(this);
+        m_Simplifier_DRQ.forceClear(this);
         m_Fixedpoint_DRQ.forceClear(this);
 
         m_boolSort = null;

src/api/java/Simplifier.java

@@ -0,0 +1,58 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    Simplifiers.cs
+
+Abstract:
+
+    Z3 Managed API: Simplifiers
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-21
+
+--*/
+
+package com.microsoft.z3;
+
+
+public class Simplifier extends Z3Object {
+    /*
+     * A string containing a description of parameters accepted by the simplifier.
+     */
+
+    public String getHelp()
+    {
+	return Native.simplifierGetHelp(getContext().nCtx(), getNativeObject());
+    }
+
+    /*
+     * Retrieves parameter descriptions for Simplifiers.
+     */
+    public ParamDescrs getParameterDescriptions() {
+	return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject())); 
+    }
+
+    Simplifier(Context ctx, long obj)
+    {
+	super(ctx, obj);
+    }
+
+    Simplifier(Context ctx, String name)
+    {
+	super(ctx, Native.mkSimplifier(ctx.nCtx(), name));
+    }
+
+    @Override
+    void incRef()
+    {
+	Native.simplifierIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
+        getContext().getSimplifierDRQ().storeReference(getContext(), this);
+    }
+}	

src/api/java/SimplifierDecRefQueue.java

@@ -0,0 +1,31 @@
+/**
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    SimplifierDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
+package com.microsoft.z3;
+
+class SimplifierDecRefQueue extends IDecRefQueue<Simplifier> {
+    public SimplifierDecRefQueue() 
+    {
+        super();
+    }
+
+    @Override
+    protected void decRef(Context ctx, long obj)
+    {
+        Native.simplifierDecRef(ctx.nCtx(), obj);
+    }
+}

src/ast/simplifiers/dependent_expr_state.h

@@ -90,7 +90,8 @@ public:
     * 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/ast/simplifiers/dominator_simplifier.cpp

@@ -41,7 +41,7 @@ expr_ref dominator_simplifier::simplify_ite(app * ite) {
             if (is_subexpr(child, t) && !is_subexpr(child, e)) 
                 simplify_rec(child);            
         
-        pop(scope_level() - old_lvl);
+        local_pop(scope_level() - old_lvl);
         expr_ref new_t = simplify_arg(t);
         reset_cache();
         if (!assert_expr(new_c, true)) {
@@ -50,7 +50,7 @@ expr_ref dominator_simplifier::simplify_ite(app * ite) {
         for (expr * child : tree(ite)) 
             if (is_subexpr(child, e) && !is_subexpr(child, t)) 
                 simplify_rec(child);
-        pop(scope_level() - old_lvl);
+        local_pop(scope_level() - old_lvl);
         expr_ref new_e = simplify_arg(e);
 
         if (c == new_c && t == new_t && e == new_e) {
@@ -159,7 +159,7 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
         r = simplify_arg(arg);                              
         args.push_back(r);                                  
         if (!assert_expr(r, !is_and)) {                     
-            pop(scope_level() - old_lvl);                   
+            local_pop(scope_level() - old_lvl);                   
             r = is_and ? m.mk_false() : m.mk_true();        
             reset_cache();
             return true;
@@ -181,7 +181,7 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
         args.reverse();
     }
     
-    pop(scope_level() - old_lvl);
+    local_pop(scope_level() - old_lvl);
     reset_cache();
     return { is_and ? mk_and(args) : mk_or(args), m };
 }
@@ -191,7 +191,7 @@ expr_ref dominator_simplifier::simplify_not(app * e) {
     ENSURE(m.is_not(e, ee));
     unsigned old_lvl = scope_level();
     expr_ref t = simplify_rec(ee);
-    pop(scope_level() - old_lvl);
+    local_pop(scope_level() - old_lvl);
     reset_cache();
     return mk_not(t);
 }
@@ -245,7 +245,7 @@ void dominator_simplifier::reduce() {
             }
             m_fmls.update(i, dependent_expr(m, r, new_pr, d));
         }
-        pop(scope_level());
+        local_pop(scope_level());
 
         // go backwards
         m_forward = false;
@@ -268,7 +268,7 @@ void dominator_simplifier::reduce() {
             }
             m_fmls.update(i, dependent_expr(m, r, new_pr, d));
         }
-        pop(scope_level());
+        local_pop(scope_level());
     }
     SASSERT(scope_level() == 0);
 }

src/ast/simplifiers/dominator_simplifier.h

@@ -48,7 +48,7 @@ class dominator_simplifier : public dependent_expr_simplifier {
     expr* idom(expr *e) const { return m_dominators.idom(e); }
 
     unsigned scope_level() { return m_simplifier->scope_level(); }
-    void pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); }
+    void local_pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); }
     bool assert_expr(expr* f, bool sign) { return m_simplifier->assert_expr(f, sign); }
 
 

src/ast/substitution/demodulator_rewriter.cpp

@@ -780,7 +780,6 @@ void demodulator_rewriter::operator()(expr_ref_vector const& exprs,
 
 
 demodulator_match_subst::demodulator_match_subst(ast_manager & m):
-    m(m),
     m_subst(m) {
 }
 

src/ast/substitution/demodulator_rewriter.h

@@ -111,7 +111,6 @@ class demodulator_match_subst {
     typedef std::pair<expr *, expr *>      expr_pair;
     typedef obj_pair_hashtable<expr, expr> cache;
     
-    ast_manager &         m;
     substitution          m_subst;
     cache                 m_cache;
     svector<expr_pair>    m_todo;

src/math/lp/nla_powers.cpp

@@ -131,7 +131,7 @@ namespace nla {
             return l_false;
         }
 
-        if (xval >= 3 && yval != 0 & rval <= yval + 1) {
+        if (xval >= 3 && yval != 0 && rval <= yval + 1) {
             new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1");
             lemma |= ineq(x, llc::LT, rational(3));
             lemma |= ineq(y, llc::EQ, rational::zero());

src/muz/spacer/spacer_cluster.cpp

@@ -378,7 +378,7 @@ void lemma_cluster_finder::cluster(lemma_ref &lemma) {
                                    << pattern << "\n"
                                    << " and lemma cube: " << lcube << "\n";);
 
-    for (const lemma_ref &l : neighbours) {
+    for (auto l : neighbours) {
         SASSERT(cluster->can_contain(l));
         bool added = cluster->add_lemma(l, false);
         (void)added;

src/smt/theory_fpa.cpp

@@ -671,7 +671,6 @@ namespace smt {
 
         out << "equivalence classes:\n";
         for (enode * n : ctx.enodes()) {
-            expr * e = n->get_expr();
             expr * r = n->get_root()->get_expr();
             out << r->get_id() << " --> " << enode_pp(n, ctx) << "\n";
         }

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;
@@ -225,7 +224,7 @@ public:
     }
 
     proof_ref m_proof;
-    proof* get_proof_core() { 
+    proof* get_proof_core() override { 
         proof* p = s->get_proof(); 
         m_proof = p;
         if (p) {
@@ -272,7 +271,7 @@ public:
     std::string reason_unknown() const override { return s->reason_unknown(); }
     void set_reason_unknown(char const* msg) override { s->set_reason_unknown(msg); }
     void get_labels(svector<symbol>& r) override { s->get_labels(r); }
-    void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); replace(r); }
+    void get_unsat_core(expr_ref_vector& r) override { s->get_unsat_core(r); replace(r); }
     ast_manager& get_manager() const override { return s->get_manager(); }    
     void reset_params(params_ref const& p) override { s->reset_params(p); }
     params_ref const& get_params() const override { return s->get_params(); }
@@ -314,7 +313,7 @@ public:
             clauses1.push_back(expr_ref_vector(m, c.size(), es.data() + offset));
             offset += c.size();
         }
-        return check_sat_cc(cube1, clauses1); 
+        return s->check_sat_cc(cube1, clauses1); 
     }
 
     lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override {