From 9d2c86f214304d224b7c439bc3bfd43da002dbdc Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 8 Dec 2017 20:31:22 -0500 Subject: [PATCH 01/12] fix incorrect clause in argumentsValid subterm of substr reduction --- src/smt/theory_str.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 7936b581c..022a2ad73 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1450,7 +1450,7 @@ namespace smt { // pos < strlen(base) // --> pos + -1*strlen(base) < 0 argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge( - m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)), + m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, mk_strlen(substrBase))), zero))); // len >= 0 From 2e186633ee17f9ee3c8265f976321cb0cd8f44b3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 11 Dec 2017 14:59:25 +0000 Subject: [PATCH 02/12] Turned assertion failure into proper error message. --- src/ast/ast.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index e7d808b2b..3824325b3 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1289,7 +1289,7 @@ decl_kind user_sort_plugin::register_name(symbol s) { decl_plugin * user_sort_plugin::mk_fresh() { user_sort_plugin * p = alloc(user_sort_plugin); - for (symbol const& s : m_sort_names) + for (symbol const& s : m_sort_names) p->register_name(s); return p; } @@ -1415,7 +1415,7 @@ ast_manager::~ast_manager() { p->finalize(); } for (decl_plugin* p : m_plugins) { - if (p) + if (p) dealloc(p); } m_plugins.reset(); @@ -1454,13 +1454,13 @@ ast_manager::~ast_manager() { mark_array_ref(mark, to_quantifier(n)->get_num_patterns(), to_quantifier(n)->get_patterns()); mark_array_ref(mark, to_quantifier(n)->get_num_no_patterns(), to_quantifier(n)->get_no_patterns()); break; - } - } + } + } for (ast * n : m_ast_table) { if (!mark.is_marked(n)) { roots.push_back(n); } - } + } SASSERT(!roots.empty()); for (unsigned i = 0; i < roots.size(); ++i) { ast* a = roots[i]; @@ -1683,7 +1683,7 @@ ast * ast_manager::register_node_core(ast * n) { bool contains = m_ast_table.contains(n); CASSERT("nondet_bug", contains || slow_not_contains(n)); #endif - + ast * r = m_ast_table.insert_if_not_there(n); SASSERT(r->m_hash == h); if (r != n) { @@ -2358,8 +2358,9 @@ quantifier * ast_manager::mk_quantifier(bool forall, unsigned num_decls, sort * unsigned num_patterns, expr * const * patterns, unsigned num_no_patterns, expr * const * no_patterns) { SASSERT(body); - SASSERT(num_patterns == 0 || num_no_patterns == 0); SASSERT(num_decls > 0); + if (num_patterns != 0 && num_no_patterns != 0) + throw ast_exception("simultaneous patterns and no-patterns not supported"); DEBUG_CODE({ for (unsigned i = 0; i < num_patterns; ++i) { TRACE("ast", tout << i << " " << mk_pp(patterns[i], *this) << "\n";); @@ -2763,7 +2764,7 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs } proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs, expr * n1, expr * n2) { - if (num_proofs == 0) + if (num_proofs == 0) return nullptr; if (num_proofs == 1) return proofs[0]; From 49678065bd133721445bb7ef7be6ac03d826dd36 Mon Sep 17 00:00:00 2001 From: Ivan Gotovchits Date: Wed, 13 Dec 2017 14:37:19 -0500 Subject: [PATCH 03/12] fixes compilation flags for OCaml plugins The `-linkall` option is needed for a plugin to be standalone, otherwise it will miss those dependencies that are not used. --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b155fd7c2..03256125c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1990,7 +1990,7 @@ class MLComponent(Component): out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3dllso, z3mls)) out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3)) out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls)) - out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls)) + out.write('\t%s -linkall -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls)) out.write('\n') out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls)) From 5a479fca76d6e249490c7a9b42d9431318ddb6c9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2017 13:48:24 -0800 Subject: [PATCH 04/12] generalize model finder code to be independent of conjunction elimination Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_finder.cpp | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 11202d58a..28a65f898 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2272,10 +2272,9 @@ namespace smt { process_literal(atom, pol == NEG); } - void process_or(app * n, polarity p) { - unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - visit_formula(n->get_arg(i), p); + void process_and_or(app * n, polarity p) { + for (expr* arg : *n) + visit_formula(arg, p); } void process_ite(app * n, polarity p) { @@ -2306,13 +2305,13 @@ namespace smt { if (is_app(curr)) { if (to_app(curr)->get_family_id() == m_manager.get_basic_family_id() && m_manager.is_bool(curr)) { switch (static_cast(to_app(curr)->get_decl_kind())) { - case OP_AND: case OP_IMPLIES: case OP_XOR: UNREACHABLE(); // simplifier eliminated ANDs, IMPLIEs, and XORs break; case OP_OR: - process_or(to_app(curr), pol); + case OP_AND: + process_and_or(to_app(curr), pol); break; case OP_NOT: visit_formula(to_app(curr)->get_arg(0), neg(pol)); From 58c6cb87c3bc26824fd2386e2eeb74bb3a826537 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Dec 2017 11:48:22 -0800 Subject: [PATCH 05/12] small improvements to QF_NIA tactic Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_nl.h | 1 + src/tactic/smtlogics/qfnia_tactic.cpp | 35 +++++++++++++++++++++------ 2 files changed, 29 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 230b6de77..87b811e8f 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -711,6 +711,7 @@ namespace smt { if (ctx.is_relevant(get_enode(*it)) && !check_monomial_assignment(*it, computed_epsilon)) { TRACE("non_linear_failed", tout << "check_monomial_assignment failed for:\n" << mk_ismt2_pp(var2expr(*it), get_manager()) << "\n"; display_var(tout, *it);); + return false; } } diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 3fb733ca4..f0a4ceb57 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -26,8 +26,10 @@ Notes: #include "tactic/bv/max_bv_sharing_tactic.h" #include "sat/tactic/sat_tactic.h" #include "tactic/arith/nla2bv_tactic.h" +#include "tactic/arith/elim01_tactic.h" #include "tactic/core/ctx_simplify_tactic.h" #include "tactic/core/cofactor_term_ite_tactic.h" +#include "nlsat/tactic/qfnra_nlsat_tactic.h" static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { params_ref p = p_ref; @@ -61,8 +63,6 @@ static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) { ctx_simp_p.set_uint("max_depth", 30); ctx_simp_p.set_uint("max_steps", 5000000); - params_ref simp_p = p_ref; - simp_p.set_bool("hoist_mul", true); params_ref elim_p = p_ref; elim_p.set_uint("max_memory",20); @@ -73,21 +73,42 @@ static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) { using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), using_params(mk_simplify_tactic(m), pull_ite_p), mk_elim_uncnstr_tactic(m), - skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p)), - using_params(mk_simplify_tactic(m), simp_p)); + mk_elim01_tactic(m), + skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p))); } static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) { params_ref nia2sat_p = p; - nia2sat_p.set_uint("nla2bv_max_bv_size", 64); + nia2sat_p.set_uint("nla2bv_max_bv_size", 64); + params_ref simp_p = p; + simp_p.set_bool("hoist_mul", true); // hoist multipliers to create smaller circuits. - return and_then(mk_nla2bv_tactic(m, nia2sat_p), + return and_then(using_params(mk_simplify_tactic(m), simp_p), + mk_nla2bv_tactic(m, nia2sat_p), mk_qfnia_bv_solver(m, p), mk_fail_if_undecided_tactic()); } +static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) { + params_ref nia2sat_p = p; + nia2sat_p.set_uint("nla2bv_max_bv_size", 64); + params_ref simp_p = p; + simp_p.set_bool("som", true); // expand into sums of monomials + simp_p.set_bool("factor", false); + + + return and_then(using_params(mk_simplify_tactic(m), simp_p), + try_for(mk_qfnra_nlsat_tactic(m, simp_p), 10000), + mk_fail_if_undecided_tactic()); +} + tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { + params_ref simp_p = p; + simp_p.set_bool("som", true); // expand into sums of monomials + return and_then(mk_qfnia_premable(m, p), or_else(mk_qfnia_sat_solver(m, p), - mk_smt_tactic())); + mk_qfnia_nlsat_solver(m, p), + and_then(using_params(mk_simplify_tactic(m), simp_p), + mk_smt_tactic()))); } From e5fa35e969283027e6ca4b75a5dc5ee493c2e5e9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Dec 2017 17:07:17 -0800 Subject: [PATCH 06/12] add integer branch and bound to nlsat Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_interval_set.cpp | 4 +- src/nlsat/nlsat_interval_set.h | 2 +- src/nlsat/nlsat_solver.cpp | 70 ++++++++++++++++++++++++--- src/tactic/smtlogics/qfnia_tactic.cpp | 2 +- 4 files changed, 68 insertions(+), 10 deletions(-) diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index 2028095f4..090f94eeb 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -672,14 +672,14 @@ namespace nlsat { return new_set; } - void interval_set_manager::peek_in_complement(interval_set const * s, anum & w, bool randomize) { + void interval_set_manager::peek_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize) { SASSERT(!is_full(s)); if (s == 0) { if (randomize) { int num = m_rand() % 2 == 0 ? 1 : -1; #define MAX_RANDOM_DEN_K 4 int den_k = (m_rand() % MAX_RANDOM_DEN_K); - int den = 1 << den_k; + int den = is_int ? 1 : (1 << den_k); scoped_mpq _w(m_am.qm()); m_am.qm().set(_w, num, den); m_am.set(w, _w); diff --git a/src/nlsat/nlsat_interval_set.h b/src/nlsat/nlsat_interval_set.h index 24b2ab37f..363d48de9 100644 --- a/src/nlsat/nlsat_interval_set.h +++ b/src/nlsat/nlsat_interval_set.h @@ -108,7 +108,7 @@ namespace nlsat { \pre !is_full(s) */ - void peek_in_complement(interval_set const * s, anum & w, bool randomize); + void peek_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize); }; typedef obj_ref interval_set_ref; diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index c5e9babae..0ccaa2f2c 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -903,15 +903,18 @@ namespace nlsat { */ lbool value(literal l) { lbool val = assigned_value(l); - if (val != l_undef) + if (val != l_undef) { return val; + } bool_var b = l.var(); atom * a = m_atoms[b]; - if (a == 0) + if (a == 0) { return l_undef; + } var max = a->max_var(); - if (!m_assignment.is_assigned(max)) + if (!m_assignment.is_assigned(max)) { return l_undef; + } val = to_lbool(m_evaluator.eval(a, l.sign())); TRACE("value_bug", tout << "value of: "; display(tout, l); tout << " := " << val << "\n"; tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n"; @@ -1168,7 +1171,7 @@ namespace nlsat { void select_witness() { scoped_anum w(m_am); SASSERT(!m_ism.is_full(m_infeasible[m_xk])); - m_ism.peek_in_complement(m_infeasible[m_xk], w, m_randomize); + m_ism.peek_in_complement(m_infeasible[m_xk], m_is_int[m_xk], w, m_randomize); TRACE("nlsat", tout << "infeasible intervals: "; m_ism.display(tout, m_infeasible[m_xk]); tout << "\n"; tout << "assigning "; m_display_var(tout, m_xk); tout << "(x" << m_xk << ") -> " << w << "\n";); @@ -1232,6 +1235,61 @@ namespace nlsat { } } + lbool search_check() { + lbool r = l_undef; + while (true) { + r = search(); + if (r != l_true) break; + random_gen r(++m_random_seed); + unsigned start = r(num_vars()); + for (var y = 0; y < num_vars(); y++) { + var x = (y + start) % num_vars(); + if (m_is_int[x] && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) { + scoped_anum v(m_am), vlo(m_am), vhi(m_am); + rational lo, hi; + bool is_even = false; + v = m_assignment.value(x); + init_search(); + m_am.int_lt(v, vlo); + m_am.int_gt(v, vhi); + if (!m_am.is_int(vlo)) break; + if (!m_am.is_int(vhi)) break; + m_am.to_rational(vlo, lo); + m_am.to_rational(vhi, hi); + + // derive tight bounds. + while (true) { + lo++; + if (!m_am.gt(v, lo.to_mpq())) { lo--; break; } + } + while (true) { + hi--; + if (!m_am.lt(v, hi.to_mpq())) { hi++; break; } + } + + polynomial_ref p(m_pm); + rational one(1); + m_lemma.reset(); + p = m_pm.mk_linear(1, &one, &x, -lo); + poly* p1 = p.get(); + m_lemma.push_back(~mk_ineq_literal(atom::GT, 1, &p1, &is_even)); + p = m_pm.mk_linear(1, &one, &x, -hi); + poly* p2 = p.get(); + m_lemma.push_back(~mk_ineq_literal(atom::LT, 1, &p2, &is_even)); + + // perform branch and bound + clause * cls = mk_clause(m_lemma.size(), m_lemma.c_ptr(), false, 0); + if (cls) { + TRACE("nlsat", display(tout << "conflict " << lo << " " << hi, *cls); tout << "\n";); + } + r = l_undef; + break; + } + } + } + return r; + } + lbool check() { TRACE("nlsat_smt2", display_smt2(tout);); TRACE("nlsat_fd", tout << "is_full_dimensional: " << is_full_dimensional() << "\n";); @@ -1250,7 +1308,7 @@ namespace nlsat { reordered = true; } sort_watched_clauses(); - lbool r = search(); + lbool r = search_check(); CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout);); if (reordered) restore_order(); @@ -1929,7 +1987,7 @@ namespace nlsat { for (var x = 0; x < num; x++) { p.push_back(x); } - random_gen r(m_random_seed); + random_gen r(++m_random_seed); shuffle(p.size(), p.c_ptr(), r); reorder(p.size(), p.c_ptr()); } diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index f0a4ceb57..b4f25243a 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -107,7 +107,7 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { simp_p.set_bool("som", true); // expand into sums of monomials return and_then(mk_qfnia_premable(m, p), - or_else(mk_qfnia_sat_solver(m, p), + or_else(// mk_qfnia_sat_solver(m, p), mk_qfnia_nlsat_solver(m, p), and_then(using_params(mk_simplify_tactic(m), simp_p), mk_smt_tactic()))); From 1dac5bd45973c5954f29db23fbb77c429ddf7395 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Dec 2017 17:07:52 -0800 Subject: [PATCH 07/12] remove comment out Signed-off-by: Nikolaj Bjorner --- src/tactic/smtlogics/qfnia_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index b4f25243a..f0a4ceb57 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -107,7 +107,7 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { simp_p.set_bool("som", true); // expand into sums of monomials return and_then(mk_qfnia_premable(m, p), - or_else(// mk_qfnia_sat_solver(m, p), + or_else(mk_qfnia_sat_solver(m, p), mk_qfnia_nlsat_solver(m, p), and_then(using_params(mk_simplify_tactic(m), simp_p), mk_smt_tactic()))); From ab39f06df7833f1f3a47efbac2e7e8db3741c5d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Dec 2017 17:22:49 -0800 Subject: [PATCH 08/12] fix crashes in nlsat Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 9 ++++++--- src/tactic/smtlogics/qfnia_tactic.cpp | 4 ++-- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 0ccaa2f2c..0e3bf8c95 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -734,8 +734,10 @@ namespace nlsat { void undo_set_updt(interval_set * old_set) { SASSERT(m_xk != null_var); var x = m_xk; - m_ism.dec_ref(m_infeasible[x]); - m_infeasible[x] = old_set; + if (x < m_infeasible.size() && m_infeasible[x]) { + m_ism.dec_ref(m_infeasible[x]); + m_infeasible[x] = old_set; + } } void undo_new_stage() { @@ -757,7 +759,8 @@ namespace nlsat { void undo_updt_eq(atom * a) { SASSERT(m_xk != null_var); - m_var2eq[m_xk] = a; + if (m_var2eq.size() > m_xk) + m_var2eq[m_xk] = a; } template diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index f0a4ceb57..3b890b632 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -107,8 +107,8 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { simp_p.set_bool("som", true); // expand into sums of monomials return and_then(mk_qfnia_premable(m, p), - or_else(mk_qfnia_sat_solver(m, p), - mk_qfnia_nlsat_solver(m, p), + or_else(mk_qfnia_nlsat_solver(m, p), + mk_qfnia_sat_solver(m, p), and_then(using_params(mk_simplify_tactic(m), simp_p), mk_smt_tactic()))); } From 1c3d385c253b94b1932adf769a0059d1fad58b65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Dec 2017 17:24:13 -0800 Subject: [PATCH 09/12] fix crashes in nlsat Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 0e3bf8c95..da4f9646d 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -734,7 +734,7 @@ namespace nlsat { void undo_set_updt(interval_set * old_set) { SASSERT(m_xk != null_var); var x = m_xk; - if (x < m_infeasible.size() && m_infeasible[x]) { + if (x < m_infeasible.size()) { m_ism.dec_ref(m_infeasible[x]); m_infeasible[x] = old_set; } From 397cdfc608229a745879aa34ac191b56a79b3c6b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2017 06:38:56 -0800 Subject: [PATCH 10/12] avoid crash on nl Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 6 ++---- src/tactic/portfolio/default_tactic.cpp | 2 +- src/tactic/smtlogics/quant_tactics.cpp | 1 - 3 files changed, 3 insertions(+), 6 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index da4f9646d..8f61fffac 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -732,7 +732,7 @@ namespace nlsat { } void undo_set_updt(interval_set * old_set) { - SASSERT(m_xk != null_var); + if (m_xk == null_var) return; var x = m_xk; if (x < m_infeasible.size()) { m_ism.dec_ref(m_infeasible[x]); @@ -741,8 +741,7 @@ namespace nlsat { } void undo_new_stage() { - SASSERT(m_xk != null_var); - if (m_xk == 0) { + if (m_xk == 0 || m_xk == null_var) { m_xk = null_var; } else { @@ -758,7 +757,6 @@ namespace nlsat { } void undo_updt_eq(atom * a) { - SASSERT(m_xk != null_var); if (m_var2eq.size() > m_xk) m_var2eq[m_xk] = a; } diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 420cb961a..09052869b 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -41,8 +41,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { cond(mk_is_qflra_probe(), mk_qflra_tactic(m), cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m), cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m), - cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_lira_probe(), mk_lira_tactic(m, p), + cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p), //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), mk_smt_tactic()))))))))))), diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 400089a0c..8438d1a32 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -24,7 +24,6 @@ Revision History: #include "qe/qe_tactic.h" #include "qe/qe_lite.h" #include "qe/qsat.h" -#include "qe/nlqsat.h" #include "tactic/core/ctx_simplify_tactic.h" #include "smt/tactic/smt_tactic.h" #include "tactic/core/elim_term_ite_tactic.h" From 21f685fa5a4a6f20e27bb0eb86828c0e553138dc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2017 06:54:02 -0800 Subject: [PATCH 11/12] fix nlsat regression Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 87 +++++++++++++-------------- src/tactic/smtlogics/qfnia_tactic.cpp | 2 +- 2 files changed, 43 insertions(+), 46 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 8f61fffac..c088c406b 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -732,19 +732,19 @@ namespace nlsat { } void undo_set_updt(interval_set * old_set) { - if (m_xk == null_var) return; + if (m_xk == null_var) return; var x = m_xk; - if (x < m_infeasible.size()) { - m_ism.dec_ref(m_infeasible[x]); - m_infeasible[x] = old_set; - } + if (x < m_infeasible.size()) { + m_ism.dec_ref(m_infeasible[x]); + m_infeasible[x] = old_set; + } } void undo_new_stage() { - if (m_xk == 0 || m_xk == null_var) { + if (m_xk == 0) { m_xk = null_var; } - else { + else if (m_xk != null_var) { m_xk--; m_assignment.reset(m_xk); } @@ -757,7 +757,7 @@ namespace nlsat { } void undo_updt_eq(atom * a) { - if (m_var2eq.size() > m_xk) + if (m_var2eq.size() > m_xk) m_var2eq[m_xk] = a; } @@ -1241,50 +1241,47 @@ namespace nlsat { while (true) { r = search(); if (r != l_true) break; - random_gen r(++m_random_seed); - unsigned start = r(num_vars()); - for (var y = 0; y < num_vars(); y++) { - var x = (y + start) % num_vars(); - if (m_is_int[x] && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) { - scoped_anum v(m_am), vlo(m_am), vhi(m_am); - rational lo, hi; - bool is_even = false; - v = m_assignment.value(x); - init_search(); - m_am.int_lt(v, vlo); - m_am.int_gt(v, vhi); - if (!m_am.is_int(vlo)) break; - if (!m_am.is_int(vhi)) break; - m_am.to_rational(vlo, lo); - m_am.to_rational(vhi, hi); + vector lows; + vector vars; + for (var x = 0; x < num_vars(); x++) { + if (m_is_int[x] && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) { + scoped_anum v(m_am), vlo(m_am); + v = m_assignment.value(x); + rational lo; + m_am.int_lt(v, vlo); + if (!m_am.is_int(vlo)) continue; // derive tight bounds. while (true) { lo++; if (!m_am.gt(v, lo.to_mpq())) { lo--; break; } } - while (true) { - hi--; - if (!m_am.lt(v, hi.to_mpq())) { hi++; break; } - } - - polynomial_ref p(m_pm); - rational one(1); - m_lemma.reset(); - p = m_pm.mk_linear(1, &one, &x, -lo); - poly* p1 = p.get(); - m_lemma.push_back(~mk_ineq_literal(atom::GT, 1, &p1, &is_even)); - p = m_pm.mk_linear(1, &one, &x, -hi); - poly* p2 = p.get(); - m_lemma.push_back(~mk_ineq_literal(atom::LT, 1, &p2, &is_even)); + lows.push_back(lo); + vars.push_back(x); + } + } + if (lows.empty()) break; - // perform branch and bound - clause * cls = mk_clause(m_lemma.size(), m_lemma.c_ptr(), false, 0); - if (cls) { - TRACE("nlsat", display(tout << "conflict " << lo << " " << hi, *cls); tout << "\n";); - } - r = l_undef; - break; + init_search(); + for (unsigned i = 0; i < lows.size(); ++i) { + rational lo = lows[i]; + rational hi = lo + rational::one(); + var x = vars[i]; + bool is_even = false; + polynomial_ref p(m_pm); + rational one(1); + m_lemma.reset(); + p = m_pm.mk_linear(1, &one, &x, -lo); + poly* p1 = p.get(); + m_lemma.push_back(~mk_ineq_literal(atom::GT, 1, &p1, &is_even)); + p = m_pm.mk_linear(1, &one, &x, -hi); + poly* p2 = p.get(); + m_lemma.push_back(~mk_ineq_literal(atom::LT, 1, &p2, &is_even)); + + // perform branch and bound + clause * cls = mk_clause(m_lemma.size(), m_lemma.c_ptr(), false, 0); + if (cls) { + TRACE("nlsat", display(tout << "conflict " << lo << " " << hi, *cls); tout << "\n";); } } } diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 3b890b632..5374ba1c1 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -98,7 +98,7 @@ static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) { return and_then(using_params(mk_simplify_tactic(m), simp_p), - try_for(mk_qfnra_nlsat_tactic(m, simp_p), 10000), + try_for(mk_qfnra_nlsat_tactic(m, simp_p), 3000), mk_fail_if_undecided_tactic()); } From c3add4eeda15dd44d8afe7423b0037dec34e9c8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2017 06:56:36 -0800 Subject: [PATCH 12/12] add back missing initialization of lo Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index c088c406b..e1dadf12b 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1251,6 +1251,7 @@ namespace nlsat { rational lo; m_am.int_lt(v, vlo); if (!m_am.is_int(vlo)) continue; + m_am.to_rational(vlo, lo); // derive tight bounds. while (true) { lo++;