From 3d995648eea72722cee40bd51694c2b2a2d3f374 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Aug 2014 20:39:20 +0900 Subject: [PATCH 1/7] partial fix to model generation bug for non-linear constraints: avoid epsilon refinment for non-shared variables Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 1 + src/smt/theory_arith_core.h | 3 ++- src/smt/theory_arith_nl.h | 12 ++++++++---- 3 files changed, 11 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index e7037f31a..998dd72e6 100644 --- a/src/smt/theory_arith.h +++ b/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_vector; + typedef map, default_eq > rational2var; static const int dead_row_id = -1; protected: diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 195d78e25..fbc043048 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -2780,7 +2780,6 @@ namespace smt { */ template void theory_arith::refine_epsilon() { - typedef map, default_eq > 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; diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index bab921ed2..d02c9e540 100644 --- a/src/smt/theory_arith_nl.h +++ b/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 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);); From 0df0174d6216a9cbaeb1dab0443e9a626ec5dddb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Aug 2014 15:24:08 +0100 Subject: [PATCH 2/7] .NET API: Enabled .xml documentation generation by default. Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b73f7a7a8..035cdd3c4 100644 --- a/scripts/mk_util.py +++ b/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 From 47ac5c06333bdd81b1f8084c4e5416cc5f235d23 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Aug 2014 11:41:04 +0900 Subject: [PATCH 3/7] fix doc bug Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 41ac1fa31..16073f3b3 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3523,7 +3523,7 @@ namespace Microsoft.Z3 /// /// /// The list of all configuration parameters can be obtained using the Z3 executable: - /// z3.exe -ini? + /// z3.exe -p /// Only a few configuration parameters are mutable once the context is created. /// An exception is thrown when trying to modify an immutable parameter. /// From 5a45711f22d92880c771e81e95da0c6525c781a4 Mon Sep 17 00:00:00 2001 From: mattpark Date: Mon, 11 Aug 2014 15:44:10 +0100 Subject: [PATCH 4/7] Dealt with some concurrency issues due to concurrent GC. --- src/api/dotnet/Context.cs | 2 +- src/api/dotnet/Z3Object.cs | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 16073f3b3..5436fe0a0 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3646,7 +3646,7 @@ namespace Microsoft.Z3 internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Fixedpoint_DRQ; } } - internal uint refCount = 0; + internal int refCount = 0; /// /// Finalizer. diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs index e8654ce21..8e474041a 100644 --- a/src/api/dotnet/Z3Object.cs +++ b/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 (m_ctx.refCount == 0) + if (Interlocked.Decrement(ref 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; From 0cf1f9c2106ee7110465809f0fd000946c9d0e9a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Aug 2014 12:15:58 +0100 Subject: [PATCH 5/7] .NET API context refcounting; changed int to long to be on the safe side on 64-bit platforms. Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Context.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 5436fe0a0..2b88cbab7 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3646,7 +3646,7 @@ namespace Microsoft.Z3 internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Fixedpoint_DRQ; } } - internal int refCount = 0; + internal long refCount = 0; /// /// Finalizer. From 37ed4b04d078d6d1e35db2799d769e8d4b87f775 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Aug 2014 12:18:00 +0100 Subject: [PATCH 6/7] Bugfix: param_refs didn't make it through to smt::solver (smt_params) in some cases. Thanks to user xor88 for pointing us in the right direction! Signed-off-by: Christoph M. Wintersteiger --- src/api/api_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index ac30a0c21..c8b1723f1 100644 --- a/src/api/api_solver.cpp +++ b/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) { From 60054ce469c3e2bc8c34e7b9285c8450e4232812 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2014 21:20:56 -0700 Subject: [PATCH 7/7] fix cache bug in PDR reported by Phillip Ruemmer Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 38 +++++++++++++++++++++++++------------ src/muz/pdr/pdr_context.h | 13 ++++++++----- 2 files changed, 34 insertions(+), 17 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index b09280d35..94dd5d0a0 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/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(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; - ++count; - if (count == 1 || is_repeated(n)) { + model_nodes ns; + model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value; + 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& model_search::cache(model_node const& n) { + obj_map >& 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 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()); } - void model_search::remove_node(model_node& n) { - if (0 == --cache(n).find(n.state())) { + void model_search::remove_node(model_node& n, bool backtrack) { + 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); - remove_node(*m_root); + erase_children(*m_root, false); + 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), diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 8a4f3e438..a85011600 100644 --- a/src/muz/pdr/pdr_context.h +++ b/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_nodes; + ast_manager& m; bool m_bfs; model_node* m_root; std::deque m_leaves; - vector > m_cache; + vector > m_cache; - obj_map& cache(model_node const& n); - void erase_children(model_node& n); + obj_map& cache(model_node const& 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();