CVC3  2.4.1
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:
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:
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 
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:
73  std::list<SatProofNode*> d_nodes;
74  public:
75  SatProof() : d_root(NULL) { };
76 
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
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
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
109  DebugAssert(d_root != NULL, "null root found in getRoot");
110  return d_root;
111  }
112  };
113 
114 }
115 
116 #endif
CVC3::Proof d_proof
Definition: sat_proof.h:43
SatProofNode * d_root
Definition: sat_proof.h:72
CVC3::Theorem d_theorem
Definition: sat_proof.h:39
bool isNull() const
Definition: proof.h:47
CVC3::Theorem getLeaf()
Definition: sat_proof.h:59
std::list< SatProofNode * > d_nodes
Definition: sat_proof.h:73
bool hasNodeProof()
Definition: sat_proof.h:63
SatProofNode * getRoot()
Definition: sat_proof.h:108
#define DebugAssert(cond, str)
Definition: debug.h:408
CVC3::Proof getNodeProof()
Definition: sat_proof.h:64
static int left(int i)
Definition: minisat_heap.h:53
SatProofNode(SatProofNode *left, SatProofNode *right, SAT::Lit lit)
Definition: sat_proof.h:52
SatProofNode(CVC3::Theorem theorem)
Definition: sat_proof.h:45
Definition: cnf.h:51
bool isNull() const
Definition: theorem.h:164
void setRoot(SatProofNode *root)
Definition: sat_proof.h:100
SatProofNode * registerNode(SatProofNode *left, SatProofNode *right, SAT::Lit l)
Definition: sat_proof.h:94
SatProofNode * getLeftParent()
Definition: sat_proof.h:60
SAT::Lit getLit()
Definition: sat_proof.h:62
static int right(int i)
Definition: minisat_heap.h:54
SatProofNode * getRightParent()
Definition: sat_proof.h:61
Definition: cnf.h:32
SatProofNode * registerLeaf(CVC3::Theorem theorem)
Definition: sat_proof.h:87
void setNodeProof(CVC3::Proof pf)
Definition: sat_proof.h:65
SAT::Lit d_lit
Definition: sat_proof.h:42
SatProofNode * d_left
Definition: sat_proof.h:40
SatProofNode * d_right
Definition: sat_proof.h:41