diff options
Diffstat (limited to 'src/sat/bsat/satSolver2.h')
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 4b1eec61..ffbae964 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <assert.h> #include "satVec.h" +#include "vecSet.h" ABC_NAMESPACE_HEADER_START @@ -112,16 +113,19 @@ struct sat_solver2_t veci clauses; // clause memory veci learnts; // learnt memory veci* wlists; // watcher lists (for each literal) + veci claActs; // clause activities + veci claProofs; // clause proofs int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) - int hClausePivot; // the pivot among problem clause - int hLearntPivot; // the pivot among learned clause - int iVarPivot; // the pivot among the variables - int iSimpPivot; // marker of unit-clauses int nof_learnts; // the number of clauses to trigger reduceDB - veci claActs; // clause activities - veci claProofs; // clause proofs + // rollback + int iVarPivot; // the pivot for variables + int iTrailPivot; // the pivot for trail + int iProofPivot; // the pivot for proof records + int hClausePivot; // the pivot for problem clause + int hLearntPivot; // the pivot for learned clause + int hProofPivot; // the pivot for proof records // internal state varinfo2 * vi; // variable information @@ -146,8 +150,8 @@ struct sat_solver2_t veci learnt_live; // remaining clauses after reduce DB // proof logging - veci proofs; // sequence of proof records - int iStartChain; // temporary variable to remember beginning of the current chain in proof logging + Vec_Set_t Proofs; // sequence of proof records + veci temp_proof; // temporary place to store proofs int nUnits; // the total number of unit clauses // statistics @@ -251,10 +255,12 @@ static inline int sat_solver2_set_learntmax(sat_solver2* s, int nLearntMax) static inline void sat_solver2_bookmark(sat_solver2* s) { assert( s->qhead == s->qtail ); - s->hLearntPivot = veci_size(&s->learnts); - s->hClausePivot = veci_size(&s->clauses); s->iVarPivot = s->size; - s->iSimpPivot = s->qhead; + s->iTrailPivot = s->qhead; + s->iProofPivot = Vec_SetEntryNum(&s->Proofs); + s->hClausePivot = veci_size(&s->clauses); + s->hLearntPivot = veci_size(&s->learnts); + s->hProofPivot = Vec_SetHandCurrent(&s->Proofs); } static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) |