|
cprover
|
#include "satcheck_minisat2.h"#include <inttypes.h>#include <cassert>#include <stack>#include <util/invariant.h>#include <util/threeval.h>#include <minisat/core/Solver.h>#include <minisat/simp/SimpSolver.h>Go to the source code of this file.
Functions | |
| void | convert (const bvt &bv, Minisat::vec< Minisat::Lit > &dest) |
| void convert | ( | const bvt & | bv, |
| Minisat::vec< Minisat::Lit > & | dest | ||
| ) |
Definition at line 29 of file satcheck_minisat2.cpp.
References forall_literals.
Referenced by satcheck_minisat2_baset< Minisat::Solver >::lcnf(), and satcheck_minisat2_baset< Minisat::Solver >::prop_solve().