CBMC
|
#include "satcheck_minisat2.h"
#include <signal.h>
#include <unistd.h>
#include <limits>
#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.
Macros | |
#define | l_False Minisat::l_False |
#define | l_True Minisat::l_True |
Functions | |
void | convert (const bvt &bv, Minisat::vec< Minisat::Lit > &dest) |
void | convert_assumptions (const bvt &bv, Minisat::vec< Minisat::Lit > &dest) |
static void | interrupt_solver (int signum) |
Variables | |
static Minisat::Solver * | solver_to_interrupt =nullptr |
#define l_False Minisat::l_False |
Definition at line 25 of file satcheck_minisat2.cpp.
#define l_True Minisat::l_True |
Definition at line 26 of file satcheck_minisat2.cpp.
Definition at line 33 of file satcheck_minisat2.cpp.
Definition at line 46 of file satcheck_minisat2.cpp.
Definition at line 198 of file satcheck_minisat2.cpp.
|
static |
Definition at line 196 of file satcheck_minisat2.cpp.