minisat.h.patch

diff -Naur minisat/minisat/core/Solver.h minisat-mod/minisat/core/Solver.h
--- minisat/minisat/core/Solver.h	2018-09-10 15:01:12.898158196 +0200
+++ minisat-mod/minisat/core/Solver.h	2018-09-10 15:38:58.349220610 +0200
@@ -56,6 +56,12 @@
     bool    addClause_(      vec<Lit>& ps);                     // Add a clause to the solver without making superflous internal copy. Will
                                                                 // change the passed vector 'ps'.
 
+    // Portfolio support
+    void (*learnedClsCallback)(const vec<Lit>&, void* issuer);  // callback for clause learning
+    void *issuer;                                               // used as the callback parameter
+    void addLearnedClause(const vec<Lit>& cls);                 // add a learned clause by hand
+    int  lastDecision;                                          // the last decision made by the solver
+
     // Solving:
     //
     bool    simplify     ();                        // Removes already satisfied clauses.
@@ -300,6 +306,13 @@
 //=================================================================================================
 // Implementation of inline methods:
 
+inline void Solver::addLearnedClause(const vec<Lit>& cls) {
+    CRef cr = ca.alloc(cls, true);
+    learnts.push(cr);
+    attachClause(cr);
+    claBumpActivity(ca[cr]);
+}
+
 inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
 inline int  Solver::level (Var x) const { return vardata[x].level; }