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