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

examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs

@@ -0,0 +1,36 @@
+using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following 
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("SolverFoundation.Plugin.Z3")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("Microsoft")]
+[assembly: AssemblyProduct("SolverFoundation.Plugin.Z3")]
+[assembly: AssemblyCopyright("Copyright © Microsoft 2010")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible 
+// to COM components.  If you need to access a type in this assembly from 
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// The following GUID is for the ID of the typelib if this project is exposed to COM
+[assembly: Guid("ed1476c0-96de-4d2c-983d-3888b140c3ad")]
+
+// Version information for an assembly consists of the following four values:
+//
+//      Major Version
+//      Minor Version 
+//      Build Number
+//      Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers 
+// by using the '*' as shown below:
+// [assembly: AssemblyVersion("1.0.*")]
+[assembly: AssemblyVersion("1.0.0.0")]
+[assembly: AssemblyFileVersion("1.0.0.0")]

examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs

@@ -47,7 +47,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
         private Dictionary<int, Expr> _variables = new Dictionary<int, Expr>();
 
         /// <summary>A map from MSF variable ids to Z3 goal ids</summary>
-        private Dictionary<IGoal, uint> _goals = new Dictionary<IGoal, uint>();
+        private Dictionary<IGoal, Optimize.Handle> _goals = new Dictionary<IGoal, Optimize.Handle>();
 
         internal Z3BaseSolver(IRowVariableModel model)
         {
@@ -64,7 +64,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
             get { return _variables; }
         }
 
-        internal Dictionary<IGoal, uint> Goals
+        internal Dictionary<IGoal, Optimize.Handle> Goals
         {
             get { return _goals; }
         }
@@ -332,7 +332,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
                             // Remember all objective values
                             foreach (var pair in _goals)
                             {
-                                var optimalValue = Utils.ToRational(_optSolver.GetUpper(pair.Value));
+                                var optimalValue = Utils.ToRational(pair.Value.Upper);
                                 _model.SetValue(pair.Key.Index, optimalValue);
                             }
                             model.Dispose();
@@ -356,7 +356,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
                                     // Remember all objective values
                                     foreach (var pair in _goals)
                                     {
-                                        var optimalValue = Utils.ToRational(_optSolver.GetUpper(pair.Value));
+                                        var optimalValue = Utils.ToRational(pair.Value.Upper);
                                         _model.SetValue(pair.Key.Index, optimalValue);
                                     }
                                     subOptimalModel.Dispose();

src/ast/rewriter/seq_rewriter.h

@@ -149,6 +149,9 @@ public:
     void updt_params(params_ref const & p) {}
     static void get_param_descrs(param_descrs & r) {}
 
+    void set_solver(expr_solver* solver) { m_re2aut.set_solver(solver); }
+
+
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
 

src/ast/rewriter/th_rewriter.cpp

@@ -692,6 +692,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         return false;
     }
 
+
 };
 
 template class rewriter_tpl<th_rewriter_cfg>;
@@ -705,6 +706,10 @@ struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
     expr_ref mk_app(func_decl* f, unsigned sz, expr* const* args) {
         return m_cfg.mk_app(f, sz, args);
     }
+
+    void set_solver(expr_solver* solver) {
+        m_cfg.m_seq_rw.set_solver(solver);
+    }
 };
 
 th_rewriter::th_rewriter(ast_manager & m, params_ref const & p):
