mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 09:04:07 +00:00
Code Activity

create simplifier_solver wrapper to supply simplifier layer

Browse source 
move sat_smt_preprocess to solver
fix bugs in model_reconstruction_trail for dependency replay

This is a preparatory step for exposing pre-processing as tactics.
This commit is contained in:
Nikolaj Bjorner 2023-01-30 16:12:25 -08:00
parent 304b316314
commit dd0decfe5d
11 changed files with 474 additions and 248 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
scripts/mk_project.py
View file

@ -41,7 +41,9 @@ def init_project_def():
add_lib('converters', ['model'], 'ast/converters')
add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'converters', 'substitution'], 'ast/simplifiers')
add_lib('tactic', ['simplifiers'])
add_lib('solver', ['params', 'model', 'tactic', 'proofs'])
add_lib('mbp', ['model', 'simplex'], 'qe/mbp')
add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite')
add_lib('solver', ['params', 'smt_params', 'model', 'tactic', 'qe_lite', 'proofs'])
add_lib('cmd_context', ['solver', 'rewriter', 'params'])
add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
@ -50,8 +52,6 @@ def init_project_def():
add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
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')
add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite')
add_lib('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite'], 'solver/assertions')
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')

4
src/CMakeLists.txt
View file

@ -55,6 +55,8 @@ add_subdirectory(ast/converters)
add_subdirectory(ast/substitution)
add_subdirectory(ast/simplifiers)
add_subdirectory(tactic)
add_subdirectory(qe/mbp)
add_subdirectory(qe/lite)
add_subdirectory(smt/params)
add_subdirectory(parsers/util)
add_subdirectory(math/grobner)
@ -68,8 +70,6 @@ add_subdirectory(solver)
add_subdirectory(cmd_context)
add_subdirectory(cmd_context/extra_cmds)
add_subdirectory(parsers/smt2)
add_subdirectory(qe/mbp)
add_subdirectory(qe/lite)
add_subdirectory(solver/assertions)
add_subdirectory(ast/pattern)
add_subdirectory(math/lp)

6
src/ast/simplifiers/model_reconstruction_trail.h
View file

