satcheck_minisat2.cpp File Reference

#include "satcheck_minisat2.h"
#include <inttypes.h>
#include <signal.h>
#include <unistd.h>
#include <limits>
#include <stack>
#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:

Go to the source code of this file.

Functions
void	convert (const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
static void	interrupt_solver (int signum)

Variables
static Minisat::Solver *	solver_to_interrupt =nullptr

Function Documentation

convert()

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

Definition at line 30 of file satcheck_minisat2.cpp.

References forall_literals, and PRECONDITION.

Referenced by satcheck_minisat2_baset< Minisat::Solver >::lcnf(), and satcheck_minisat2_baset< Minisat::Solver >::prop_solve().

interrupt_solver()

static void interrupt_solver ( int  signum )

static

Definition at line 157 of file satcheck_minisat2.cpp.

References solver_to_interrupt.

Referenced by satcheck_minisat2_baset< Minisat::Solver >::prop_solve().

Variable Documentation

solver_to_interrupt

Minisat::Solver* solver_to_interrupt =nullptr

static

Definition at line 155 of file satcheck_minisat2.cpp.

Referenced by interrupt_solver(), and satcheck_minisat2_baset< Minisat::Solver >::prop_solve().