mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
simplify models
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
36816e3b2f
commit
dd62ca5eb3
|
@ -47,6 +47,7 @@ Notes:
|
|||
#include "dl_boogie_proof.h"
|
||||
#include "qe_util.h"
|
||||
#include "scoped_proof.h"
|
||||
#include "expr_safe_replace.h"
|
||||
|
||||
namespace pdr {
|
||||
|
||||
|
@ -1062,10 +1063,7 @@ namespace pdr {
|
|||
predicates.pop_back();
|
||||
for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) {
|
||||
subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
|
||||
dctx.get_rewriter()(tmp);
|
||||
if (!m.is_true(tmp)) {
|
||||
constraints.push_back(tmp);
|
||||
}
|
||||
constraints.push_back(tmp);
|
||||
}
|
||||
for (unsigned i = 0; i < constraints.size(); ++i) {
|
||||
max_var = std::max(vc.get_max_var(constraints[i].get()), max_var);
|
||||
|
@ -1088,7 +1086,28 @@ namespace pdr {
|
|||
|
||||
children.append(n->children());
|
||||
}
|
||||
return pm.mk_and(constraints);
|
||||
|
||||
expr_safe_replace repl(m);
|
||||
for (unsigned i = 0; i < constraints.size(); ++i) {
|
||||
expr* e = constraints[i].get(), *e1, *e2;
|
||||
if (m.is_eq(e, e1, e2) && is_var(e1) && is_ground(e2)) {
|
||||
repl.insert(e1, e2);
|
||||
}
|
||||
else if (m.is_eq(e, e1, e2) && is_var(e2) && is_ground(e1)) {
|
||||
repl.insert(e2, e1);
|
||||
}
|
||||
}
|
||||
expr_ref_vector result(m);
|
||||
for (unsigned i = 0; i < constraints.size(); ++i) {
|
||||
expr_ref tmp(m);
|
||||
tmp = constraints[i].get();
|
||||
repl(tmp);
|
||||
dctx.get_rewriter()(tmp);
|
||||
if (!m.is_true(tmp)) {
|
||||
result.push_back(tmp);
|
||||
}
|
||||
}
|
||||
return pm.mk_and(result);
|
||||
}
|
||||
|
||||
proof_ref model_search::get_proof_trace(context const& ctx) {
|
||||
|
|
Loading…
Reference in a new issue