mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

fixing bugs with validation code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-10-15 03:53:33 -07:00
parent 9b34350646
commit eb4c10c037
4 changed files with 14 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz/pdr/pdr_context.cpp
View file

@ -1123,9 +1123,7 @@ namespace pdr {
n->mk_instantiate(r0, r1, binding); n->mk_instantiate(r0, r1, binding);
proof_ref p1(m), p2(m); proof_ref p1(m), p2(m);
p1 = r0->get_proof(); p1 = r0->get_proof();
if (!p1) { IF_VERBOSE(0, if (!p1) r0->display(dctx, verbose_stream()););
r0->display(dctx, std::cout);
}
SASSERT(p1); SASSERT(p1);
pfs[0] = p1; pfs[0] = p1;
rls[0] = r1; rls[0] = r1;

11
src/muz/transforms/dl_mk_array_blast.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include "dl_mk_array_blast.h" #include "dl_mk_array_blast.h"
#include "qe_util.h" #include "qe_util.h"
#include "scoped_proof.h"
namespace datalog { namespace datalog {
@ -270,7 +271,7 @@ namespace datalog {
} }
} }
expr_ref fml2(m), body(m), head(m); expr_ref fml1(m), fml2(m), body(m), head(m);
body = m.mk_and(new_conjs.size(), new_conjs.c_ptr()); body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
head = r.get_head(); head = r.get_head();
sub(body); sub(body);
@ -287,9 +288,17 @@ namespace datalog {
proof_ref p(m); proof_ref p(m);
rule_set new_rules(m_ctx); rule_set new_rules(m_ctx);
rm.mk_rule(fml2, p, new_rules, r.name()); rm.mk_rule(fml2, p, new_rules, r.name());
rule_ref new_rule(rm); rule_ref new_rule(rm);
if (m_simplifier.transform_rule(new_rules.last(), new_rule)) { if (m_simplifier.transform_rule(new_rules.last(), new_rule)) {
if (r.get_proof()) {
scoped_proof _sc(m);
r.to_formula(fml1);
p = m.mk_rewrite(fml1, fml2);
p = m.mk_modus_ponens(r.get_proof(), p);
new_rule->set_proof(m, p);
}
rules.add_rule(new_rule.get()); rules.add_rule(new_rule.get());
rm.mk_rule_rewrite_proof(r, *new_rule.get()); rm.mk_rule_rewrite_proof(r, *new_rule.get());
TRACE("dl", new_rule->display(m_ctx, tout << "new rule\n");); TRACE("dl", new_rule->display(m_ctx, tout << "new rule\n"););

4
src/muz/transforms/dl_mk_bit_blast.cpp
View file

@ -25,6 +25,7 @@ Revision History:
#include "filter_model_converter.h" #include "filter_model_converter.h"
#include "dl_mk_interp_tail_simplifier.h" #include "dl_mk_interp_tail_simplifier.h"
#include "fixedpoint_params.hpp" #include "fixedpoint_params.hpp"
#include "scoped_proof.h"
namespace datalog { namespace datalog {
@ -268,7 +269,8 @@ namespace datalog {
r->to_formula(fml); r->to_formula(fml);
if (blast(r, fml)) { if (blast(r, fml)) {
proof_ref pr(m); proof_ref pr(m);
if (m_context.generate_proof_trace()) { if (r->get_proof()) {
scoped_proof _sc(m);
pr = m.mk_asserted(fml); // loses original proof of r. pr = m.mk_asserted(fml); // loses original proof of r.
} }
// TODO add logic for pc: // TODO add logic for pc:

1
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -341,7 +341,6 @@ namespace datalog {
} }
head = mk_head(source, *result, r.get_head(), cnt); head = mk_head(source, *result, r.get_head(), cnt);
fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head); fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head);
rule_ref_vector added_rules(rm);
proof_ref pr(m); proof_ref pr(m);
rm.mk_rule(fml, pr, *result); rm.mk_rule(fml, pr, *result);
TRACE("dl", result->last()->display(m_ctx, tout);); TRACE("dl", result->last()->display(m_ctx, tout););