diff options
Diffstat (limited to 'src/sat/bsat/satSolver2.h')
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 186 |
1 files changed, 110 insertions, 76 deletions
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index c64a4213..1cdc8bd9 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -41,39 +41,41 @@ struct sat_solver2_t; typedef struct sat_solver2_t sat_solver2; extern sat_solver2* sat_solver2_new(void); -extern void sat_solver2_delete(sat_solver2* s); +extern void sat_solver2_delete(sat_solver2* s); -extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end); -extern int sat_solver2_simplify(sat_solver2* s); -extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); +extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end); +extern int sat_solver2_simplify(sat_solver2* s); +extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); -extern void sat_solver2_setnvars(sat_solver2* s,int n); +extern void sat_solver2_setnvars(sat_solver2* s,int n); -extern void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); -extern void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p ); -extern int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars ); -extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar ); +extern void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); +extern void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p ); +extern int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars ); +extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar ); // trace recording -extern void sat_solver2TraceStart( sat_solver2 * pSat, char * pName ); -extern void sat_solver2TraceStop( sat_solver2 * pSat ); -extern void sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot ); +extern void sat_solver2TraceStart( sat_solver2 * pSat, char * pName ); +extern void sat_solver2TraceStop( sat_solver2 * pSat ); +extern void sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot ); // clause storage -extern void sat_solver2_store_alloc( sat_solver2 * s ); -extern void sat_solver2_store_write( sat_solver2 * s, char * pFileName ); -extern void sat_solver2_store_free( sat_solver2 * s ); -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 ); +extern void sat_solver2_store_alloc( sat_solver2 * s ); +extern void sat_solver2_store_write( sat_solver2 * s, char * pFileName ); +extern void sat_solver2_store_free( sat_solver2 * s ); +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); +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); - +extern int clause_is_partA (sat_solver2* s, int handle); +extern void clause_set_partA(sat_solver2* s, int handle, int partA); +// other clause functions +extern int clause_id(sat_solver2* s, int h); + //================================================================================================= // Solver representation: @@ -83,75 +85,105 @@ typedef struct varinfo_t varinfo; struct sat_solver2_t { - int size; // nof variables - int cap; // size of varmaps - int qhead; // Head index of queue. - int qtail; // Tail index of queue. - - int root_level; // Level of first proper decision. - int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. - int simpdb_props; // Number of propagations before next 'simplifyDB()'. - double random_seed; - double progress_estimate; - int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - int fNotUseRandom; // do not allow random decisions with a fixed probability -// int fSkipSimplify; // set to one to skip simplification of the clause database - int fProofLogging; // enable proof-logging + int size; // nof variables + int cap; // size of varmaps + int qhead; // Head index of queue. + int qtail; // Tail index of queue. + + int root_level; // Level of first proper decision. + int simpdb_assigns; // Number of top-level assignments at last 'simplifyDB()'. + int simpdb_props; // Number of propagations before next 'simplifyDB()'. + double random_seed; + double progress_estimate; + int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything + int fNotUseRandom; // do not allow random decisions with a fixed probability +// int fSkipSimplify; // set to one to skip simplification of the clause database + int fProofLogging; // enable proof-logging // clauses - veci clauses; // clause memory - veci* wlists; // watcher lists (for each literal) - int iFirstLearnt; // the first learnt clause + veci clauses; // clause memory + veci* wlists; // watcher lists (for each literal) + int iLearntFirst; // the first learnt clause + int iLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) // activities #ifdef USE_FLOAT_ACTIVITY - double var_inc; // Amount to bump next variable with. - double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. - float cla_inc; // Amount to bump next clause with. - float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. - double* activity; // A heuristic measurement of the activity of a variable. + double var_inc; // Amount to bump next variable with. + double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. + float cla_inc; // Amount to bump next clause with. + float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + double* activity; // A heuristic measurement of the activity of a variable. #else - int var_inc; // Amount to bump next variable with. - int cla_inc; // Amount to bump next clause with. - unsigned* activity; // A heuristic measurement of the activity of a variable. + int var_inc; // Amount to bump next variable with. + int cla_inc; // Amount to bump next clause with. + unsigned* activity; // A heuristic measurement of the activity of a variable. #endif - veci claActs; // clause activities - veci claProofs; // clause proofs + veci claActs; // clause activities + veci claProofs; // clause proofs // internal state - varinfo * vi; // variable information - lit* trail; // sequence of assignment and implications - int* orderpos; // Index in variable order. - cla* reasons; // reason clauses - cla* units; // unit clauses - - veci tagged; // (contains: var) - veci stack; // (contains: var) - veci order; // Variable order. (heap) (contains: var) - veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) - veci temp_clause; // temporary storage for a CNF clause - veci model; // If problem is solved, this vector contains the model (contains: lbool). - veci conf_final; // If problem is unsatisfiable (possibly under assumptions), - // this vector represent the final conflict clause expressed in the assumptions. - veci mark_levels; // temporary storage for labeled levels - veci min_lit_order; // ordering of removable literals - veci min_step_order;// ordering of resolution steps + varinfo * vi; // variable information + lit* trail; // sequence of assignment and implications + int* orderpos; // Index in variable order. + cla* reasons; // reason clauses + cla* units; // unit clauses + + veci tagged; // (contains: var) + veci stack; // (contains: var) + veci order; // Variable order. (heap) (contains: var) + veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) + veci temp_clause; // temporary storage for a CNF clause + veci model; // If problem is solved, this vector contains the model (contains: lbool). + veci conf_final; // If problem is unsatisfiable (possibly under assumptions), + // this vector represent the final conflict clause expressed in the assumptions. + veci mark_levels; // temporary storage for labeled levels + veci min_lit_order; // ordering of removable literals + veci min_step_order; // ordering of resolution steps + veci glob_vars; // global variables // proof logging - veci proof_clas; // sequence of proof clauses - veci proof_vars; // sequence of proof variables - int iStartChain; // temporary variable to remember beginning of the current chain in proof logging - int fLastConfId; // in proof-logging mode, the ID of the final conflict clause (conf_final) - int nUnits; // the total number of unit clauses + veci proof_clas; // sequence of proof clauses + veci proof_vars; // sequence of proof variables + int iStartChain; // temporary variable to remember beginning of the current chain in proof logging + int nUnits; // the total number of unit clauses // statistics - stats_t stats; - ABC_INT64_T nConfLimit; // external limit on the number of conflicts - ABC_INT64_T nInsLimit; // external limit on the number of implications - int nRuntimeLimit; // external limit on runtime + stats_t stats; + ABC_INT64_T nConfLimit; // external limit on the number of conflicts + ABC_INT64_T nInsLimit; // external limit on the number of implications + int nRuntimeLimit; // external limit on runtime +}; +typedef struct satset_t satset; +struct satset_t +{ + unsigned learnt : 1; + unsigned mark : 1; + unsigned partA : 1; + unsigned nEnts : 29; + int Id; + lit pEnts[0]; }; +static inline satset* satset_read (veci* p, cla h ) { return h ? (satset*)(veci_begin(p) + h) : NULL; } +static inline cla satset_handle (veci* p, satset* c) { return (cla)((int *)c - veci_begin(p)); } +static inline int satset_check (veci* p, satset* c) { return (int*)c > veci_begin(p) && (int*)c < veci_begin(p) + veci_size(p); } +static inline int satset_size (int nLits) { return sizeof(satset)/4 + nLits; } +static inline void satset_print (satset * c) { + int i; + printf( "{ " ); + for ( i = 0; i < (int)c->nEnts; i++ ) + printf( "%d ", (c->pEnts[i] & 1)? -(c->pEnts[i] >> 1) : c->pEnts[i] >> 1 ); + printf( "}\n" ); +} + + +#define satset_foreach_entry( p, c, h, s ) \ + for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) ) + +//================================================================================================= +// Public APIs: + static inline int sat_solver2_nvars(sat_solver2* s) { return s->size; @@ -213,6 +245,8 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) return fNotUseRandomOld; } +extern void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars ); + ABC_NAMESPACE_HEADER_END #endif |