From 052a8b7383363018d60e383bdda20a81b6ce7650 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= Date: Fri, 29 Apr 2022 18:40:10 +0200 Subject: [PATCH 1/6] TermMarker: add method to check if term is in domain --- src/logics/Logic.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/logics/Logic.h b/src/logics/Logic.h index b3430b2b6..04aee7424 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -92,6 +92,7 @@ class Logic { } 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; From ed525f50a988032179d5d730d6ec1ef0b4ede96a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= Date: Tue, 10 May 2022 11:37:46 +0200 Subject: [PATCH 2/6] NatSet: introduce a safe version --- src/common/NatSet.h | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/src/common/NatSet.h b/src/common/NatSet.h index 71ec6bcc5..d72e716c6 100644 --- a/src/common/NatSet.h +++ b/src/common/NatSet.h @@ -23,15 +23,12 @@ Revision History: #include #include - class nat_set { - unsigned m_curr_timestamp; + unsigned m_curr_timestamp = 0; std::vector 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); } @@ -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); @@ -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 From 9c23c7b01842cb1679991729ae9f1fcdd196a7ef Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= Date: Thu, 28 Apr 2022 19:05:40 +0200 Subject: [PATCH 3/6] Logic: Sort commutative Boolean operators --- src/logics/Logic.cc | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index 445d3e201..e3eb3cfbc 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -840,6 +840,11 @@ Logic::mkFun(SymRef sym, vec&& 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]; @@ -860,17 +865,13 @@ Logic::mkFun(SymRef sym, vec&& 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; @@ -882,8 +883,7 @@ Logic::mkFun(SymRef sym, vec&& 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 From e7fd88c1d7ec5d48d6f956af5ee20ced01ad81b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= Date: Tue, 10 May 2022 10:52:29 +0200 Subject: [PATCH 4/6] Logic: Add a private NatSet for nested use --- src/logics/Logic.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/logics/Logic.h b/src/logics/Logic.h index 04aee7424..8d76f30f9 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -95,6 +95,7 @@ class Logic { inline bool isInDomain(PTId id) const { return Idx(id) < innerSet.get_domain(); } }; mutable nat_set auxiliaryNatSet; + mutable nat_set privateNatSet; SSymRef sym_IndexedSort; @@ -197,6 +198,9 @@ class Logic { * Relies on a term invariant that id of a child is lower than id of a parent. */ 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 From d32290c3804bfdb40b8c0ece70edd17807ff0af0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= Date: Tue, 10 May 2022 11:31:40 +0200 Subject: [PATCH 5/6] Logic: use safe NatSet --- src/logics/Logic.h | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/logics/Logic.h b/src/logics/Logic.h index 8d76f30f9..cef24380d 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -84,18 +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 nat_set privateNatSet; + mutable SafeNatSet auxiliaryNatSet; + mutable SafeNatSet privateNatSet; SSymRef sym_IndexedSort; @@ -196,6 +199,8 @@ 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: From 2d54dc0347d7d9f068b334386fecd9a98255ad66 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= Date: Mon, 2 May 2022 19:38:12 +0200 Subject: [PATCH 6/6] Logic: Improve mkAnd and mkOr --- src/logics/Logic.cc | 107 ++++++++++++++++---------------------------- 1 file changed, 39 insertions(+), 68 deletions(-) diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index e3eb3cfbc..fe53503cd 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -427,47 +427,33 @@ Logic::mkIte(vec&& args) // Check if arguments contain trues or a false and return the simplified // term -PTRef Logic::mkAnd(vec&& args) { +PTRef Logic::mkAnd(vec && args) { if (args.size() == 0) { return getTerm_true(); } - // Remove duplicates - vec 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(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)); } @@ -475,44 +461,29 @@ PTRef Logic::mkAnd(vec&& args) { PTRef Logic::mkOr(vec && args) { if (args.size() == 0) { return getTerm_false(); } // Remove duplicates - vec 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(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); + for (i = j = 0; i < args.size(); i++) { + PTRef tr = args[i]; + if (isTrue(tr)) { 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) { - 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)); }