From 832ade3ac8ac89f77c1107df414d33b9154f8a5e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 31 Oct 2012 10:37:05 -0700
Subject: [PATCH] local changes
---
src/muz_qe/pdr_context.cpp | 41 +++++++++++++++++++++++++++++++++
src/muz_qe/pdr_context.h | 2 ++
src/muz_qe/pdr_dl_interface.cpp | 1 +
3 files changed, 44 insertions(+)
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index b89e7852f..7d7438f7b 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1297,6 +1297,45 @@ namespace pdr {
}
};
+ void context::validate() {
+ if (!m_params.get_bool(":validate-result", false)) {
+ return;
+ }
+ switch(m_last_result) {
+ case l_true: {
+ proof_ref pr = get_proof();
+ proof_checker checker(m);
+ expr_ref_vector side_conditions(m);
+ bool ok = check(pr, side_conditions);
+ if (!ok) {
+ IF_VERBOSE(0, verbose_stream() << "proof validation failed\n";);
+ }
+ break;
+ }
+ case l_false: {
+ expr_ref_vector refs(m);
+ model_ref model;
+ vector<relation_info> rs;
+ get_level_property(m_inductive_lvl, refs, rs);
+ inductive_property ex(m, const_cast<model_converter_ref&>(m_mc), rs);
+ ex.to_model(model);
+ decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
+ var_subst vs(m, false);
+ for (; it != end; ++it) {
+ ptr_vector<datalog::rule> const& rules = it->m_value->rules();
+ for (unsigned i = 0; i < rules.size(); ++i) {
+ datalog::rule* rule = rules[i];
+ // vs(rule->get_head(),
+ // apply interpretation of predicates to rule.
+ // create formula and check for unsat.
+ }
+ }
+ break;
+ }
+ default:
+ break;
+ }
+ }
void context::reset_core_generalizers() {
std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc<core_generalizer>());
@@ -1371,6 +1410,7 @@ namespace pdr {
check_quantifiers();
IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream()););
m_last_result = l_true;
+ validate();
return l_true;
}
catch (inductive_exception) {
@@ -1378,6 +1418,7 @@ namespace pdr {
m_last_result = l_false;
TRACE("pdr", display_certificate(tout););
IF_VERBOSE(1, display_certificate(verbose_stream()););
+ validate();
return l_false;
}
catch (unknown_exception) {
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 5e7f08b85..71b59ac26 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -333,6 +333,8 @@ namespace pdr {
void reset_core_generalizers();
+ void validate();
+
public:
/**
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp
index e336d314b..69f0995f0 100644
--- a/src/muz_qe/pdr_dl_interface.cpp
+++ b/src/muz_qe/pdr_dl_interface.cpp
@@ -206,6 +206,7 @@ void dl_interface::collect_params(param_descrs& p) {
p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples by extending candidate trace within search area");
p.insert(":unfold-rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring");
p.insert(":use-model-generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)");
+ p.insert(":validate-result", CPK_BOOL, "PDR (default false) validate result (by proof checking or model checking)");
PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states"););
PRIVATE_PARAMS(p.insert(":use-inductive-generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening"););
PRIVATE_PARAMS(p.insert(":use-interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation"););