CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
dpllt_basic.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file dpllt_basic.h
4
*\brief Basic implementation of dpllt module
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Mon Dec 12 19:06:58 2005
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_basic_h_
22
#define _cvc3__sat__dpllt_basic_h_
23
24
#include "
dpllt.h
"
25
#include "
sat_api.h
"
26
#include "
cdo.h
"
27
#include "
proof.h
"
28
#include "
cnf_manager.h
"
29
30
namespace
SAT {
31
32
class
DPLLTBasic
:
public
DPLLT
{
33
34
CVC3::ContextManager
*
d_cm
;
35
36
bool
d_ready
;
37
SatSolver
*
d_mng
;
38
CNF_Formula_Impl
*
d_cnf
;
39
CD_CNF_Formula
*
d_assertions
;
40
41
std::vector<SatSolver*>
d_mngStack
;
42
std::vector<CNF_Formula_Impl*>
d_cnfStack
;
43
std::vector<CD_CNF_Formula*>
d_assertionsStack
;
44
bool
d_printStats
;
45
46
CVC3::CDO<unsigned>
d_pushLevel
;
47
CVC3::CDO<bool>
d_readyPrev
;
48
CVC3::CDO<unsigned>
d_prevStackSize
;
49
CVC3::CDO<unsigned>
d_prevAStackSize
;
50
51
void
createManager
();
52
void
generate_CDB
(
CNF_Formula_Impl
& cnf);
53
void
handle_result
(
SatSolver::SATStatus
outcome);
54
void
verify_solution
();
55
56
public
:
57
DPLLTBasic
(
TheoryAPI
*
theoryAPI
,
Decider
*
decider
,
CVC3::ContextManager
* cm,
58
bool
printStats =
false
);
59
virtual
~DPLLTBasic
();
60
61
void
addNewClause
(
const
Clause
& c);
62
void
addNewClauses
(
CNF_Formula_Impl
& cnf);
63
64
SatSolver::Lit
cvc2SAT
(
Lit
l)
65
{
return
l.
isNull
() ?
SatSolver::Lit
() :
66
d_mng
->
MakeLit
(
d_mng
->
GetVar
(l.
getVar
()), l.
isPositive
() ? 0 : 1); }
67
68
Lit
SAT2cvc
(
SatSolver::Lit
l)
69
{
return
l.
IsNull
() ?
Lit
() :
70
Lit
(
d_mng
->
GetVarIndex
(
d_mng
->
GetVarFromLit
(l)),
71
d_mng
->
GetPhaseFromLit
(l) == 0); }
72
73
SatSolver
*
satSolver
() {
return
d_mng
; }
74
75
// Implementation of virtual DPLLT methods
76
77
void
push
();
78
void
pop
();
79
void
addAssertion
(
const
CNF_Formula
& cnf);
80
virtual
std::vector<SAT::Lit>
getCurAssignments
() ;
81
virtual
std::vector<std::vector<SAT::Lit> >
getCurClauses
();
82
83
CVC3::QueryResult
checkSat
(
const
CNF_Formula
& cnf);
84
CVC3::QueryResult
continueCheck
(
const
CNF_Formula
& cnf);
85
Var::Val
getValue
(
Var
v) {
return
Var::Val
(
d_mng
->
GetVarAssignment
(
d_mng
->
GetVar
(v))); }
86
87
CVC3::Proof
getSatProof
(
CNF_Manager
*,
CVC3::TheoryCore
*);
88
89
};
90
91
}
92
93
#endif
Generated on Mon Aug 19 2013 14:42:40 for CVC3 by
1.8.4