diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-25 18:06:36 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-25 18:06:36 -0800 |
commit | 9726d5a85e132e117cbc5caf7a3d8b6cd2f9e4fc (patch) | |
tree | 5eb399f32c6f4ab4dcb6e44fddfe9e5de799ab03 /src/sat/bsat/satSolver.h | |
parent | 7a0a4d4d7917290168450c2296f1504f06b34b88 (diff) | |
download | abc-9726d5a85e132e117cbc5caf7a3d8b6cd2f9e4fc.tar.gz abc-9726d5a85e132e117cbc5caf7a3d8b6cd2f9e4fc.tar.bz2 abc-9726d5a85e132e117cbc5caf7a3d8b6cd2f9e4fc.zip |
Improvement to the SAT solver (skipping binary clauses).
Diffstat (limited to 'src/sat/bsat/satSolver.h')
-rw-r--r-- | src/sat/bsat/satSolver.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index a67e829a..f500b46b 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -36,7 +36,7 @@ ABC_NAMESPACE_HEADER_START //================================================================================================= // Simple types: - +/* #ifndef __cplusplus #ifndef false # define false 0 @@ -64,7 +64,7 @@ static inline int lit_sign (lit l) { return l & 1; } static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } - +*/ //================================================================================================= // Public interface: @@ -84,14 +84,14 @@ extern int sat_solver_nclauses(sat_solver* s); extern int sat_solver_nconflicts(sat_solver* s); extern void sat_solver_setnvars(sat_solver* s,int n); - +/* struct stats_t { ABC_INT64_T starts, decisions, propagations, inspects, conflicts; ABC_INT64_T clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; }; typedef struct stats_t stats_t; - +*/ extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ); extern int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ); |