merging with unstable

scripts/mk_util.py

@@ -1151,7 +1151,11 @@ class DotNetDLLComponent(Component):
                 out.write(' ')
                 out.write(cs_file)
             out.write('\n')
-            out.write('  csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /define:DEBUG;TRACE /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /debug+ /debug:full /filealign:512 /optimize- /linkresource:%s.dll /out:%s.dll /target:library' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name))
+            out.write('  csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /filealign:512 /linkresource:%s.dll /out:%s.dll /target:library /doc:%s.xml' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name, self.dll_name))
+            if DEBUG_MODE:
+                out.write(' /define:DEBUG;TRACE /debug+ /debug:full /optimize-')
+            else:
+                out.write(' /optimize+')
             if VS_X64:
                 out.write(' /platform:x64')
             else:
@@ -1174,6 +1178,13 @@ class DotNetDLLComponent(Component):
             mk_dir(os.path.join(dist_path, 'bin'))
             shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
                         '%s.dll' % os.path.join(dist_path, 'bin', self.dll_name))
+            shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
+                        '%s.xml' % os.path.join(dist_path, 'bin', self.dll_name))
+            if DEBUG_MODE:
+                shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
+                            '%s.pdb' % os.path.join(dist_path, 'bin', self.dll_name))
+
+
 
     def mk_unix_dist(self, build_path, dist_path):
         # Do nothing

src/api/api_solver.cpp

