mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add rewrite to each branch of mbp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-24 17:06:49 -07:00
parent c32bfb5ecd
commit 915983821b
4 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/model/model.h
View file

@ -94,5 +94,7 @@ public:
}; };
}; };
std::ostream& operator<<(std::ostream& out, model_core const& m);
#endif /* MODEL_H_ */ #endif /* MODEL_H_ */

1
src/model/model_smt2_pp.h
View file

@ -25,6 +25,5 @@ Revision History:
void model_smt2_pp(std::ostream & out, ast_printer_context & ctx, model_core const & m, unsigned indent); void model_smt2_pp(std::ostream & out, ast_printer_context & ctx, model_core const & m, unsigned indent);
void model_smt2_pp(std::ostream & out, ast_manager & m, model_core const & md, unsigned indent); void model_smt2_pp(std::ostream & out, ast_manager & m, model_core const & md, unsigned indent);
std::ostream& operator<<(std::ostream& out, model_core const& m);
#endif #endif

2
src/muz/spacer/spacer_context.cpp
View file

@ -1347,7 +1347,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
if (is_sat == l_true || is_sat == l_undef) { if (is_sat == l_true || is_sat == l_undef) {
if (core) { core->reset(); } if (core) { core->reset(); }
if (model && *model) { if (model && model->get()) {
r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach); r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach);
TRACE ("spacer", tout << "reachable " TRACE ("spacer", tout << "reachable "
<< "is_concrete " << is_concrete << " rused: "; << "is_concrete " << is_concrete << " rused: ";

13
src/qe/qe_mbp.cpp
View file

@ -31,7 +31,6 @@ Revision History:
#include "qe/qe_arrays.h" #include "qe/qe_arrays.h"
#include "qe/qe_datatypes.h" #include "qe/qe_datatypes.h"
#include "qe/qe_lite.h" #include "qe/qe_lite.h"
#include "model/model_pp.h"
#include "model/model_evaluator.h" #include "model/model_evaluator.h"
@ -617,26 +616,25 @@ public:
qe::array_project_plugin ap(m); qe::array_project_plugin ap(m);
ap(mdl, array_vars, fml, vars, m_reduce_all_selects); ap(mdl, array_vars, fml, vars, m_reduce_all_selects);
SASSERT (array_vars.empty ()); SASSERT (array_vars.empty ());
m_rw (fml); m_rw(fml);
SASSERT (!m.is_false (fml)); SASSERT (!m.is_false (fml));
TRACE ("qe", TRACE ("qe",
tout << "extended model:\n"; tout << "extended model:\n" << mdl;
model_pp (tout, mdl);
tout << "Vars: " << vars << "\n"; tout << "Vars: " << vars << "\n";
); );
} }
// project reals, ints and other variables. // project reals, ints and other variables.
if (!other_vars.empty ()) { if (!other_vars.empty ()) {
TRACE ("qe", tout << "Other vars: " << other_vars << "\n"; TRACE ("qe", tout << "Other vars: " << other_vars << "\n" << mdl;);
model_pp(tout, mdl););
expr_ref_vector fmls(m); expr_ref_vector fmls(m);
flatten_and (fml, fmls); flatten_and (fml, fmls);
(*this)(false, other_vars, mdl, fmls); (*this)(false, other_vars, mdl, fmls);
fml = mk_and (fmls); fml = mk_and (fmls);
m_rw(fml);
TRACE ("qe", TRACE ("qe",
tout << "Projected other vars:\n" << fml << "\n"; tout << "Projected other vars:\n" << fml << "\n";
@ -646,14 +644,15 @@ public:
if (!other_vars.empty ()) { if (!other_vars.empty ()) {
project_vars (mdl, other_vars, fml); project_vars (mdl, other_vars, fml);
m_rw(fml);
} }
// substitute any remaining other vars // substitute any remaining other vars
if (!m_dont_sub && !other_vars.empty ()) { if (!m_dont_sub && !other_vars.empty ()) {
subst_vars (eval, other_vars, fml); subst_vars (eval, other_vars, fml);
TRACE ("qe", tout << "After substituting remaining other vars:\n" << fml << "\n";);
// an extra round of simplification because subst_vars is not simplifying // an extra round of simplification because subst_vars is not simplifying
m_rw(fml); m_rw(fml);
TRACE ("qe", tout << "After substituting remaining other vars:\n" << fml << "\n";);
other_vars.reset(); other_vars.reset();
} }