Skip to content

Sort commutative boolean ops #491

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

Draft
aehyvari wants to merge 6 commits into
base: master
Choose a base branch
from
Draft

Sort commutative boolean ops #491

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
052a8b7
TermMarker: add method to check if term is in domain
aehyvari Apr 29, 2022
ed525f5
NatSet: introduce a safe version
aehyvari May 10, 2022
9c23c7b
Logic: Sort commutative Boolean operators
aehyvari Apr 28, 2022
e7fd88c
Logic: Add a private NatSet for nested use
aehyvari May 10, 2022
d32290c
Logic: use safe NatSet
aehyvari May 10, 2022
2d54dc0
Logic: Improve mkAnd and mkOr
aehyvari May 2, 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
25 changes: 19 additions & 6 deletions src/common/NatSet.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,15 +23,12 @@ Revision History:
#include <climits>
#include <vector>


class nat_set {
unsigned m_curr_timestamp;
unsigned m_curr_timestamp = 0;
std::vector<unsigned> m_timestamps;

public:
nat_set(unsigned s = 0):
m_curr_timestamp(0),
m_timestamps() {
nat_set(unsigned s = 0) {
if (s > 0) {
m_timestamps.resize(s, 0);
}
Expand Down Expand Up @@ -66,7 +63,7 @@ class nat_set {
m_timestamps[v] = m_curr_timestamp;
}

void reset() {
virtual void reset() {
m_curr_timestamp++;
if (m_curr_timestamp == UINT_MAX) {
std::fill(m_timestamps.begin(), m_timestamps.end(), 0);
Expand All @@ -85,4 +82,20 @@ class nat_set {
return true;
}
};

class SafeNatSet : public nat_set {
private:
bool inUse = false;
public:
void release() {
inUse = false;
}

void reset() override {
assert(not inUse);
nat_set::reset();
inUse = true;
}
};

#endif //OPENSMT_NATSET_H
125 changes: 48 additions & 77 deletions src/logics/Logic.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -427,92 +427,63 @@ Logic::mkIte(vec<PTRef>&& args)

// Check if arguments contain trues or a false and return the simplified
// term
PTRef Logic::mkAnd(vec<PTRef>&& args) {
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());
// Remove duplicates and simplify
assert(getNumberOfTerms() > 0);
TermMarks tm = getPrivateTermMarks(PTId{static_cast<uint32_t>(getNumberOfTerms()-1)});
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 = j = 0; i < args.size(); i++) {
PTRef tr = args[i];
if (isTrue(tr)) {
continue;
} else if (isFalse(tr)) {
return getTerm_false();
} else {
tmp_args[j++] = p = tmp_args[i];
} else if (not tm.isMarked(getPterm(tr).getId())) {
// Check if the atom appears negated in the clause
PTId negatedId = getPterm(mkNot(tr)).getId();
if (tm.isInDomain(negatedId) and tm.isMarked(negatedId)) {
return getTerm_false();
}
args[j++] = args[i];
tm.mark(getPterm(tr).getId());
}
}
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());
assert(getNumberOfTerms() > 0);
TermMarks tm = getPrivateTermMarks(PTId{static_cast<uint32_t>(getNumberOfTerms()-1)});
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 = j = 0; i < args.size(); i++) {
PTRef tr = args[i];
if (isTrue(tr)) {
return getTerm_true();
} else {
tmp_args[j++] = p = tmp_args[i];
} else if (isFalse(tr)) {
continue;
} else if (not tm.isMarked(getPterm(tr).getId())) {
PTId negatedId = getPterm(mkNot(tr)).getId();
if (tm.isInDomain(negatedId) and tm.isMarked(negatedId)) {
return getTerm_true(); // A tautology
}
args[j++] = args[i];
tm.mark(getPterm(tr).getId());
}
}
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 Expand Up @@ -840,6 +811,11 @@ Logic::mkFun(SymRef sym, vec<PTRef>&& terms)
#endif

PTRef res = PTRef_Undef;

if (sym_store[sym].commutes()) {
termSort(terms);
}

if (terms.size() == 0) {
if (term_store.hasCtermKey(sym)) //cterm_map.contains(sym))
res = term_store.getFromCtermMap(sym); //cterm_map[sym];
Expand All @@ -860,17 +836,13 @@ Logic::mkFun(SymRef sym, vec<PTRef>&& terms)
PTLKey k;
k.sym = sym;
terms.moveTo(k.args);
if (sym_store[sym].commutes()) {
termSort(k.args);
}
if (term_store.hasCplxKey(k))
if (term_store.hasCplxKey(k)) {
res = term_store.getFromCplxMap(k);
else {
} else {
res = term_store.newTerm(sym, k.args);
term_store.addToCplxMap(std::move(k), res);
}
}
else {
} else {
// Boolean operator
PTLKey k;
k.sym = sym;
Expand All @@ -882,8 +854,7 @@ Logic::mkFun(SymRef sym, vec<PTRef>&& terms)
cerr << "duplicate: " << ts << endl;
::free(ts);
#endif
}
else {
} else {
res = term_store.newTerm(sym, k.args);
term_store.addToBoolMap(std::move(k), res);
#ifdef SIMPLIFY_DEBUG
Expand Down
16 changes: 13 additions & 3 deletions src/logics/Logic.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,16 +84,21 @@ class Logic {
PtStore term_store;

class TermMarks {
nat_set & innerSet;
SafeNatSet & innerSet;
public:
TermMarks(nat_set & innerSet, unsigned int domainSize) : innerSet(innerSet){
TermMarks(SafeNatSet & innerSet, unsigned int domainSize) : innerSet(innerSet) {
innerSet.assure_domain(domainSize);
innerSet.reset();
}
~TermMarks() {
innerSet.release();
}
inline void mark(PTId id) { innerSet.insert(Idx(id)); }
inline bool isMarked(PTId id) const { return innerSet.contains(Idx(id)); }
inline bool isInDomain(PTId id) const { return Idx(id) < innerSet.get_domain(); }
};
mutable nat_set auxiliaryNatSet;
mutable SafeNatSet auxiliaryNatSet;
mutable SafeNatSet privateNatSet;

SSymRef sym_IndexedSort;

Expand Down Expand Up @@ -194,8 +199,13 @@ class Logic {
* Provides an efficient data structure for representing a set of terms through "marking".
*
* Relies on a term invariant that id of a child is lower than id of a parent.
*
* Do not use recursively.
*/
TermMarks getTermMarks(PTId maxTermId) const { return TermMarks(auxiliaryNatSet, Idx(maxTermId) + 1); }
private:
TermMarks getPrivateTermMarks(PTId maxTermId) const { return TermMarks(privateNatSet, Idx(maxTermId) + 1); }
public:
// Default values for the logic

// Deprecated! Use getDefaultValuePTRef instead
Expand Down