@@ -790,3 +795,7 @@ void th_rewriter::reset_used_dependencies() {
 expr_ref th_rewriter::mk_app(func_decl* f, unsigned num_args, expr* const* args) {
     return m_imp->mk_app(f, num_args, args);
 }
+
+void th_rewriter::set_solver(expr_solver* solver) {
+    m_imp->set_solver(solver);
+}

src/ast/rewriter/th_rewriter.h

@@ -25,6 +25,8 @@ Notes:
 
 class expr_substitution;
 
+class expr_solver;
+
 class th_rewriter {
     struct     imp;
     imp *      m_imp;
@@ -58,6 +60,9 @@ public:
     // Remark: reset_used_dependecies will reset the internal cache if get_used_dependencies() != 0
     expr_dependency * get_used_dependencies();
     void reset_used_dependencies();
+
+    void set_solver(expr_solver* solver);
+
 };
 
 #endif

src/cmd_context/simplify_cmd.cpp

@@ -24,9 +24,30 @@ Notes:
 #include"scoped_timer.h"
 #include"scoped_ctrl_c.h"
 #include"cancel_eh.h"
+#include"seq_rewriter.h"
 #include<iomanip>
 
 class simplify_cmd : public parametric_cmd {
+
+    class th_solver : public expr_solver {
+        cmd_context& m_ctx;
+        params_ref   m_params;
+        ref<solver> m_solver;
+    public:
+        th_solver(cmd_context& ctx): m_ctx(ctx) {}
+        
+        virtual lbool check_sat(expr* e) {
+            if (!m_solver) {
+                m_solver = m_ctx.get_solver_factory()(m_ctx.m(), m_params, false, true, false, symbol::null);
+            }
+            m_solver->push();
+            m_solver->assert_expr(e);
+            lbool r = m_solver->check_sat(0,0);
+            m_solver->pop(1);
+            return r;
+        }
+    };
+
     expr *                   m_target;
 public:
     simplify_cmd(char const * name = "simplify"):parametric_cmd(name) {}
@@ -70,10 +91,12 @@ public:
         if (m_params.get_bool("som", false))
             m_params.set_bool("flat", true);
         th_rewriter s(ctx.m(), m_params);
+        th_solver solver(ctx);
+        s.set_solver(alloc(th_solver, ctx));
         unsigned cache_sz;
         unsigned num_steps = 0;
         unsigned timeout   = m_params.get_uint("timeout", UINT_MAX);
-        unsigned rlimit    = m_params.get_uint("rlimit", UINT_MAX);
+        unsigned rlimit    = m_params.get_uint("rlimit", UINT_MAX);        
         bool failed = false;
         cancel_eh<reslimit> eh(ctx.m().limit());
         { 

src/solver/solver.h

@@ -149,8 +149,13 @@ public:
     */
     virtual expr * get_assumption(unsigned idx) const = 0;
 
-
+    /**
-
+    \brief under assumptions, asms, retrieve set of consequences that fix values for expressions that can be 
+      built from fns. For functions that take 0 arguments, we require that the function returns all consequences
+      that mention these functions. The consequences are clauses whose first literal constrain one of the 
+      functions from fns and the other literals are negations of literals from asms.
+     */
+    //virtual lbool get_consequences(expr_ref_vector const& asms, func_ref_vector const& fns, expr_ref_vector& consequences);
 
     /**
        \brief Display the content of this solver.

src/test/uint_set.cpp

@@ -131,6 +131,32 @@ static void tst4() {
     SASSERT(!s.contains(0));
 }
 
+#include "map.h"
+
+template <typename Value>
+struct uint_map : public map<uint_set, Value, uint_set::hash, uint_set::eq> {};
+
+static void tst5() {
+    uint_set s;
+    std::cout << s.get_hash() << "\n";
+    s.insert(1);
+    std::cout << s.get_hash() << "\n";
+    s.insert(2);
+    std::cout << s.get_hash() << "\n";
+    s.insert(44);
+    std::cout << s.get_hash() << "\n";
+
+    uint_map<unsigned> m;
+    m.insert(s, 1);
+    s.insert(4);
+    m.insert(s, 3);
+    uint_map<unsigned>::iterator it = m.begin(), end = m.end();
+    for (; it != end; ++it) {
+        std::cout << it->m_key << " : " << it->m_value << "\n";
+    }
+    
+}
+
 void tst_uint_set() {
     for (unsigned i = 0; i < 100; i++) {
         tst1(1 + rand()%31);
@@ -146,5 +172,6 @@ void tst_uint_set() {
     tst3(12);
     tst3(100);
     tst4();
+    tst5();
 }
 

src/util/uint_set.h

@@ -218,6 +218,18 @@ public:
 
     iterator const begin() const { return iterator(*this, false); }
     iterator const end() const { return iterator(*this, true); }
+
+    unsigned get_hash() const {
+        unsigned h = 0;
+        for (unsigned i = 0; i < size(); ++i) {
+            h += (i+1)*((*this)[i]);
+        }
+        return h;
+    }
+
+    struct eq { bool operator()(uint_set const& s1, uint_set const& s2) const { return s1 == s2; } };
+    struct hash { unsigned operator()(uint_set const& s) const { return s.get_hash(); } };
+        
 };
 
 inline std::ostream & operator<<(std::ostream & target, const uint_set & s) {