From 8192f36c5038b07ecc09716e836c1d2092ba3af3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Aug 2023 13:06:22 -0700 Subject: [PATCH] refactor dependencies Signed-off-by: Nikolaj Bjorner --- src/CMakeLists.txt | 1 + src/cmd_context/extra_cmds/CMakeLists.txt | 1 + src/cmd_context/extra_cmds/dbg_cmds.cpp | 2 +- src/qe/CMakeLists.txt | 1 - src/qe/{ => mbi}/qe_mbi.cpp | 2 +- src/qe/{ => mbi}/qe_mbi.h | 0 src/sat/smt/CMakeLists.txt | 1 + src/sat/smt/synth_solver.cpp | 43 +++++++++-------------- 8 files changed, 21 insertions(+), 30 deletions(-) rename src/qe/{ => mbi}/qe_mbi.cpp (99%) rename src/qe/{ => mbi}/qe_mbi.h (100%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e091db15f..b39f2c04d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -57,6 +57,7 @@ add_subdirectory(ast/simplifiers) add_subdirectory(tactic) add_subdirectory(qe/mbp) add_subdirectory(qe/lite) +add_subdirectory(qe/mbi) add_subdirectory(smt/params) add_subdirectory(parsers/util) add_subdirectory(math/grobner) diff --git a/src/cmd_context/extra_cmds/CMakeLists.txt b/src/cmd_context/extra_cmds/CMakeLists.txt index 1c36745b1..ae6db620a 100644 --- a/src/cmd_context/extra_cmds/CMakeLists.txt +++ b/src/cmd_context/extra_cmds/CMakeLists.txt @@ -5,6 +5,7 @@ z3_add_component(extra_cmds subpaving_cmds.cpp proof_cmds.cpp COMPONENT_DEPENDENCIES + mbi arith_tactics cmd_context subpaving_tactic diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index c8f5deb7d..3beb304bb 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -33,7 +33,7 @@ Notes: #include "ast/ast_util.h" #include "util/gparams.h" #include "qe/qe_mbp.h" -#include "qe/qe_mbi.h" +#include "qe/mbi/qe_mbi.h" #include "qe/mbp/mbp_term_graph.h" #include "qe/mbp/mbp_qel.h" #include "qe/lite/qe_lite_tactic.h" diff --git a/src/qe/CMakeLists.txt b/src/qe/CMakeLists.txt index 8539db7a2..4d5dfca4b 100644 --- a/src/qe/CMakeLists.txt +++ b/src/qe/CMakeLists.txt @@ -10,7 +10,6 @@ z3_add_component(qe qe.cpp qe_datatype_plugin.cpp qe_dl_plugin.cpp - qe_mbi.cpp qe_mbp.cpp qe_tactic.cpp qsat.cpp diff --git a/src/qe/qe_mbi.cpp b/src/qe/mbi/qe_mbi.cpp similarity index 99% rename from src/qe/qe_mbi.cpp rename to src/qe/mbi/qe_mbi.cpp index b1dc58999..3a8c242ab 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/mbi/qe_mbi.cpp @@ -38,7 +38,7 @@ Notes: #include "ast/arith_decl_plugin.h" #include "model/model_evaluator.h" #include "solver/solver.h" -#include "qe/qe_mbi.h" +#include "qe/mbi/qe_mbi.h" #include "qe/mbp/mbp_term_graph.h" #include "qe/mbp/mbp_arith.h" #include "qe/mbp/mbp_arrays.h" diff --git a/src/qe/qe_mbi.h b/src/qe/mbi/qe_mbi.h similarity index 100% rename from src/qe/qe_mbi.h rename to src/qe/mbi/qe_mbi.h diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index cc8466003..7d6d9ac0e 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -53,5 +53,6 @@ z3_add_component(sat_smt euf mbp smt_params + mbi ) diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp index b29832d48..c49eb1425 100644 --- a/src/sat/smt/synth_solver.cpp +++ b/src/sat/smt/synth_solver.cpp @@ -19,7 +19,7 @@ Author: #include "ast/rewriter/th_rewriter.h" #include "sat/smt/synth_solver.h" #include "sat/smt/euf_solver.h" -#include "qe/qe_mbi.h" +#include "qe/mbi/qe_mbi.h" namespace synth { @@ -102,6 +102,7 @@ namespace synth { } sat::check_result solver::check() { + verbose_stream() << "check\n"; if (m_synth.empty()) return sat::check_result::CR_DONE; @@ -184,6 +185,7 @@ namespace synth { for (auto& e : m_synth) { euf::enode* n = expr2enode(e.output()); if (is_computable(n) && !e.is_solved()) { + verbose_stream() << "set solution\n"; e.set_solution(nullptr); ctx.push(synth_objective::unset_solution(e)); } @@ -360,6 +362,12 @@ namespace synth { expr_ref cond = compute_condition(); add_unit(~mk_literal(cond)); IF_VERBOSE(0, verbose_stream() << "if " << cond << "\n"); + + // clear the solutions that are computed by projection + // projection may not contradict the current assignment and therefore + // not cause backtracking. + for (synth_objective& e : m_synth) + e.clear_solution(); return true; } @@ -412,8 +420,8 @@ namespace synth { return false; model_ref mdl = alloc(model, m); ctx.update_model(mdl, false); - verbose_stream() << "int-real-objective\n"; - verbose_stream() << *mdl << "\n"; + // verbose_stream() << "int-real-objective\n"; + // verbose_stream() << *mdl << "\n"; expr_ref_vector lits(m), core(m); for (unsigned i = 0; i < s().trail_size(); ++i) { @@ -424,16 +432,16 @@ namespace synth { if (e) lits.push_back(e); } - verbose_stream() << lits << "\n"; + // verbose_stream() << lits << "\n"; - sat::no_drat_params no_drat_params; + sat::no_drat_params no_drat_params; ref<::solver> solver = mk_smt2_solver(m, no_drat_params, symbol::null); solver->assert_expr(m.mk_not(m.mk_and(m_spec))); lbool r = solver->check_sat(lits); if (r != l_false) return false; solver->get_unsat_core(core); - verbose_stream() << "core " << core << "\n"; + // verbose_stream() << "core " << core << "\n"; qe::uflia_project proj(m); auto& egraph = ctx.get_egraph(); @@ -444,37 +452,18 @@ namespace synth { visited.mark(n->get_decl(), true); shared.push_back(n->get_decl()); } - verbose_stream() << "shared " << shared << "\n"; + // verbose_stream() << "shared " << shared << "\n"; proj.set_shared(shared); auto defs = proj.project_solve(mdl, core); for (auto const& d : defs) { - verbose_stream() << d.var << " := " << d.term << "\n"; + IF_VERBOSE(3, verbose_stream() << d.var << " := " << d.term << "\n"); if (d.var == obj.output()) { obj.set_solution(d.term); ctx.push(synth_objective::unset_solution(obj)); return true; } } -#if 0 - // - retrieve literal dependencies - // - difference cert? - // - split arith? - // - split_arith, arith_vars, rpoejct, project_euf, - // produce projection - - add_dcert(mdl, lits); - expr_ref_vector alits(m), uflits(m); - split_arith(lits, alits, uflits); - auto avars = get_arith_vars(lits); - vector defs = arith_project(mdl, avars, alits); - for (auto const& d : defs) uflits.push_back(m.mk_eq(d.var, d.term)); - TRACE("qe", tout << "uflits: " << uflits << "\n";); - project_euf(mdl, uflits); - lits.reset(); - lits.append(alits); - lits.append(uflits); -#endif return false; }