mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

deal with infinite loop in diagonalization attempt in datatype factory

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-05-21 10:23:31 -07:00
parent e3098b0ec5
commit 2ee416fc8f
2 changed files with 35 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/smt/proto_model/datatype_factory.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include"proto_model.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"expr_functors.h"
datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
struct_factory(m, m.mk_family_id("datatype"), md),
@ -47,8 +48,10 @@ expr * datatype_factory::get_some_value(sort * s) {
*/
expr * datatype_factory::get_last_fresh_value(sort * s) {
expr * val = 0;
if (m_last_fresh_value.find(s, val))
if (m_last_fresh_value.find(s, val)) {
TRACE("datatype_factory", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
return val;
}
value_set * set = get_value_set(s);
if (set->empty())
val = get_some_value(s);
@ -59,6 +62,17 @@ expr * datatype_factory::get_last_fresh_value(sort * s) {
return val;
}
bool datatype_factory::is_subterm_of_last_value(app* e) {
expr* last;
if (!m_last_fresh_value.find(m_manager.get_sort(e), last)) {
return false;
}
contains_app contains(m_manager, e);
bool result = contains(last);
TRACE("datatype_factory", tout << mk_pp(e, m_manager) << " in " << mk_pp(last, m_manager) << " " << result << "\n";);
return result;
}
/**
\brief Create an almost fresh value. If s is recursive, then the result is not 0.
It also updates m_last_fresh_value
@ -105,11 +119,18 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
}
}
if (recursive || found_fresh_arg) {
expr * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
app * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
SASSERT(!found_fresh_arg || !set->contains(new_value));
register_value(new_value);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, new_value);
if (m_util.is_recursive(s)) {
if (is_subterm_of_last_value(new_value)) {
new_value = static_cast<app*>(m_last_fresh_value.find(s));
}
else {
m_last_fresh_value.insert(s, new_value);
}
}
TRACE("datatype_factory", tout << "almost fresh: " << mk_pp(new_value, m_manager) << "\n";);
return new_value;
}
}
@ -181,12 +202,20 @@ expr * datatype_factory::get_fresh_value(sort * s) {
expr_ref_vector args(m_manager);
bool found_sibling = false;
unsigned num = constructor->get_arity();
TRACE("datatype_factory", tout << "checking constructor: " << constructor->get_name() << "\n";);
for (unsigned i = 0; i < num; i++) {
sort * s_arg = constructor->get_domain(i);
TRACE("datatype_factory", tout << mk_pp(s, m_manager) << " "
<< mk_pp(s_arg, m_manager) << " are_siblings "
<< m_util.are_siblings(s, s_arg) << " is_datatype "
<< m_util.is_datatype(s_arg) << " found_sibling "
<< found_sibling << "\n";);
if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
found_sibling = true;
expr * maybe_new_arg = get_almost_fresh_value(s_arg);
if (!maybe_new_arg) {
TRACE("datatype_factory",
tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
maybe_new_arg = m_model.get_some_value(s_arg);
found_sibling = false;
}

2
src/smt/proto_model/datatype_factory.h
View file

@ -29,6 +29,8 @@ class datatype_factory : public struct_factory {
expr * get_last_fresh_value(sort * s);
expr * get_almost_fresh_value(sort * s);
bool is_subterm_of_last_value(app* e);
public:
datatype_factory(ast_manager & m, proto_model & md);
virtual ~datatype_factory() {}