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:
SatProofNode(CVC3::Theorem theorem)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 
SatProofNode(SatProofNode * left,SatProofNode * right,SAT::Lit lit)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 
isLeaf()58     bool isLeaf() { return !d_theorem.isNull(); }
getLeaf()59     CVC3::Theorem getLeaf() { DebugAssert(isLeaf(), "SatProofNode: getLeaf"); return d_theorem; }
getLeftParent()60     SatProofNode* getLeftParent() { DebugAssert(!isLeaf(), "SatProofNode: getLeftParent"); return d_left; }
getRightParent()61     SatProofNode* getRightParent() { DebugAssert(!isLeaf(), "SatProofNode: getRightParent"); return d_right; }
getLit()62     SAT::Lit getLit() { DebugAssert(!isLeaf(), "SatProofNode: getLit"); return d_lit; }
hasNodeProof()63     bool hasNodeProof() {return !d_proof.isNull();};
getNodeProof()64     CVC3::Proof getNodeProof() {DebugAssert(!d_proof.isNull(), "SatProofNode: nodeProof get null"); return d_proof;}
setNodeProof(CVC3::Proof pf)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:
SatProof()75     SatProof() : d_root(NULL) { };
76 
~SatProof()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
registerLeaf(CVC3::Theorem theorem)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
registerNode(SatProofNode * left,SatProofNode * right,SAT::Lit l)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 
setRoot(SatProofNode * root)100     void setRoot(SatProofNode* root) {
101       d_root = root;
102     }
103 
104 
105     // access proof
106 
107     // ownership of all nodes remains with SatProof
getRoot()108     SatProofNode* getRoot() {
109       DebugAssert(d_root != NULL, "null root found in getRoot");
110       return d_root;
111     }
112   };
113 
114 }
115 
116 #endif
117