diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-13 17:53:19 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-13 17:53:19 +0700 |
| commit | a64957a526ed1ff4df552db5e1d7bc5fd687900a (patch) | |
| tree | 5765d34e2748d5a3cc19d0778042f4ad4099d5e6 /src/sat/bsat | |
| parent | 21289bf08a668e1fc329bdaeca3e462910135286 (diff) | |
| download | abc-a64957a526ed1ff4df552db5e1d7bc5fd687900a.tar.gz abc-a64957a526ed1ff4df552db5e1d7bc5fd687900a.tar.bz2 abc-a64957a526ed1ff4df552db5e1d7bc5fd687900a.zip | |
Adding an option to bmc3 to use Satoko intead of the default SAT solver.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satClause.h | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h index 3a6afa20..d2ed3b75 100644 --- a/src/sat/bsat/satClause.h +++ b/src/sat/bsat/satClause.h @@ -146,7 +146,7 @@ static inline void clause_set_id( clause * c, int id ) { c->lits[c- static inline int clause_size( clause * c ) { return c->size; } static inline lit * clause_begin( clause * c ) { return c->lits; } static inline lit * clause_end( clause * c ) { return c->lits + c->size; } -static inline void clause_print( clause * c ) +static inline void clause_print_( clause * c ) { int i; printf( "{ " ); diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 7a4470f1..0d17766c 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1783,7 +1783,7 @@ void sat_solver2_verify( sat_solver2* s ) if ( k == (int)c->size ) { Abc_Print(1, "Clause %d is not satisfied. ", c->Id ); - clause_print( c ); + clause_print_( c ); sat_solver2_find_clause( s, clause_handle(&s->clauses, c), 1 ); Counter++; } |