From ccb50f5d8a6459246792c9c469514de9c2fbbb9c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Oct 2012 08:33:43 -0700 Subject: [PATCH 1/2] updated comments to create_children Signed-off-by: Nikolaj Bjorner --- lib/pdr_context.cpp | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp index 53cc9aac5..b24c6fa1c 100644 --- a/lib/pdr_context.cpp +++ b/lib/pdr_context.cpp @@ -1674,24 +1674,16 @@ namespace pdr { - T(x0,x1,x) for transition - phi(x) for n.state() - - psi(x0,x1,x) for psi - M(x0,x1,x) for n.model() Assumptions: - M => psi - psi => phi & T - psi & M agree on which rules are taken. + M => phi & T In other words, - 1. psi is a weakening of M - 2. phi & T is implied by psi + 1. phi & T is implied by M Goal is to find phi0(x0), phi1(x1) such that: - phi(x) & phi0(x0) & phi1(x1) => psi(x0, x1, x) - - or at least (ignoring psi alltogether): - phi(x) & phi0(x0) & phi1(x1) => T(x0, x1, x) Strategy: From 090ca2e46c73aa4db2e3c3aa345298261c330e9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Oct 2012 10:47:30 -0700 Subject: [PATCH 2/2] refined difference logic check, consolidate scoped modes Signed-off-by: Nikolaj Bjorner --- lib/dl_util.h | 23 ++++++++++++++++++----- lib/pdr_util.cpp | 20 +++++--------------- 2 files changed, 23 insertions(+), 20 deletions(-) diff --git a/lib/dl_util.h b/lib/dl_util.h index 3e01fb8d2..1969da1a9 100644 --- a/lib/dl_util.h +++ b/lib/dl_util.h @@ -171,19 +171,32 @@ namespace datalog { */ void display_fact(context & ctx, app * f, std::ostream & out); - class scoped_coarse_proof { - ast_manager& m; + class scoped_proof_mode { + ast_manager& m; proof_gen_mode m_mode; public: - scoped_coarse_proof(ast_manager& m): m(m) { + scoped_proof_mode(ast_manager& m, proof_gen_mode mode): m(m) { m_mode = m.proof_mode(); - m.toggle_proof_mode(PGM_COARSE); + m.toggle_proof_mode(mode); } - ~scoped_coarse_proof() { + ~scoped_proof_mode() { m.toggle_proof_mode(m_mode); } + }; + class scoped_coarse_proof : public scoped_proof_mode { + public: + scoped_coarse_proof(ast_manager& m): scoped_proof_mode(m, PGM_COARSE) {} + }; + + class scoped_no_proof : public scoped_proof_mode { + public: + scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {} + }; + + + class variable_intersection { bool values_match(const expr * v1, const expr * v2); diff --git a/lib/pdr_util.cpp b/lib/pdr_util.cpp index c09f1a246..1ec358fe1 100644 --- a/lib/pdr_util.cpp +++ b/lib/pdr_util.cpp @@ -911,22 +911,9 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { template class rewriter_tpl; - class scoped_no_proof { - ast_manager& m; - proof_gen_mode m_mode; - public: - scoped_no_proof(ast_manager& m): m(m) { - m_mode = m.proof_mode(); - m.toggle_proof_mode(PGM_DISABLED); - } - ~scoped_no_proof() { - m.toggle_proof_mode(m_mode); - } - }; - void hoist_non_bool_if(expr_ref& fml) { ast_manager& m = fml.get_manager(); - scoped_no_proof _sp(m); + datalog::scoped_no_proof _sp(m); params_ref p; ite_hoister_star ite_rw(m, p); expr_ref tmp(m); @@ -951,7 +938,7 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { } bool test_ineq(expr* e) const { - SASSERT(a.is_le(e) || a.is_ge(e)); + SASSERT(a.is_le(e) || a.is_ge(e) || m.is_eq(e)); SASSERT(to_app(e)->get_num_args() == 2); expr * lhs = to_app(e)->get_arg(0); expr * rhs = to_app(e)->get_arg(1); @@ -985,6 +972,9 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { if (!a.is_int_real(lhs)) { return true; } + if (a.is_numeral(lhs) || a.is_numeral(rhs)) { + return test_ineq(e); + } return test_term(lhs) && test_term(rhs); }