mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
use datatype name instead of instantiation for cycle detection #5482
This commit is contained in:
parent
e90ec457c3
commit
e5b6cd36f0
|
@ -706,18 +706,20 @@ namespace datatype {
|
|||
\brief Return true if the inductive datatype is recursive.
|
||||
*/
|
||||
bool util::is_recursive_core(sort* s) const {
|
||||
obj_map<sort, status> already_found;
|
||||
map<symbol, status, symbol_hash_proc, symbol_eq_proc> already_found;
|
||||
ptr_vector<sort> todo, subsorts;
|
||||
sort* s0 = s;
|
||||
todo.push_back(s);
|
||||
status st;
|
||||
std::cout << "is recursive " << mk_pp(s, m) << "\n";
|
||||
while (!todo.empty()) {
|
||||
s = todo.back();
|
||||
if (already_found.find(s, st) && st == BLACK) {
|
||||
std::cout << "is recursive - todo " << mk_pp(s, m) << "\n";
|
||||
if (already_found.find(datatype_name(s), st) && st == BLACK) {
|
||||
todo.pop_back();
|
||||
continue;
|
||||
}
|
||||
already_found.insert(s, GRAY);
|
||||
already_found.insert(datatype_name(s), GRAY);
|
||||
def const& d = get_def(s);
|
||||
bool can_process = true;
|
||||
for (constructor const* c : d) {
|
||||
|
@ -728,9 +730,9 @@ namespace datatype {
|
|||
get_subsorts(d, subsorts);
|
||||
for (sort * s2 : subsorts) {
|
||||
if (is_datatype(s2)) {
|
||||
if (already_found.find(s2, st)) {
|
||||
if (already_found.find(datatype_name(s2), st)) {
|
||||
// type is recursive
|
||||
if (st == GRAY && s0 == s2)
|
||||
if (st == GRAY && datatype_name(s0) == datatype_name(s2))
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
|
@ -742,7 +744,7 @@ namespace datatype {
|
|||
}
|
||||
}
|
||||
if (can_process) {
|
||||
already_found.insert(s, BLACK);
|
||||
already_found.insert(datatype_name(s), BLACK);
|
||||
todo.pop_back();
|
||||
}
|
||||
}
|
||||
|
|
|
@ -323,6 +323,7 @@ namespace datatype {
|
|||
bool is_covariant(ast_mark& mark, ptr_vector<sort>& subsorts, sort* s) const;
|
||||
def& get_def(symbol const& s) { return plugin().get_def(s); }
|
||||
void get_subsorts(sort* s, ptr_vector<sort>& sorts) const;
|
||||
symbol datatype_name(sort* s) const { return s->get_parameter(0).get_symbol(); }
|
||||
|
||||
public:
|
||||
util(ast_manager & m);
|
||||
|
|
Loading…
Reference in a new issue