diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-16 19:54:28 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-16 19:54:28 -0700 |
| commit | 8093611068a89328a56f177e0a19b0422349b03c (patch) | |
| tree | 8eaf66e2df0b0e64e1702f54bbb86085d4404ce8 | |
| parent | 17cbe3567e1dc128610e8a714cc5ca702f4259f1 (diff) | |
| download | abc-8093611068a89328a56f177e0a19b0422349b03c.tar.gz abc-8093611068a89328a56f177e0a19b0422349b03c.tar.bz2 abc-8093611068a89328a56f177e0a19b0422349b03c.zip | |
Added comment how to print binary clauses in procedure Sat_SolverWriteDimacs().
| -rw-r--r-- | src/sat/bsat/satUtil.c | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index d782386e..f1f03ce2 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -61,7 +61,10 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement ) Synopsis [Write the clauses in the solver into a file in DIMACS format.] - Description [] + Description [This procedure by default does not print binary clauses. To enable + printing of binary clauses, please set fUseBinaryClauses to 0 in the body of + procedure sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt) + in file "satSolver.c".] SideEffects [] |