@ -70,7 +70,7 @@ class model_reconstruction_trail {
return true;
if (m_subst) {
for (auto const& [k, v] : m_subst->sub())
if (free_vars.is_marked(k))
if (free_vars.is_marked(to_app(k)->get_decl()))
return true;
}
return false;
@ -88,8 +88,10 @@ class model_reconstruction_trail {
void add_vars(expr* e, ast_mark& free_vars) {
for (expr* t : subterms::all(expr_ref(e, m)))
if (is_app(t))
if (is_app(t) && is_uninterp(t)) {
TRACE("simplifier", tout << "add var " << to_app(t)->get_decl()->get_name() << "\n");
free_vars.mark(to_app(t)->get_decl(), true);
}
}
void add_vars(dependent_expr const& d, ast_mark& free_vars) {

1
src/sat/sat_solver/CMakeLists.txt
View file

@ -1,7 +1,6 @@
z3_add_component(sat_solver
SOURCES
inc_sat_solver.cpp
sat_smt_preprocess.cpp
sat_smt_solver.cpp
COMPONENT_DEPENDENCIES
aig_tactic

106
src/sat/sat_solver/sat_smt_preprocess.cpp
View file

@ -1,106 +0,0 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
sat_smt_preprocess.cpp
Abstract:
SAT pre-process
Author:
Nikolaj Bjorner (nbjorner) 2022-11-28
--*/
#include "ast/rewriter/rewriter_def.h"
#include "ast/simplifiers/bit_blaster.h"
#include "ast/simplifiers/max_bv_sharing.h"
#include "ast/simplifiers/card2bv.h"
#include "ast/simplifiers/propagate_values.h"
#include "ast/simplifiers/rewriter_simplifier.h"
#include "ast/simplifiers/solve_eqs.h"
#include "ast/simplifiers/bv_slice.h"
#include "ast/simplifiers/eliminate_predicates.h"
#include "ast/simplifiers/elim_unconstrained.h"
#include "ast/simplifiers/pull_nested_quantifiers.h"
#include "ast/simplifiers/distribute_forall.h"
#include "ast/simplifiers/refine_inj_axiom.h"
#include "ast/simplifiers/elim_bounds.h"
#include "ast/simplifiers/bit2int.h"
#include "ast/simplifiers/bv_elim.h"
#include "ast/simplifiers/push_ite.h"
#include "ast/simplifiers/elim_term_ite.h"
#include "ast/simplifiers/flatten_clauses.h"
#include "ast/simplifiers/cnf_nnf.h"
#include "sat/sat_params.hpp"
#include "smt/params/smt_params.h"
#include "sat/sat_solver/sat_smt_preprocess.h"
#include "qe/lite/qe_lite.h"
void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) {
sat_params sp(p);
smt_params smtp(p);
if (sp.euf() || sp.smt()) {
s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st));
if (smtp.m_solve_eqs) s.add_simplifier(alloc(euf::solve_eqs, m, st));
if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st));
if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st));
if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st));
if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st));
if (smtp.m_pull_nested_quantifiers) s.add_simplifier(alloc(pull_nested_quantifiers_simplifier, m, p, st));
if (smtp.m_max_bv_sharing) s.add_simplifier(mk_max_bv_sharing(m, p, st));
if (smtp.m_refine_inj_axiom) s.add_simplifier(alloc(refine_inj_axiom_simplifier, m, p, st));
if (smtp.m_bv_size_reduce) s.add_simplifier(alloc(bv::slice, m, st));
if (smtp.m_distribute_forall) s.add_simplifier(alloc(distribute_forall_simplifier, m, p, st));
if (smtp.m_eliminate_bounds) s.add_simplifier(alloc(elim_bounds_simplifier, m, p, st));
if (smtp.m_simplify_bit2int) s.add_simplifier(alloc(bit2int_simplifier, m, p, st));
if (smtp.m_bb_quantifiers) s.add_simplifier(alloc(bv::elim_simplifier, m, p, st));
if (smtp.m_eliminate_term_ite && smtp.m_lift_ite != lift_ite_kind::LI_FULL) s.add_simplifier(alloc(elim_term_ite_simplifier, m, p, st));
if (smtp.m_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(push_ite_simplifier, m, p, st, smtp.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE));
if (smtp.m_ng_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(ng_push_ite_simplifier, m, p, st, smtp.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE));
s.add_simplifier(alloc(flatten_clauses, m, p, st));
//
// add:
// euf_completion?
//
// add: make it externally programmable
//
#if 0
if (!invoke(m_apply_quasi_macros)) return;
#endif
}
else {
params_ref simp1_p = p;
simp1_p.set_bool("som", true);
simp1_p.set_bool("pull_cheap_ite", true);
simp1_p.set_bool("push_ite_bv", false);
simp1_p.set_bool("local_ctx", true);
simp1_p.set_uint("local_ctx_limit", 10000000);
simp1_p.set_bool("flat", true); // required by som
simp1_p.set_bool("hoist_mul", false); // required by som
simp1_p.set_bool("elim_and", true);
simp1_p.set_bool("blast_distinct", true);
simp1_p.set_bool("flat_and_or", false);
params_ref simp2_p = p;
simp2_p.set_bool("flat", false);
simp2_p.set_bool("flat_and_or", false);
s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
s.add_simplifier(alloc(propagate_values, m, p, st));
s.add_simplifier(alloc(card2bv, m, p, st));
s.add_simplifier(alloc(rewriter_simplifier, m, simp1_p, st));
s.add_simplifier(mk_max_bv_sharing(m, p, st));
s.add_simplifier(alloc(bit_blaster_simplifier, m, p, st));
s.add_simplifier(alloc(rewriter_simplifier, m, simp2_p, st));
}
}

173
src/sat/sat_solver/sat_smt_solver.cpp
View file

