removing the now redundant parameter of CoreSMTSolver::addOriginalClause_

Author: Martin Blicha

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;
 }
 //

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,16 +299,16 @@ 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);
         for(Lit l : resolvedUnits) {
             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

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:
     //

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;
     }
 

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).