mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
bug fix: unsound pruning of assumptions. remove deprecated reduce() feature from smt_kernel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
70baa3c8c9
commit
f8f23382dc
|
@ -33,7 +33,6 @@ Notes:
|
|||
#include "pdr_prop_solver.h"
|
||||
#include "pdr_context.h"
|
||||
#include "pdr_generalizers.h"
|
||||
#include "datatype_decl_plugin.h"
|
||||
#include "for_each_expr.h"
|
||||
#include "dl_rule_set.h"
|
||||
#include "unit_subsumption_tactic.h"
|
||||
|
@ -1682,7 +1681,8 @@ namespace pdr {
|
|||
case l_false: {
|
||||
core_generalizer::cores cores;
|
||||
cores.push_back(std::make_pair(cube, uses_level));
|
||||
|
||||
TRACE("pdr", tout << "cube:\n";
|
||||
for (unsigned j = 0; j < cube.size(); ++j) tout << mk_pp(cube[j].get(), m) << "\n";);
|
||||
for (unsigned i = 0; !cores.empty() && i < m_core_generalizers.size(); ++i) {
|
||||
core_generalizer::cores new_cores;
|
||||
for (unsigned j = 0; j < cores.size(); ++j) {
|
||||
|
|
|
@ -398,6 +398,11 @@ namespace pdr {
|
|||
for (unsigned i = 0; i < r->size(); ++i) {
|
||||
lemmas.push_back(r->form(i));
|
||||
}
|
||||
TRACE("farkas_simplify_lemmas",
|
||||
tout << "simplified:\n";
|
||||
for (unsigned i = 0; i < lemmas.size(); ++i) {
|
||||
tout << mk_pp(lemmas[i].get(), m) << "\n";
|
||||
});
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -46,7 +46,6 @@ namespace pdr {
|
|||
expr_ref_vector m_assumptions;
|
||||
obj_map<app,expr *> m_proxies2expr;
|
||||
obj_map<expr, app*> m_expr2proxies;
|
||||
obj_hashtable<expr> m_implies;
|
||||
unsigned m_num_proxies;
|
||||
|
||||
app * mk_proxy(expr* literal) {
|
||||
|
@ -72,7 +71,6 @@ namespace pdr {
|
|||
expr_ref implies(m.mk_or(m.mk_not(res), literal), m);
|
||||
s.m_ctx->assert_expr(implies);
|
||||
m_assumptions.push_back(implies);
|
||||
m_implies.insert(implies);
|
||||
TRACE("pdr_verbose", tout << "name asserted " << mk_pp(implies, m) << "\n";);
|
||||
return res;
|
||||
}
|
||||
|
@ -92,6 +90,19 @@ namespace pdr {
|
|||
m_assumptions.append(conjs);
|
||||
}
|
||||
|
||||
expr* apply_accessor(
|
||||
ptr_vector<func_decl> const& acc,
|
||||
unsigned j,
|
||||
func_decl* f,
|
||||
expr* c) {
|
||||
if (is_app(c) && to_app(c)->get_decl() == f) {
|
||||
return to_app(c)->get_arg(j);
|
||||
}
|
||||
else {
|
||||
return m.mk_app(acc[j], c);
|
||||
}
|
||||
}
|
||||
|
||||
void expand_literals(expr_ref_vector& conjs) {
|
||||
arith_util arith(m);
|
||||
datatype_util dt(m);
|
||||
|
@ -100,6 +111,12 @@ namespace pdr {
|
|||
rational r;
|
||||
unsigned bv_size;
|
||||
|
||||
TRACE("pdr",
|
||||
tout << "begin expand\n";
|
||||
for (unsigned i = 0; i < conjs.size(); ++i) {
|
||||
tout << mk_pp(conjs[i].get(), m) << "\n";
|
||||
});
|
||||
|
||||
for (unsigned i = 0; i < conjs.size(); ++i) {
|
||||
expr* e = conjs[i].get();
|
||||
if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) {
|
||||
|
@ -117,10 +134,10 @@ namespace pdr {
|
|||
(m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){
|
||||
func_decl* f = to_app(val)->get_decl();
|
||||
func_decl* r = dt.get_constructor_recognizer(f);
|
||||
conjs[i] = m.mk_app(r,c);
|
||||
conjs[i] = m.mk_app(r, c);
|
||||
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f);
|
||||
for (unsigned i = 0; i < acc.size(); ++i) {
|
||||
conjs.push_back(m.mk_eq(m.mk_app(acc[i], c), to_app(val)->get_arg(i)));
|
||||
for (unsigned j = 0; j < acc.size(); ++j) {
|
||||
conjs.push_back(m.mk_eq(apply_accessor(acc, j, f, c), to_app(val)->get_arg(j)));
|
||||
}
|
||||
}
|
||||
else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) ||
|
||||
|
@ -142,6 +159,11 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
}
|
||||
TRACE("pdr",
|
||||
tout << "end expand\n";
|
||||
for (unsigned i = 0; i < conjs.size(); ++i) {
|
||||
tout << mk_pp(conjs[i].get(), m) << "\n";
|
||||
});
|
||||
}
|
||||
|
||||
public:
|
||||
|
@ -190,12 +212,7 @@ namespace pdr {
|
|||
expr_ref e(m);
|
||||
for (unsigned i = 0; i < es.size(); ++i) {
|
||||
e = es[i].get();
|
||||
if (m_implies.contains(e)) {
|
||||
e = m.mk_true();
|
||||
}
|
||||
else {
|
||||
rep(e);
|
||||
}
|
||||
rep(e);
|
||||
es[i] = e;
|
||||
if (m.is_true(e)) {
|
||||
es[i] = es.back();
|
||||
|
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
#include "pdr_smt_context_manager.h"
|
||||
#include "has_free_vars.h"
|
||||
#include "ast_pp.h"
|
||||
#include "ast_smt_pp.h"
|
||||
#include <sstream>
|
||||
#include "smt_params.h"
|
||||
|
||||
|
@ -78,6 +79,25 @@ namespace pdr {
|
|||
if (!m.is_true(m_pred)) {
|
||||
assumptions.push_back(m_pred);
|
||||
}
|
||||
TRACE("pdr_check",
|
||||
{
|
||||
ast_smt_pp pp(m);
|
||||
for (unsigned i = 0; i < m_context.size(); ++i) {
|
||||
pp.add_assumption(m_context.get_formulas()[i]);
|
||||
}
|
||||
for (unsigned i = 0; i < assumptions.size(); ++i) {
|
||||
pp.add_assumption(assumptions[i].get());
|
||||
}
|
||||
pp.display_smt2(tout, m.mk_true());
|
||||
|
||||
static unsigned lemma_id = 0;
|
||||
std::ostringstream strm;
|
||||
strm << "pdr-lemma-" << lemma_id << ".smt2";
|
||||
std::ofstream out(strm.str().c_str());
|
||||
pp.display_smt2(out, m.mk_true());
|
||||
out.close();
|
||||
lemma_id++;
|
||||
});
|
||||
lbool result = m_context.check(assumptions.size(), assumptions.c_ptr());
|
||||
if (!m.is_true(m_pred)) {
|
||||
assumptions.pop_back();
|
||||
|
|
|
@ -69,10 +69,6 @@ namespace smt {
|
|||
return m_kernel.get_asserted_formulas();
|
||||
}
|
||||
|
||||
bool reduce() {
|
||||
return m_kernel.reduce_assertions();
|
||||
}
|
||||
|
||||
void push() {
|
||||
TRACE("smt_kernel", tout << "push()\n";);
|
||||
m_kernel.push();
|
||||
|
@ -221,9 +217,6 @@ namespace smt {
|
|||
return m_imp->get_formulas();
|
||||
}
|
||||
|
||||
bool kernel::reduce() {
|
||||
return m_imp->reduce();
|
||||
}
|
||||
|
||||
void kernel::push() {
|
||||
m_imp->push();
|
||||
|
|
|
@ -84,15 +84,6 @@ namespace smt {
|
|||
*/
|
||||
expr * const * get_formulas() const;
|
||||
|
||||
/**
|
||||
\brief Reduce the set of asserted formulas using preprocessors.
|
||||
Return true if an inconsistency is detected.
|
||||
|
||||
\remark This is mainly used by dl_smt_relation. This method
|
||||
seens to be misplaced. This is not the right place.
|
||||
*/
|
||||
bool reduce();
|
||||
|
||||
/**
|
||||
\brief Create a backtracking point (aka scope level).
|
||||
*/
|
||||
|
|
Loading…
Reference in a new issue