From 5ec2b1d5740533f7cc3b94cc3e0fdff73b9bd315 Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@usi.ch>
Date: Sat, 23 Jan 2021 16:28:01 +0100
Subject: [PATCH 1/2] Storing clause partitioning directly in Proof

This cleans up Cnfizer a bit, because it does not need to know about the
partitioning anymore.
---
 src/api/MainSolver.cc           |  1 +
 src/api/MainSolver.h            |  2 +-
 src/api/PartitionManager.cc     |  6 ------
 src/api/PartitionManager.h      |  4 ----
 src/cnfizers/Cnfizer.cc         | 19 -------------------
 src/cnfizers/Cnfizer.h          |  6 ------
 src/cnfizers/Tseitin.h          |  2 --
 src/common/PartitionInfo.cc     |  8 --------
 src/common/PartitionInfo.h      |  3 ---
 src/proof/PGBuild.cc            |  2 +-
 src/smtsolvers/CoreSMTSolver.cc |  6 ++++++
 src/smtsolvers/CoreSMTSolver.h  |  1 +
 src/smtsolvers/Proof.cc         |  8 ++++++++
 src/smtsolvers/Proof.h          |  8 +++++++-
 14 files changed, 25 insertions(+), 51 deletions(-)

diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc
index 93f1f8e2b..dd65cda5e 100644
--- a/src/api/MainSolver.cc
+++ b/src/api/MainSolver.cc
@@ -165,6 +165,7 @@ sstat MainSolver::simplifyFormulas(char** err_msg)
                 }
                 assert(pmanager.getPartitionIndex(fla) != -1);
                 pmanager.propagatePartitionMask(fla);
+                getSMTSolver().setPartition(pmanager.getPartitionIndex(fla));
                 status = giveToSolver(fla, frame.getId());
             }
         } else {
diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h
index b58bc1290..7bf463d6a 100644
--- a/src/api/MainSolver.h
+++ b/src/api/MainSolver.h
@@ -166,7 +166,7 @@ class MainSolver
         pmanager(logic),
         config(conf),
         pfstore(getTheory().pfstore),
-        ts( config, logic, pmanager, term_mapper, *smt_solver ),
+        ts( config, logic, term_mapper, *smt_solver ),
         solver_name {std::move(name)},
         check_called(0),
         status(s_Undef),
diff --git a/src/api/PartitionManager.cc b/src/api/PartitionManager.cc
index f78dc5162..18019590b 100644
--- a/src/api/PartitionManager.cc
+++ b/src/api/PartitionManager.cc
@@ -69,12 +69,6 @@ PartitionManager::getPartition(const ipartitions_t& mask, PartitionManager::part
     return A;
 }
 
-void
-PartitionManager::addClauseClassMask(CRef c, const ipartitions_t& toadd)
-{
-    partitionInfo.addClausePartition(c, toadd);
-}
-
 void
 PartitionManager::invalidatePartitions(const ipartitions_t& toinvalidate) {
     partitionInfo.invalidatePartitions(toinvalidate);
diff --git a/src/api/PartitionManager.h b/src/api/PartitionManager.h
index e7266b9f2..ec8177783 100644
--- a/src/api/PartitionManager.h
+++ b/src/api/PartitionManager.h
@@ -42,10 +42,6 @@ class PartitionManager {
 
     ipartitions_t computeAllowedPartitions(PTRef p);
 
-    const ipartitions_t & getClauseClassMask(CRef c) const { return partitionInfo.getClausePartitions(c); }
-
-    void addClauseClassMask(CRef c, const ipartitions_t & toadd);
-
     void invalidatePartitions(const ipartitions_t & toinvalidate);
 
     inline std::vector<PTRef> getPartitions() { return partitionInfo.getTopLevelFormulas(); }
diff --git a/src/cnfizers/Cnfizer.cc b/src/cnfizers/Cnfizer.cc
index f3b58273a..8afde6c5b 100644
--- a/src/cnfizers/Cnfizer.cc
+++ b/src/cnfizers/Cnfizer.cc
@@ -33,14 +33,12 @@ using namespace std;
 
 Cnfizer::Cnfizer ( SMTConfig       &config_
                    , Logic         &logic_
-                   , PartitionManager &pmanager_
                    , TermMapper    &tmap
                    , SimpSMTSolver &solver_
                  ) :
       solver   (solver_)
     , config   (config_  )
     , logic    (logic_)
-    , pmanager (pmanager_)
     , tmap     (tmap)
     , s_empty  (true)
     , alreadyAsserted(logic.getTerm_true())
@@ -52,7 +50,6 @@ Cnfizer::Cnfizer ( SMTConfig       &config_
 void Cnfizer::initialize()
 {
     // TODO: MB: why is all this initialization necessary?
-    currentPartition = 0;
     vec<Lit> c;
     Lit l = this->getOrCreateLiteralFor (logic.getTerm_true());
     c.push (l);
@@ -61,7 +58,6 @@ void Cnfizer::initialize()
     l = this->getOrCreateLiteralFor (logic.getTerm_false());
     c.push (~l);
     addClause(c);
-    currentPartition = -1;
 }
 
 lbool
@@ -148,11 +144,6 @@ lbool Cnfizer::cnfizeAndGiveToSolver(PTRef formula, FrameId frame_id)
 #ifdef PEDANTIC_DEBUG
     cerr << "cnfizerAndGiveToSolver: " << logic.printTerm (formula) << endl;
 #endif
-
-    if (keepPartitionInfo()) {
-        assert(pmanager.getPartitionIndex(formula) != -1);
-        currentPartition = pmanager.getPartitionIndex(formula);
-    }
     vec<PTRef> top_level_formulae;
     // Retrieve top-level formulae - this is a list constructed from a conjunction
     retrieveTopLevelFormulae (formula, top_level_formulae);
@@ -214,7 +205,6 @@ lbool Cnfizer::cnfizeAndGiveToSolver(PTRef formula, FrameId frame_id)
         declareVars(logic.propFormulasAppearingInUF);
     }
 
-    currentPartition = -1;
     return res == false ? l_False : l_Undef;
 }
 
@@ -442,15 +432,6 @@ bool Cnfizer::addClause(const vec<Lit> & c_in)
 #endif
     opensmt::pair<CRef, CRef> iorefs{CRef_Undef, CRef_Undef};
     bool res = solver.addOriginalSMTClause(c, iorefs);
-    if (keepPartitionInfo()) {
-        CRef ref = iorefs.first;
-        if (ref != CRef_Undef) {
-            ipartitions_t parts = 0;
-            assert(currentPartition != -1);
-            setbit(parts, static_cast<unsigned int>(currentPartition));
-            pmanager.addClauseClassMask(ref, parts);
-        }
-    }
     return res;
 }
 //
diff --git a/src/cnfizers/Cnfizer.h b/src/cnfizers/Cnfizer.h
index 1cb1af5d1..33f7cfab9 100644
--- a/src/cnfizers/Cnfizer.h
+++ b/src/cnfizers/Cnfizer.h
@@ -30,13 +30,11 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #include "Global.h"
 #include "Theory.h"
 #include "Logic.h"
-#include "PartitionManager.h"
 #include "TermMapper.h"
 
 #include <unordered_set>
 
 class SimpSMTSolver;
-class CnfState;
 class THandler;
 struct SMTConfig;
 
@@ -50,7 +48,6 @@ class Cnfizer
 protected:
     SMTConfig&          config;
     Logic&              logic;
-    PartitionManager&   pmanager;
     TermMapper&         tmap;
     bool                s_empty;
 
@@ -70,7 +67,6 @@ class Cnfizer
 
     Cnfizer( SMTConfig &    config_
            , Logic&        logic_
-           , PartitionManager& pmanager_
            , TermMapper&    tmap_
            , SimpSMTSolver& solver_
            );
@@ -121,8 +117,6 @@ class Cnfizer
 
     bool keepPartitionInfo() const { return config.produce_inter(); }
 
-    int currentPartition = -1;
-
     PTRef frame_term;
     vec<PTRef> frame_terms;
     void setFrameTerm(FrameId frame_id);
diff --git a/src/cnfizers/Tseitin.h b/src/cnfizers/Tseitin.h
index ee7c4a9d9..8add4dddb 100644
--- a/src/cnfizers/Tseitin.h
+++ b/src/cnfizers/Tseitin.h
@@ -37,13 +37,11 @@ class Tseitin : public Cnfizer
 
     Tseitin( SMTConfig&     config_
            , Logic&         logic_
-           , PartitionManager &pmanager_
            , TermMapper&    tmap_
            , SimpSMTSolver& solver_
            )
       : Cnfizer( config_
                 , logic_
-                , pmanager_
                 , tmap_
                 , solver_ )
         , alreadyCnfized(logic_.getTerm_true())
diff --git a/src/common/PartitionInfo.cc b/src/common/PartitionInfo.cc
index 1edbe816b..9d0314936 100644
--- a/src/common/PartitionInfo.cc
+++ b/src/common/PartitionInfo.cc
@@ -35,14 +35,6 @@ PartitionInfo::addIPartitions(SymRef _s, const ipartitions_t& _p) {
     sym_partitions[_s] |= _p;
 }
 
-const ipartitions_t & PartitionInfo::getClausePartitions(CRef c) const {
-    return clause_class.at(c);
-}
-
-void PartitionInfo::addClausePartition(CRef c, const ipartitions_t & p) {
-//    opensmt::orbit(clause_class[c], clause_class[c], p);
-    clause_class[c] |= p;
-}
 
 void PartitionInfo::invalidatePartitions(const ipartitions_t& toinvalidate) {
     auto negated = ~toinvalidate;
diff --git a/src/common/PartitionInfo.h b/src/common/PartitionInfo.h
index d9b5f6f38..b99ebc70e 100644
--- a/src/common/PartitionInfo.h
+++ b/src/common/PartitionInfo.h
@@ -17,7 +17,6 @@
 class PartitionInfo {
     std::unordered_map<SymRef, ipartitions_t, SymRefHash> sym_partitions;
     std::unordered_map<PTRef, ipartitions_t, PTRefHash> term_partitions;
-    std::unordered_map<CRef, ipartitions_t> clause_class;
     FlaPartitionMap flaPartitionMap;
 
 public:
@@ -26,8 +25,6 @@ class PartitionInfo {
     void addIPartitions(PTRef t, const ipartitions_t& p);
     ipartitions_t& getIPartitions(SymRef _s);
     void addIPartitions(SymRef s, const ipartitions_t& p);
-    const ipartitions_t& getClausePartitions(CRef) const;
-    void addClausePartition(CRef c, const ipartitions_t& p);
 
     inline std::vector<PTRef> getTopLevelFormulas() const { return flaPartitionMap.get_top_level_flas(); }
     inline unsigned int getNoOfPartitions() const {return flaPartitionMap.getNoOfPartitions(); }
diff --git a/src/proof/PGBuild.cc b/src/proof/PGBuild.cc
index 76b9f8b8f..ccbb23b7b 100644
--- a/src/proof/PGBuild.cc
+++ b/src/proof/PGBuild.cc
@@ -238,7 +238,7 @@ void ProofGraph::buildProofGraph( int nVars )
                     if (_ctype == clause_type::CLA_ORIG) {
                         n->initClause(proof.getClause(clause));
                         n->setClauseRef(clause);
-                        n->setInterpPartitionMask(pmanager.getClauseClassMask(clause));
+                        n->setInterpPartitionMask(proof.getClauseClassMask(clause));
                         //Sort clause literals
                         std::sort(n->getClause().begin(),n->getClause().end());
                         if (n->getClauseSize() >= max_leaf_size) {
diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc
index 9f8e5a186..270ccdacd 100644
--- a/src/smtsolvers/CoreSMTSolver.cc
+++ b/src/smtsolvers/CoreSMTSolver.cc
@@ -1044,6 +1044,12 @@ void CoreSMTSolver::finalizeProof(CRef finalConflict) {
     proof->endChain(CRef_Undef);
 }
 
+void CoreSMTSolver::setPartition(std::size_t partitionIndex) {
+    if (proof) {
+        proof->setPartition(partitionIndex);
+    }
+}
+
 /*_________________________________________________________________________________________________
   |
   |  analyzeFinal : (p : Lit)  ->  [void]
diff --git a/src/smtsolvers/CoreSMTSolver.h b/src/smtsolvers/CoreSMTSolver.h
index 049978a09..e566e3ba5 100644
--- a/src/smtsolvers/CoreSMTSolver.h
+++ b/src/smtsolvers/CoreSMTSolver.h
@@ -755,6 +755,7 @@ class CoreSMTSolver
 public:
 
     void    printTrace() const;
+    void    setPartition(std::size_t partitionIndex);
 
 protected:
     virtual inline void clausesPublish() {};
diff --git a/src/smtsolvers/Proof.cc b/src/smtsolvers/Proof.cc
index 65cb0203b..d151c1e22 100644
--- a/src/smtsolvers/Proof.cc
+++ b/src/smtsolvers/Proof.cc
@@ -35,6 +35,14 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
   , cl_al		( cl )
 { }
 
+void Proof::newOriginalClause(CRef c) {
+    assert(currentPartition != static_cast<std::size_t>(-1));
+    newLeafClause(c, clause_type::CLA_ORIG);
+    ipartitions_t partition = 0;
+    setbit(partition, currentPartition);
+    clause_class[c] |= partition;
+}
+
 void Proof::newLeafClause(CRef c, clause_type t)
 {
     assert(c != CRef_Undef);
diff --git a/src/smtsolvers/Proof.h b/src/smtsolvers/Proof.h
index 8add9421a..b994db68e 100644
--- a/src/smtsolvers/Proof.h
+++ b/src/smtsolvers/Proof.h
@@ -89,14 +89,20 @@ class Proof
     std::unordered_map< CRef, ProofDer>     clause_to_proof_der;
     ClauseAllocator&            cl_al;
     std::unordered_map<Lit, CRef, LitHash> assumed_literals;
+    std::unordered_map<CRef, ipartitions_t> clause_class;
+    std::size_t currentPartition = 0;
 
 public:
 
     Proof ( ClauseAllocator& cl );
     ~Proof( ) = default;
 
+    void setPartition(std::size_t partition) { currentPartition = partition; }
+
+    ipartitions_t getClauseClassMask(CRef c) const { assert(clause_class.count(c) != 0); return clause_class.at(c); }
+
     // Notifies the proof about a new original clause.
-    void newOriginalClause(CRef c) { newLeafClause(c, clause_type::CLA_ORIG); }
+    void newOriginalClause(CRef c);
 
     // Notifies the proof about a new T-clause.
     void newTheoryClause(CRef c) { newLeafClause(c, clause_type::CLA_THEORY); }

From 6806db73e2023b5a4e2254ba048689c98fed6ead Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@usi.ch>
Date: Sat, 23 Jan 2021 16:48:25 +0100
Subject: [PATCH 2/2] removing the now redundant parameter of
 CoreSMTSolver::addOriginalClause_

---
 src/cnfizers/Cnfizer.cc         |  3 +--
 src/smtsolvers/CoreSMTSolver.cc | 19 +++++--------------
 src/smtsolvers/CoreSMTSolver.h  |  1 -
 src/smtsolvers/SimpSMTSolver.cc | 11 ++++-------
 src/smtsolvers/SimpSMTSolver.h  |  2 +-
 5 files changed, 11 insertions(+), 25 deletions(-)

diff --git a/src/cnfizers/Cnfizer.cc b/src/cnfizers/Cnfizer.cc
index 8afde6c5b..77316d604 100644
--- a/src/cnfizers/Cnfizer.cc
+++ b/src/cnfizers/Cnfizer.cc
@@ -430,8 +430,7 @@ bool Cnfizer::addClause(const vec<Lit> & c_in)
     }
 
 #endif
-    opensmt::pair<CRef, CRef> iorefs{CRef_Undef, CRef_Undef};
-    bool res = solver.addOriginalSMTClause(c, iorefs);
+    bool res = solver.addOriginalSMTClause(c);
     return res;
 }
 //
diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc
index 270ccdacd..3ce2b7a7c 100644
--- a/src/smtsolvers/CoreSMTSolver.cc
+++ b/src/smtsolvers/CoreSMTSolver.cc
@@ -269,17 +269,9 @@ Var CoreSMTSolver::newVar(bool sign, bool dvar)
     return v;
 }
 
-
 bool CoreSMTSolver::addOriginalClause_(const vec<Lit> & _ps)
-{
-    opensmt::pair<CRef, CRef> fake;
-    return addOriginalClause_(_ps, fake);
-}
-
-bool CoreSMTSolver::addOriginalClause_(const vec<Lit> & _ps, opensmt::pair<CRef, CRef> & inOutCRefs)
 {
     assert(decisionLevel() == 0);
-    inOutCRefs = {CRef_Undef, CRef_Undef};
     if (!isOK()) { return false; }
     bool logsProofForInterpolation = this->logsProofForInterpolation();
     vec<Lit> ps;
@@ -307,6 +299,7 @@ bool CoreSMTSolver::addOriginalClause_(const vec<Lit> & _ps, opensmt::pair<CRef,
         }
     }
     ps.shrink(i - j);
+    CRef clauseToInsert = CRef_Undef;
     if (logsProofForInterpolation) {
         vec<Lit> original;
         ps.copyTo(original);
@@ -314,9 +307,8 @@ bool CoreSMTSolver::addOriginalClause_(const vec<Lit> & _ps, opensmt::pair<CRef,
             original.push(l);
         }
         CRef inputClause = ca.alloc(original, false);
-        CRef outputClause = resolvedUnits.empty() ? inputClause :
+        clauseToInsert = resolvedUnits.empty() ? inputClause :
                 ps.size() == 0 ? CRef_Undef : ca.alloc(ps, false);
-        inOutCRefs = {inputClause, outputClause};
         proof->newOriginalClause(inputClause);
         if (!resolvedUnits.empty()) {
             proof->beginChain( inputClause );
@@ -325,7 +317,7 @@ bool CoreSMTSolver::addOriginalClause_(const vec<Lit> & _ps, opensmt::pair<CRef,
                 assert(reason(v) != CRef_Undef);
                 proof->addResolutionStep(reason(v), v);
             }
-            proof->endChain(outputClause);
+            proof->endChain(clauseToInsert);
         }
     }
     if (ps.size() == 0) {
@@ -334,7 +326,7 @@ bool CoreSMTSolver::addOriginalClause_(const vec<Lit> & _ps, opensmt::pair<CRef,
     if (ps.size() == 1)
     {
         assert(value(ps[0]) == l_Undef);
-        CRef reasonForAssignment = inOutCRefs.second;
+        CRef reasonForAssignment = clauseToInsert;
         assert((logsProofForInterpolation && reasonForAssignment != CRef_Undef) || (!logsProofForInterpolation && reasonForAssignment == CRef_Undef));
         uncheckedEnqueue(ps[0], reasonForAssignment);
         CRef confl = propagate();
@@ -343,8 +335,7 @@ bool CoreSMTSolver::addOriginalClause_(const vec<Lit> & _ps, opensmt::pair<CRef,
     }
     else
     {
-        CRef clauseToAttach = logsProofForInterpolation ? inOutCRefs.second : ca.alloc(ps, false);
-        inOutCRefs.second = clauseToAttach;
+        CRef clauseToAttach = logsProofForInterpolation ? clauseToInsert : ca.alloc(ps, false);
         clauses.push(clauseToAttach);
         attachClause(clauseToAttach);
         // MB: TODO: remove this undo_stack
diff --git a/src/smtsolvers/CoreSMTSolver.h b/src/smtsolvers/CoreSMTSolver.h
index e566e3ba5..cc6346fa6 100644
--- a/src/smtsolvers/CoreSMTSolver.h
+++ b/src/smtsolvers/CoreSMTSolver.h
@@ -255,7 +255,6 @@ class CoreSMTSolver
     bool    addOriginalClause(Lit p, Lit q, Lit r);                    // Add a ternary clause to the solver.
 protected:
     bool addOriginalClause_(const vec<Lit> & _ps);                                          // Add a clause to the solver
-    bool addOriginalClause_(const vec<Lit> & _ps, opensmt::pair<CRef, CRef> & inOutCRefs);  // Add a clause to the solver without making superflous internal copy. Will change the passed vector 'ps'.  Write the new clause to cr
 public:
     // Solving:
     //
diff --git a/src/smtsolvers/SimpSMTSolver.cc b/src/smtsolvers/SimpSMTSolver.cc
index 4eb15fdf2..0112906a2 100644
--- a/src/smtsolvers/SimpSMTSolver.cc
+++ b/src/smtsolvers/SimpSMTSolver.cc
@@ -184,9 +184,8 @@ lbool SimpSMTSolver::solve_(bool do_simp, bool turn_off_simp)
 //=================================================================================================
 // Added code
 
-bool SimpSMTSolver::addOriginalSMTClause(const vec<Lit> & smt_clause, opensmt::pair<CRef, CRef> & inOutCRefs)
+bool SimpSMTSolver::addOriginalSMTClause(const vec<Lit> & smt_clause)
 {
-    inOutCRefs = {CRef_Undef, CRef_Undef};
     assert( config.sat_preprocess_theory == 0 );
 
     // Check that the variables exist in the solver
@@ -213,7 +212,7 @@ bool SimpSMTSolver::addOriginalSMTClause(const vec<Lit> & smt_clause, opensmt::p
         cerr << "XXX skipped handling of unary theory literal?" << endl;
     }
     int nclauses = clauses.size();
-    if (!CoreSMTSolver::addOriginalClause_(smt_clause, inOutCRefs))
+    if (!CoreSMTSolver::addOriginalClause_(smt_clause))
         return false;
 
     if (use_simplification && clauses.size() == nclauses + 1)
@@ -622,8 +621,7 @@ bool SimpSMTSolver::eliminateVar(Var v)
     vec<Lit>& resolvent = add_tmp;
     for (int i = 0; i < pos.size(); i++) {
         for (int j = 0; j < neg.size(); j++) {
-            opensmt::pair<CRef,CRef> dummy {CRef_Undef, CRef_Undef};
-            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addOriginalSMTClause(resolvent, dummy))
+            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addOriginalSMTClause(resolvent))
                 return false;
         }
     }
@@ -665,8 +663,7 @@ bool SimpSMTSolver::substitute(Var v, Lit x)
 
         removeClause(cls[i]);
 
-        opensmt::pair<CRef,CRef> dummy {CRef_Undef, CRef_Undef};
-        if (!addOriginalSMTClause(subst_clause, dummy))
+        if (!addOriginalSMTClause(subst_clause))
             return ok = false;
     }
 
diff --git a/src/smtsolvers/SimpSMTSolver.h b/src/smtsolvers/SimpSMTSolver.h
index 430699542..78ec5f392 100644
--- a/src/smtsolvers/SimpSMTSolver.h
+++ b/src/smtsolvers/SimpSMTSolver.h
@@ -63,7 +63,7 @@ class SimpSMTSolver : public CoreSMTSolver
     //
     Var     newVar    (bool polarity = true, bool dvar = true) override;
 
-    bool addOriginalSMTClause(const vec<Lit> & smt_clause, opensmt::pair<CRef, CRef> & inOutCRefs);
+    bool addOriginalSMTClause(const vec<Lit> & smt_clause);
 public:
 
     bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).