From c25f5dee05c24c146680c555176b827d0008a444 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 27 Aug 2012 13:49:53 -0700
Subject: Bug fix in &gla.

---
 src/sat/bsat/satProof2.h  |  1 +
 src/sat/bsat/satSolver2.c | 15 ++++++++++++---
 src/sat/bsat/satSolver2.h |  5 +++--
 3 files changed, 16 insertions(+), 5 deletions(-)

(limited to 'src/sat')

diff --git a/src/sat/bsat/satProof2.h b/src/sat/bsat/satProof2.h
index 25ad0d07..b82d9590 100644
--- a/src/sat/bsat/satProof2.h
+++ b/src/sat/bsat/satProof2.h
@@ -290,6 +290,7 @@ static inline Vec_Int_t * Prf_ManUnsatCore( Prf_Man_t * p )
     int i, Entry;
     assert( p->iFirst >= 0 );
     assert( p->pInfo == NULL );
+    assert( Prf_ManSize(p) > 0 );
     vCore = Vec_IntAlloc( 64 * p->nWords );
     p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
     if ( p->vId2Pr == NULL )
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index dfe01a23..2b65170a 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -80,8 +80,9 @@ struct varinfo2_t
 //    unsigned lev    : 24;  // variable level
 };
 
-int    var_is_partA (sat_solver2* s, int v)              { return s->vi[v].partA;  }
-void   var_set_partA(sat_solver2* s, int v, int partA)   { s->vi[v].partA = partA; }
+int    var_is_assigned(sat_solver2* s, int v)            { return s->assigns[v] != varX; }
+int    var_is_partA (sat_solver2* s, int v)              { return s->vi[v].partA;        }
+void   var_set_partA(sat_solver2* s, int v, int partA)   { s->vi[v].partA = partA;       }
 
 //static inline int     var_level     (sat_solver2* s, int v)            { return s->vi[v].lev; }
 static inline int     var_level     (sat_solver2* s, int v)            { return s->levels[v];  }
@@ -95,6 +96,11 @@ static inline void    var_set_level (sat_solver2* s, int v, int lev)   { s->leve
 static inline void    var_set_value (sat_solver2* s, int v, int val)   { s->assigns[v] = val; }
 static inline void    var_set_polar (sat_solver2* s, int v, int pol)   { s->vi[v].pol = pol;  }
 
+// check if the literal is false under current assumptions
+static inline int     solver2_lit_is_false( sat_solver2* s, int Lit )  { return var_value(s, lit_var(Lit)) == !lit_sign(Lit); }
+
+
+
 // variable tags
 static inline int     var_tag       (sat_solver2* s, int v)            { return s->vi[v].tag; }
 static inline void    var_set_tag   (sat_solver2* s, int v, int tag)   {
@@ -1884,7 +1890,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
             }
             else
             {
-                assert( 0 );
+//                assert( 0 );
+//                r = var_unit_clause( s, lit_var(p) );
+//                assert( r != NULL );
+//                proof_id = clause2_proofid(s, r, 0);
                 proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions)
                 veci_resize(&s->conf_final,0);
                 veci_push(&s->conf_final, lit_neg(p));
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index bed774ef..a1539637 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -62,8 +62,9 @@ extern int *        Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars
 extern void         Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
 
 // global variables
-extern int          var_is_partA (sat_solver2* s, int v);
-extern void         var_set_partA(sat_solver2* s, int v, int partA);
+extern int          var_is_assigned(sat_solver2* s, int v);
+extern int          var_is_partA   (sat_solver2* s, int v);
+extern void         var_set_partA  (sat_solver2* s, int v, int partA);
 
 // proof-based APIs
 extern void *       Sat_ProofCore( sat_solver2 * s );
-- 
cgit v1.2.3