From 002d166f7215fe7e4f611d030d952bc8b90ddd7e Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Thu, 10 Nov 2022 18:05:17 +0100 Subject: [PATCH] Xor (#6448) * Added function to select the next variable to split on * Fixed typo * Small fixes * uint -> int * Fixed missing assignment for binary clauses * Memory leak in .NET user-propagator The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically * Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation * Update (not compiling yet) * #6429 * remove ternary clause optimization Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured. * Update: Missing data-structures (still not compiling) * Nearly compiling * Some missing arguments * Polishing * Only conflicts/propagations/justifications are missing for making it compile * Added propagation (justifications for them are still missing) * Use the right deallocation * Use Z3's memory allocation system * Ported "seen" * Polishing * Added 64-bit "1" counting * More polishing * minor fixes - ensure mk_extract performs simplification to distribute over extract and removing extract if the range is the entire bit-vector - ensure bool_rewriter simplifeis disjunctions when applicable. * adding simplifiers layer simplifiers layer is a common substrate for global non-incremental and incremental processing. The first two layers are new, but others are to be ported form tactics. - bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values. - euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization. The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized. * Create bv_slice_tactic.cpp missing file * adding virtual destructor Signed-off-by: Nikolaj Bjorner * Added 64-bit "1" counting (#6434) * Memory leak in .NET user-propagator The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically * Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation * Added 64-bit "1" counting * remove incorrect assertion Signed-off-by: Nikolaj Bjorner * Added limit to "visit" to allow detecting multiple visits (#6435) * Memory leak in .NET user-propagator The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically * Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation * Added limit to "visit" to allow detecting multiple visits * Putting visit in a separate class (Reason: We will probably need two of them in the sat::solver) * Bugfix * init solve_eqs * working on solve_eqs * Update .gitignore * wip - converting the equation solver as a simplifier * make visited_helper independent of literals re-introduce shorthands in sat::solver for visited and have them convert literals to unsigned. * build fix * move model and proof converters to self-contained module * Create solve_eqs2_tactic.h * add converters module to python build * move tactic_params to params * move more converters * move horn_subsume_model_converter to ast/converters * add initial stubs for model reconstruction trail * fixing build Signed-off-by: Nikolaj Bjorner * fixes #6439 #6436 * It's compiling (However, two important functions are commented out) Signed-off-by: Nikolaj Bjorner Co-authored-by: Nikolaj Bjorner --- .gitignore | 1 + scripts/mk_project.py | 6 +- src/CMakeLists.txt | 4 +- .../ackermannize_bv_model_converter.h | 2 +- src/ackermannization/ackr_model_converter.h | 2 +- .../lackr_model_converter_lazy.h | 2 +- src/api/api_ast.cpp | 8 +- src/ast/arith_decl_plugin.h | 3 + src/ast/ast.h | 1 + src/ast/converters/CMakeLists.txt | 11 + src/{tactic => ast/converters}/converter.h | 0 .../converters}/equiv_proof_converter.cpp | 2 +- .../converters}/equiv_proof_converter.h | 2 +- .../converters}/generic_model_converter.cpp | 2 +- .../converters}/generic_model_converter.h | 2 +- .../horn_subsume_model_converter.cpp | 10 +- .../horn_subsume_model_converter.h | 2 +- .../converters}/model_converter.cpp | 2 +- .../converters}/model_converter.h | 2 +- .../converters}/proof_converter.cpp | 38 +- .../converters}/proof_converter.h | 9 +- .../converters}/replace_proof_converter.cpp | 2 +- .../converters}/replace_proof_converter.h | 2 +- src/ast/euf/euf_egraph.cpp | 4 + src/ast/euf/euf_etable.cpp | 2 - src/ast/expr_substitution.h | 1 + src/ast/justified_expr.h | 11 +- src/ast/recfun_decl_plugin.h | 3 +- src/ast/rewriter/bool_rewriter.cpp | 2 +- src/ast/rewriter/mk_extract_proc.cpp | 7 + src/ast/rewriter/th_rewriter.h | 1 + src/ast/simplifiers/CMakeLists.txt | 11 + src/ast/simplifiers/bv_slice.cpp | 207 +++ src/ast/simplifiers/bv_slice.h | 55 + src/ast/simplifiers/dependent_expr.h | 75 ++ src/ast/simplifiers/dependent_expr_state.h | 90 ++ src/ast/simplifiers/euf_completion.cpp | 328 +++++ src/ast/simplifiers/euf_completion.h | 63 + src/ast/simplifiers/extract_eqs.cpp | 257 ++++ src/ast/simplifiers/extract_eqs.h | 48 + .../model_reconstruction_trail.cpp | 44 + .../simplifiers/model_reconstruction_trail.h | 80 ++ src/ast/simplifiers/solve_eqs.cpp | 215 ++++ src/ast/simplifiers/solve_eqs.h | 84 ++ src/cmd_context/cmd_context.cpp | 2 +- src/cmd_context/cmd_context.h | 2 +- src/math/simplex/model_based_opt.cpp | 2 +- src/muz/base/dl_context.cpp | 6 + src/muz/base/dl_context.h | 2 +- src/muz/base/dl_rule.cpp | 2 +- src/muz/base/dl_rule.h | 4 +- src/muz/base/dl_util.h | 5 +- src/muz/base/hnf.h | 2 +- src/muz/fp/horn_tactic.cpp | 6 +- src/muz/spacer/spacer_manager.cpp | 2 +- src/muz/transforms/dl_mk_array_blast.h | 2 +- src/muz/transforms/dl_mk_bit_blast.cpp | 2 +- src/muz/transforms/dl_mk_coi_filter.cpp | 2 +- src/muz/transforms/dl_mk_elim_term_ite.h | 2 +- .../transforms/dl_mk_subsumption_checker.cpp | 2 +- src/nlsat/tactic/goal2nlsat.h | 2 +- src/opt/opt_context.cpp | 2 +- src/opt/opt_context.h | 2 +- src/opt/opt_solver.h | 2 +- src/opt/sortmax.cpp | 2 +- src/params/CMakeLists.txt | 1 + src/{tactic => params}/tactic_params.pyg | 0 src/qe/mbp/mbp_arith.cpp | 38 +- src/qe/qsat.h | 2 +- src/sat/sat_cleaner.cpp | 3 - src/sat/sat_config.cpp | 1 + src/sat/sat_config.h | 6 + src/sat/sat_drat.cpp | 4 - src/sat/sat_gc.cpp | 24 - src/sat/sat_integrity_checker.cpp | 26 - src/sat/sat_justification.h | 21 +- src/sat/sat_lut_finder.cpp | 4 +- src/sat/sat_params.pyg | 10 +- src/sat/sat_proof_trim.cpp | 17 - src/sat/sat_simplifier.cpp | 3 - src/sat/sat_solver.cpp | 217 +--- src/sat/sat_solver.h | 28 +- src/sat/sat_types.h | 2 - src/sat/sat_watched.cpp | 33 - src/sat/sat_watched.h | 38 +- src/sat/sat_xor_finder.cpp | 5 +- src/sat/smt/CMakeLists.txt | 1 + src/sat/smt/euf_solver.h | 2 +- src/sat/smt/pb_solver.cpp | 28 - src/sat/smt/xor_gaussian.cpp | 1135 +++++++++++++++++ src/sat/smt/xor_gaussian.h | 706 ++++++++++ src/sat/smt/xor_matrix_finder.cpp | 103 +- src/sat/smt/xor_matrix_finder.h | 14 +- src/sat/smt/xor_solver.cpp | 683 +++++++++- src/sat/smt/xor_solver.h | 229 ++-- src/sat/tactic/goal2sat.cpp | 2 +- src/sat/tactic/sat2goal.cpp | 2 +- src/sat/tactic/sat2goal.h | 2 +- src/smt/smt_context_pp.cpp | 2 +- src/smt/tactic/smt_tactic_core.cpp | 2 +- src/smt/theory_arith_aux.h | 2 +- src/smt/theory_lra.cpp | 2 +- src/smt/theory_wmaxsat.h | 2 +- src/solver/check_sat_result.h | 2 +- src/solver/solver.cpp | 2 +- src/solver/solver2tactic.cpp | 2 +- src/solver/solver2tactic.h | 2 +- src/tactic/CMakeLists.txt | 10 +- src/tactic/arith/card2bv_tactic.cpp | 2 +- src/tactic/arith/degree_shift_tactic.cpp | 2 +- src/tactic/arith/fix_dl_var_tactic.cpp | 2 +- src/tactic/arith/lia2card_tactic.cpp | 2 +- src/tactic/arith/lia2pb_tactic.cpp | 2 +- src/tactic/arith/nla2bv_tactic.cpp | 2 +- src/tactic/arith/normalize_bounds_tactic.cpp | 2 +- src/tactic/arith/pb2bv_model_converter.h | 2 +- src/tactic/arith/pb2bv_tactic.cpp | 2 +- src/tactic/arith/purify_arith_tactic.cpp | 2 +- src/tactic/arith/recover_01_tactic.cpp | 2 +- src/tactic/bv/CMakeLists.txt | 2 + src/tactic/bv/bit_blaster_model_converter.cpp | 2 +- src/tactic/bv/bit_blaster_model_converter.h | 2 +- src/tactic/bv/bv_size_reduction_tactic.cpp | 2 +- src/tactic/bv/bv_slice_tactic.cpp | 33 + src/tactic/bv/bv_slice_tactic.h | 29 + src/tactic/bv/bvarray2uf_rewriter.h | 2 +- src/tactic/bv/bvarray2uf_tactic.cpp | 2 +- src/tactic/bv/dt2bv_tactic.cpp | 2 +- src/tactic/bv/elim_small_bv_tactic.cpp | 2 +- src/tactic/core/CMakeLists.txt | 2 + src/tactic/core/blast_term_ite_tactic.cpp | 2 +- src/tactic/core/elim_term_ite_tactic.cpp | 2 +- src/tactic/core/elim_uncnstr_tactic.cpp | 2 +- src/tactic/core/euf_completion_tactic.cpp | 32 + src/tactic/core/euf_completion_tactic.h | 29 + src/tactic/core/nnf_tactic.cpp | 2 +- src/tactic/core/occf_tactic.cpp | 2 +- src/tactic/core/pb_preprocess_tactic.cpp | 2 +- src/tactic/core/propagate_values_tactic.cpp | 2 +- src/tactic/core/reduce_args_tactic.cpp | 2 +- src/tactic/core/reduce_invertible_tactic.cpp | 2 +- src/tactic/core/solve_eqs2_tactic.h | 41 + src/tactic/core/solve_eqs_tactic.cpp | 21 +- src/tactic/core/solve_eqs_tactic.h | 3 +- src/tactic/core/split_clause_tactic.cpp | 1 + src/tactic/core/symmetry_reduce_tactic.cpp | 5 +- src/tactic/core/tseitin_cnf_tactic.cpp | 2 +- src/tactic/dependency_converter.h | 2 +- src/tactic/dependent_expr_state_tactic.h | 103 ++ .../fd_solver/bounded_int2bv_solver.cpp | 2 +- src/tactic/fd_solver/enum2bv_solver.cpp | 2 +- src/tactic/fd_solver/pb2bv_solver.cpp | 2 +- src/tactic/fpa/fpa2bv_model_converter.h | 2 +- src/tactic/goal.h | 4 +- src/tactic/goal_proof_converter.h | 63 + src/tactic/portfolio/smt_strategic_solver.cpp | 2 +- src/tactic/sls/sls_engine.h | 2 +- .../smtlogics/qfufbv_ackr_model_converter.h | 2 +- src/tactic/tactical.cpp | 1 + src/tactic/ufbv/macro_finder_tactic.cpp | 2 +- src/tactic/ufbv/quasi_macros_tactic.cpp | 2 +- src/test/horn_subsume_model_converter.cpp | 2 +- src/util/sat_literal.h | 2 +- src/util/util.h | 21 + src/util/visit_helper.h | 49 + 165 files changed, 4849 insertions(+), 846 deletions(-) create mode 100644 src/ast/converters/CMakeLists.txt rename src/{tactic => ast/converters}/converter.h (100%) rename src/{tactic => ast/converters}/equiv_proof_converter.cpp (93%) rename src/{tactic => ast/converters}/equiv_proof_converter.h (95%) rename src/{tactic => ast/converters}/generic_model_converter.cpp (99%) rename src/{tactic => ast/converters}/generic_model_converter.h (97%) rename src/{tactic => ast/converters}/horn_subsume_model_converter.cpp (99%) rename src/{tactic => ast/converters}/horn_subsume_model_converter.h (97%) rename src/{tactic => ast/converters}/model_converter.cpp (99%) rename src/{tactic => ast/converters}/model_converter.h (98%) rename src/{tactic => ast/converters}/proof_converter.cpp (68%) rename src/{tactic => ast/converters}/proof_converter.h (78%) rename src/{tactic => ast/converters}/replace_proof_converter.cpp (97%) rename src/{tactic => ast/converters}/replace_proof_converter.h (95%) create mode 100644 src/ast/simplifiers/CMakeLists.txt create mode 100644 src/ast/simplifiers/bv_slice.cpp create mode 100644 src/ast/simplifiers/bv_slice.h create mode 100644 src/ast/simplifiers/dependent_expr.h create mode 100644 src/ast/simplifiers/dependent_expr_state.h create mode 100644 src/ast/simplifiers/euf_completion.cpp create mode 100644 src/ast/simplifiers/euf_completion.h create mode 100644 src/ast/simplifiers/extract_eqs.cpp create mode 100644 src/ast/simplifiers/extract_eqs.h create mode 100644 src/ast/simplifiers/model_reconstruction_trail.cpp create mode 100644 src/ast/simplifiers/model_reconstruction_trail.h create mode 100644 src/ast/simplifiers/solve_eqs.cpp create mode 100644 src/ast/simplifiers/solve_eqs.h rename src/{tactic => params}/tactic_params.pyg (100%) create mode 100644 src/sat/smt/xor_gaussian.cpp create mode 100644 src/sat/smt/xor_gaussian.h create mode 100644 src/tactic/bv/bv_slice_tactic.cpp create mode 100644 src/tactic/bv/bv_slice_tactic.h create mode 100644 src/tactic/core/euf_completion_tactic.cpp create mode 100644 src/tactic/core/euf_completion_tactic.h create mode 100644 src/tactic/core/solve_eqs2_tactic.h create mode 100644 src/tactic/dependent_expr_state_tactic.h create mode 100644 src/tactic/goal_proof_converter.h create mode 100644 src/util/visit_helper.h 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