diff --git a/.gitignore b/.gitignore index 17465d9ae..936f977aa 100644 --- a/.gitignore +++ b/.gitignore @@ -95,3 +95,4 @@ CMakeSettings.json *.swp .DS_Store dbg/** +*.wsp diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 60cbdcc56..e9f54be05 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -32,9 +32,11 @@ def init_project_def(): add_lib('lp', ['util', 'nlsat', 'grobner', 'interval', 'smt_params'], 'math/lp') add_lib('rewriter', ['ast', 'polynomial', 'automata', 'params'], 'ast/rewriter') add_lib('macros', ['rewriter'], 'ast/macros') - add_lib('normal_forms', ['rewriter'], 'ast/normal_forms') add_lib('model', ['rewriter', 'macros']) - add_lib('tactic', ['ast', 'model']) + add_lib('converters', ['model'], 'ast/converters') + add_lib('simplifiers', ['euf', 'rewriter', 'converters'], 'ast/simplifiers') + add_lib('normal_forms', ['rewriter'], 'ast/normal_forms') + add_lib('tactic', ['ast', 'model', 'simplifiers']) add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution') add_lib('parser_util', ['ast'], 'parsers/util') add_lib('proofs', ['rewriter', 'util'], 'ast/proofs') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b96638944..fd4fa04b5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -49,9 +49,11 @@ add_subdirectory(ast/rewriter) add_subdirectory(ast/normal_forms) add_subdirectory(ast/macros) add_subdirectory(model) +add_subdirectory(ast/euf) +add_subdirectory(ast/converters) +add_subdirectory(ast/simplifiers) add_subdirectory(tactic) add_subdirectory(ast/substitution) -add_subdirectory(ast/euf) add_subdirectory(smt/params) add_subdirectory(parsers/util) add_subdirectory(math/grobner) diff --git a/src/ackermannization/ackermannize_bv_model_converter.h b/src/ackermannization/ackermannize_bv_model_converter.h index 59dff3ed2..759ec3c13 100644 --- a/src/ackermannization/ackermannize_bv_model_converter.h +++ b/src/ackermannization/ackermannize_bv_model_converter.h @@ -16,7 +16,7 @@ --*/ #pragma once -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "ackermannization/ackr_info.h" model_converter * mk_ackermannize_bv_model_converter(ast_manager & m, const ackr_info_ref& info); diff --git a/src/ackermannization/ackr_model_converter.h b/src/ackermannization/ackr_model_converter.h index 8fc8edecc..df134f227 100644 --- a/src/ackermannization/ackr_model_converter.h +++ b/src/ackermannization/ackr_model_converter.h @@ -15,7 +15,7 @@ Revision History: --*/ #pragma once -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "ackermannization/ackr_info.h" model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info, model_ref & abstr_model); diff --git a/src/ackermannization/lackr_model_converter_lazy.h b/src/ackermannization/lackr_model_converter_lazy.h index 9a713753b..a16722356 100644 --- a/src/ackermannization/lackr_model_converter_lazy.h +++ b/src/ackermannization/lackr_model_converter_lazy.h @@ -16,7 +16,7 @@ --*/ #pragma once -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "ackermannization/ackr_info.h" model_converter * mk_lackr_model_converter_lazy(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model); diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index df3059d4b..a8f4d74b7 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -137,7 +137,7 @@ extern "C" { ast_manager& m = mk_c(c)->m(); recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin(); if (!p.has_def(d)) { - std::string msg = "function " + mk_pp(d, m) + " needs to be defined using rec_func_decl"; + std::string msg = "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl"; SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str()); return; } @@ -158,6 +158,12 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return; } + if (!pd.get_def()->get_cases().empty()) { + std::string msg = "function " + mk_pp(d, m) + " has already been given a definition"; + SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str()); + return; + } + if (abs_body->get_sort() != d->get_range()) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return; diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 781996662..0c77867d4 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -453,6 +453,9 @@ public: app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_MUL, arg1, arg2); } app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_MUL, arg1, arg2, arg3); } app * mk_mul(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(arith_family_id, OP_MUL, num_args, args); } + app * mk_mul(ptr_buffer const& args) const { return mk_mul(args.size(), args.data()); } + app * mk_mul(ptr_vector const& args) const { return mk_mul(args.size(), args.data()); } + app * mk_mul(expr_ref_vector const& args) const { return mk_mul(args.size(), args.data()); } app * mk_uminus(expr * arg) const { return m_manager.mk_app(arith_family_id, OP_UMINUS, arg); } app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_DIV, arg1, arg2); } app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_IDIV, arg1, arg2); } diff --git a/src/ast/ast.h b/src/ast/ast.h index ce9de96d4..7514055c5 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1387,6 +1387,7 @@ inline bool is_app_of(expr const * n, family_id fid, decl_kind k) { return n->ge inline bool is_sort_of(sort const * s, family_id fid, decl_kind k) { return s->is_sort_of(fid, k); } inline bool is_uninterp_const(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id; } inline bool is_uninterp(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_family_id() == null_family_id; } +inline bool is_uninterp(func_decl const * n) { return n->get_family_id() == null_family_id; } inline bool is_decl_of(func_decl const * d, family_id fid, decl_kind k) { return d->get_family_id() == fid && d->get_decl_kind() == k; } inline bool is_ground(expr const * n) { return is_app(n) && to_app(n)->is_ground(); } inline bool is_non_ground(expr const * n) { return ( ! is_ground(n)); } diff --git a/src/ast/converters/CMakeLists.txt b/src/ast/converters/CMakeLists.txt new file mode 100644 index 000000000..52895f064 --- /dev/null +++ b/src/ast/converters/CMakeLists.txt @@ -0,0 +1,11 @@ +z3_add_component(converters + SOURCES + equiv_proof_converter.cpp + generic_model_converter.cpp + horn_subsume_model_converter.cpp + model_converter.cpp + proof_converter.cpp + replace_proof_converter.cpp + COMPONENT_DEPENDENCIES + model +) diff --git a/src/tactic/converter.h b/src/ast/converters/converter.h similarity index 100% rename from src/tactic/converter.h rename to src/ast/converters/converter.h diff --git a/src/tactic/equiv_proof_converter.cpp b/src/ast/converters/equiv_proof_converter.cpp similarity index 93% rename from src/tactic/equiv_proof_converter.cpp rename to src/ast/converters/equiv_proof_converter.cpp index 8bec082d3..d0ed94d8b 100644 --- a/src/tactic/equiv_proof_converter.cpp +++ b/src/ast/converters/equiv_proof_converter.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#include "tactic/equiv_proof_converter.h" +#include "ast/converters/equiv_proof_converter.h" #include "ast/ast_pp.h" #include "ast/scoped_proof.h" diff --git a/src/tactic/equiv_proof_converter.h b/src/ast/converters/equiv_proof_converter.h similarity index 95% rename from src/tactic/equiv_proof_converter.h rename to src/ast/converters/equiv_proof_converter.h index 87a8f7131..7f98d1e0c 100644 --- a/src/tactic/equiv_proof_converter.h +++ b/src/ast/converters/equiv_proof_converter.h @@ -23,7 +23,7 @@ Revision History: #pragma once -#include "tactic/replace_proof_converter.h" +#include "ast/converters/replace_proof_converter.h" class equiv_proof_converter : public proof_converter { ast_manager& m; diff --git a/src/tactic/generic_model_converter.cpp b/src/ast/converters/generic_model_converter.cpp similarity index 99% rename from src/tactic/generic_model_converter.cpp rename to src/ast/converters/generic_model_converter.cpp index 2886eb6ab..f805e169b 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/ast/converters/generic_model_converter.cpp @@ -24,7 +24,7 @@ Notes: #include "ast/occurs.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/rewriter/th_rewriter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "model/model_v2_pp.h" #include "model/model_evaluator.h" diff --git a/src/tactic/generic_model_converter.h b/src/ast/converters/generic_model_converter.h similarity index 97% rename from src/tactic/generic_model_converter.h rename to src/ast/converters/generic_model_converter.h index e809fe734..c20bfebb3 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/ast/converters/generic_model_converter.h @@ -19,7 +19,7 @@ Notes: --*/ #pragma once -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" class generic_model_converter : public model_converter { enum instruction { HIDE, ADD }; diff --git a/src/tactic/horn_subsume_model_converter.cpp b/src/ast/converters/horn_subsume_model_converter.cpp similarity index 99% rename from src/tactic/horn_subsume_model_converter.cpp rename to src/ast/converters/horn_subsume_model_converter.cpp index 979359a46..a0c8b341e 100644 --- a/src/tactic/horn_subsume_model_converter.cpp +++ b/src/ast/converters/horn_subsume_model_converter.cpp @@ -18,14 +18,14 @@ Revision History: --*/ -#include "tactic/horn_subsume_model_converter.h" -#include "ast/rewriter/var_subst.h" #include "ast/ast_pp.h" -#include "model/model_smt2_pp.h" -#include "ast/rewriter/bool_rewriter.h" -#include "ast/rewriter/th_rewriter.h" #include "ast/for_each_expr.h" #include "ast/well_sorted.h" +#include "ast/rewriter/var_subst.h" +#include "ast/rewriter/bool_rewriter.h" +#include "ast/rewriter/th_rewriter.h" +#include "model/model_smt2_pp.h" +#include "ast/converters/horn_subsume_model_converter.h" void horn_subsume_model_converter::insert(app* head, expr* body) { m_delay_head.push_back(head); diff --git a/src/tactic/horn_subsume_model_converter.h b/src/ast/converters/horn_subsume_model_converter.h similarity index 97% rename from src/tactic/horn_subsume_model_converter.h rename to src/ast/converters/horn_subsume_model_converter.h index 41e59070e..2576ad1f9 100644 --- a/src/tactic/horn_subsume_model_converter.h +++ b/src/ast/converters/horn_subsume_model_converter.h @@ -34,7 +34,7 @@ Subsumption transformation (remove Horn clause): #pragma once -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "ast/rewriter/th_rewriter.h" class horn_subsume_model_converter : public model_converter { diff --git a/src/tactic/model_converter.cpp b/src/ast/converters/model_converter.cpp similarity index 99% rename from src/tactic/model_converter.cpp rename to src/ast/converters/model_converter.cpp index 5c08da76f..bba18ecd6 100644 --- a/src/tactic/model_converter.cpp +++ b/src/ast/converters/model_converter.cpp @@ -16,7 +16,7 @@ Author: Notes: --*/ -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "model/model_v2_pp.h" #include "ast/ast_smt2_pp.h" diff --git a/src/tactic/model_converter.h b/src/ast/converters/model_converter.h similarity index 98% rename from src/tactic/model_converter.h rename to src/ast/converters/model_converter.h index 377ecce67..335e0d276 100644 --- a/src/tactic/model_converter.h +++ b/src/ast/converters/model_converter.h @@ -57,7 +57,7 @@ Notes: #include "util/ref.h" #include "ast/ast_pp_util.h" #include "model/model.h" -#include "tactic/converter.h" +#include "ast/converters/converter.h" class labels_vec : public svector {}; class smt2_pp_environment; diff --git a/src/tactic/proof_converter.cpp b/src/ast/converters/proof_converter.cpp similarity index 68% rename from src/tactic/proof_converter.cpp rename to src/ast/converters/proof_converter.cpp index d1905b383..88358b7c3 100644 --- a/src/tactic/proof_converter.cpp +++ b/src/ast/converters/proof_converter.cpp @@ -16,8 +16,7 @@ Author: Notes: --*/ -#include "tactic/proof_converter.h" -#include "tactic/goal.h" +#include "ast/converters/proof_converter.h" #include "ast/ast_smt2_pp.h" class concat_proof_converter : public concat_converter { @@ -46,41 +45,6 @@ proof_converter * concat(proof_converter * pc1, proof_converter * pc2) { return alloc(concat_proof_converter, pc1, pc2); } -class subgoal_proof_converter : public proof_converter { - proof_converter_ref m_pc; - goal_ref_buffer m_goals; -public: - subgoal_proof_converter(proof_converter* pc, unsigned n, goal * const* goals): - m_pc(pc) - { - for (unsigned i = 0; i < n; ++i) m_goals.push_back(goals[i]); - } - - proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { - // ignore the proofs from the arguments, instead obtain the proofs fromt he subgoals. - SASSERT(num_source == 0); - proof_converter_ref_buffer pc_buffer; - for (goal_ref g : m_goals) { - pc_buffer.push_back(g->pc()); - - } - return apply(m, m_pc, pc_buffer); - } - - proof_converter* translate(ast_translation& tr) override { - proof_converter_ref pc1 = m_pc->translate(tr); - goal_ref_buffer goals; - for (goal_ref g : m_goals) goals.push_back(g->translate(tr)); - return alloc(subgoal_proof_converter, pc1.get(), goals.size(), goals.data()); - } - - void display(std::ostream& out) override {} - -}; - -proof_converter * concat(proof_converter *pc, unsigned n, goal* const* goals) { - return alloc(subgoal_proof_converter, pc, n, goals); -} class proof2pc : public proof_converter { proof_ref m_pr; diff --git a/src/tactic/proof_converter.h b/src/ast/converters/proof_converter.h similarity index 78% rename from src/tactic/proof_converter.h rename to src/ast/converters/proof_converter.h index 88152ce5b..d977f2563 100644 --- a/src/tactic/proof_converter.h +++ b/src/ast/converters/proof_converter.h @@ -20,8 +20,7 @@ Notes: #include "ast/ast.h" #include "util/ref.h" -#include "tactic/converter.h" -class goal; +#include "ast/converters/converter.h" class proof_converter : public converter { public: @@ -36,12 +35,6 @@ typedef sref_buffer proof_converter_ref_buffer; proof_converter * concat(proof_converter * pc1, proof_converter * pc2); -/** - \brief create a proof converter that takes a set of subgoals and converts their proofs to a proof of - the goal they were derived from. - */ -proof_converter * concat(proof_converter *pc1, unsigned n, goal* const* goals); - proof_converter * proof2proof_converter(ast_manager & m, proof * pr); void apply(ast_manager & m, proof_converter * pc, proof_ref & pr); diff --git a/src/tactic/replace_proof_converter.cpp b/src/ast/converters/replace_proof_converter.cpp similarity index 97% rename from src/tactic/replace_proof_converter.cpp rename to src/ast/converters/replace_proof_converter.cpp index 4a98110eb..81fe251a3 100644 --- a/src/tactic/replace_proof_converter.cpp +++ b/src/ast/converters/replace_proof_converter.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#include "tactic/replace_proof_converter.h" +#include "ast/converters/replace_proof_converter.h" #include "ast/expr_functors.h" #include "ast/ast_pp.h" #include "ast/for_each_expr.h" diff --git a/src/tactic/replace_proof_converter.h b/src/ast/converters/replace_proof_converter.h similarity index 95% rename from src/tactic/replace_proof_converter.h rename to src/ast/converters/replace_proof_converter.h index 37bbf55b3..6a877bc58 100644 --- a/src/tactic/replace_proof_converter.h +++ b/src/ast/converters/replace_proof_converter.h @@ -22,7 +22,7 @@ Revision History: #pragma once -#include "tactic/proof_converter.h" +#include "ast/converters/proof_converter.h" class replace_proof_converter : public proof_converter { ast_manager& m; diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 6034d8428..c8605b297 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -904,6 +904,10 @@ template void euf::egraph::explain_todo(ptr_vector& justifications, cc_j template void euf::egraph::explain_eq(ptr_vector& justifications, cc_justification*, enode* a, enode* b); template unsigned euf::egraph::explain_diseq(ptr_vector& justifications, cc_justification*, enode* a, enode* b); +template void euf::egraph::explain(ptr_vector& justifications, cc_justification*); +template void euf::egraph::explain_todo(ptr_vector& justifications, cc_justification*); +template void euf::egraph::explain_eq(ptr_vector& justifications, cc_justification*, enode* a, enode* b); +template unsigned euf::egraph::explain_diseq(ptr_vector& justifications, cc_justification*, enode* a, enode* b); #if 0 diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp index cfc99e4a0..e007297ef 100644 --- a/src/ast/euf/euf_etable.cpp +++ b/src/ast/euf/euf_etable.cpp @@ -201,8 +201,6 @@ namespace euf { enode_bool_pair etable::insert(enode * n) { // it doesn't make sense to insert a constant. SASSERT(n->num_args() > 0); - SASSERT(!m_manager.is_and(n->get_expr())); - SASSERT(!m_manager.is_or(n->get_expr())); enode * n_prime; void * t = get_table(n); switch (static_cast(GET_TAG(t))) { diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index bbd1c0e8e..6d4b1b618 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -45,6 +45,7 @@ public: unsigned size() const { return m_subst.size(); } void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr); void erase(expr * s); + expr* find(expr* s) { proof* pr; expr* def; VERIFY(find(s, def, pr)); SASSERT(def); return def; } bool find(expr * s, expr * & def, proof * & def_pr); bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep); bool contains(expr * s); diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h index 786061065..a599ff5a1 100644 --- a/src/ast/justified_expr.h +++ b/src/ast/justified_expr.h @@ -33,8 +33,7 @@ public: justified_expr(justified_expr const& other): m(other.m), m_fml(other.m_fml), - m_proof(other.m_proof) - { + m_proof(other.m_proof) { m.inc_ref(m_fml); m.inc_ref(m_proof); } @@ -42,8 +41,7 @@ public: justified_expr(justified_expr && other) noexcept : m(other.m), m_fml(nullptr), - m_proof(nullptr) - { + m_proof(nullptr) { std::swap(m_fml, other.m_fml); std::swap(m_proof, other.m_proof); } @@ -51,10 +49,11 @@ public: ~justified_expr() { m.dec_ref(m_fml); m.dec_ref(m_proof); - m_fml = nullptr; - m_proof = nullptr; + m_fml = nullptr; + m_proof = nullptr; } expr* get_fml() const { return m_fml; } + proof* get_proof() const { return m_proof; } }; diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index dcff35e82..8e1279c0a 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -203,8 +203,9 @@ namespace recfun { def const& get_def(func_decl* f) const { return *(m_defs[f]); } promise_def get_promise_def(func_decl* f) const { return promise_def(&u(), m_defs[f]); } def& get_def(func_decl* f) { return *(m_defs[f]); } - bool has_case_def(func_decl* f) const { return m_case_defs.contains(f); } + bool has_case_def(func_decl* f) const { return m_case_defs.contains(f); } case_def& get_case_def(func_decl* f) { SASSERT(has_case_def(f)); return *(m_case_defs[f]); } + bool is_defined(func_decl* f) {return has_case_def(f) && !get_def(f).get_cases().empty(); } func_decl_ref_vector get_rec_funs() { func_decl_ref_vector result(m()); diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 80495853a..1964e6528 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -290,7 +290,7 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args, ast_lt lt; std::sort(flat_args.begin(), flat_args.end(), lt); } - result = m().mk_or(flat_args); + result = mk_or_app(flat_args.size(), flat_args.data()); } return BR_DONE; } diff --git a/src/ast/rewriter/mk_extract_proc.cpp b/src/ast/rewriter/mk_extract_proc.cpp index be61047a4..cc18ae176 100644 --- a/src/ast/rewriter/mk_extract_proc.cpp +++ b/src/ast/rewriter/mk_extract_proc.cpp @@ -32,8 +32,15 @@ mk_extract_proc::~mk_extract_proc() { } app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) { + unsigned l, h; + while (m_util.is_extract(arg, l, h, arg)) { + low += l; + high += l; + } ast_manager & m = m_util.get_manager(); sort * s = arg->get_sort(); + if (low == 0 && high + 1 == m_util.get_bv_size(arg) && is_app(arg)) + return to_app(arg); if (m_low == low && m_high == high && m_domain == s) return m.mk_app(m_f_cached, arg); // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h index 271500551..e432678a4 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/src/ast/rewriter/th_rewriter.h @@ -47,6 +47,7 @@ public: expr_ref operator()(expr * n, unsigned num_bindings, expr * const * bindings); expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args); + expr_ref mk_app(func_decl* f, ptr_vector const& args) { return mk_app(f, args.size(), args.data()); } bool reduce_quantifier(quantifier * old_q, expr * new_body, diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt new file mode 100644 index 000000000..dc7aa6fb6 --- /dev/null +++ b/src/ast/simplifiers/CMakeLists.txt @@ -0,0 +1,11 @@ +z3_add_component(simplifiers + SOURCES + bv_slice.cpp + euf_completion.cpp + extract_eqs.cpp + model_reconstruction_trail.cpp + solve_eqs.cpp + COMPONENT_DEPENDENCIES + euf + rewriter +) diff --git a/src/ast/simplifiers/bv_slice.cpp b/src/ast/simplifiers/bv_slice.cpp new file mode 100644 index 000000000..f39fa932e --- /dev/null +++ b/src/ast/simplifiers/bv_slice.cpp @@ -0,0 +1,207 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + bv_slice.cpp + +Abstract: + + simplifier for extracting bit-vector ranges + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + +#include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" +#include "ast/simplifiers/bv_slice.h" + +namespace bv { + + void slice::reduce() { + process_eqs(); + apply_subst(); + advance_qhead(m_fmls.size()); + } + + void slice::process_eqs() { + for (unsigned i = m_qhead; i < m_fmls.size(); ++i) { + auto const [f, d] = m_fmls[i](); + process_eq(f); + } + } + + void slice::process_eq(expr* e) { + expr* x, * y; + if (!m.is_eq(e, x, y)) + return; + if (!m_bv.is_bv(x)) + return; + m_xs.reset(); + m_ys.reset(); + get_concats(x, m_xs); + get_concats(y, m_ys); + slice_eq(); + } + + void slice::slice_eq() { + unsigned i = m_xs.size(), j = m_ys.size(); + unsigned offx = 0, offy = 0; + while (0 < i) { + SASSERT(0 < j); + expr* x = m_xs[i - 1]; // least significant bits are last + expr* y = m_ys[j - 1]; + SASSERT(offx == 0 || offy == 0); + unsigned szx = m_bv.get_bv_size(x); + unsigned szy = m_bv.get_bv_size(y); + SASSERT(offx < szx); + SASSERT(offy < szy); + if (szx - offx == szy - offy) { + register_slice(offx, szx - 1, x); + register_slice(offy, szy - 1, y); + --i; + --j; + offx = 0; + offy = 0; + } + else if (szx - offx < szy - offy) { + register_slice(offx, szx - 1, x); + register_slice(offy, offy + szx - offx - 1, y); + offy += szx - offx; + offx = 0; + --i; + } + else { + register_slice(offy, szy - 1, y); + register_slice(offx, offx + szy - offy - 1, x); + offx += szy - offy; + offy = 0; + --j; + } + } + } + + void slice::register_slice(unsigned lo, unsigned hi, expr* x) { + SASSERT(lo <= hi && hi < m_bv.get_bv_size(x)); + unsigned l, h; + while (m_bv.is_extract(x, l, h, x)) { + // x[l:h][lo:hi] = x[l+lo:l+hi] + hi += l; + lo += l; + SASSERT(lo <= hi && hi < m_bv.get_bv_size(x)); + } + unsigned sz = m_bv.get_bv_size(x); + if (hi - lo + 1 == sz) + return; + SASSERT(0 < lo || hi + 1 < sz); + auto& b = m_boundaries.insert_if_not_there(x, uint_set()); + + struct remove_set : public trail { + uint_set& b; + unsigned i; + remove_set(uint_set& b, unsigned i) :b(b), i(i) {} + void undo() override { + b.remove(i); + } + }; + if (lo > 0 && !b.contains(lo)) { + b.insert(lo); + if (m_num_scopes > 0) + m_trail.push(remove_set(b, lo)); + } + if (hi + 1 < sz && !b.contains(hi + 1)) { + b.insert(hi + 1); + if (m_num_scopes > 0) + m_trail.push(remove_set(b, hi+ 1)); + } + } + + expr* slice::mk_extract(unsigned hi, unsigned lo, expr* x) { + unsigned l, h; + while (m_bv.is_extract(x, l, h, x)) { + lo += l; + hi += l; + } + if (lo == 0 && hi + 1 == m_bv.get_bv_size(x)) + return x; + else + return m_bv.mk_extract(hi, lo, x); + } + + void slice::apply_subst() { + if (m_boundaries.empty()) + return; + expr_ref_vector cache(m), pin(m); + ptr_vector todo, args; + expr* c; + for (unsigned i = m_qhead; i < m_fmls.size(); ++i) { + auto const [f, d] = m_fmls[i](); + todo.push_back(f); + pin.push_back(f); + while (!todo.empty()) { + expr* e = todo.back(); + c = cache.get(e->get_id(), nullptr); + if (c) { + todo.pop_back(); + continue; + } + if (!is_app(e)) { + cache.setx(e->get_id(), e); + todo.pop_back(); + continue; + } + args.reset(); + unsigned sz = todo.size(); + bool change = false; + for (expr* arg : *to_app(e)) { + c = cache.get(arg->get_id(), nullptr); + if (c) { + args.push_back(c); + change |= c != arg; + SASSERT(c->get_sort() == arg->get_sort()); + } + else + todo.push_back(arg); + } + if (sz == todo.size()) { + todo.pop_back(); + if (change) + cache.setx(e->get_id(), m_rewriter.mk_app(to_app(e)->get_decl(), args)); + else + cache.setx(e->get_id(), e); + SASSERT(e->get_sort() == cache.get(e->get_id())->get_sort()); + uint_set b; + if (m_boundaries.find(e, b)) { + expr* r = cache.get(e->get_id()); + expr_ref_vector xs(m); + unsigned lo = 0; + for (unsigned hi : b) { + xs.push_back(mk_extract(hi - 1, lo, r)); + lo = hi; + } + xs.push_back(mk_extract(m_bv.get_bv_size(r) - 1, lo, r)); + xs.reverse(); + expr_ref xc(m_bv.mk_concat(xs), m); + cache.setx(e->get_id(), xc); + SASSERT(e->get_sort() == xc->get_sort()); + } + } + } + c = cache.get(f->get_id()); + if (c != f) + m_fmls.update(i, dependent_expr(m, c, d)); + } + } + + void slice::get_concats(expr* x, ptr_vector& xs) { + while (m_bv.is_concat(x)) { + xs.append(to_app(x)->get_num_args(), to_app(x)->get_args()); + x = xs.back(); + xs.pop_back(); + } + xs.push_back(x); + } +} diff --git a/src/ast/simplifiers/bv_slice.h b/src/ast/simplifiers/bv_slice.h new file mode 100644 index 000000000..cc0f48cfc --- /dev/null +++ b/src/ast/simplifiers/bv_slice.h @@ -0,0 +1,55 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + bv_slice.h + +Abstract: + + simplifier for extracting bit-vector ranges + It rewrites a state using bit-vector slices. + Slices are extracted from bit-vector equality assertions + in the style of (but not fully implementing a full slicing) + Bjorner & Pichora, TACAS 1998 and Brutomesso et al 2008. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + + +#pragma once + +#include "util/uint_set.h" +#include "ast/bv_decl_plugin.h" +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/rewriter/th_rewriter.h" + + +namespace bv { + + class slice : public dependent_expr_simplifier { + bv_util m_bv; + th_rewriter m_rewriter; + obj_map m_boundaries; + ptr_vector m_xs, m_ys; + + expr* mk_extract(unsigned hi, unsigned lo, expr* x); + void process_eqs(); + void process_eq(expr* e); + void slice_eq(); + void register_slice(unsigned lo, unsigned hi, expr* x); + void apply_subst(); + void get_concats(expr* x, ptr_vector& xs); + + public: + + slice(ast_manager& m, dependent_expr_state& fmls) : dependent_expr_simplifier(m, fmls), m_bv(m), m_rewriter(m) {} + + void push() override { dependent_expr_simplifier::push(); } + void pop(unsigned n) override { dependent_expr_simplifier::pop(n); } + void reduce() override; + }; +} diff --git a/src/ast/simplifiers/dependent_expr.h b/src/ast/simplifiers/dependent_expr.h new file mode 100644 index 000000000..9d6d8625e --- /dev/null +++ b/src/ast/simplifiers/dependent_expr.h @@ -0,0 +1,75 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + dependent_expr.h + +Abstract: + + Container class for dependent expressions. + They represent how assertions are tracked in goals. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ +#pragma once + +#include "ast/ast.h" + +class dependent_expr { + ast_manager& m; + expr* m_fml; + expr_dependency* m_dep; +public: + dependent_expr(ast_manager& m, expr* fml, expr_dependency* d): + m(m), + m_fml(fml), + m_dep(d) { + SASSERT(fml); + m.inc_ref(fml); + m.inc_ref(d); + } + + dependent_expr& operator=(dependent_expr const& other) { + SASSERT(&m == &other.m); + if (this != &other) { + m.inc_ref(other.m_fml); + m.inc_ref(other.m_dep); + m.dec_ref(m_fml); + m.dec_ref(m_dep); + m_fml = other.m_fml; + m_dep = other.m_dep; + } + return *this; + } + + dependent_expr(dependent_expr const& other): + m(other.m), + m_fml(other.m_fml), + m_dep(other.m_dep) { + m.inc_ref(m_fml); + m.inc_ref(m_dep); + } + + dependent_expr(dependent_expr && other) noexcept : + m(other.m), + m_fml(nullptr), + m_dep(nullptr) { + std::swap(m_fml, other.m_fml); + std::swap(m_dep, other.m_dep); + } + + ~dependent_expr() { + m.dec_ref(m_fml); + m.dec_ref(m_dep); + m_fml = nullptr; + m_dep = nullptr; + } + + std::tuple operator()() const { + return { m_fml, m_dep }; + } +}; diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h new file mode 100644 index 000000000..32ad59681 --- /dev/null +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -0,0 +1,90 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + dependent_expr_state.h + +Abstract: + + abstraction for simplification of depenent expression states. + A dependent_expr_state is an interface to a set of dependent expressions. + Dependent expressions are formulas together with a set of dependencies that are coarse grained + proof hints or justifications for them. Input assumptions can be self-justified. + + The dependent_expr_simplifier implements main services: + - push, pop - that scope the local state + - reduce - to process formulas in a dependent_expr_state between the current value of m_qhead and the size() + of the depdenent_expr_state + + A dependent expr_simplifier can be used to: + - to build a tactic + - for incremental pre-processing + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + +#pragma once + +#include "util/trail.h" +#include "util/statistics.h" +#include "util/params.h" +#include "ast/converters/model_converter.h" +#include "ast/simplifiers/dependent_expr.h" + + +/** + abstract interface to state updated by simplifiers. + */ +class dependent_expr_state { +public: + virtual ~dependent_expr_state() {} + virtual unsigned size() const = 0; + virtual dependent_expr const& operator[](unsigned i) = 0; + virtual void update(unsigned i, dependent_expr const& j) = 0; + virtual bool inconsistent() = 0; +}; + +/** + Shared interface of simplifiers. + */ +class dependent_expr_simplifier { +protected: + ast_manager& m; + dependent_expr_state& m_fmls; + unsigned m_qhead = 0; // pointer into last processed formula in m_fmls + unsigned m_num_scopes = 0; + trail_stack m_trail; + void advance_qhead(unsigned sz) { if (m_num_scopes > 0) m_trail.push(value_trail(m_qhead)); m_qhead = sz; } +public: + dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s) {} + virtual ~dependent_expr_simplifier() {} + virtual void push() { m_num_scopes++; m_trail.push_scope(); } + virtual void pop(unsigned n) { m_num_scopes -= n; m_trail.pop_scope(n); } + virtual void reduce() = 0; + virtual void collect_statistics(statistics& st) const {} + virtual void reset_statistics() {} + virtual void updt_params(params_ref const& p) {} + virtual model_converter_ref get_model_converter() { return model_converter_ref(); } +}; + +/** + Factory interface for creating simplifiers. + The use of a factory allows delaying the creation of the dependent_expr_state + argument until the point where the expression simplifier is created. + This is used in tactics where the dependent_expr_state is a reference to the + new tactic. + + Alternatively have a clone method on dependent_expr_simplifier. + */ +class dependent_expr_simplifier_factory { + unsigned m_ref = 0; +public: + virtual dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) = 0; + virtual ~dependent_expr_simplifier_factory() {} + void inc_ref() { ++m_ref; } + void dec_ref() { if (--m_ref == 0) dealloc(this); } +}; diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp new file mode 100644 index 000000000..e5b328d7f --- /dev/null +++ b/src/ast/simplifiers/euf_completion.cpp @@ -0,0 +1,328 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + euf_completion.cpp + +Abstract: + + Ground completion for equalities + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-30 + +Notes: + +Create a congruence closure of E. +Select _simplest_ term in each equivalence class. A term is _simplest_ +if it is smallest in a well-order, such as a ground Knuth-Bendix order. +A basic approach is terms that are of smallest depth, are values can be chosen as simplest. +Ties between equal-depth terms can be resolved arbitrarily. + + +Algorithm for extracting canonical form from an E-graph: + +* Compute function canon(t) that maps every term in E to a canonical, least with respect to well-order relative to the congruence closure. + That is, terms that are equal modulo the congruence closure have the same canonical representative. + +* Each f(t) = g(s) in E: + * add f(canon(t)) = canon(f(t)), g(canon(s)) = canon(g(s)) where canon(f(t)) = canon(g(s)) by construction. + +* Each other g(t) in E: + * add g(canon(t)) to E. + * Note that canon(g(t)) = true because g(t) = true is added to congruence closure of E. +* We claim the new formula is equivalent. +* The dependencies for each rewrite can be computed by following the equality justification data-structure. + + +--*/ + +#include "ast/ast_pp.h" +#include "ast/ast_util.h" +#include "ast/euf/euf_egraph.h" +#include "ast/simplifiers/euf_completion.h" + +namespace euf { + + completion::completion(ast_manager& m, dependent_expr_state& fmls): + dependent_expr_simplifier(m, fmls), + m_egraph(m), + m_canonical(m), + m_eargs(m), + m_deps(m), + m_rewriter(m) { + m_tt = m_egraph.mk(m.mk_true(), 0, 0, nullptr); + m_ff = m_egraph.mk(m.mk_false(), 0, 0, nullptr); + } + + void completion::reduce() { + ++m_epoch; + add_egraph(); + map_canonical(); + read_egraph(); + } + + void completion::add_egraph() { + m_nodes.reset(); + unsigned sz = m_fmls.size(); + expr* x, *y; + for (unsigned i = m_qhead; i < sz; ++i) { + auto [f,d] = m_fmls[i](); + auto* n = mk_enode(f); + if (m.is_eq(f, x, y)) + m_egraph.merge(n->get_arg(0), n->get_arg(1), d); + if (m.is_not(f, x)) + m_egraph.merge(n->get_arg(0), m_ff, d); + else + m_egraph.merge(n, m_tt, d); + } + m_egraph.propagate(); + } + + void completion::read_egraph() { + + if (m_egraph.inconsistent()) { + auto* d = explain_conflict(); + dependent_expr de(m, m.mk_false(), d); + m_fmls.update(0, de); + return; + } + + for (unsigned i = m_qhead; i < m_fmls.size(); ++i) { + auto [f, d] = m_fmls[i](); + + expr_dependency_ref dep(d, m); + expr_ref g = canonize_fml(f, dep); + if (g != f) { + m_fmls.update(i, dependent_expr(m, g, dep)); + m_stats.m_num_rewrites++; + IF_VERBOSE(10, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n"); + } + CTRACE("euf_completion", g != f, tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n"); + } + advance_qhead(m_fmls.size()); + } + + enode* completion::mk_enode(expr* e) { + m_todo.push_back(e); + enode* n; + while (!m_todo.empty()) { + e = m_todo.back(); + if (m_egraph.find(e)) { + m_todo.pop_back(); + continue; + } + if (!is_app(e)) { + m_nodes.push_back(m_egraph.mk(e, 0, 0, nullptr)); + m_todo.pop_back(); + continue; + } + m_args.reset(); + unsigned sz = m_todo.size(); + for (expr* arg : *to_app(e)) { + n = m_egraph.find(arg); + if (n) + m_args.push_back(n); + else + m_todo.push_back(arg); + } + if (sz == m_todo.size()) { + m_nodes.push_back(m_egraph.mk(e, 0, m_args.size(), m_args.data())); + m_todo.pop_back(); + } + } + return m_egraph.find(e); + } + + expr_ref completion::canonize_fml(expr* f, expr_dependency_ref& d) { + + expr* x, * y; + if (m.is_eq(f, x, y)) { + expr_ref x1 = canonize(x, d); + expr_ref y1 = canonize(y, d); + + if (x == x1 && y == y1) + return expr_ref(f, m); + if (x1 == y1) + return expr_ref(m.mk_true(), m); + else { + expr* c = get_canonical(x, d); + if (c == x1) + return expr_ref(m.mk_eq(y1, c), m); + else if (c == y1) + return expr_ref(m.mk_eq(x1, c), m); + else + return expr_ref(m.mk_and(m.mk_eq(x1, c), m.mk_eq(y1, c)), m); + } + } + + if (m.is_not(f, x)) { + expr_ref x1 = canonize(x, d); + return expr_ref(mk_not(m, x1), m); + } + + return canonize(f, d); + } + + expr_ref completion::canonize(expr* f, expr_dependency_ref& d) { + if (!is_app(f)) + return expr_ref(f, m); // todo could normalize ground expressions under quantifiers + + m_eargs.reset(); + bool change = false; + for (expr* arg : *to_app(f)) { + m_eargs.push_back(get_canonical(arg, d)); + change = arg != m_eargs.back(); + } + + if (!change) + return expr_ref(f, m); + else + return expr_ref(m_rewriter.mk_app(to_app(f)->get_decl(), m_eargs.size(), m_eargs.data()), m); + } + + expr* completion::get_canonical(expr* f, expr_dependency_ref& d) { + enode* n = m_egraph.find(f); + enode* r = n->get_root(); + d = m.mk_join(d, explain_eq(n, r)); + d = m.mk_join(d, m_deps.get(r->get_id(), nullptr)); + return m_canonical.get(r->get_id()); + } + + expr* completion::get_canonical(enode* n) { + if (m_epochs.get(n->get_id(), 0) == m_epoch) + return m_canonical.get(n->get_id()); + else + return nullptr; + } + + void completion::set_canonical(enode* n, expr* e) { + class vtrail : public trail { + expr_ref_vector& c; + unsigned idx; + expr_ref old_value; + public: + vtrail(expr_ref_vector& c, unsigned idx) : + c(c), idx(idx), old_value(c.get(idx), c.m()) { + } + + void undo() override { + c[idx] = old_value; + old_value = nullptr; + } + }; + if (m_num_scopes > 0) + m_trail.push(vtrail(m_canonical, n->get_id())); + m_canonical.setx(n->get_id(), e); + m_epochs.setx(n->get_id(), m_epoch, 0); + } + + expr_dependency* completion::explain_eq(enode* a, enode* b) { + if (a == b) + return nullptr; + ptr_vector just; + m_egraph.begin_explain(); + m_egraph.explain_eq(just, nullptr, a, b); + m_egraph.end_explain(); + expr_dependency* d = nullptr; + for (expr_dependency* d2 : just) + d = m.mk_join(d, d2); + return d; + } + + expr_dependency* completion::explain_conflict() { + ptr_vector just; + m_egraph.begin_explain(); + m_egraph.explain(just, nullptr); + m_egraph.end_explain(); + expr_dependency* d = nullptr; + for (expr_dependency* d2 : just) + d = m.mk_join(d, d2); + return d; + } + + void completion::collect_statistics(statistics& st) const { + st.update("euf-completion-rewrites", m_stats.m_num_rewrites); + } + + void completion::map_canonical() { + m_todo.reset(); + enode_vector roots; + for (unsigned i = 0; i < m_nodes.size(); ++i) { + enode* n = m_nodes[i]->get_root(); + if (n->is_marked1()) + continue; + n->mark1(); + roots.push_back(n); + enode* rep = nullptr; + for (enode* k : enode_class(n)) + if (!rep || m.is_value(k->get_expr()) || get_depth(rep->get_expr()) > get_depth(k->get_expr())) + rep = k; + m_reps.setx(n->get_id(), rep, nullptr); + + TRACE("euf_completion", tout << "rep " << m_egraph.bpp(n) << " -> " << m_egraph.bpp(rep) << "\n"; + for (enode* k : enode_class(n)) tout << m_egraph.bpp(k) << "\n";); + m_todo.push_back(n->get_expr()); + for (enode* arg : enode_args(n)) { + arg = arg->get_root(); + if (!arg->is_marked1()) + m_nodes.push_back(arg); + } + } + for (enode* r : roots) + r->unmark1(); + + // explain dependencies when no nodes are marked. + // explain_eq uses both mark1 and mark2 on e-nodes so + // we cannot call it inside the previous loop where mark1 is used + // to track which roots have been processed. + for (enode* r : roots) { + enode* rep = m_reps[r->get_id()]; + auto* d = explain_eq(r, rep); + m_deps.setx(r->get_id(), d); + } + expr_ref new_expr(m); + while (!m_todo.empty()) { + expr* e = m_todo.back(); + enode* n = m_egraph.find(e); + SASSERT(n->is_root()); + enode* rep = m_reps[n->get_id()]; + if (get_canonical(n)) + m_todo.pop_back(); + else if (get_depth(rep->get_expr()) == 0 || !is_app(rep->get_expr())) { + set_canonical(n, rep->get_expr()); + m_todo.pop_back(); + } + else { + m_eargs.reset(); + unsigned sz = m_todo.size(); + bool new_arg = false; + expr_dependency* d = m_deps.get(n->get_id(), nullptr); + for (enode* arg : enode_args(rep)) { + enode* rarg = arg->get_root(); + expr* c = get_canonical(rarg); + if (c) { + m_eargs.push_back(c); + new_arg |= c != arg->get_expr(); + d = m.mk_join(d, m_deps.get(rarg->get_id(), nullptr)); + } + else + m_todo.push_back(rarg->get_expr()); + } + if (sz == m_todo.size()) { + m_todo.pop_back(); + if (new_arg) + new_expr = m_rewriter.mk_app(to_app(rep->get_expr())->get_decl(), m_eargs.size(), m_eargs.data()); + else + new_expr = rep->get_expr(); + set_canonical(n, new_expr); + m_deps.setx(n->get_id(), d); + } + } + } + } +} + + diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h new file mode 100644 index 000000000..9e293ca0e --- /dev/null +++ b/src/ast/simplifiers/euf_completion.h @@ -0,0 +1,63 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + euf_completion.h + +Abstract: + + Ground completion for equalities + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-30 + +--*/ + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/euf/euf_egraph.h" +#include "ast/rewriter/th_rewriter.h" + +namespace euf { + + class completion : public dependent_expr_simplifier { + + struct stats { + unsigned m_num_rewrites = 0; + void reset() { memset(this, 0, sizeof(*this)); } + }; + + egraph m_egraph; + enode* m_tt, *m_ff; + ptr_vector m_todo; + enode_vector m_args, m_reps, m_nodes; + expr_ref_vector m_canonical, m_eargs; + expr_dependency_ref_vector m_deps; + unsigned m_epoch = 0; + unsigned_vector m_epochs; + th_rewriter m_rewriter; + stats m_stats; + + enode* mk_enode(expr* e); + void add_egraph(); + void map_canonical(); + void read_egraph(); + expr_ref canonize(expr* f, expr_dependency_ref& dep); + expr_ref canonize_fml(expr* f, expr_dependency_ref& dep); + expr* get_canonical(expr* f, expr_dependency_ref& d); + expr* get_canonical(enode* n); + void set_canonical(enode* n, expr* e); + expr_dependency* explain_eq(enode* a, enode* b); + expr_dependency* explain_conflict(); + public: + completion(ast_manager& m, dependent_expr_state& fmls); + void push() override { m_egraph.push(); dependent_expr_simplifier::push(); } + void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_egraph.pop(n); } + void reduce() override; + void collect_statistics(statistics& st) const override; + void reset_statistics() override { m_stats.reset(); } + }; +} diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp new file mode 100644 index 000000000..1e9b576e1 --- /dev/null +++ b/src/ast/simplifiers/extract_eqs.cpp @@ -0,0 +1,257 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + extract_eqs.cpp + +Abstract: + + simplifier for solving equations + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + + +#include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include "ast/ast_pp.h" +#include "ast/arith_decl_plugin.h" +#include "ast/simplifiers/extract_eqs.h" +#include "params/tactic_params.hpp" + + +namespace euf { + + class basic_extract_eq : public extract_eq { + ast_manager& m; + bool m_ite_solver = true; + + public: + basic_extract_eq(ast_manager& m) : m(m) {} + + void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override { + auto [f, d] = e(); + expr* x, * y; + if (m.is_eq(f, x, y)) { + if (is_uninterp_const(x)) + eqs.push_back(dependent_eq(to_app(x), expr_ref(y, m), d)); + if (is_uninterp_const(y)) + eqs.push_back(dependent_eq(to_app(y), expr_ref(x, m), d)); + } + expr* c, * th, * el, * x1, * y1, * x2, * y2; + if (m_ite_solver && m.is_ite(f, c, th, el)) { + if (m.is_eq(th, x1, y1) && m.is_eq(el, x2, y2)) { + if (x1 == y2 && is_uninterp_const(x1)) + std::swap(x2, y2); + if (x2 == y2 && is_uninterp_const(x2)) + std::swap(x2, y2), std::swap(x1, y1); + if (x2 == y1 && is_uninterp_const(x2)) + std::swap(x1, y1); + if (x1 == x2 && is_uninterp_const(x1)) + eqs.push_back(dependent_eq(to_app(x1), expr_ref(m.mk_ite(c, y1, y2), m), d)); + } + } + if (is_uninterp_const(f)) + eqs.push_back(dependent_eq(to_app(f), expr_ref(m.mk_true(), m), d)); + if (m.is_not(f, x) && is_uninterp_const(x)) + eqs.push_back(dependent_eq(to_app(x), expr_ref(m.mk_false(), m), d)); + } + + void updt_params(params_ref const& p) { + tactic_params tp(p); + m_ite_solver = p.get_bool("ite_solver", tp.solve_eqs_ite_solver()); + } + }; + + class arith_extract_eq : public extract_eq { + ast_manager& m; + arith_util a; + expr_ref_vector m_args; + expr_sparse_mark m_nonzero; + bool m_enabled = true; + + + // solve u mod r1 = y -> u = r1*mod!1 + y + void solve_mod(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + expr* u, * z; + rational r1, r2; + if (!a.is_mod(x, u, z)) + return; + if (!a.is_numeral(z, r1)) + return; + if (r1 <= 0) + return; + expr_ref term(m); + term = a.mk_add(a.mk_mul(z, m.mk_fresh_const("mod", a.mk_int())), y); + solve_eq(u, term, d, eqs); + } + + /*** + * Solve + * x + Y = Z -> x = Z - Y + * -1*x + Y = Z -> x = Y - Z + * a*x + Y = Z -> x = (Z - Y)/a for is-real(x) + */ + void solve_add(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + if (!a.is_add(x)) + return; + expr* u, * z; + rational r; + expr_ref term(m); + unsigned i = 0; + auto mk_term = [&](unsigned i) { + term = y; + unsigned j = 0; + for (expr* arg2 : *to_app(x)) { + if (i != j) + term = a.mk_sub(term, arg2); + ++j; + } + }; + for (expr* arg : *to_app(x)) { + if (is_uninterp_const(arg)) { + mk_term(i); + eqs.push_back(dependent_eq(to_app(arg), term, d)); + } + else if (a.is_mul(arg, u, z) && a.is_numeral(u, r) && is_uninterp_const(z)) { + if (r == -1) { + mk_term(i); + term = a.mk_uminus(term); + eqs.push_back(dependent_eq(to_app(z), term, d)); + } + else if (a.is_real(arg) && r != 0) { + mk_term(i); + term = a.mk_div(term, u); + eqs.push_back(dependent_eq(to_app(z), term, d)); + } + } + else if (a.is_real(arg) && a.is_mul(arg)) { + unsigned j = 0; + for (expr* xarg : *to_app(arg)) { + ++j; + if (!is_uninterp_const(xarg)) + continue; + unsigned k = 0; + bool nonzero = true; + for (expr* yarg : *to_app(arg)) { + ++k; + nonzero = k == j || m_nonzero.is_marked(yarg) || (a.is_numeral(yarg, r) && r != 0); + if (!nonzero) + break; + } + if (!nonzero) + continue; + + k = 0; + ptr_buffer args; + for (expr* yarg : *to_app(arg)) { + ++k; + if (k != j) + args.push_back(yarg); + } + mk_term(i); + term = a.mk_div(term, a.mk_mul(args.size(), args.data())); + eqs.push_back(dependent_eq(to_app(xarg), term, d)); + } + } + ++i; + } + } + + /*** + * Solve for x * Y = Z, where Y != 0 -> x = Z / Y + */ + void solve_mul(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + if (!a.is_mul(x)) + return; + rational r; + expr_ref term(m); + unsigned i = 0; + for (expr* arg : *to_app(x)) { + ++i; + if (!is_uninterp_const(arg)) + continue; + unsigned j = 0; + bool nonzero = true; + for (expr* arg2 : *to_app(x)) { + ++j; + nonzero = j == i || m_nonzero.is_marked(arg2) || (a.is_numeral(arg2, r) && r != 0); + if (!nonzero) + break; + } + if (!nonzero) + continue; + ptr_buffer args; + j = 0; + for (expr* arg2 : *to_app(x)) { + ++j; + if (j != i) + args.push_back(arg2); + } + term = a.mk_div(y, a.mk_mul(args)); + eqs.push_back(dependent_eq(to_app(arg), term, d)); + } + } + + void add_pos(expr* f) { + expr* lhs = nullptr, * rhs = nullptr; + rational val; + if (a.is_le(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_neg()) + m_nonzero.mark(lhs); + else if (a.is_ge(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_pos()) + m_nonzero.mark(lhs); + else if (m.is_not(f, f)) { + if (a.is_le(f, lhs, rhs) && a.is_numeral(rhs, val) && !val.is_neg()) + m_nonzero.mark(lhs); + else if (a.is_ge(f, lhs, rhs) && a.is_numeral(rhs, val) && !val.is_pos()) + m_nonzero.mark(lhs); + else if (m.is_eq(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_zero()) + m_nonzero.mark(lhs); + } + } + + void solve_eq(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + solve_add(x, y, d, eqs); + solve_mod(x, y, d, eqs); + solve_mul(x, y, d, eqs); + } + + public: + arith_extract_eq(ast_manager& m) : m(m), a(m), m_args(m) {} + void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override { + if (!m_enabled) + return; + auto [f, d] = e(); + expr* x, * y; + if (m.is_eq(f, x, y) && a.is_int_real(x)) { + solve_eq(x, y, d, eqs); + solve_eq(y, x, d, eqs); + } + } + + void pre_process(dependent_expr_state& fmls) override { + if (!m_enabled) + return; + m_nonzero.reset(); + for (unsigned i = 0; i < fmls.size(); ++i) { + auto [f, d] = fmls[i](); + add_pos(f); + } + } + + + void updt_params(params_ref const& p) { + tactic_params tp(p); + m_enabled = p.get_bool("theory_solver", tp.solve_eqs_ite_solver()); + } + }; + + void register_extract_eqs(ast_manager& m, scoped_ptr_vector& ex) { + ex.push_back(alloc(arith_extract_eq, m)); + ex.push_back(alloc(basic_extract_eq, m)); + } +} diff --git a/src/ast/simplifiers/extract_eqs.h b/src/ast/simplifiers/extract_eqs.h new file mode 100644 index 000000000..00f96f59b --- /dev/null +++ b/src/ast/simplifiers/extract_eqs.h @@ -0,0 +1,48 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + extract_eqs.h + +Abstract: + + simplifier for solving equations + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/expr_substitution.h" +#include "util/scoped_ptr_vector.h" + + +namespace euf { + + struct dependent_eq { + app* var; + expr_ref term; + expr_dependency* dep; + dependent_eq(app* var, expr_ref const& term, expr_dependency* d) : var(var), term(term), dep(d) {} + }; + + typedef vector dep_eq_vector; + + class extract_eq { + public: + virtual ~extract_eq() {} + virtual void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) = 0; + virtual void pre_process(dependent_expr_state& fmls) {} + virtual void updt_params(params_ref const& p) {} + }; + + void register_extract_eqs(ast_manager& m, scoped_ptr_vector& ex); + +} diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp new file mode 100644 index 000000000..2e8eab0e6 --- /dev/null +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -0,0 +1,44 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + model_reconstruction_trail.cpp + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-3. + +--*/ + + +#include "ast/for_each_expr.h" +#include "ast/simplifiers/model_reconstruction_trail.h" +#include "ast/converters/generic_model_converter.h" + + +void model_reconstruction_trail::replay(dependent_expr const& d, vector& added) { + // accumulate a set of dependent exprs, updating m_trail to exclude loose + // substitutions that use variables from the dependent expressions. + ast_mark free_vars; + auto [f, dep] = d(); + for (expr* t : subterms::all(expr_ref(f, m))) + free_vars.mark(t, true); + + NOT_IMPLEMENTED_YET(); +} + +/** + * retrieve the current model converter corresponding to chaining substitutions from the trail. + */ +model_converter_ref model_reconstruction_trail::get_model_converter() { + model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model"); + // walk the trail from the back + // add substitutions from the back to the generic model converter + // after they have been normalized using a global replace that replaces + // substituted variables by their terms. + NOT_IMPLEMENTED_YET(); + return mc; + +} + diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h new file mode 100644 index 000000000..eeaf786d9 --- /dev/null +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -0,0 +1,80 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + model_reconstruction_trail.h + +Abstract: + + Model reconstruction trail + A model reconstruction trail comprises of a sequence of assignments + together with assertions that were removed in favor of the assignments. + The assignments satisfy the removed assertions but are not (necessarily) + equivalent to the removed assertions. For the case where assignments + are equivalent to removed assertions, we squash the removed assertions + and don't track them. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-3. + +--*/ + +#pragma once + +#include "util/scoped_ptr_vector.h" +#include "ast/rewriter/expr_replacer.h" +#include "ast/simplifiers/dependent_expr.h" +#include "ast/converters/model_converter.h" + +class model_reconstruction_trail { + + ast_manager& m; + + struct model_reconstruction_trail_entry { + scoped_ptr m_replace; + vector m_removed; + model_reconstruction_trail_entry(expr_replacer* r, vector const& rem) : + m_replace(r), m_removed(rem) {} + }; + + scoped_ptr_vector m_trail; + unsigned_vector m_limit; + +public: + + model_reconstruction_trail(ast_manager& m) : m(m) {} + + /** + * add a new substitution to the stack + */ + void push(expr_replacer* r, vector const& removed) { + m_trail.push_back(alloc(model_reconstruction_trail_entry, r, removed)); + } + + /** + * register a new depedent expression, update the trail + * by removing substitutions that are not equivalence preserving. + */ + void replay(dependent_expr const& d, vector& added); + + /** + * retrieve the current model converter corresponding to chaining substitutions from the trail. + */ + model_converter_ref get_model_converter(); + + /** + * push a context. Portions of the trail added within a context are removed after a context pop. + */ + void push() { + m_limit.push_back(m_trail.size()); + } + + void pop(unsigned n) { + unsigned old_sz = m_limit[m_limit.size() - n]; + m_trail.resize(old_sz); + m_limit.shrink(m_limit.size() - n); + } +}; + diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp new file mode 100644 index 000000000..6b2a27d2d --- /dev/null +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -0,0 +1,215 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + solve_eqs.cpp + +Abstract: + + simplifier for solving equations + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + + +#include "util/trace.h" +#include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include "ast/ast_pp.h" +#include "ast/recfun_decl_plugin.h" +#include "ast/rewriter/expr_replacer.h" +#include "ast/simplifiers/solve_eqs.h" +#include "ast/converters/generic_model_converter.h" +#include "params/tactic_params.hpp" + + +namespace euf { + + // initialize graph that maps variable ids to next ids + void solve_eqs::extract_dep_graph(dep_eq_vector& eqs) { + m_var2id.reset(); + m_id2var.reset(); + m_next.reset(); + unsigned sz = 0; + for (auto const& [v, t, d] : eqs) + sz = std::max(sz, v->get_id()); + m_var2id.resize(sz + 1, UINT_MAX); + for (auto const& [v, t, d] : eqs) { + if (is_var(v) || !can_be_var(v)) + continue; + m_var2id[v->get_id()] = m_id2var.size(); + m_id2var.push_back(v); + } + m_next.resize(m_id2var.size()); + + for (auto const& eq : eqs) + if (can_be_var(eq.var)) + m_next[var2id(eq.var)].push_back(eq); + } + + /** + * Build a substitution while assigning levels to terms. + * The substitution is well-formed when variables are replaced with terms whose + * Free variables have higher levels. + */ + void solve_eqs::extract_subst() { + m_id2level.reset(); + m_id2level.resize(m_id2var.size(), UINT_MAX); + m_subst_ids.reset(); + m_subst = alloc(expr_substitution, m, false, false); + + auto is_explored = [&](unsigned id) { + return m_id2level[id] != UINT_MAX; + }; + + auto is_safe = [&](unsigned lvl, expr* t) { + for (auto* e : subterms::all(expr_ref(t, m))) + if (is_var(e) && m_id2level[var2id(e)] < lvl) + return false; + return true; + }; + + unsigned init_level = UINT_MAX; + unsigned_vector todo; + for (unsigned id = 0; id < m_id2var.size(); ++id) { + if (is_explored(id)) + continue; + // initialize current level to have enough room to assign different levels to all variables. + if (init_level < m_id2var.size() + 1) + return; + init_level -= m_id2var.size() + 1; + unsigned curr_level = init_level; + todo.push_back(id); + while (!todo.empty()) { + unsigned j = todo.back(); + todo.pop_back(); + if (is_explored(j)) + continue; + m_id2level[id] = curr_level++; + for (auto const& eq : m_next[j]) { + auto const& [v, t, d] = eq; + if (!is_safe(curr_level, t)) + continue; + m_next[j][0] = eq; + m_subst_ids.push_back(id); + for (expr* e : subterms::all(expr_ref(t, m))) + if (is_var(e) && !is_explored(var2id(e))) + todo.push_back(var2id(e)); + break; + } + } + } + } + + void solve_eqs::add_subst(dependent_eq const& eq) { + SASSERT(can_be_var(eq.var)); + m_subst->insert(eq.var, eq.term, nullptr, eq.dep); + ++m_stats.m_num_elim_vars; + } + + void solve_eqs::normalize() { + scoped_ptr rp = mk_default_expr_replacer(m, true); + m_subst->reset(); + rp->set_substitution(m_subst.get()); + + std::sort(m_subst_ids.begin(), m_subst_ids.end(), [&](unsigned u, unsigned v) { return m_id2level[u] > m_id2level[v]; }); + + expr_dependency_ref new_dep(m); + expr_ref new_def(m); + proof_ref new_pr(m); + + for (unsigned id : m_subst_ids) { + if (!m.inc()) + break; + auto const& [v, def, dep] = m_next[id][0]; + rp->operator()(def, new_def, new_pr, new_dep); + m_stats.m_num_steps += rp->get_num_steps() + 1; + new_dep = m.mk_join(dep, new_dep); + m_subst->insert(v, new_def, new_pr, new_dep); + // we updated the substitution, but we don't need to reset rp + // because all cached values there do not depend on v. + } + + TRACE("solve_eqs", + tout << "after normalizing variables\n"; + for (unsigned id : m_subst_ids) { + auto const& eq = m_next[id][0]; + expr* def = m_subst->find(eq.var); + tout << mk_pp(eq.var, m) << "\n----->\n" << mk_pp(def, m) << "\n\n"; + }); + } + + void solve_eqs::apply_subst() { + if (!m.inc()) + return; + scoped_ptr rp = mk_default_expr_replacer(m, true); + rp->set_substitution(m_subst.get()); + expr_ref new_f(m); + proof_ref new_pr(m); + expr_dependency_ref new_dep(m); + for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i) { + auto [f, d] = m_fmls[i](); + rp->operator()(f, new_f, new_pr, new_dep); + if (new_f == f) + continue; + new_dep = m.mk_join(d, new_dep); + m_fmls.update(i, dependent_expr(m, new_f, new_dep)); + } + } + + void solve_eqs::reduce() { + + for (extract_eq* ex : m_extract_plugins) + ex->pre_process(m_fmls); + + // TODO add a loop. + dep_eq_vector eqs; + get_eqs(eqs); + extract_dep_graph(eqs); + extract_subst(); + apply_subst(); + advance_qhead(m_fmls.size()); + } + + void solve_eqs::filter_unsafe_vars() { + m_unsafe_vars.reset(); + recfun::util rec(m); + for (func_decl* f : rec.get_rec_funs()) + for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m))) + m_unsafe_vars.mark(term); + } + + typedef generic_model_converter gmc; + + model_converter_ref solve_eqs::get_model_converter() { + model_converter_ref mc = alloc(gmc, m, "solve-eqs"); + for (unsigned id : m_subst_ids) { + auto* v = m_id2var[id]; + static_cast(mc.get())->add(v, m_subst->find(v)); + } + return mc; + } + + solve_eqs::solve_eqs(ast_manager& m, dependent_expr_state& fmls) : + dependent_expr_simplifier(m, fmls), m_rewriter(m) { + register_extract_eqs(m, m_extract_plugins); + } + + void solve_eqs::updt_params(params_ref const& p) { + tactic_params tp(p); + m_config.m_max_occs = p.get_uint("solve_eqs_max_occs", tp.solve_eqs_max_occs()); + m_config.m_context_solve = p.get_bool("context_solve", tp.solve_eqs_context_solve()); + for (auto* ex : m_extract_plugins) + ex->updt_params(p); + } + + void solve_eqs::collect_statistics(statistics& st) const { + st.update("solve-eqs-steps", m_stats.m_num_steps); + st.update("solve-eqs-elim-vars", m_stats.m_num_elim_vars); + } + +} diff --git a/src/ast/simplifiers/solve_eqs.h b/src/ast/simplifiers/solve_eqs.h new file mode 100644 index 000000000..49cd90ca2 --- /dev/null +++ b/src/ast/simplifiers/solve_eqs.h @@ -0,0 +1,84 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + solve_eqs.h + +Abstract: + + simplifier for solving equations + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + + +#pragma once + +#include "util/scoped_ptr_vector.h" +#include "ast/expr_substitution.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/simplifiers/extract_eqs.h" + +namespace euf { + + class solve_eqs : public dependent_expr_simplifier { + struct stats { + unsigned m_num_steps = 0; + unsigned m_num_elim_vars = 0; + }; + struct config { + bool m_context_solve = true; + unsigned m_max_occs = UINT_MAX; + }; + + th_rewriter m_rewriter; + scoped_ptr_vector m_extract_plugins; + unsigned_vector m_var2id, m_id2level, m_subst_ids; + ptr_vector m_id2var; + vector m_next; + scoped_ptr m_subst; + + expr_mark m_unsafe_vars; // expressions that cannot be replaced + stats m_stats; + config m_config; + + void add_subst(dependent_eq const& eq); + + bool is_var(expr* e) const { return e->get_id() < m_var2id.size() && m_var2id[e->get_id()] != UINT_MAX; } + unsigned var2id(expr* v) const { return m_var2id[v->get_id()]; } + + void get_eqs(dep_eq_vector& eqs) { + for (unsigned i = m_qhead; i < m_fmls.size(); ++i) + get_eqs(m_fmls[i], eqs); + } + + void get_eqs(dependent_expr const& f, dep_eq_vector& eqs) { + for (extract_eq* ex : m_extract_plugins) + ex->get_eqs(f, eqs); + } + + void filter_unsafe_vars(); + bool can_be_var(expr* e) const { return is_uninterp_const(e) && !m_unsafe_vars.is_marked(e); } + void extract_subst(); + void extract_dep_graph(dep_eq_vector& eqs); + void normalize(); + void apply_subst(); + + public: + + solve_eqs(ast_manager& m, dependent_expr_state& fmls); + + void push() override { dependent_expr_simplifier::push(); } + void pop(unsigned n) override { dependent_expr_simplifier::pop(n); } + void reduce() override; + + void updt_params(params_ref const& p) override; + void collect_statistics(statistics& st) const override; + + model_converter_ref get_model_converter() override; + }; +} diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index a5c66f78b..2d90b70c3 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -47,7 +47,7 @@ Notes: #include "model/model_v2_pp.h" #include "model/model_params.hpp" #include "tactic/tactic_exception.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "solver/smt_logics.h" #include "cmd_context/basic_cmds.h" #include "cmd_context/cmd_context.h" diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 15b5df0d1..93d2c0d3e 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -33,7 +33,7 @@ Notes: #include "ast/datatype_decl_plugin.h" #include "ast/recfun_decl_plugin.h" #include "ast/rewriter/seq_rewriter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "solver/solver.h" #include "solver/check_logic.h" #include "solver/progress_callback.h" diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index ac7e89d5b..9e7ac75ce 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -1299,7 +1299,7 @@ namespace opt { def result; unsigned_vector div_rows(_div_rows), mod_rows(_mod_rows); SASSERT(!div_rows.empty() || !mod_rows.empty()); - TRACE("opt", display(tout << "solve_div " << x << "\n")); + TRACE("opt", display(tout << "solve_div v" << x << "\n")); rational K(1); for (unsigned ri : div_rows) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 4efe79dd3..c9d2c7797 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -644,6 +644,12 @@ namespace datalog { } void context::add_table_fact(func_decl * pred, const table_fact & fact) { + if (!is_uninterp(pred)) { + std::stringstream strm; + strm << "Predicate " << pred->get_name() << " when used for facts should be uninterpreted"; + throw default_exception(strm.str()); + } + if (get_engine() == DATALOG_ENGINE) { ensure_engine(); m_rel->add_fact(pred, fact); diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index eae846835..3479fef0d 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -30,7 +30,7 @@ Revision History: #include "util/statistics.h" #include "util/params.h" #include "util/trail.h" -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "model/model2expr.h" #include "smt/params/smt_params.h" #include "muz/base/dl_rule_transformer.h" diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index d0c872c3c..a1864d3b9 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -41,7 +41,7 @@ Revision History: #include "ast/rewriter/expr_replacer.h" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/expr_safe_replace.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/scoped_proof.h" #include "ast/datatype_decl_plugin.h" #include "ast/ast_util.h" diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index c9fa2f6b3..6a21a2621 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -23,8 +23,8 @@ Revision History: #include "muz/base/dl_costs.h" #include "muz/base/dl_util.h" #include "ast/used_vars.h" -#include "tactic/proof_converter.h" -#include "tactic/model_converter.h" +#include "ast/converters/proof_converter.h" +#include "ast/converters/model_converter.h" #include "ast/rewriter/ast_counter.h" #include "ast/rewriter/rewriter.h" #include "muz/base/hnf.h" diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h index 46e0b42bf..4688a67fd 100644 --- a/src/muz/base/dl_util.h +++ b/src/muz/base/dl_util.h @@ -18,13 +18,14 @@ Revision History: --*/ #pragma once + #include #include "ast/ast.h" #include "util/hashtable.h" #include "util/obj_hashtable.h" #include "util/uint_set.h" -#include "tactic/horn_subsume_model_converter.h" -#include "tactic/replace_proof_converter.h" +#include "ast/converters/horn_subsume_model_converter.h" +#include "ast/converters/replace_proof_converter.h" #include "ast/substitution/substitution.h" #include "ast/rewriter/ast_counter.h" #include "util/statistics.h" diff --git a/src/muz/base/hnf.h b/src/muz/base/hnf.h index 45b651b56..0df0269d9 100644 --- a/src/muz/base/hnf.h +++ b/src/muz/base/hnf.h @@ -27,7 +27,7 @@ Copyright (c) 2015 Microsoft Corporation #include "ast/ast.h" #include "util/params.h" #include "ast/normal_forms/defined_names.h" -#include "tactic/proof_converter.h" +#include "ast/converters/proof_converter.h" class hnf { class imp; diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 560202ab3..1a58bc92b 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -20,9 +20,9 @@ Revision History: #include "ast/rewriter/var_subst.h" #include "ast/rewriter/expr_replacer.h" #include "tactic/tactical.h" -#include "tactic/model_converter.h" -#include "tactic/proof_converter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/model_converter.h" +#include "ast/converters/proof_converter.h" +#include "ast/converters/generic_model_converter.h" #include "muz/fp/horn_tactic.h" #include "muz/base/dl_context.h" #include "muz/fp/dl_register_engine.h" diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index e8d769621..470901a96 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -28,7 +28,7 @@ Revision History: #include "ast/expr_abstract.h" #include "model/model2expr.h" #include "model/model_smt2_pp.h" -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "smt/smt_solver.h" namespace spacer { diff --git a/src/muz/transforms/dl_mk_array_blast.h b/src/muz/transforms/dl_mk_array_blast.h index 6d1a69825..352c8a248 100644 --- a/src/muz/transforms/dl_mk_array_blast.h +++ b/src/muz/transforms/dl_mk_array_blast.h @@ -22,9 +22,9 @@ Revision History: #include "muz/base/dl_rule_set.h" #include "muz/base/dl_rule_transformer.h" #include "muz/transforms/dl_mk_interp_tail_simplifier.h" -#include "tactic/equiv_proof_converter.h" #include "ast/array_decl_plugin.h" #include "ast/rewriter/expr_safe_replace.h" +#include "ast/converters/equiv_proof_converter.h" namespace datalog { diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 070432e52..439cb4540 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -22,7 +22,7 @@ Revision History: #include "ast/rewriter/rewriter_def.h" #include "ast/ast_pp.h" #include "ast/rewriter/expr_safe_replace.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "muz/transforms/dl_mk_interp_tail_simplifier.h" #include "muz/base/fp_params.hpp" #include "ast/scoped_proof.h" diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index ba85e569a..73541b0cd 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -21,7 +21,7 @@ Author: #include "muz/dataflow/dataflow.h" #include "muz/dataflow/reachability.h" #include "ast/ast_pp.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/ast_util.h" namespace datalog { diff --git a/src/muz/transforms/dl_mk_elim_term_ite.h b/src/muz/transforms/dl_mk_elim_term_ite.h index 11bfb8f23..98acd12f1 100644 --- a/src/muz/transforms/dl_mk_elim_term_ite.h +++ b/src/muz/transforms/dl_mk_elim_term_ite.h @@ -21,7 +21,7 @@ Revision History: #include "muz/base/dl_context.h" #include "muz/base/dl_rule_set.h" #include "muz/base/dl_rule_transformer.h" -#include "tactic/equiv_proof_converter.h" +#include "ast/converters/equiv_proof_converter.h" namespace datalog { class mk_elim_term_ite : public rule_transformer::plugin { diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index b91b9e5c8..e8b1f4001 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -25,7 +25,7 @@ Revision History: #include "ast/rewriter/rewriter_def.h" #include "muz/transforms/dl_mk_subsumption_checker.h" #include "muz/base/fp_params.hpp" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" namespace datalog { diff --git a/src/nlsat/tactic/goal2nlsat.h b/src/nlsat/tactic/goal2nlsat.h index 8dda03105..52b975cc2 100644 --- a/src/nlsat/tactic/goal2nlsat.h +++ b/src/nlsat/tactic/goal2nlsat.h @@ -24,7 +24,7 @@ Notes: #pragma once #include "nlsat/nlsat_types.h" -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" class goal; class expr2var; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index ba31d74cf..5895643bd 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -39,7 +39,7 @@ Notes: #include "tactic/arith/card2bv_tactic.h" #include "tactic/arith/eq2bv_tactic.h" #include "tactic/bv/dt2bv_tactic.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ackermannization/ackermannize_bv_tactic.h" #include "sat/sat_solver/inc_sat_solver.h" #include "sat/sat_params.hpp" diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index a93400592..9e61ae92c 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -20,7 +20,7 @@ Notes: #include "ast/ast.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "tactic/tactic.h" #include "qe/qsat.h" #include "opt/opt_solver.h" diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index bd83f06c8..84d31ed0f 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -29,7 +29,7 @@ Notes: #include "smt/params/smt_params.h" #include "smt/smt_types.h" #include "smt/theory_opt.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" namespace opt { diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index da25e2285..28448fbe4 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -24,7 +24,7 @@ Notes: #include "smt/smt_context.h" #include "opt/opt_context.h" #include "util/sorting_network.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" namespace opt { diff --git a/src/params/CMakeLists.txt b/src/params/CMakeLists.txt index f420ddd6d..cdc21da97 100644 --- a/src/params/CMakeLists.txt +++ b/src/params/CMakeLists.txt @@ -16,6 +16,7 @@ z3_add_component(params rewriter_params.pyg seq_rewriter_params.pyg solver_params.pyg + tactic_params.pyg EXTRA_REGISTER_MODULE_HEADERS context_params.h ) diff --git a/src/tactic/tactic_params.pyg b/src/params/tactic_params.pyg similarity index 100% rename from src/tactic/tactic_params.pyg rename to src/params/tactic_params.pyg diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index e97eb4ef7..5d9d3c19c 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -421,15 +421,23 @@ namespace mbp { mbo.display(tout);); vector defs = mbo.project(real_vars.size(), real_vars.data(), compute_def); + vector rows; + u_map def_vars; mbo.get_live_rows(rows); - rows2fmls(rows, index2expr, fmls); + for (row const& r : rows) { + if (r.m_type == opt::t_mod) + def_vars.insert(r.m_id, r); + else if (r.m_type == opt::t_div) + def_vars.insert(r.m_id, r); + } + rows2fmls(def_vars, rows, index2expr, fmls); TRACE("qe", mbo.display(tout << "mbo result\n"); for (auto const& d : defs) tout << "def: " << d << "\n"; tout << fmls << "\n";); if (compute_def) - optdefs2mbpdef(defs, index2expr, real_vars, result); + optdefs2mbpdef(def_vars, defs, index2expr, real_vars, result); if (m_apply_projection && !apply_projection(eval, result, fmls)) return false; @@ -442,7 +450,7 @@ namespace mbp { return true; } - void optdefs2mbpdef(vector const& defs, ptr_vector const& index2expr, unsigned_vector const& real_vars, vector& result) { + void optdefs2mbpdef(u_map const& def_vars, vector const& defs, ptr_vector const& index2expr, unsigned_vector const& real_vars, vector& result) { SASSERT(defs.size() == real_vars.size()); for (unsigned i = 0; i < defs.size(); ++i) { auto const& d = defs[i]; @@ -450,8 +458,12 @@ namespace mbp { bool is_int = a.is_int(x); expr_ref_vector ts(m); expr_ref t(m); - for (var const& v : d.m_vars) - ts.push_back(var2expr(index2expr, v)); + for (var const& v : d.m_vars) { + t = id2expr(def_vars, index2expr, v.m_id); + if (v.m_coeff != 1) + t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t); + ts.push_back(t); + } if (!d.m_coeff.is_zero()) ts.push_back(a.mk_numeral(d.m_coeff, is_int)); if (ts.empty()) @@ -492,7 +504,8 @@ namespace mbp { t = a.mk_int(mod(r.m_coeff, r.m_mod)); return t; } - ts.push_back(a.mk_int(r.m_coeff)); + if (r.m_coeff != 0) + ts.push_back(a.mk_int(r.m_coeff)); t = mk_add(ts); t = a.mk_mod(t, a.mk_int(r.m_mod)); return t; @@ -501,7 +514,8 @@ namespace mbp { t = a.mk_int(div(r.m_coeff, r.m_mod)); return t; } - ts.push_back(a.mk_int(r.m_coeff)); + if (r.m_coeff != 0) + ts.push_back(a.mk_int(r.m_coeff)); t = mk_add(ts); t = a.mk_idiv(t, a.mk_int(r.m_mod)); return t; @@ -513,15 +527,7 @@ namespace mbp { } } - void rows2fmls(vector const& rows, ptr_vector const& index2expr, expr_ref_vector& fmls) { - - u_map def_vars; - for (row const& r : rows) { - if (r.m_type == opt::t_mod) - def_vars.insert(r.m_id, r); - else if (r.m_type == opt::t_div) - def_vars.insert(r.m_id, r); - } + void rows2fmls(u_map& def_vars, vector const& rows, ptr_vector const& index2expr, expr_ref_vector& fmls) { for (row const& r : rows) { expr_ref t(m), s(m), val(m); diff --git a/src/qe/qsat.h b/src/qe/qsat.h index 381d244e1..2f7502a67 100644 --- a/src/qe/qsat.h +++ b/src/qe/qsat.h @@ -21,7 +21,7 @@ Revision History: #pragma once #include "tactic/tactic.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "qe/qe_mbp.h" namespace qe { diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index bbdedab86..8da933fb2 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -64,9 +64,6 @@ namespace sat { } TRACE("cleanup_bug", tout << "keeping: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";); break; -#if ENABLE_TERNARY - case watched::TERNARY: -#endif case watched::CLAUSE: // skip break; diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 1c54d6f97..512ec8424 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -265,6 +265,7 @@ namespace sat { m_xor_gauss_max_matrix_columns = p.xor_gauss_max_matrix_columns(); m_xor_gauss_max_num_matrices = p.xor_gauss_max_num_matrices(); m_xor_gauss_force_use_all_matrices = p.xor_gauss_force_use_all_matrices(); + m_xor_gauss_min_usefulness_cutoff = p.xor_gauss_min_usefulness_cutoff(); sat_simplifier_params ssp(_p); m_elim_vars = ssp.elim_vars(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index f8ea7b6dc..13e9a08d7 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -208,6 +208,12 @@ namespace sat { unsigned m_xor_gauss_max_matrix_columns; unsigned m_xor_gauss_max_num_matrices; bool m_xor_gauss_force_use_all_matrices; + double m_xor_gauss_min_usefulness_cutoff; + + const bool m_xor_gauss_doMatrixFind = true; + const unsigned m_xor_gauss_min_clauses = 2; + const unsigned m_xor_gauss_max_clauses = 500000; + const unsigned m_xor_gauss_var_per_cut = 2; config(params_ref const & p); diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 306ff2493..46a608151 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -445,10 +445,6 @@ namespace sat { return false; case justification::BINARY: return contains(c, j.get_literal()); -#if ENABLE_TERNARY - case justification::TERNARY: - return contains(c, j.get_literal1(), j.get_literal2()); -#endif case justification::CLAUSE: return contains(s.get_clause(j)); default: diff --git a/src/sat/sat_gc.cpp b/src/sat/sat_gc.cpp index ab9bc8857..a655956db 100644 --- a/src/sat/sat_gc.cpp +++ b/src/sat/sat_gc.cpp @@ -178,33 +178,9 @@ namespace sat { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";); } -#if ENABLE_TERNARY - bool solver::can_delete3(literal l1, literal l2, literal l3) const { - if (value(l1) == l_true && - value(l2) == l_false && - value(l3) == l_false) { - justification const& j = m_justification[l1.var()]; - if (j.is_ternary_clause()) { - watched w1(l2, l3); - watched w2(j.get_literal1(), j.get_literal2()); - return w1 != w2; - } - } - return true; - } -#endif - bool solver::can_delete(clause const & c) const { if (c.on_reinit_stack()) return false; -#if ENABLE_TERNARY - if (c.size() == 3) { - return - can_delete3(c[0],c[1],c[2]) && - can_delete3(c[1],c[0],c[2]) && - can_delete3(c[2],c[0],c[1]); - } -#endif literal l0 = c[0]; if (value(l0) != l_true) return true; diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index a6086d8a7..223e58677 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -26,13 +26,6 @@ namespace sat { integrity_checker::integrity_checker(solver const & _s): s(_s) { } - -#if ENABLE_TERNARY - // for ternary clauses - static bool contains_watched(watch_list const & wlist, literal l1, literal l2) { - return wlist.contains(watched(l1, l2)); - } -#endif // for nary clauses static bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) { @@ -65,18 +58,6 @@ namespace sat { if (c.frozen()) return true; -#if ENABLE_TERNARY - if (c.size() == 3) { - CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n"; - tout << "watch_list:\n"; - s.display_watch_list(tout, s.get_wlist(~c[0])); - tout << "\n";); - VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2])); - VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2])); - VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1])); - return true; - } -#endif { if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) { bool on_prop_stack = false; @@ -174,13 +155,6 @@ namespace sat { tout << "\n";); VERIFY(find_binary_watch(s.get_wlist(~(w.get_literal())), l)); break; -#if ENABLE_TERNARY - case watched::TERNARY: - VERIFY(!s.was_eliminated(w.get_literal1().var())); - VERIFY(!s.was_eliminated(w.get_literal2().var())); - VERIFY(w.get_literal1().index() < w.get_literal2().index()); - break; -#endif case watched::CLAUSE: VERIFY(!s.get_clause(w.get_clause_offset()).was_removed()); break; diff --git a/src/sat/sat_justification.h b/src/sat/sat_justification.h index 1fc97a38c..f83173aa7 100644 --- a/src/sat/sat_justification.h +++ b/src/sat/sat_justification.h @@ -22,11 +22,7 @@ namespace sat { class justification { public: - enum kind { NONE = 0, BINARY = 1, -#if ENABLE_TERNARY - TERNARY = 2, -#endif - CLAUSE = 3, EXT_JUSTIFICATION = 4}; + enum kind { NONE = 0, BINARY = 1, CLAUSE = 2, EXT_JUSTIFICATION = 3}; private: unsigned m_level; size_t m_val1; @@ -36,9 +32,7 @@ namespace sat { public: justification(unsigned lvl):m_level(lvl), m_val1(0), m_val2(NONE) {} explicit justification(unsigned lvl, literal l):m_level(lvl), m_val1(l.to_uint()), m_val2(BINARY) {} -#if ENABLE_TERNARY - justification(unsigned lvl, literal l1, literal l2):m_level(lvl), m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {} -#endif + explicit justification(unsigned lvl, clause_offset cls_off):m_level(lvl), m_val1(cls_off), m_val2(CLAUSE) {} static justification mk_ext_justification(unsigned lvl, ext_justification_idx idx) { return justification(lvl, idx, EXT_JUSTIFICATION); } @@ -51,12 +45,6 @@ namespace sat { bool is_binary_clause() const { return m_val2 == BINARY; } literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(val1()); } -#if ENABLE_TERNARY - bool is_ternary_clause() const { return get_kind() == TERNARY; } - literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(val1()); } - literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); } -#endif - bool is_clause() const { return m_val2 == CLAUSE; } clause_offset get_clause_offset() const { return m_val1; } @@ -73,11 +61,6 @@ namespace sat { case justification::BINARY: out << "binary " << j.get_literal(); break; -#if ENABLE_TERNARY - case justification::TERNARY: - out << "ternary " << j.get_literal1() << " " << j.get_literal2(); - break; -#endif case justification::CLAUSE: out << "clause"; break; diff --git a/src/sat/sat_lut_finder.cpp b/src/sat/sat_lut_finder.cpp index 5459ab2a4..60143f91c 100644 --- a/src/sat/sat_lut_finder.cpp +++ b/src/sat/sat_lut_finder.cpp @@ -124,8 +124,8 @@ namespace sat { } bool lut_finder::extract_lut(literal l1, literal l2) { - SASSERT(s.is_visited(l1.var())); - SASSERT(s.is_visited(l2.var())); + SASSERT(s.m_visited.is_visited(l1.var())); + SASSERT(s.m_visited.is_visited(l2.var())); m_missing.reset(); unsigned mask = 0; for (unsigned i = 0; i < m_vars.size(); ++i) { diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index d02513f06..9ee8889ab 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -135,13 +135,13 @@ def_module_params('sat', # ('xor.allow_elim_vars', BOOL, 'tbd'), # ('xor.var_per_cut', UINT, 'tbd'), # ('xor.force_preserve_xors', BOOL, 'tbd'), - ('xor.gauss.max_matrix_columns', UINT, UINT_MAX, 'tbd'), - ('xor.gauss.max_matrix_rows', UINT, UINT_MAX, 'The maximum matrix size -- no. of rows'), - ('xor.gauss.min_matrix_rows', UINT, 0, 'The minimum matrix size -- no. of rows'), - ('xor.gauss.max_num_matrices', UINT, UINT_MAX, 'Maximum number of matrices'), + ('xor.gauss.max_matrix_columns', UINT, 1000, 'tbd'), + ('xor.gauss.max_matrix_rows', UINT, 2000, 'The maximum matrix size -- no. of rows'), + ('xor.gauss.min_matrix_rows', UINT, 3, 'The minimum matrix size -- no. of rows'), + ('xor.gauss.max_num_matrices', UINT, 5, 'Maximum number of matrices'), ('xor.gauss.force_use_all_matrices', BOOL, True, 'tbd'), # ('xor.gauss.autodisable', BOOL, False, 'tbd'), - # ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0, 'tbd'), + ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0.2, 'tbd'), # ('xor.gauss.do_matrix_find', BOOL, True, 'tbd'), # ('xor.gauss.min_xor_clauses', UINT, 2, 'tbd'), # ('xor.gauss.max_xor_clauses, UINT, 500000, 'tbd') diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp index 4c4b9ecaf..df55aecd7 100644 --- a/src/sat/sat_proof_trim.cpp +++ b/src/sat/sat_proof_trim.cpp @@ -125,10 +125,6 @@ namespace sat { in_coi |= m_in_coi.contains(lit.index()); else if (js.is_binary_clause()) in_coi = m_in_coi.contains(js.get_literal().index()); -#if ENABLE_TERNARY - else if (js.is_ternary_clause()) - in_coi = m_in_coi.contains(js.get_literal1().index()) || m_in_coi.contains(js.get_literal2().index()); -#endif else UNREACHABLE(); // approach does not work for external justifications @@ -226,12 +222,6 @@ namespace sat { case justification::BINARY: add_dependency(j.get_literal()); break; -#if ENABLE_TERNARY - case justification::TERNARY: - add_dependency(j.get_literal1()); - add_dependency(j.get_literal2()); - break; -#endif case justification::CLAUSE: for (auto lit : s.get_clause(j)) if (s.value(lit) == l_false) @@ -262,13 +252,6 @@ namespace sat { m_clause.push_back(l); m_clause.push_back(j.get_literal()); break; -#if ENABLE_TERNARY - case justification::TERNARY: - m_clause.push_back(l); - m_clause.push_back(j.get_literal1()); - m_clause.push_back(j.get_literal2()); - break; -#endif case justification::CLAUSE: s.get_clause(j).mark_used(); IF_VERBOSE(3, verbose_stream() << "add core " << s.get_clause(j) << "\n"); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index b67ef6a2a..9ba536091 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -271,9 +271,6 @@ namespace sat { watch_list::iterator end2 = wlist.end(); for (; it2 != end2; ++it2) { switch (it2->get_kind()) { -#if ENABLE_TERNARY - case watched::TERNARY: -#endif case watched::CLAUSE: // consume break; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index c9a092c1b..2566e1be9 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -454,10 +454,6 @@ namespace sat { if (redundant && m_par) m_par->share_clause(*this, lits[0], lits[1]); return nullptr; -#if ENABLE_TERNARY - case 3: - return mk_ter_clause(lits, st); -#endif default: return mk_nary_clause(num_lits, lits, st); } @@ -551,58 +547,6 @@ namespace sat { m_clauses_to_reinit.push_back(clause_wrapper(l1, l2)); } -#if ENABLE_TERNARY - clause * solver::mk_ter_clause(literal * lits, sat::status st) { - VERIFY(ENABLE_TERNARY); - m_stats.m_mk_ter_clause++; - clause * r = alloc_clause(3, lits, st.is_redundant()); - bool reinit = attach_ter_clause(*r, st); - if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r); - if (st.is_redundant()) - m_learned.push_back(r); - else - m_clauses.push_back(r); - for (literal l : *r) { - m_touched[l.var()] = m_touch_index; - } - return r; - } - - bool solver::attach_ter_clause(clause & c, sat::status st) { - VERIFY(ENABLE_TERNARY); - bool reinit = false; - if (m_config.m_drat) m_drat.add(c, st); - TRACE("sat_verbose", tout << c << "\n";); - SASSERT(!c.was_removed()); - m_watches[(~c[0]).index()].push_back(watched(c[1], c[2])); - m_watches[(~c[1]).index()].push_back(watched(c[0], c[2])); - m_watches[(~c[2]).index()].push_back(watched(c[0], c[1])); - if (!at_base_lvl()) - reinit = propagate_ter_clause(c); - return reinit; - } - - bool solver::propagate_ter_clause(clause& c) { - bool reinit = false; - if (value(c[1]) == l_false && value(c[2]) == l_false) { - m_stats.m_ter_propagate++; - assign(c[0], justification(std::max(lvl(c[1]), lvl(c[2])), c[1], c[2])); - reinit = !c.is_learned(); - } - else if (value(c[0]) == l_false && value(c[2]) == l_false) { - m_stats.m_ter_propagate++; - assign(c[1], justification(std::max(lvl(c[0]), lvl(c[2])), c[0], c[2])); - reinit = !c.is_learned(); - } - else if (value(c[0]) == l_false && value(c[1]) == l_false) { - m_stats.m_ter_propagate++; - assign(c[2], justification(std::max(lvl(c[0]), lvl(c[1])), c[0], c[1])); - reinit = !c.is_learned(); - } - return reinit; - } -#endif - clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) { m_stats.m_mk_clause++; clause * r = alloc_clause(num_lits, lits, st.is_redundant()); @@ -669,13 +613,7 @@ namespace sat { void solver::attach_clause(clause & c, bool & reinit) { SASSERT(c.size() > 2); - reinit = false; -#if ENABLE_TERNARY - if (ENABLE_TERNARY && c.size() == 3) - reinit = attach_ter_clause(c, c.is_learned() ? sat::status::redundant() : sat::status::asserted()); - else -#endif - reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack()); + reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack()); } void solver::set_learned(clause& c, bool redundant) { @@ -923,12 +861,6 @@ namespace sat { } void solver::detach_clause(clause& c) { -#if ENABLE_TERNARY - if (c.size() == 3) { - detach_ter_clause(c); - return; - } -#endif detach_nary_clause(c); } @@ -938,14 +870,6 @@ namespace sat { erase_clause_watch(get_wlist(~c[1]), cls_off); } -#if ENABLE_TERNARY - void solver::detach_ter_clause(clause & c) { - erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]); - erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]); - erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]); - } -#endif - // ----------------------- // // Basic @@ -1129,31 +1053,6 @@ namespace sat { *it2 = *it; it2++; break; -#if ENABLE_TERNARY - case watched::TERNARY: { - lbool val1, val2; - l1 = it->get_literal1(); - l2 = it->get_literal2(); - val1 = value(l1); - val2 = value(l2); - if (val1 == l_false && val2 == l_undef) { - m_stats.m_ter_propagate++; - assign_core(l2, justification(std::max(curr_level, lvl(l1)), l1, not_l)); - } - else if (val1 == l_undef && val2 == l_false) { - m_stats.m_ter_propagate++; - assign_core(l1, justification(std::max(curr_level, lvl(l2)), l2, not_l)); - } - else if (val1 == l_false && val2 == l_false) { - CONFLICT_CLEANUP(); - set_conflict(justification(std::max(curr_level, lvl(l1)), l1, not_l), ~l2); - return false; - } - *it2 = *it; - it2++; - break; - } -#endif case watched::CLAUSE: { if (value(it->get_blocked_literal()) == l_true) { TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n"; @@ -2540,12 +2439,6 @@ namespace sat { case justification::BINARY: process_antecedent(~(js.get_literal()), num_marks); break; -#if ENABLE_TERNARY - case justification::TERNARY: - process_antecedent(~(js.get_literal1()), num_marks); - process_antecedent(~(js.get_literal2()), num_marks); - break; -#endif case justification::CLAUSE: { clause & c = get_clause(js); unsigned i = 0; @@ -2724,13 +2617,6 @@ namespace sat { SASSERT(consequent != null_literal); process_antecedent_for_unsat_core(~(js.get_literal())); break; -#if ENABLE_TERNARY - case justification::TERNARY: - SASSERT(consequent != null_literal); - process_antecedent_for_unsat_core(~(js.get_literal1())); - process_antecedent_for_unsat_core(~(js.get_literal2())); - break; -#endif case justification::CLAUSE: { clause & c = get_clause(js); unsigned i = 0; @@ -2867,12 +2753,6 @@ namespace sat { case justification::BINARY: level = update_max_level(js.get_literal(), level, unique_max); return level; -#if ENABLE_TERNARY - case justification::TERNARY: - level = update_max_level(js.get_literal1(), level, unique_max); - level = update_max_level(js.get_literal2(), level, unique_max); - return level; -#endif case justification::CLAUSE: for (literal l : get_clause(js)) level = update_max_level(l, level, unique_max); @@ -3224,15 +3104,6 @@ namespace sat { return false; } break; -#if ENABLE_TERNARY - case justification::TERNARY: - if (!process_antecedent_for_minimization(~(js.get_literal1())) || - !process_antecedent_for_minimization(~(js.get_literal2()))) { - reset_unmark(old_size); - return false; - } - break; -#endif case justification::CLAUSE: { clause & c = get_clause(js); unsigned i = 0; @@ -3388,12 +3259,6 @@ namespace sat { case justification::BINARY: update_lrb_reasoned(js.get_literal()); break; -#if ENABLE_TERNARY - case justification::TERNARY: - update_lrb_reasoned(js.get_literal1()); - update_lrb_reasoned(js.get_literal2()); - break; -#endif case justification::CLAUSE: { clause & c = get_clause(js); for (literal l : c) { @@ -3463,20 +3328,6 @@ namespace sat { unmark_lit(~l2); } } -#if ENABLE_TERNARY - else if (w.is_ternary_clause()) { - literal l2 = w.get_literal1(); - literal l3 = w.get_literal2(); - if (is_marked_lit(l2) && is_marked_lit(~l3) && l0 != ~l3) { - // eliminate ~l3 from lemma because we have the clause l \/ l2 \/ l3 - unmark_lit(~l3); - } - else if (is_marked_lit(~l2) && is_marked_lit(l3) && l0 != ~l2) { - // eliminate ~l2 from lemma because we have the clause l \/ l2 \/ l3 - unmark_lit(~l2); - } - } -#endif else { // May miss some binary/ternary clauses, but that is ok. // I sort the watch lists at every simplification round. @@ -3599,7 +3450,7 @@ namespace sat { mark_visited(cw[j].var()); } for (literal lit : m_lemma) - mark_visited(lit.var()); + mark_visited(lit.var()); auto is_active = [&](bool_var v) { return value(v) != l_undef && lvl(v) <= new_lvl; @@ -3741,17 +3592,6 @@ namespace sat { } else { clause & c = *(cw.get_clause()); -#if ENABLE_TERNARY - if (ENABLE_TERNARY && c.size() == 3) { - if (propagate_ter_clause(c) && !at_base_lvl()) - m_clauses_to_reinit[j++] = cw; - else if (has_variables_to_reinit(c) && !at_base_lvl()) - m_clauses_to_reinit[j++] = cw; - else - c.set_reinit_stack(false); - continue; - } -#endif detach_clause(c); attach_clause(c, reinit); if (reinit && !at_base_lvl()) @@ -4018,12 +3858,6 @@ namespace sat { case justification::BINARY: out << "binary " << js.get_literal() << "@" << lvl(js.get_literal()); break; -#if ENABLE_TERNARY - case justification::TERNARY: - out << "ternary " << js.get_literal1() << "@" << lvl(js.get_literal1()) << " "; - out << js.get_literal2() << "@" << lvl(js.get_literal2()); - break; -#endif case justification::CLAUSE: { out << "("; bool first = true; @@ -4683,24 +4517,14 @@ namespace sat { if (!check_domain(lit, ~js.get_literal())) return false; s |= m_antecedents.find(js.get_literal().var()); break; -#if ENABLE_TERNARY - case justification::TERNARY: - if (!check_domain(lit, ~js.get_literal1()) || - !check_domain(lit, ~js.get_literal2())) return false; - s |= m_antecedents.find(js.get_literal1().var()); - s |= m_antecedents.find(js.get_literal2().var()); - break; -#endif case justification::CLAUSE: { clause & c = get_clause(js); for (literal l : c) { if (l != lit) { - if (check_domain(lit, ~l) && all_found) { - s |= m_antecedents.find(l.var()); - } - else { - all_found = false; - } + if (check_domain(lit, ~l) && all_found) + s |= m_antecedents.find(l.var()); + else + all_found = false; } } break; @@ -4735,12 +4559,11 @@ namespace sat { bool solver::extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq) { index_set s; - if (m_antecedents.contains(lit.var())) { + if (m_antecedents.contains(lit.var())) return true; - } - if (assumptions.contains(lit)) { - s.insert(lit.index()); - } + + if (assumptions.contains(lit)) + s.insert(lit.index()); else { if (!extract_assumptions(lit, s)) { SASSERT(!m_todo_antecedents.empty()); @@ -4812,7 +4635,7 @@ namespace sat { clause_vector const & cs = *(vs[i]); for (clause* cp : cs) { clause & c = *cp; - if (ENABLE_TERNARY && c.size() == 3) + if (c.size() == 3) num_ter++; else num_cls++; @@ -4899,22 +4722,4 @@ namespace sat { return true; } - void solver::init_ts(unsigned n, svector& v, unsigned& ts) { - if (v.empty()) - ts = 0; - - ts++; - if (ts == 0) { - ts = 1; - v.reset(); - } - while (v.size() < n) - v.push_back(0); - } - - void solver::init_visited() { - init_ts(2 * num_vars(), m_visited, m_visited_ts); - } - - }; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 639b07a73..e29a7bcc2 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -28,6 +28,7 @@ Revision History: #include "util/rlimit.h" #include "util/scoped_ptr_vector.h" #include "util/scoped_limit_trail.h" +#include "util/visit_helper.h" #include "sat/sat_types.h" #include "sat/sat_clause.h" #include "sat/sat_watched.h" @@ -51,6 +52,10 @@ namespace pb { class solver; }; +namespace xr { + class solver; +}; + namespace sat { /** @@ -176,8 +181,7 @@ namespace sat { std::string m_reason_unknown; bool m_trim = false; - svector m_visited; - unsigned m_visited_ts; + visit_helper m_visited; struct scope { unsigned m_trail_lim; @@ -221,6 +225,7 @@ namespace sat { friend class simplifier; friend class scc; friend class pb::solver; + friend class xr::solver; friend class anf_simplifier; friend class cut_simplifier; friend class parallel; @@ -307,11 +312,6 @@ namespace sat { void mk_bin_clause(literal l1, literal l2, sat::status st); void mk_bin_clause(literal l1, literal l2, bool learned) { mk_bin_clause(l1, l2, learned ? sat::status::redundant() : sat::status::asserted()); } bool propagate_bin_clause(literal l1, literal l2); -#if ENABLE_TERNARY - clause * mk_ter_clause(literal * lits, status st); - bool attach_ter_clause(clause & c, status st); - bool propagate_ter_clause(clause& c); -#endif clause * mk_nary_clause(unsigned num_lits, literal * lits, status st); bool has_variables_to_reinit(clause const& c) const; bool has_variables_to_reinit(literal l1, literal l2) const; @@ -347,16 +347,16 @@ namespace sat { void detach_bin_clause(literal l1, literal l2, bool learned); void detach_clause(clause & c); void detach_nary_clause(clause & c); - void detach_ter_clause(clause & c); void push_reinit_stack(clause & c); void push_reinit_stack(literal l1, literal l2); - - void init_ts(unsigned n, svector& v, unsigned& ts); - void init_visited(); - void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; } + + void init_visited(unsigned lim = 1) { m_visited.init_visited(2 * num_vars(), lim); } + bool is_visited(sat::bool_var v) const { return is_visited(literal(v, false)); } + bool is_visited(literal lit) const { return m_visited.is_visited(lit.index()); } + unsigned num_visited(bool_var v) const { return m_visited.num_visited(v); } + void mark_visited(literal lit) { m_visited.mark_visited(lit.index()); } void mark_visited(bool_var v) { mark_visited(literal(v, false)); } - bool is_visited(bool_var v) const { return is_visited(literal(v, false)); } - bool is_visited(literal l) const { return m_visited[l.index()] == m_visited_ts; } + void inc_visited(bool_var v) { m_visited.inc_visited(v); } bool all_distinct(literal_vector const& lits); bool all_distinct(clause const& cl); diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 7c4e4fb73..4e119a2ae 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -34,8 +34,6 @@ class params_ref; class reslimit; class statistics; -#define ENABLE_TERNARY false - namespace sat { #define SAT_VB_LVL 10 diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp index dedbf45f0..5573212f5 100644 --- a/src/sat/sat_watched.cpp +++ b/src/sat/sat_watched.cpp @@ -71,34 +71,6 @@ namespace sat { VERIFY(found); } -#if ENABLE_TERNARY - void erase_ternary_watch(watch_list& wlist, literal l1, literal l2) { - watched w(l1, l2); - watch_list::iterator it = wlist.begin(), end = wlist.end(); - watch_list::iterator it2 = it; - bool found = false; - for (; it != end; ++it) { - if (!found && w == *it) { - found = true; - } - else { - *it2 = *it; - ++it2; - } - } - wlist.set_end(it2); -#if 0 - VERIFY(found); - for (watched const& w2 : wlist) { - if (w2 == w) { - std::cout << l1 << " " << l2 << "\n"; - } - //VERIFY(w2 != w); - } -#endif - } -#endif - void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) { watch_list::iterator end = wlist.end(); for (; it != end; ++it, ++it2) @@ -120,11 +92,6 @@ namespace sat { if (w.is_learned()) out << "*"; break; -#if ENABLE_TERNARY - case watched::TERNARY: - out << "(" << w.get_literal1() << " " << w.get_literal2() << ")"; - break; -#endif case watched::CLAUSE: out << "(" << w.get_blocked_literal() << " " << *(ca.get_clause(w.get_clause_offset())) << ")"; break; diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index 7e88c8c51..6d91434db 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -40,11 +40,7 @@ namespace sat { class watched { public: enum kind { - BINARY = 0, -#if ENABLE_TERNARY - TERNARY, -#endif - CLAUSE, EXT_CONSTRAINT + BINARY = 0, CLAUSE, EXT_CONSTRAINT }; private: size_t m_val1; @@ -59,18 +55,6 @@ namespace sat { SASSERT(learned || is_binary_non_learned_clause()); } -#if ENABLE_TERNARY - watched(literal l1, literal l2) { - SASSERT(l1 != l2); - if (l1.index() > l2.index()) - std::swap(l1, l2); - m_val1 = l1.to_uint(); - m_val2 = static_cast(TERNARY) + (l2.to_uint() << 2); - SASSERT(is_ternary_clause()); - SASSERT(get_literal1() == l1); - SASSERT(get_literal2() == l2); - } -#endif unsigned val2() const { return m_val2; } @@ -101,11 +85,6 @@ namespace sat { void set_learned(bool l) { if (l) m_val2 |= 4u; else m_val2 &= ~4u; SASSERT(is_learned() == l); } -#if ENABLE_TERNARY - bool is_ternary_clause() const { return get_kind() == TERNARY; } - literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast(m_val1)); } - literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); } -#endif bool is_clause() const { return get_kind() == CLAUSE; } clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast(m_val1); } @@ -124,21 +103,14 @@ namespace sat { bool operator!=(watched const & w) const { return !operator==(w); } }; - static_assert(0 <= watched::BINARY && watched::BINARY <= 3, ""); -#if ENABLE_TERNARY - static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, ""); -#endif - static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, ""); - static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, ""); + static_assert(0 <= watched::BINARY && watched::BINARY <= 2, ""); + static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 2, ""); + static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 2, ""); struct watched_lt { bool operator()(watched const & w1, watched const & w2) const { if (w2.is_binary_clause()) return false; if (w1.is_binary_clause()) return true; -#if ENABLE_TERNARY - if (w2.is_ternary_clause()) return false; - if (w1.is_ternary_clause()) return true; -#endif return false; } }; @@ -148,8 +120,6 @@ namespace sat { watched* find_binary_watch(watch_list & wlist, literal l); watched const* find_binary_watch(watch_list const & wlist, literal l); bool erase_clause_watch(watch_list & wlist, clause_offset c); - void erase_ternary_watch(watch_list & wlist, literal l1, literal l2); - void set_ternary_learned(watch_list& wlist, literal l1, literal l2, bool learned); class clause_allocator; std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext); diff --git a/src/sat/sat_xor_finder.cpp b/src/sat/sat_xor_finder.cpp index dbe08d96c..826acf5f3 100644 --- a/src/sat/sat_xor_finder.cpp +++ b/src/sat/sat_xor_finder.cpp @@ -107,7 +107,6 @@ namespace sat { m_combination |= (1 << mask); } - void xor_finder::add_xor(bool parity, clause& c) { DEBUG_CODE(for (clause* cp : m_clauses_to_remove) VERIFY(cp->was_used());); m_removed_clauses.append(m_clauses_to_remove); @@ -122,8 +121,8 @@ namespace sat { } bool xor_finder::extract_xor(bool parity, clause& c, literal l1, literal l2) { - SASSERT(s.is_visited(l1.var())); - SASSERT(s.is_visited(l2.var())); + SASSERT(s.m_visited.is_visited(l1.var())); + SASSERT(s.m_visited.is_visited(l2.var())); m_missing.reset(); unsigned mask = 0; for (unsigned i = 0; i < c.size(); ++i) { diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index c5bf5b60d..6b5e50c50 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -46,6 +46,7 @@ z3_add_component(sat_smt user_solver.cpp xor_matrix_finder.cpp xor_solver.cpp + xor_gaussian.cpp COMPONENT_DEPENDENCIES sat ast diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 64577430c..d9eaa7e89 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -22,7 +22,7 @@ Author: #include "ast/ast_util.h" #include "ast/euf/euf_egraph.h" #include "ast/rewriter/th_rewriter.h" -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "sat/sat_extension.h" #include "sat/smt/atom2bool_var.h" #include "sat/smt/sat_th.h" diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index c3e43bfbe..424b20d4e 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/src/sat/smt/pb_solver.cpp @@ -690,15 +690,6 @@ namespace pb { inc_coeff(consequent, offset); process_antecedent(js.get_literal(), offset); break; -#if ENABLE_TERNARY - case sat::justification::TERNARY: - inc_bound(offset); - SASSERT (consequent != sat::null_literal); - inc_coeff(consequent, offset); - process_antecedent(js.get_literal1(), offset); - process_antecedent(js.get_literal2(), offset); - break; -#endif case sat::justification::CLAUSE: { inc_bound(offset); sat::clause & c = s().get_clause(js); @@ -1019,16 +1010,6 @@ namespace pb { inc_coeff(consequent, 1); process_antecedent(js.get_literal()); break; -#if ENABLE_TERNARY - case sat::justification::TERNARY: - SASSERT(consequent != sat::null_literal); - round_to_one(consequent.var()); - inc_bound(1); - inc_coeff(consequent, 1); - process_antecedent(js.get_literal1()); - process_antecedent(js.get_literal2()); - break; -#endif case sat::justification::CLAUSE: { sat::clause & c = s().get_clause(js); unsigned i = 0; @@ -3476,15 +3457,6 @@ namespace pb { ineq.push(lit, offset); ineq.push(js.get_literal(), offset); break; -#if ENABLE_TERNARY - case sat::justification::TERNARY: - SASSERT(lit != sat::null_literal); - ineq.reset(offset); - ineq.push(lit, offset); - ineq.push(js.get_literal1(), offset); - ineq.push(js.get_literal2(), offset); - break; -#endif case sat::justification::CLAUSE: { ineq.reset(offset); sat::clause & c = s().get_clause(js); diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp new file mode 100644 index 000000000..1bfaee9da --- /dev/null +++ b/src/sat/smt/xor_gaussian.cpp @@ -0,0 +1,1135 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + xor_gaussian.cpp + +Abstract: + + A roughly 1:1 port of CryptoMiniSAT's gaussian elimination datastructures/algorithms + +--*/ + + +#include +#include +#include +#include +#include + +#include "xor_solver.h" + +using std::ostream; +using std::set; + +using namespace xr; + +// if variable is not in Gaussian matrix, assign unknown column +static const unsigned unassigned_col = UINT32_MAX; + +///returns popcnt +unsigned PackedRow::find_watchVar( + sat::literal_vector& tmp_clause, + const unsigned_vector& col_to_var, + char_vector &var_has_resp_row, + unsigned& non_resp_var) { + unsigned popcnt = 0; + non_resp_var = UINT_MAX; + tmp_clause.clear(); + + for(int i = 0; i < size*64; i++) { + if (this->operator[](i)){ + popcnt++; + unsigned var = col_to_var[i]; + tmp_clause.push_back(sat::literal(var, false)); + + if (!var_has_resp_row[var]) { + non_resp_var = var; + } else { + //What??? WARNING + //This var already has a responsible for it... + //How can it be 1??? + std::swap(tmp_clause[0], tmp_clause.back()); + } + } + } + SASSERT(tmp_clause.size() == popcnt); + SASSERT(popcnt == 0 || var_has_resp_row[ tmp_clause[0].var() ]) ; + return popcnt; +} + +void PackedRow::get_reason( + sat::literal_vector& tmp_clause, + const unsigned_vector& col_to_var, + PackedRow& cols_vals, + PackedRow& tmp_col2, + literal prop) { + tmp_col2.set_and(*this, cols_vals); + for (int i = 0; i < size; i++) if (mp[i]) { + int64_t tmp = mp[i]; + unsigned long at; + at = scan_fwd_64b(tmp); + int extra = 0; + while (at != 0) { + unsigned col = extra + at-1 + i*64; + SASSERT(operator[](col) == 1); + const unsigned var = col_to_var[col]; + if (var == prop.var()) { + tmp_clause.push_back(prop); + std::swap(tmp_clause[0], tmp_clause.back()); + } else { + const bool val_bool = tmp_col2[col]; + tmp_clause.push_back(sat::literal(var, val_bool)); + } + + extra += at; + if (extra == 64) + break; + + tmp >>= at; + at = scan_fwd_64b(tmp); + } + } +} + +gret PackedRow::propGause( + const unsigned_vector& col_to_var, + char_vector &var_has_resp_row, + unsigned& new_resp_var, + PackedRow& tmp_col, + PackedRow& tmp_col2, + PackedRow& cols_vals, + PackedRow& cols_unset, + sat::literal& ret_lit_prop) { + + unsigned pop = tmp_col.set_and_until_popcnt_atleast2(*this, cols_unset); + + //Find new watch + if (pop >= 2) { + for (int i = 0; i < size; i++) if (tmp_col.mp[i]) { + int64_t tmp = tmp_col.mp[i]; + unsigned long at; + at = scan_fwd_64b(tmp); + int extra = 0; + while (at != 0) { + unsigned col = extra + at-1 + i*64; + const unsigned var = col_to_var[col]; + // found new non-basic variable, let's watch it + if (!var_has_resp_row[var]) { + new_resp_var = var; + return gret::nothing_fnewwatch; + } + + extra += at; + if (extra == 64) + break; + + tmp >>= at; + at = scan_fwd_64b(tmp); + } + } + } + + //Calc value of row + tmp_col2.set_and(*this, cols_vals); + const unsigned pop_t = tmp_col2.popcnt() + (unsigned)rhs(); + + //Lazy prop + if (pop == 1) { + for (int i = 0; i < size; i++) { + if (tmp_col.mp[i]) { + int at = scan_fwd_64b(tmp_col.mp[i]); + + // found prop + unsigned col = at-1 + i*64; + SASSERT(tmp_col[col] == 1); + const unsigned var = col_to_var[col]; + ret_lit_prop = sat::literal(var, !(pop_t % 2)); + return gret::prop; + } + } + UNREACHABLE(); + } + + //Only SAT & UNSAT left. + SASSERT(pop == 0); + + //Satisfied + if (pop_t % 2 == 0) { + return gret::nothing_satisfied; + } + + //Conflict + return gret::confl; +} + +EGaussian::EGaussian(xr::solver& _solver, const unsigned _matrix_no, const vector& _xorclauses) : + m_xorclauses(_xorclauses), m_solver(_solver), matrix_no(_matrix_no) { } + +EGaussian::~EGaussian() { + delete_gauss_watch_this_matrix(); + for (auto& x: tofree) + memory::deallocate(x); + tofree.clear(); + + delete cols_unset; + delete cols_vals; + delete tmp_col; + delete tmp_col2; +} + +/*class ColSorter { + + xr::solver* m_solver; + +public: + + explicit ColSorter(xr::solver* _solver) : m_solver(_solver) { + for (const auto& ass: m_solver.assumptions) { + literal p = m_solver.map_outer_to_inter(ass.lit_outer); + if (p.var() < m_solver.s().num_vars()) { + assert(m_solver.seen.size() > p.var()); + m_solver.seen[p.var()] = 1; + } + } + } + + void finishup() { + for (const auto& ass: m_solver.assumptions) { + literal p = m_solver.map_outer_to_inter(ass.lit_outer); + if (p.var() < m_solver.s().num_vars()) + m_solver.seen[p.var()] = 0; + } + } + + bool operator()(const unsigned a, const unsigned b) { + SASSERT(m_solver.seen.size() > a); + SASSERT(m_solver.seen.size() > b); + if (m_solver.seen[b] && !m_solver.seen[a]) + return true; + + if (!m_solver.seen[b] && m_solver.seen[a]) + return false; + + return false; + } +};*/ + +void EGaussian::select_columnorder() { + var_to_col.clear(); + var_to_col.resize(m_solver.s().num_vars(), unassigned_col); + unsigned_vector vars_needed; + unsigned largest_used_var = 0; + + for (const xor_clause& x : m_xorclauses) { + for (const unsigned v : x) { + SASSERT(m_solver.s().value(v) == l_undef); + if (var_to_col[v] == unassigned_col) { + vars_needed.push_back(v); + var_to_col[v] = unassigned_col - 1; + largest_used_var = std::max(largest_used_var, v); + } + } + } + + if (vars_needed.size() >= UINT32_MAX / 2 - 1) { + throw default_exception("Matrix has too many rows"); + } + if (m_xorclauses.size() >= UINT32_MAX / 2 - 1) { + throw default_exception("Matrix has too many rows"); + } + var_to_col.resize(largest_used_var + 1); + + + /*TODO: for assumption variables; ignored right now + ColSorter c(m_solver); + std::sort(vars_needed.begin(), vars_needed.end(), c); + c.finishup();*/ + + col_to_var.clear(); + for (unsigned v : vars_needed) { + SASSERT(var_to_col[v] == unassigned_col - 1); + col_to_var.push_back(v); + var_to_col[v] = col_to_var.size() - 1; + } + + // for the ones that were not in the order_heap, but are marked in var_to_col + for (unsigned v = 0; v < var_to_col.size(); v++) { + if (var_to_col[v] == unassigned_col - 1) { + col_to_var.push_back(v); + var_to_col[v] = col_to_var.size() - 1; + } + } +} + +void EGaussian::fill_matrix() { + var_to_col.clear(); + + // decide which variable in matrix column and the number of rows + select_columnorder(); + num_rows = m_xorclauses.size(); + num_cols = col_to_var.size(); + if (num_rows == 0 || num_cols == 0) { + return; + } + mat.resize(num_rows, num_cols); // initial gaussian matrix + + bdd_matrix.clear(); + for (unsigned row = 0; row < num_rows; row++) { + const xor_clause& c = m_xorclauses[row]; + mat[row].set(c, var_to_col, num_cols); + char_vector line; + line.resize(num_rows, 0); + line[row] = 1; + bdd_matrix.push_back(line); + } + SASSERT(bdd_matrix.size() == num_rows); + + // reset + var_has_resp_row.clear(); + var_has_resp_row.resize(m_solver.s().num_vars(), 0); + row_to_var_non_resp.clear(); + + delete_gauss_watch_this_matrix(); + + //reset satisfied_xor state + SASSERT(m_solver.m_num_scopes == 0); + satisfied_xors.clear(); + satisfied_xors.resize(num_rows, 0); +} + +void EGaussian::delete_gauss_watch_this_matrix() { + for (unsigned ii = 0; ii < m_solver.m_gwatches.size(); ii++) { + clear_gwatches(ii); + } +} + +void EGaussian::clear_gwatches(const unsigned var) { + //if there is only one matrix, don't check, just empty it + if (m_solver.m_gmatrices.empty()) { + m_solver.m_gwatches[var].clear(); + return; + } + + unsigned j = 0; + for (auto& w : m_solver.m_gwatches[var]) { + if (w.matrix_num != matrix_no) + m_solver.m_gwatches[var][j++] = w; + } + m_solver.m_gwatches[var].shrink(j); +} + +bool EGaussian::full_init(bool& created) { + SASSERT(!inconsistent()); + SASSERT(m_solver.m_num_scopes == 0); + SASSERT(initialized == false); + created = true; + + unsigned trail_before; + while (true) { + trail_before = m_solver.s().trail_size(); + m_solver.clean_xor_clauses(m_xorclauses); + + fill_matrix(); + before_init_density = get_density(); + if (num_rows == 0 || num_cols == 0) { + created = false; + return !inconsistent(); + } + + eliminate(); + + // find some row already true false, and insert watch list + gret ret = init_adjust_matrix(); + + switch (ret) { + case gret::confl: + return false; + case gret::prop: + SASSERT(m_solver.m_num_scopes == 0); + m_solver.s().propagate(false); // TODO: Can we really do this here? + // m_solver.ok = m_solver.propagate().isNull(); + if (inconsistent()) { + TRACE("xor", tout << "eliminate & adjust matrix during init lead to UNSAT\n";); + return false; + } + break; + default: + break; + } + + //Let's exit if nothing new happened + if (m_solver.s().trail_size() == trail_before) + break; + } + DEBUG_CODE(check_watchlist_sanity();); + TRACE("xor", tout << "initialised matrix " << matrix_no << "\n"); + + xor_reasons.resize(num_rows); + unsigned num_64b = num_cols/64+(bool)(num_cols%64); + for (auto& x: tofree) { + memory::deallocate(x); + } + tofree.clear(); + dealloc(cols_unset); + dealloc(cols_vals); + dealloc(tmp_col); + dealloc(tmp_col2); + + int64_t* x = (int64_t*)memory::allocate(sizeof(int64_t) * (num_64b + 1)); + tofree.push_back(x); + cols_unset = alloc(PackedRow, num_64b, x); + + x = (int64_t*)memory::allocate(sizeof(int64_t) * (num_64b + 1)); + tofree.push_back(x); + cols_vals = alloc(PackedRow, num_64b, x); + + x = (int64_t*)memory::allocate(sizeof(int64_t) * (num_64b + 1)); + tofree.push_back(x); + tmp_col = alloc(PackedRow, num_64b, x); + + x = (int64_t*)memory::allocate(sizeof(int64_t) * (num_64b + 1)); + tofree.push_back(x); + tmp_col2 = alloc(PackedRow, num_64b, x); + + cols_vals->rhs() = 0; + cols_unset->rhs() = 0; + tmp_col->rhs() = 0; + tmp_col2->rhs() = 0; + after_init_density = get_density(); + + initialized = true; + update_cols_vals_set(true); + DEBUG_CODE(check_invariants();); + + return !inconsistent(); +} + +void EGaussian::eliminate() { + PackedMatrix::iterator end_row_it = mat.begin() + num_rows; + PackedMatrix::iterator rowI = mat.begin(); + unsigned row_i = 0; + unsigned col = 0; + + // Gauss-Jordan Elimination + while (row_i != num_rows && col != num_cols) { + PackedMatrix::iterator row_with_1_in_col = rowI; + unsigned row_with_1_in_col_n = row_i; + + //Find first "1" in column. + for (; row_with_1_in_col != end_row_it; ++row_with_1_in_col, row_with_1_in_col_n++) { + if ((*row_with_1_in_col)[col]) { + break; + } + } + + //We have found a "1" in this column + if (row_with_1_in_col != end_row_it) { + var_has_resp_row[col_to_var[col]] = 1; + + // swap row row_with_1_in_col and rowIt + if (row_with_1_in_col != rowI) { + (*rowI).swapBoth(*row_with_1_in_col); + std::swap(bdd_matrix[row_i], bdd_matrix[row_with_1_in_col_n]); + } + + // XOR into *all* rows that have a "1" in column COL + // Since we XOR into *all*, this is Gauss-Jordan (and not just Gauss) + unsigned k = 0; + for (PackedMatrix::iterator k_row = mat.begin() + ; k_row != end_row_it + ; ++k_row, k++ + ) { + // xor rows K and I + if (k_row != rowI && (*k_row)[col]) { + (*k_row).xor_in(*rowI); + } + } + row_i++; + ++rowI; + } + col++; + } +} + +sat::literal_vector* EGaussian::get_reason(const unsigned row, int& out_ID) { + if (!xor_reasons[row].m_must_recalc) { + out_ID = xor_reasons[row].m_ID; + return &(xor_reasons[row].m_reason); + } + + // Clean up previous one + + svector& to_fill = xor_reasons[row].m_reason; + to_fill.clear(); + + mat[row].get_reason( + to_fill, + col_to_var, + *cols_vals, + *tmp_col2, + xor_reasons[row].m_propagated); + + xor_reasons[row].m_must_recalc = false; + xor_reasons[row].m_ID = out_ID; + return &to_fill; +} + +gret EGaussian::init_adjust_matrix() { + SASSERT(m_solver.s().at_search_lvl()); + SASSERT(row_to_var_non_resp.empty()); + SASSERT(satisfied_xors.size() >= num_rows); + TRACE("xor", tout << "mat[" << matrix_no << "] init adjusting matrix";); + + unsigned row_i = 0; // row index + unsigned adjust_zero = 0; // elimination row + for (PackedRow row : mat) { + if (row_i >= num_rows) + break; + unsigned non_resp_var; + const unsigned popcnt = row.find_watchVar(tmp_clause, col_to_var, var_has_resp_row, non_resp_var); + + switch (popcnt) { + + //Conflict or satisfied + case 0: + TRACE("xor", tout << "Empty XOR during init_adjust_matrix, rhs: " << row.rhs() << "\n"); + adjust_zero++; + + // conflict + if (row.rhs()) { + // TODO: Is this enough? What's the justification? + m_solver.s().set_conflict(); + TRACE("xor", tout << "-> empty clause during init_adjust_matrix";); + TRACE("xor", tout << "-> conflict on row: " << row_i;); + return gret::confl; + } + TRACE("xor", tout << "-> empty on row: " << row_i;); + TRACE("xor", tout << "-> Satisfied XORs set for row: " << row_i;); + satisfied_xors[row_i] = 1; + break; + + //Unit (i.e. toplevel unit) + case 1: + { + TRACE("xor", tout << "Unit XOR during init_adjust_matrix, vars: " << tmp_clause;); + bool xorEqualFalse = !mat[row_i].rhs(); + tmp_clause[0] = literal(tmp_clause[0].var(), xorEqualFalse); + SASSERT(m_solver.s().value(tmp_clause[0].var()) == l_undef); + + m_solver.s().assign_scoped(tmp_clause[0]); + + TRACE("xor", tout << "-> UNIT during adjust: " << tmp_clause[0];); + TRACE("xor", tout << "-> Satisfied XORs set for row: " << row_i;); + satisfied_xors[row_i] = 1; + SASSERT(check_row_satisfied(row_i)); + + //adjusting + row.setZero(); // reset this row all zero + row_to_var_non_resp.push_back(UINT32_MAX); + var_has_resp_row[tmp_clause[0].var()] = 0; + return gret::prop; + } + + //Binary XOR (i.e. toplevel binary XOR) + case 2: + { + TRACE("xor", tout << "Binary XOR during init_adjust_matrix, vars: " << tmp_clause;); + bool xorEqualFalse = !mat[row_i].rhs(); + + tmp_clause[0] = tmp_clause[0].unsign(); + tmp_clause[1] = tmp_clause[1].unsign(); + + m_solver.add_xor_clause(tmp_clause, !xorEqualFalse, true); + TRACE("xor", tout << "-> toplevel bin-xor on row: " << row_i << " cl2: " << tmp_clause;); + + // reset this row all zero, no need for this row + row.rhs() = 0; // TODO: The RHS is copied by value (unlike the content of the matrix) Bug? + row.setZero(); + + row_to_var_non_resp.push_back(UINT32_MAX); // delete non-basic value in this row + var_has_resp_row[tmp_clause[0].var()] = 0; // delete basic value in this row + break; + } + + default: // need to update watch list + SASSERT(non_resp_var != UINT32_MAX); + + // insert watch list + TRACE("xor", tout << "-> watch 1: resp var " << tmp_clause[0].var()+1 << " for row " << row_i << "\n";); + TRACE("xor", tout << "-> watch 2: non-resp var " << non_resp_var+1 << " for row " << row_i << "\n";); + m_solver.m_gwatches[tmp_clause[0].var()].push_back( + gauss_watched(row_i, matrix_no)); // insert basic variable + m_solver.m_gwatches[non_resp_var].push_back( + gauss_watched(row_i, matrix_no)); // insert non-basic variable + row_to_var_non_resp.push_back(non_resp_var); // record in this row non-basic variable + break; + } + row_i++; + } + SASSERT(row_to_var_non_resp.size() == row_i - adjust_zero); + + mat.resizeNumRows(row_i - adjust_zero); + num_rows = row_i - adjust_zero; + + return gret::nothing_satisfied; +} + +// Delete this row because we have already add to xor clause, nothing to do anymore +void EGaussian::delete_gausswatch(const unsigned row_n) { + // clear nonbasic value watch list + bool debug_find = false; + svector& ws_t = m_solver.m_gwatches[row_to_var_non_resp[row_n]]; + + for (int tmpi = ws_t.size(); tmpi-- > 0;) { + if (ws_t[tmpi].row_n == row_n + && ws_t[tmpi].matrix_num == matrix_no + ) { + ws_t[tmpi] = *ws_t.end(); + ws_t.shrink(1); + debug_find = true; + break; + } + } + SASSERT(debug_find); +} + +unsigned EGaussian::get_max_level(const gauss_data& gqd, const unsigned row_n) { + int ID; + auto cl = get_reason(row_n, ID); + unsigned nMaxLevel = gqd.currLevel; + unsigned nMaxInd = 1; + + for (unsigned i = 1; i < cl->size(); i++) { + literal l = (*cl)[i]; + unsigned nLevel = m_solver.s().lvl(l); + if (nLevel > nMaxLevel) { + nMaxLevel = nLevel; + nMaxInd = i; + } + } + + //should we?? + if (nMaxInd != 1) { + std::swap((*cl)[1], (*cl)[nMaxInd]); + } + return nMaxLevel; +} + +bool EGaussian::find_truths( + gauss_watched*& i, + gauss_watched*& j, + const unsigned var, + const unsigned row_n, + gauss_data& gqd) { + SASSERT(gqd.status != gauss_res::confl); + SASSERT(initialized); + + // printf("dd Watch variable : %d , Wathch row num %d n", p , row_n); + + TRACE("xor", tout + << "mat[" << matrix_no << "] find_truths\n" + << "-> row: " << row_n << "\n" + << "-> var: " << var+1 << "\n" + << "-> dec lev:" << m_solver.m_num_scopes); + SASSERT(row_n < num_rows); + SASSERT(satisfied_xors.size() > row_n); + + // this XOR is already satisfied + if (satisfied_xors[row_n]) { + TRACE("xor", tout << "-> xor satisfied as per satisfied_xors[row_n]";); + SASSERT(check_row_satisfied(row_n)); + *j++ = *i; + find_truth_ret_satisfied_precheck++; + return true; + } + + // swap resp and non-resp variable + bool was_resp_var = false; + if (var_has_resp_row[var] == 1) { + //var has a responsible row, so THIS row must be it! + //since if a var has a responsible row, only ONE row can have a 1 there + was_resp_var = true; + var_has_resp_row[row_to_var_non_resp[row_n]] = 1; + var_has_resp_row[var] = 0; + } + + unsigned new_resp_var; + literal ret_lit_prop; + const gret ret = mat[row_n].propGause( + col_to_var, + var_has_resp_row, + new_resp_var, + *tmp_col, + *tmp_col2, + *cols_vals, + *cols_unset, + ret_lit_prop); + find_truth_called_propgause++; + + switch (ret) { + case gret::confl: { + find_truth_ret_confl++; + *j++ = *i; + + xor_reasons[row_n].m_must_recalc = true; + xor_reasons[row_n].m_propagated = sat::null_literal; + gqd.conflict = m_solver.mk_justification(m_solver.s().search_lvl(), matrix_no, row_n); + gqd.status = gauss_res::confl; + TRACE("xor", tout << "--> conflict";); + + if (was_resp_var) { // recover + var_has_resp_row[row_to_var_non_resp[row_n]] = 0; + var_has_resp_row[var] = 1; + } + + return false; + } + + case gret::prop: { + find_truth_ret_prop++; + TRACE("xor", tout << "--> propagation";); + *j++ = *i; + + xor_reasons[row_n].m_must_recalc = true; + xor_reasons[row_n].m_propagated = ret_lit_prop; + SASSERT(m_solver.s().value(ret_lit_prop.var()) == l_undef); + prop_lit(gqd, row_n, ret_lit_prop); + + update_cols_vals_set(ret_lit_prop); + gqd.status = gauss_res::prop; + + if (was_resp_var) { // recover + var_has_resp_row[row_to_var_non_resp[row_n]] = 0; + var_has_resp_row[var] = 1; + } + + TRACE("xor", tout << "--> Satisfied XORs set for row: " << row_n;); + satisfied_xors[row_n] = 1; + SASSERT(check_row_satisfied(row_n)); + return true; + } + + // find new watch list + case gret::nothing_fnewwatch: + TRACE("xor", tout << "--> found new watch: " << new_resp_var+1;); + + find_truth_ret_fnewwatch++; + // printf("%d:This row is find new watch:%d => orig %d p:%d n",row_n , + // new_resp_var,orig_basic , p); + + if (was_resp_var) { + /// clear watchlist, because only one responsible value in watchlist + SASSERT(new_resp_var != var); + clear_gwatches(new_resp_var); + TRACE("xor", tout << "Cleared watchlist for new resp var: " << new_resp_var+1;); + TRACE("xor", tout << "After clear...";); + } + SASSERT(new_resp_var != var); + DEBUG_CODE(check_row_not_in_watch(new_resp_var, row_n);); + m_solver.m_gwatches[new_resp_var].push_back(gauss_watched(row_n, matrix_no)); + + if (was_resp_var) { + //it was the responsible one, so the newly watched var + //is the new column it's responsible for + //so elimination will be needed + + //clear old one, add new resp + var_has_resp_row[row_to_var_non_resp[row_n]] = 0; + var_has_resp_row[new_resp_var] = 1; + + // store the eliminate variable & row + gqd.new_resp_var = new_resp_var; + gqd.new_resp_row = row_n; + if (m_solver.m_gmatrices.size() == 1) { + SASSERT(m_solver.m_gwatches[gqd.new_resp_var].size() == 1); + } + gqd.do_eliminate = true; + return true; + } else { + row_to_var_non_resp[row_n] = new_resp_var; + return true; + } + + // this row already true + case gret::nothing_satisfied: + TRACE("xor", tout << "--> satisfied";); + + find_truth_ret_satisfied++; + // printf("%d:This row is nothing( maybe already true) n",row_n); + *j++ = *i; + if (was_resp_var) { // recover + var_has_resp_row[row_to_var_non_resp[row_n]] = 0; + var_has_resp_row[var] = 1; + } + + TRACE("xor", tout << "--> Satisfied XORs set for row: " << row_n;); + satisfied_xors[row_n] = 1; + SASSERT(check_row_satisfied(row_n)); + return true; + + //error here + default: + UNREACHABLE(); // cannot be here + return true; + } + + UNREACHABLE(); + return true; +} + +inline void EGaussian::update_cols_vals_set(const literal lit1) { + cols_unset->clearBit(var_to_col[lit1.var()]); + if (!lit1.sign()) { + cols_vals->setBit(var_to_col[lit1.var()]); + } +} + +void EGaussian::update_cols_vals_set(bool force) { + SASSERT(initialized); + + //cancelled_since_val_update = true; + if (cancelled_since_val_update || force) { + cols_vals->setZero(); + cols_unset->setOne(); + + for (unsigned col = 0; col < col_to_var.size(); col++) { + unsigned var = col_to_var[col]; + if (m_solver.s().value(var) != l_undef) { + cols_unset->clearBit(col); + if (m_solver.s().value(var) == l_true) { + cols_vals->setBit(col); + } + } + } + last_val_update = m_solver.s().trail_size(); + cancelled_since_val_update = false; + return; + } + + SASSERT(m_solver.s().trail_size() >= last_val_update); + for(unsigned i = last_val_update; i < m_solver.s().trail_size(); i++) { + sat::bool_var var = m_solver.s().trail_literal(i).var(); + if (var_to_col.size() <= var) { + continue; + } + unsigned col = var_to_col[var]; + if (col != unassigned_col) { + SASSERT(m_solver.s().value(var) != l_undef); + cols_unset->clearBit(col); + if (m_solver.s().value(var) == l_true) { + cols_vals->setBit(col); + } + } + } + last_val_update = m_solver.s().trail_size(); +} + +void EGaussian::prop_lit(const gauss_data& gqd, const unsigned row_i, const literal ret_lit_prop) { + unsigned level; + if (gqd.currLevel == m_solver.m_num_scopes) + level = gqd.currLevel; + else + level = get_max_level(gqd, row_i); + + m_solver.s().assign(ret_lit_prop, m_solver.mk_justification(level, matrix_no, row_i)); +} + +bool EGaussian::inconsistent() const { + return m_solver.s().inconsistent(); +} + +void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) { + const unsigned new_resp_row_n = gqd.new_resp_row; + PackedMatrix::iterator rowI = mat.begin(); + PackedMatrix::iterator end = mat.end(); + const unsigned new_resp_col = var_to_col[gqd.new_resp_var]; + unsigned row_i = 0; + + elim_called++; + + while (rowI != end) { + //Row has a '1' in eliminating column, and it's not the row responsible + if (new_resp_row_n != row_i && (*rowI)[new_resp_col]) { + + // detect orignal non-basic watch list change or not + unsigned orig_non_resp_var = row_to_var_non_resp[row_i]; + unsigned orig_non_resp_col = var_to_col[orig_non_resp_var]; + SASSERT((*rowI)[orig_non_resp_col]); + TRACE("xor", tout << "--> This row " << row_i + << " is being watched on var: " << orig_non_resp_var + 1 + << " i.e. it must contain '1' for this var's column";); + + SASSERT(satisfied_xors[row_i] == 0); + (*rowI).xor_in(*(mat.begin() + new_resp_row_n)); + + elim_xored_rows++; + + //NOTE: responsible variable cannot be eliminated of course + // (it's the only '1' in that column). + // But non-responsible can be eliminated. So let's check that + // and then deal with it if we have to + if (!(*rowI)[orig_non_resp_col]) { + + // Delete orignal non-responsible var from watch list + if (orig_non_resp_var != gqd.new_resp_var) { + delete_gausswatch(row_i); + } else { + //this does not need a delete, because during + //find_truths, we already did clear_gwatches of the + //orig_non_resp_var, so there is nothing to delete here + } + + literal ret_lit_prop; + unsigned new_non_resp_var = 0; + const gret ret = (*rowI).propGause( + col_to_var, + var_has_resp_row, + new_non_resp_var, + *tmp_col, + *tmp_col2, + *cols_vals, + *cols_unset, + ret_lit_prop + ); + elim_called_propgause++; + + switch (ret) { + case gret::confl: { + elim_ret_confl++; + TRACE("xor", tout << "---> conflict during eliminate_col's fixup";); + m_solver.m_gwatches[p].push_back(gauss_watched(row_i, matrix_no)); + + // update in this row non-basic variable + row_to_var_non_resp[row_i] = p; + + xor_reasons[row_i].m_must_recalc = true; + xor_reasons[row_i].m_propagated = sat::null_literal; + gqd.conflict = m_solver.mk_justification(m_solver.s().search_lvl(), matrix_no, row_i); + gqd.status = gauss_res::confl; + + break; + } + case gret::prop: { + elim_ret_prop++; + TRACE("xor", tout << "---> propagation during eliminate_col's fixup";); + + // if conflicted already, just update non-basic variable + if (gqd.status == gauss_res::confl) { + DEBUG_CODE(check_row_not_in_watch(p, row_i);); + m_solver.m_gwatches[p].push_back(gauss_watched(row_i, matrix_no)); + row_to_var_non_resp[row_i] = p; + break; + } + + // update no_basic information + DEBUG_CODE(check_row_not_in_watch(p, row_i);); + m_solver.m_gwatches[p].push_back(gauss_watched(row_i, matrix_no)); + row_to_var_non_resp[row_i] = p; + + xor_reasons[row_i].m_must_recalc = true; + xor_reasons[row_i].m_propagated = ret_lit_prop; + SASSERT(m_solver.s().value(ret_lit_prop.var()) == l_undef); + prop_lit(gqd, row_i, ret_lit_prop); + + update_cols_vals_set(ret_lit_prop); + gqd.status = gauss_res::prop; + + TRACE("xor", tout << "---> Satisfied XORs set for row: " << row_i;); + satisfied_xors[row_i] = 1; + SASSERT(check_row_satisfied(row_i)); + break; + } + + // find new watch list + case gret::nothing_fnewwatch: + elim_ret_fnewwatch++; + + DEBUG_CODE(check_row_not_in_watch(new_non_resp_var, row_i);); + m_solver.m_gwatches[new_non_resp_var].push_back(gauss_watched(row_i, matrix_no)); + row_to_var_non_resp[row_i] = new_non_resp_var; + break; + + // this row already satisfied + case gret::nothing_satisfied: + elim_ret_satisfied++; + TRACE("xor", tout << "---> Nothing to do, already satisfied , pushing in " << p+1 << " as non-responsible var ( " << row_i << " row)\n"); + + // printf("%d:This row is nothing( maybe already true) in eliminate col + // n",num_row); + + DEBUG_CODE(check_row_not_in_watch(p, row_i);); + m_solver.m_gwatches[p].push_back(gauss_watched(row_i, matrix_no)); + row_to_var_non_resp[row_i] = p; + + TRACE("xor", tout << "---> Satisfied XORs set for row: " << row_i;); + satisfied_xors[row_i] = 1; + SASSERT(check_row_satisfied(row_i)); + break; + default: + // can not here + SASSERT(false); + break; + } + } else { + TRACE("xor", tout << "--> OK, this row " << row_i << " still contains '1', can still be responsible";); + } + } + ++rowI; + row_i++; + } + +} + +////////////////// +// Checking functions below +////////////////// + +void EGaussian::check_row_not_in_watch(const unsigned v, const unsigned row_num) const { + for (const auto& x: m_solver.m_gwatches[v]) { + SASSERT(!(x.matrix_num == matrix_no && x.row_n == row_num)); + } +} + + +void EGaussian::check_no_prop_or_unsat_rows() { + TRACE("xor", tout << "mat[" << matrix_no << "] checking invariants...";); + + for (unsigned row = 0; row < num_rows; row++) { + unsigned bits_unset = 0; + bool val = mat[row].rhs(); + for (unsigned col = 0; col < num_cols; col++) { + if (mat[row][col]) { + unsigned var = col_to_var[col]; + if (m_solver.s().value(var) == l_undef) { + bits_unset++; + } else { + val ^= (m_solver.s().value(var) == l_true); + } + } + } + + bool error = false; + if (bits_unset == 1) { + TRACE("xor", tout << "ERROR: row " << row << " is PROP but did not propagate!!!\n";); + } + if (bits_unset == 0 && val) { + TRACE("xor", tout << "ERROR: row " << row << " is UNSAT but did not conflict!\n";); + error = true; + } + if (error) { + for(unsigned var = 0; var < m_solver.s().num_vars(); var++) { + const auto& ws = m_solver.m_gwatches[var]; + for (const auto& w: ws) { + if (w.matrix_num == matrix_no && w.row_n == row) { + TRACE("xor", tout << " gauss watched at var: " << var+1 << " val: " << m_solver.s().value(var) << "\n";); + } + } + } + + TRACE("xor", tout + << " matrix no: " << matrix_no << "\n" + << " row: " << row << "\n" + << " non-resp var: " << row_to_var_non_resp[row] + 1 << "\n" + << " dec level: " << m_solver.m_num_scopes << "\n";); + } + SASSERT(bits_unset > 1 || (bits_unset == 0 && val == 0)); + } +} + +void EGaussian::check_watchlist_sanity() { + for (unsigned i = 0; i < m_solver.s().num_vars(); i++) { + for (auto w: m_solver.m_gwatches[i]) { + if (w.matrix_num == matrix_no) { + SASSERT(i < var_to_col.size()); + } + } + } +} + +void EGaussian::check_tracked_cols_only_one_set() { + unsigned_vector row_resp_for_var(num_rows, l_undef); + for (unsigned col = 0; col < num_cols; col++) { + unsigned var = col_to_var[col]; + if (var_has_resp_row[var]) { + unsigned num_ones = 0; + unsigned found_row = l_undef; + for (unsigned row = 0; row < num_rows; row++) { + if (mat[row][col]) { + num_ones++; + found_row = row; + } + } + if (num_ones == 0) { + TRACE("xor", tout + << "mat[" << matrix_no << "] " + << "WARNING: Tracked col " << col + << " var: " << var+1 + << " has 0 rows' bit set to 1..." + << "\n";); + } + if (num_ones > 1) { + TRACE("xor", tout << "mat[" << matrix_no << "] " + << "ERROR: Tracked col " << col + << " var: " << var+1 + << " has " << num_ones << " rows' bit set to 1!!\n";); + SASSERT(false); + } + if (num_ones == 1) { + if (row_resp_for_var[found_row] != l_undef) { + TRACE("xor", tout << "ERROR One row can only be responsible for one col" + << " but row " << found_row << " is responsible for" + << " var: " << row_resp_for_var[found_row] + 1 + << " and var: " << var+1 << "\n";); + SASSERT(false); + } + row_resp_for_var[found_row] = var; + } + } + } +} + +void EGaussian::check_invariants() { + if (!initialized) return; + check_tracked_cols_only_one_set(); + check_no_prop_or_unsat_rows(); + TRACE("xor", tout << "mat[" << matrix_no << "] " << "Checked invariants. Dec level: " << m_solver.m_num_scopes << "\n";); +} + +bool EGaussian::check_row_satisfied(const unsigned row) { + bool ret = true; + bool fin = mat[row].rhs(); + for (unsigned i = 0; i < num_cols; i++) { + if (mat[row][i]) { + unsigned var = col_to_var[i]; + auto val = m_solver.s().value(var); + if (val == l_undef) { + TRACE("xor", tout << "Var " << var+1 << " col: " << i << " is undef!\n";); + ret = false; + } + fin ^= val == l_true; + } + } + return ret && !fin; +} + +bool EGaussian::must_disable(gauss_data& gqd) { + SASSERT(initialized); + gqd.disable_checks++; + if ((gqd.disable_checks & 0x3ff) == 0x3ff) { + uint64_t egcalled = elim_called + find_truth_ret_satisfied_precheck + find_truth_called_propgause; + unsigned limit = (unsigned)((double)egcalled * m_solver.s().get_config().m_xor_gauss_min_usefulness_cutoff); + unsigned useful = find_truth_ret_prop+find_truth_ret_confl+elim_ret_prop+elim_ret_confl; + if (egcalled > 200 && useful < limit) + return true; + } + + return false; +} + +void EGaussian::move_back_xor_clauses() { + for (const auto& x: m_xorclauses) { + m_solver.m_xorclauses.push_back(std::move(x)); + } +} \ No newline at end of file diff --git a/src/sat/smt/xor_gaussian.h b/src/sat/smt/xor_gaussian.h new file mode 100644 index 000000000..432b67d0a --- /dev/null +++ b/src/sat/smt/xor_gaussian.h @@ -0,0 +1,706 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + xor_gaussian.h + +Abstract: + + A roughly 1:1 port of CryptoMiniSAT's gaussian elimination datastructures/algorithms + +--*/ + +#pragma once + +#include "sat/smt/euf_solver.h" + +#include "util/debug.h" +#include "util/sat_literal.h" +#include "util/trace.h" + +namespace xr { + + typedef sat::literal literal; + typedef sat::bool_var bool_var; + typedef sat::literal_vector literal_vector; + typedef sat::bool_var_vector bool_var_vector; + + + class solver; + +#ifdef _MSC_VER + inline int scan_fwd_64b(int64_t value) { + unsigned long at; + unsigned char ret = _BitScanForward64(&at, value); + at++; + if (!ret) at = 0; + return at; + } +#else + inline int scan_fwd_64b(uint64_t value) { + return __builtin_ffsll(value); + } +#endif + + class justification { + + friend class solver; + + unsigned matrix_num; + unsigned row_num; + + //XOR + justification(const unsigned matrix_num, const unsigned row_num): + matrix_num(matrix_num), + row_num(row_num) { + SASSERT(matrix_num != -1); + SASSERT(row_num != -1); + } + + public: + justification() : matrix_num(-1), row_num(-1) {} + + void deallocate(small_object_allocator& a) { a.deallocate(get_obj_size(), sat::constraint_base::mem2base_ptr(this)); } + sat::ext_constraint_idx to_index() const { return sat::constraint_base::mem2base(this); } + static justification& from_index(size_t idx) { + return *reinterpret_cast(sat::constraint_base::from_index(idx)->mem()); + } + static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(justification)); } + + unsigned get_matrix_num() const { + return matrix_num; + } + + unsigned get_row_num() const { + return row_num; + } + + bool isNull() const { + return matrix_num == -1; + } + + bool operator==(const justification other) const { + return matrix_num == other.matrix_num && row_num == other.row_num; + } + + bool operator!=(const justification other) const { + return !(*this == other); + } + }; + + inline std::ostream& operator<<(std::ostream& os, const justification& pb) { + if (!pb.isNull()) { + return os << " xor reason, matrix= " << pb.get_matrix_num() << " row: " << pb.get_row_num(); + } + return os << " NULL"; + } + + enum class gret : unsigned { confl, prop, nothing_satisfied, nothing_fnewwatch }; + enum class gauss_res : unsigned { none, confl, prop }; + + struct gauss_watched { + gauss_watched(unsigned r, unsigned m) : row_n(r) , matrix_num(m) { } + + unsigned row_n; // watch row + unsigned matrix_num; // watch matrix + + bool operator<(const gauss_watched& other) const { + if (matrix_num < other.matrix_num) + return true; + if (matrix_num > other.matrix_num) + return false; + return row_n < other.row_n; + } + }; + + struct gauss_data { + bool do_eliminate; // we do elimination when basic variable is invoked + unsigned new_resp_var; // do elimination variable + unsigned new_resp_row ; // do elimination row + sat::justification conflict = sat::justification(0); // returning conflict + gauss_res status; // status + unsigned currLevel; // level at which the variable was decided on + + unsigned num_props = 0; // total gauss propagation time for DPLL + unsigned num_conflicts = 0; // total gauss conflict time for DPLL + unsigned disable_checks = 0; + bool disabled = false; // decide to do gaussian elimination + + void reset() { + do_eliminate = false; + status = gauss_res::none; + } + }; + + struct reason { + bool m_must_recalc = true; + literal m_propagated = sat::null_literal; + unsigned m_ID = 0; + literal_vector m_reason; + }; + + struct xor_clause { + + bool m_rhs = false; + bool_var_vector m_clash_vars; + bool m_detached = false; + bool_var_vector m_vars; + + xor_clause() = default; + xor_clause(const xor_clause& c) = default; + xor_clause(xor_clause&& c) noexcept : m_rhs(c.m_rhs), m_clash_vars(std::move(c.m_clash_vars)), m_detached(c.m_detached), m_vars(std::move(c.m_vars)) { } + + ~xor_clause() = default; + + xor_clause& operator=(const xor_clause& c) = default; + + explicit xor_clause(const unsigned_vector& cl, const bool _rhs, const bool_var_vector& _clash_vars) : m_rhs(_rhs), m_clash_vars(_clash_vars) { + for (unsigned i = 0; i < cl.size(); i++) { + m_vars.push_back(cl[i]); + } + } + + template + explicit xor_clause(const T& cl, const bool _rhs, const bool_var_vector& _clash_vars) : m_rhs(_rhs), m_clash_vars(_clash_vars) { + for (unsigned i = 0; i < cl.size(); i++) { + m_vars.push_back(cl[i].var()); + } + } + + explicit xor_clause(const bool_var_vector& cl, const bool _rhs, const unsigned clash_var) : m_rhs(_rhs) { + m_clash_vars.push_back(clash_var); + for (unsigned i = 0; i < cl.size(); i++) { + m_vars.push_back(cl[i]); + } + } + + unsigned_vector::const_iterator begin() const { + return m_vars.begin(); + } + + unsigned_vector::const_iterator end() const { + return m_vars.end(); + } + + unsigned_vector::iterator begin() { + return m_vars.begin(); + } + + unsigned_vector::iterator end() { + return m_vars.end(); + } + + bool operator<(const xor_clause& other) const { + unsigned i = 0; + while(i < other.size() && i < size()) { + if (other[i] != m_vars[i]) + return m_vars[i] < other[i]; + i++; + } + + if (other.size() != size()) { + return size() < other.size(); + } + return false; + } + + const unsigned& operator[](const unsigned at) const { + return m_vars[at]; + } + + unsigned& operator[](const unsigned at) { + return m_vars[at]; + } + + void shrink(const unsigned newsize) { + m_vars.shrink(newsize); + } + + bool_var_vector& get_vars() { + return m_vars; + } + + const bool_var_vector& get_vars() const { + return m_vars; + } + + unsigned size() const { + return m_vars.size(); + } + + bool empty() const { + if (!m_vars.empty()) + return false; + if (!m_clash_vars.empty()) + return false; + return !m_rhs; + } + + // add all elements in other.m_clash_vars that are not yet in m_clash_vars: + void merge_clash(const xor_clause& other, visit_helper& visited) { + visited.init_visited(m_clash_vars.size()); + for (const bool_var& v: m_clash_vars) { + visited.mark_visited(v); + } + + for (const auto& v: other.m_clash_vars) { + if (!visited.is_visited(v)) { + visited.mark_visited(v); + m_clash_vars.push_back(v); + } + } + } + }; + + inline std::ostream& operator<<(std::ostream& os, const xor_clause& thisXor) { + for (unsigned i = 0; i < thisXor.size(); i++) { + os << literal(thisXor[i], false); + + if (i + 1 < thisXor.size()) + os << " + "; + } + os << " = " << std::boolalpha << thisXor.m_rhs << std::noboolalpha; + + os << " -- clash: "; + for (const auto& c: thisXor.m_clash_vars) { + os << c + 1 << ", "; + } + + return os; + } + + class PackedRow { + + friend class PackedMatrix; + friend class EGaussian; + friend std::ostream& operator<<(std::ostream& os, const PackedRow& m); + + PackedRow(const unsigned _size, int64_t* const _mp) : + mp(_mp+1), + rhs_internal(*_mp), + size(_size) {} + + int64_t* __restrict const mp; + int64_t& rhs_internal; + const int size; + + public: + + PackedRow() = delete; + + PackedRow& operator=(const PackedRow& b) { + //start from -1, because that's wher RHS is + for (int i = -1; i < size; i++) { + *(mp + i) = *(b.mp + i); + } + + return *this; + } + + PackedRow& operator^=(const PackedRow& b) { + //start from -1, because that's wher RHS is + for (int i = -1; i < size; i++) { + *(mp + i) ^= *(b.mp + i); + } + + return *this; + } + + void set_and(const PackedRow& a, const PackedRow& b) { + for (int i = 0; i < size; i++) { + *(mp + i) = *(a.mp + i) & *(b.mp + i); + } + } + + unsigned set_and_until_popcnt_atleast2(const PackedRow& a, const PackedRow& b) { + unsigned pop = 0; + for (int i = 0; i < size && pop < 2; i++) { + *(mp + i) = *(a.mp + i) & *(b.mp + i); + pop += get_num_1bits((uint64_t)*(mp + i)); + } + + return pop; + } + + void xor_in(const PackedRow& b) { + rhs_internal ^= b.rhs_internal; + for (int i = 0; i < size; i++) { + *(mp + i) ^= *(b.mp + i); + } + } + + inline const int64_t& rhs() const { + return rhs_internal; + } + + inline int64_t& rhs() { + return rhs_internal; + } + + inline bool isZero() const { + for (int i = 0; i < size; i++) { + if (mp[i]) return false; + } + return true; + } + + inline void setZero() { + memset(mp, 0, sizeof(int64_t)*size); + } + + inline void setOne() { + memset(mp, 0xff, sizeof(int64_t)*size); + } + + inline void clearBit(const unsigned i) { + mp[i / 64] &= ~(1LL << (i % 64)); + } + + inline void setBit(const unsigned i) { + mp[i / 64] |= (1LL << (i % 64)); + } + + inline void invert_rhs(const bool b = true) { + rhs_internal ^= (int)b; + } + + void swapBoth(PackedRow b) { + int64_t* __restrict mp1 = mp - 1; + int64_t* __restrict mp2 = b.mp - 1; + + unsigned i = size+1; + while(i != 0) { + std::swap(*mp1, *mp2); + mp1++; + mp2++; + i--; + } + } + + inline bool operator[](const unsigned i) const { + return (mp[i / 64] >> (i % 64)) & 1; + } + + template + void set( + const T& v, + const unsigned_vector& var_to_col, + const unsigned num_cols) { + SASSERT(size == ((int)num_cols/64) + ((bool)(num_cols % 64))); + + setZero(); + for (unsigned i = 0; i != v.size(); i++) { + const unsigned toset_var = var_to_col[v[i]]; + SASSERT(toset_var != UINT32_MAX); + + setBit(toset_var); + } + + rhs_internal = v.m_rhs; + } + + // using find nonbasic and basic value + unsigned find_watchVar( + sat::literal_vector& tmp_clause, + const unsigned_vector& col_to_var, + char_vector &var_has_resp_row, + unsigned& non_resp_var); + + // using find nonbasic value after watch list is enter + gret propGause( + const unsigned_vector& col_to_var, + char_vector &var_has_resp_row, + unsigned& new_resp_var, + PackedRow& tmp_col, + PackedRow& tmp_col2, + PackedRow& cols_vals, + PackedRow& cols_unset, + literal& ret_lit_prop + ); + + void get_reason( + sat::literal_vector& tmp_clause, + const unsigned_vector& col_to_var, + PackedRow& cols_vals, + PackedRow& tmp_col2, + literal prop + ); + + unsigned popcnt() const { + unsigned ret = 0; + for (int i = 0; i < size; i++) { + ret += get_num_1bits((uint64_t)mp[i]); + } + return ret; + } + }; + + class PackedMatrix { + public: + PackedMatrix() : mp(nullptr), numRows(0), numCols(0) { } + + ~PackedMatrix() { + #ifdef _WIN32 + _aligned_free((void*)mp); + #else + free(mp); + #endif + } + + void resize(const unsigned num_rows, unsigned num_cols) { + num_cols = num_cols / 64 + (bool)(num_cols % 64); + if (numRows * (numCols + 1) < (int)num_rows * ((int)num_cols + 1)) { + size_t size = sizeof(int64_t) * num_rows*(num_cols+1); + #ifdef _WIN32 + _aligned_free((void*)mp); + mp = (int64_t*)_aligned_malloc(size, 16); + #else + free(mp); + posix_memalign((void**)&mp, 16, size); + #endif + } + + numRows = num_rows; + numCols = num_cols; + } + + void resizeNumRows(const unsigned num_rows) { + SASSERT((int)num_rows <= numRows); + numRows = num_rows; + } + + PackedMatrix& operator=(const PackedMatrix& b) { + if (numRows*(numCols+1) < b.numRows*(b.numCols+1)) { + size_t size = sizeof(int64_t) * b.numRows*(b.numCols+1); + #ifdef _WIN32 + _aligned_free((void*)mp); + mp = (int64_t*)_aligned_malloc(size, 16); + #else + free(mp); + posix_memalign((void**)&mp, 16, size); + #endif + } + numRows = b.numRows; + numCols = b.numCols; + memcpy(mp, b.mp, sizeof(int)*numRows*(numCols+1)); + + return *this; + } + + inline PackedRow operator[](const unsigned i) { + return PackedRow(numCols, mp+i*(numCols+1)); + } + + inline PackedRow operator[](const unsigned i) const { + return PackedRow(numCols, mp+i*(numCols+1)); + } + + class iterator { + int64_t* mp; + const unsigned numCols; + + iterator(int64_t* _mp, const unsigned _numCols) : mp(_mp), numCols(_numCols) { } + + public: + friend class PackedMatrix; + + PackedRow operator*() { + return PackedRow(numCols, mp); + } + + iterator& operator++() { + mp += (numCols+1); + return *this; + } + + iterator operator+(const unsigned num) const { + iterator ret(*this); + ret.mp += (numCols + 1) * num; + return ret; + } + + unsigned operator-(const iterator& b) const { + return (unsigned)(mp - b.mp) / (numCols + 1); + } + + void operator+=(const unsigned num) { + mp += (numCols + 1) * num; // add by f4 + } + + bool operator!=(const iterator& it) const { + return mp != it.mp; + } + + bool operator==(const iterator& it) const { + return mp == it.mp; + } + }; + + inline iterator begin() { + return iterator(mp, numCols); + } + + inline iterator end() { + return iterator(mp+numRows*(numCols+1), numCols); + } + + private: + + int64_t *mp; + int numRows; + int numCols; + }; + + class EGaussian { + public: + EGaussian( + solver& solver, + const unsigned matrix_no, + const vector& xorclauses + ); + ~EGaussian(); + bool is_initialized() const; + + ///returns FALSE in case of conflict + bool find_truths( + gauss_watched*& i, + gauss_watched*& j, + const unsigned var, + const unsigned row_n, + gauss_data& gqd + ); + + sat::literal_vector* get_reason(const unsigned row, int& out_ID); + + // when basic variable is touched , eliminate one col + void eliminate_col( + unsigned p, + gauss_data& gqd + ); + void canceling(); + bool full_init(bool& created); + void update_cols_vals_set(bool force = false); + bool must_disable(gauss_data& gqd); + void check_invariants(); + void update_matrix_no(unsigned n); + void check_watchlist_sanity(); + void move_back_xor_clauses(); + + vector m_xorclauses; + + private: + xr::solver& m_solver; // original sat solver + + //Cleanup + void clear_gwatches(const unsigned var); + void delete_gauss_watch_this_matrix(); + void delete_gausswatch(const unsigned row_n); + + //Invariant checks, debug + void check_no_prop_or_unsat_rows(); + void check_tracked_cols_only_one_set(); + bool check_row_satisfied(const unsigned row); + void check_row_not_in_watch(const unsigned v, const unsigned row_num) const; + + //Reason generation + vector xor_reasons; + sat::literal_vector tmp_clause; + unsigned get_max_level(const gauss_data& gqd, const unsigned row_n); + + //Initialisation + void eliminate(); + void fill_matrix(); + void select_columnorder(); + gret init_adjust_matrix(); // adjust matrix, include watch, check row is zero, etc. + double get_density(); + + //Helper functions + void prop_lit(const gauss_data& gqd, const unsigned row_i, const sat::literal ret_lit_prop); + bool inconsistent() const; + + /////////////// + // stats + /////////////// + unsigned find_truth_ret_satisfied_precheck = 0; + unsigned find_truth_called_propgause = 0; + unsigned find_truth_ret_fnewwatch = 0; + unsigned find_truth_ret_confl = 0; + unsigned find_truth_ret_satisfied = 0; + unsigned find_truth_ret_prop = 0; + + unsigned elim_called = 0; + unsigned elim_xored_rows = 0; + unsigned elim_called_propgause = 0; + unsigned elim_ret_prop = 0; + unsigned elim_ret_confl = 0; + unsigned elim_ret_satisfied = 0; + unsigned elim_ret_fnewwatch = 0; + double before_init_density = 0; + double after_init_density = 0; + + /////////////// + // Internal data + /////////////// + unsigned matrix_no; + bool initialized = false; + bool cancelled_since_val_update = true; + unsigned last_val_update = 0; + + //Is the clause at this ROW satisfied already? + //satisfied_xors[row] tells me that + // TODO: Are characters enough? + char_vector satisfied_xors; + + // Someone is responsible for this column if TRUE + ///we always WATCH this variable + char_vector var_has_resp_row; + + ///row_to_var_non_resp[ROW] gives VAR it's NOT responsible for + ///we always WATCH this variable + unsigned_vector row_to_var_non_resp; + + + PackedMatrix mat; + svector bdd_matrix; // TODO: we will probably not need it + unsigned_vector var_to_col; ///var->col mapping. Index with VAR + unsigned_vector col_to_var; ///col->var mapping. Index with COL + unsigned num_rows = 0; + unsigned num_cols = 0; + + //quick lookup + PackedRow* cols_vals = nullptr; + PackedRow* cols_unset = nullptr; + PackedRow* tmp_col = nullptr; + PackedRow* tmp_col2 = nullptr; + void update_cols_vals_set(const sat::literal lit1); + + //Data to free (with delete[] x) + // TODO: This are always 4 equally sized elements; merge them into one block + svector tofree; + }; + + inline void EGaussian::canceling() { + cancelled_since_val_update = true; + memset(satisfied_xors.data(), 0, satisfied_xors.size()); + } + + inline double EGaussian::get_density() { + if (num_rows*num_cols == 0) + return 0; + + unsigned pop = 0; + for (const auto& row: mat) { + pop += row.popcnt(); + } + return (double)pop/(double)(num_rows*num_cols); + } + + inline void EGaussian::update_matrix_no(unsigned n) { + matrix_no = n; + } + + inline bool EGaussian::is_initialized() const { + return initialized; + } +} \ No newline at end of file diff --git a/src/sat/smt/xor_matrix_finder.cpp b/src/sat/smt/xor_matrix_finder.cpp index e003f0e3c..ecc9a77a0 100644 --- a/src/sat/smt/xor_matrix_finder.cpp +++ b/src/sat/smt/xor_matrix_finder.cpp @@ -15,6 +15,7 @@ Notes: --*/ +#include "sat/sat_xor_finder.h" #include "sat/smt/xor_matrix_finder.h" #include "sat/smt/xor_solver.h" @@ -23,8 +24,8 @@ namespace xr { xor_matrix_finder::xor_matrix_finder(solver& s) : m_xor(s), m_sat(s.s()) { } - inline bool xor_matrix_finder::belong_same_matrix(const constraint& x) { - uint32_t comp_num = -1; + inline bool xor_matrix_finder::belong_same_matrix(const xor_clause& x) { + unsigned comp_num = -1; for (sat::bool_var v : x) { if (m_table[v] == l_undef) // Belongs to none, abort return false; @@ -39,72 +40,73 @@ namespace xr { bool xor_matrix_finder::find_matrices(bool& can_detach) { SASSERT(!m_sat.inconsistent()); -#if 0 - SASSERT(m_xor.gmatrices.empty()); + SASSERT(m_xor.m_gmatrices.empty()); + can_detach = true; m_table.clear(); - m_table.resize(m_solver->nVars(), l_undef); - m_reverseTable.clear(); - clash_vars_unused.clear(); + m_table.resize(m_sat.num_vars(), l_undef); + m_reverseTable.reset(); + clash_vars_unused.reset(); m_matrix_no = 0; - XorFinder finder(NULL, solver); + for (auto& x: m_xor.m_xorclauses_unused) + m_xor.m_xorclauses.push_back(x); + m_xor.m_xorclauses_unused.clear(); + m_xor.clean_xor_clauses(m_xor.m_xorclauses); - for (auto& x: m_solver->xorclauses_unused) - m_xor.xorclauses.push_back(std::move(x)); - m_xor.xorclauses_unused.clear(); - m_xor.clauseCleaner->clean_xor_clauses(solver->xorclauses); - - finder.grab_mem(); - finder.move_xors_without_connecting_vars_to_unused(); - if (!finder.xor_together_xors(m_solver->xorclauses)) + m_xor.move_xors_without_connecting_vars_to_unused(); + if (!m_xor.xor_together_xors(m_xor.m_xorclauses)) return false; - finder.move_xors_without_connecting_vars_to_unused(); - finder.clean_equivalent_xors(m_solver->xorclauses); - for (const auto& x: m_xor.xorclauses_unused) - clash_vars_unused.insert(x.clash_vars.begin(), x.clash_vars.end()); + m_xor.move_xors_without_connecting_vars_to_unused(); + m_xor.clean_equivalent_xors(m_xor.m_xorclauses); + for (const auto& c : m_xor.m_xorclauses_unused){ + for (const auto& v : c) { + clash_vars_unused.insert(v); + } + } - if (m_xor.xorclauses.size() < m_sat.get_config().m_min_gauss_xor_clauses) { + if (m_xor.m_xorclauses.size() < m_sat.get_config().m_xor_gauss_min_clauses) { can_detach = false; return true; } //Just one giant matrix. - // if (m_sat.get_config().m_xor_gauss_do_matrix_find) - if (!m_sat.get_config().m_xor_doMatrixFind) { - m_xor.gmatrices.push_back(new EGaussian(m_xor, 0, m_xor.xorclauses)); - m_xor.gqueuedata.resize(m_xor.gmatrices.size()); + if (!m_sat.get_config().m_xor_gauss_doMatrixFind) { + m_xor.m_gmatrices.push_back(alloc(EGaussian, m_xor, 0, m_xor.m_xorclauses)); + m_xor.m_gqueuedata.resize(m_xor.m_gmatrices.size()); return true; } - std::vector newSet; - uint_set tomerge; - for (const constraint& x : m_xor.m_constraints) { + unsigned_vector newSet; + unsigned_vector tomerge; + for (const xor_clause& x : m_xor.m_xorclauses) { if (belong_same_matrix(x)) continue; - tomerge.clear(); + tomerge.reset(); newSet.clear(); - for (uint32_t v : x) { + for (unsigned v : x) { if (m_table[v] != l_undef) - tomerge.insert(m_table[v]); + tomerge.push_back(m_table[v]); else newSet.push_back(v); } if (tomerge.size() == 1) { - const uint32_t into = *tomerge.begin(); - auto intoReverse = m_reverseTable.find(into); - for (uint32_t i = 0; i < newSet.size(); i++) { - intoReverse->second.push_back(newSet[i]); + const unsigned into = *tomerge.begin(); + unsigned_vector& intoReverse = m_reverseTable.find(into); + for (unsigned i = 0; i < newSet.size(); i++) { + intoReverse.push_back(newSet[i]); m_table[newSet[i]] = into; } continue; } - for (uint32_t v: tomerge) { - newSet.insert(newSet.end(), m_reverseTable[v].begin(), m_reverseTable[v].end()); + for (unsigned v: tomerge) { + for (const auto& v2 : m_reverseTable[v]) { + newSet.insert(v2); + } m_reverseTable.erase(v); } for (auto j : newSet) @@ -115,14 +117,13 @@ namespace xr { set_matrixes(); -#endif return !m_sat.inconsistent(); } unsigned xor_matrix_finder::set_matrixes() { svector matrix_shapes; - svector> xors_in_matrix(m_matrix_no); + vector> xors_in_matrix(m_matrix_no); for (unsigned i = 0; i < m_matrix_no; i++) { matrix_shapes.push_back(matrix_shape(i)); @@ -130,18 +131,18 @@ namespace xr { matrix_shapes[i].m_cols = m_reverseTable[i].size(); } - for (constraint* x : m_xor.m_constraints) { + for (xor_clause& x : m_xor.m_xorclauses) { // take 1st variable to check which matrix it's in. - const uint32_t matrix = m_table[(*x)[0]]; + const unsigned matrix = m_table[x[0]]; SASSERT(matrix < m_matrix_no); //for stats matrix_shapes[matrix].m_rows ++; - matrix_shapes[matrix].m_sum_xor_sizes += x->get_size(); + matrix_shapes[matrix].m_sum_xor_sizes += x.size(); xors_in_matrix[matrix].push_back(x); } - m_xor.m_constraints.clear(); + m_xor.m_xorclauses.clear(); for (auto& m: matrix_shapes) if (m.tot_size() > 0) @@ -182,7 +183,7 @@ namespace xr { // if already detached, we MUST use the matrix for (const auto& x: xors_in_matrix[i]) { - if (x->is_detached()) { + if (x.m_detached) { use_matrix = true; break; } @@ -191,23 +192,23 @@ namespace xr { if (m_sat.get_config().m_xor_gauss_force_use_all_matrices) use_matrix = true; -#if 0 if (use_matrix) { - m_xor.gmatrices.push_back( + m_xor.m_gmatrices.push_back( alloc(EGaussian, m_xor, realMatrixNum, xors_in_matrix[i])); - m_xor.gqueuedata.resize(m_solver->gmatrices.size()); + m_xor.m_gqueuedata.resize(m_xor.m_gmatrices.size()); realMatrixNum++; - SASSERT(m_xor.gmatrices.size() == realMatrixNum); + SASSERT(m_xor.m_gmatrices.size() == realMatrixNum); } else { for (auto& x: xors_in_matrix[i]) { - m_xor.xorclauses_unused.push_back(x); - clash_vars_unused.insert(x.clash_vars.begin(), x.clash_vars.end()); + m_xor.m_xorclauses_unused.push_back(x); + for (const auto& v : x.m_clash_vars) { + clash_vars_unused.insert(v); + } } unusedMatrix++; } -#endif } return realMatrixNum; } diff --git a/src/sat/smt/xor_matrix_finder.h b/src/sat/smt/xor_matrix_finder.h index b060dfc52..ddaade4df 100644 --- a/src/sat/smt/xor_matrix_finder.h +++ b/src/sat/smt/xor_matrix_finder.h @@ -18,6 +18,7 @@ Abstract: #include "util/uint_set.h" #include "util/map.h" #include "sat/sat_solver.h" +#include "sat/smt/xor_gaussian.h" namespace xr { @@ -25,17 +26,16 @@ namespace xr { class constraint; class xor_matrix_finder { - - + struct matrix_shape { matrix_shape(uint32_t matrix_num) : m_num(matrix_num) {} matrix_shape() {} - uint32_t m_num = 0; - uint32_t m_rows = 0; - uint32_t m_cols = 0; - uint32_t m_sum_xor_sizes = 0; + unsigned m_num = 0; + unsigned m_rows = 0; + unsigned m_cols = 0; + unsigned m_sum_xor_sizes = 0; double m_density = 0; uint64_t tot_size() const { @@ -59,7 +59,7 @@ namespace xr { unsigned set_matrixes(); - inline bool belong_same_matrix(const constraint& x); + inline bool belong_same_matrix(const xor_clause& x); public: xor_matrix_finder(solver& solver); diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp index 343933f38..fc43cd712 100644 --- a/src/sat/smt/xor_solver.cpp +++ b/src/sat/smt/xor_solver.cpp @@ -12,34 +12,207 @@ Abstract: --*/ - +#include "sat/smt/xor_matrix_finder.h" #include "sat/smt/xor_solver.h" #include "sat/sat_simplifier_params.hpp" #include "sat/sat_xor_finder.h" namespace xr { - - - solver::solver(euf::solver& ctx): + + solver::solver(euf::solver& ctx) : solver(ctx.get_manager(), ctx.get_manager().mk_family_id("xor")) { m_ctx = &ctx; } - solver::solver(ast_manager& m, euf::theory_id id) - : euf::th_solver(m, symbol("xor"), id) { + solver::solver(ast_manager& m, euf::theory_id id) : euf::th_solver(m, symbol("xor"), id) { } + + solver::~solver() { + /*for (justification* j : m_justifications) { + j->deallocate(m_allocator); + }*/ + clear_gauss_matrices(true); } euf::th_solver* solver::clone(euf::solver& ctx) { // and relevant copy internal state return alloc(solver, ctx); } + + void solver::add_every_combination_xor(const sat::literal_vector& lits, const bool attach) { + unsigned at = 0, num = 0; + sat::literal_vector xorlits; + m_tmp_xor_clash_vars.clear(); + sat::literal lastlit_added = sat::null_literal; + while (at != lits.size()) { + xorlits.clear(); + for (unsigned last_at = at; at < last_at + s().get_config().m_xor_gauss_var_per_cut && at < lits.size(); at++) { + xorlits.push_back(lits[at]); + } + + //Connect to old cut + if (lastlit_added != sat::null_literal) { + xorlits.push_back(lastlit_added); + } else if (at < lits.size()) { + xorlits.push_back(lits[at]); + at++; + } + + if (at + 1 == lits.size()) { + xorlits.push_back(lits[at]); + at++; + } + + //New lit to connect to next cut + if (at != lits.size()) { + const sat::bool_var new_var = m_solver->mk_var(); + m_tmp_xor_clash_vars.push_back(new_var); + const sat::literal to_add = sat::literal(new_var, false); + xorlits.push_back(to_add); + lastlit_added = to_add; + } + + // TODO: Implement the following function. Unfortunately, it is needed + // add_xor_clause_inter_cleaned_cut(xorlits, attach); + if (s().inconsistent()) + break; + + num++; + } + } + + void solver::add_xor_clause(const sat::literal_vector& lits, bool rhs, const bool attach) { + // TODO: make overload in which "lits" ==> svector; however, first implement missing function "add_xor_clause_inter_cleaned_cut" + if (s().inconsistent()) + return; + TRACE("xor", tout << "adding xor: " << lits << " rhs: " << rhs << "\n"); + SASSERT(!attach || m_prop_queue_head == m_prop_queue.size()); + SASSERT(s().at_search_lvl()); + + sat::literal_vector ps(lits); + for (sat::literal& lit: ps) { + if (lit.sign()) { + rhs ^= true; + lit.neg(); + } + } + clean_xor_no_prop(ps, rhs); + + if (ps.size() >= (0x01UL << 28)) + throw default_exception("xor clause too long"); + + if (ps.empty()) { + if (rhs) + m_solver->set_conflict(); + return; + } + + if (rhs) + ps[0].neg(); + + add_every_combination_xor(ps, attach); + if (ps.size() > 2) { + m_xor_clauses_updated = true; + m_xorclauses.push_back(xor_clause(ps, rhs, m_tmp_xor_clash_vars)); + m_xorclauses_orig.push_back(xor_clause(ps, rhs, m_tmp_xor_clash_vars)); + } + } - void solver::asserted(sat::literal l) { - + void solver::asserted(sat::literal l) { + TRACE("xor", tout << "asserted: " << l << "\n";); + force_push(); + m_prop_queue.push_back(l); } bool solver::unit_propagate() { - return false; + if (m_prop_queue_head == m_prop_queue.size()) + return false; + force_push(); + m_ctx->push(value_trail(m_prop_queue_head)); + for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) { + sat::literal const p = m_prop_queue[m_prop_queue_head]; + sat::justification conflict = gauss_jordan_elim(p, m_num_scopes); + if (conflict.is_none()) { + m_prop_queue_head = m_prop_queue.size(); + s().set_conflict(conflict); + } + } + return true; + } + + sat::justification solver::gauss_jordan_elim(const sat::literal p, const unsigned currLevel) { + if (m_gmatrices.empty()) + return sat::justification(-1); + for (unsigned i = 0; i < m_gqueuedata.size(); i++) { + if (m_gqueuedata[i].disabled || !m_gmatrices[i]->is_initialized()) continue; + m_gqueuedata[i].reset(); + m_gmatrices[i]->update_cols_vals_set(); + } + + bool confl_in_gauss = false; + SASSERT(m_gwatches.size() > p.var()); + svector& ws = m_gwatches[p.var()]; + gauss_watched* i = ws.begin(); + gauss_watched* j = i; + const gauss_watched* end = ws.end(); + + for (; i != end; i++) { + if (m_gqueuedata[i->matrix_num].disabled || !m_gmatrices[i->matrix_num]->is_initialized()) + continue; //remove watch and continue + + m_gqueuedata[i->matrix_num].new_resp_var = UINT_MAX; + m_gqueuedata[i->matrix_num].new_resp_row = UINT_MAX; + m_gqueuedata[i->matrix_num].do_eliminate = false; + m_gqueuedata[i->matrix_num].currLevel = currLevel; + + if (m_gmatrices[i->matrix_num]->find_truths(i, j, p.var(), i->row_n, m_gqueuedata[i->matrix_num])) { + continue; + } else { + confl_in_gauss = true; + i++; + break; + } + } + + for (; i != end; i++) + *j++ = *i; + ws.shrink((unsigned)(i - j)); + + for (unsigned g = 0; g < m_gqueuedata.size(); g++) { + if (m_gqueuedata[g].disabled || !m_gmatrices[g]->is_initialized()) + continue; + + if (m_gqueuedata[g].do_eliminate) { + m_gmatrices[g]->eliminate_col(p.var(), m_gqueuedata[g]); + confl_in_gauss |= (m_gqueuedata[g].status == gauss_res::confl); + } + } + + for (gauss_data& gqd: m_gqueuedata) { + if (gqd.disabled) continue; + + //There was a conflict but this is not that matrix. + //Just skip. + if (confl_in_gauss && gqd.status != gauss_res::confl) + continue; + + switch (gqd.status) { + case gauss_res::confl: + gqd.num_conflicts++; + return gqd.conflict; + + case gauss_res::prop: + gqd.num_props++; + break; + + case gauss_res::none: + //nothing + break; + + default: + UNREACHABLE(); + } + } + return sat::justification(-1); } void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, @@ -51,10 +224,44 @@ namespace xr { return sat::check_result::CR_DONE; } + // TODO: we should separate this parts from the euf_solver. Other non-euf theories might need it as well + // Similar: Attaching "theory_var"s in non-euf/enode cases + void solver::force_push() { + for (; m_num_scopes > 0; --m_num_scopes) { + push_core(); + } + } + + void solver::push_core() { + m_prop_queue_lim.push_back(m_prop_queue.size()); + //m_justifications_lim.push_back(m_justifications.size()); + } + + void solver::pop_core(unsigned num_scopes) { + SASSERT(m_num_scopes == 0); + unsigned old_sz = m_prop_queue_lim.size() - num_scopes; + m_prop_queue.shrink(m_prop_queue_lim[old_sz]); + m_prop_queue_lim.shrink(old_sz); + + /*old_sz = m_justifications_lim.size() - num_scopes; + unsigned lim = m_justifications_lim[old_sz]; + for (unsigned i = m_justifications.size(); i > lim; i--) { + m_justifications[i - 1].destroy(m_allocator); + } + m_justifications_lim.shrink(old_sz); + m_justifications.shrink(old_sz);*/ + } + void solver::push() { + m_num_scopes++; } void solver::pop(unsigned n) { + unsigned k = std::min(m_num_scopes, n); + m_num_scopes -= k; + n -= k; + if (n > 0) + pop_core(n); } // inprocessing @@ -73,6 +280,463 @@ namespace xr { return out; } + bool solver::clean_xor_clauses(vector& xors) { + SASSERT(!inconsistent()); + + unsigned last_trail = UINT_MAX; + while (last_trail != s().trail_size() && !inconsistent()) { + last_trail = s().trail_size(); + unsigned j = 0; + for (xor_clause& x : xors) { + if (inconsistent()) { + xors[j++] = x; + continue; + } + + const bool keep = clean_one_xor(x); + if (keep) { + SASSERT(x.size() > 2); + xors[j++] = x; + } + else { + for (const auto& v : x.m_clash_vars) { + m_removed_xorclauses_clash_vars.insert(v); + } + } + } + xors.shrink(j); + if (inconsistent()) break; + s().propagate(false); + } + + return !inconsistent(); + } + + + bool solver::clean_one_xor(xor_clause& x) { + + unsigned j = 0; + for (auto const& v : x.m_clash_vars) + if (s().value(v) == l_undef) + x.m_clash_vars[j++] = v; + + x.m_clash_vars.shrink(j); + + j = 0; + for (auto const& v : x) { + if (s().value(v) != l_undef) + x.m_rhs ^= s().value(v) == l_true; + else + x[j++] = v; + } + x.shrink(j); + SASSERT(!inconsistent()); + switch (x.size()) { + case 0: + if (x.m_rhs) + s().set_conflict(); + /*TODO: Implement + if (inconsistent()) { + SASSERT(m_solver.unsat_cl_ID == 0); + m_solver.unsat_cl_ID = solver->clauseID; + }*/ + return false; + case 1: { + s().assign_scoped(sat::literal(x[0], !x.m_rhs)); + s().propagate(false); + return false; + } + case 2: { + sat::literal_vector vec(x.size()); + for (const auto& v : x.m_vars) + vec.push_back(sat::literal(v)); + add_xor_clause(vec, x.m_rhs, true); + return false; + } + default: + return true; + } + } + + bool solver::clear_gauss_matrices(const bool destruct) { + // TODO: Include; ignored for now. Maybe we can ignore the detached clauses + /*if (!destruct) { + if (!fully_undo_xor_detach()) + return false; + }*/ + m_xor_clauses_updated = true; + + for (EGaussian* g: m_gmatrices) + g->move_back_xor_clauses(); + for (EGaussian* g: m_gmatrices) + dealloc(g); + for (auto& w: m_gwatches) + w.clear(); + + m_gmatrices.clear(); + m_gqueuedata.clear(); + + m_xorclauses.clear(); // we rely on xorclauses_orig now + m_xorclauses_unused.clear(); + + if (!destruct) + for (const auto& x: m_xorclauses_orig) + m_xorclauses.push_back(x); + + return !s().inconsistent(); + } + + bool solver::find_and_init_all_matrices() { + if (!m_xor_clauses_updated/* && (!m_detached_xor_clauses || !assump_contains_xor_clash())*/) + return true; + + bool can_detach; + if (!clear_gauss_matrices(false)) + return false; + + xor_matrix_finder mfinder(*this); + mfinder.find_matrices(can_detach); + if (s().inconsistent()) return false; + if (!init_all_matrices()) return false; + + /* TODO: Make this work (ignored for now) + bool ret_no_irred_nonxor_contains_clash_vars; + if (can_detach && + s().get_config().m_xor_gauss_detach_reattach && + !s().get_config().autodisable && + (ret_no_irred_nonxor_contains_clash_vars = no_irred_nonxor_contains_clash_vars())) { + detach_xor_clauses(mfinder.clash_vars_unused); + unset_clash_decision_vars(xorclauses); + rebuildOrderHeap(); + }*/ + m_xor_clauses_updated = false; + return true; + } + + bool solver::init_all_matrices() { + SASSERT(!s().inconsistent()); + SASSERT(s().at_search_lvl()); + SASSERT(m_gmatrices.size() == m_gqueuedata.size()); + + for (unsigned i = 0; i < m_gmatrices.size(); i++) { + auto& g = m_gmatrices[i]; + bool created = false; + if (!g->full_init(created)) + return false; + SASSERT(!s().inconsistent()); + + if (!created) { + m_gqueuedata[i].disabled = true; + memory::deallocate(g); + g = nullptr; + } + } + + unsigned j = 0; + bool modified = false; + for (unsigned i = 0; i < m_gqueuedata.size(); i++) { + if (m_gmatrices[i] == nullptr) { + modified = true; + continue; + } + if (!modified) { + j++; + continue; + } + m_gmatrices[j] = m_gmatrices[i]; + m_gmatrices[j]->update_matrix_no(j); + m_gqueuedata[j] = m_gqueuedata[i]; + + for (unsigned var = 0; var < s().num_vars(); var++) { + for (gauss_watched& k : m_gwatches[var]) { + if (k.matrix_num == i) + k.matrix_num = j; + } + } + j++; + } + m_gqueuedata.shrink(j); + m_gmatrices.shrink(j); + + return !s().inconsistent(); + } + + bool solver::xor_has_interesting_var(const xor_clause& x) { + return std::any_of(x.begin(), x.end(), [&](bool_var v) { return s().num_visited(v) > 1; }); + } + + void solver::move_xors_without_connecting_vars_to_unused() { + if (m_xorclauses.empty()) + return; + + vector cleaned; + s().init_visited(2); + + for(const xor_clause& x: m_xorclauses) { + for (unsigned v : x) { + s().inc_visited(v); + } + } + + //has at least 1 var with occur of 2 + for(const xor_clause& x: m_xorclauses) { + if (xor_has_interesting_var(x) || x.m_detached) { + TRACE("xor", tout << "XOR has connecting var: " << x << "\n";); + cleaned.push_back(x); + } else { + TRACE("xor", tout << "XOR has no connecting var: " << x << "\n";); + m_xorclauses_unused.push_back(x); + } + } + + m_xorclauses = cleaned; + } + + void solver::clean_equivalent_xors(vector& txors){ + if (!txors.empty()) { + size_t orig_size = txors.size(); + for (xor_clause& x: txors) { + std::sort(x.begin(), x.end()); + } + std::sort(txors.begin(), txors.end()); + + unsigned sz = 1; + unsigned j = 0; + for (unsigned i = 1; i < txors.size(); i++) { + auto& jd = txors[j]; + auto& id = txors[i]; + if (jd.m_vars == id.m_vars && jd.m_rhs == id.m_rhs) { + jd.merge_clash(id, m_visited); + jd.m_detached |= id.m_detached; + } else { + j++; + j = i; + sz++; + } + } + txors.resize(sz); + } + } + + sat::justification solver::mk_justification(const int level, const unsigned int matrix_no, const unsigned int row_i) { + void* mem = m_ctx->get_region().allocate(justification::get_obj_size()); + sat::constraint_base::initialize(mem, this); + auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(matrix_no, row_i); + return sat::justification::mk_ext_justification(level, constraint->to_index()); + } + + void solver::clean_xor_no_prop(sat::literal_vector & ps, bool & rhs) { + std::sort(ps.begin(), ps.end()); + sat::literal p = sat::null_literal; + unsigned i = 0, j = 0; + for (; i != ps.size(); i++) { + SASSERT(!ps[i].sign()); + if (ps[i].var() == p.var()) { + //added, but easily removed + j--; + p = sat::null_literal; + //Flip rhs if necessary + if (s().value(ps[i]) != l_undef) { + rhs ^= s().value(ps[i]) == l_true; + } + } else if (s().value(ps[i]) == l_undef) { + //Add and remember as last one to have been added + ps[j++] = p = ps[i]; + } else { + //modify rhs instead of adding + rhs ^= s().value(ps[i]) == l_true; + } + } + ps.resize(ps.size() - (i - j)); + } + + bool solver::xor_together_xors(vector& xors) { + + if (xors.empty()) + return !s().inconsistent(); + + if (m_occ_cnt.size() != s().num_vars()) { + m_occ_cnt.clear(); + m_occ_cnt.resize(s().num_vars(), 0); + } + + TRACE_CODE( + TRACE("xor", tout << "XOR-ing together XORs. Starting with: " << "\n";); + for (const auto& x: xors) { + TRACE("xor", tout << "XOR before xor-ing together: " << x << "\n";); + }; + ); + + SASSERT(!s().inconsistent()); + SASSERT(s().at_search_lvl()); + const size_t origsize = xors.size(); + + unsigned xored = 0; + SASSERT(m_occurrences.empty()); + #if 0 + //Link in xors into watchlist + for (unsigned i = 0; i < xors.size(); i++) { + const xor_clause& x = xors[i]; + for (bool_var v: x) { + if (m_occ_cnt[v] == 0) { + m_occurrences.push_back(v); + } + m_occ_cnt[v]++; + + sat::literal l(v, false); + SASSERT(s()->watches.size() > l.toInt()); + m_watches[l].push(Watched(i, WatchType::watch_idx_t)); + m_watches.smudge(l); + } + } + + //Don't XOR together over variables that are in regular clauses + s().init_visited(); + + for (unsigned i = 0; i < 2 * s().num_vars(); i++) { + const auto& ws = s().get_wlist(i); + for (const auto& w: ws) { + if (w.is_binary_clause()/* TODO: Does redundancy information exist in Z3? Can we use learned instead of "!w.red()"?*/ && !w.is_learned()) { + sat::bool_var v = w.get_literal().var(); + s().mark_visited(v); + } + } + } + + for (const auto& cl: s().clauses()) { + /* TODO: Do we need this? Are the xors still in the clause set? + if (cl->red() || cl->used_in_xor()) { + continue; + }*/ + // TODO: maybe again instead + if (cl->is_learned()) + continue; + for (literal l: *cl) + s().mark_visited(l.var()); + } + + //until fixedpoint + bool changed = true; + while (changed) { + changed = false; + m_interesting.clear(); + for (const unsigned l : m_occurrences) { + if (m_occ_cnt[l] == 2 && !s().is_visited(l)) { + m_interesting.push_back(l); + } + } + + while (!m_interesting.empty()) { + + //Pop and check if it can be XOR-ed together + const unsigned v = m_interesting.back(); + m_interesting.resize(m_interesting.size()-1); + if (m_occ_cnt[v] != 2) + continue; + + unsigned indexes[2]; + unsigned at = 0; + size_t i2 = 0; + //SASSERT(watches.size() > literal(v, false).index()); + vector ws = s().get_wlist(literal(v, false)); + + //Remove the 2 indexes from the watchlist + for (unsigned i = 0; i < ws.size(); i++) { + const sat::watched& w = ws[i]; + if (!w.isIdx()) { + ws[i2++] = ws[i]; + } else if (!xors[w.get_idx()].empty()) { + SASSERT(at < 2); + indexes[at] = w.get_idx(); + at++; + } + } + SASSERT(at == 2); + ws.resize(i2); + + xor_clause& x0 = xors[indexes[0]]; + xor_clause& x1 = xors[indexes[1]]; + unsigned clash_var; + unsigned clash_num = xor_two(&x0, &x1, clash_var); + + //If they are equivalent + if (x0.size() == x1.size() + && x0.m_rhs == x1.m_rhs + && clash_num == x0.size() + ) { + TRACE("xor", tout + << "x1: " << x0 << " -- at idx: " << indexes[0] + << "and x2: " << x1 << " -- at idx: " << indexes[1] + << "are equivalent.\n"); + + //Update clash values & detached values + x1.merge_clash(x0, m_visited); + x1.m_detached |= x0.m_detached; + + TRACE("xor", tout << "after merge: " << x1 << " -- at idx: " << indexes[1] << "\n";); + + x0 = xor_clause(); + + //Re-attach the other, remove the occur of the one we deleted + s().m_watches[Lit(v, false)].push(Watched(indexes[1], WatchType::watch_idx_t)); + + for (unsigned v2: x1) { + sat::literal l(v2, false); + SASSERT(m_occ_cnt[l.var()] >= 2); + m_occ_cnt[l.var()]--; + if (m_occ_cnt[l.var()] == 2 && !s().is_visited(l.var())) { + m_interesting.push_back(l.var()); + } + } + } else if (clash_num > 1 || x0.m_detached || x1.m_detached) { + //add back to ws, can't do much + ws.push(Watched(indexes[0], WatchType::watch_idx_t)); + ws.push(Watched(indexes[1], WatchType::watch_idx_t)); + continue; + } else { + m_occ_cnt[v] -= 2; + SASSERT(m_occ_cnt[v] == 0); + + xor_clause x_new(m_tmp_vars_xor_two, x0.m_rhs ^ x1.m_rhs, clash_var); + x_new.merge_clash(x0, m_visited); + x_new.merge_clash(x1, m_visited); + + TRACE("xor", tout + << "x1: " << x0 << " -- at idx: " << indexes[0] << "\n" + << "x2: " << x1 << " -- at idx: " << indexes[1] << "\n" + << "clashed on var: " << clash_var+1 << "\n" + << "final: " << x_new << " -- at idx: " << xors.size() << "\n";); + + changed = true; + xors.push_back(x_new); + for(uint32_t v2: x_new) { + sat::literal l(v2, false); + s().watches[l].push(Watched(xors.size()-1, WatchType::watch_idx_t)); + SASSERT(m_occ_cnt[l.var()] >= 1); + if (m_occ_cnt[l.var()] == 2 && !s().is_visited(l.var())) { + m_interesting.push_back(l.var()); + } + } + xors[indexes[0]] = xor_clause(); + xors[indexes[1]] = xor_clause(); + xored++; + } + } + } + + //Clear + for (const bool_var l : m_occurrences) { + m_occ_cnt[l] = 0; + } + m_occurrences.clear(); + + clean_occur_from_idx_types_only_smudged(); + clean_xors_from_empty(xors); + #endif + + return !s().inconsistent(); + } + std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { return out; } @@ -80,6 +744,5 @@ namespace xr { std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { return out; } - } diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h index fd1e902e5..845446d58 100644 --- a/src/sat/smt/xor_solver.h +++ b/src/sat/smt/xor_solver.h @@ -15,178 +15,80 @@ Abstract: #pragma once #include "sat/smt/euf_solver.h" +#include "sat/smt/xor_gaussian.h" namespace xr { - - class constraint { - unsigned m_size; - bool m_detached = false; - size_t m_obj_size; - bool m_rhs; - sat::bool_var m_vars[0]; - - public: - static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(constraint) + num_lits * sizeof(sat::bool_var)); } - - constraint(const svector& ids, bool expected_result) : m_size(ids.size()), m_obj_size(get_obj_size(ids.size())), m_rhs(expected_result) { - unsigned i = 0; - for (auto v : ids) - m_vars[i++] = v; - } - sat::ext_constraint_idx cindex() const { return sat::constraint_base::mem2base(this); } - void deallocate(small_object_allocator& a) { a.deallocate(m_obj_size, sat::constraint_base::mem2base_ptr(this)); } - sat::bool_var operator[](unsigned i) const { return m_vars[i]; } - bool is_detached() const { return m_detached; } - unsigned get_size() const { return m_size; } - bool get_rhs() const { return m_rhs; } - sat::bool_var const* begin() const { return m_vars; } - sat::bool_var const* end() const { return m_vars + m_size; } - std::ostream& display(std::ostream& out) const { - bool first = true; - for (auto v : *this) - out << (first ? "" : " ^ ") << v, first = false; - return out << " = " << m_rhs; - } - }; - -#if 0 - class EGaussian { - public: - EGaussian( - solver* solver, - const uint32_t matrix_no, - const vector& xorclauses - ); - ~EGaussian(); - bool is_initialized() const; - - ///returns FALSE in case of conflict - bool find_truths( - GaussWatched*& i, - GaussWatched*& j, - const uint32_t var, - const uint32_t row_n, - gauss_data& gqd - ); - - vector* get_reason(const uint32_t row, int32_t& out_ID); - - // when basic variable is touched , eliminate one col - void eliminate_col( - uint32_t p, - gauss_data& gqd - ); - void canceling(); - bool full_init(bool& created); - void update_cols_vals_set(bool force = false); - void print_matrix_stats(uint32_t verbosity); - bool must_disable(gauss_data& gqd); - void check_invariants(); - void update_matrix_no(uint32_t n); - void check_watchlist_sanity(); - uint32_t get_matrix_no(); - void finalize_frat(); - void move_back_xor_clauses(); - - vector xorclauses; - - private: - solver* solver; // orignal sat solver - - //Cleanup - void clear_gwatches(const uint32_t var); - void delete_gauss_watch_this_matrix(); - void delete_gausswatch(const uint32_t row_n); - - //Invariant checks, debug - void check_no_prop_or_unsat_rows(); - void check_tracked_cols_only_one_set(); - bool check_row_satisfied(const uint32_t row); - void print_gwatches(const uint32_t var) const; - void check_row_not_in_watch(const uint32_t v, const uint32_t row_num) const; - - //Reason generation - vector xor_reasons; - vector tmp_clause; - uint32_t get_max_level(const GaussQData& gqd, const uint32_t row_n); - - //Initialisation - void eliminate(); - void fill_matrix(); - void select_columnorder(); - gret init_adjust_matrix(); // adjust matrix, include watch, check row is zero, etc. - double get_density(); - - //Helper functions - void prop_lit( - const gauss_data& gqd, const uint32_t row_i, const Lit ret_lit_prop); - - /////////////// - // Internal data - /////////////// - uint32_t matrix_no; - bool initialized = false; - bool cancelled_since_val_update = true; - uint32_t last_val_update = 0; - - //Is the clause at this ROW satisfied already? - //satisfied_xors[decision_level][row] tells me that - vector satisfied_xors; - - // Someone is responsible for this column if TRUE - ///we always WATCH this variable - vector var_has_resp_row; - - ///row_to_var_non_resp[ROW] gives VAR it's NOT responsible for - ///we always WATCH this variable - vector row_to_var_non_resp; - - - PackedMatrix mat; - vector> bdd_matrix; - vector var_to_col; ///var->col mapping. Index with VAR - vector col_to_var; ///col->var mapping. Index with COL - uint32_t num_rows = 0; - uint32_t num_cols = 0; - - //quick lookup - PackedRow* cols_vals = NULL; - PackedRow* cols_unset = NULL; - PackedRow* tmp_col = NULL; - PackedRow* tmp_col2 = NULL; - void update_cols_vals_set(const Lit lit1); - - //Data to free (with delete[] x) - vector tofree; - }; -#endif + + class solver; class solver : public euf::th_solver { friend class xor_matrix_finder; + friend class EGaussian; + euf::solver* m_ctx = nullptr; - euf::solver* m_ctx = nullptr; + unsigned m_num_scopes = 0; - ptr_vector m_constraints; + literal_vector m_prop_queue; + unsigned_vector m_prop_queue_lim; + unsigned m_prop_queue_head = 0; + // ptr_vector m_justifications; + // unsigned_vector m_justifications_lim; -// ptr_vector gmatrices; + bool_var_vector m_tmp_xor_clash_vars; + + vector m_xorclauses; + vector m_xorclauses_orig; + vector m_xorclauses_unused; + + bool_var_vector m_removed_xorclauses_clash_vars; + bool m_detached_xor_clauses = false; + bool m_xor_clauses_updated = false; + + vector> m_gwatches; + ptr_vector m_gmatrices; + svector m_gqueuedata; + + visit_helper m_visited; + + // tmp + bool_var_vector m_occurrences; + // unfortunately, we cannot use generic "m_visited" here, + // as the number of occurrences might be quite high + // and we need the list of occurrences + unsigned_vector m_occ_cnt; + bool_var_vector m_interesting; + + void force_push(); + void push_core(); + void pop_core(unsigned num_scopes); + bool xor_has_interesting_var(const xor_clause& x); + + void clean_xor_no_prop(sat::literal_vector& ps, bool& rhs); + void add_every_combination_xor(const sat::literal_vector& lits, const bool attach); + + void add_xor_clause(const sat::literal_vector& lits, bool rhs, const bool attach); + + bool inconsistent() const { return s().inconsistent(); } + public: solver(euf::solver& ctx); solver(ast_manager& m, euf::theory_id id); + ~solver() override; th_solver* clone(euf::solver& ctx) override; - - void add_xor(sat::literal_vector const& lits) override { NOT_IMPLEMENTED_YET(); } - - + void add_xor(const sat::literal_vector& lits) override { + add_xor_clause(lits, true, true); + } + sat::literal internalize(expr* e, bool sign, bool root) override { UNREACHABLE(); return sat::null_literal; } void internalize(expr* e) override { UNREACHABLE(); } - - + void asserted(sat::literal l) override; bool unit_propagate() override; + sat::justification gauss_jordan_elim(const sat::literal p, const unsigned currLevel); void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override; void pre_simplify() override; @@ -195,11 +97,26 @@ namespace xr { sat::check_result check() override; void push() override; void pop(unsigned n) override; - + + void init_search() override { + find_and_init_all_matrices(); + } + + bool clean_xor_clauses(vector& xors); + bool clean_one_xor(xor_clause& x); + bool clear_gauss_matrices(const bool destruct); + bool find_and_init_all_matrices(); + bool init_all_matrices(); + + void move_xors_without_connecting_vars_to_unused(); + void clean_equivalent_xors(vector& txors); + + bool xor_together_xors(vector& xors); + + sat::justification mk_justification(const int level, const unsigned int matrix_no, const unsigned int row_i); + std::ostream& display(std::ostream& out) const override; std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override; std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; - - }; - +}; } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 96a1a51a4..749608e8e 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -37,7 +37,7 @@ Notes: #include "model/model_evaluator.h" #include "model/model_v2_pp.h" #include "tactic/tactic.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "sat/sat_cut_simplifier.h" #include "sat/sat_drat.h" #include "sat/tactic/goal2sat.h" diff --git a/src/sat/tactic/sat2goal.cpp b/src/sat/tactic/sat2goal.cpp index 7614857cb..899345ad8 100644 --- a/src/sat/tactic/sat2goal.cpp +++ b/src/sat/tactic/sat2goal.cpp @@ -37,7 +37,7 @@ Notes: #include "model/model_evaluator.h" #include "model/model_v2_pp.h" #include "tactic/tactic.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "sat/sat_cut_simplifier.h" #include "sat/sat_drat.h" #include "sat/tactic/sat2goal.h" diff --git a/src/sat/tactic/sat2goal.h b/src/sat/tactic/sat2goal.h index 1e1dfcd5e..8c0b1bf83 100644 --- a/src/sat/tactic/sat2goal.h +++ b/src/sat/tactic/sat2goal.h @@ -31,7 +31,7 @@ Notes: #include "tactic/goal.h" #include "sat/sat_model_converter.h" #include "sat/sat_solver.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "sat/smt/atom2bool_var.h" class sat2goal { diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 24bfb3355..40e789204 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -166,7 +166,7 @@ namespace smt { unsigned num = get_num_bool_vars(); for (unsigned v = 0; v < num; v++) { expr * n = m_bool_var2expr[v]; - ast_def_ll_pp(out, m, n, get_pp_visited(), true, false); + ast_def_ll_pp(out << v << " ", m, n, get_pp_visited(), true, false); } } diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index 5527f12f5..5ef52a54c 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -26,7 +26,7 @@ Notes: #include "smt/smt_solver.h" #include "tactic/tactic.h" #include "tactic/tactical.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "solver/solver2tactic.h" #include "solver/solver.h" #include "solver/mus.h" diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 4b57f043e..593c32d83 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -22,7 +22,7 @@ Revision History: #include "smt/theory_arith.h" #include "smt/smt_farkas_util.h" #include "ast/rewriter/th_rewriter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" namespace smt { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c46331d07..4075f39dd 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -43,7 +43,7 @@ #include "smt/smt_model_generator.h" #include "smt/arith_eq_adapter.h" #include "util/nat_set.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "util/cancel_eh.h" diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h index 03a205ca6..9cac6b96b 100644 --- a/src/smt/theory_wmaxsat.h +++ b/src/smt/theory_wmaxsat.h @@ -21,7 +21,7 @@ Notes: #include "smt/smt_theory.h" #include "smt/smt_clause.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" namespace smt { class theory_wmaxsat : public theory { diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index e00b53cc9..936f6d3df 100644 --- a/src/solver/check_sat_result.h +++ b/src/solver/check_sat_result.h @@ -23,7 +23,7 @@ Notes: #include "util/statistics.h" #include "util/event_handler.h" #include "util/timer.h" -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" /** \brief Abstract interface for the result of a (check-sat) like command. diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index d582ec2db..bf05554af 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -22,7 +22,7 @@ Notes: #include "ast/ast_pp.h" #include "ast/ast_pp_util.h" #include "ast/display_dimacs.h" -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "solver/solver.h" #include "params/solver_params.hpp" #include "model/model_evaluator.h" diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index 81d21f959..b8e3dd37a 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -19,7 +19,7 @@ Notes: #include "solver/solver.h" #include "tactic/tactic.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "solver/solver2tactic.h" #include "ast/ast_util.h" diff --git a/src/solver/solver2tactic.h b/src/solver/solver2tactic.h index a5b529f69..4640ee276 100644 --- a/src/solver/solver2tactic.h +++ b/src/solver/solver2tactic.h @@ -19,7 +19,7 @@ Notes: #pragma once #include "tactic/tactic.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" class solver; tactic * mk_solver2tactic(solver* s); diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt index 114e4f849..72bbbc303 100644 --- a/src/tactic/CMakeLists.txt +++ b/src/tactic/CMakeLists.txt @@ -1,25 +1,19 @@ z3_add_component(tactic SOURCES dependency_converter.cpp - equiv_proof_converter.cpp - generic_model_converter.cpp goal.cpp goal_num_occurs.cpp goal_shared_occs.cpp goal_util.cpp - horn_subsume_model_converter.cpp - model_converter.cpp probe.cpp - proof_converter.cpp - replace_proof_converter.cpp tactical.cpp tactic.cpp COMPONENT_DEPENDENCIES ast model + simplifiers + converters TACTIC_HEADERS probe.h tactic.h - PYG_FILES - tactic_params.pyg ) diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 25c5620c2..4f79a887d 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -22,7 +22,7 @@ Notes: #include "ast/rewriter/pb2bv_rewriter.h" #include "ast/ast_util.h" #include "ast/ast_pp.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" class card2bv_tactic : public tactic { ast_manager & m; diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index e34910e78..26c3f9ef5 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -20,7 +20,7 @@ Revision History: --*/ #include "tactic/tactical.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/arith_decl_plugin.h" #include "tactic/core/simplify_tactic.h" #include "ast/ast_smt2_pp.h" diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 87061b189..13479e1bf 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -23,7 +23,7 @@ Revision History: --*/ #include "tactic/tactical.h" #include "ast/rewriter/th_rewriter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/arith_decl_plugin.h" #include "ast/expr_substitution.h" #include "ast/ast_smt2_pp.h" diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 97c6f466f..cb6f6c228 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -25,7 +25,7 @@ Notes: #include "ast/ast_pp_util.h" #include "tactic/tactical.h" #include "tactic/arith/bound_manager.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" class lia2card_tactic : public tactic { diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 46404ffb0..f78e85621 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -20,7 +20,7 @@ Revision History: #include "tactic/arith/bound_manager.h" #include "ast/rewriter/th_rewriter.h" #include "ast/for_each_expr.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/arith_decl_plugin.h" #include "ast/expr_substitution.h" #include "ast/ast_smt2_pp.h" diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index 36df89da5..bdcf57953 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -27,7 +27,7 @@ Notes: #include "util/optional.h" #include "tactic/arith/bv2int_rewriter.h" #include "tactic/arith/bv2real_rewriter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "tactic/arith/bound_manager.h" #include "util/obj_pair_hashtable.h" #include "ast/ast_smt2_pp.h" diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index b7ef28f49..cba791ee1 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -21,7 +21,7 @@ Revision History: #include "tactic/tactical.h" #include "tactic/arith/bound_manager.h" #include "ast/rewriter/th_rewriter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/arith_decl_plugin.h" #include "ast/expr_substitution.h" #include "ast/ast_smt2_pp.h" diff --git a/src/tactic/arith/pb2bv_model_converter.h b/src/tactic/arith/pb2bv_model_converter.h index 5560ce7da..2de873ba2 100644 --- a/src/tactic/arith/pb2bv_model_converter.h +++ b/src/tactic/arith/pb2bv_model_converter.h @@ -18,7 +18,7 @@ Notes: --*/ #pragma once -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "tactic/arith/bound_manager.h" class pb2bv_model_converter : public model_converter { diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index c418115a9..5ff7425ba 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -29,7 +29,7 @@ Notes: #include "ast/rewriter/pb2bv_rewriter.h" #include "tactic/tactical.h" #include "tactic/arith/bound_manager.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "tactic/arith/pb2bv_model_converter.h" #include "tactic/arith/pb2bv_tactic.h" diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index afcecd7d3..7c69ef12e 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -27,7 +27,7 @@ Revision History: #include "tactic/core/nnf_tactic.h" #include "tactic/core/simplify_tactic.h" #include "ast/rewriter/th_rewriter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_pp.h" #include "ast/rewriter/expr_replacer.h" diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 251d78e72..d97f9b80f 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -57,7 +57,7 @@ Revision History: --*/ #include "tactic/tactical.h" #include "ast/rewriter/th_rewriter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/arith_decl_plugin.h" #include "ast/expr_substitution.h" #include "util/dec_ref_util.h" diff --git a/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt index e9f0927d5..653571265 100644 --- a/src/tactic/bv/CMakeLists.txt +++ b/src/tactic/bv/CMakeLists.txt @@ -8,6 +8,7 @@ z3_add_component(bv_tactics bv_bound_chk_tactic.cpp bv_bounds_tactic.cpp bv_size_reduction_tactic.cpp + bv_slice_tactic.cpp dt2bv_tactic.cpp elim_small_bv_tactic.cpp max_bv_sharing_tactic.cpp @@ -21,6 +22,7 @@ z3_add_component(bv_tactics bv_bound_chk_tactic.h bv_bounds_tactic.h bv_size_reduction_tactic.h + bv_slice_tactic.h bvarray2uf_tactic.h dt2bv_tactic.h elim_small_bv_tactic.h diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index 5c26fb2b5..88ff11683 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include "model/model.h" #include "model/model_pp.h" -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "ast/bv_decl_plugin.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_pp.h" diff --git a/src/tactic/bv/bit_blaster_model_converter.h b/src/tactic/bv/bit_blaster_model_converter.h index debfdd526..dae3cd40e 100644 --- a/src/tactic/bv/bit_blaster_model_converter.h +++ b/src/tactic/bv/bit_blaster_model_converter.h @@ -18,7 +18,7 @@ Notes: --*/ #pragma once -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" model_converter * mk_bit_blaster_model_converter(ast_manager & m, obj_map const & const2bits, ptr_vector const& newbits); model_converter * mk_bv1_blaster_model_converter(ast_manager & m, obj_map const & const2bits, ptr_vector const& newbits); diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 788f562d3..286375b6a 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -24,7 +24,7 @@ Notes: #include "tactic/tactical.h" #include "ast/bv_decl_plugin.h" #include "ast/rewriter/expr_replacer.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/ast_smt2_pp.h" namespace { diff --git a/src/tactic/bv/bv_slice_tactic.cpp b/src/tactic/bv/bv_slice_tactic.cpp new file mode 100644 index 000000000..040068e39 --- /dev/null +++ b/src/tactic/bv/bv_slice_tactic.cpp @@ -0,0 +1,33 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + bv_slice_tactic.cpp + +Abstract: + + Tactic for simplifying with bit-vector slices + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-30 + +--*/ + +#include "ast/simplifiers/bv_slice.h" +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "tactic/bv/bv_slice_tactic.h" + + +class bv_slice_factory : public dependent_expr_simplifier_factory { +public: + dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { + return alloc(bv::slice, m, s); + } +}; + +tactic* mk_bv_slice_tactic(ast_manager& m, params_ref const& p) { + return alloc(dependent_expr_state_tactic, m, p, alloc(bv_slice_factory), "bv-slice"); +} diff --git a/src/tactic/bv/bv_slice_tactic.h b/src/tactic/bv/bv_slice_tactic.h new file mode 100644 index 000000000..23ed16680 --- /dev/null +++ b/src/tactic/bv/bv_slice_tactic.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + bv_slice_tactic.h + +Abstract: + + Tactic for simplifying with bit-vector slices + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-30 + +--*/ +#pragma once + +#include "util/params.h" +class ast_manager; +class tactic; + +tactic * mk_bv_slice_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("bv-slice", "simplify using bit-vector slices.", "mk_bv_slice_tactic(m, p)") +*/ + + diff --git a/src/tactic/bv/bvarray2uf_rewriter.h b/src/tactic/bv/bvarray2uf_rewriter.h index df5c93a14..d6733d4a6 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.h +++ b/src/tactic/bv/bvarray2uf_rewriter.h @@ -20,7 +20,7 @@ Notes: #pragma once #include "ast/rewriter/rewriter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" class bvarray2uf_rewriter_cfg : public default_rewriter_cfg { ast_manager & m_manager; diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index da86ed663..3a4971e04 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -20,7 +20,7 @@ Notes: #include "tactic/tactical.h" #include "ast/bv_decl_plugin.h" #include "ast/rewriter/expr_replacer.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/ast_smt2_pp.h" #include "tactic/bv/bvarray2uf_tactic.h" diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 650095207..190403349 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -21,7 +21,7 @@ Revision History: #include "tactic/bv/dt2bv_tactic.h" #include "tactic/tactical.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/datatype_decl_plugin.h" #include "ast/bv_decl_plugin.h" #include "ast/rewriter/rewriter_def.h" diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 02ec522c6..54f4dc915 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #include "tactic/tactical.h" #include "ast/rewriter/rewriter_def.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/bv_decl_plugin.h" #include "ast/used_vars.h" #include "ast/well_sorted.h" diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index a247c7b20..e57510d4f 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -10,6 +10,7 @@ z3_add_component(core_tactics dom_simplify_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp + euf_completion_tactic.cpp injectivity_tactic.cpp nnf_tactic.cpp occf_tactic.cpp @@ -38,6 +39,7 @@ z3_add_component(core_tactics dom_simplify_tactic.h elim_term_ite_tactic.h elim_uncnstr_tactic.h + euf_completion_tactic.h injectivity_tactic.h nnf_tactic.h occf_tactic.h diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index 38b4e172e..49e43e633 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -20,7 +20,7 @@ Notes: #include "ast/rewriter/rewriter_def.h" #include "ast/scoped_proof.h" #include "tactic/tactical.h" -#include "tactic/tactic_params.hpp" +#include "params/tactic_params.hpp" diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index 2a0593ade..c67443862 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -20,7 +20,7 @@ Notes: #include "tactic/tactical.h" #include "ast/normal_forms/defined_names.h" #include "ast/rewriter/rewriter_def.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" class elim_term_ite_tactic : public tactic { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index c97fa670e..cb60eb482 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "tactic/tactical.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/rewriter/rewriter_def.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" diff --git a/src/tactic/core/euf_completion_tactic.cpp b/src/tactic/core/euf_completion_tactic.cpp new file mode 100644 index 000000000..bdd940f17 --- /dev/null +++ b/src/tactic/core/euf_completion_tactic.cpp @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + euf_completion_tactic.cpp + +Abstract: + + Tactic for simplifying with equations. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-30 + +--*/ + +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/euf_completion.h" +#include "tactic/core/euf_completion_tactic.h" + +class euf_completion_tactic_factory : public dependent_expr_simplifier_factory { +public: + dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { + return alloc(euf::completion, m, s); + } +}; + +tactic * mk_euf_completion_tactic(ast_manager& m, params_ref const& p) { + return alloc(dependent_expr_state_tactic, m, p, alloc(euf_completion_tactic_factory), "euf-completion"); +} diff --git a/src/tactic/core/euf_completion_tactic.h b/src/tactic/core/euf_completion_tactic.h new file mode 100644 index 000000000..36511bbe3 --- /dev/null +++ b/src/tactic/core/euf_completion_tactic.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + euf_completion_tactic.h + +Abstract: + + Tactic for simplifying with equations. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-30 + +--*/ +#pragma once + +#include "util/params.h" +class ast_manager; +class tactic; + +tactic * mk_euf_completion_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("euf-completion", "simplify using equalities.", "mk_euf_completion_tactic(m, p)") +*/ + + diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index 959a1fc18..3a5ce8d0a 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #include "ast/normal_forms/nnf.h" #include "tactic/tactical.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" class nnf_tactic : public tactic { params_ref m_params; diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index c3c027fef..1784a434d 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -23,7 +23,7 @@ Revision History: --*/ #include "tactic/tactical.h" #include "tactic/core/occf_tactic.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" class occf_tactic : public tactic { struct imp { diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 2c4b80b93..9f0717135 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -33,7 +33,7 @@ Notes: --*/ #include "tactic/core/pb_preprocess_tactic.h" #include "tactic/tactical.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/for_each_expr.h" #include "ast/pb_decl_plugin.h" #include "ast/rewriter/th_rewriter.h" diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 5b7fcbf10..041e4d1c2 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -24,7 +24,7 @@ Revision History: #include "ast/ast_pp.h" #include "ast/expr_substitution.h" #include "tactic/goal_shared_occs.h" -#include "tactic/tactic_params.hpp" +#include "params/tactic_params.hpp" namespace { class propagate_values_tactic : public tactic { diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 7f0d82f2e..b2a10fafa 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -22,7 +22,7 @@ Notes: #include "ast/has_free_vars.h" #include "util/map.h" #include "ast/rewriter/rewriter_def.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" /** \brief Reduce the number of arguments in function applications. diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index df3de8219..ba9b5d752 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -29,7 +29,7 @@ Notes: #include "tactic/tactic.h" #include "tactic/core/reduce_invertible_tactic.h" #include "tactic/core/collect_occs.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include namespace { diff --git a/src/tactic/core/solve_eqs2_tactic.h b/src/tactic/core/solve_eqs2_tactic.h new file mode 100644 index 000000000..91b3875ae --- /dev/null +++ b/src/tactic/core/solve_eqs2_tactic.h @@ -0,0 +1,41 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + solve_eqs2_tactic.h + +Abstract: + + Tactic for solving variables + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-30 + +--*/ +#pragma once + +#include "util/params.h" +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/solve_eqs.h" + + +class solve_eqs2_tactic_factory : public dependent_expr_simplifier_factory { +public: + dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { + return alloc(euf::solve_eqs, m, s); + } +}; + +inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p) { + return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs2"); +} + + +/* + ADD_TACTIC("solve-eqs2", "solve for variables.", "mk_solve_eqs2_tactic(m, p)") +*/ + + diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index a7b206d5b..3e338b57e 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -27,8 +27,8 @@ Revision History: #include "ast/rewriter/hoist_rewriter.h" #include "tactic/goal_shared_occs.h" #include "tactic/tactical.h" -#include "tactic/generic_model_converter.h" -#include "tactic/tactic_params.hpp" +#include "ast/converters/generic_model_converter.h" +#include "params/tactic_params.hpp" class solve_eqs_tactic : public tactic { struct imp { @@ -977,14 +977,8 @@ class solve_eqs_tactic : public tactic { if (m_produce_models) { if (!mc.get()) mc = alloc(gmc, m(), "solve-eqs"); - for (app* v : m_ordered_vars) { - expr * def = nullptr; - proof * pr; - expr_dependency * dep = nullptr; - m_norm_subst->find(v, def, pr, dep); - SASSERT(def); - static_cast(mc.get())->add(v, def); - } + for (app* v : m_ordered_vars) + static_cast(mc.get())->add(v, m_norm_subst->find(v)); } } @@ -1141,9 +1135,6 @@ public: }; -tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r) { - if (r == nullptr) - return clean(alloc(solve_eqs_tactic, m, p, mk_expr_simp_replacer(m, p), true)); - else - return clean(alloc(solve_eqs_tactic, m, p, r, false)); +tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(solve_eqs_tactic, m, p, mk_expr_simp_replacer(m, p), true)); } diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h index d986b0dbf..d65a33046 100644 --- a/src/tactic/core/solve_eqs_tactic.h +++ b/src/tactic/core/solve_eqs_tactic.h @@ -21,9 +21,8 @@ Revision History: #include "util/params.h" class ast_manager; class tactic; -class expr_replacer; -tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref(), expr_replacer * r = nullptr); +tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()); /* ADD_TACTIC("solve-eqs", "eliminate variables by solving equations.", "mk_solve_eqs_tactic(m, p)") diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp index 99a69395b..c29a2f3f2 100644 --- a/src/tactic/core/split_clause_tactic.cpp +++ b/src/tactic/core/split_clause_tactic.cpp @@ -18,6 +18,7 @@ Notes: --*/ #include "tactic/tactical.h" +#include "tactic/goal_proof_converter.h" #include "tactic/core/split_clause_tactic.h" class split_clause_tactic : public tactic { diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index 9aa4c9448..e94e83679 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -25,6 +25,7 @@ Notes: #include "ast/rewriter/expr_replacer.h" #include "ast/rewriter/rewriter_def.h" #include "ast/ast_pp.h" +#include "ast/ast_util.h" class symmetry_reduce_tactic : public tactic { class imp; @@ -608,12 +609,12 @@ private: return (j == A.size())?0:A[j]; } - app* mk_member(app* t, term_set const& C) { + expr* mk_member(app* t, term_set const& C) { expr_ref_vector eqs(m()); for (unsigned i = 0; i < C.size(); ++i) { eqs.push_back(m().mk_eq(t, C[i])); } - return m().mk_or(eqs.size(), eqs.data()); + return mk_or(m(), eqs.size(), eqs.data()); } }; diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index eec05b604..e4476548a 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -52,7 +52,7 @@ Notes: #include "ast/ast_pp.h" #include "tactic/tactical.h" #include "tactic/goal_shared_occs.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/rewriter/bool_rewriter.h" #include "tactic/core/simplify_tactic.h" diff --git a/src/tactic/dependency_converter.h b/src/tactic/dependency_converter.h index 474767a98..1d86f8c39 100644 --- a/src/tactic/dependency_converter.h +++ b/src/tactic/dependency_converter.h @@ -22,7 +22,7 @@ Notes: #include "util/ref.h" #include "ast/ast_pp_util.h" #include "model/model.h" -#include "tactic/converter.h" +#include "ast/converters/converter.h" class goal; diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h new file mode 100644 index 000000000..ae3635c77 --- /dev/null +++ b/src/tactic/dependent_expr_state_tactic.h @@ -0,0 +1,103 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + dependent_expr_state_tactic.h + +Abstract: + + The dependent_expr_state_tactic creates a tactic from a dependent_expr_simplifier. + It relies on a factory for building simplifiers. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ +#include "tactic/tactic.h" +#include "ast/simplifiers/dependent_expr_state.h" + +class dependent_expr_state_tactic : public tactic, public dependent_expr_state { + ast_manager& m; + params_ref m_params; + std::string m_name; + ref m_factory; + scoped_ptr m_simp; + goal_ref m_goal; + dependent_expr m_dep; + + void init() { + if (!m_simp) + m_simp = m_factory->mk(m, m_params, *this); + } + +public: + + dependent_expr_state_tactic(ast_manager& m, params_ref const& p, dependent_expr_simplifier_factory* f, char const* name): + m(m), + m_params(p), + m_name(name), + m_factory(f), + m_simp(f->mk(m, p, *this)), + m_dep(m, m.mk_true(), nullptr) + {} + + /** + * size(), [](), update() and inconsisent() implement the abstract interface of dependent_expr_state + */ + unsigned size() const override { return m_goal->size(); } + + dependent_expr const& operator[](unsigned i) override { + m_dep = dependent_expr(m, m_goal->form(i), m_goal->dep(i)); + return m_dep; + } + void update(unsigned i, dependent_expr const& j) override { + auto [f, d] = j(); + m_goal->update(i, f, nullptr, d); + } + + bool inconsistent() override { + return m_goal->inconsistent(); + } + + char const* name() const override { return m_name.c_str(); } + + void updt_params(params_ref const & p) override { + m_params.append(p); + init(); + m_simp->updt_params(m_params); + } + + tactic * translate(ast_manager & m) override { + return alloc(dependent_expr_state_tactic, m, m_params, m_factory.get(), name()); + } + + void operator()(goal_ref const & in, + goal_ref_buffer & result) override { + if (in->proofs_enabled()) + throw tactic_exception("tactic does not support low level proofs"); + init(); + tactic_report report(name(), *in); + m_goal = in.get(); + m_simp->reduce(); + m_goal->inc_depth(); + if (in->models_enabled()) + in->set(m_simp->get_model_converter().get()); + result.push_back(in.get()); + } + + void cleanup() override { + } + + void collect_statistics(statistics & st) const override { + if (m_simp) + m_simp->collect_statistics(st); + } + + void reset_statistics() override { + if (m_simp) + m_simp->reset_statistics(); + } +}; + diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp index ed10f7efb..7b7ca630e 100644 --- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp +++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp @@ -20,7 +20,7 @@ Notes: #include "solver/solver_na2as.h" #include "tactic/tactic.h" #include "ast/rewriter/pb2bv_rewriter.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/ast_pp.h" #include "model/model_smt2_pp.h" #include "tactic/arith/bound_manager.h" diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index 5e05fdf31..7ec5243e7 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -26,7 +26,7 @@ Notes: #include "ast/rewriter/enum2bv_rewriter.h" #include "model/model_smt2_pp.h" #include "tactic/tactic.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "tactic/fd_solver/enum2bv_solver.h" #include "solver/solver_na2as.h" diff --git a/src/tactic/fd_solver/pb2bv_solver.cpp b/src/tactic/fd_solver/pb2bv_solver.cpp index 609ed173d..1a5f7d16a 100644 --- a/src/tactic/fd_solver/pb2bv_solver.cpp +++ b/src/tactic/fd_solver/pb2bv_solver.cpp @@ -22,7 +22,7 @@ Notes: #include "ast/rewriter/th_rewriter.h" #include "model/model_smt2_pp.h" #include "tactic/tactic.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "solver/solver_na2as.h" #include "tactic/fd_solver/pb2bv_solver.h" diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 452a629c4..4debe781a 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -19,7 +19,7 @@ Notes: #pragma once #include "ast/fpa/fpa2bv_converter.h" -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "ast/fpa/bv2fpa_converter.h" class fpa2bv_model_converter : public model_converter { diff --git a/src/tactic/goal.h b/src/tactic/goal.h index 5e7e0b2fe..b0b8d95f1 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -34,8 +34,8 @@ Revision History: #include "util/ref.h" #include "util/ref_vector.h" #include "util/ref_buffer.h" -#include "tactic/model_converter.h" -#include "tactic/proof_converter.h" +#include "ast/converters/model_converter.h" +#include "ast/converters/proof_converter.h" #include "tactic/dependency_converter.h" class goal { diff --git a/src/tactic/goal_proof_converter.h b/src/tactic/goal_proof_converter.h new file mode 100644 index 000000000..a17ff0ea1 --- /dev/null +++ b/src/tactic/goal_proof_converter.h @@ -0,0 +1,63 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + goal_proof_converter.h + +Abstract: + + Proof converter for goals + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-23 + +--*/ + +#pragma once + +#include "ast/converters/proof_converter.h" +class goal; + +/** + \brief create a proof converter that takes a set of subgoals and converts their proofs to a proof of + the goal they were derived from. + */ +proof_converter * concat(proof_converter *pc1, unsigned n, goal* const* goals); + +class subgoal_proof_converter : public proof_converter { + proof_converter_ref m_pc; + goal_ref_buffer m_goals; +public: + subgoal_proof_converter(proof_converter* pc, unsigned n, goal * const* goals): + m_pc(pc) + { + for (unsigned i = 0; i < n; ++i) m_goals.push_back(goals[i]); + } + + proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { + // ignore the proofs from the arguments, instead obtain the proofs fromt he subgoals. + SASSERT(num_source == 0); + proof_converter_ref_buffer pc_buffer; + for (goal_ref g : m_goals) { + pc_buffer.push_back(g->pc()); + + } + return apply(m, m_pc, pc_buffer); + } + + proof_converter* translate(ast_translation& tr) override { + proof_converter_ref pc1 = m_pc->translate(tr); + goal_ref_buffer goals; + for (goal_ref g : m_goals) goals.push_back(g->translate(tr)); + return alloc(subgoal_proof_converter, pc1.get(), goals.size(), goals.data()); + } + + void display(std::ostream& out) override {} + +}; + +inline proof_converter * concat(proof_converter *pc, unsigned n, goal* const* goals) { + return alloc(subgoal_proof_converter, pc, n, goals); +} diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 483be4cca..b521095be 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -44,7 +44,7 @@ Notes: #include "solver/solver2tactic.h" #include "solver/parallel_tactic.h" #include "solver/parallel_params.hpp" -#include "tactic/tactic_params.hpp" +#include "params/tactic_params.hpp" #include "parsers/smt2/smt2parser.h" diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index bf726beb9..5f290c626 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -20,7 +20,7 @@ Notes: #include "util/stopwatch.h" #include "util/lbool.h" -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "tactic/goal.h" #include "tactic/sls/sls_tracker.h" diff --git a/src/tactic/smtlogics/qfufbv_ackr_model_converter.h b/src/tactic/smtlogics/qfufbv_ackr_model_converter.h index 092e41634..c60902228 100644 --- a/src/tactic/smtlogics/qfufbv_ackr_model_converter.h +++ b/src/tactic/smtlogics/qfufbv_ackr_model_converter.h @@ -16,7 +16,7 @@ --*/ #pragma once -#include "tactic/model_converter.h" +#include "ast/converters/model_converter.h" #include "ackermannization/ackr_info.h" model_converter * mk_qfufbv_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 0d1062d78..5b1ea9587 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -20,6 +20,7 @@ Notes: #include "util/cancel_eh.h" #include "util/scoped_ptr_vector.h" #include "tactic/tactical.h" +#include "tactic/goal_proof_converter.h" #ifndef SINGLE_THREAD #include #endif diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 2358abcd1..3f45feb37 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -20,7 +20,7 @@ Notes: #include "ast/recfun_decl_plugin.h" #include "ast/macros/macro_manager.h" #include "ast/macros/macro_finder.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "tactic/ufbv/macro_finder_tactic.h" class macro_finder_tactic : public tactic { diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index b0eb113b8..051ee4fed 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "tactic/tactical.h" -#include "tactic/generic_model_converter.h" +#include "ast/converters/generic_model_converter.h" #include "ast/macros/macro_manager.h" #include "ast/macros/macro_finder.h" #include "ast/macros/quasi_macros.h" diff --git a/src/test/horn_subsume_model_converter.cpp b/src/test/horn_subsume_model_converter.cpp index aea819d7a..95b14ea31 100644 --- a/src/test/horn_subsume_model_converter.cpp +++ b/src/test/horn_subsume_model_converter.cpp @@ -5,7 +5,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#include "tactic/horn_subsume_model_converter.h" +#include "ast/converters/horn_subsume_model_converter.h" #include "ast/arith_decl_plugin.h" #include "model/model_smt2_pp.h" #include "ast/reg_decl_plugins.h" diff --git a/src/util/sat_literal.h b/src/util/sat_literal.h index aeb23bddd..da36c1270 100644 --- a/src/util/sat_literal.h +++ b/src/util/sat_literal.h @@ -72,7 +72,7 @@ namespace sat { } friend literal operator~(literal l) { - l.m_val = l.m_val ^1; + l.m_val = l.m_val ^ 1; return l; } diff --git a/src/util/util.h b/src/util/util.h index f08558f37..ffd94629c 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -103,6 +103,7 @@ unsigned uint64_log2(uint64_t v); static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits"); // Return the number of 1 bits in v. +// see e.g. http://en.wikipedia.org/wiki/Hamming_weight static inline unsigned get_num_1bits(unsigned v) { #ifdef __GNUC__ return __builtin_popcount(v); @@ -122,6 +123,26 @@ static inline unsigned get_num_1bits(unsigned v) { #endif } +static inline unsigned get_num_1bits(uint64_t v) { +#ifdef __GNUC__ + return __builtin_popcountll(v); +#else +#ifdef Z3DEBUG + unsigned c; + uint64_t v1 = v; + for (c = 0; v1; c++) { + v1 &= v1 - 1; + } +#endif + v = v - (v >> 1) & 0x5555555555555555; + v = (v & 0x3333333333333333) + ((v >> 2) & 0x3333333333333333); + v = (v + (v >> 4)) & 0x0F0F0F0F0F0F0F0F; + uint64_t r = (v * 0x0101010101010101) >> 56; + SASSERT(c == r); + return (unsigned)r; +#endif +} + // Remark: on gcc, the operators << and >> do not produce zero when the second argument >= 64. // So, I'm using the following two definitions to fix the problem static inline uint64_t shift_right(uint64_t x, uint64_t y) { diff --git a/src/util/visit_helper.h b/src/util/visit_helper.h new file mode 100644 index 000000000..418e2715c --- /dev/null +++ b/src/util/visit_helper.h @@ -0,0 +1,49 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + visit_helper.h + +Abstract: + + Routine for marking and counting visited occurrences + +Author: + + Clemens Eisenhofer 2022-11-03 + +--*/ +#pragma once + + +class visit_helper { + + unsigned_vector m_visited; + unsigned m_visited_begin = 0; + unsigned m_visited_end = 0; + +public: + + void init_visited(unsigned n, unsigned lim = 1) { + SASSERT(lim > 0); + if (m_visited_end >= m_visited_end + lim) { // overflow + m_visited_begin = 0; + m_visited_end = lim; + m_visited.reset(); + } + else { + m_visited_begin = m_visited_end; + m_visited_end = m_visited_end + lim; + } + while (m_visited.size() < n) + m_visited.push_back(0); + } + + void mark_visited(unsigned v) { m_visited[v] = m_visited_begin + 1; } + void inc_visited(unsigned v) { + m_visited[v] = std::min(m_visited_end, std::max(m_visited_begin, m_visited[v]) + 1); + } + bool is_visited(unsigned v) const { return m_visited[v] > m_visited_begin; } + unsigned num_visited(unsigned v) const { return std::max(m_visited_begin, m_visited[v]) - m_visited_begin; } +}; \ No newline at end of file