CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
dpllt_minisat.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file dpllt_minisat.h
4
*\brief Implementation of dpllt module based on minisat
5
*
6
* Author: Alexander Fuchs
7
*
8
* Created: Fri Sep 08 11:04:00 2006
9
*
10
* <hr>
11
*
12
* License to use, copy, modify, sell and/or distribute this software
13
* and its documentation for any purpose is hereby granted without
14
* royalty, subject to the terms and conditions defined in the \ref
15
* LICENSE file provided with this distribution.
16
*
17
* <hr>
18
*/
19
/*****************************************************************************/
20
21
#ifndef _cvc3__sat__dpllt_minisat_h_
22
#define _cvc3__sat__dpllt_minisat_h_
23
24
#include "
dpllt.h
"
25
#include "
proof.h
"
26
#include "
cnf_manager.h
"
27
#include <stack>
28
29
30
// forward declaration of the minisat solver
31
namespace
MiniSat {
32
class
Solver
;
33
}
34
35
namespace
SAT {
36
37
class
SatProof;
38
39
// an implementation of the DPLLT interface using an adapted MiniSat SAT solver
40
class
DPLLTMiniSat
:
public
DPLLT
{
41
public
:
42
43
protected
:
44
// determines if the derivation statistic of the solver
45
// is printed after the derivation terminates.
46
// can only be set with the constructor
47
bool
d_printStats
;
48
49
// if true then minisat will create a derivation
50
// of the empty clause for an unsatisfiable problem.
51
// see getProof().
52
bool
d_createProof
;
53
54
// if d_createProof, then the proof of the last unsatisfiable search
55
SatProof
*
d_proof
;
56
57
// the dpllt interface operates in a stack fashion via checkSat and push.
58
// each stack's data is stored in a level, which is just an instance of MiniSat.
59
// whenever a checkSat or push is done on a solver that is already in a search,
60
// a new solver is created and pushed.
61
std::stack<MiniSat::Solver*>
d_solvers
;
62
63
// returnes the currently active MiniSat instance
64
//
65
// must not be called when there is no active MiniSat instance,
66
// i.e. d_solvers is empty.
67
MiniSat::Solver
*
getActiveSolver
();
68
69
// creates a solver as an extension of the previous solver
70
// (i.e. takes clauses/assignments/lemmas)
71
// and pushes it on d_solvers
72
void
pushSolver
();
73
74
// called by checkSat and continueCheck to initiate a search
75
// with a SAT solver
76
CVC3::QueryResult
search
();
77
78
79
80
public
:
81
DPLLTMiniSat
(
TheoryAPI
*
theoryAPI
,
Decider
*
decider
,
82
bool
printStats =
false
,
bool
createProof =
false
);
83
virtual
~DPLLTMiniSat
();
84
85
86
// Implementation of the DPLLT interface
87
virtual
CVC3::QueryResult
checkSat
(
const
CNF_Formula
& cnf);
88
virtual
CVC3::QueryResult
continueCheck
(
const
CNF_Formula
& cnf);
89
virtual
void
push
();
90
virtual
void
pop
();
91
virtual
void
addAssertion
(
const
CNF_Formula
& cnf);
92
virtual
std::vector<SAT::Lit>
getCurAssignments
() ;
93
virtual
std::vector<std::vector<SAT::Lit> >
getCurClauses
();
94
virtual
Var::Val
getValue
(
Var
v);
95
96
// if createProof was given returns a proof of the last unsatisfiable search,
97
// otherwise (or if there was no unsatisfiable search) NULL
98
// ownership remains with DPLLTMiniSat
99
SatProof
*
getProof
() {
100
DebugAssert
((
d_proof
!= NULL),
"null proof foound"
) ;
101
return
d_proof
;
102
};
103
104
CVC3::Proof
getSatProof
(
CNF_Manager
*,
CVC3::TheoryCore
*) ;
105
};
106
107
}
108
109
#endif
Generated on Fri Aug 9 2013 10:34:40 for CVC3 by
1.8.4