mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

avoid name clash for multiple special relations #6743

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-06-07 17:55:11 -07:00
parent ab4b7c50ed
commit 1d62964c58
1 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_special_relations.cpp
View file

@ -888,9 +888,14 @@ namespace smt {
func_decl* memf, *nextf, *connectedf; func_decl* memf, *nextf, *connectedf;
std::string member, next, connected_sym;
unsigned index = r.decl()->get_parameter(0).get_int();
member = "member" + std::to_string(index);
next = "next" + std::to_string(index);
connected_sym = "connected" + std::to_string(index);
{ {
sort* dom[2] = { s, listS }; sort* dom[2] = { s, listS };
recfun::promise_def mem = p.ensure_def(symbol("member"), 2, dom, m.mk_bool_sort(), true); recfun::promise_def mem = p.ensure_def(symbol(member), 2, dom, m.mk_bool_sort(), true);
memf = mem.get_def()->get_decl(); memf = mem.get_def()->get_decl();
var_ref xV(m.mk_var(1, s), m); var_ref xV(m.mk_var(1, s), m);
@ -913,7 +918,7 @@ namespace smt {
{ {
sort* dom[5] = { s, s, listS, listS, tup }; sort* dom[5] = { s, s, listS, listS, tup };
recfun::promise_def nxt = p.ensure_def(symbol("next"), 5, dom, tup, true); recfun::promise_def nxt = p.ensure_def(symbol(next), 5, dom, tup, true);
nextf = nxt.get_def()->get_decl(); nextf = nxt.get_def()->get_decl();
expr_ref next_body(m); expr_ref next_body(m);
@ -934,7 +939,7 @@ namespace smt {
{ {
sort* dom[3] = { listS, s, listS }; sort* dom[3] = { listS, s, listS };
recfun::promise_def connected = p.ensure_def(symbol("connected"), 3, dom, m.mk_bool_sort(), true); recfun::promise_def connected = p.ensure_def(symbol(connected_sym), 3, dom, m.mk_bool_sort(), true);
connectedf = connected.get_def()->get_decl(); connectedf = connected.get_def()->get_decl();
var_ref AV(m.mk_var(2, listS), m); var_ref AV(m.mk_var(2, listS), m);
var_ref dstV(m.mk_var(1, s), m); var_ref dstV(m.mk_var(1, s), m);