Skip to content

Commit

Permalink
fix unsoundness in explanation handling for nested datatypes and sequ…
Browse files Browse the repository at this point in the history 
…ences
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jul 4, 2022
1 parent e6e0c74 commit 1e8f907
Show file tree
Hide file tree
Showing 4 changed files with 54 additions and 30 deletions.
16 changes: 16 additions & 0 deletions src/ast/seq_decl_plugin.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -971,6 +971,22 @@ bool seq_util::str::is_len_sub(expr const* s, expr*& l, expr*& u, rational& k) c
return false;
}

bool seq_util::str::is_concat_of_units(expr* s) const {
ptr_vector<expr> todo;
todo.push_back(s);
while (!todo.empty()) {
expr* e = todo.back();
todo.pop_back();
if (is_empty(e) || is_unit(e))
continue;
if (is_concat(e))
todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
else
return false;
}
return true;
}

bool seq_util::str::is_unit_string(expr const* s, expr_ref& c) const {
zstring z;
expr* ch = nullptr;
Expand Down
1 change: 1 addition & 0 deletions src/ast/seq_decl_plugin.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -375,6 +375,7 @@ class seq_util {
bool is_to_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_TO_CODE); }

bool is_len_sub(expr const* n, expr*& l, expr*& u, rational& k) const;
bool is_concat_of_units(expr* n) const;

