mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix bugs uncovered from running non-Horn SDV samples
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
cefa2d7650
commit
646ace6842
|
@ -90,21 +90,30 @@ class horn_tactic : public tactic {
|
|||
m_ctx.register_predicate(to_app(a)->get_decl(), true);
|
||||
}
|
||||
|
||||
void check_predicate(expr* a) {
|
||||
expr* a1 = 0;
|
||||
while (true) {
|
||||
void check_predicate(ast_mark& mark, expr* a) {
|
||||
ptr_vector<expr> todo;
|
||||
todo.push_back(a);
|
||||
while (!todo.empty()) {
|
||||
a = todo.back();
|
||||
todo.pop_back();
|
||||
if (mark.is_marked(a)) {
|
||||
continue;
|
||||
}
|
||||
mark.mark(a, true);
|
||||
if (is_quantifier(a)) {
|
||||
a = to_quantifier(a)->get_expr();
|
||||
continue;
|
||||
todo.push_back(a);
|
||||
}
|
||||
if (m.is_not(a, a1)) {
|
||||
a = a1;
|
||||
continue;
|
||||
else if (m.is_not(a) || m.is_and(a) || m.is_or(a) || m.is_implies(a)) {
|
||||
todo.append(to_app(a)->get_num_args(), to_app(a)->get_args());
|
||||
}
|
||||
if (is_predicate(a)) {
|
||||
else if (m.is_ite(a)) {
|
||||
todo.append(to_app(a)->get_arg(1));
|
||||
todo.append(to_app(a)->get_arg(2));
|
||||
}
|
||||
else if (is_predicate(a)) {
|
||||
register_predicate(a);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -112,14 +121,15 @@ class horn_tactic : public tactic {
|
|||
|
||||
formula_kind get_formula_kind(expr_ref& f) {
|
||||
normalize(f);
|
||||
ast_mark mark;
|
||||
expr_ref_vector args(m), body(m);
|
||||
expr_ref head(m);
|
||||
expr* a = 0, *a1 = 0;
|
||||
datalog::flatten_or(f, args);
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
a = args[i].get();
|
||||
check_predicate(a);
|
||||
if (m.is_not(a, a1) && is_predicate(a1)) {
|
||||
a = args[i].get();
|
||||
check_predicate(mark, a);
|
||||
if (m.is_not(a, a1)) {
|
||||
body.push_back(a1);
|
||||
}
|
||||
else if (is_predicate(a)) {
|
||||
|
@ -128,9 +138,6 @@ class horn_tactic : public tactic {
|
|||
}
|
||||
head = a;
|
||||
}
|
||||
else if (m.is_not(a, a1)) {
|
||||
body.push_back(a1);
|
||||
}
|
||||
else {
|
||||
body.push_back(m.mk_not(a));
|
||||
}
|
||||
|
|
|
@ -1827,10 +1827,8 @@ namespace pdr {
|
|||
proof_ref pr(m);
|
||||
pr = m.mk_asserted(m.mk_true());
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
if (smt::is_value_sort(m, vars[i].get())) {
|
||||
tmp = mev.eval(M, vars[i].get());
|
||||
sub.insert(vars[i].get(), tmp, pr);
|
||||
}
|
||||
tmp = mev.eval(M, vars[i].get());
|
||||
sub.insert(vars[i].get(), tmp, pr);
|
||||
}
|
||||
if (!rep) rep = mk_expr_simp_replacer(m);
|
||||
rep->set_substitution(&sub);
|
||||
|
|
|
@ -608,6 +608,7 @@ namespace pdr {
|
|||
best effort evaluator of extensional array equality.
|
||||
*/
|
||||
void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2) {
|
||||
TRACE("pdr", tout << "array equality: " << mk_pp(e, m) << "\n";);
|
||||
expr_ref v1(m), v2(m);
|
||||
m_model->eval(arg1, v1);
|
||||
m_model->eval(arg2, v2);
|
||||
|
@ -633,7 +634,10 @@ namespace pdr {
|
|||
|
||||
if (else1 != else2) {
|
||||
if (m.is_value(else1) && m.is_value(else2)) {
|
||||
set_bool(e, false);
|
||||
TRACE("pdr", tout
|
||||
<< "defaults are different: " << mk_pp(e, m) << " "
|
||||
<< mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";);
|
||||
set_false(e);
|
||||
}
|
||||
else {
|
||||
TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
|
||||
|
@ -659,7 +663,10 @@ namespace pdr {
|
|||
continue;
|
||||
}
|
||||
else if (m.is_value(w1) && m.is_value(w2)) {
|
||||
set_bool(e, false);
|
||||
TRACE("pdr", tout << "Equality evaluation: " << mk_pp(e, m) << "\n";
|
||||
tout << mk_pp(s1, m) << " |-> " << mk_pp(w1, m) << "\n";
|
||||
tout << mk_pp(s2, m) << " |-> " << mk_pp(w2, m) << "\n";);
|
||||
set_false(e);
|
||||
return;
|
||||
}
|
||||
else {
|
||||
|
@ -668,7 +675,7 @@ namespace pdr {
|
|||
return;
|
||||
}
|
||||
}
|
||||
set_bool(e, true);
|
||||
set_true(e);
|
||||
}
|
||||
|
||||
void model_evaluator::eval_eq(app* e, expr* arg1, expr* arg2) {
|
||||
|
|
|
@ -102,6 +102,7 @@ template<typename Ext>
|
|||
bool theory_diff_logic<Ext>::internalize_term(app * term) {
|
||||
bool result = null_theory_var != mk_term(term);
|
||||
CTRACE("arith", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";);
|
||||
TRACE("non_diff_logic", tout << "Terms may not be internalized\n";);
|
||||
found_non_diff_logic_expr(term);
|
||||
return result;
|
||||
}
|
||||
|
@ -831,6 +832,7 @@ theory_var theory_diff_logic<Ext>::mk_var(app* n) {
|
|||
v = mk_var(e);
|
||||
}
|
||||
if (is_interpreted(n)) {
|
||||
TRACE("non_diff_logic", tout << "Variable should not be interpreted\n";);
|
||||
found_non_diff_logic_expr(n);
|
||||
}
|
||||
TRACE("arith", tout << mk_pp(n, get_manager()) << " |-> " << v << "\n";);
|
||||
|
|
Loading…
Reference in a new issue