@ -17,14 +17,10 @@ Author:
Notes:
- add translation for preprocess state.
- If the pre-processors are stateful, they need to be properly translated.
- add back get_consequences, maybe or just have them handled by inc_sat_solver
- could also port the layered solver used by smtfd and used by get_consequences to simplifiers
- port various pre-processing to simplifiers
- qe-lite, fm-elimination, ite-lifting, other from asserted_formulas
--*/
@ -36,7 +32,7 @@ Notes:
#include "model/model_smt2_pp.h"
#include "model/model_evaluator.h"
#include "sat/sat_solver.h"
#include "sat/sat_solver/sat_smt_preprocess.h"
#include "solver/simplifier_solver.h"
#include "sat/sat_params.hpp"
#include "sat/smt/euf_solver.h"
#include "sat/tactic/goal2sat.h"
@ -47,54 +43,6 @@ Notes:
// incremental SAT solver.
class sat_smt_solver : public solver {
struct dep_expr_state : public dependent_expr_state {
sat_smt_solver& s;
model_reconstruction_trail m_reconstruction_trail;
dep_expr_state(sat_smt_solver& s):dependent_expr_state(s.m), s(s), m_reconstruction_trail(s.m, m_trail) {}
~dep_expr_state() override {}
virtual unsigned qtail() const override { return s.m_fmls.size(); }
dependent_expr const& operator[](unsigned i) override { return s.m_fmls[i]; }
void update(unsigned i, dependent_expr const& j) override { SASSERT(j.fml()); s.m_fmls[i] = j; }
void add(dependent_expr const& j) override { s.m_fmls.push_back(j); }
bool inconsistent() override { return s.m_solver.inconsistent(); }
model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; }
std::ostream& display(std::ostream& out) const override {
unsigned i = 0;
for (auto const& d : s.m_fmls) {
if (i > 0 && i == qhead())
out << "---- head ---\n";
out << d << "\n";
++i;
}
m_reconstruction_trail.display(out);
return out;
}
void append(generic_model_converter& mc) { model_trail().append(mc); }
void replay(unsigned qhead, expr_ref_vector& assumptions) { m_reconstruction_trail.replay(qhead, assumptions, *this); }
void flatten_suffix() override {
expr_mark seen;
unsigned j = qhead();
for (unsigned i = qhead(); i < qtail(); ++i) {
expr* f = s.m_fmls[i].fml();
if (seen.is_marked(f))
continue;
seen.mark(f, true);
if (s.m.is_true(f))
continue;
if (s.m.is_and(f)) {
auto* d = s.m_fmls[i].dep();
for (expr* arg : *to_app(f))
s.m_fmls.push_back(dependent_expr(s.m, arg, nullptr, d));
continue;
}
if (i != j)
s.m_fmls[j] = s.m_fmls[i];
++j;
}
s.m_fmls.shrink(j);
}
};
struct dependency2assumptions {
ast_manager& m;
trail_stack& m_trail;
@ -152,15 +100,12 @@ class sat_smt_solver : public solver {
mutable sat::solver m_solver;
params_ref m_params;
vector<dependent_expr> m_fmls;
dep_expr_state m_preprocess_state;
seq_simplifier m_preprocess;
trail_stack& m_trail;
trail_stack m_trail;
dependency2assumptions m_dep;
goal2sat m_goal2sat;
expr_ref_vector m_assumptions, m_core, m_ors, m_aux_fmls, m_internalized_fmls;
unsigned m_qhead = 0;
expr_ref_vector m_assumptions, m_core, m_ors, m_fmls, m_internalized_fmls;
atom2bool_var m_map;
generic_model_converter_ref m_mc;
mutable model_converter_ref m_cached_mc;
mutable ref<sat2goal::mc> m_sat_mc;
std::string m_unknown = "no reason given";
@ -168,20 +113,16 @@ class sat_smt_solver : public solver {
// this allows to access the internal state of the SAT solver and carry on partial results.
bool m_internalized_converted = false; // have internalized formulas been converted back
bool is_internalized() const { return m_preprocess_state.qhead() == m_fmls.size(); }
bool is_internalized() const { return m_qhead == m_fmls.size(); }
public:
sat_smt_solver(ast_manager& m, params_ref const& p):
solver(m),
m_solver(p, m.limit()),
m_preprocess_state(*this),
m_preprocess(m, p, m_preprocess_state),
m_trail(m_preprocess_state.m_trail),
m_dep(m, m_trail),
m_assumptions(m), m_core(m), m_ors(m), m_aux_fmls(m), m_internalized_fmls(m),
m_assumptions(m), m_core(m), m_ors(m), m_fmls(m), m_internalized_fmls(m),
m_map(m) {
updt_params(p);
init_preprocess();
m_solver.set_incremental(true);
}
@ -203,13 +144,10 @@ public:
}
// TODO: copy preprocess state
for (auto const& [k, v] : m_dep.m_dep2orig) result->m_dep.insert(tr(v), tr(k));
for (dependent_expr const& f : m_fmls) result->m_fmls.push_back(dependent_expr(tr, f));
for (expr* f : m_assumptions) result->m_assumptions.push_back(tr(f));
for (auto & kv : m_map) result->m_map.insert(tr(kv.m_key), kv.m_value);
for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
if (m_mc) result->m_mc = dynamic_cast<generic_model_converter*>(m_mc->translate(tr));
result->m_dep.copy(tr, m_dep);
if (m_sat_mc) result->m_sat_mc = dynamic_cast<sat2goal::mc*>(m_sat_mc->translate(tr));
result->m_internalized_converted = m_internalized_converted;
return result;
}
@ -234,8 +172,6 @@ public:
expr_ref_vector assumptions(m);
for (unsigned i = 0; i < sz; ++i)
assumptions.push_back(ensure_literal(_assumptions[i]));
for (expr* a : assumptions)
m_preprocess_state.freeze(a);
TRACE("sat", tout << assumptions << "\n";);
lbool r = internalize_formulas(assumptions);
if (r != l_true)
@ -284,17 +220,15 @@ public:
m_solver.user_push();
m_goal2sat.user_push();
m_map.push();
m_preprocess_state.push();
m_preprocess.push();
m_trail.push_scope();
m_trail.push(restore_vector(m_assumptions));
m_trail.push(restore_vector(m_fmls));
m_trail.push(value_trail(m_qhead));
}
void pop(unsigned n) override {
n = std::min(n, m_trail.get_num_scopes()); // allow sat_smt_solver to take over for another solver.
m_preprocess.pop(n);
m_preprocess_state.pop(n);
m_trail.pop_scope(n);
m_map.pop(n);
m_goal2sat.user_pop(n);
m_solver.user_pop(n);
@ -345,18 +279,32 @@ public:
return a;
expr* new_dep = m.mk_fresh_const("dep", m.mk_bool_sort());
expr* fml = m.mk_iff(new_dep, a);
m_fmls.push_back(dependent_expr(m, fml, nullptr, nullptr));
m_fmls.push_back(fml);
m_dep.insert(a, new_dep);
return new_dep;
}
void assert_expr_core2(expr * t, expr * a) override {
a = ensure_literal(a);
m_fmls.push_back(dependent_expr(m, t, nullptr, m.mk_leaf(a)));
m_ors.reset();
m_ors.push_back(t);
if (m.is_and(a)) {
for (expr* arg : *to_app(a)) {
arg = ensure_literal(arg);
m_ors.push_back(mk_not(m, arg));
m_assumptions.push_back(arg);
}
}
else {
a = ensure_literal(a);
m_assumptions.push_back(a);
m_ors.push_back(mk_not(m, a));
}
flatten_or(m_ors);
m_fmls.push_back(mk_or(m_ors));
}
void assert_expr_core(expr * t) override {
m_fmls.push_back(dependent_expr(m, t, nullptr, nullptr));
m_fmls.push_back(t);
}
ast_manager& get_manager() const override { return m; }
@ -367,7 +315,6 @@ public:
solver::collect_param_descrs(r);
goal2sat::collect_param_descrs(r);
sat::solver::collect_param_descrs(r);
m_preprocess.collect_param_descrs(r);
}
void updt_params(params_ref const & p) override {
@ -377,13 +324,11 @@ public:
m_params.set_sym("pb.solver", sp.pb_solver());
m_solver.updt_params(m_params);
m_solver.set_incremental(true);
m_preprocess.updt_params(m_params);
if (sp.smt())
ensure_euf();
}
void collect_statistics(statistics & st) const override {
m_preprocess.collect_statistics(st);
m_solver.collect_statistics(st);
}
@ -531,7 +476,7 @@ public:
expr * get_assertion(unsigned idx) const override {
if (is_internalized() && m_internalized_converted)
return m_internalized_fmls[idx];
return m_fmls[idx].fml();
return m_fmls.get(idx);
}
unsigned get_num_assumptions() const override {
@ -549,7 +494,7 @@ public:
return m_cached_mc;
if (is_internalized() && m_internalized_converted) {
if (m_sat_mc) m_sat_mc->flush_smc(m_solver, m_map);
m_cached_mc = concat(solver::get_model_converter().get(), m_mc.get(), m_sat_mc.get());
m_cached_mc = concat(solver::get_model_converter().get(), m_sat_mc.get());
TRACE("sat", m_cached_mc->display(tout););
return m_cached_mc;
}
@ -574,10 +519,6 @@ public:
m_internalized_converted = true;
}
void init_preprocess() {
::init_preprocess(m, m_params, m_preprocess, m_preprocess_state);
}
euf::solver* get_euf() {
return dynamic_cast<euf::solver*>(m_solver.get_extension());
}
@ -646,50 +587,20 @@ private:
if (is_internalized() && assumptions.empty())
return l_true;
unsigned qhead = m_preprocess_state.qhead();
TRACE("sat", tout << "qhead " << qhead << "\n");
TRACE("sat", tout << "qhead " << m_qhead << "\n");
m_internalized_converted = false;
m_preprocess_state.replay(qhead, assumptions);
m_preprocess.reduce();
if (!m.inc())
return l_undef;
m_preprocess_state.advance_qhead();
m_mc = alloc(generic_model_converter, m, "sat-model-converter");
m_preprocess_state.append(*m_mc);
m_solver.pop_to_base_level();
m_aux_fmls.reset();
for (; qhead < m_fmls.size(); ++qhead)
add_with_dependency(m_fmls[qhead]);
init_goal2sat();
m_goal2sat(m_aux_fmls.size(), m_aux_fmls.data());
m_goal2sat(m_fmls.size() - m_qhead, m_fmls.data() + m_qhead);
if (!m_sat_mc)
m_sat_mc = alloc(sat2goal::mc, m);
m_sat_mc->flush_smc(m_solver, m_map);
m_qhead = m_fmls.size();
return m.inc() ? l_true : l_undef;
}
ptr_vector<expr> m_deps;
void add_with_dependency(dependent_expr const& de) {
if (!de.dep()) {
m_aux_fmls.push_back(de.fml());
return;
}
m_deps.reset();
m.linearize(de.dep(), m_deps);
m_ors.reset();
m_ors.push_back(de.fml());
flatten_or(m_ors);
for (expr* d : m_deps) {
SASSERT(m.is_bool(d));
SASSERT(is_literal(d));
m_assumptions.push_back(d);
m_ors.push_back(mk_not(m, d));
}
m_aux_fmls.push_back(mk_or(m_ors));
}
void extract_core() {
m_core.reset();
if (m_dep.m_literals.empty())
@ -720,7 +631,7 @@ private:
mdl = nullptr;
if (!m_solver.model_is_current())
return;
if (m_fmls.size() > m_preprocess_state.qhead())
if (m_fmls.size() > m_qhead)
return;
TRACE("sat", m_solver.display_model(tout););
CTRACE("sat", m_sat_mc, m_sat_mc->display(tout););
@ -751,7 +662,6 @@ private:
if (m_sat_mc)
(*m_sat_mc)(mdl);
m_goal2sat.update_model(mdl);
TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););
@ -760,25 +670,24 @@ private:
model_evaluator eval(*mdl);
eval.set_model_completion(true);
bool all_true = true;
for (dependent_expr const& d : m_fmls) {
if (has_quantifiers(d.fml()))
for (expr* f : m_fmls) {
if (has_quantifiers(f))
continue;
expr_ref tmp(m);
eval(d.fml(), tmp);
eval(f, tmp);
if (m.limit().is_canceled())
return;
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(d.fml(), m) << " to " << tmp << "\n";
tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n";
model_smt2_pp(tout, m, *(mdl.get()), 0););
if (m.is_false(tmp)) {
IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(d.fml(), m) << "\n");
IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n");
IF_VERBOSE(0, verbose_stream() << "evaluated to " << tmp << "\n");
all_true = false;
}
}
if (!all_true) {
IF_VERBOSE(0, verbose_stream() << m_params << "\n");
IF_VERBOSE(0, if (m_mc) m_mc->display(verbose_stream() << "mc0\n"));
IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n");
exit(0);
}
@ -786,13 +695,11 @@ private:
IF_VERBOSE(1, verbose_stream() << "solution verified\n");
}
}
TRACE("sat", m_mc->display(tout););
(*m_mc)(mdl);
}
};
solver* mk_sat_smt_solver(ast_manager& m, params_ref const& p) {
return alloc(sat_smt_solver, m, p);
return mk_simplifier_solver(alloc(sat_smt_solver, m, p));
}

4
src/solver/CMakeLists.txt
View file

@ -5,15 +5,19 @@ z3_add_component(solver
combined_solver.cpp
mus.cpp
parallel_tactical.cpp
simplifier_solver.cpp
smt_logics.cpp
solver.cpp
solver_na2as.cpp
solver_pool.cpp
solver_preprocess.cpp
solver2tactic.cpp
tactic2solver.cpp
COMPONENT_DEPENDENCIES
model
tactic
smt_params
qe_lite
PYG_FILES
combined_solver_params.pyg
parallel_params.pyg

317
src/solver/simplifier_solver.cpp Normal file
View file

@ -0,0 +1,317 @@
/*++
Copyright (c) 2023 Microsoft Corporation
Module Name:
simplifier_solver.cpp
Abstract:
Implements a solver with simplifying pre-processing.
Author:
Nikolaj Bjorner (nbjorner) 2023-01-30
Notes:
- add translation for preprocess state.
- If the pre-processors are stateful, they need to be properly translated.
--*/
#include "util/params.h"
#include "ast/ast_util.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/simplifiers/seq_simplifier.h"
#include "solver/solver.h"
#include "solver/simplifier_solver.h"
#include "solver/solver_preprocess.h"
class simplifier_solver : public solver {
struct dep_expr_state : public dependent_expr_state {
simplifier_solver& s;
model_reconstruction_trail m_reconstruction_trail;
dep_expr_state(simplifier_solver& s) :dependent_expr_state(s.m), s(s), m_reconstruction_trail(s.m, m_trail) {}
~dep_expr_state() override {}
virtual unsigned qtail() const override { return s.m_fmls.size(); }
dependent_expr const& operator[](unsigned i) override { return s.m_fmls[i]; }
void update(unsigned i, dependent_expr const& j) override {
SASSERT(j.fml());
check_false(j.fml());
s.m_fmls[i] = j;
}
void add(dependent_expr const& j) override { check_false(j.fml()); s.m_fmls.push_back(j); }
bool inconsistent() override { return s.m_inconsistent; }
model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; }
std::ostream& display(std::ostream& out) const override {
unsigned i = 0;
for (auto const& d : s.m_fmls) {
if (i > 0 && i == qhead())
out << "---- head ---\n";
out << d << "\n";
++i;
}
m_reconstruction_trail.display(out);
return out;
}
void check_false(expr* f) {
if (s.m.is_false(f))
s.set_inconsistent();
}
void append(generic_model_converter& mc) { model_trail().append(mc); }
void replay(unsigned qhead, expr_ref_vector& assumptions) { m_reconstruction_trail.replay(qhead, assumptions, *this); }
void flatten_suffix() override {
expr_mark seen;
unsigned j = qhead();
for (unsigned i = qhead(); i < qtail(); ++i) {
expr* f = s.m_fmls[i].fml();
if (seen.is_marked(f))
continue;
seen.mark(f, true);
if (s.m.is_true(f))
continue;
if (s.m.is_and(f)) {
auto* d = s.m_fmls[i].dep();
for (expr* arg : *to_app(f))
add(dependent_expr(s.m, arg, nullptr, d));
continue;
}
if (i != j)
s.m_fmls[j] = s.m_fmls[i];
++j;
}
s.m_fmls.shrink(j);
}
};
ast_manager& m;
scoped_ptr<solver> s;
vector<dependent_expr> m_fmls;
dep_expr_state m_preprocess_state;
seq_simplifier m_preprocess;
expr_ref_vector m_assumptions;
generic_model_converter_ref m_mc;
bool m_inconsistent = false;
void flush(expr_ref_vector& assumptions) {
unsigned qhead = m_preprocess_state.qhead();
if (qhead < m_fmls.size()) {
for (expr* a : assumptions)
m_preprocess_state.freeze(a);
TRACE("solver", tout << "qhead " << qhead << "\n");
m_preprocess_state.replay(qhead, assumptions);
m_preprocess.reduce();
if (!m.inc())
return;
m_preprocess_state.advance_qhead();
}
m_mc = alloc(generic_model_converter, m, "simplifier-model-converter");
m_cached_mc = nullptr;
m_preprocess_state.append(*m_mc);
for (; qhead < m_fmls.size(); ++qhead)
add_with_dependency(m_fmls[qhead]);
}
ptr_vector<expr> m_deps;
void add_with_dependency(dependent_expr const& de) {
if (!de.dep()) {
s->assert_expr(de.fml());
return;
}
m_deps.reset();
m.linearize(de.dep(), m_deps);
m_assumptions.reset();
for (expr* d : m_deps)
m_assumptions.push_back(d);
s->assert_expr(de.fml(), mk_and(m_assumptions));
}
bool inconsistent() const {
return m_inconsistent;
}
void set_inconsistent() {
if (!m_inconsistent) {
m_preprocess_state.m_trail.push(value_trail(m_inconsistent));
m_inconsistent = true;
}
}
public:
simplifier_solver(solver* s) :
solver(s->get_manager()),
m(s->get_manager()),
s(s),
m_preprocess_state(*this),
m_preprocess(m, s->get_params(), m_preprocess_state),
m_assumptions(m),
m_proof(m)
{
init_preprocess(m, s->get_params(), m_preprocess, m_preprocess_state);
}
void assert_expr_core2(expr* t, expr* a) override {
m_cached_model = nullptr;
m_cached_mc = nullptr;
proof* pr = m.proofs_enabled() ? m.mk_asserted(t) : nullptr;
m_fmls.push_back(dependent_expr(m, t, pr, m.mk_leaf(a)));
}
void assert_expr_core(expr* t) override {
m_cached_model = nullptr;
m_cached_mc = nullptr;
proof* pr = m.proofs_enabled() ? m.mk_asserted(t) : nullptr;
m_fmls.push_back(dependent_expr(m, t, pr, nullptr));
}
void push() override {
expr_ref_vector none(m);
flush(none);
m_preprocess_state.push();
m_preprocess.push();
m_preprocess_state.m_trail.push(restore_vector(m_fmls));
s->push();
}
void pop(unsigned n) override {
s->pop(n);
m_cached_model = nullptr;
m_preprocess.pop(n);
m_preprocess_state.pop(n);
}
lbool check_sat_core(unsigned num_assumptions, expr* const* assumptions) override {
expr_ref_vector _assumptions(m, num_assumptions, assumptions);
flush(_assumptions);
return s->check_sat_core(num_assumptions, assumptions);
}
void collect_statistics(statistics& st) const override {
s->collect_statistics(st);
m_preprocess.collect_statistics(st);
}
model_ref m_cached_model;
void get_model_core(model_ref& m) override {
if (m_cached_model) {
m = m_cached_model;
return;
}
s->get_model(m);
if (m_mc)
(*m_mc)(m);
m_cached_model = m;
}
proof_ref m_proof;
proof* get_proof_core() {
proof* p = s->get_proof();
m_proof = p;
if (p) {
expr_ref tmp(p, m);
expr_safe_replace sub(m);
for (auto const& d : m_fmls) {
if (d.pr())
sub.insert(m.mk_asserted(d.fml()), d.pr());
}
sub(tmp);
SASSERT(is_app(tmp));
m_proof = to_app(tmp);
}
return m_proof;
}
solver* translate(ast_manager& m, params_ref const& p) override {
solver* new_s = s->translate(m, p);
ast_translation tr(get_manager(), m);
simplifier_solver* result = alloc(simplifier_solver, new_s);
for (dependent_expr const& f : m_fmls)
result->m_fmls.push_back(dependent_expr(tr, f));
if (m_mc)
result->m_mc = dynamic_cast<generic_model_converter*>(m_mc->translate(tr));
// copy m_preprocess_state?
return result;
}
void updt_params(params_ref const& p) override {
s->updt_params(p);
m_preprocess.updt_params(p);
}
mutable model_converter_ref m_cached_mc;
model_converter_ref get_model_converter() const override {
if (!m_cached_mc)
m_cached_mc = concat(solver::get_model_converter().get(), m_mc.get(), s->get_model_converter().get());
return m_cached_mc;
}
unsigned get_num_assertions() const override { return s->get_num_assertions(); }
expr* get_assertion(unsigned idx) const override { return s->get_assertion(idx); }
std::string reason_unknown() const override { return s->reason_unknown(); }
void set_reason_unknown(char const* msg) override { s->set_reason_unknown(msg); }
void get_labels(svector<symbol>& r) override { s->get_labels(r); }
void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); }
ast_manager& get_manager() const override { return s->get_manager(); }
void reset_params(params_ref const& p) override { s->reset_params(p); }
params_ref const& get_params() const override { return s->get_params(); }
void collect_param_descrs(param_descrs& r) override { s->collect_param_descrs(r); }
void push_params() override { s->push_params(); }
void pop_params() override { s->pop_params(); }
void set_produce_models(bool f) override { s->set_produce_models(f); }
void set_phase(expr* e) override { s->set_phase(e); }
void move_to_front(expr* e) override { s->move_to_front(e); }
phase* get_phase() override { return s->get_phase(); }
void set_phase(phase* p) override { s->set_phase(p); }
unsigned get_num_assumptions() const override { return s->get_num_assumptions(); }
expr* get_assumption(unsigned idx) const override { return s->get_assumption(idx); }
unsigned get_scope_level() const override { return s->get_scope_level(); }
lbool check_sat_cc(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) override { return check_sat_cc(cube, clauses); }
void set_progress_callback(progress_callback* callback) override { s->set_progress_callback(callback); }
lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override {
return s->get_consequences(asms, vars, consequences);
}
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override { return s->find_mutexes(vars, mutexes); }
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) override { return s->preferred_sat(asms, cores); }
expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { return s->cube(vars, backtrack_level); }
expr* congruence_root(expr* e) override { return s->congruence_root(e); }
expr* congruence_next(expr* e) override { return s->congruence_next(e); }
std::ostream& display(std::ostream& out, unsigned n, expr* const* assumptions) const override {
return s->display(out, n, assumptions);
}
void get_units_core(expr_ref_vector& units) override { s->get_units_core(units); }
expr_ref_vector get_trail(unsigned max_level) override { return s->get_trail(max_level); }
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override { s->get_levels(vars, depth); }
void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override {
s->register_on_clause(ctx, on_clause);
}
void user_propagate_init(
void* ctx,
user_propagator::push_eh_t& push_eh,
user_propagator::pop_eh_t& pop_eh,
user_propagator::fresh_eh_t& fresh_eh) override {
s->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
}
void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override { s->user_propagate_register_fixed(fixed_eh); }
void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { s->user_propagate_register_final(final_eh); }
void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { s->user_propagate_register_eq(eq_eh); }
void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { s->user_propagate_register_diseq(diseq_eh); }
void user_propagate_register_expr(expr* e) override { /*m_preprocess.user_propagate_register_expr(e); */ s->user_propagate_register_expr(e); }
void user_propagate_register_created(user_propagator::created_eh_t& r) override { s->user_propagate_register_created(r); }
// void user_propagate_clear() override { m_preprocess.user_propagate_clear(); s->user_propagate_clear(); }
};
solver* mk_simplifier_solver(solver* s) {
return alloc(simplifier_solver, s);
}

