From 3afa409abbe7172dcecdd419977c70614c301ca8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Feb 2014 15:44:47 -0800 Subject: [PATCH] snapshot adding simplex Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- src/smt/params/smt_params_helper.pyg | 1 + src/smt/params/theory_pb_params.cpp | 1 + src/smt/params/theory_pb_params.h | 4 +- src/smt/theory_pb.cpp | 68 +++++++++++++++++++++++++++- src/smt/theory_pb.h | 43 ++++++++++++++++++ src/tactic/arith/elim01_tactic.cpp | 2 +- 7 files changed, 117 insertions(+), 4 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 952c22c20..bf026c4d5 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -49,7 +49,7 @@ def init_project_def(): add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params') add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model') add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', - 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util']) + 'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util']) add_lib('user_plugin', ['smt'], 'smt/user_plugin') add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv') add_lib('fuzzing', ['ast'], 'test/fuzzing') diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index cc1527b9c..cf9b8f57e 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -46,6 +46,7 @@ def_module_params(module_name='smt', ('pb.conflict_frequency', UINT, 0, 'conflict frequency for Pseudo-Boolean theory'), ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'), ('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'), + ('pb.enable_simplex', BOOL, False, 'enable simplex to check rational feasibility'), ('array.weak', BOOL, False, 'weak array theory'), ('array.extensional', BOOL, True, 'extensional array theory') )) diff --git a/src/smt/params/theory_pb_params.cpp b/src/smt/params/theory_pb_params.cpp index b82d5b460..6d980fe5d 100644 --- a/src/smt/params/theory_pb_params.cpp +++ b/src/smt/params/theory_pb_params.cpp @@ -24,4 +24,5 @@ void theory_pb_params::updt_params(params_ref const & _p) { m_pb_conflict_frequency = p.pb_conflict_frequency(); m_pb_learn_complements = p.pb_learn_complements(); m_pb_enable_compilation = p.pb_enable_compilation(); + m_pb_enable_simplex = p.pb_enable_simplex(); } diff --git a/src/smt/params/theory_pb_params.h b/src/smt/params/theory_pb_params.h index 30778caad..03deb8930 100644 --- a/src/smt/params/theory_pb_params.h +++ b/src/smt/params/theory_pb_params.h @@ -26,10 +26,12 @@ struct theory_pb_params { unsigned m_pb_conflict_frequency; bool m_pb_learn_complements; bool m_pb_enable_compilation; + bool m_pb_enable_simplex; theory_pb_params(params_ref const & p = params_ref()): m_pb_conflict_frequency(0), m_pb_learn_complements(true), - m_pb_enable_compilation(true) + m_pb_enable_compilation(true), + m_pb_enable_simplex(false) {} void updt_params(params_ref const & p); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index ebb5aee10..22f872978 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -61,6 +61,20 @@ namespace smt { }; }; + unsigned theory_pb::ineq::get_hash() const { + return get_composite_hash(m_args, m_args.size()); + } + + bool theory_pb::ineq::operator==(ineq const& other) const { + if (size() != other.size()) return false; + for (unsigned i = 0; i < size(); ++i) { + if (lit(i) != other.lit(i)) return false; + if (coeff(i) != other.coeff(i)) return false; + } + return true; + } + + void theory_pb::ineq::negate() { SASSERT(!m_is_eq); m_lit.neg(); @@ -101,6 +115,16 @@ namespace smt { util.prune(m_args, m_k, m_is_eq); } + void theory_pb::ineq::remove_negations() { + for (unsigned i = 0; i < size(); ++i) { + if (lit(i).sign()) { + m_args[i].first.neg(); + m_args[i].second.neg(); + m_k += coeff(i); + } + } + } + lbool theory_pb::ineq::normalize() { pb_lit_rewriter_util pbu; pb_rewriter_util util(pbu); @@ -152,9 +176,10 @@ namespace smt { m_lemma(null_literal, false), m_max_compiled_coeff(rational(8)) { - m_learn_complements = p.m_pb_learn_complements; + m_learn_complements = p.m_pb_learn_complements; m_conflict_frequency = p.m_pb_conflict_frequency; m_enable_compilation = p.m_pb_enable_compilation; + m_enable_simplex = p.m_pb_enable_simplex; } theory_pb::~theory_pb() { @@ -273,6 +298,47 @@ namespace smt { m_ineqs.insert(abv, c); m_ineqs_trail.push_back(abv); + if (m_enable_simplex) { + // + // TBD: using abv as slack identity doesn't quite + // work if psuedo-Booleans are used + // in a nested way. So assume + // + + // + // TBD: track and delete rows. + // + ineq rep(*c); + rep.remove_negations(); // normalize representative + numeral k = rep.k(); + theory_var slack; + bool_var abv2; + row r; + if (m_ineq_rep.find(rep, abv2)) { + slack = abv2; + r = m_ineq_row_info.find(abv2).m_row; + TRACE("pb", tout << "Found: " << abv << " |-> " << slack << " " << m_ineq_row_info.find(abv2).m_bound << " vs. " << k << "\n";); + } + else { + m_ineq_rep.insert(rep, abv); + svector vars; + unsynch_mpz_manager mgr; + scoped_mpz_vector coeffs(mgr); + for (unsigned i = 0; i < rep.size(); ++i) { + unsigned v = rep.lit(i).var(); + std::cout << v << "\n"; + m_simplex.ensure_var(v); + vars.push_back(v); + coeffs.push_back(rep.coeff(i).to_mpq().numerator()); + } + slack = abv; + m_simplex.ensure_var(abv); + r = m_simplex.add_row(vars.size(), slack, vars.c_ptr(), coeffs.c_ptr()); + TRACE("pb", tout << "New row: " << abv << " " << k << "\n";); + } + m_ineq_row_info.insert(abv, row_info(slack, k, rep, r)); + } + TRACE("pb", display(tout, *c);); return true; diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 922ab76f8..5b1adbd25 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -24,6 +24,7 @@ Notes: #include "pb_decl_plugin.h" #include "smt_clause.h" #include "theory_pb_params.h" +#include "simplex.h" namespace smt { class theory_pb : public theory { @@ -37,6 +38,8 @@ namespace smt { class negate_ineq; typedef rational numeral; typedef vector > arg_t; + typedef simplex::simplex simplex; + typedef simplex::row row; struct stats { unsigned m_num_conflicts; @@ -69,6 +72,8 @@ namespace smt { unsigned m_compilation_threshold; lbool m_compiled; + ineq(): m_lit(null_literal), m_is_eq(false) {} + ineq(literal l, bool is_eq) : m_lit(l), m_is_eq(is_eq) { reset(); } @@ -111,12 +116,46 @@ namespace smt { void prune(); + void remove_negations(); + bool well_formed() const; app_ref to_expr(context& ctx, ast_manager& m); bool is_eq() const { return m_is_eq; } bool is_ge() const { return !m_is_eq; } + + unsigned get_hash() const; + bool operator==(ineq const& other) const; + + struct hash { + unsigned operator()(ineq const& i) const { return i.get_hash(); } + }; + struct eq { + bool operator()(ineq const& a, ineq const& b) const { + return a == b; + } + }; + struct child_hash { + unsigned operator()(arg_t const& args, unsigned idx) const { + return args[idx].first.hash() ^ args[idx].second.hash(); + } + }; + struct kind_hash { + unsigned operator()(arg_t const& args) const { + return args.size(); + } + }; + }; + + struct row_info { + unsigned m_slack; // slack variable in simplex tableau + numeral m_bound; // bound + ineq m_rep; // representative + row m_row; + row_info(theory_var slack, numeral const& b, ineq const& r, row const& ro): + m_slack(slack), m_bound(b), m_rep(r), m_row(ro) {} + row_info(): m_slack(0) {} }; typedef ptr_vector watch_list; @@ -125,6 +164,9 @@ namespace smt { u_map m_lwatch; // per literal. u_map m_vwatch; // per variable. u_map m_ineqs; // per inequality. + map m_ineq_rep; // Simplex: representative inequality + u_map m_ineq_row_info; // Simplex: row information per variable. + simplex m_simplex; // Simplex unsigned_vector m_ineqs_trail; unsigned_vector m_ineqs_lim; literal_vector m_literals; // temporary vector @@ -134,6 +176,7 @@ namespace smt { unsigned m_conflict_frequency; bool m_learn_complements; bool m_enable_compilation; + bool m_enable_simplex; rational m_max_compiled_coeff; // internalize_atom: diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index 6a2c2cb2a..e6c345734 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -127,7 +127,7 @@ public: elim01_tactic(ast_manager & _m, params_ref const & p): m(_m), a(m), - m_max_hi_default(1), + m_max_hi_default(8), m_max_hi(rational(m_max_hi_default)) { }