mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix bugs encountered by regression tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ec907a4705
commit
f44631ce73
|
@ -2883,9 +2883,9 @@ proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premis
|
|||
ptr_vector<expr> fmls;
|
||||
SASSERT(positions.size() + 1 == substs.size());
|
||||
for (unsigned i = 0; i < num_premises; ++i) {
|
||||
TRACE("dl", tout << mk_pp(premises[i], *this) << "\n";);
|
||||
TRACE("hyper_res", tout << mk_pp(premises[i], *this) << "\n";);
|
||||
fmls.push_back(get_fact(premises[i]));
|
||||
}
|
||||
}
|
||||
SASSERT(is_bool(concl));
|
||||
vector<parameter> params;
|
||||
for (unsigned i = 0; i < substs.size(); ++i) {
|
||||
|
@ -2898,6 +2898,10 @@ proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premis
|
|||
params.push_back(parameter(positions[i].second));
|
||||
}
|
||||
}
|
||||
TRACE("hyper_res",
|
||||
for (unsigned i = 0; i < params.size(); ++i) {
|
||||
params[i].display(tout); tout << "\n";
|
||||
});
|
||||
ptr_vector<sort> sorts;
|
||||
ptr_vector<expr> args;
|
||||
for (unsigned i = 0; i < num_premises; ++i) {
|
||||
|
|
|
@ -638,7 +638,16 @@ namespace datalog {
|
|||
|
||||
TRACE("dl",
|
||||
tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
|
||||
tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";);
|
||||
for (unsigned i = 0; i < s1.size(); ++i) {
|
||||
tout << mk_pp(s1[i], m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";
|
||||
for (unsigned i = 0; i < s2.size(); ++i) {
|
||||
tout << mk_pp(s2[i], m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
);
|
||||
|
||||
pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs);
|
||||
pc->insert(pr);
|
||||
|
|
|
@ -42,6 +42,7 @@ Notes:
|
|||
#include "dl_mk_rule_inliner.h"
|
||||
#include "ast_smt2_pp.h"
|
||||
#include "qe_lite.h"
|
||||
#include "ast_ll_pp.h"
|
||||
|
||||
namespace pdr {
|
||||
|
||||
|
@ -398,6 +399,9 @@ namespace pdr {
|
|||
lbool is_sat = m_solver.check_conjunction_as_assumptions(n.state());
|
||||
if (is_sat == l_true && core) {
|
||||
core->reset();
|
||||
TRACE("pdr", tout << "updating model\n";
|
||||
model_smt2_pp(tout, m, *model, 0);
|
||||
tout << mk_pp(n.state(), m) << "\n";);
|
||||
n.set_model(model);
|
||||
}
|
||||
return is_sat;
|
||||
|
@ -758,7 +762,7 @@ namespace pdr {
|
|||
}
|
||||
r0 = const_cast<datalog::rule*>(&pt().find_rule(*m_model.get()));
|
||||
app_ref_vector& inst = pt().get_inst(r0);
|
||||
TRACE("pdr", tout << mk_pp(state(), m) << "\n";);
|
||||
TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";);
|
||||
for (unsigned i = 0; i < inst.size(); ++i) {
|
||||
expr* v;
|
||||
if (model.find(inst[i].get(), v)) {
|
||||
|
@ -1421,6 +1425,7 @@ namespace pdr {
|
|||
proof_ref proof(m);
|
||||
SASSERT(m_last_result == l_true);
|
||||
proof = m_search.get_proof_trace(*this);
|
||||
TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
|
||||
apply(m, m_pc.get(), proof);
|
||||
return proof;
|
||||
}
|
||||
|
@ -1844,7 +1849,7 @@ namespace pdr {
|
|||
break;
|
||||
}
|
||||
case l_true: {
|
||||
strm << mk_ismt2_pp(mk_sat_answer(), m);
|
||||
strm << mk_pp(mk_sat_answer(), m);
|
||||
break;
|
||||
}
|
||||
case l_undef: {
|
||||
|
|
|
@ -126,9 +126,6 @@ void model_evaluator::setup_model(model_ref& model) {
|
|||
m_refs.push_back(e);
|
||||
assign_value(e, val);
|
||||
}
|
||||
|
||||
m_level1 = m1.get_level();
|
||||
m_level2 = m2.get_level();
|
||||
}
|
||||
|
||||
void model_evaluator::reset() {
|
||||
|
@ -170,11 +167,11 @@ expr_ref_vector model_evaluator::minimize_literals(ptr_vector<expr> const& formu
|
|||
tout << "formulas:\n";
|
||||
for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n";
|
||||
);
|
||||
|
||||
setup_model(mdl);
|
||||
|
||||
expr_ref_vector result(m);
|
||||
ptr_vector<expr> tocollect;
|
||||
|
||||
|
||||
setup_model(mdl);
|
||||
collect(formulas, tocollect);
|
||||
for (unsigned i = 0; i < tocollect.size(); ++i) {
|
||||
expr* e = tocollect[i];
|
||||
|
@ -301,8 +298,6 @@ void model_evaluator::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>
|
|||
ptr_vector<expr> todo;
|
||||
todo.append(formulas);
|
||||
m_visited.reset();
|
||||
m1.set_level(m_level1);
|
||||
m2.set_level(m_level2);
|
||||
|
||||
VERIFY(check_model(formulas));
|
||||
|
||||
|
@ -923,13 +918,32 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
|
|||
arith_util a;
|
||||
bool m_is_dl;
|
||||
|
||||
// NB. ite terms are non-arihmetical but their then/else branches can be.
|
||||
// this gets ignored (also in static_features)
|
||||
bool is_numeric(expr* e) const {
|
||||
if (a.is_numeral(e)) {
|
||||
return true;
|
||||
}
|
||||
expr* cond, *th, *el;
|
||||
if (m.is_ite(e, cond, th, el)) {
|
||||
return is_numeric(th) && is_numeric(el);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool is_arith_expr(expr *e) const {
|
||||
return is_app(e) && a.get_family_id() == to_app(e)->get_family_id();
|
||||
}
|
||||
|
||||
bool is_var_or_numeric(expr* e) const {
|
||||
if (a.is_numeral(e)) {
|
||||
return true;
|
||||
}
|
||||
expr* cond, *th, *el;
|
||||
if (m.is_ite(e, cond, th, el)) {
|
||||
return is_var_or_numeric(th) && is_var_or_numeric(el);
|
||||
}
|
||||
return !is_arith_expr(e);
|
||||
}
|
||||
|
||||
bool is_minus_one(expr const * e) const {
|
||||
rational r; return a.is_numeral(e, r) && r.is_minus_one();
|
||||
}
|
||||
|
@ -939,14 +953,14 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
|
|||
SASSERT(to_app(e)->get_num_args() == 2);
|
||||
expr * lhs = to_app(e)->get_arg(0);
|
||||
expr * rhs = to_app(e)->get_arg(1);
|
||||
if (!is_arith_expr(lhs) && !is_arith_expr(rhs))
|
||||
if (is_var_or_numeric(lhs) && is_var_or_numeric(rhs))
|
||||
return true;
|
||||
if (!a.is_numeral(rhs))
|
||||
if (!is_numeric(rhs))
|
||||
std::swap(lhs, rhs);
|
||||
if (!a.is_numeral(rhs))
|
||||
if (!is_numeric(rhs))
|
||||
return false;
|
||||
// lhs can be 'x' or '(+ x (* -1 y))'
|
||||
if (!is_arith_expr(lhs))
|
||||
if (is_var_or_numeric(lhs))
|
||||
return true;
|
||||
expr* arg1, *arg2;
|
||||
if (!a.is_add(lhs, arg1, arg2))
|
||||
|
@ -960,7 +974,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
|
|||
expr* m1, *m2;
|
||||
if (!a.is_mul(arg2, m1, m2))
|
||||
return false;
|
||||
return is_minus_one(m1) && !is_arith_expr(m2);
|
||||
return is_minus_one(m1) && is_var_or_numeric(m2);
|
||||
}
|
||||
|
||||
bool test_eq(expr* e) const {
|
||||
|
@ -976,21 +990,21 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
|
|||
}
|
||||
|
||||
bool test_term(expr* e) const {
|
||||
if (!is_arith_expr(e)) {
|
||||
return true;
|
||||
}
|
||||
if (m.is_bool(e)) {
|
||||
return true;
|
||||
}
|
||||
if (a.is_numeral(e)) {
|
||||
return true;
|
||||
}
|
||||
if (is_var_or_numeric(e)) {
|
||||
return true;
|
||||
}
|
||||
expr* lhs, *rhs;
|
||||
if (a.is_add(e, lhs, rhs)) {
|
||||
if (!a.is_numeral(lhs)) {
|
||||
std::swap(lhs, rhs);
|
||||
}
|
||||
return a.is_numeral(lhs) && !is_arith_expr(rhs);
|
||||
return a.is_numeral(lhs) && is_var_or_numeric(rhs);
|
||||
}
|
||||
if (a.is_mul(e, lhs, rhs)) {
|
||||
return is_minus_one(lhs) || is_minus_one(rhs);
|
||||
|
@ -998,6 +1012,17 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool is_non_arith_or_basic(expr* e) {
|
||||
if (!is_app(e)) {
|
||||
return false;
|
||||
}
|
||||
family_id fid = to_app(e)->get_family_id();
|
||||
return
|
||||
fid != m.get_basic_family_id() &&
|
||||
fid != null_family_id &&
|
||||
fid != a.get_family_id();
|
||||
}
|
||||
|
||||
public:
|
||||
test_diff_logic(ast_manager& m): m(m), a(m), m_is_dl(true) {}
|
||||
|
||||
|
@ -1011,8 +1036,11 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
|
|||
else if (m.is_eq(e)) {
|
||||
m_is_dl = test_eq(e);
|
||||
}
|
||||
else if (is_non_arith_or_basic(e)) {
|
||||
m_is_dl = false;
|
||||
}
|
||||
else if (is_app(e)) {
|
||||
app* a = to_app(e);
|
||||
app* a = to_app(e);
|
||||
for (unsigned i = 0; m_is_dl && i < a->get_num_args(); ++i) {
|
||||
m_is_dl = test_term(a->get_arg(i));
|
||||
}
|
||||
|
|
|
@ -65,10 +65,8 @@ namespace pdr {
|
|||
//01 -- X
|
||||
//10 -- false
|
||||
//11 -- true
|
||||
ast_fast_mark1 m1;
|
||||
ast_fast_mark2 m2;
|
||||
unsigned m_level1;
|
||||
unsigned m_level2;
|
||||
expr_mark m1;
|
||||
expr_mark m2;
|
||||
expr_mark m_visited;
|
||||
|
||||
|
||||
|
@ -84,7 +82,7 @@ namespace pdr {
|
|||
void inherit_value(expr* e, expr* v);
|
||||
|
||||
inline bool is_unknown(expr* x) { return !m1.is_marked(x) && !m2.is_marked(x); }
|
||||
inline void set_unknown(expr* x) { m1.reset_mark(x); m2.reset_mark(x); }
|
||||
inline void set_unknown(expr* x) { m1.mark(x, false); m2.mark(x, false); }
|
||||
inline bool is_x(expr* x) { return !m1.is_marked(x) && m2.is_marked(x); }
|
||||
inline bool is_false(expr* x) { return m1.is_marked(x) && !m2.is_marked(x); }
|
||||
inline bool is_true(expr* x) { return m1.is_marked(x) && m2.is_marked(x); }
|
||||
|
|
|
@ -107,6 +107,7 @@ namespace qe {
|
|||
ast_manager& m;
|
||||
app_ref_vector m_recognizers;
|
||||
expr_ref_vector m_eqs;
|
||||
expr_ref_vector m_neqs;
|
||||
app_ref_vector m_eq_atoms;
|
||||
app_ref_vector m_neq_atoms;
|
||||
app_ref_vector m_unsat_atoms;
|
||||
|
@ -117,7 +118,8 @@ namespace qe {
|
|||
datatype_atoms(ast_manager& m) :
|
||||
m(m),
|
||||
m_recognizers(m),
|
||||
m_eqs(m),
|
||||
m_eqs(m),
|
||||
m_neqs(m),
|
||||
m_eq_atoms(m), m_neq_atoms(m), m_unsat_atoms(m), m_eq_conds(m),
|
||||
m_util(m) {}
|
||||
|
||||
|
@ -291,6 +293,7 @@ namespace qe {
|
|||
}
|
||||
app* a = to_app(a0);
|
||||
if (a == x) {
|
||||
m_neqs.push_back(b);
|
||||
return true;
|
||||
}
|
||||
if (!m_util.is_constructor(a)) {
|
||||
|
|
|
@ -972,6 +972,7 @@ model_value_proc * theory_diff_logic<Ext>::mk_value(enode * n, model_generator &
|
|||
SASSERT(v != null_theory_var);
|
||||
numeral val = m_graph.get_assignment(v);
|
||||
rational num = val.get_rational().to_rational() + m_delta * val.get_infinitesimal().to_rational();
|
||||
TRACE("arith", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
|
||||
return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(n->get_owner())));
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue