Storing clause partitioning directly in Proof

Martin Blicha · Martin Blicha · commit 6bbfd2717abe · 2021-01-23T16:30:13.000+01:00
This cleans up Cnfizer a bit, because it does not need to know about the
partitioning anymore.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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); }

Original file line number	Diff line number	Diff line change
`@@ -165,6 +165,7 @@ sstat MainSolver::simplifyFormulas(char** err_msg)`
`165`	`165`	`}`
`166`	`166`	`assert(pmanager.getPartitionIndex(fla) != -1);`
`167`	`167`	`pmanager.propagatePartitionMask(fla);`
	`168`	`+ getSMTSolver().setPartition(pmanager.getPartitionIndex(fla));`
`168`	`169`	`status = giveToSolver(fla, frame.getId());`
`169`	`170`	`}`
`170`	`171`	`} else {`