25
src/solver/simplifier_solver.h Normal file
View file

@ -0,0 +1,25 @@
/*++
Copyright (c) 2023 Microsoft Corporation
Module Name:
simplifier_solver.cpp
Abstract:
Implements a solver with simplifying pre-processing.
Author:
Nikolaj Bjorner (nbjorner) 2023-01-30
--*/
#pragma once
#include "util/params.h"
class solver;
class solver_factory;
solver * mk_simplifier_solver(solver * s);

78
src/solver/solver_preprocess.cpp Normal file
View file

@ -0,0 +1,78 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
solver_preprocess.cpp
Abstract:
pre-process initialization module for solver
Author:
Nikolaj Bjorner (nbjorner) 2022-11-28
Notes:
- port various pre-processing to simplifiers
- qe-lite, fm-elimination, ite-lifting, other from asserted_formulas
--*/
#include "ast/rewriter/rewriter_def.h"
#include "ast/simplifiers/bit_blaster.h"
#include "ast/simplifiers/max_bv_sharing.h"
#include "ast/simplifiers/card2bv.h"
#include "ast/simplifiers/propagate_values.h"
#include "ast/simplifiers/rewriter_simplifier.h"
#include "ast/simplifiers/solve_eqs.h"
#include "ast/simplifiers/bv_slice.h"
#include "ast/simplifiers/eliminate_predicates.h"
#include "ast/simplifiers/elim_unconstrained.h"
#include "ast/simplifiers/pull_nested_quantifiers.h"
#include "ast/simplifiers/distribute_forall.h"
#include "ast/simplifiers/refine_inj_axiom.h"
#include "ast/simplifiers/elim_bounds.h"
#include "ast/simplifiers/bit2int.h"
#include "ast/simplifiers/bv_elim.h"
#include "ast/simplifiers/push_ite.h"
#include "ast/simplifiers/elim_term_ite.h"
#include "ast/simplifiers/flatten_clauses.h"
#include "ast/simplifiers/cnf_nnf.h"
#include "smt/params/smt_params.h"
#include "solver/solver_preprocess.h"
#include "qe/lite/qe_lite.h"
void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) {
smt_params smtp(p);
s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st));
if (smtp.m_solve_eqs) s.add_simplifier(alloc(euf::solve_eqs, m, st));
if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st));
if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st));
if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st));
if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st));
if (smtp.m_pull_nested_quantifiers) s.add_simplifier(alloc(pull_nested_quantifiers_simplifier, m, p, st));
if (smtp.m_max_bv_sharing) s.add_simplifier(mk_max_bv_sharing(m, p, st));
if (smtp.m_refine_inj_axiom) s.add_simplifier(alloc(refine_inj_axiom_simplifier, m, p, st));
if (smtp.m_bv_size_reduce) s.add_simplifier(alloc(bv::slice, m, st));
if (smtp.m_distribute_forall) s.add_simplifier(alloc(distribute_forall_simplifier, m, p, st));
if (smtp.m_eliminate_bounds) s.add_simplifier(alloc(elim_bounds_simplifier, m, p, st));
if (smtp.m_simplify_bit2int) s.add_simplifier(alloc(bit2int_simplifier, m, p, st));
if (smtp.m_bb_quantifiers) s.add_simplifier(alloc(bv::elim_simplifier, m, p, st));
if (smtp.m_eliminate_term_ite && smtp.m_lift_ite != lift_ite_kind::LI_FULL) s.add_simplifier(alloc(elim_term_ite_simplifier, m, p, st));
if (smtp.m_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(push_ite_simplifier, m, p, st, smtp.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE));
if (smtp.m_ng_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(ng_push_ite_simplifier, m, p, st, smtp.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE));
s.add_simplifier(alloc(flatten_clauses, m, p, st));
//
// add:
// euf_completion?
//
// add: make it externally programmable
//
}

2
src/sat/sat_solver/sat_smt_preprocess.h → src/solver/solver_preprocess.h
View file

@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation
Module Name:
sat_smt_preprocess.h
solver_preprocess.h
Abstract: