Skip to content

Logic: Rewrite mkAnd/mkOr to avoid memory allocations and term lookup #504

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
blishko wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Logic: Rewrite mkAnd/mkOr to avoid memory allocations and term lookup #504

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
598602c
Logic: Rewrite mkAnd/mkOr to avoid term and memory allocations
May 27, 2022
83c4bbe
Logic: Use std::sort in *junction creation
Jun 3, 2022
f35c28e
Logic: Remove unnecessary check for corner case
Jun 3, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
102 changes: 38 additions & 64 deletions src/logics/Logic.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,18 @@

using namespace std;

namespace {
struct LessThanPTRefIgnoreNot {
Logic const & logic;
LessThanPTRefIgnoreNot(Logic & logic) : logic{logic} {}
bool operator() (PTRef first, PTRef second) {
auto firstVal = logic.isNot(first) ? logic.getPterm(first)[0].x : first.x;
auto secondVal = logic.isNot(second) ? logic.getPterm(second)[0].x : second.x;
return firstVal < secondVal;
}
};
}

/***********************************************************
* Class defining logic
***********************************************************/
Expand Down Expand Up @@ -428,91 +440,53 @@ Logic::mkIte(vec<PTRef>&& args)
// Check if arguments contain trues or a false and return the simplified
// term
PTRef Logic::mkAnd(vec<PTRef>&& args) {
if (args.size() == 0) { return getTerm_true(); }
// Remove duplicates
vec<PtAsgn> tmp_args;
tmp_args.capacity(args.size());
for (int i = 0; i < args.size(); i++) {
if (!hasSortBool(args[i])) {
return PTRef_Undef;
}
if (isNot(args[i])) {
tmp_args.push(PtAsgn(getPterm(args[i])[0], l_False));
} else {
tmp_args.push(PtAsgn(args[i], l_True));
}
}
std::sort(tmp_args.begin(), tmp_args.end(), LessThan_PtAsgn());
std::sort(args.begin(), args.end(), LessThanPTRefIgnoreNot(*this));
int i, j;
PtAsgn p = PtAsgn_Undef;
for (i = 0, j = 0; i < tmp_args.size(); i++) {
if (isFalse(tmp_args[i].tr)) {
assert(tmp_args[i].sgn == l_True);
return getTerm_false();
} else if (isTrue(tmp_args[i].tr)) { // skip
assert(tmp_args[i].sgn == l_True);
} else if (p == tmp_args[i]) { // skip
} else if (p.tr == tmp_args[i].tr && p.sgn != tmp_args[i].sgn) {
for (i = 0, j = 0; i < args.size(); i++) {
if (isFalse(args[i])) {
return getTerm_false();
} else if (isTrue(args[i])) { // skip
} else {
tmp_args[j++] = p = tmp_args[i];
PtAsgn arg = toPtAsgn(args[i]);
if (arg == p) { continue; }
if (arg.tr == p.tr) { assert(arg.sgn != p.sgn); return getTerm_false(); }
args[j++] = args[i];
p = arg;
}
}
tmp_args.shrink(i - j);
if (tmp_args.size() == 0) {
args.shrink(i - j);
if (args.size() == 0) {
return getTerm_true();
} else if (tmp_args.size() == 1) {
return tmp_args[0].sgn == l_True ? tmp_args[0].tr : mkNot(tmp_args[0].tr);
}
args.clear();
args.capacity(tmp_args.size());
for (PtAsgn tmp_arg : tmp_args) {
args.push(tmp_arg.sgn == l_True ? tmp_arg.tr : mkNot(tmp_arg.tr));
} else if (args.size() == 1) {
return args[0];
}
return mkFun(getSym_and(), std::move(args));
}

PTRef Logic::mkOr(vec<PTRef> && args) {
if (args.size() == 0) { return getTerm_false(); }
// Remove duplicates
vec<PtAsgn> tmp_args;
tmp_args.capacity(args.size());
for (int i = 0; i < args.size(); i++) {
if (!hasSortBool(args[i])) {
return PTRef_Undef;
}
if (isNot(args[i])) {
tmp_args.push(PtAsgn(getPterm(args[i])[0], l_False));
} else {
tmp_args.push(PtAsgn(args[i], l_True));
}
}
std::sort(tmp_args.begin(), tmp_args.end(), LessThan_PtAsgn());
std::sort(args.begin(), args.end(), LessThanPTRefIgnoreNot(*this));
int i, j;
PtAsgn p = PtAsgn_Undef;
for (i = 0, j = 0; i < tmp_args.size(); i++) {
if (isTrue(tmp_args[i].tr)) {
assert(tmp_args[i].sgn == l_True);
return getTerm_true();
} else if (isFalse(tmp_args[i].tr)) { // skip
assert(tmp_args[i].sgn == l_True);
} else if (p == tmp_args[i]) { // skip
} else if (p.tr == tmp_args[i].tr && p.sgn != tmp_args[i].sgn) {
for (i = 0, j = 0; i < args.size(); i++) {
if (isTrue(args[i])) {
return getTerm_true();
} else if (isFalse(args[i])) { // skip
} else {
tmp_args[j++] = p = tmp_args[i];
PtAsgn arg = toPtAsgn(args[i]);
if (arg == p) { continue; }
if (arg.tr == p.tr) { assert(arg.sgn != p.sgn); return getTerm_true(); }
args[j++] = args[i];
p = arg;
}
}
tmp_args.shrink(i - j);
if (tmp_args.size() == 0) {
args.shrink(i - j);
if (args.size() == 0) {
return getTerm_false();
} else if (tmp_args.size() == 1) {
return tmp_args[0].sgn == l_True ? tmp_args[0].tr : mkNot(tmp_args[0].tr);
}
args.clear();
args.capacity(tmp_args.size());
for (PtAsgn tmp_arg : tmp_args) {
args.push(tmp_arg.sgn == l_True ? tmp_arg.tr : mkNot(tmp_arg.tr));
} else if (args.size() == 1) {
return args[0];
}
return mkFun(getSym_or(), std::move(args));
}
Expand Down
2 changes: 2 additions & 0 deletions src/logics/Logic.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -238,6 +238,8 @@ class Logic {
bool isInternalSort(SRef) const;
void newUninterpretedSortHandler(SRef);

PtAsgn toPtAsgn(PTRef ref) const { return isNot(ref) ? PtAsgn(getPterm(ref)[0], l_False) : PtAsgn(ref, l_True); }

public:

// General disequalities
Expand Down