From dd62ca5eb36c2a62ee44fc5a79fc27c883de21ae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 6 Sep 2014 20:54:16 -0700 Subject: [PATCH] simplify models Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 29 ++++++++++++++++++++++++----- 1 file changed, 24 insertions(+), 5 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index d8b96297a..f07964395 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -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) {