From 066e8d1b173d11aeb837ffda56a8ba1bb7ddb214 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 23 Jan 2018 19:45:17 -0800 Subject: Experiments with SAT-based simulation. --- src/sat/satoko/solver_api.c | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'src/sat') diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index adf30cef..79d48c3b 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -281,7 +281,13 @@ int satoko_add_clause(solver_t *s, int *lits, int size) solver_enqueue(s, vec_uint_at(s->temp_lits, 0), UNDEF); return (s->status = (solver_propagate(s) == UNDEF)); } - + if ( 0 ) { + for ( i = 0; i < vec_uint_size(s->temp_lits); i++ ) { + int lit = vec_uint_at(s->temp_lits, i); + printf( "%s%d ", lit&1 ? "!":"", lit>>1 ); + } + printf( "\n" ); + } cref = solver_clause_create(s, s->temp_lits, 0); clause_watch(s, cref); return SATOKO_OK; -- cgit v1.2.3