#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>

Include dependency graph for satcheck_minisat2.cpp:

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

Macro Definition Documentation

◆ l_False

#define l_False Minisat::l_False

Definition at line 25 of file satcheck_minisat2.cpp.

◆ l_True

#define l_True Minisat::l_True

Definition at line 26 of file satcheck_minisat2.cpp.

Function Documentation

◆ convert()

void convert	(	const bvt &	bv,
		Minisat::vec< Minisat::Lit > &	dest
	)

Definition at line 33 of file satcheck_minisat2.cpp.

◆ convert_assumptions()

void convert_assumptions	(	const bvt &	bv,
		Minisat::vec< Minisat::Lit > &	dest
	)

Definition at line 46 of file satcheck_minisat2.cpp.

◆ interrupt_solver()

static void interrupt_solver ( int signum )

static

Definition at line 198 of file satcheck_minisat2.cpp.

Variable Documentation

◆ solver_to_interrupt

Minisat::Solver* solver_to_interrupt =nullptr