/*
tests if s is a single character string(c) or a unit (c)
Expand Down
65 changes: 36 additions & 29 deletions src/smt/theory_datatype.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ Revision History:
#include "smt/theory_datatype.h"
#include "smt/theory_array.h"
#include "smt/smt_model_generator.h"
#include <iostream>

namespace smt {

Expand Down Expand Up @@ -519,9 +520,8 @@ namespace smt {

void theory_datatype::explain_is_child(enode* parent, enode* child) {
enode * parentc = oc_get_cstor(parent);
if (parent != parentc) {
if (parent != parentc)
m_used_eqs.push_back(enode_pair(parent, parentc));
}

// collect equalities on all children that may have been used.
bool found = false;
Expand All @@ -546,11 +546,13 @@ namespace smt {
}
sort* se = nullptr;
if (m_sutil.is_seq(s, se) && m_util.is_datatype(se)) {
for (enode* aarg : get_seq_args(arg)) {
enode* sibling;
for (enode* aarg : get_seq_args(arg, sibling)) {
if (aarg->get_root() == child->get_root()) {
if (aarg != child) {
if (aarg != child)
m_used_eqs.push_back(enode_pair(aarg, child));
}
if (sibling != arg)
m_used_eqs.push_back(enode_pair(arg, sibling));
found = true;
}
}
Expand Down Expand Up @@ -582,9 +584,11 @@ namespace smt {

TRACE("datatype",
tout << "occurs_check\n";
for (enode_pair const& p : m_used_eqs) {
for (enode_pair const& p : m_used_eqs)
tout << enode_eq_pp(p, ctx);
});
for (auto const& [a,b] : m_used_eqs)
tout << mk_pp(a->get_expr(), m) << " = " << mk_pp(b->get_expr(), m) << "\n";
);
}

// start exploring subgraph below `app`
Expand All @@ -596,9 +600,9 @@ namespace smt {
}
v = m_find.find(v);
var_data * d = m_var_data[v];
if (!d->m_constructor) {

if (!d->m_constructor)
return false;
}
enode * parent = d->m_constructor;
oc_mark_on_stack(parent);
auto process_arg = [&](enode* aarg) {
Expand All @@ -616,9 +620,8 @@ namespace smt {
};

for (enode * arg : enode::args(parent)) {
if (oc_cycle_free(arg)) {
if (oc_cycle_free(arg))
continue;
}
if (oc_on_stack(arg)) {
// arg was explored before app, and is still on the stack: cycle
occurs_check_explain(parent, arg);
Expand All @@ -632,9 +635,11 @@ namespace smt {
oc_push_stack(arg);
}
else if (m_sutil.is_seq(s, se) && m_util.is_datatype(se)) {
for (enode* sarg : get_seq_args(arg))
if (process_arg(sarg))
enode* sibling;
for (enode* sarg : get_seq_args(arg, sibling)) {
if (process_arg(sarg))
return true;
}
}
else if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
for (enode* aarg : get_array_args(arg))
Expand All @@ -645,7 +650,7 @@ namespace smt {
return false;
}

ptr_vector<enode> const& theory_datatype::get_seq_args(enode* n) {
ptr_vector<enode> const& theory_datatype::get_seq_args(enode* n, enode*& sibling) {
m_args.reset();
m_todo.reset();
auto add_todo = [&](enode* n) {
Expand All @@ -654,9 +659,14 @@ namespace smt {
m_todo.push_back(n);
}
};

for (enode* sib : *n)
add_todo(sib);

for (enode* sib : *n) {
if (m_sutil.str.is_concat_of_units(sib->get_expr())) {
add_todo(sib);
sibling = sib;
break;
}
}

for (unsigned i = 0; i < m_todo.size(); ++i) {
enode* n = m_todo[i];
Expand Down Expand Up @@ -691,7 +701,7 @@ namespace smt {
a3 = cons(v3, a1)
*/
bool theory_datatype::occurs_check(enode * n) {
TRACE("datatype", tout << "occurs check: " << enode_pp(n, ctx) << "\n";);
TRACE("datatype_verbose", tout << "occurs check: " << enode_pp(n, ctx) << "\n";);
m_stats.m_occurs_check++;

bool res = false;
Expand All @@ -706,7 +716,7 @@ namespace smt {
if (oc_cycle_free(app))
continue;

TRACE("datatype", tout << "occurs check loop: " << enode_pp(app, ctx) << (op==ENTER?" enter":" exit")<< "\n";);
TRACE("datatype_verbose", tout << "occurs check loop: " << enode_pp(app, ctx) << (op==ENTER?" enter":" exit")<< "\n";);

switch (op) {
case ENTER:
Expand Down Expand Up @@ -830,15 +840,14 @@ namespace smt {
SASSERT(d->m_constructor);
func_decl * c_decl = d->m_constructor->get_decl();
datatype_value_proc * result = alloc(datatype_value_proc, c_decl);
for (enode* arg : enode::args(d->m_constructor)) {
for (enode* arg : enode::args(d->m_constructor))
result->add_dependency(arg);
}
TRACE("datatype",
tout << pp(n, m) << "\n";
tout << "depends on\n";
for (enode* arg : enode::args(d->m_constructor)) {
for (enode* arg : enode::args(d->m_constructor))
tout << " " << pp(arg, m) << "\n";
});
);
return result;
}

Expand Down Expand Up @@ -965,12 +974,11 @@ namespace smt {
SASSERT(!lits.empty());
region & reg = ctx.get_region();
TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_expr(), m) << "\n";
for (literal l : lits) {
for (literal l : lits)
ctx.display_detailed_literal(tout, l) << "\n";
}
for (auto const& p : eqs) {
for (auto const& p : eqs)
tout << enode_eq_pp(p, ctx);
});
);
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, lits.size(), lits.data(), eqs.size(), eqs.data())));
}
else if (num_unassigned == 1) {
Expand Down Expand Up @@ -1052,9 +1060,8 @@ namespace smt {
ctx.mark_as_relevant(curr);
return;
}
else if (ctx.get_assignment(curr) != l_false) {
else if (ctx.get_assignment(curr) != l_false)
return;
}
}
if (r == nullptr)
return; // all recognizers are asserted to false... conflict will be detected...
Expand Down
2 changes: 1 addition & 1 deletion src/smt/theory_datatype.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ namespace smt {
void oc_push_stack(enode * n);
ptr_vector<enode> m_args, m_todo;
ptr_vector<enode> const& get_array_args(enode* n);
ptr_vector<enode> const& get_seq_args(enode* n);
ptr_vector<enode> const& get_seq_args(enode* n, enode*& sibling);

// class for managing state of final_check
class final_check_st {
Expand Down

0 comments on commit 1e8f907

Please sign in to comment.