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