@@ -40,6 +40,7 @@ extern "C" {
         params_ref p = s->m_params;
         mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
         s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
+        s->m_solver->updt_params(p);
     }
 
     static void init_solver(Z3_context c, Z3_solver s) {

src/api/dotnet/Context.cs

@@ -3523,7 +3523,7 @@ namespace Microsoft.Z3
         /// </summary>
         /// <remarks>
         /// The list of all configuration parameters can be obtained using the Z3 executable:
-        /// <c>z3.exe -ini?</c>
+        /// <c>z3.exe -p</c>
         /// Only a few configuration parameters are mutable once the context is created.
         /// An exception is thrown when trying to modify an immutable parameter.
         /// </remarks>
@@ -3646,7 +3646,7 @@ namespace Microsoft.Z3
         internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
 
 
-        internal uint refCount = 0;
+        internal long refCount = 0;
 
         /// <summary>
         /// Finalizer.

src/api/dotnet/Z3Object.cs

@@ -19,6 +19,7 @@ Notes:
 
 using System;
 using System.Diagnostics.Contracts;
+using System.Threading;
 
 namespace Microsoft.Z3
 {
@@ -50,8 +51,7 @@ namespace Microsoft.Z3
 
             if (m_ctx != null)
             {
-                m_ctx.refCount--;
+                if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
-                if (m_ctx.refCount == 0)
                     GC.ReRegisterForFinalize(m_ctx);
                 m_ctx = null;
             }
@@ -77,7 +77,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(ctx != null);
 
-            ctx.refCount++;
+            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
         }
 
@@ -85,7 +85,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(ctx != null);
 
-            ctx.refCount++;
+            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
             IncRef(obj);
             m_n_obj = obj;

src/muz/pdr/pdr_context.cpp

@@ -736,6 +736,11 @@ namespace pdr {
         m_closed = true; 
     }
 
+    void model_node::reopen() {
+        SASSERT(m_closed);
+        m_closed = false;
+    }
+
     static bool is_ini(datalog::rule const& r) {
         return r.get_uninterpreted_tail_size() == 0;
     }
@@ -745,6 +750,7 @@ namespace pdr {
             return const_cast<datalog::rule*>(m_rule);
         }
         // only initial states are not set by the PDR search.
+        SASSERT(m_model.get());
         datalog::rule const& rl1 = pt().find_rule(*m_model);
         if (is_ini(rl1)) {
             set_rule(&rl1);
@@ -864,9 +870,10 @@ namespace pdr {
     }
 
     void model_search::add_leaf(model_node& n) {
-        unsigned& count = cache(n).insert_if_not_there2(n.state(), 0)->get_data().m_value;
+        model_nodes ns;
-        ++count;
+        model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value;
-        if (count == 1 || is_repeated(n)) {
+        nodes.push_back(&n);
+        if (nodes.size() == 1 || is_repeated(n)) {
             set_leaf(n);
         }
         else {
@@ -875,7 +882,7 @@ namespace pdr {
     }
 
     void model_search::set_leaf(model_node& n) {
-        erase_children(n);
+        erase_children(n, true);
         SASSERT(n.is_open());      
         enqueue_leaf(n);
     }
@@ -897,7 +904,7 @@ namespace pdr {
         set_leaf(*root);
     }
 
-    obj_map<expr, unsigned>& model_search::cache(model_node const& n) {
+    obj_map<expr, ptr_vector<model_node> >& model_search::cache(model_node const& n) {
         unsigned l = n.orig_level();
         if (l >= m_cache.size()) {
             m_cache.resize(l + 1);
@@ -905,7 +912,7 @@ namespace pdr {
         return m_cache[l];
     }
 
-    void model_search::erase_children(model_node& n) {
+    void model_search::erase_children(model_node& n, bool backtrack) {
         ptr_vector<model_node> todo, nodes;
         todo.append(n.children());
         erase_leaf(n);
@@ -916,13 +923,20 @@ namespace pdr {
             nodes.push_back(m);
             todo.append(m->children());
             erase_leaf(*m);
-            remove_node(*m);
+            remove_node(*m, backtrack);
         }
         std::for_each(nodes.begin(), nodes.end(), delete_proc<model_node>());
     }
 
-    void model_search::remove_node(model_node& n) {
+    void model_search::remove_node(model_node& n, bool backtrack) {
-        if (0 == --cache(n).find(n.state())) {
+        model_nodes& nodes = cache(n).find(n.state());
+        nodes.erase(&n);
+        if (nodes.size() > 0 && n.is_open() && backtrack) {
+            for (unsigned i = 0; i < nodes.size(); ++i) {
+                nodes[i]->reopen();
+            }
+        }
+        if (nodes.empty()) {            
             cache(n).remove(n.state());
         }
     }
@@ -1203,8 +1217,8 @@ namespace pdr {
 
     void model_search::reset() {
         if (m_root) {
-            erase_children(*m_root);
+            erase_children(*m_root, false);
-            remove_node(*m_root);
+            remove_node(*m_root, false);
             dealloc(m_root);
             m_root = 0;
         }
@@ -1240,7 +1254,7 @@ namespace pdr {
           m_pm(m_fparams, params.max_num_contexts(), m),
           m_query_pred(m),
           m_query(0),
-          m_search(m_params.bfs_model_search()),
+          m_search(m_params.bfs_model_search(), m),
           m_last_result(l_undef),
           m_inductive_lvl(0),
           m_expanded_lvl(0),

src/muz/pdr/pdr_context.h

@@ -231,6 +231,7 @@ namespace pdr {
         }
 
         void set_closed();     
+        void reopen();
         void set_pre_closed() { m_closed = true; }
         void reset() { m_children.reset(); }
 
@@ -243,19 +244,21 @@ namespace pdr {
     };
 
     class model_search {
+        typedef ptr_vector<model_node> model_nodes;
+        ast_manager&       m;
         bool               m_bfs;
         model_node*        m_root;
         std::deque<model_node*> m_leaves;
-        vector<obj_map<expr, unsigned> > m_cache;
+        vector<obj_map<expr, model_nodes > > m_cache;
         
-        obj_map<expr, unsigned>& cache(model_node const& n);
+        obj_map<expr, model_nodes>& cache(model_node const& n);
-        void erase_children(model_node& n);
+        void erase_children(model_node& n, bool backtrack);
         void erase_leaf(model_node& n);
-        void remove_node(model_node& n);
+        void remove_node(model_node& n, bool backtrack);
         void enqueue_leaf(model_node& n); // add leaf to priority queue.
         void update_models();
     public:
-        model_search(bool bfs): m_bfs(bfs), m_root(0) {}
+        model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {}
         ~model_search();
 
         void reset();

src/smt/theory_arith.h

@@ -85,6 +85,7 @@ namespace smt {
         typedef typename Ext::numeral     numeral;
         typedef typename Ext::inf_numeral inf_numeral;
         typedef vector<numeral> numeral_vector; 
+        typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
 
         static const int    dead_row_id = -1;
     protected:

src/smt/theory_arith_core.h

@@ -2780,7 +2780,6 @@ namespace smt {
     */
     template<typename Ext>
     void theory_arith<Ext>::refine_epsilon() {
-        typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
         while (true) {
             rational2var mapping;
             theory_var num = get_num_vars();
@@ -2788,6 +2787,8 @@ namespace smt {
             for (theory_var v = 0; v < num; v++) {
                 if (is_int(v))
                     continue;
+                if (!get_context().is_shared(get_enode(v)))
+                    continue;
                 inf_numeral const & val = get_value(v);
                 rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
                 theory_var v2;

src/smt/theory_arith_nl.h

@@ -654,6 +654,7 @@ namespace smt {
         }
         return get_value(v, computed_epsilon) == val;
     }
+    
 
     /**
        \brief Return true if for every monomial x_1 * ... * x_n,
@@ -2309,8 +2310,9 @@ namespace smt {
         if (m_nl_monomials.empty())
             return FC_DONE;
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return FC_DONE;
+        }
 
         if (!m_params.m_nl_arith)
             return FC_GIVEUP;
@@ -2338,9 +2340,10 @@ namespace smt {
         if (!max_min_nl_vars())
             return FC_CONTINUE;
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
-        
+        }
+
         svector<theory_var> vars;
         get_non_linear_cluster(vars);
 
@@ -2391,8 +2394,9 @@ namespace smt {
         }
         while (m_nl_strategy_idx != old_idx);
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
+        }
 
         TRACE("non_linear", display(tout););