Adding support for reading wrong assumptions

[satlib.git] / glucose-syrup / core / Solver.h

diff --git a/glucose-syrup/core/Solver.h b/glucose-syrup/core/Solver.h
index 63d531615697437459ac5ec74c0b677617a1930f..b0cd3b004a90faa9d78eb12ceecec93900427051 100644 (file)
--- a/glucose-syrup/core/Solver.h
+++ b/glucose-syrup/core/Solver.h
@@ -135,6 +135,7 @@ public:
     int     nClauses   ()      const;       // The current number of original clauses.
     int     nLearnts   ()      const;       // The current number of learnt clauses.
     int     nVars      ()      const;       // The current number of variables.
     int     nClauses   ()      const;       // The current number of original clauses.
     int     nLearnts   ()      const;       // The current number of learnt clauses.
     int     nVars      ()      const;       // The current number of variables.

+    int     assumptionsSize      ()      const;       // The current number of variables.

     int     nFreeVars  ()      const;
 
     inline char valuePhase(Var v) {return polarity[v];}
     int     nFreeVars  ()      const;
 
     inline char valuePhase(Var v) {return polarity[v];}


@@ -477,6 +478,7 @@ inline int      Solver::nAssigns      ()      const   { return trail.size(); }
 inline int      Solver::nClauses      ()      const   { return clauses.size(); }
 inline int      Solver::nLearnts      ()      const   { return learnts.size(); }
 inline int      Solver::nVars         ()      const   { return vardata.size(); }
 inline int      Solver::nClauses      ()      const   { return clauses.size(); }
 inline int      Solver::nLearnts      ()      const   { return learnts.size(); }
 inline int      Solver::nVars         ()      const   { return vardata.size(); }

+inline int      Solver::assumptionsSize         ()      const   { return assumptions.size(); }

 inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
 inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
 inline void     Solver::setDecisionVar(Var v, bool b) 
 inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
 inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
 inline void     Solver::setDecisionVar(Var v, bool b)