diff --git a/scripts/mk_project.py b/scripts/mk_project.py index e9f54be05..497aa350f 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -20,26 +20,27 @@ def init_project_def(): add_lib('simplex', ['util'], 'math/simplex') add_lib('hilbert', ['util'], 'math/hilbert') add_lib('automata', ['util'], 'math/automata') + add_lib('params', ['util']) + add_lib('smt_params', ['params'], 'smt/params') add_lib('realclosure', ['interval'], 'math/realclosure') add_lib('subpaving', ['interval'], 'math/subpaving') add_lib('ast', ['util', 'polynomial']) - add_lib('euf', ['ast', 'util'], 'ast/euf') - add_lib('params', ['util']) - add_lib('smt_params', ['params'], 'smt/params') + add_lib('parser_util', ['ast'], 'parsers/util') + add_lib('euf', ['ast'], 'ast/euf') add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner') add_lib('sat', ['params', 'util', 'dd', 'grobner']) add_lib('nlsat', ['polynomial', 'sat']) 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('model', ['rewriter', 'macros']) - add_lib('converters', ['model'], 'ast/converters') - add_lib('simplifiers', ['euf', 'rewriter', 'converters'], 'ast/simplifiers') + add_lib('bit_blaster', ['rewriter'], 'ast/rewriter/bit_blaster') 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') + add_lib('substitution', ['rewriter'], 'ast/substitution') + add_lib('proofs', ['rewriter'], 'ast/proofs') + add_lib('macros', ['rewriter'], 'ast/macros') + add_lib('model', ['macros']) + add_lib('converters', ['model'], 'ast/converters') + add_lib('simplifiers', ['euf', 'rewriter', 'bit_blaster', 'converters'], 'ast/simplifiers') + add_lib('tactic', ['simplifiers']) add_lib('solver', ['params', 'model', 'tactic', 'proofs']) add_lib('cmd_context', ['solver', 'rewriter', 'params']) add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2') @@ -47,7 +48,6 @@ def init_project_def(): add_lib('aig_tactic', ['tactic'], 'tactic/aig') add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization') add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa') - add_lib('bit_blaster', ['rewriter', 'params'], 'ast/rewriter/bit_blaster') add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core') add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith') add_lib('mbp', ['model', 'simplex'], 'qe/mbp') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index fd4fa04b5..dadd70bba 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -46,6 +46,7 @@ add_subdirectory(math/subpaving) add_subdirectory(ast) add_subdirectory(params) add_subdirectory(ast/rewriter) +add_subdirectory(ast/rewriter/bit_blaster) add_subdirectory(ast/normal_forms) add_subdirectory(ast/macros) add_subdirectory(model) @@ -71,7 +72,6 @@ add_subdirectory(qe/mbp) add_subdirectory(qe/lite) add_subdirectory(solver/assertions) add_subdirectory(ast/pattern) -add_subdirectory(ast/rewriter/bit_blaster) add_subdirectory(math/lp) add_subdirectory(sat/smt) add_subdirectory(sat/tactic) diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index 042c29a0e..c488a6269 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -15,4 +15,5 @@ z3_add_component(simplifiers COMPONENT_DEPENDENCIES euf rewriter + bit_blaster ) diff --git a/src/ast/simplifiers/card2bv.cpp b/src/ast/simplifiers/card2bv.cpp index 145ea71f5..2da9b6e44 100644 --- a/src/ast/simplifiers/card2bv.cpp +++ b/src/ast/simplifiers/card2bv.cpp @@ -49,7 +49,7 @@ void card2bv::reduce() { for (func_decl* f : fns) m_fmls.model_trail().hide(f); - advance_qhead(m_fmls.size()); + advance_qhead(m_fmls.size()); } void card2bv::collect_statistics(statistics& st) const { diff --git a/src/ast/simplifiers/rewriter_simplifier.h b/src/ast/simplifiers/rewriter_simplifier.h new file mode 100644 index 000000000..938e30b83 --- /dev/null +++ b/src/ast/simplifiers/rewriter_simplifier.h @@ -0,0 +1,53 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + rewriter_simplifier.h + +Abstract: + + rewriter simplifier + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-24 + +--*/ + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/rewriter/th_rewriter.h" + + +class rewriter_simplifier : public dependent_expr_simplifier { + + unsigned m_num_steps = 0; + params_ref m_params; + +public: + rewriter_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls): + dependent_expr_simplifier(m, fmls) { + updt_params(p); + } + + void reduce() override { + m_num_steps = 0; + expr_ref new_curr(m); + proof_ref new_pr(m); + for (unsigned idx = m_qhead; idx < m_fmls.size(); idx++) { + if (m_fmls.inconsistent()) + break; + auto [f, d] = m_fmls[i](); + m_rewriter(f, new_curr, new_pr); + m_num_steps += m_rewriter.get_num_steps(); + m_fmls.update(idx, dependent_expr(m, new_curr, d)); + } + advance_qhead(m_fmls.size()); + } + void collect_statistics(statistics& st) const override { st.update("simplifier", m_num_steps); } + void reset_statistics() override { m_stats.reset(); } + void updt_params(params_ref const& p) override { m_params.append(p); m_rewriter.updt_params(m_params); } + void collect_param_descrs(param_descrs& r) override { th_rewriter::get_param_descrs(r); } +}; diff --git a/src/ast/simplifiers/seq_simplifier.h b/src/ast/simplifiers/seq_simplifier.h new file mode 100644 index 000000000..5a3a7da60 --- /dev/null +++ b/src/ast/simplifiers/seq_simplifier.h @@ -0,0 +1,72 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + seq_simplifier.h + +Abstract: + + create a simplifier from a sequence of simplifiers + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-24 + +--*/ + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" + + +class seq_simplifier : public dependent_expr_simplifier { + scoped_ptr_vector m_simplifiers; + +public: + seq_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls): + dependent_expr_simplifier(m, fmls) { + } + + void add_simplifier(dependent_expr_simplifier* s) { + m_simplifiers.push_back(s); + } + + void reduce() override { + for (auto* s : m_simplifiers) { + if (m_fmls.inconsistent()) + break; + s->reduce(); + } + } + + void collect_statistics(statistics& st) const override { + for (auto* s : m_simplifiers) + s->collect_statistics(st); + } + + void reset_statistics() override { + for (auto* s : m_simplifiers) + s->reset_statistics(st); + } + + void updt_params(params_ref const& p) override { + for (auto* s : m_simplifiers) + s->updt_params(p); + } + + void collect_param_descrs(param_descrs& r) override { + for (auto* s : m_simplifiers) + s->collect_param_descrs(r); + } + + void push() override { + for (auto* s : m_simplifiers) + s->push(); + } + + void pop(unsigned n) override { + for (auto* s : m_simplifiers) + s->pop(n); + } +};