From 20bbdfe31a7e8ceb72c49ee5f2dbff112825801f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Mar 2016 15:35:26 -0700 Subject: [PATCH] moving remaining qsat functionality over Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/ast/rewriter/CMakeLists.txt | 1 + contrib/cmake/src/qe/CMakeLists.txt | 8 +- scripts/mk_project.py | 2 +- src/api/c++/z3++.h | 33 +- src/api/python/z3.py | 9 - src/ast/rewriter/label_rewriter.cpp | 53 + src/ast/rewriter/label_rewriter.h | 41 + src/muz/base/dl_rule.cpp | 26 +- src/muz/base/dl_rule.h | 14 +- src/nlsat/nlsat_evaluator.cpp | 30 +- src/nlsat/nlsat_evaluator.h | 4 +- src/nlsat/nlsat_explain.cpp | 530 +++++++- src/nlsat/nlsat_explain.h | 49 +- src/nlsat/nlsat_solver.cpp | 297 ++++- src/nlsat/nlsat_solver.h | 56 +- src/qe/nlqsat.cpp | 921 +++++++++++++ src/qe/nlqsat.h | 38 + src/qe/qe_util.cpp | 26 - src/qe/qe_util.h | 31 - src/qe/qsat.cpp | 1176 +++++++++++++++++ src/qe/qsat.h | 135 ++ src/test/nlsat.cpp | 414 +++++- src/test/qe_arith.cpp | 207 ++- 23 files changed, 3876 insertions(+), 225 deletions(-) create mode 100644 src/ast/rewriter/label_rewriter.cpp create mode 100644 src/ast/rewriter/label_rewriter.h create mode 100644 src/qe/nlqsat.cpp create mode 100644 src/qe/nlqsat.h delete mode 100644 src/qe/qe_util.cpp delete mode 100644 src/qe/qe_util.h create mode 100644 src/qe/qsat.cpp create mode 100644 src/qe/qsat.h diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt index 59834ea13..921cace75 100644 --- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt +++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt @@ -12,6 +12,7 @@ z3_add_component(rewriter expr_safe_replace.cpp factor_rewriter.cpp fpa_rewriter.cpp + label_rewriter.cpp mk_simplified_app.cpp pb_rewriter.cpp quant_hoist.cpp diff --git a/contrib/cmake/src/qe/CMakeLists.txt b/contrib/cmake/src/qe/CMakeLists.txt index b20854de1..b197183dc 100644 --- a/contrib/cmake/src/qe/CMakeLists.txt +++ b/contrib/cmake/src/qe/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(qe SOURCES nlarith_util.cpp + nlqsat.cpp qe_arith.cpp qe_arith_plugin.cpp qe_array_plugin.cpp @@ -16,9 +17,12 @@ z3_add_component(qe qe_mbp.cpp qe_sat_tactic.cpp qe_tactic.cpp - qe_util.cpp + qsat.cpp vsubst_tactic.cpp COMPONENT_DEPENDENCIES + nlsat_tactic + nlqsat sat - smt + smt + tactic ) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 3e476b99e..e7177000f 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -57,7 +57,7 @@ def init_project_def(): add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') - add_lib('qe', ['smt','sat'], 'qe') + add_lib('qe', ['smt','sat','nlsat','tactic','nlsat_tactic'], 'qe') add_lib('duality', ['smt', 'interp', 'qe']) add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base') add_lib('dataflow', ['muz'], 'muz/dataflow') diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 05085a3d7..fad4ca7a2 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -608,12 +608,12 @@ namespace z3 { small integers, 64 bit integers or rational or decimal strings. */ bool is_numeral() const { return kind() == Z3_NUMERAL_AST; } - bool is_numeral_i64(__int64& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); return r;} - bool is_numeral_u64(__uint64& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); return r;} - bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); return r;} - bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); return r;} - bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); return true; } - bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); return true; } + bool is_numeral_i64(__int64& i) const { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;} + bool is_numeral_u64(__uint64& i) const { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;} + bool is_numeral_i(int& i) const { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;} + bool is_numeral_u(unsigned& i) const { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;} + bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; } + bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; } /** \brief Return true if this expression is an application. */ @@ -633,7 +633,7 @@ namespace z3 { /** \brief Return true if expression is an algebraic number. */ - bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_ast); } + bool is_algebraic() const { return 0 != Z3_is_algebraic_number(ctx(), m_ast); } /** \brief Return true if this expression is well sorted (aka type correct). @@ -657,12 +657,11 @@ namespace z3 { \pre is_numeral() */ - int get_numeral_int() const { - assert(is_numeral()); + int get_numeral_int() const { int result; - Z3_bool state = Z3_get_numeral_int(ctx(), m_ast, &result); - if (state != Z3_TRUE) + if (!is_numeral_i(result)) { throw exception("numeral does not fit in machine int"); + } return result; } @@ -675,9 +674,9 @@ namespace z3 { unsigned get_numeral_uint() const { assert(is_numeral()); unsigned result; - Z3_bool state = Z3_get_numeral_uint(ctx(), m_ast, &result); - if (state != Z3_TRUE) + if (!is_numeral_u(result)) { throw exception("numeral does not fit in machine uint"); + } return result; } @@ -690,9 +689,9 @@ namespace z3 { __int64 get_numeral_int64() const { assert(is_numeral()); __int64 result; - Z3_bool state = Z3_get_numeral_int64(ctx(), m_ast, &result); - if (state != Z3_TRUE) + if (!is_numeral_i64(result)) { throw exception("numeral does not fit in machine __int64"); + } return result; } @@ -705,9 +704,9 @@ namespace z3 { __uint64 get_numeral_uint64() const { assert(is_numeral()); __uint64 result; - Z3_bool state = Z3_get_numeral_uint64(ctx(), m_ast, &result); - if (state != Z3_TRUE) + if (!is_numeral_u64(result)) { throw exception("numeral does not fit in machine __uint64"); + } return result; } diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 2cd50c181..211b6777e 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -4162,15 +4162,6 @@ def Select(a, i): _z3_assert(is_array(a), "First argument must be a Z3 array expression") return a[i] -def Default(a): - """ Return a default value for array expression. - >>> b = K(IntSort(), 1) - >>> prove(Default(b) == 1) - proved - """ - if __debug__: - _z3_assert(is_array(a), "First argument must be a Z3 array expression") - return a.mk_default() def Map(f, *args): """Return a Z3 map array expression. diff --git a/src/ast/rewriter/label_rewriter.cpp b/src/ast/rewriter/label_rewriter.cpp new file mode 100644 index 000000000..3017f413c --- /dev/null +++ b/src/ast/rewriter/label_rewriter.cpp @@ -0,0 +1,53 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + label_rewriter.cpp + +Abstract: + + Basic rewriting rules for removing labels. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-19-10 + +Notes: + +--*/ + +#include"rewriter.h" +#include"rewriter_def.h" +#include"label_rewriter.h" + + +label_rewriter::label_rewriter(ast_manager & m) : + m_label_fid(m.get_label_family_id()), + m_rwr(m, false, *this) {} + +label_rewriter::~label_rewriter() {} + +br_status label_rewriter::reduce_app( + func_decl * f, unsigned num, expr * const * args, expr_ref & result, + proof_ref & result_pr) { + if (is_decl_of(f, m_label_fid, OP_LABEL)) { + SASSERT(num == 1); + result = args[0]; + return BR_DONE; + } + return BR_FAILED; +} + +void label_rewriter::remove_labels(expr_ref& fml, proof_ref& pr) { + ast_manager& m = fml.get_manager(); + expr_ref tmp(m); + m_rwr(fml, tmp); + if (pr && fml != tmp) { + pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp)); + } + fml = tmp; +} + + +//template class rewriter_tpl; diff --git a/src/ast/rewriter/label_rewriter.h b/src/ast/rewriter/label_rewriter.h new file mode 100644 index 000000000..6400aa442 --- /dev/null +++ b/src/ast/rewriter/label_rewriter.h @@ -0,0 +1,41 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + label_rewriter.h + +Abstract: + + Basic rewriting rules for labels. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-19-10 + +Notes: + +--*/ +#ifndef LABEL_REWRITER_H_ +#define LABEL_REWRITER_H_ + +#include"ast.h" +#include"rewriter_types.h" + + +class label_rewriter : public default_rewriter_cfg { + family_id m_label_fid; + rewriter_tpl m_rwr; +public: + label_rewriter(ast_manager & m); + ~label_rewriter(); + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, + proof_ref & result_pr); + + + void remove_labels(expr_ref& fml, proof_ref& pr); + +}; + +#endif diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 693391bef..56cc6e154 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -55,8 +55,7 @@ namespace datalog { m_args(m), m_hnf(m), m_qe(m), - m_cfg(m), - m_rwr(m, false, m_cfg), + m_rwr(m), m_ufproc(m) {} void rule_manager::inc_ref(rule * r) { @@ -76,28 +75,8 @@ namespace datalog { } } - rule_manager::remove_label_cfg::~remove_label_cfg() {} - - br_status rule_manager::remove_label_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, - proof_ref & result_pr) - { - if (is_decl_of(f, m_label_fid, OP_LABEL)) { - SASSERT(num == 1); - result = args[0]; - return BR_DONE; - } - return BR_FAILED; - } - - void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) { - expr_ref tmp(m); - m_rwr(fml, tmp); - if (pr && fml != tmp) { - - pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp)); - } - fml = tmp; + m_rwr.remove_labels(fml, pr); } var_idx_set& rule_manager::collect_vars(expr* e) { @@ -1092,5 +1071,4 @@ namespace datalog { }; -template class rewriter_tpl; diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 2261a7a00..f7dc18b5e 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -32,6 +32,7 @@ Revision History: #include"qe_lite.h" #include"var_subst.h" #include"datatype_decl_plugin.h" +#include"label_rewriter.h" namespace datalog { @@ -102,16 +103,6 @@ namespace datalog { */ class rule_manager { - class remove_label_cfg : public default_rewriter_cfg { - family_id m_label_fid; - public: - remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {} - virtual ~remove_label_cfg(); - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, - proof_ref & result_pr); - }; - ast_manager& m; context& m_ctx; rule_counter m_counter; @@ -124,8 +115,7 @@ namespace datalog { svector m_neg; hnf m_hnf; qe_lite m_qe; - remove_label_cfg m_cfg; - rewriter_tpl m_rwr; + label_rewriter m_rwr; mutable uninterpreted_function_finder_proc m_ufproc; mutable quantifier_finder_proc m_qproc; mutable expr_sparse_mark m_visited; diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index 92c5634a1..db18d8854 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -18,10 +18,12 @@ Revision History: --*/ #include"nlsat_evaluator.h" +#include"nlsat_solver.h" namespace nlsat { struct evaluator::imp { + solver& m_solver; assignment const & m_assignment; pmanager & m_pm; small_object_allocator & m_allocator; @@ -357,7 +359,8 @@ namespace nlsat { sign_table m_sign_table_tmp; - imp(assignment const & x2v, pmanager & pm, small_object_allocator & allocator): + imp(solver& s, assignment const & x2v, pmanager & pm, small_object_allocator & allocator): + m_solver(s), m_assignment(x2v), m_pm(pm), m_allocator(allocator), @@ -420,10 +423,25 @@ namespace nlsat { scoped_anum_vector & roots = m_tmp_values; roots.reset(); m_am.isolate_roots(polynomial_ref(a->p(), m_pm), undef_var_assignment(m_assignment, a->x()), roots); + TRACE("nlsat", + m_solver.display(tout << (neg?"!":""), *a); tout << "\n"; + if (roots.empty()) { + tout << "No roots\n"; + } + else { + tout << "Roots for "; + for (unsigned i = 0; i < roots.size(); ++i) { + m_am.display_interval(tout, roots[i]); tout << " "; + } + tout << "\n"; + } + m_assignment.display(tout); + ); SASSERT(a->i() > 0); - if (a->i() > roots.size()) - return false; // p does have sufficient roots - int sign = m_am.compare(m_assignment.value(a->x()), roots[a->i() - 1]); + if (a->i() > roots.size()) { + return neg; + } + int sign = m_am.compare(m_assignment.value(a->x()), roots[a->i() - 1]); return satisfied(sign, k, neg); } @@ -649,8 +667,8 @@ namespace nlsat { } }; - evaluator::evaluator(assignment const & x2v, pmanager & pm, small_object_allocator & allocator) { - m_imp = alloc(imp, x2v, pm, allocator); + evaluator::evaluator(solver& s, assignment const & x2v, pmanager & pm, small_object_allocator & allocator) { + m_imp = alloc(imp, s, x2v, pm, allocator); } evaluator::~evaluator() { diff --git a/src/nlsat/nlsat_evaluator.h b/src/nlsat/nlsat_evaluator.h index 0762c5360..a82ce79fb 100644 --- a/src/nlsat/nlsat_evaluator.h +++ b/src/nlsat/nlsat_evaluator.h @@ -26,11 +26,13 @@ Revision History: namespace nlsat { + class solver; + class evaluator { struct imp; imp * m_imp; public: - evaluator(assignment const & x2v, pmanager & pm, small_object_allocator & allocator); + evaluator(solver& s, assignment const & x2v, pmanager & pm, small_object_allocator & allocator); ~evaluator(); interval_set_manager & ism() const; diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 4b87f9e65..23480eed4 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -36,6 +36,7 @@ namespace nlsat { polynomial::cache & m_cache; pmanager & m_pm; polynomial_ref_vector m_ps; + polynomial_ref_vector m_ps2; polynomial_ref_vector m_psc_tmp; polynomial_ref_vector m_factors; scoped_anum_vector m_roots_tmp; @@ -43,6 +44,7 @@ namespace nlsat { bool m_full_dimensional; bool m_minimize_cores; bool m_factor; + bool m_signed_project; struct todo_set { polynomial::cache & m_cache; @@ -137,6 +139,7 @@ namespace nlsat { m_cache(u), m_pm(u.pm()), m_ps(m_pm), + m_ps2(m_pm), m_psc_tmp(m_pm), m_factors(m_pm), m_roots_tmp(m_am), @@ -148,6 +151,7 @@ namespace nlsat { m_simplify_cores = false; m_full_dimensional = false; m_minimize_cores = false; + m_signed_project = false; } ~imp() { @@ -202,7 +206,7 @@ namespace nlsat { void reset_already_added() { SASSERT(m_result != 0); unsigned sz = m_result->size(); - for (unsigned i = 0; i < sz; i++) + for (unsigned i = 0; i < sz; i++) m_already_added_literal[(*m_result)[i].index()] = false; } @@ -212,7 +216,7 @@ namespace nlsat { max_var(p) must be assigned in the current interpretation. */ int sign(polynomial_ref const & p) { - TRACE("nlsat_explain", tout << "p: " << p << "\n";); + TRACE("nlsat_explain", tout << "p: " << p << " var: " << max_var(p) << "\n";); SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p))); return m_am.eval_sign_at(p, m_assignment); } @@ -697,39 +701,163 @@ namespace nlsat { } } + void test_root_literal(atom::kind k, var y, unsigned i, poly * p, scoped_literal_vector& result) { + m_result = &result; + add_root_literal(k, y, i, p); + reset_already_added(); + m_result = 0; + } + void add_root_literal(atom::kind k, var y, unsigned i, poly * p) { + polynomial_ref pr(p, m_pm); + TRACE("nlsat_explain", + display(tout << "x" << y << " " << k << "[" << i << "](", pr); tout << ")\n";); + + if (!mk_linear_root(k, y, i, p) && + //!mk_plinear_root(k, y, i, p) && + !mk_quadratic_root(k, y, i, p)&& + true) { + bool_var b = m_solver.mk_root_atom(k, y, i, p); + literal l(b, true); + TRACE("nlsat_explain", tout << "adding literal\n"; display(tout, l); tout << "\n";); + add_literal(l); + } + } + + /** + * literal can be expressed using a linear ineq_atom + */ + bool mk_linear_root(atom::kind k, var y, unsigned i, poly * p) { scoped_mpz c(m_pm.m()); - bool_var b; - bool lsign = false; if (m_pm.degree(p, y) == 1 && m_pm.const_coeff(p, y, 1, c)) { SASSERT(!m_pm.m().is_zero(c)); - // literal can be expressed using a linear ineq_atom - polynomial_ref p_prime(m_pm); - p_prime = p; - if (m_pm.m().is_neg(c)) - p_prime = neg(p_prime); - p = p_prime.get(); - switch (k) { - case atom::ROOT_EQ: k = atom::EQ; lsign = false; break; - case atom::ROOT_LT: k = atom::LT; lsign = false; break; - case atom::ROOT_GT: k = atom::GT; lsign = false; break; - case atom::ROOT_LE: k = atom::GT; lsign = true; break; - case atom::ROOT_GE: k = atom::LT; lsign = true; break; - default: - UNREACHABLE(); - break; - } - bool is_even = false; - b = m_solver.mk_ineq_atom(k, 1, &p, &is_even); + mk_linear_root(k, y, i, p, m_pm.m().is_neg(c)); + return true; } - else { - b = m_solver.mk_root_atom(k, y, i, p); - lsign = false; + return false; + } + + + /** + Create pseudo-linear root depending on the sign of the coefficient to y. + */ + bool mk_plinear_root(atom::kind k, var y, unsigned i, poly * p) { + if (m_pm.degree(p, y) != 1) { + return false; } - lsign = !lsign; // adding as an assumption - literal l(b, lsign); - TRACE("nlsat_explain", tout << "adding literal\n"; display(tout, l); tout << "\n";); - add_literal(l); + polynomial_ref c(m_pm); + c = m_pm.coeff(p, y, 1); + int s = sign(c); + if (s == 0) { + return false; + } + ensure_sign(c); + mk_linear_root(k, y, i, p, s < 0); + return true; + } + + /** + Encode root conditions for quadratic polynomials. + + Basically implements Thom's theorem. The roots are characterized by the sign of polynomials and their derivatives. + + b^2 - 4ac = 0: + - there is only one root, which is -b/2a. + - relation to root is a function of the sign of + - 2ax + b + b^2 - 4ac > 0: + - assert i == 1 or i == 2 + - relation to root is a function of the signs of: + - 2ax + b + - ax^2 + bx + c + */ + + bool mk_quadratic_root(atom::kind k, var y, unsigned i, poly * p) { + if (m_pm.degree(p, y) != 2) { + return false; + } + if (i != 1 && i != 2) { + return false; + } + + SASSERT(m_assignment.is_assigned(y)); + polynomial_ref A(m_pm), B(m_pm), C(m_pm), q(m_pm), p_diff(m_pm), yy(m_pm); + A = m_pm.coeff(p, y, 2); + B = m_pm.coeff(p, y, 1); + C = m_pm.coeff(p, y, 0); + // TBD throttle based on degree of q? + q = (B*B) - (4*A*C); + yy = m_pm.mk_polynomial(y); + p_diff = 2*A*yy + B; + p_diff = m_pm.normalize(p_diff); + int sq = ensure_sign(q); + if (sq < 0) { + return false; + } + int sa = ensure_sign(A); + if (sa == 0) { + q = B*yy + C; + return mk_plinear_root(k, y, i, q); + } + ensure_sign(p_diff); + if (sq > 0) { + polynomial_ref pr(p, m_pm); + ensure_sign(pr); + } + return true; + } + + int ensure_sign(polynomial_ref & p) { +#if 0 + polynomial_ref f(m_pm); + factor(p, m_factors); + m_is_even.reset(); + unsigned num_factors = m_factors.size(); + int s = 1; + for (unsigned i = 0; i < num_factors; i++) { + f = m_factors.get(i); + s *= sign(f); + m_is_even.push_back(false); + } + if (num_factors > 0) { + atom::kind k = atom::EQ; + if (s == 0) k = atom::EQ; + if (s < 0) k = atom::LT; + if (s > 0) k = atom::GT; + bool_var b = m_solver.mk_ineq_atom(k, num_factors, m_factors.c_ptr(), m_is_even.c_ptr()); + add_literal(literal(b, true)); + } + return s; +#else + int s = sign(p); + if (!is_const(p)) { + add_simple_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p); + } + return s; +#endif + } + + /** + Auxiliary function to linear roots. + */ + void mk_linear_root(atom::kind k, var y, unsigned i, poly * p, bool mk_neg) { + polynomial_ref p_prime(m_pm); + p_prime = p; + bool lsign = false; + if (mk_neg) + p_prime = neg(p_prime); + p = p_prime.get(); + switch (k) { + case atom::ROOT_EQ: k = atom::EQ; lsign = false; break; + case atom::ROOT_LT: k = atom::LT; lsign = false; break; + case atom::ROOT_GT: k = atom::GT; lsign = false; break; + case atom::ROOT_LE: k = atom::GT; lsign = true; break; + case atom::ROOT_GE: k = atom::LT; lsign = true; break; + default: + UNREACHABLE(); + break; + } + add_simple_assumption(k, p, lsign); } /** @@ -1332,10 +1460,333 @@ namespace nlsat { TRACE("nlsat_explain", tout << "[explain] result\n"; display(tout, result);); CASSERT("nlsat", check_already_added()); } + + + void project(var x, unsigned num, literal const * ls, scoped_literal_vector & result) { + m_result = &result; + svector lits; + TRACE("nlsat", tout << "project x" << x << "\n"; m_solver.display(tout);); + + DEBUG_CODE( + for (unsigned i = 0; i < num; ++i) { + SASSERT(m_solver.value(ls[i]) == l_true); + atom* a = m_atoms[ls[i].var()]; + SASSERT(!a || m_evaluator.eval(a, ls[i].sign())); + }); + split_literals(x, num, ls, lits); + collect_polys(lits.size(), lits.c_ptr(), m_ps); + var mx_var = max_var(m_ps); + if (!m_ps.empty()) { + svector renaming; + if (x != mx_var) { + for (var i = 0; i < m_solver.num_vars(); ++i) { + renaming.push_back(i); + } + std::swap(renaming[x], renaming[mx_var]); + m_solver.reorder(renaming.size(), renaming.c_ptr()); + TRACE("qe", tout << "x: " << x << " max: " << mx_var << " num_vars: " << m_solver.num_vars() << "\n"; + m_solver.display(tout);); + } + elim_vanishing(m_ps); + if (m_signed_project) { + signed_project(m_ps, mx_var); + } + else { + project(m_ps, mx_var); + } + reset_already_added(); + m_result = 0; + if (x != mx_var) { + m_solver.restore_order(); + } + } + else { + reset_already_added(); + m_result = 0; + } + for (unsigned i = 0; i < result.size(); ++i) { + result.set(i, ~result[i]); + } + DEBUG_CODE( + for (unsigned i = 0; i < result.size(); ++i) { + SASSERT(l_true == m_solver.value(result[i])); + }); + + } + + void split_literals(var x, unsigned n, literal const* ls, svector& lits) { + var_vector vs; + for (unsigned i = 0; i < n; ++i) { + vs.reset(); + m_solver.vars(ls[i], vs); + if (vs.contains(x)) { + lits.push_back(ls[i]); + } + else { + add_literal(~ls[i]); + } + } + } + + /** + Signed projection. + + Assumptions: + - any variable in ps is at most x. + - root expressions are satisfied (positive literals) + + Effect: + - if x not in p, then + - if sign(p) < 0: p < 0 + - if sign(p) = 0: p = 0 + - if sign(p) > 0: p > 0 + else: + - let roots_j be the roots of p_j or roots_j[i] + - let L = { roots_j[i] | M(roots_j[i]) < M(x) } + - let U = { roots_j[i] | M(roots_j[i]) > M(x) } + - let E = { roots_j[i] | M(roots_j[i]) = M(x) } + - let glb in L, s.t. forall l in L . M(glb) >= M(l) + - let lub in U, s.t. forall u in U . M(lub) <= M(u) + - if root in E, then + - add E x . x = root & x > lb for lb in L + - add E x . x = root & x < ub for ub in U + - add E x . x = root & x = root2 for root2 in E \ { root } + - else + - assume |L| <= |U| (other case is symmetric) + - add E x . lb <= x & x <= glb for lb in L + - add E x . x = glb & x < ub for ub in U + */ + + + void signed_project(polynomial_ref_vector& ps, var x) { + + TRACE("nlsat_explain", tout << "Signed projection\n";); + polynomial_ref p(m_pm); + unsigned eq_index = 0; + bool eq_valid = false; + unsigned eq_degree = 0; + for (unsigned i = 0; i < ps.size(); ++i) { + p = ps.get(i); + int s = sign(p); + if (max_var(p) != x) { + atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT)); + add_simple_assumption(k, p, false); + ps[i] = ps.back(); + ps.pop_back(); + --i; + } + else if (s == 0) { + if (!eq_valid || degree(p, x) < eq_degree) { + eq_index = i; + eq_valid = true; + eq_degree = degree(p, x); + } + } + } + + if (ps.empty()) { + return; + } + + if (ps.size() == 1) { + project_single(x, ps.get(0)); + return; + } + + // ax + b = 0, p(x) > 0 -> + + if (eq_valid) { + p = ps.get(eq_index); + if (degree(p, x) == 1) { + // ax + b = 0 + // let d be maximal degree of x in p. + // p(x) -> a^d*p(-b/a), a + // perform virtual substitution with equality. + solve_eq(x, eq_index, ps); + } + else { + project_pairs(x, eq_index, ps); + } + return; + } + + unsigned num_lub = 0, num_glb = 0; + unsigned glb_index = 0, lub_index = 0; + scoped_anum lub(m_am), glb(m_am), x_val(m_am); + x_val = m_assignment.value(x); + for (unsigned i = 0; i < ps.size(); ++i) { + p = ps.get(i); + scoped_anum_vector & roots = m_roots_tmp; + roots.reset(); + m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); + bool glb_valid = false, lub_valid = false; + for (unsigned j = 0; j < roots.size(); ++j) { + int s = m_am.compare(x_val, roots[j]); + SASSERT(s != 0); + lub_valid |= s < 0; + glb_valid |= s > 0; + + if (s < 0 && m_am.lt(roots[j], lub)) { + lub_index = i; + m_am.set(lub, roots[j]); + } + + if (s > 0 && m_am.lt(glb, roots[j])) { + glb_index = i; + m_am.set(glb, roots[j]); + } + } + if (glb_valid) { + ++num_glb; + } + if (lub_valid) { + ++num_lub; + } + } + + if (num_lub == 0) { + project_plus_infinity(x, ps); + return; + } + + if (num_glb == 0) { + project_minus_infinity(x, ps); + return; + } + + if (num_lub <= num_glb) { + glb_index = lub_index; + } + + project_pairs(x, glb_index, ps); + } + + void project_plus_infinity(var x, polynomial_ref_vector const& ps) { + polynomial_ref p(m_pm), lc(m_pm); + for (unsigned i = 0; i < ps.size(); ++i) { + p = ps.get(i); + unsigned d = degree(p, x); + lc = m_pm.coeff(p, x, d); + if (!is_const(lc)) { + unsigned s = sign(p); + SASSERT(s != 0); + atom::kind k = (s > 0)?(atom::GT):(atom::LT); + add_simple_assumption(k, lc); + } + } + } + + void project_minus_infinity(var x, polynomial_ref_vector const& ps) { + polynomial_ref p(m_pm), lc(m_pm); + for (unsigned i = 0; i < ps.size(); ++i) { + p = ps.get(i); + unsigned d = degree(p, x); + lc = m_pm.coeff(p, x, d); + if (!is_const(lc)) { + unsigned s = sign(p); + SASSERT(s != 0); + atom::kind k; + if (s > 0) { + k = (d % 2 == 0)?(atom::GT):(atom::LT); + } + else { + k = (d % 2 == 0)?(atom::LT):(atom::GT); + } + add_simple_assumption(k, lc); + } + } + } + + void project_pairs(var x, unsigned idx, polynomial_ref_vector const& ps) { + polynomial_ref p(m_pm); + p = ps.get(idx); + for (unsigned i = 0; i < ps.size(); ++i) { + if (i != idx) { + project_pair(x, ps.get(i), p); + } + } + } + + void project_pair(var x, polynomial::polynomial* p1, polynomial::polynomial* p2) { + m_ps2.reset(); + m_ps2.push_back(p1); + m_ps2.push_back(p2); + project(m_ps2, x); + } + + void project_single(var x, polynomial::polynomial* p) { + m_ps2.reset(); + m_ps2.push_back(p); + project(m_ps2, x); + } + + void solve_eq(var x, unsigned idx, polynomial_ref_vector const& ps) { + polynomial_ref p(m_pm), A(m_pm), B(m_pm), C(m_pm), D(m_pm), E(m_pm), q(m_pm), r(m_pm); + polynomial_ref_vector qs(m_pm); + p = ps.get(idx); + SASSERT(degree(p, x) == 1); + A = m_pm.coeff(p, x, 1); + B = m_pm.coeff(p, x, 0); + B = neg(B); + TRACE("nlsat_explain", tout << "p: " << p << " A: " << A << " B: " << B << "\n";); + // x = B/A + for (unsigned i = 0; i < ps.size(); ++i) { + if (i != idx) { + q = ps.get(i); + unsigned d = degree(q, x); + D = m_pm.mk_const(rational(1)); + E = D; + r = m_pm.mk_zero(); + for (unsigned j = 0; j <= d; ++j) { + qs.push_back(D); + D = D*A; + } + for (unsigned j = 0; j <= d; ++j) { + // A^d*p0 + A^{d-1}*B*p1 + ... + B^j*A^{d-j}*pj + ... + B^d*p_d + C = m_pm.coeff(q, x, j); + if (!is_zero(C)) { + D = qs.get(d-j); + r = r + D*E*C; + } + E = E*B; + } + TRACE("nlsat_explain", tout << "q: " << q << " r: " << r << "\n";); + ensure_sign(r); + } + else { + ensure_sign(A); + } + } + + } + + void maximize(var x, unsigned num, literal const * ls, scoped_anum& val, bool& unbounded) { + svector lits; + polynomial_ref p(m_pm); + split_literals(x, num, ls, lits); + collect_polys(lits.size(), lits.c_ptr(), m_ps); + unbounded = true; + scoped_anum x_val(m_am); + x_val = m_assignment.value(x); + for (unsigned i = 0; i < m_ps.size(); ++i) { + p = m_ps.get(i); + scoped_anum_vector & roots = m_roots_tmp; + roots.reset(); + m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); + for (unsigned j = 0; j < roots.size(); ++j) { + int s = m_am.compare(x_val, roots[j]); + if (s <= 0 && (unbounded || m_am.compare(roots[j], val) <= 0)) { + unbounded = false; + val = roots[j]; + } + } + } + } + }; - explain::explain(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq, - evaluator & ev) { + explain::explain(solver & s, assignment const & x2v, polynomial::cache & u, + atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev) { m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev); } @@ -1364,10 +1815,26 @@ namespace nlsat { m_imp->m_factor = f; } + void explain::set_signed_project(bool f) { + m_imp->m_signed_project = f; + } + void explain::operator()(unsigned n, literal const * ls, scoped_literal_vector & result) { (*m_imp)(n, ls, result); } + void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) { + m_imp->project(x, n, ls, result); + } + + void explain::maximize(var x, unsigned n, literal const * ls, scoped_anum& val, bool& unbounded) { + m_imp->maximize(x, n, ls, val, unbounded); + } + + void explain::test_root_literal(atom::kind k, var y, unsigned i, poly* p, scoped_literal_vector & result) { + m_imp->test_root_literal(k, y, i, p, result); + } + }; #ifdef Z3DEBUG @@ -1398,3 +1865,4 @@ void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) { std::cout << std::endl; } #endif + diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index ac99b434c..4309a0090 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -22,9 +22,11 @@ Revision History: #include"nlsat_solver.h" #include"nlsat_scoped_literal_vector.h" #include"polynomial_cache.h" +#include"algebraic_numbers.h" namespace nlsat { class evaluator; + class explain { public: @@ -32,8 +34,8 @@ namespace nlsat { private: imp * m_imp; public: - explain(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq, - evaluator & ev); + explain(solver & s, assignment const & x2v, polynomial::cache & u, + atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev); ~explain(); void reset(); @@ -41,6 +43,7 @@ namespace nlsat { void set_full_dimensional(bool f); void set_minimize_cores(bool f); void set_factor(bool f); + void set_signed_project(bool f); /** \brief Given a set of literals ls[0], ... ls[n-1] s.t. @@ -60,6 +63,48 @@ namespace nlsat { - s_1, ..., s_m are false in the current interpretation */ void operator()(unsigned n, literal const * ls, scoped_literal_vector & result); + + + /** + \brief projection for a given variable. + + Given: M |= l1[x] /\ ... /\ ln[x] + + Find: M |= s1, ..., sm + + Such that: |= ~s1 \/ ... \/ ~sm \/ E x. l1[x] /\ ... /\ ln[x] + + Contrast this with with the core-based projection above: + + Given: M |= A x . l1[x] \/ ... \/ ln[x] + + Find: M |= ~s1, ..., ~sm. + + Such that: |= s1 \/ ... \/ sm \/ A x . l1[x] \/ ... \/ ln[x] + + Claim: the two compute the same solutions if the projection operators are independent of the value of x. + Claim: A complete, convergent projection operator can be obtained from M in a way that is independent of x. + + + */ + void project(var x, unsigned n, literal const * ls, scoped_literal_vector & result); + + /** + Maximize the value of x (locally) under the current assignment to other variables and + while maintaining the assignment to the literals ls. + Set unbounded to 'true' if the value of x is unbounded. + + Precondition: the set of literals are true in the current model. + + By local optimization we understand that x is increased to the largest value within + the signs delineated by the roots of the polynomials in ls. + */ + void maximize(var x, unsigned n, literal const * ls, scoped_anum& val, bool& unbounded); + + /** + Unit test routine. + */ + void test_root_literal(atom::kind k, var y, unsigned i, poly* p, scoped_literal_vector & result); }; }; diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index c723d9961..40177bb08 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -66,7 +66,6 @@ namespace nlsat { typedef polynomial::cache cache; typedef ptr_vector interval_set_vector; - solver & m_solver; reslimit& m_rlimit; small_object_allocator m_allocator; unsynch_mpq_manager m_qm; @@ -159,8 +158,7 @@ namespace nlsat { unsigned m_stages; unsigned m_irrational_assignments; // number of irrational witnesses - imp(solver & s, reslimit& rlim, params_ref const & p): - m_solver(s), + imp(solver& s, reslimit& rlim, params_ref const & p): m_rlimit(rlim), m_allocator("nlsat"), m_pm(rlim, m_qm, &m_allocator), @@ -168,7 +166,7 @@ namespace nlsat { m_am(rlim, m_qm, p, &m_allocator), m_asm(*this, m_allocator), m_assignment(m_am), - m_evaluator(m_assignment, m_pm, m_allocator), + m_evaluator(s, m_assignment, m_pm, m_allocator), m_ism(m_evaluator.ism()), m_num_bool_vars(0), m_display_var(m_perm), @@ -183,12 +181,7 @@ namespace nlsat { } ~imp() { - m_explain.reset(); - m_lemma.reset(); - m_lazy_clause.reset(); - undo_until_size(0); - del_clauses(); - del_unref_atoms(); + reset(); } void mk_true_bvar() { @@ -216,6 +209,18 @@ namespace nlsat { m_am.updt_params(p.p); } + void reset() { + m_explain.reset(); + m_lemma.reset(); + m_lazy_clause.reset(); + undo_until_size(0); + del_clauses(); + del_unref_atoms(); + m_cache.reset(); + m_assignment.reset(); + } + + void checkpoint() { if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg()); if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); @@ -252,6 +257,7 @@ namespace nlsat { } void inc_ref(bool_var b) { + TRACE("ref", tout << "inc: " << b << "\n";); if (b == null_bool_var) return; if (m_atoms[b] == 0) @@ -264,6 +270,7 @@ namespace nlsat { } void dec_ref(bool_var b) { + TRACE("ref", tout << "dec: " << b << "\n";); if (b == null_bool_var) return; atom * a = m_atoms[b]; @@ -412,6 +419,34 @@ namespace nlsat { return x; } + svector m_found_vars; + void vars(literal l, var_vector& vs) { + vs.reset(); + atom * a = m_atoms[l.var()]; + if (a == 0) { + + } + else if (a->is_ineq_atom()) { + unsigned sz = to_ineq_atom(a)->size(); + var_vector new_vs; + for (unsigned j = 0; j < sz; j++) { + m_found_vars.reset(); + m_pm.vars(to_ineq_atom(a)->p(j), new_vs); + for (unsigned i = 0; i < new_vs.size(); ++i) { + if (!m_found_vars.get(new_vs[i], false)) { + m_found_vars.setx(new_vs[i], true, false); + vs.push_back(new_vs[i]); + } + } + } + } + else { + m_pm.vars(to_root_atom(a)->p(), vs); + //vs.erase(max_var(to_root_atom(a)->p())); + vs.push_back(to_root_atom(a)->x()); + } + } + void deallocate(ineq_atom * a) { unsigned obj_sz = ineq_atom::get_obj_size(a->size()); a->~ineq_atom(); @@ -491,6 +526,7 @@ namespace nlsat { TRACE("nlsat_table_bug", ineq_atom::hash_proc h; tout << "mk_ineq_atom hash: " << h(new_atom) << "\n"; display(tout, *new_atom, m_display_var); tout << "\n";); ineq_atom * old_atom = m_ineq_atoms.insert_if_not_there(new_atom); + CTRACE("nlsat_table_bug", old_atom->max_var() != max, display(tout, *old_atom, m_display_var); tout << "\n";); SASSERT(old_atom->max_var() == max); if (old_atom != new_atom) { deallocate(new_atom); @@ -726,7 +762,7 @@ namespace nlsat { template void undo_until(Predicate const & pred) { - while (pred()) { + while (pred() && !m_trail.empty()) { trail & t = m_trail.back(); switch (t.m_kind) { case trail::BVAR_ASSIGNMENT: @@ -803,6 +839,14 @@ namespace nlsat { SASSERT(m_bvalues[b] == l_undef); } + struct true_pred { + bool operator()() const { return true; } + }; + + void undo_until_empty() { + undo_until(true_pred()); + } + /** \brief Create a new scope level */ @@ -868,10 +912,11 @@ namespace nlsat { var max = a->max_var(); if (!m_assignment.is_assigned(max)) return l_undef; - TRACE("value_bug", tout << "value of: "; display(tout, l); tout << "\n"; tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n"; - display_assignment(tout); - display_bool_assignment(tout);); - return to_lbool(m_evaluator.eval(a, l.sign())); + 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"; + display_assignment(tout);); + return val; } /** @@ -880,8 +925,10 @@ namespace nlsat { bool is_satisfied(clause const & cls) const { unsigned sz = cls.size(); for (unsigned i = 0; i < sz; i++) { - if (const_cast(this)->value(cls[i]) == l_true) + if (const_cast(this)->value(cls[i]) == l_true) { + TRACE("value_bug:", tout << cls[i] << " := true\n";); return true; + } } return false; } @@ -984,8 +1031,10 @@ namespace nlsat { If satisfy_learned is true, then learned clauses are satisfied even if m_lazy > 0 */ bool process_arith_clause(clause const & cls, bool satisfy_learned) { - if (!satisfy_learned && m_lazy >= 2 && cls.is_learned()) + if (!satisfy_learned && m_lazy >= 2 && cls.is_learned()) { + TRACE("nlsat", tout << "skip learned\n";); return true; // ignore lemmas in super lazy mode + } SASSERT(m_xk == max_var(cls)); unsigned num_undef = 0; // number of undefined literals unsigned first_undef = UINT_MAX; // position of the first undefined literal @@ -1064,7 +1113,7 @@ namespace nlsat { If satisfy_learned is true, then (arithmetic) learned clauses are satisfied even if m_lazy > 0 */ bool process_clause(clause const & cls, bool satisfy_learned) { - TRACE("nlsat", tout << "processing clause:\n"; display(tout, cls); tout << "\n";); + TRACE("nlsat", tout << "processing clause: "; display(tout, cls); tout << "\n";); if (is_satisfied(cls)) return true; if (m_xk == null_var) @@ -1151,7 +1200,7 @@ namespace nlsat { } TRACE("nlsat_bug", tout << "xk: x" << m_xk << " bk: b" << m_bk << "\n";); if (m_bk == null_bool_var && m_xk >= num_vars()) { - TRACE("nlsat", tout << "found model\n"; display_assignment(tout); display_bool_assignment(tout);); + TRACE("nlsat", tout << "found model\n"; display_assignment(tout);); return l_true; // all variables were assigned, and all clauses were satisfied. } TRACE("nlsat", tout << "processing variable "; @@ -1186,23 +1235,102 @@ namespace nlsat { lbool check() { TRACE("nlsat_smt2", display_smt2(tout);); TRACE("nlsat_fd", tout << "is_full_dimensional: " << is_full_dimensional() << "\n";); - m_xk = null_var; + init_search(); m_explain.set_full_dimensional(is_full_dimensional()); - if (m_random_order) { + bool reordered = false; + if (!can_reorder()) { + + } + else if (m_random_order) { shuffle_vars(); + reordered = true; } else if (m_reorder) { heuristic_reorder(); + reordered = true; } sort_watched_clauses(); lbool r = search(); - CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout); display_bool_assignment(tout);); - if (m_reorder) + CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout);); + if (reordered) restore_order(); - CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout); display_bool_assignment(tout);); + CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout);); + CTRACE("nlsat", r == l_false, display(tout);); return r; } + void init_search() { + undo_until_empty(); + while (m_scope_lvl > 0) { + undo_new_level(); + } + m_xk = null_var; + for (unsigned i = 0; i < m_bvalues.size(); ++i) { + m_bvalues[i] = l_undef; + } + m_assignment.reset(); + } + + lbool check(literal_vector& assumptions) { + literal_vector result; + unsigned sz = assumptions.size(); + literal const* ptr = assumptions.c_ptr(); + for (unsigned i = 0; i < sz; ++i) { + mk_clause(1, ptr+i, (assumption)(ptr+i)); + } + lbool r = check(); + + if (r == l_false) { + // collect used literals from m_lemma_assumptions + vector deps; + m_asm.linearize(m_lemma_assumptions.get(), deps); + for (unsigned i = 0; i < deps.size(); ++i) { + literal const* lp = (literal const*)(deps[i]); + if (ptr <= lp && lp < ptr + sz) { + result.push_back(*lp); + } + } + } + collect(assumptions, m_clauses); + collect(assumptions, m_learned); + + assumptions.reset(); + assumptions.append(result); + return r; + } + + void collect(literal_vector const& assumptions, clause_vector& clauses) { + unsigned n = clauses.size(); + unsigned j = 0; + for (unsigned i = 0; i < n; i++) { + clause * c = clauses[i]; + if (collect(assumptions, *c)) { + del_clause(c); + } + else { + clauses[j] = c; + j++; + } + } + clauses.shrink(j); + } + + bool collect(literal_vector const& assumptions, clause const& c) { + unsigned sz = assumptions.size(); + literal const* ptr = assumptions.c_ptr(); + _assumption_set asms = static_cast<_assumption_set>(c.assumptions()); + if (asms == 0) { + return false; + } + vector deps; + m_asm.linearize(asms, deps); + bool found = false; + for (unsigned i = 0; !found && i < deps.size(); ++i) { + found = ptr <= deps[i] && deps[i] < ptr + sz; + } + return found; + } + // ----------------------- // // Conflict Resolution @@ -1447,7 +1575,7 @@ namespace nlsat { TRACE("nlsat", tout << "resolve, conflicting clause:\n"; display(tout, *conflict_clause); tout << "\n"; tout << "xk: "; if (m_xk != null_var) m_display_var(tout, m_xk); else tout << ""; tout << "\n"; tout << "scope_lvl: " << scope_lvl() << "\n"; - tout << "current assignment\n"; display_assignment(tout); display_bool_assignment(tout);); + tout << "current assignment\n"; display_assignment(tout);); // static unsigned counter = 0; // counter++; @@ -1588,7 +1716,7 @@ namespace nlsat { conflict_clause = new_cls; goto start; } - TRACE("nlsat_resolve_done", display_assignment(tout); display_bool_assignment(tout);); + TRACE("nlsat_resolve_done", display_assignment(tout);); return true; } @@ -1801,6 +1929,15 @@ namespace nlsat { reorder(p.size(), p.c_ptr()); } + bool can_reorder() const { + for (unsigned i = 0; i < m_atoms.size(); ++i) { + if (m_atoms[i]) { + if (m_atoms[i]->is_root_atom()) return false; + } + } + return true; + } + /** \brief Reorder variables using the giving permutation. p maps internal variables to their new positions @@ -1921,6 +2058,9 @@ namespace nlsat { void reinit_cache() { reinit_cache(m_clauses); reinit_cache(m_learned); + for (unsigned i = 0; i < m_atoms.size(); ++i) { + reinit_cache(m_atoms[i]); + } } void reinit_cache(clause_vector const & cs) { unsigned sz = cs.size(); @@ -1934,10 +2074,13 @@ namespace nlsat { } void reinit_cache(literal l) { bool_var b = l.var(); - atom * a = m_atoms[b]; - if (a == 0) - return; - if (a->is_ineq_atom()) { + reinit_cache(m_atoms[b]); + } + void reinit_cache(atom* a) { + if (a == 0) { + + } + else if (a->is_ineq_atom()) { var max = 0; unsigned sz = to_ineq_atom(a)->size(); for (unsigned i = 0; i < sz; i++) { @@ -2073,7 +2216,7 @@ namespace nlsat { // // ----------------------- - void display_assignment(std::ostream & out, display_var_proc const & proc) const { + void display_num_assignment(std::ostream & out, display_var_proc const & proc) const { for (var x = 0; x < num_vars(); x++) { if (m_assignment.is_assigned(x)) { proc(out, x); @@ -2084,7 +2227,7 @@ namespace nlsat { } } - void display_bool_assignment(std::ostream & out, display_var_proc const & proc) const { + void display_bool_assignment(std::ostream & out) const { unsigned sz = m_atoms.size(); for (bool_var b = 0; b < sz; b++) { if (m_atoms[b] == 0 && m_bvalues[b] != l_undef) { @@ -2112,12 +2255,13 @@ namespace nlsat { return !first; } - void display_assignment(std::ostream & out) const { - display_assignment(out, m_display_var); + void display_num_assignment(std::ostream & out) const { + display_num_assignment(out, m_display_var); } - void display_bool_assignment(std::ostream & out) const { - display_bool_assignment(out, m_display_var); + void display_assignment(std::ostream& out) const { + display_bool_assignment(out); + display_num_assignment(out); } void display(std::ostream & out, ineq_atom const & a, display_var_proc const & proc, bool use_star = false) const { @@ -2511,6 +2655,7 @@ namespace nlsat { void display(std::ostream & out) const { display(out, m_display_var); + display_assignment(out); } void display_vars(std::ostream & out) const { @@ -2562,6 +2707,20 @@ namespace nlsat { return m_imp->check(); } + lbool solver::check(literal_vector& assumptions) { + return m_imp->check(assumptions); + } + + void solver::reset() { + m_imp->reset(); + } + + + void solver::updt_params(params_ref const & p) { + m_imp->updt_params(p); + } + + void solver::collect_param_descrs(param_descrs & d) { algebraic_numbers::manager::collect_param_descrs(d); nlsat_params::collect_param_descrs(d); @@ -2583,6 +2742,10 @@ namespace nlsat { m_imp->m_display_var.m_proc = &proc; } + unsigned solver::num_vars() const { + return m_imp->num_vars(); + } + bool solver::is_int(var x) const { return m_imp->is_int(x); } @@ -2590,10 +2753,61 @@ namespace nlsat { bool_var solver::mk_bool_var() { return m_imp->mk_bool_var(); } + + literal solver::mk_true() { + return literal(0, false); + } atom * solver::bool_var2atom(bool_var b) { return m_imp->m_atoms[b]; } + + void solver::vars(literal l, var_vector& vs) { + m_imp->vars(l, vs); + } + + atom_vector const& solver::get_atoms() { + return m_imp->m_atoms; + } + + atom_vector const& solver::get_var2eq() { + return m_imp->m_var2eq; + } + + evaluator& solver::get_evaluator() { + return m_imp->m_evaluator; + } + + explain& solver::get_explain() { + return m_imp->m_explain; + } + + void solver::reorder(unsigned sz, var const* p) { + m_imp->reorder(sz, p); + } + + void solver::restore_order() { + m_imp->restore_order(); + } + + void solver::set_rvalues(assignment const& as) { + m_imp->m_assignment.copy(as); + } + + void solver::get_rvalues(assignment& as) { + as.copy(m_imp->m_assignment); + } + + void solver::get_bvalues(svector& vs) { + vs.reset(); + vs.append(m_imp->m_bvalues); + } + + void solver::set_bvalues(svector const& vs) { + m_imp->m_bvalues.reset(); + m_imp->m_bvalues.append(vs); + m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef); + } var solver::mk_var(bool is_int) { return m_imp->mk_var(is_int); @@ -2631,10 +2845,21 @@ namespace nlsat { m_imp->display(out, l); } + void solver::display(std::ostream & out, unsigned n, literal const* ls) const { + for (unsigned i = 0; i < n; ++i) { + display(out, ls[i]); + out << "; "; + } + } + void solver::display(std::ostream & out, var x) const { m_imp->m_display_var(out, x); } + void solver::display(std::ostream & out, atom const& a) const { + m_imp->display(out, a, m_imp->m_display_var); + } + display_var_proc const & solver::display_proc() const { return m_imp->m_display_var; } diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 2875bbc8c..eec5ba19f 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -28,6 +28,9 @@ Revision History: namespace nlsat { + class evaluator; + class explain; + class solver { struct imp; imp * m_imp; @@ -63,7 +66,9 @@ namespace nlsat { nonlinear arithmetic atom. */ bool_var mk_bool_var(); - + + literal mk_true(); + /** \brief Create a real/integer variable. */ @@ -121,6 +126,48 @@ namespace nlsat { */ atom * bool_var2atom(bool_var b); + /** + \brief extract free variables from literal. + */ + void vars(literal l, var_vector& vs); + + /** + \brief provide access to atoms. Used by explain. + */ + atom_vector const& get_atoms(); + + /** + \brief Access var -> asserted equality. + */ + + atom_vector const& get_var2eq(); + + /** + \brief expose evaluator. + */ + + evaluator& get_evaluator(); + + /** + \brief Access explanation module. + */ + explain& get_explain(); + + /** + \brief Access assignments to variables. + */ + void get_rvalues(assignment& as); + void set_rvalues(assignment const& as); + + void get_bvalues(svector& vs); + void set_bvalues(svector const& vs); + + /** + \brief reorder variables. + */ + void reorder(unsigned sz, var const* permutation); + void restore_order(); + /** \brief Return number of integer/real variables */ @@ -135,6 +182,8 @@ namespace nlsat { // ----------------------- lbool check(); + lbool check(literal_vector& assumptions); + // ----------------------- // // Model @@ -154,6 +203,7 @@ namespace nlsat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); + void reset(); void collect_statistics(statistics & st); void reset_statistics(); void display_status(std::ostream & out) const; @@ -174,6 +224,10 @@ namespace nlsat { */ void display(std::ostream & out, literal l) const; + void display(std::ostream & out, unsigned n, literal const* ls) const; + + void display(std::ostream & out, atom const& a) const; + /** \brief Display variable */ diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp new file mode 100644 index 000000000..7318ba06a --- /dev/null +++ b/src/qe/nlqsat.cpp @@ -0,0 +1,921 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + nlqsat.cpp + +Abstract: + + Quantifier Satisfiability Solver for nlsat + +Author: + + Nikolaj Bjorner (nbjorner) 2015-10-17 + +Revision History: + + +--*/ + +#include "nlqsat.h" +#include "nlsat_solver.h" +#include "nlsat_explain.h" +#include "nlsat_assignment.h" +#include "qsat.h" +#include "quant_hoist.h" +#include "goal2nlsat.h" +#include "expr2var.h" +#include "uint_set.h" +#include "ast_util.h" +#include "tseitin_cnf_tactic.h" +#include "expr_safe_replace.h" + +namespace qe { + + enum qsat_mode_t { + qsat_t, + elim_t, + interp_t + }; + + class nlqsat : public tactic { + + typedef unsigned_vector assumption_vector; + typedef nlsat::scoped_literal_vector clause; + + struct stats { + unsigned m_num_rounds; + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + }; + + ast_manager& m; + qsat_mode_t m_mode; + params_ref m_params; + nlsat::solver m_solver; + tactic_ref m_nftactic; + nlsat::literal_vector m_asms; + nlsat::literal_vector m_cached_asms; + unsigned_vector m_cached_asms_lim; + nlsat::literal m_is_true; + nlsat::assignment m_rmodel; + svector m_bmodel; + nlsat::assignment m_rmodel0; + svector m_bmodel0; + bool m_valid_model; + vector m_bound_rvars; + vector > m_bound_bvars; + vector m_preds; + svector m_rvar2level; + u_map m_bvar2level; + expr2var m_a2b, m_t2x; + u_map m_b2a, m_x2t; + volatile bool m_cancel; + stats m_stats; + statistics m_st; + obj_hashtable m_free_vars; + expr_ref_vector m_answer; + expr_safe_replace m_answer_simplify; + nlsat::literal_vector m_assumptions; + u_map m_asm2fml; + expr_ref_vector m_trail; + + lbool check_sat() { + while (true) { + ++m_stats.m_num_rounds; + check_cancel(); + init_assumptions(); + lbool res = m_solver.check(m_asms); + switch (res) { + case l_true: + TRACE("qe", display(tout); ); + save_model(); + push(); + break; + case l_false: + if (0 == level()) return l_false; + if (1 == level() && m_mode == qsat_t) return l_true; + project(); + break; + case l_undef: + return res; + } + } + return l_undef; + } + + void init_assumptions() { + unsigned lvl = level(); + m_asms.reset(); + m_asms.push_back(is_exists()?m_is_true:~m_is_true); + m_asms.append(m_assumptions); + TRACE("qe", tout << "model valid: " << m_valid_model << " level: " << lvl << " "; + display_assumptions(tout); + m_solver.display(tout);); + + if (!m_valid_model) { + m_asms.append(m_cached_asms); + return; + } + unsave_model(); + if (lvl == 0) { + SASSERT(m_cached_asms.empty()); + return; + } + if (lvl <= m_preds.size()) { + for (unsigned j = 0; j < m_preds[lvl - 1].size(); ++j) { + add_literal(m_cached_asms, m_preds[lvl - 1][j]); + } + } + m_asms.append(m_cached_asms); + + for (unsigned i = lvl + 1; i < m_preds.size(); i += 2) { + for (unsigned j = 0; j < m_preds[i].size(); ++j) { + nlsat::literal l = m_preds[i][j]; + max_level lv = m_bvar2level.find(l.var()); + bool use = + (lv.m_fa == i && (lv.m_ex == UINT_MAX || lv.m_ex < lvl)) || + (lv.m_ex == i && (lv.m_fa == UINT_MAX || lv.m_fa < lvl)); + if (use) { + add_literal(m_asms, l); + } + } + } + TRACE("qe", display(tout); + for (unsigned i = 0; i < m_asms.size(); ++i) { + m_solver.display(tout, m_asms[i]); tout << "\n"; + }); + save_model(); + } + + void add_literal(nlsat::literal_vector& lits, nlsat::literal l) { + lbool r = m_solver.value(l); + switch (r) { + case l_true: + lits.push_back(l); + break; + case l_false: + lits.push_back(~l); + break; + default: + UNREACHABLE(); + break; + } + } + + template + void insert_set(S& set, T const& vec) { + for (unsigned i = 0; i < vec.size(); ++i) { + set.insert(vec[i]); + } + } + + + void mbp(unsigned level, nlsat::scoped_literal_vector& result) { + nlsat::var_vector vars; + uint_set fvars; + extract_vars(level, vars, fvars); + mbp(vars, fvars, result); + } + + void extract_vars(unsigned level, nlsat::var_vector& vars, uint_set& fvars) { + for (unsigned i = 0; i < m_bound_rvars.size(); ++i) { + if (i < level) { + insert_set(fvars, m_bound_bvars[i]); + } + else { + vars.append(m_bound_rvars[i]); + } + } + } + + void mbp(nlsat::var_vector const& vars, uint_set const& fvars, clause& result) { + // + // Also project auxiliary variables from clausification. + // + unsave_model(); + nlsat::explain& ex = m_solver.get_explain(); + nlsat::scoped_literal_vector new_result(m_solver); + result.reset(); + // project quantified Boolean variables. + for (unsigned i = 0; i < m_asms.size(); ++i) { + nlsat::literal lit = m_asms[i]; + if (!m_b2a.contains(lit.var()) || fvars.contains(lit.var())) { + result.push_back(lit); + } + } + TRACE("qe", m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";); + // project quantified real variables. + // They are sorted by size, so we project the largest variables first to avoid + // renaming variables. + for (unsigned i = vars.size(); i > 0;) { + --i; + new_result.reset(); + ex.project(vars[i], result.size(), result.c_ptr(), new_result); + result.swap(new_result); + TRACE("qe", m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";); + } + negate_clause(result); + } + + void negate_clause(clause& result) { + for (unsigned i = 0; i < result.size(); ++i) { + result.set(i, ~result[i]); + } + } + + void save_model() { + m_solver.get_rvalues(m_rmodel); + m_solver.get_bvalues(m_bmodel); + m_valid_model = true; + if (is_exists(level())) { + m_rmodel0.copy(m_rmodel); + m_bmodel0.reset(); + m_bmodel0.append(m_bmodel); + } + } + + void unsave_model() { + SASSERT(m_valid_model); + m_solver.set_rvalues(m_rmodel); + m_solver.set_bvalues(m_bmodel); + } + + void clear_model() { + m_valid_model = false; + m_rmodel.reset(); + m_bmodel.reset(); + m_solver.set_rvalues(m_rmodel); + } + + unsigned level() const { + return m_cached_asms_lim.size(); + } + + void enforce_parity(clause& cl) { + cl.push_back(is_exists()?~m_is_true:m_is_true); + } + + void add_clause(clause& cl) { + if (cl.empty()) { + cl.push_back(~m_solver.mk_true()); + } + SASSERT(!cl.empty()); + nlsat::literal_vector lits(cl.size(), cl.c_ptr()); + m_solver.mk_clause(lits.size(), lits.c_ptr()); + } + + max_level get_level(clause const& cl) { + return get_level(cl.size(), cl.c_ptr()); + } + + max_level get_level(unsigned n, nlsat::literal const* ls) { + max_level level; + for (unsigned i = 0; i < n; ++i) { + level.merge(get_level(ls[i])); + } + return level; + } + + max_level get_level(nlsat::literal l) { + max_level level; + if (m_bvar2level.find(l.var(), level)) { + return level; + } + nlsat::var_vector vs; + m_solver.vars(l, vs); + for (unsigned i = 0; i < vs.size(); ++i) { + level.merge(m_rvar2level[vs[i]]); + } + set_level(l.var(), level); + return level; + } + + void set_level(nlsat::bool_var v, max_level const& level) { + unsigned k = level.max(); + while (m_preds.size() <= k) { + m_preds.push_back(nlsat::scoped_literal_vector(m_solver)); + } + nlsat::literal l(v, false); + m_preds[k].push_back(l); + m_bvar2level.insert(v, level); + TRACE("qe", m_solver.display(tout, l); tout << ": " << level << "\n";); + } + + void project() { + TRACE("qe", display_assumptions(tout);); + if (!m_valid_model) { + pop(1); + return; + } + if (m_mode == elim_t) { + project_qe(); + return; + } + SASSERT(level() >= 2); + unsigned num_scopes; + clause cl(m_solver); + mbp(level()-1, cl); + + max_level clevel = get_level(cl); + enforce_parity(cl); + add_clause(cl); + + if (clevel.max() == UINT_MAX) { + num_scopes = 2*(level()/2); + } + else { + SASSERT(clevel.max() + 2 <= level()); + num_scopes = level() - clevel.max(); + if ((num_scopes % 2) != 0) { + --num_scopes; + } + SASSERT(num_scopes >= 2); + } + + TRACE("qe", tout << "backtrack: " << num_scopes << "\n";); + pop(num_scopes); + } + + void project_qe() { + SASSERT(level() >= 1 && m_mode == elim_t && m_valid_model); + clause cl(m_solver); + mbp(std::max(1u, level()-1), cl); + + expr_ref fml = clause2fml(cl); + TRACE("qe", tout << level() << ": " << fml << "\n";); + max_level clevel = get_level(cl); + if (level() == 1 || clevel.max() == 0) { + add_assumption_literal(cl, fml); + } + else { + enforce_parity(cl); + } + add_clause(cl); + + if (level() == 1) { // is_forall() && clevel.max() == 0 + add_to_answer(fml); + } + + if (level() == 1) { + pop(1); + } + else { + pop(2); + } + } + + void add_to_answer(expr_ref& fml) { + m_answer_simplify(fml); + expr* e; + if (m.is_not(fml, e)) { + m_answer_simplify.insert(e, m.mk_false()); + } + else { + m_answer_simplify.insert(fml, m.mk_true()); + } + m_answer.push_back(fml); + } + + expr_ref clause2fml(nlsat::scoped_literal_vector const& clause) { + expr_ref_vector fmls(m); + expr_ref fml(m); + expr* t; + nlsat2goal n2g(m); + for (unsigned i = 0; i < clause.size(); ++i) { + nlsat::literal l = clause[i]; + if (m_asm2fml.find(l.var(), t)) { + fml = t; + if (l.sign()) { + fml = push_not(fml); + } + SASSERT(l.sign()); + fmls.push_back(fml); + } + else { + fmls.push_back(n2g(m_solver, m_b2a, m_x2t, l)); + } + } + fml = mk_or(fmls); + return fml; + } + + void add_assumption_literal(clause& clause, expr* fml) { + nlsat::bool_var b = m_solver.mk_bool_var(); + clause.push_back(nlsat::literal(b, true)); + m_assumptions.push_back(nlsat::literal(b, false)); + m_asm2fml.insert(b, fml); + m_trail.push_back(fml); + m_bvar2level.insert(b, max_level()); + } + + bool is_exists() const { return is_exists(level()); } + bool is_forall() const { return is_forall(level()); } + bool is_exists(unsigned level) const { return (level % 2) == 0; } + bool is_forall(unsigned level) const { return is_exists(level+1); } + + void check_cancel() { + if (m_cancel) { + throw tactic_exception(TACTIC_CANCELED_MSG); + } + } + + void reset() { + //m_solver.reset(); + m_asms.reset(); + m_cached_asms.reset(); + m_cached_asms_lim.reset(); + m_is_true = nlsat::null_literal; + m_rmodel.reset(); + m_valid_model = false; + m_bound_rvars.reset(); + m_bound_bvars.reset(); + m_preds.reset(); + m_rvar2level.reset(); + m_bvar2level.reset(); + m_t2x.reset(); + m_a2b.reset(); + m_b2a.reset(); + m_x2t.reset(); + m_cancel = false; + m_st.reset(); + m_solver.collect_statistics(m_st); + m_free_vars.reset(); + m_answer.reset(); + m_answer_simplify.reset(); + m_assumptions.reset(); + m_asm2fml.reset(); + m_trail.reset(); + } + + void push() { + m_cached_asms_lim.push_back(m_cached_asms.size()); + } + + void pop(unsigned num_scopes) { + clear_model(); + unsigned new_level = level() - num_scopes; + m_cached_asms.shrink(m_cached_asms_lim[new_level]); + m_cached_asms_lim.shrink(new_level); + } + + void display(std::ostream& out) { + display_preds(out); + display_assumptions(out); + m_solver.display(out << "solver:\n"); + } + + void display_assumptions(std::ostream& out) { + m_solver.display(out << "assumptions: ", m_asms.size(), m_asms.c_ptr()); + out << "\n"; + } + + void display_preds(std::ostream& out) { + for (unsigned i = 0; i < m_preds.size(); ++i) { + m_solver.display(out << i << ": ", m_preds[i].size(), m_preds[i].c_ptr()); + out << "\n"; + } + } + + // expr -> nlsat::solver + + void hoist(expr_ref& fml) { + quantifier_hoister hoist(m); + vector qvars; + app_ref_vector vars(m); + bool is_forall = false; + pred_abs abs(m); + abs.get_free_vars(fml, vars); + insert_set(m_free_vars, vars); + qvars.push_back(vars); + vars.reset(); + if (m_mode == elim_t) { + is_forall = true; + hoist.pull_quantifier(is_forall, fml, vars); + qvars.push_back(vars); + } + else { + hoist.pull_quantifier(is_forall, fml, vars); + qvars.back().append(vars); + } + do { + is_forall = !is_forall; + vars.reset(); + hoist.pull_quantifier(is_forall, fml, vars); + qvars.push_back(vars); + } + while (!vars.empty()); + SASSERT(qvars.back().empty()); + init_expr2var(qvars); + + goal2nlsat g2s; + + expr_ref is_true(m), fml1(m), fml2(m); + is_true = m.mk_fresh_const("is_true", m.mk_bool_sort()); + fml = m.mk_iff(is_true, fml); + goal_ref g = alloc(goal, m); + g->assert_expr(fml); + proof_converter_ref pc; + expr_dependency_ref core(m); + model_converter_ref mc; + goal_ref_buffer result; + (*m_nftactic)(g, result, mc, pc, core); + SASSERT(result.size() == 1); + TRACE("qe", result[0]->display(tout);); + g2s(*result[0], m_params, m_solver, m_a2b, m_t2x); + + // insert variables and their levels. + for (unsigned i = 0; i < qvars.size(); ++i) { + m_bound_bvars.push_back(svector()); + m_bound_rvars.push_back(nlsat::var_vector()); + max_level lvl; + if (is_exists(i)) lvl.m_ex = i; else lvl.m_fa = i; + for (unsigned j = 0; j < qvars[i].size(); ++j) { + app* v = qvars[i][j].get(); + + if (m_a2b.is_var(v)) { + SASSERT(m.is_bool(v)); + nlsat::bool_var b = m_a2b.to_var(v); + m_bound_bvars.back().push_back(b); + set_level(b, lvl); + } + else if (m_t2x.is_var(v)) { + nlsat::var w = m_t2x.to_var(v); + m_bound_rvars.back().push_back(w); + m_rvar2level.setx(w, lvl, max_level()); + } + } + } + init_var2expr(); + m_is_true = nlsat::literal(m_a2b.to_var(is_true), false); + // insert literals from arithmetical sub-formulas + nlsat::atom_vector const& atoms = m_solver.get_atoms(); + for (unsigned i = 0; i < atoms.size(); ++i) { + if (atoms[i]) { + get_level(nlsat::literal(i, false)); + } + } + TRACE("qe", tout << fml << "\n";); + } + + void init_expr2var(vector const& qvars) { + for (unsigned i = 0; i < qvars.size(); ++i) { + init_expr2var(qvars[i]); + } + } + + void init_expr2var(app_ref_vector const& qvars) { + for (unsigned i = 0; i < qvars.size(); ++i) { + app* v = qvars[i]; + if (m.is_bool(v)) { + m_a2b.insert(v, m_solver.mk_bool_var()); + } + else { + // TODO: assert it is of type Real. + m_t2x.insert(v, m_solver.mk_var(false)); + } + } + } + + void init_var2expr() { + expr2var::iterator it = m_t2x.begin(), end = m_t2x.end(); + for (; it != end; ++it) { + m_x2t.insert(it->m_value, it->m_key); + } + it = m_a2b.begin(), end = m_a2b.end(); + for (; it != end; ++it) { + m_b2a.insert(it->m_value, it->m_key); + } + } + + + // Return false if nlsat assigned noninteger value to an integer variable. + // [copied from nlsat_tactic.cpp] + bool mk_model(model_converter_ref & mc) { + bool ok = true; + model_ref md = alloc(model, m); + arith_util util(m); + expr2var::iterator it = m_t2x.begin(), end = m_t2x.end(); + for (; it != end; ++it) { + nlsat::var x = it->m_value; + expr * t = it->m_key; + if (!is_uninterp_const(t) || !m_free_vars.contains(t)) + continue; + expr * v; + try { + v = util.mk_numeral(m_rmodel0.value(x), util.is_int(t)); + } + catch (z3_error & ex) { + throw ex; + } + catch (z3_exception &) { + v = util.mk_to_int(util.mk_numeral(m_rmodel0.value(x), false)); + ok = false; + } + md->register_decl(to_app(t)->get_decl(), v); + } + it = m_a2b.begin(), end = m_a2b.end(); + for (; it != end; ++it) { + expr * a = it->m_key; + nlsat::bool_var b = it->m_value; + if (a == 0 || !is_uninterp_const(a) || b == m_is_true.var() || !m_free_vars.contains(a)) + continue; + lbool val = m_bmodel0.get(b, l_undef); + if (val == l_undef) + continue; // don't care + md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false()); + } + mc = model2model_converter(md.get()); + return ok; + } + + public: + nlqsat(ast_manager& m, qsat_mode_t mode, params_ref const& p): + m(m), + m_mode(mode), + m_params(p), + m_solver(m.limit(), p), + m_nftactic(0), + m_rmodel(m_solver.am()), + m_rmodel0(m_solver.am()), + m_valid_model(false), + m_a2b(m), + m_t2x(m), + m_cancel(false), + m_answer(m), + m_answer_simplify(m), + m_trail(m) + { + m_solver.get_explain().set_signed_project(true); + m_nftactic = mk_tseitin_cnf_tactic(m); + } + + virtual ~nlqsat() { + } + + void updt_params(params_ref const & p) { + params_ref p2(p); + p2.set_bool("factor", false); + m_solver.updt_params(p2); + } + + void collect_param_descrs(param_descrs & r) { + } + + + void operator()(/* in */ goal_ref const & in, + /* out */ goal_ref_buffer & result, + /* out */ model_converter_ref & mc, + /* out */ proof_converter_ref & pc, + /* out */ expr_dependency_ref & core) { + + tactic_report report("nlqsat-tactic", *in); + + ptr_vector fmls; + expr_ref fml(m); + mc = 0; pc = 0; core = 0; + in->get_formulas(fmls); + fml = mk_and(m, fmls.size(), fmls.c_ptr()); + if (m_mode == elim_t) { + fml = m.mk_not(fml); + } + reset(); + TRACE("qe", tout << fml << "\n";); + hoist(fml); + TRACE("qe", tout << "ex: " << fml << "\n";); + lbool is_sat = check_sat(); + + switch (is_sat) { + case l_false: + in->reset(); + in->inc_depth(); + if (m_mode == elim_t) { + fml = mk_and(m_answer); + } + else { + fml = m.mk_false(); + } + in->assert_expr(fml); + result.push_back(in.get()); + break; + case l_true: + SASSERT(m_mode == qsat_t); + in->reset(); + in->inc_depth(); + result.push_back(in.get()); + if (in->models_enabled()) { + VERIFY(mk_model(mc)); + } + break; + case l_undef: + result.push_back(in.get()); + std::string s = "search failed"; + throw tactic_exception(s.c_str()); + } + } + + + void collect_statistics(statistics & st) const { + st.copy(m_st); + st.update("qsat num rounds", m_stats.m_num_rounds); + } + + void reset_statistics() { + m_stats.reset(); + m_solver.reset_statistics(); + } + + void cleanup() { + reset(); + } + + void set_logic(symbol const & l) { + } + + void set_progress_callback(progress_callback * callback) { + } + + tactic * translate(ast_manager & m) { + return alloc(nlqsat, m, m_mode, m_params); + } + +#if 0 + + /** + + Algorithm: + I := true + while there is M, such that M |= ~B & I: + find P, such that M => P => exists y . ~B & I + ; forall y B => ~P + C := core of P with respect to A + ; A => ~ C => ~ P + I := I & ~C + + + Alternative Algorithm: + R := false + while there is M, such that M |= A & ~R: + find I, such that M => I => forall y . B + R := R | I + + */ + + lbool interpolate(expr* a, expr* b, expr_ref& result) { + SASSERT(m_mode == interp_t); + + reset(); + app_ref enableA(m), enableB(m); + expr_ref A(m), B(m), fml(m); + expr_ref_vector fmls(m), answer(m); + + // varsB are private to B. + nlsat::var_vector vars; + uint_set fvars; + private_vars(a, b, vars, fvars); + + enableA = m.mk_const(symbol("#A"), m.mk_bool_sort()); + enableB = m.mk_not(enableA); + A = m.mk_implies(enableA, a); + B = m.mk_implies(enableB, m.mk_not(b)); + fml = m.mk_and(A, B); + hoist(fml); + + + + nlsat::literal _enableB = nlsat::literal(m_a2b.to_var(enableB), false); + nlsat::literal _enableA = ~_enableB; + + while (true) { + m_mode = qsat_t; + // enable B + m_assumptions.reset(); + m_assumptions.push_back(_enableB); + lbool is_sat = check_sat(); + + switch (is_sat) { + case l_undef: + return l_undef; + case l_true: + break; + case l_false: + result = mk_and(answer); + return l_true; + } + + // disable B, enable A + m_assumptions.reset(); + m_assumptions.push_back(_enableA); + // add blocking clause to solver. + + nlsat::scoped_literal_vector core(m_solver); + + m_mode = elim_t; + + mbp(vars, fvars, core); + + // minimize core. + nlsat::literal_vector _core(core.size(), core.c_ptr()); + _core.push_back(_enableA); + is_sat = m_solver.check(_core); // TBD: only for quantifier-free A. Generalize output of elim_t to be a core. + switch (is_sat) { + case l_undef: + return l_undef; + case l_true: + UNREACHABLE(); + case l_false: + core.reset(); + core.append(_core.size(), _core.c_ptr()); + break; + } + negate_clause(core); + // keep polarity of enableA, such that clause is only + // used when checking satisfiability of B. + for (unsigned i = 0; i < core.size(); ++i) { + if (core[i].var() == _enableA.var()) core.set(i, ~core[i]); + } + add_clause(core); // Invariant is added as assumption for B. + answer.push_back(clause2fml(core)); // TBD: remove answer literal. + } + } + + /** + \brief extract variables that are private to a (not used in b). + vars cover the real variables, and fvars cover the Boolean variables. + + TBD: We want fvars to be the complement such that returned core contains + Shared boolean variables, but not the ones private to B. + */ + void private_vars(expr* a, expr* b, nlsat::var_vector& vars, uint_set& fvars) { + app_ref_vector varsA(m), varsB(m); + obj_hashtable varsAS; + pred_abs abs(m); + abs.get_free_vars(a, varsA); + abs.get_free_vars(b, varsB); + insert_set(varsAS, varsA); + for (unsigned i = 0; i < varsB.size(); ++i) { + if (varsAS.contains(varsB[i].get())) { + varsB[i] = varsB.back(); + varsB.pop_back(); + --i; + } + } + for (unsigned j = 0; j < varsB.size(); ++j) { + app* v = varsB[j].get(); + if (m_a2b.is_var(v)) { + fvars.insert(m_a2b.to_var(v)); + } + else if (m_t2x.is_var(v)) { + vars.push_back(m_t2x.to_var(v)); + } + } + } + + lbool maximize(app* _x, expr* _fml, scoped_anum& result, bool& unbounded) { + expr_ref fml(_fml, m); + reset(); + hoist(fml); + nlsat::literal_vector lits; + lbool is_sat = l_true; + nlsat::var x = m_t2x.to_var(_x); + m_mode = qsat_t; + while (is_sat == l_true) { + is_sat = check_sat(); + if (is_sat == l_true) { + // m_asms is minimized set of literals that satisfy formula. + nlsat::explain& ex = m_solver.get_explain(); + polynomial::manager& pm = m_solver.pm(); + anum_manager& am = m_solver.am(); + ex.maximize(x, m_asms.size(), m_asms.c_ptr(), result, unbounded); + if (unbounded) { + break; + } + // TBD: assert the new bound on x using the result. + bool is_even = false; + polynomial::polynomial_ref pr(pm); + pr = pm.mk_polynomial(x); + rational r; + am.get_upper(result, r); + // result is algebraic numeral, but polynomials are not defined over extension field. + polynomial::polynomial* p = pr; + nlsat::bool_var b = m_solver.mk_ineq_atom(nlsat::atom::GT, 1, &p, &is_even); + nlsat::literal bound(b, false); + m_solver.mk_clause(1, &bound); + } + } + return is_sat; + } +#endif + }; +}; + +tactic * mk_nlqsat_tactic(ast_manager & m, params_ref const& p) { + return alloc(qe::nlqsat, m, qe::qsat_t, p); +} + +tactic * mk_nlqe_tactic(ast_manager & m, params_ref const& p) { + return alloc(qe::nlqsat, m, qe::elim_t, p); +} + + diff --git a/src/qe/nlqsat.h b/src/qe/nlqsat.h new file mode 100644 index 000000000..9d0cb6af4 --- /dev/null +++ b/src/qe/nlqsat.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + nlqsat.h + +Abstract: + + Quantifier Satisfiability Solver for nlsat + +Author: + + Nikolaj Bjorner (nbjorner) 2015-10-17 + +Revision History: + + +--*/ + +#ifndef QE_NLQSAT_H__ +#define QE_NLQSAT_H__ + +#include "tactic.h" + + +tactic * mk_nlqsat_tactic(ast_manager & m, params_ref const& p = params_ref()); +tactic * mk_nlqe_tactic(ast_manager & m, params_ref const& p = params_ref()); + + +/* + ADD_TACTIC("nlqsat", "apply a NL-QSAT solver.", "mk_nlqsat_tactic(m, p)") + +*/ + +// TBD_TACTIC("nlqe", "apply a NL-QE solver.", "mk_nlqe_tactic(m, p)") + +#endif diff --git a/src/qe/qe_util.cpp b/src/qe/qe_util.cpp deleted file mode 100644 index 2bcda608f..000000000 --- a/src/qe/qe_util.cpp +++ /dev/null @@ -1,26 +0,0 @@ - -/*++ -Copyright (c) 2015 Microsoft Corporation - ---*/ - -#include "qe_util.h" -#include "bool_rewriter.h" - -namespace qe { - - expr_ref mk_and(expr_ref_vector const& fmls) { - ast_manager& m = fmls.get_manager(); - expr_ref result(m); - bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), result); - return result; - } - - expr_ref mk_or(expr_ref_vector const& fmls) { - ast_manager& m = fmls.get_manager(); - expr_ref result(m); - bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), result); - return result; - } - -} diff --git a/src/qe/qe_util.h b/src/qe/qe_util.h deleted file mode 100644 index ea082d78c..000000000 --- a/src/qe/qe_util.h +++ /dev/null @@ -1,31 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - qe_util.h - -Abstract: - - Utilities for quantifiers. - -Author: - - Nikolaj Bjorner (nbjorner) 2013-08-28 - -Revision History: - ---*/ -#ifndef QE_UTIL_H_ -#define QE_UTIL_H_ - -#include "ast.h" - -namespace qe { - - expr_ref mk_and(expr_ref_vector const& fmls); - - expr_ref mk_or(expr_ref_vector const& fmls); - -} -#endif diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp new file mode 100644 index 000000000..75cf57fa3 --- /dev/null +++ b/src/qe/qsat.cpp @@ -0,0 +1,1176 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qsat.cpp + +Abstract: + + Quantifier Satisfiability Solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-28 + +Revision History: + +Notes: + + +--*/ + +#include "smt_kernel.h" +#include "qe_mbp.h" +#include "smt_params.h" +#include "ast_util.h" +#include "quant_hoist.h" +#include "ast_pp.h" +#include "model_v2_pp.h" +#include "qsat.h" +#include "expr_abstract.h" +#include "qe.h" +#include "label_rewriter.h" + + +namespace qe { + + pred_abs::pred_abs(ast_manager& m): + m(m), + m_asms(m), + m_trail(m), + m_fmc(alloc(filter_model_converter, m)) + { + } + + filter_model_converter* pred_abs::fmc() { + return m_fmc.get(); + } + + void pred_abs::reset() { + m_trail.reset(); + dec_keys(m_pred2lit); + dec_keys(m_lit2pred); + dec_keys(m_asm2pred); + dec_keys(m_pred2asm); + m_lit2pred.reset(); + m_pred2lit.reset(); + m_asm2pred.reset(); + m_pred2asm.reset(); + m_elevel.reset(); + m_asms.reset(); + m_asms_lim.reset(); + m_preds.reset(); + } + + max_level pred_abs::compute_level(app* e) { + unsigned sz0 = todo.size(); + todo.push_back(e); + while (sz0 != todo.size()) { + app* a = to_app(todo.back()); + if (m_elevel.contains(a)) { + todo.pop_back(); + continue; + } + max_level lvl, lvl0; + bool has_new = false; + if (m_flevel.find(a->get_decl(), lvl)) { + lvl0.merge(lvl); + } + for (unsigned i = 0; i < a->get_num_args(); ++i) { + app* arg = to_app(a->get_arg(i)); + if (m_elevel.find(arg, lvl)) { + lvl0.merge(lvl); + } + else { + todo.push_back(arg); + has_new = true; + } + } + if (!has_new) { + m_elevel.insert(a, lvl0); + todo.pop_back(); + } + } + return m_elevel.find(e); + } + + void pred_abs::add_pred(app* p, app* lit) { + m.inc_ref(p); + m_pred2lit.insert(p, lit); + add_lit(p, lit); + } + + void pred_abs::add_lit(app* p, app* lit) { + if (!m_lit2pred.contains(lit)) { + m.inc_ref(lit); + m_lit2pred.insert(lit, p); + } + } + + void pred_abs::add_asm(app* p, expr* assum) { + SASSERT(!m_asm2pred.contains(assum)); + m.inc_ref(p); + m.inc_ref(assum); + m_asm2pred.insert(assum, p); + m_pred2asm.insert(p, assum); + } + + void pred_abs::push() { + m_asms_lim.push_back(m_asms.size()); + } + + void pred_abs::pop(unsigned num_scopes) { + unsigned l = m_asms_lim.size() - num_scopes; + m_asms.resize(m_asms_lim[l]); + m_asms_lim.shrink(l); + } + + void pred_abs::insert(app* a, max_level const& lvl) { + unsigned l = lvl.max(); + if (l == UINT_MAX) l = 0; + while (m_preds.size() <= l) { + m_preds.push_back(app_ref_vector(m)); + } + m_preds[l].push_back(a); + } + + bool pred_abs::is_predicate(app* a, unsigned l) { + max_level lvl1; + return m_flevel.find(a->get_decl(), lvl1) && lvl1.max() < l; + } + + void pred_abs::get_assumptions(model* mdl, expr_ref_vector& asms) { + unsigned level = m_asms_lim.size(); + if (level > m_preds.size()) { + level = m_preds.size(); + } + if (!mdl) { + asms.append(m_asms); + return; + } + if (level == 0) { + return; + } + expr_ref val(m); + for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) { + app* p = m_preds[level - 1][j].get(); + TRACE("qe", tout << "process level: " << level - 1 << ": " << mk_pp(p, m) << "\n";); + + VERIFY(mdl->eval(p, val)); + + if (m.is_false(val)) { + m_asms.push_back(m.mk_not(p)); + } + else { + SASSERT(m.is_true(val)); + m_asms.push_back(p); + } + } + asms.append(m_asms); + + for (unsigned i = level + 1; i < m_preds.size(); i += 2) { + for (unsigned j = 0; j < m_preds[i].size(); ++j) { + app* p = m_preds[i][j].get(); + max_level lvl = m_elevel.find(p); + bool use = + (lvl.m_fa == i && (lvl.m_ex == UINT_MAX || lvl.m_ex < level)) || + (lvl.m_ex == i && (lvl.m_fa == UINT_MAX || lvl.m_fa < level)); + if (use) { + VERIFY(mdl->eval(p, val)); + if (m.is_false(val)) { + asms.push_back(m.mk_not(p)); + } + else { + asms.push_back(p); + } + } + } + } + TRACE("qe", tout << "level: " << level << "\n"; + model_v2_pp(tout, *mdl); + display(tout, asms);); + } + + void pred_abs::set_expr_level(app* v, max_level const& lvl) { + m_elevel.insert(v, lvl); + } + + void pred_abs::set_decl_level(func_decl* f, max_level const& lvl) { + m_flevel.insert(f, lvl); + } + + void pred_abs::abstract_atoms(expr* fml, expr_ref_vector& defs) { + max_level level; + abstract_atoms(fml, level, defs); + } + /** + \brief create propositional abstraction of formula by replacing atomic sub-formulas by fresh + propositional variables, and adding definitions for each propositional formula on the side. + Assumption is that the formula is quantifier-free. + */ + void pred_abs::abstract_atoms(expr* fml, max_level& level, expr_ref_vector& defs) { + expr_mark mark; + ptr_vector args; + app_ref r(m), eq(m); + app* p; + unsigned sz0 = todo.size(); + todo.push_back(fml); + m_trail.push_back(fml); + max_level l; + while (sz0 != todo.size()) { + app* a = to_app(todo.back()); + todo.pop_back(); + if (mark.is_marked(a)) { + continue; + } + + mark.mark(a); + if (m_lit2pred.find(a, p)) { + TRACE("qe", tout << mk_pp(a, m) << " " << mk_pp(p, m) << "\n";); + level.merge(m_elevel.find(p)); + continue; + } + + if (is_uninterp_const(a) && m.is_bool(a)) { + l = m_elevel.find(a); + level.merge(l); + if (!m_pred2lit.contains(a)) { + add_pred(a, a); + insert(a, l); + } + continue; + } + + unsigned sz = a->get_num_args(); + for (unsigned i = 0; i < sz; ++i) { + expr* f = a->get_arg(i); + if (!mark.is_marked(f)) { + todo.push_back(f); + } + } + + bool is_boolop = + (a->get_family_id() == m.get_basic_family_id()) && + (!m.is_eq(a) || m.is_bool(a->get_arg(0))) && + (!m.is_distinct(a) || m.is_bool(a->get_arg(0))); + + if (!is_boolop && m.is_bool(a)) { + TRACE("qe", tout << mk_pp(a, m) << "\n";); + r = fresh_bool("p"); + max_level l = compute_level(a); + add_pred(r, a); + m_elevel.insert(r, l); + eq = m.mk_eq(r, a); + defs.push_back(eq); + if (!is_predicate(a, l.max())) { + insert(r, l); + } + level.merge(l); + } + } + } + + app_ref pred_abs::fresh_bool(char const* name) { + app_ref r(m.mk_fresh_const(name, m.mk_bool_sort()), m); + m_fmc->insert(r->get_decl()); + return r; + } + + + // optional pass to replace atoms by predicates + // so that SMT core works on propositional + // abstraction only. + expr_ref pred_abs::mk_abstract(expr* fml) { + expr_ref_vector trail(m), args(m); + obj_map cache; + app* b; + expr_ref r(m); + unsigned sz0 = todo.size(); + todo.push_back(fml); + while (sz0 != todo.size()) { + app* a = to_app(todo.back()); + if (cache.contains(a)) { + todo.pop_back(); + continue; + } + if (m_lit2pred.find(a, b)) { + cache.insert(a, b); + todo.pop_back(); + continue; + } + unsigned sz = a->get_num_args(); + bool diff = false; + args.reset(); + for (unsigned i = 0; i < sz; ++i) { + expr* f = a->get_arg(i), *f1; + if (cache.find(f, f1)) { + args.push_back(f1); + diff |= f != f1; + } + else { + todo.push_back(f); + } + } + if (sz == args.size()) { + if (diff) { + r = m.mk_app(a->get_decl(), sz, args.c_ptr()); + trail.push_back(r); + } + else { + r = a; + } + cache.insert(a, r); + todo.pop_back(); + } + } + return expr_ref(cache.find(fml), m); + } + + expr_ref pred_abs::mk_assumption_literal(expr* a, model* mdl, max_level const& lvl, expr_ref_vector& defs) { + expr_ref A(m); + A = pred2asm(a); + a = A; + app_ref p(m); + expr_ref q(m), fml(m); + app *b; + expr *c, *d; + max_level lvl2; + TRACE("qe", tout << mk_pp(a, m) << " " << lvl << "\n";); + if (m_asm2pred.find(a, b)) { + q = b; + } + else if (m.is_not(a, c) && m_asm2pred.find(c, b)) { + q = m.mk_not(b); + } + else if (m_pred2asm.find(a, d)) { + q = a; + } + else if (m.is_not(a, c) && m_pred2asm.find(c, d)) { + q = a; + } + else { + p = fresh_bool("def"); + if (m.is_not(a, a)) { + if (mdl) + mdl->register_decl(p->get_decl(), m.mk_false()); + q = m.mk_not(p); + } + else { + if (mdl) + mdl->register_decl(p->get_decl(), m.mk_true()); + q = p; + } + m_elevel.insert(p, lvl); + insert(p, lvl); + fml = a; + abstract_atoms(fml, lvl2, defs); + fml = mk_abstract(fml); + defs.push_back(m.mk_eq(p, fml)); + add_asm(p, a); + TRACE("qe", tout << mk_pp(a, m) << " |-> " << p << "\n";); + } + return q; + } + + void pred_abs::mk_concrete(expr_ref_vector& fmls, obj_map const& map) { + obj_map cache; + expr_ref_vector trail(m); + expr* p; + app_ref r(m); + ptr_vector args; + unsigned sz0 = todo.size(); + todo.append(fmls.size(), (expr*const*)fmls.c_ptr()); + while (sz0 != todo.size()) { + app* a = to_app(todo.back()); + if (cache.contains(a)) { + todo.pop_back(); + continue; + } + if (map.find(a, p)) { + cache.insert(a, p); + todo.pop_back(); + continue; + } + unsigned sz = a->get_num_args(); + args.reset(); + bool diff = false; + for (unsigned i = 0; i < sz; ++i) { + expr* f = a->get_arg(i), *f1; + if (cache.find(f, f1)) { + args.push_back(f1); + diff |= f != f1; + } + else { + todo.push_back(f); + } + } + if (args.size() == sz) { + if (diff) { + r = m.mk_app(a->get_decl(), sz, args.c_ptr()); + } + else { + r = to_app(a); + } + cache.insert(a, r); + trail.push_back(r); + todo.pop_back(); + } + } + for (unsigned i = 0; i < fmls.size(); ++i) { + fmls[i] = to_app(cache.find(fmls[i].get())); + } + } + + void pred_abs::pred2lit(expr_ref_vector& fmls) { + mk_concrete(fmls, m_pred2lit); + } + + expr_ref pred_abs::pred2asm(expr* fml) { + expr_ref_vector fmls(m); + fmls.push_back(fml); + mk_concrete(fmls, m_pred2asm); + return mk_and(fmls); + } + + void pred_abs::collect_statistics(statistics& st) const { + st.update("qsat num predicates", m_pred2lit.size()); + } + + void pred_abs::display(std::ostream& out) const { + out << "pred2lit:\n"; + obj_map::iterator it = m_pred2lit.begin(), end = m_pred2lit.end(); + for (; it != end; ++it) { + out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value, m) << "\n"; + } + for (unsigned i = 0; i < m_preds.size(); ++i) { + out << "level " << i << "\n"; + for (unsigned j = 0; j < m_preds[i].size(); ++j) { + app* p = m_preds[i][j]; + expr* e; + if (m_pred2lit.find(p, e)) { + out << mk_pp(p, m) << " := " << mk_pp(e, m) << "\n"; + } + else { + out << mk_pp(p, m) << "\n"; + } + } + } + } + + void pred_abs::display(std::ostream& out, expr_ref_vector const& asms) const { + max_level lvl; + for (unsigned i = 0; i < asms.size(); ++i) { + expr* e = asms[i]; + bool is_not = m.is_not(asms[i], e); + out << mk_pp(asms[i], m); + if (m_elevel.find(e, lvl)) { + lvl.display(out << " - "); + } + if (m_pred2lit.find(e, e)) { + out << " : " << (is_not?"!":"") << mk_pp(e, m); + } + out << "\n"; + } + } + + void pred_abs::get_free_vars(expr* fml, app_ref_vector& vars) { + ast_fast_mark1 mark; + unsigned sz0 = todo.size(); + todo.push_back(fml); + while (sz0 != todo.size()) { + expr* e = todo.back(); + todo.pop_back(); + if (mark.is_marked(e) || is_var(e)) { + continue; + } + mark.mark(e); + if (is_quantifier(e)) { + todo.push_back(to_quantifier(e)->get_expr()); + continue; + } + SASSERT(is_app(e)); + app* a = to_app(e); + if (is_uninterp_const(a)) { // TBD generalize for uninterpreted functions. + vars.push_back(a); + } + for (unsigned i = 0; i < a->get_num_args(); ++i) { + todo.push_back(a->get_arg(i)); + } + } + } + + class qsat : public tactic { + + struct stats { + unsigned m_num_rounds; + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + }; + + class kernel { + ast_manager& m; + smt_params m_smtp; + smt::kernel m_kernel; + + public: + kernel(ast_manager& m): + m(m), + m_kernel(m, m_smtp) + { + m_smtp.m_model = true; + m_smtp.m_relevancy_lvl = 0; + } + + smt::kernel& k() { return m_kernel; } + smt::kernel const& k() const { return m_kernel; } + + void assert_expr(expr* e) { + m_kernel.assert_expr(e); + } + + void get_core(expr_ref_vector& core) { + unsigned sz = m_kernel.get_unsat_core_size(); + core.reset(); + for (unsigned i = 0; i < sz; ++i) { + core.push_back(m_kernel.get_unsat_core_expr(i)); + } + TRACE("qe", tout << "core: " << core << "\n"; + m_kernel.display(tout); + tout << "\n"; + ); + } + }; + + ast_manager& m; + params_ref m_params; + stats m_stats; + statistics m_st; + qe::mbp m_mbp; + kernel m_fa; + kernel m_ex; + pred_abs m_pred_abs; + expr_ref_vector m_answer; + expr_ref_vector m_asms; + vector m_vars; // variables from alternating prefixes. + unsigned m_level; + model_ref m_model; + bool m_qelim; // perform quantifier elimination + bool m_force_elim; // force elimination of variables during projection. + app_ref_vector m_avars; // variables to project + app_ref_vector m_free_vars; + + + /** + \brief check alternating satisfiability. + Even levels are existential, odd levels are universal. + */ + lbool check_sat() { + while (true) { + ++m_stats.m_num_rounds; + check_cancel(); + expr_ref_vector asms(m_asms); + m_pred_abs.get_assumptions(m_model.get(), asms); + TRACE("qe", tout << asms << "\n";); + smt::kernel& k = get_kernel(m_level).k(); + lbool res = k.check(asms); + switch (res) { + case l_true: + k.get_model(m_model); + SASSERT(validate_model(asms)); + TRACE("qe", k.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); ); + push(); + break; + case l_false: + switch (m_level) { + case 0: return l_false; + case 1: + if (!m_qelim) return l_true; + if (m_model.get()) { + project_qe(asms); + } + else { + pop(1); + } + break; + default: + if (m_model.get()) { + project(asms); + } + else { + pop(1); + } + break; + } + break; + case l_undef: + return res; + } + } + return l_undef; + } + + kernel& get_kernel(unsigned j) { + if (is_exists(j)) { + return m_ex; + } + else { + return m_fa; + } + } + + bool is_exists(unsigned level) const { + return (level % 2) == 0; + } + + bool is_forall(unsigned level) const { + return is_exists(level+1); + } + + void push() { + m_level++; + m_pred_abs.push(); + } + + void pop(unsigned num_scopes) { + m_model.reset(); + SASSERT(num_scopes <= m_level); + m_pred_abs.pop(num_scopes); + m_level -= num_scopes; + } + + void reset() { + m_st.reset(); + m_fa.k().collect_statistics(m_st); + m_ex.k().collect_statistics(m_st); + m_pred_abs.collect_statistics(m_st); + m_level = 0; + m_answer.reset(); + m_asms.reset(); + m_pred_abs.reset(); + m_vars.reset(); + m_model = 0; + m_fa.k().reset(); + m_ex.k().reset(); + m_free_vars.reset(); + } + + /** + \brief create a quantifier prefix formula. + */ + void hoist(expr_ref& fml) { + proof_ref pr(m); + label_rewriter rw(m); + rw.remove_labels(fml, pr); + quantifier_hoister hoist(m); + app_ref_vector vars(m); + bool is_forall = false; + m_pred_abs.get_free_vars(fml, vars); + m_vars.push_back(vars); + vars.reset(); + if (m_qelim) { + is_forall = true; + hoist.pull_quantifier(is_forall, fml, vars); + m_vars.push_back(vars); + } + else { + hoist.pull_quantifier(is_forall, fml, vars); + m_vars.back().append(vars); + } + do { + is_forall = !is_forall; + vars.reset(); + hoist.pull_quantifier(is_forall, fml, vars); + m_vars.push_back(vars); + } + while (!vars.empty()); + SASSERT(m_vars.back().empty()); + initialize_levels(); + TRACE("qe", tout << fml << "\n";); + } + + void initialize_levels() { + // initialize levels. + for (unsigned i = 0; i < m_vars.size(); ++i) { + max_level lvl; + if (is_exists(i)) { + lvl.m_ex = i; + } + else { + lvl.m_fa = i; + } + for (unsigned j = 0; j < m_vars[i].size(); ++j) { + m_pred_abs.set_expr_level(m_vars[i][j].get(), lvl); + } + } + } + + void get_core(expr_ref_vector& core, unsigned level) { + get_kernel(level).get_core(core); + m_pred_abs.pred2lit(core); + } + + void check_cancel() { + if (m.canceled()) { + throw tactic_exception(m.limit().get_cancel_msg()); + } + } + + void display(std::ostream& out) const { + out << "level: " << m_level << "\n"; + for (unsigned i = 0; i < m_vars.size(); ++i) { + for (unsigned j = 0; j < m_vars[i].size(); ++j) { + expr* v = m_vars[i][j]; + out << mk_pp(v, m) << " "; + } + out << "\n"; + } + m_pred_abs.display(out); + } + + void display(std::ostream& out, model& model) const { + display(out); + model_v2_pp(out, model); + } + + void display(std::ostream& out, expr_ref_vector const& asms) const { + m_pred_abs.display(out, asms); + } + + void add_assumption(expr* fml) { + expr_ref eq(m); + app_ref b = m_pred_abs.fresh_bool("b"); + m_asms.push_back(b); + eq = m.mk_eq(b, fml); + m_ex.assert_expr(eq); + m_fa.assert_expr(eq); + m_pred_abs.add_pred(b, to_app(fml)); + max_level lvl; + m_pred_abs.set_expr_level(b, lvl); + } + + void project_qe(expr_ref_vector& core) { + SASSERT(m_level == 1); + expr_ref fml(m); + model& mdl = *m_model.get(); + get_core(core, m_level); + SASSERT(validate_core(core)); + get_vars(m_level); + m_mbp(m_force_elim, m_avars, mdl, core); + fml = negate_core(core); + add_assumption(fml); + m_answer.push_back(fml); + m_free_vars.append(m_avars); + pop(1); + } + + void project(expr_ref_vector& core) { + get_core(core, m_level); + TRACE("qe", display(tout); display(tout << "core\n", core);); + SASSERT(validate_core(core)); + SASSERT(m_level >= 2); + expr_ref fml(m); + expr_ref_vector defs(m), core_save(m); + max_level level; + model& mdl = *m_model.get(); + + get_vars(m_level-1); + SASSERT(validate_project(mdl, core)); + m_mbp(m_force_elim, m_avars, mdl, core); + m_free_vars.append(m_avars); + fml = negate_core(core); + unsigned num_scopes = 0; + + m_pred_abs.abstract_atoms(fml, level, defs); + m_ex.assert_expr(mk_and(defs)); + m_fa.assert_expr(mk_and(defs)); + if (level.max() == UINT_MAX) { + num_scopes = 2*(m_level/2); + } + else if (m_qelim && !m_force_elim) { + num_scopes = 2; + } + else { + SASSERT(level.max() + 2 <= m_level); + num_scopes = m_level - level.max(); + SASSERT(num_scopes >= 2); + if ((num_scopes % 2) != 0) { + --num_scopes; + } + } + + pop(num_scopes); + TRACE("qe", tout << "backtrack: " << num_scopes << " new level: " << m_level << "\nproject:\n" << core << "\n|->\n" << fml << "\n";); + if (m_level == 0 && m_qelim) { + add_assumption(fml); + } + else { + fml = m_pred_abs.mk_abstract(fml); + get_kernel(m_level).assert_expr(fml); + } + } + + void get_vars(unsigned level) { + m_avars.reset(); + for (unsigned i = level; i < m_vars.size(); ++i) { + m_avars.append(m_vars[i]); + } + } + + expr_ref negate_core(expr_ref_vector& core) { + return ::push_not(::mk_and(core)); + } + + expr_ref elim_rec(expr* fml) { + expr_ref tmp(m); + expr_ref_vector trail(m); + obj_map visited; + ptr_vector todo; + trail.push_back(fml); + todo.push_back(fml); + expr* e = 0, *r = 0; + + while (!todo.empty()) { + check_cancel(); + + e = todo.back(); + if (visited.contains(e)) { + todo.pop_back(); + continue; + } + + switch(e->get_kind()) { + case AST_APP: { + app* a = to_app(e); + expr_ref_vector args(m); + unsigned num_args = a->get_num_args(); + bool all_visited = true; + for (unsigned i = 0; i < num_args; ++i) { + if (visited.find(a->get_arg(i), r)) { + args.push_back(r); + } + else { + todo.push_back(a->get_arg(i)); + all_visited = false; + } + } + if (all_visited) { + r = m.mk_app(a->get_decl(), args.size(), args.c_ptr()); + todo.pop_back(); + trail.push_back(r); + visited.insert(e, r); + } + break; + } + case AST_QUANTIFIER: { + app_ref_vector vars(m); + quantifier* q = to_quantifier(e); + bool is_fa = q->is_forall(); + tmp = q->get_expr(); + extract_vars(q, tmp, vars); + TRACE("qe", tout << vars << " " << mk_pp(q, m) << " " << tmp << "\n";); + tmp = elim_rec(tmp); + if (is_fa) { + tmp = ::push_not(tmp); + } + tmp = elim(vars, tmp); + if (is_fa) { + tmp = ::push_not(tmp); + } + trail.push_back(tmp); + visited.insert(e, tmp); + todo.pop_back(); + break; + } + default: + UNREACHABLE(); + break; + } + } + VERIFY (visited.find(fml, e)); + return expr_ref(e, m); + } + + expr_ref elim(app_ref_vector const& vars, expr* _fml) { + expr_ref fml(_fml, m); + reset(); + m_vars.push_back(app_ref_vector(m)); + m_vars.push_back(vars); + initialize_levels(); + fml = push_not(fml); + + TRACE("qe", tout << vars << " " << fml << "\n";); + expr_ref_vector defs(m); + m_pred_abs.abstract_atoms(fml, defs); + fml = m_pred_abs.mk_abstract(fml); + m_ex.assert_expr(mk_and(defs)); + m_fa.assert_expr(mk_and(defs)); + m_ex.assert_expr(fml); + m_fa.assert_expr(m.mk_not(fml)); + TRACE("qe", tout << "ex: " << fml << "\n";); + lbool is_sat = check_sat(); + fml = ::mk_and(m_answer); + TRACE("qe", tout << "ans: " << fml << "\n"; + tout << "Free vars: " << m_free_vars << "\n";); + if (is_sat == l_false) { + obj_hashtable vars; + for (unsigned i = 0; i < m_free_vars.size(); ++i) { + app* v = m_free_vars[i].get(); + if (vars.contains(v)) { + m_free_vars[i] = m_free_vars.back(); + m_free_vars.pop_back(); + --i; + } + else { + vars.insert(v); + } + } + fml = mk_exists(m, m_free_vars.size(), m_free_vars.c_ptr(), fml); + return fml; + } + else { + return expr_ref(_fml, m); + } + } + + bool validate_core(expr_ref_vector const& core) { + TRACE("qe", tout << "Validate core\n";); + smt::kernel& k = get_kernel(m_level).k(); + expr_ref_vector fmls(m); + fmls.append(core.size(), core.c_ptr()); + fmls.append(k.size(), k.get_formulas()); + return check_fmls(fmls); + } + + bool check_fmls(expr_ref_vector const& fmls) { + smt_params p; + smt::kernel solver(m, p); + for (unsigned i = 0; i < fmls.size(); ++i) { + solver.assert_expr(fmls[i]); + } + lbool is_sat = solver.check(); + CTRACE("qe", is_sat != l_false, + tout << fmls << "\nare not unsat\n";); + return (is_sat == l_false); + } + + bool validate_model(expr_ref_vector const& asms) { + TRACE("qe", tout << "Validate model\n";); + smt::kernel& k = get_kernel(m_level).k(); + return + validate_model(*m_model, asms.size(), asms.c_ptr()) && + validate_model(*m_model, k.size(), k.get_formulas()); + } + + bool validate_model(model& mdl, unsigned sz, expr* const* fmls) { + expr_ref val(m); + for (unsigned i = 0; i < sz; ++i) { + if (!m_model->eval(fmls[i], val)) { + TRACE("qe", tout << "Formula does not evaluate in model: " << mk_pp(fmls[i], m) << "\n";); + return false; + } + if (!m.is_true(val)) { + TRACE("qe", tout << mk_pp(fmls[i], m) << " evaluates to " << val << " in model\n";); + return false; + } + } + return true; + } + + // validate the following: + // proj is true in model. + // core is true in model. + // proj does not contain vars. + // proj => exists vars . core + // (core[model(vars)/vars] => proj) + + bool validate_project(model& mdl, expr_ref_vector const& core) { + TRACE("qe", tout << "Validate projection\n";); + if (!validate_model(mdl, core.size(), core.c_ptr())) return false; + + expr_ref_vector proj(core); + app_ref_vector vars(m_avars); + m_mbp(false, vars, mdl, proj); + if (!vars.empty()) { + TRACE("qe", tout << "Not validating partial projection\n";); + return true; + } + if (!validate_model(mdl, proj.size(), proj.c_ptr())) { + TRACE("qe", tout << "Projection is false in model\n";); + return false; + } + for (unsigned i = 0; i < m_avars.size(); ++i) { + contains_app cont(m, m_avars[i].get()); + if (cont(proj)) { + TRACE("qe", tout << "Projection contains free variable: " << mk_pp(m_avars[i].get(), m) << "\n";); + return false; + } + } + + // + // TBD: proj => exists vars . core, + // e.g., extract and use realizer functions from mbp. + // + + // (core[model(vars)/vars] => proj) + expr_ref_vector fmls(m); + fmls.append(core.size(), core.c_ptr()); + for (unsigned i = 0; i < m_avars.size(); ++i) { + expr_ref val(m); + VERIFY(mdl.eval(m_avars[i].get(), val)); + fmls.push_back(m.mk_eq(m_avars[i].get(), val)); + } + fmls.push_back(m.mk_not(mk_and(proj))); + if (!check_fmls(fmls)) { + TRACE("qe", tout << "implication check failed, could be due to turning != into >\n";); + } + return true; + } + + public: + + qsat(ast_manager& m, params_ref const& p, bool qelim, bool force_elim): + m(m), + m_mbp(m), + m_fa(m), + m_ex(m), + m_pred_abs(m), + m_answer(m), + m_asms(m), + m_level(0), + m_qelim(qelim), + m_force_elim(force_elim), + m_avars(m), + m_free_vars(m) + { + reset(); + } + + virtual ~qsat() { + reset(); + } + + void updt_params(params_ref const & p) { + } + + void collect_param_descrs(param_descrs & r) { + } + + + void operator()(/* in */ goal_ref const & in, + /* out */ goal_ref_buffer & result, + /* out */ model_converter_ref & mc, + /* out */ proof_converter_ref & pc, + /* out */ expr_dependency_ref & core) { + tactic_report report("qsat-tactic", *in); + ptr_vector fmls; + expr_ref_vector defs(m); + expr_ref fml(m); + mc = 0; pc = 0; core = 0; + in->get_formulas(fmls); + fml = mk_and(m, fmls.size(), fmls.c_ptr()); + + // for now: + // fail if cores. (TBD) + // fail if proofs. (TBD) + + if (!m_force_elim) { + fml = elim_rec(fml); + in->reset(); + in->inc_depth(); + in->assert_expr(fml); + result.push_back(in.get()); + return; + } + + reset(); + TRACE("qe", tout << fml << "\n";); + if (m_qelim) { + fml = push_not(fml); + } + hoist(fml); + m_pred_abs.abstract_atoms(fml, defs); + fml = m_pred_abs.mk_abstract(fml); + m_ex.assert_expr(mk_and(defs)); + m_fa.assert_expr(mk_and(defs)); + m_ex.assert_expr(fml); + m_fa.assert_expr(m.mk_not(fml)); + TRACE("qe", tout << "ex: " << fml << "\n";); + lbool is_sat = check_sat(); + + switch (is_sat) { + case l_false: + in->reset(); + in->inc_depth(); + if (m_qelim) { + fml = ::mk_and(m_answer); + in->assert_expr(fml); + } + else { + in->assert_expr(m.mk_false()); + } + result.push_back(in.get()); + break; + case l_true: + in->reset(); + in->inc_depth(); + result.push_back(in.get()); + if (in->models_enabled()) { + mc = model2model_converter(m_model.get()); + mc = concat(m_pred_abs.fmc(), mc.get()); + } + break; + case l_undef: + result.push_back(in.get()); + std::string s = m_ex.k().last_failure_as_string(); + if (s == "ok") { + s = m_fa.k().last_failure_as_string(); + } + throw tactic_exception(s.c_str()); + } + } + + void collect_statistics(statistics & st) const { + st.copy(m_st); + st.update("qsat num rounds", m_stats.m_num_rounds); + m_pred_abs.collect_statistics(st); + } + + void reset_statistics() { + m_stats.reset(); + m_fa.k().reset_statistics(); + m_ex.k().reset_statistics(); + } + + void cleanup() { + reset(); + } + + void set_logic(symbol const & l) { + } + + void set_progress_callback(progress_callback * callback) { + } + + tactic * translate(ast_manager & m) { + return alloc(qsat, m, m_params, m_qelim, m_force_elim); + } + + + }; + +}; + +tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) { + return alloc(qe::qsat, m, p, false, true); +} + +tactic * mk_qe2_tactic(ast_manager& m, params_ref const& p) { + return alloc(qe::qsat, m, p, true, true); +} + +tactic * mk_qe_rec_tactic(ast_manager& m, params_ref const& p) { + return alloc(qe::qsat, m, p, true, false); +} + + diff --git a/src/qe/qsat.h b/src/qe/qsat.h new file mode 100644 index 000000000..ee9f9e6ad --- /dev/null +++ b/src/qe/qsat.h @@ -0,0 +1,135 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qsat.h + +Abstract: + + Quantifier Satisfiability Solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-28 + +Revision History: + + +--*/ + +#ifndef QE_QSAT_H__ +#define QE_QSAT_H__ + +#include "tactic.h" +#include "filter_model_converter.h" + +namespace qe { + + struct max_level { + unsigned m_ex, m_fa; + max_level(): m_ex(UINT_MAX), m_fa(UINT_MAX) {} + void merge(max_level const& other) { + merge(m_ex, other.m_ex); + merge(m_fa, other.m_fa); + } + static unsigned max(unsigned a, unsigned b) { + if (a == UINT_MAX) return b; + if (b == UINT_MAX) return a; + return std::max(a, b); + } + unsigned max() const { + return max(m_ex, m_fa); + } + void merge(unsigned& lvl, unsigned other) { + lvl = max(lvl, other); + } + std::ostream& display(std::ostream& out) const { + if (m_ex != UINT_MAX) out << "e" << m_ex << " "; + if (m_fa != UINT_MAX) out << "a" << m_fa << " "; + return out; + } + + bool operator==(max_level const& other) const { + return + m_ex == other.m_ex && + m_fa == other.m_fa; + } + }; + + inline std::ostream& operator<<(std::ostream& out, max_level const& lvl) { + return lvl.display(out); + } + + class pred_abs { + ast_manager& m; + vector m_preds; + expr_ref_vector m_asms; + unsigned_vector m_asms_lim; + obj_map m_pred2lit; // maintain definitions of predicates. + obj_map m_lit2pred; // maintain reverse mapping to predicates + obj_map m_asm2pred; // maintain map from assumptions to predicates + obj_map m_pred2asm; // predicates |-> assumptions + expr_ref_vector m_trail; + filter_model_converter_ref m_fmc; + ptr_vector todo; + obj_map m_elevel; + obj_map m_flevel; + + template + void dec_keys(obj_map& map) { + typename obj_map::iterator it = map.begin(), end = map.end(); + for (; it != end; ++it) { + m.dec_ref(it->m_key); + } + } + void add_lit(app* p, app* lit); + void add_asm(app* p, expr* lit); + bool is_predicate(app* a, unsigned l); + void mk_concrete(expr_ref_vector& fmls, obj_map const& map); + public: + + pred_abs(ast_manager& m); + filter_model_converter* fmc(); + void reset(); + max_level compute_level(app* e); + void push(); + void pop(unsigned num_scopes); + void insert(app* a, max_level const& lvl); + void get_assumptions(model* mdl, expr_ref_vector& asms); + void set_expr_level(app* v, max_level const& lvl); + void set_decl_level(func_decl* v, max_level const& lvl); + void abstract_atoms(expr* fml, max_level& level, expr_ref_vector& defs); + void abstract_atoms(expr* fml, expr_ref_vector& defs); + expr_ref mk_abstract(expr* fml); + void pred2lit(expr_ref_vector& fmls); + expr_ref pred2asm(expr* fml); + void get_free_vars(expr* fml, app_ref_vector& vars); + expr_ref mk_assumption_literal(expr* a, model* mdl, max_level const& lvl, expr_ref_vector& defs); + void add_pred(app* p, app* lit); + app_ref fresh_bool(char const* name); + void display(std::ostream& out) const; + void display(std::ostream& out, expr_ref_vector const& asms) const; + void collect_statistics(statistics& st) const; + }; + + +} + +tactic * mk_qsat_tactic(ast_manager & m, params_ref const& p = params_ref()); + +tactic * mk_qe2_tactic(ast_manager & m, params_ref const& p = params_ref()); + +tactic * mk_qe_rec_tactic(ast_manager & m, params_ref const& p = params_ref()); + + +/* + ADD_TACTIC("qsat", "apply a QSAT solver.", "mk_qsat_tactic(m, p)") + + ADD_TACTIC("qe2", "apply a QSAT based quantifier elimination.", "mk_qe2_tactic(m, p)") + + ADD_TACTIC("qe_rec", "apply a QSAT based quantifier elimination recursively.", "mk_qe_rec_tactic(m, p)") + +*/ + +#endif diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 7777a6c42..27a0aa1da 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -21,6 +21,8 @@ Notes: #include"nlsat_evaluator.h" #include"nlsat_solver.h" #include"util.h" +#include"nlsat_explain.h" +#include"polynomial_cache.h" #include"rlimit.h" nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1, @@ -29,7 +31,6 @@ nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1, bool check_num_intervals = true) { nlsat::interval_set_manager & ism = s1.m(); nlsat::interval_set_ref r(ism); - std::cout << "------------------\n"; std::cout << "s1: " << s1 << "\n"; std::cout << "s2: " << s2 << "\n"; r = ism.mk_union(s1, s2); @@ -277,10 +278,12 @@ static void tst5() { nlsat::assignment as(am); small_object_allocator allocator; nlsat::interval_set_manager ism(am, allocator); - nlsat::evaluator ev(as, pm, allocator); + nlsat::evaluator ev(s, as, pm, allocator); nlsat::var x0, x1; x0 = pm.mk_var(); x1 = pm.mk_var(); + nlsat::interval_set_ref i(ism); + polynomial_ref p(pm); polynomial_ref _x0(pm), _x1(pm); _x0 = pm.mk_polynomial(x0); @@ -291,7 +294,6 @@ static void tst5() { nlsat::bool_var b = s.mk_ineq_atom(nlsat::atom::GT, 1, _p, is_even); nlsat::atom * a = s.bool_var2atom(b); SASSERT(a != 0); - nlsat::interval_set_ref i(ism); scoped_anum zero(am); am.set(zero, 0); as.set(0, zero); @@ -302,8 +304,414 @@ static void tst5() { std::cout << "2) " << i << "\n"; } + + +static void project(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) { + std::cout << "Project "; + s.display(std::cout, num, lits); + nlsat::scoped_literal_vector result(s); + ex.project(x, num, lits, result); + s.display(std::cout << "\n==>\n", result.size(), result.c_ptr()); + std::cout << "\n"; +} + +static nlsat::literal mk_gt(nlsat::solver& s, nlsat::poly* p) { + nlsat::poly * _p[1] = { p }; + bool is_even[1] = { false }; + return s.mk_ineq_literal(nlsat::atom::GT, 1, _p, is_even); +} + +static nlsat::literal mk_eq(nlsat::solver& s, nlsat::poly* p) { + nlsat::poly * _p[1] = { p }; + bool is_even[1] = { false }; + return s.mk_ineq_literal(nlsat::atom::EQ, 1, _p, is_even); +} + +static void tst6() { + params_ref ps; + reslimit rlim; + nlsat::solver s(rlim, ps); + anum_manager & am = s.am(); + nlsat::pmanager & pm = s.pm(); + nlsat::assignment as(am); + nlsat::explain& ex = s.get_explain(); + nlsat::var x0, x1, x2, a, b, c, d; + a = s.mk_var(false); + b = s.mk_var(false); + c = s.mk_var(false); + d = s.mk_var(false); + x0 = s.mk_var(false); + x1 = s.mk_var(false); + x2 = s.mk_var(false); + + polynomial_ref p1(pm), p2(pm), p3(pm), p4(pm), p5(pm); + polynomial_ref _x0(pm), _x1(pm), _x2(pm); + polynomial_ref _a(pm), _b(pm), _c(pm), _d(pm); + _x0 = pm.mk_polynomial(x0); + _x1 = pm.mk_polynomial(x1); + _x2 = pm.mk_polynomial(x2); + _a = pm.mk_polynomial(a); + _b = pm.mk_polynomial(b); + _c = pm.mk_polynomial(c); + _d = pm.mk_polynomial(d); + + p1 = (_a*(_x0^2)) + _x2 + 2; + p2 = (_b*_x1) - (2*_x2) - _x0 + 8; + nlsat::scoped_literal_vector lits(s); + lits.push_back(mk_gt(s, p1)); + lits.push_back(mk_gt(s, p2)); + lits.push_back(mk_gt(s, (_c*_x0) + _x2 + 1)); + lits.push_back(mk_gt(s, (_d*_x0) - _x1 + 5*_x2)); + + scoped_anum zero(am), one(am), two(am); + am.set(zero, 0); + am.set(one, 1); + am.set(two, 2); + as.set(0, one); + as.set(1, one); + as.set(2, two); + as.set(3, two); + as.set(4, two); + as.set(5, one); + as.set(6, one); + s.set_rvalues(as); + + + project(s, ex, x0, 2, lits.c_ptr()); + project(s, ex, x1, 3, lits.c_ptr()); + project(s, ex, x2, 3, lits.c_ptr()); + project(s, ex, x2, 2, lits.c_ptr()); + project(s, ex, x2, 4, lits.c_ptr()); + project(s, ex, x2, 3, lits.c_ptr()+1); + + +} + +static void tst7() { + params_ref ps; + reslimit rlim; + nlsat::solver s(rlim, ps); + anum_manager & am = s.am(); + nlsat::pmanager & pm = s.pm(); + nlsat::var x0, x1, x2, a, b, c, d; + a = s.mk_var(false); + b = s.mk_var(false); + c = s.mk_var(false); + d = s.mk_var(false); + x0 = s.mk_var(false); + x1 = s.mk_var(false); + x2 = s.mk_var(false); + polynomial_ref p1(pm), p2(pm), p3(pm), p4(pm), p5(pm); + polynomial_ref _x0(pm), _x1(pm), _x2(pm); + polynomial_ref _a(pm), _b(pm), _c(pm), _d(pm); + _x0 = pm.mk_polynomial(x0); + _x1 = pm.mk_polynomial(x1); + _x2 = pm.mk_polynomial(x2); + _a = pm.mk_polynomial(a); + _b = pm.mk_polynomial(b); + _c = pm.mk_polynomial(c); + _d = pm.mk_polynomial(d); + + p1 = _x0 + _x1; + p2 = _x2 - _x0; + p3 = (-1*_x0) - _x1; + + nlsat::scoped_literal_vector lits(s); + lits.push_back(mk_gt(s, p1)); + lits.push_back(mk_gt(s, p2)); + lits.push_back(mk_gt(s, p3)); + + nlsat::literal_vector litsv(lits.size(), lits.c_ptr()); + lbool res = s.check(litsv); + SASSERT(res == l_false); + for (unsigned i = 0; i < litsv.size(); ++i) { + s.display(std::cout, litsv[i]); + std::cout << " "; + } + std::cout << "\n"; + + litsv.reset(); + litsv.append(2, lits.c_ptr()); + res = s.check(litsv); + SASSERT(res == l_true); + s.display(std::cout); + s.am().display(std::cout, s.value(x0)); std::cout << "\n"; + s.am().display(std::cout, s.value(x1)); std::cout << "\n"; + s.am().display(std::cout, s.value(x2)); std::cout << "\n"; + +} + +static void tst8() { + params_ref ps; + reslimit rlim; + nlsat::solver s(rlim, ps); + anum_manager & am = s.am(); + nlsat::pmanager & pm = s.pm(); + nlsat::assignment as(am); + nlsat::explain& ex = s.get_explain(); + nlsat::var x0, x1, x2, a, b, c, d; + a = s.mk_var(false); + b = s.mk_var(false); + c = s.mk_var(false); + d = s.mk_var(false); + x0 = s.mk_var(false); + x1 = s.mk_var(false); + x2 = s.mk_var(false); + + polynomial_ref p1(pm), p2(pm), p3(pm), p4(pm), p5(pm); + polynomial_ref _x0(pm), _x1(pm), _x2(pm); + polynomial_ref _a(pm), _b(pm), _c(pm), _d(pm); + _x0 = pm.mk_polynomial(x0); + _x1 = pm.mk_polynomial(x1); + _x2 = pm.mk_polynomial(x2); + _a = pm.mk_polynomial(a); + _b = pm.mk_polynomial(b); + _c = pm.mk_polynomial(c); + _d = pm.mk_polynomial(d); + + scoped_anum zero(am), one(am), two(am), six(am); + am.set(zero, 0); + am.set(one, 1); + am.set(two, 2); + am.set(six, 6); + as.set(0, two); // a + as.set(1, one); // b + as.set(2, six); // c + as.set(3, zero); // d + as.set(4, zero); // x0 + as.set(5, zero); // x1 + as.set(6, two); // x2 + s.set_rvalues(as); + + nlsat::scoped_literal_vector lits(s); + lits.push_back(mk_eq(s, (_a*_x2*_x2) - (_b*_x2) - _c)); + project(s, ex, x2, 1, lits.c_ptr()); +} + + + +static void tst9() { + params_ref ps; + reslimit rlim; + nlsat::solver s(rlim, ps); + anum_manager & am = s.am(); + nlsat::pmanager & pm = s.pm(); + nlsat::assignment as(am); + nlsat::explain& ex = s.get_explain(); + int num_lo = 4; + int num_hi = 5; + svector los, his; + for (int i = 0; i < num_lo; ++i) { + los.push_back(s.mk_var(false)); + scoped_anum num(am); + am.set(num, - i - 1); + as.set(i, num); + } + for (int i = 0; i < num_hi; ++i) { + his.push_back(s.mk_var(false)); + scoped_anum num(am); + am.set(num, i + 1); + as.set(num_lo + i, num); + } + nlsat::var _z = s.mk_var(false); + nlsat::var _x = s.mk_var(false); + polynomial_ref x(pm), z(pm); + x = pm.mk_polynomial(_x); + scoped_anum val(am); + am.set(val, 0); + as.set(num_lo + num_hi, val); + as.set(num_lo + num_hi + 1, val); + s.set_rvalues(as); + nlsat::scoped_literal_vector lits(s); + + for (int i = 0; i < num_lo; ++i) { + polynomial_ref y(pm); + y = pm.mk_polynomial(los[i]); + lits.push_back(mk_gt(s, x - y)); + } + for (int i = 0; i < num_hi; ++i) { + polynomial_ref y(pm); + y = pm.mk_polynomial(his[i]); + lits.push_back(mk_gt(s, y - x)); + } + z = pm.mk_polynomial(_z); + lits.push_back(mk_eq(s, x - z)); + +#define TEST_ON_OFF() \ + std::cout << "Off "; \ + ex.set_signed_project(false); \ + project(s, ex, _x, lits.size()-1, lits.c_ptr()); \ + std::cout << "On "; \ + ex.set_signed_project(true); \ + project(s, ex, _x, lits.size()-1, lits.c_ptr()); \ + std::cout << "Off "; \ + ex.set_signed_project(false); \ + project(s, ex, _x, lits.size(), lits.c_ptr()); \ + std::cout << "On "; \ + ex.set_signed_project(true); \ + project(s, ex, _x, lits.size(), lits.c_ptr()) \ + + TEST_ON_OFF(); + + lits.reset(); + polynomial_ref u(pm); + u = pm.mk_polynomial(his[1]); + for (int i = 0; i < num_lo; ++i) { + polynomial_ref y(pm); + y = pm.mk_polynomial(los[i]); + lits.push_back(mk_gt(s, u*x - y)); + } + for (int i = 0; i < num_hi; ++i) { + polynomial_ref y(pm); + y = pm.mk_polynomial(his[i]); + lits.push_back(mk_gt(s, y - u*x)); + } + z = pm.mk_polynomial(_z); + lits.push_back(mk_eq(s, u*x - z)); + + TEST_ON_OFF(); + + lits.reset(); + u = pm.mk_polynomial(los[1]); + for (int i = 0; i < num_lo; ++i) { + polynomial_ref y(pm); + y = pm.mk_polynomial(los[i]); + lits.push_back(mk_gt(s, u*x - y)); + } + for (int i = 0; i < num_hi; ++i) { + polynomial_ref y(pm); + y = pm.mk_polynomial(his[i]); + lits.push_back(mk_gt(s, y - u*x)); + } + z = pm.mk_polynomial(_z); + lits.push_back(mk_eq(s, x - z)); + + TEST_ON_OFF(); +} + + +#if 0 + + +#endif + +static void test_root_literal(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, nlsat::atom::kind k, unsigned i, nlsat::poly* p) { + nlsat::scoped_literal_vector result(s); + ex.test_root_literal(k, x, 1, p, result); + nlsat::bool_var b = s.mk_root_atom(k, x, i, p); + s.display(std::cout, nlsat::literal(b, false)); + s.display(std::cout << " ==> ", result.size(), result.c_ptr()); + std::cout << "\n"; +} + +static bool satisfies_root(nlsat::solver& s, nlsat::atom::kind k, nlsat::poly* p) { + nlsat::pmanager & pm = s.pm(); + anum_manager & am = s.am(); + nlsat::assignment as(am); + s.get_rvalues(as); + polynomial_ref pr(p, pm); + switch (k) { + case nlsat::atom::ROOT_EQ: return am.eval_sign_at(pr, as) == 0; + case nlsat::atom::ROOT_LE: return am.eval_sign_at(pr, as) <= 0; + case nlsat::atom::ROOT_LT: return am.eval_sign_at(pr, as) < 0; + case nlsat::atom::ROOT_GE: return am.eval_sign_at(pr, as) >= 0; + case nlsat::atom::ROOT_GT: return am.eval_sign_at(pr, as) > 0; + default: + UNREACHABLE(); + return false; + } +} + +static void tst10() { + params_ref ps; + reslimit rlim; + nlsat::solver s(rlim, ps); + anum_manager & am = s.am(); + nlsat::pmanager & pm = s.pm(); + nlsat::assignment as(am); + nlsat::explain& ex = s.get_explain(); + nlsat::var _a = s.mk_var(false); + nlsat::var _b = s.mk_var(false); + nlsat::var _c = s.mk_var(false); + nlsat::var _x = s.mk_var(false); + + polynomial_ref x(pm), a(pm), b(pm), c(pm), p(pm); + x = pm.mk_polynomial(_x); + a = pm.mk_polynomial(_a); + b = pm.mk_polynomial(_b); + c = pm.mk_polynomial(_c); + p = a*x*x + b*x + c; + scoped_anum one(am), two(am), three(am), mone(am), mtwo(am), mthree(am), zero(am), one_a_half(am); + am.set(zero, 0); + am.set(one, 1); + am.set(two, 2); + am.set(three, 3); + am.set(mone, -1); + am.set(mtwo, -2); + am.set(mthree, -3); + rational oah(1,2); + am.set(one_a_half, oah.to_mpq()); + + + scoped_anum_vector nums(am); + nums.push_back(one); + nums.push_back(two); + nums.push_back(one_a_half); + nums.push_back(mone); + nums.push_back(three); + + // a = 1, b = -3, c = 2: + // has roots x = 2, x = 1: + // 2^2 - 3*2 + 2 = 0 + // 1 - 3 + 2 = 0 + as.set(_a, one); + as.set(_b, mthree); + as.set(_c, two); + + for (unsigned i = 0; i < nums.size(); ++i) { + as.set(_x, nums[i]); + s.set_rvalues(as); + std::cout << p << "\n"; + as.display(std::cout); + for (unsigned k = nlsat::atom::ROOT_EQ; k <= nlsat::atom::ROOT_GE; ++k) { + if (satisfies_root(s, (nlsat::atom::kind) k, p)) { + test_root_literal(s, ex, _x, (nlsat::atom::kind) k, 1, p); + } + } + } + as.set(_a, mone); + as.set(_b, three); + as.set(_c, mtwo); + for (unsigned i = 0; i < nums.size(); ++i) { + as.set(_x, nums[i]); + s.set_rvalues(as); + std::cout << p << "\n"; + as.display(std::cout); + for (unsigned k = nlsat::atom::ROOT_EQ; k <= nlsat::atom::ROOT_GE; ++k) { + if (satisfies_root(s, (nlsat::atom::kind) k, p)) { + test_root_literal(s, ex, _x, (nlsat::atom::kind) k, 1, p); + } + } + } + std::cout << "\n"; +} + void tst_nlsat() { + tst10(); + std::cout << "------------------\n"; + exit(0); + tst9(); + std::cout << "------------------\n"; + exit(0); + tst8(); + std::cout << "------------------\n"; + tst7(); + std::cout << "------------------\n"; + tst6(); + std::cout << "------------------\n"; tst5(); + std::cout << "------------------\n"; tst4(); + std::cout << "------------------\n"; tst3(); } diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index 40ecbd8c7..a1b5c2859 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -12,9 +12,9 @@ Copyright (c) 2015 Microsoft Corporation #include "reg_decl_plugins.h" #include "arith_rewriter.h" #include "ast_pp.h" -#include "qe_util.h" #include "smt_context.h" #include "expr_abstract.h" +#include "expr_safe_replace.h" static expr_ref parse_fml(ast_manager& m, char const* str) { expr_ref result(m); @@ -29,6 +29,11 @@ static expr_ref parse_fml(ast_manager& m, char const* str) { << "(declare-const t Real)\n" << "(declare-const a Real)\n" << "(declare-const b Real)\n" + << "(declare-const i Int)\n" + << "(declare-const j Int)\n" + << "(declare-const k Int)\n" + << "(declare-const l Int)\n" + << "(declare-const m Int)\n" << "(assert " << str << ")\n"; std::istringstream is(buffer.str()); VERIFY(parse_smt2_commands(ctx, is)); @@ -42,6 +47,8 @@ static char const* example2 = "(and (<= z x) (<= x 3.0) (<= (* 3.0 x) y) (<= z y static char const* example3 = "(and (<= z x) (<= x 3.0) (< (* 3.0 x) y) (<= z y))"; static char const* example4 = "(and (<= z x) (<= x 3.0) (not (>= (* 3.0 x) y)) (<= z y))"; static char const* example5 = "(and (<= y x) (<= z x) (<= x u) (<= x v) (<= x t))"; +static char const* example7 = "(and (<= x y) (<= x z) (<= u x) (< v x))"; +static char const* example8 = "(and (<= (* 2 i) k) (<= j (* 3 i)))"; static char const* example6 = "(and (<= 0 (+ x z))\ (>= y x) \ @@ -51,30 +58,175 @@ static char const* example6 = "(and (<= 0 (+ x z))\ (>= x 0.0)\ (<= x 1.0))"; +// phi[M] => result => E x . phi[x] -static void test(char const *ex) { +static void test(app* var, expr_ref& fml) { + + ast_manager& m = fml.get_manager(); smt_params params; params.m_model = true; + + symbol x_name(var->get_decl()->get_name()); + sort* x_sort = m.get_sort(var); + + expr_ref pr(m); + expr_ref_vector lits(m); + flatten_and(fml, lits); + + model_ref md; + { + smt::context ctx(m, params); + ctx.assert_expr(fml); + lbool result = ctx.check(); + if (result != l_true) return; + ctx.get_model(md); + } + VERIFY(qe::arith_project(*md, var, lits)); + pr = mk_and(lits); + + std::cout << "original: " << mk_pp(fml, m) << "\n"; + std::cout << "projected: " << mk_pp(pr, m) << "\n"; + + // projection is consistent with model. + expr_ref tmp(m); + VERIFY(md->eval(pr, tmp) && m.is_true(tmp)); + + // projection implies E x. fml + { + qe::expr_quant_elim qelim(m, params); + expr_ref result(m), efml(m); + expr* x = var; + expr_abstract(m, 0, 1, &x, fml, efml); + efml = m.mk_exists(1, &x_sort, &x_name, efml); + qelim(m.mk_true(), efml, result); + + smt::context ctx(m, params); + ctx.assert_expr(pr); + ctx.assert_expr(m.mk_not(result)); + std::cout << "exists: " << pr << " =>\n" << result << "\n"; + VERIFY(l_false == ctx.check()); + } + + std::cout << "\n"; +} + + + +static void testR(char const *ex) { ast_manager m; reg_decl_plugins(m); arith_util a(m); expr_ref fml = parse_fml(m, ex); - app_ref_vector vars(m); - expr_ref_vector lits(m); - vars.push_back(m.mk_const(symbol("x"), a.mk_real())); - flatten_and(fml, lits); + symbol x_name("x"); + sort_ref x_sort(a.mk_real(), m); + app_ref var(m.mk_const(x_name, x_sort), m); + test(var, fml); +} - smt::context ctx(m, params); - ctx.assert_expr(fml); - lbool result = ctx.check(); - SASSERT(result == l_true); - ref md; - ctx.get_model(md); - expr_ref pr = qe::arith_project(*md, vars, lits); - - std::cout << mk_pp(fml, m) << "\n"; - std::cout << mk_pp(pr, m) << "\n"; +static void testI(char const *ex) { + ast_manager m; + reg_decl_plugins(m); + arith_util a(m); + expr_ref fml = parse_fml(m, ex); + symbol x_name("i"); + sort_ref x_sort(a.mk_int(), m); + app_ref var(m.mk_const(x_name, x_sort), m); + test(var, fml); +} + +static expr_ref_vector mk_ineqs(app* x, app* y, app_ref_vector const& nums) { + ast_manager& m = nums.get_manager(); + arith_util a(m); + expr_ref_vector result(m); + for (unsigned i = 0; i < nums.size(); ++i) { + expr_ref ax(a.mk_mul(nums[i], x), m); + result.push_back(a.mk_le(ax, y)); + result.push_back(m.mk_not(a.mk_ge(ax, y))); + result.push_back(m.mk_not(a.mk_gt(y, ax))); + result.push_back(a.mk_lt(y, ax)); + } + return result; +} + +static app_ref generate_ineqs(ast_manager& m, sort* s, vector& cs, bool mods_too) { + arith_util a(m); + app_ref_vector vars(m), nums(m); + vars.push_back(m.mk_const(symbol("x"), s)); + vars.push_back(m.mk_const(symbol("y"), s)); + vars.push_back(m.mk_const(symbol("z"), s)); + vars.push_back(m.mk_const(symbol("u"), s)); + vars.push_back(m.mk_const(symbol("v"), s)); + vars.push_back(m.mk_const(symbol("w"), s)); + nums.push_back(a.mk_numeral(rational(1), s)); + nums.push_back(a.mk_numeral(rational(2), s)); + nums.push_back(a.mk_numeral(rational(3), s)); + app* x = vars[0].get(); + app* y = vars[1].get(); + app* z = vars[2].get(); + // + // ax <= by, ax < by, not (ax >= by), not (ax > by) + // + cs.push_back(mk_ineqs(x, vars[1].get(), nums)); + cs.push_back(mk_ineqs(x, vars[2].get(), nums)); + cs.push_back(mk_ineqs(x, vars[3].get(), nums)); + cs.push_back(mk_ineqs(x, vars[4].get(), nums)); + cs.push_back(mk_ineqs(x, vars[5].get(), nums)); + + if (mods_too) { + expr_ref_vector mods(m); + expr_ref zero(a.mk_numeral(rational(0), s), m); + mods.push_back(m.mk_true()); + for (unsigned j = 0; j < nums.size(); ++j) { + mods.push_back(m.mk_eq(a.mk_mod(a.mk_add(a.mk_mul(nums[j].get(),x), y), nums[1].get()), zero)); + } + cs.push_back(mods); + mods.resize(1); + for (unsigned j = 0; j < nums.size(); ++j) { + mods.push_back(m.mk_eq(a.mk_mod(a.mk_add(a.mk_mul(nums[j].get(),x), y), nums[2].get()), zero)); + } + cs.push_back(mods); + } + return app_ref(x, m); +} + + +static void test_c(app* x, expr_ref_vector const& c) { + ast_manager& m = c.get_manager(); + expr_ref fml(m); + fml = m.mk_and(c.size(), c.c_ptr()); + test(x, fml); +} + +static void test_cs(app* x, expr_ref_vector& c, vector const& cs) { + if (c.size() == cs.size()) { + test_c(x, c); + return; + } + expr_ref_vector const& c1 = cs[c.size()]; + for (unsigned i = 0; i < c1.size(); ++i) { + c.push_back(c1[i]); + test_cs(x, c, cs); + c.pop_back(); + } +} + + +static void test_ineqs(ast_manager& m, sort* s, bool mods_too) { + vector ineqs; + app_ref x = generate_ineqs(m, s, ineqs, mods_too); + expr_ref_vector cs(m); + test_cs(x, cs, ineqs); +} + +static void test_ineqs() { + ast_manager m; + reg_decl_plugins(m); + arith_util a(m); + sort* s_int = a.mk_int(); + sort* s_real = a.mk_real(); + test_ineqs(m, s_int, true); + test_ineqs(m, s_real, false); } static void test2(char const *ex) { @@ -102,7 +254,7 @@ static void test2(char const *ex) { std::cout << mk_pp(fml, m) << "\n"; - expr_ref pr2(m), fml2(m); + expr_ref pr1(m), pr2(m), fml2(m); expr_ref_vector bound(m); ptr_vector sorts; svector names; @@ -114,7 +266,10 @@ static void test2(char const *ex) { expr_abstract(m, 0, bound.size(), bound.c_ptr(), fml, fml2); fml2 = m.mk_exists(bound.size(), sorts.c_ptr(), names.c_ptr(), fml2); qe::expr_quant_elim qe(m, params); - expr_ref pr1 = qe::arith_project(*md, vars, lits); + for (unsigned i = 0; i < vars.size(); ++i) { + VERIFY(qe::arith_project(*md, vars[i].get(), lits)); + } + pr1 = mk_and(lits); qe(m.mk_true(), fml2, pr2); std::cout << mk_pp(pr1, m) << "\n"; std::cout << mk_pp(pr2, m) << "\n"; @@ -131,11 +286,17 @@ static void test2(char const *ex) { } void tst_qe_arith() { +// enable_trace("qe"); + testI(example8); + testR(example7); + test_ineqs(); + return; + testR(example1); + testR(example2); + testR(example3); + testR(example4); + testR(example5); + return; test2(example6); return; - test(example1); - test(example2); - test(example3); - test(example4); - test(example5); }