From b18dc7d05238ec3afa7d8eac1e7b4691321b09c2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 May 2017 17:24:36 -0700 Subject: [PATCH] adding nra Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/params/theory_arith_params.h | 13 +++++----- src/smt/smt_setup.cpp | 5 ++-- src/smt/theory_lra.cpp | 22 +++++++++++++---- src/util/lp/nra_solver.cpp | 36 +++++++++++++++++++++------- src/util/lp/nra_solver.h | 5 ++++ 6 files changed, 61 insertions(+), 22 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 6c2ff4962..d2addb7dc 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -36,7 +36,7 @@ def_module_params(module_name='smt', ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), - ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination'), + ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'), ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'), diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 943bd711e..e71c0adad 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -23,12 +23,13 @@ Revision History: #include"params.h" enum arith_solver_id { - AS_NO_ARITH, - AS_DIFF_LOGIC, - AS_ARITH, - AS_DENSE_DIFF_LOGIC, - AS_UTVPI, - AS_OPTINF + AS_NO_ARITH, // 0 + AS_DIFF_LOGIC, // 1 + AS_ARITH, // 2 + AS_DENSE_DIFF_LOGIC, // 3 + AS_UTVPI, // 4 + AS_OPTINF, // 5 + AS_LRA // 6 }; enum bound_prop_mode { diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 4dd1e2510..9646bce2b 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -724,8 +724,6 @@ namespace smt { } void setup::setup_r_arith() { - // to disable theory lra - // m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); } @@ -789,6 +787,9 @@ namespace smt { case AS_OPTINF: m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params)); break; + case AS_LRA: + setup_r_arith(); + break; default: if (m_params.m_arith_int_only && int_only) m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index cd663f354..b0345c52f 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -366,6 +366,14 @@ namespace smt { terms[index] = n1; st.terms_to_internalize().push_back(n2); } + else if (a.is_mul(n)) { + theory_var v; + internalize_mul(to_app(n), v, r); + coeffs[index] *= r; + coeffs[vars.size()] = coeffs[index]; + vars.push_back(v); + ++index; + } else if (a.is_numeral(n, r)) { coeff += coeffs[index]*r; ++index; @@ -415,10 +423,13 @@ namespace smt { } } - void internalize_mul(app* t) { + void internalize_mul(app* t, theory_var& v, rational& r) { SASSERT(a.is_mul(t)); + internalize_args(t); mk_enode(t); - theory_var v = mk_var(t); + r = rational::one(); + rational r1; + v = mk_var(t); svector vars; ptr_vector todo; todo.push_back(t); @@ -430,6 +441,9 @@ namespace smt { todo.push_back(n1); todo.push_back(n2); } + else if (a.is_numeral(n, r1)) { + r *= r1; + } else { if (!ctx().e_internalized(n)) { ctx().internalize(n, false); @@ -437,7 +451,7 @@ namespace smt { vars.push_back(get_var_index(mk_var(n))); } } - // m_solver->add_monomial(get_var_index(v), vars); + m_solver->add_monomial(get_var_index(v), vars); } enode * mk_enode(app * n) { @@ -1245,7 +1259,7 @@ namespace smt { lbool check_nra() { if (m.canceled()) return l_undef; - return l_true; + // return l_true; // TBD: switch (m_solver->check_nra(m_variable_values, m_explanation)) { case lean::final_check_status::DONE: diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp index 2308b9c45..5157be92c 100644 --- a/src/util/lp/nra_solver.cpp +++ b/src/util/lp/nra_solver.cpp @@ -21,8 +21,8 @@ namespace nra { u_map m_lp2nl; // map from lar_solver variables to nlsat::solver variables struct mon_eq { - mon_eq(lean::var_index v, svector const& vs): - m_v(v), m_vs(vs) {} + mon_eq(lean::var_index v, unsigned sz, lean::var_index const* vs): + m_v(v), m_vs(sz, vs) {} lean::var_index m_v; svector m_vs; }; @@ -44,14 +44,14 @@ namespace nra { } switch (check_nlsat(m, ex)) { case l_undef: return lean::final_check_status::GIVEUP; - case l_true: lean::final_check_status::DONE; - case l_false: lean::final_check_status::UNSAT; + case l_true: return lean::final_check_status::DONE; + case l_false: return lean::final_check_status::UNSAT; } return lean::final_check_status::DONE; } void add(lean::var_index v, unsigned sz, lean::var_index const* vs) { - m_monomials.push_back(mon_eq(v, svector(sz, vs))); + m_monomials.push_back(mon_eq(v, sz, vs)); } void push() { @@ -60,7 +60,6 @@ namespace nra { void pop(unsigned n) { if (n == 0) return; - SASSERT(n < m_lim.size()); m_monomials.shrink(m_lim[m_lim.size() - n]); m_lim.shrink(m_lim.size() - n); } @@ -112,7 +111,9 @@ namespace nra { } // TBD: add variable bounds? + lbool r = solver.check(); + TRACE("arith", solver.display(tout << r << "\n");); switch (r) { case l_true: { nlsat::anum_manager& am = solver.am(); @@ -143,6 +144,7 @@ namespace nra { for (auto c : core) { unsigned idx = static_cast(static_cast(c) - this); ex.push_back(std::pair(rational(1), idx)); + TRACE("arith", tout << "ex: " << idx << "\n";); } break; } @@ -172,12 +174,12 @@ namespace nra { } void add_constraint(nlsat::solver& solver, unsigned idx) { - lean::lar_base_constraint const& c = s.get_constraint(idx); - polynomial::manager& pm = solver.pm(); + auto& c = s.get_constraint(idx); + auto& pm = solver.pm(); auto k = c.m_kind; auto rhs = c.m_right_side; auto lhs = c.get_left_side_coefficients(); - unsigned sz = lhs.size(); + auto sz = lhs.size(); svector vars; rational den = denominator(rhs); for (auto kv : lhs) { @@ -229,6 +231,17 @@ namespace nra { return r; } + std::ostream& display(std::ostream& out) const { + for (auto m : m_monomials) { + out << "v" << m.m_v << " = "; + for (auto v : m.m_vs) { + out << "v" << v << " "; + } + out << "\n"; + } + return out; + } + }; solver::solver(lean::lar_solver& s) { @@ -254,4 +267,9 @@ namespace nra { void solver::pop(unsigned n) { m_imp->pop(n); } + + std::ostream& solver::display(std::ostream& out) const { + return m_imp->display(out); + } + } diff --git a/src/util/lp/nra_solver.h b/src/util/lp/nra_solver.h index 87820728a..2fdf91729 100644 --- a/src/util/lp/nra_solver.h +++ b/src/util/lp/nra_solver.h @@ -42,5 +42,10 @@ namespace nra { void push(); void pop(unsigned n); + + /* + \brief display state + */ + std::ostream& display(std::ostream& out) const; }; }