CVC3

# sat_proof.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file sat_proof.h
00004  *\brief Sat solver proof representation
00005  *
00006  * Author: Alexander Fuchs
00007  *
00008  * Created: Sun Dec 07 11:09:00 2007
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  *
00017  * <hr>
00018  */
00019 /*****************************************************************************/
00020
00021 #ifndef _cvc3__sat__proof_h_
00022 #define _cvc3__sat__proof_h_
00023
00024 #include "theorem.h"
00025 #include <list>
00026
00027 namespace SAT {
00028
00029   // a node in a resolution tree, either:
00030   // - a leaf
00031   //   then d_clause is a clause added to the sat solver by the cvc controller;
00032   //   the other values are empty
00033   // - a binary node
00034   //   then the node represents the clause which can be derived by resolution
00035   //   between its left and right parent on d_lit,
00036   //   where d_left contains d_lit and d_right contains the negation of d_lit
00037   class SatProofNode {
00038   private:
00039     CVC3::Theorem d_theorem;
00040     SatProofNode* d_left;
00041     SatProofNode* d_right;
00042     SAT::Lit      d_lit;
00043     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
00044   public:
00045     SatProofNode(CVC3::Theorem theorem) :
00046       d_theorem(theorem), d_left(NULL), d_right(NULL){
00047       DebugAssert(!theorem.isNull(), "SatProofNode: constructor");
00048     }
00049       //we can modify the constructor of SatProofNode(clause) to store the clauses
00050       //add a method to return all clauses here
00051
00052     SatProofNode(SatProofNode* left, SatProofNode* right, SAT::Lit lit) :
00053       d_left(left), d_right(right), d_lit(lit) {
00054       DebugAssert(d_left != NULL, "SatProofNode: constructor");
00055       DebugAssert(d_right != NULL, "SatProofNode: constructor");
00056     }
00057
00058     bool isLeaf() { return !d_theorem.isNull(); }
00059     CVC3::Theorem getLeaf() { DebugAssert(isLeaf(), "SatProofNode: getLeaf"); return d_theorem; }
00060     SatProofNode* getLeftParent() { DebugAssert(!isLeaf(), "SatProofNode: getLeftParent"); return d_left; }
00061     SatProofNode* getRightParent() { DebugAssert(!isLeaf(), "SatProofNode: getRightParent"); return d_right; }
00062     SAT::Lit getLit() { DebugAssert(!isLeaf(), "SatProofNode: getLit"); return d_lit; }
00063     bool hasNodeProof() {return !d_proof.isNull();};
00064     CVC3::Proof getNodeProof() {DebugAssert(!d_proof.isNull(), "SatProofNode: nodeProof get null"); return d_proof;}
00065     void setNodeProof(CVC3::Proof pf) { d_proof=pf;}
00066   };
00067
00068
00069   // a proof of the clause d_root
00070   class SatProof {
00071   private:
00072     SatProofNode* d_root;
00073     std::list<SatProofNode*> d_nodes;
00074   public:
00075     SatProof() : d_root(NULL) { };
00076
00077     ~SatProof() {
00078       for (std::list<SatProofNode*>::iterator i = d_nodes.begin(); i != d_nodes.end(); ++i) {
00079   delete(*i);
00080       }
00081     }
00082
00083
00084     // build proof
00085
00086     // ownership of created node remains with SatProof
00087     SatProofNode* registerLeaf(CVC3::Theorem theorem) {
00088       SatProofNode* node = new SatProofNode(theorem);
00089       d_nodes.push_back(node);
00090       return node;
00091     }
00092
00093     // ownership of created node remains with SatProof
00094     SatProofNode* registerNode(SatProofNode* left, SatProofNode* right, SAT::Lit l) {
00095       SatProofNode* node = new SatProofNode(left, right, l);
00096       d_nodes.push_back(node);
00097       return node;
00098     }
00099
00100     void setRoot(SatProofNode* root) {
00101       d_root = root;
00102     }
00103
00104
00105     // access proof
00106
00107     // ownership of all nodes remains with SatProof
00108     SatProofNode* getRoot() {
00109       DebugAssert(d_root != NULL, "null root found in getRoot");
00110       return d_root;
00111     }
00112   };
00113
00114 }
00115
00116 #endif