From bb96fa361ca10886096c6884f96d32b6961fef35 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 5 Dec 2011 11:53:57 -0800 Subject: Proof-logging in the updated solver. --- src/sat/bsat/satProof.c | 2 +- src/sat/bsat/satSolver2.c | 42 +++++++++++++++++++++++++----------------- src/sat/bsat/satSolver2.h | 8 ++++++++ 3 files changed, 34 insertions(+), 18 deletions(-) (limited to 'src') diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index b3cf2b6c..5b3901a1 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -48,7 +48,7 @@ struct Sat_Set_t_ static inline int Sat_SetCheck( Vec_Int_t * p, Sat_Set_t * pNode ) { return (int *)pNode > Vec_IntArray(p) && (int *)pNode < Vec_IntLimit(p); } static inline int Sat_SetId( Vec_Int_t * p, Sat_Set_t * pNode ) { return (int *)pNode - Vec_IntArray(p); } -static inline Sat_Set_t * Sat_SetFromId( Vec_Int_t * p, int i ) { return (Sat_Set_t *)(Vec_IntArray(p) + i); } +static inline Sat_Set_t * Sat_SetFromId( Vec_Int_t * p, int i ) { return (Sat_Set_t *)(Vec_IntArray(p) + i); } static inline int Sat_SetSize( Sat_Set_t * pNode ) { return pNode->nEnts + 2; } #define Sat_PoolForEachSet( p, pNode, i ) \ diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 42297070..72e36894 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -85,28 +85,32 @@ struct varinfo_t { unsigned val : 2; // variable value unsigned pol : 1; // last polarity + unsigned glo : 1; // global variable unsigned tag : 3; // conflict analysis tags - unsigned lev : 26; // variable level + unsigned lev : 25; // variable level }; +int var_is_global (sat_solver2* s, int v) { return s->vi[v].glo; } +void var_set_global(sat_solver2* s, int v, int glo) { s->vi[v].glo = glo; } + static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; } static inline int var_polar (sat_solver2* s, int v) { return s->vi[v].pol; } static inline int var_level (sat_solver2* s, int v) { return s->vi[v].lev; } -static inline void var_set_value (sat_solver2* s, int v, int val ) { s->vi[v].val = val; } -static inline void var_set_polar (sat_solver2* s, int v, int pol ) { s->vi[v].pol = pol; } -static inline void var_set_level (sat_solver2* s, int v, int lev ) { s->vi[v].lev = lev; } +static inline void var_set_value (sat_solver2* s, int v, int val) { s->vi[v].val = val; } +static inline void var_set_polar (sat_solver2* s, int v, int pol) { s->vi[v].pol = pol; } +static inline void var_set_level (sat_solver2* s, int v, int lev) { s->vi[v].lev = lev; } // 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) { - assert( tag > 0 && tag < 16 ); + assert( tag > 0 && tag < 8 ); if ( s->vi[v].tag == 0 ) veci_push( &s->tagged, v ); s->vi[v].tag = tag; } static inline void var_add_tag (sat_solver2* s, int v, int tag) { - assert( tag > 0 && tag < 16 ); + assert( tag > 0 && tag < 8 ); if ( s->vi[v].tag == 0 ) veci_push( &s->tagged, v ); s->vi[v].tag |= tag; @@ -145,7 +149,7 @@ static inline int lit_reason (sat_solver2* s, int l) { return // Clause datatype + minor functions: typedef struct satset_t satset; -struct satset_t // should have even number of entries! +struct satset_t { unsigned learnt : 1; unsigned mark : 1; @@ -155,10 +159,14 @@ struct satset_t // should have even number of entries! lit pLits[0]; }; -static inline int clause_size (int nLits) { return sizeof(satset)/4 + nLits; } - static inline satset* get_clause (sat_solver2* s, int c) { return c ? (satset*)(veci_begin(&s->clauses) + c) : NULL; } static inline cla clause_id (sat_solver2* s, satset* c) { return (cla)((int *)c - veci_begin(&s->clauses)); } +static inline int clause_size (int nLits) { return sizeof(satset)/4 + nLits; } +static inline int clause_proofid(sat_solver2* s, satset* c) { return c->learnt ? veci_begin(&s->claProofs)[c->Id]<<1 : (clause_id(s,c)<<1) | 1; } + +// these two only work after creating a clause before the solver is called +int clause_is_partA (sat_solver2* s, int cid) { return get_clause(s, cid)->partA; } +void clause_set_partA(sat_solver2* s, int cid, int partA) { get_clause(s, cid)->partA = partA; } //static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? get_clause(s, s->reasons[v] >> 1) : NULL; } //static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1; } @@ -166,7 +174,7 @@ static inline satset* var_unit_clause(sat_solver2* s, int v) { return static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } #define sat_solver_foreach_clause( s, c, i ) \ - for ( i = 16; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) ) + for ( i = 1; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) ) #define sat_solver_foreach_learnt( s, c, i ) \ for ( i = s->iFirstLearnt; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) ) @@ -186,7 +194,7 @@ static inline void proof_chain_start( sat_solver2* s, satset* c ) s->iStartChain = veci_size(&s->proof_clas); veci_push(&s->proof_clas, 0); veci_push(&s->proof_clas, 0); - veci_push(&s->proof_clas, c->learnt ? veci_begin(&s->claProofs)[c->Id] : clause_id(s,c) ^ 1 ); + veci_push(&s->proof_clas, clause_proofid(s, c) ); veci_push(&s->proof_vars, 0); veci_push(&s->proof_vars, 0); veci_push(&s->proof_vars, 0); @@ -198,8 +206,9 @@ static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var ) if ( s->fProofLogging ) { satset* c = cls ? cls : var_unit_clause( s, Var ); - veci_push(&s->proof_clas, c->learnt ? veci_begin(&s->claProofs)[c->Id] : clause_id(s,c) ^ 1 ); + veci_push(&s->proof_clas, clause_proofid(s, c) ); veci_push(&s->proof_vars, Var); +// printf( "%d %d ", clause_proofid(s, c), Var ); } } @@ -394,7 +403,8 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) ); // printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc ); s->clauses.cap = nMemAlloc; - s->clauses.size = Abc_MaxInt( veci_size(&s->clauses), 2 ); + if ( veci_size(&s->clauses) == 0 ) + veci_push( &s->clauses, -1 ); } // create clause c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses)); @@ -1325,7 +1335,6 @@ void sat_solver2_delete(sat_solver2* s) int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) { - cla Cid; lit *i,*j; int maxvar; lit last; @@ -1375,8 +1384,7 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) return solver2_enqueue(s,*begin,0); // create new clause - Cid = clause_new(s,begin,j,0,0); - return true; + return clause_new(s,begin,j,0,0); } int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) @@ -1420,7 +1428,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) // count literals s->stats.clauses++; s->stats.clauses_literals += end - begin; - return 1; + return Cid; } diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index e67d8111..c64a4213 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -67,6 +67,14 @@ extern void sat_solver2_store_mark_roots( sat_solver2 * s ); extern void sat_solver2_store_mark_clauses_a( sat_solver2 * s ); extern void * sat_solver2_store_release( sat_solver2 * s ); +// global variables +extern int var_is_global (sat_solver2* s, int v); +extern void var_set_global(sat_solver2* s, int v, int glo); +// clause grouping (these two only work after creating a clause before the solver is called) +extern int clause_is_partA (sat_solver2* s, int cid); +extern void clause_set_partA(sat_solver2* s, int cid, int partA); + + //================================================================================================= // Solver representation: -- cgit v1.2.3