CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
sat
sat_proof.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file sat_proof.h
4
*\brief Sat solver proof representation
5
*
6
* Author: Alexander Fuchs
7
*
8
* Created: Sun Dec 07 11:09:00 2007
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__proof_h_
22
#define _cvc3__sat__proof_h_
23
24
#include "
theorem.h
"
25
#include <list>
26
27
namespace
SAT {
28
29
// a node in a resolution tree, either:
30
// - a leaf
31
// then d_clause is a clause added to the sat solver by the cvc controller;
32
// the other values are empty
33
// - a binary node
34
// then the node represents the clause which can be derived by resolution
35
// between its left and right parent on d_lit,
36
// where d_left contains d_lit and d_right contains the negation of d_lit
37
class
SatProofNode
{
38
private
:
39
CVC3::Theorem
d_theorem
;
40
SatProofNode
*
d_left
;
41
SatProofNode
*
d_right
;
42
SAT::Lit
d_lit
;
43
CVC3::Proof
d_proof
;
// by yeting, to store the proof. We do not need to set a null value to proof bcause this is done by the constructor of proof
44
public
:
45
SatProofNode
(
CVC3::Theorem
theorem) :
46
d_theorem
(theorem),
d_left
(NULL),
d_right
(NULL){
47
DebugAssert
(!theorem.
isNull
(),
"SatProofNode: constructor"
);
48
}
49
//we can modify the constructor of SatProofNode(clause) to store the clauses
50
//add a method to return all clauses here
51
52
SatProofNode
(
SatProofNode
*
left
,
SatProofNode
*
right
,
SAT::Lit
lit) :
53
d_left
(left),
d_right
(right),
d_lit
(lit) {
54
DebugAssert
(
d_left
!= NULL,
"SatProofNode: constructor"
);
55
DebugAssert
(
d_right
!= NULL,
"SatProofNode: constructor"
);
56
}
57
58
bool
isLeaf
() {
return
!
d_theorem
.
isNull
(); }
59
CVC3::Theorem
getLeaf
() {
DebugAssert
(
isLeaf
(),
"SatProofNode: getLeaf"
);
return
d_theorem
; }
60
SatProofNode
*
getLeftParent
() {
DebugAssert
(!
isLeaf
(),
"SatProofNode: getLeftParent"
);
return
d_left
; }
61
SatProofNode
*
getRightParent
() {
DebugAssert
(!
isLeaf
(),
"SatProofNode: getRightParent"
);
return
d_right
; }
62
SAT::Lit
getLit
() {
DebugAssert
(!
isLeaf
(),
"SatProofNode: getLit"
);
return
d_lit
; }
63
bool
hasNodeProof
() {
return
!
d_proof
.
isNull
();};
64
CVC3::Proof
getNodeProof
() {
DebugAssert
(!
d_proof
.
isNull
(),
"SatProofNode: nodeProof get null"
);
return
d_proof
;}
65
void
setNodeProof
(
CVC3::Proof
pf) {
d_proof
=pf;}
66
};
67
68
69
// a proof of the clause d_root
70
class
SatProof
{
71
private
:
72
SatProofNode
*
d_root
;
73
std::list<SatProofNode*>
d_nodes
;
74
public
:
75
SatProof
() :
d_root
(NULL) { };
76
77
~SatProof
() {
78
for
(std::list<SatProofNode*>::iterator i =
d_nodes
.begin(); i !=
d_nodes
.end(); ++i) {
79
delete
(*i);
80
}
81
}
82
83
84
// build proof
85
86
// ownership of created node remains with SatProof
87
SatProofNode
*
registerLeaf
(
CVC3::Theorem
theorem) {
88
SatProofNode
* node =
new
SatProofNode
(theorem);
89
d_nodes
.push_back(node);
90
return
node;
91
}
92
93
// ownership of created node remains with SatProof
94
SatProofNode
*
registerNode
(
SatProofNode
*
left
,
SatProofNode
*
right
,
SAT::Lit
l) {
95
SatProofNode
* node =
new
SatProofNode
(left, right, l);
96
d_nodes
.push_back(node);
97
return
node;
98
}
99
100
void
setRoot
(
SatProofNode
* root) {
101
d_root
= root;
102
}
103
104
105
// access proof
106
107
// ownership of all nodes remains with SatProof
108
SatProofNode
*
getRoot
() {
109
DebugAssert
(
d_root
!= NULL,
"null root found in getRoot"
);
110
return
d_root
;
111
}
112
};
113
114
}
115
116
#endif
Generated on Sat Aug 3 2013 07:58:30 for CVC3 by
1.8.4