Remove unnecessary includes from minisat component

usi-verification-and-security · Aug 7, 2024 · 8a15f5d · 8a15f5d
1 parent 17c6040
commit 8a15f5d
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 15 deletions.
diff --git a/src/minisat/core/SolverTypes.h b/src/minisat/core/SolverTypes.h
@@ -22,16 +22,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_SolverTypes_h
 #define Minisat_SolverTypes_h
 
-#include <assert.h>
-
-#include "osmtinttypes.h"
 #include "Alg.h"
 #include "Vec.h"
 #include "Map.h"
 #include "Alloc.h"
-#include "TypeUtils.h"
-
 
+#include <cassert>
 //=================================================================================================
 // Variables, literals, lifted booleans, clauses:
 
@@ -234,10 +230,9 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::moveTo(to); }
 
     template<class Lits>
-    CRef alloc(const Lits& ps, opensmt::pair<bool,uint32_t> learntAndGlue = {false, 0}) {
+    CRef alloc(const Lits& ps, bool learnt = false, uint32_t glue = 0) {
         assert(sizeof(Lit)      == sizeof(uint32_t));
         assert(sizeof(float)    == sizeof(uint32_t));
-        auto [learnt, glue] = learntAndGlue;
         bool use_extra = learnt | extra_clause_field;
 
         CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
@@ -267,7 +262,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
 
         if (c.reloced()) { cr = c.relocation(); return; }
 
-        cr = to.alloc(c, {c.learnt(), c.getGlue()});
+        cr = to.alloc(c, c.learnt(), c.getGlue());
         c.relocate(cr);
 
         // Copy extra data-fields:

diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc
@@ -682,7 +682,7 @@ void CoreSMTSolver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
             }
             else
             {
-                ctr = config.sat_temporary_learn ? ca.alloc(r, {true, computeGlue(r)}) : ca.alloc(r);
+                ctr = config.sat_temporary_learn ? ca.alloc(r, true, computeGlue(r)) : ca.alloc(r);
                 learnts.push(ctr);
                 attachClause(ctr);
                 undo_stack.push(undo_stack_el(undo_stack_el::NEWLEARNT, ctr));
@@ -860,7 +860,7 @@ bool CoreSMTSolver::litRedundant(Lit p, uint32_t abstract_levels)
             }
             else
             {
-                ct = config.sat_temporary_learn ? ca.alloc(r, {true, computeGlue(r)}) : ca.alloc(r);
+                ct = config.sat_temporary_learn ? ca.alloc(r, true, computeGlue(r)) : ca.alloc(r);
                 learnts.push(ct);
                 if (config.isIncremental() != 0)
                     undo_stack.push(undo_stack_el(undo_stack_el::NEWLEARNT, ct));
@@ -1477,7 +1477,7 @@ lbool CoreSMTSolver::search(int nof_conflicts)
                 learnts_size += learnt_clause.size( );
                 all_learnts ++;
 
-                CRef cr = ca.alloc(learnt_clause, {true, computeGlue(learnt_clause)});
+                CRef cr = ca.alloc(learnt_clause, true, computeGlue(learnt_clause));
 
                 if (logsResolutionProof()) {
                     resolutionProof->endChain(cr);

diff --git a/src/smtsolvers/LookaheadSMTSolver.cc b/src/smtsolvers/LookaheadSMTSolver.cc
@@ -92,7 +92,7 @@ lbool LookaheadSMTSolver::laPropagateWrapper() {
                 if (logsResolutionProof()) { resolutionProof->endChain(unitClause); }
                 uncheckedEnqueue(out_learnt[0], unitClause);
             } else {
-                CRef crd = ca.alloc(out_learnt, {true, computeGlue(out_learnt)});
+                CRef crd = ca.alloc(out_learnt, true, computeGlue(out_learnt));
                 if (logsResolutionProof()) { resolutionProof->endChain(crd); }
                 learnts.push(crd);
                 attachClause(crd);

diff --git a/src/smtsolvers/TheoryIF.cc b/src/smtsolvers/TheoryIF.cc
@@ -235,7 +235,7 @@ CoreSMTSolver::handleUnsat()
     {
         if (logsResolutionProof()) {
             // All conflicting atoms are dec-level 0
-            CRef confl = config.sat_temporary_learn ? ca.alloc(conflicting, {true, computeGlue(conflicting)}) : ca.alloc(conflicting);
+            CRef confl = config.sat_temporary_learn ? ca.alloc(conflicting, true, computeGlue(conflicting)) : ca.alloc(conflicting);
             resolutionProof->newTheoryClause(confl);
             this->finalizeResolutionProof(confl);
         }
@@ -253,7 +253,7 @@ CoreSMTSolver::handleUnsat()
     }
     // Learn theory lemma
     else {
-        confl = config.sat_temporary_learn ? ca.alloc(conflicting, {true, computeGlue(conflicting)}) : ca.alloc(conflicting);
+        confl = config.sat_temporary_learn ? ca.alloc(conflicting, true, computeGlue(conflicting)) : ca.alloc(conflicting);
         learnts.push(confl);
         attachClause(confl);
         claBumpActivity(ca[confl]);
@@ -294,7 +294,7 @@ CoreSMTSolver::handleUnsat()
         learnts_size += learnt_clause.size( );
         all_learnts ++;
 
-        CRef cr = ca.alloc(learnt_clause, {true, computeGlue(learnt_clause)});
+        CRef cr = ca.alloc(learnt_clause, true, computeGlue(learnt_clause));
 
         if (logsResolutionProof()) {
             resolutionProof->endChain(cr);