CVC3
LFSCBoolProof.h
Go to the documentation of this file.
1 #ifndef LFSC_BOOL_PROOF_H_
2 #define LFSC_BOOL_PROOF_H_
3 
4 #include "LFSCProof.h"
5 
6 class LFSCBoolRes : public LFSCProof
7 {
8 private:
10  int d_var;
11  bool d_col;
12  LFSCBoolRes(LFSCProof* pf1, LFSCProof* pf2, int v, bool col): LFSCProof(),
13  d_var(v), d_col(col){
14  d_children[0] = pf1;
15  d_children[1] = pf2;
16  }
17  virtual ~LFSCBoolRes(){}
18  long int get_length(){
19  return 10 + d_children[0]->get_string_length() + d_children[1]->get_string_length();
20  }
21 public:
22  virtual LFSCBoolRes* AsLFSCBoolRes(){ return this; }
23  void print_pf( std::ostream& s, int ind = 0 );
24  void print_struct( std::ostream& s, int ind = 0 );
25  //standard Make
26  static LFSCProof* Make(LFSCProof* pf1, LFSCProof* pf2, int v, bool col);
27  // make the boolean resolution proof, where p1 corresponds to pf1, p2 corresponds to pf2
28  //res is the expression to resolve upon
29  static LFSCProof* Make( LFSCProof* p1, LFSCProof* p2, const Expr& res, const Expr& pf, bool cascadeOr = false );
30  //make the boolean resolution collection proof, where e is what to resolve
31  static LFSCProof* MakeC( LFSCProof* p, const Expr& res );
32  LFSCProof* clone() { return new LFSCBoolRes( d_children[0].get(), d_children[1].get(), d_var, d_col ); }
33  int getNumChildren() { return 2; }
34  LFSCProof* getChild( int n ) { return d_children[n].get(); }
35  int checkBoolRes( std::vector< int >& clause );
36 };
37 
38 class LFSCLem : public LFSCProof
39 {
40 private:
41  int d_var;
42  LFSCLem( int v ) : LFSCProof(),
43  d_var( v ) {}
44  virtual ~LFSCLem(){}
45  long int get_length() { return 10; }
46 public:
47  virtual LFSCLem* AsLFSCLem(){ return this; }
48  void print_pf( std::ostream& s, int ind = 0 ){ s << "(lem _ _ @a" << abs( d_var ) << ")"; }
49  void print_struct( std::ostream& s, int ind = 0 ){ s << "(lem " << d_var << ")"; }
50  static LFSCProof* Make(int v){ return new LFSCLem( v ); }
51  bool IsTrivial() { return true; }
52  LFSCProof* clone() { return new LFSCLem( d_var ); }
53  int checkBoolRes( std::vector< int >& clause ){
54  clause.push_back( -d_var );
55  clause.push_back( d_var );
56  return 0;
57  }
58 };
59 
60 class LFSCClausify : public LFSCProof
61 {
62 private:
63  friend class LFSCPrinter;
64  int d_var;
66  LFSCClausify( int v, LFSCProof* pf ) : LFSCProof(), d_var( v ), d_pf( pf ){}
67  virtual ~LFSCClausify(){}
68  long int get_length() { return 10 + d_pf->get_string_length(); }
69  //this should be called by Make
70  static LFSCProof* Make_i( const Expr& e, LFSCProof* p, std::vector< Expr >& exprs, const Expr& end );
71 public:
72  virtual LFSCClausify* AsLFSCClausify(){ return this; }
73  void print_pf( std::ostream& s, int ind = 0 );
74  void print_struct( std::ostream& s, int ind = 0 ){ s << "(clausify " << d_var << ")"; }
75  //standard Make
76  static LFSCProof* Make( int v, LFSCProof* pf ){ return new LFSCClausify( v, pf ); }
77  // input : a formula e, and a proof of that formula p.
78  static LFSCProof* Make( const Expr& e, LFSCProof* p, bool cascadeOr = false );
79  //clone
80  LFSCProof* clone() { return new LFSCClausify( d_var, d_pf.get() ); }
81  int getNumChildren() { return 1; }
82  LFSCProof* getChild( int n ) { return d_pf.get(); }
83  int checkBoolRes( std::vector< int >& clause ){
84  d_pf->checkBoolRes( clause );
85  clause.push_back( d_var );
86  return 0;
87  }
88 };
89 
90 class LFSCAssume : public LFSCProof {
91 private:
92  int d_var;
94  bool d_assm;
95  int d_type;
96  LFSCAssume( int v, LFSCProof* pf, bool assm, int type ) : LFSCProof(), d_var( v ), d_pf( pf ), d_assm( assm ), d_type( type ){}
97  virtual ~LFSCAssume(){}
98  long int get_length() { return 10 + d_pf->get_string_length(); }
99 public:
100  virtual LFSCAssume* AsLFSCAssume(){ return this; }
101  void print_pf( std::ostream& s, int ind = 0 );
102  void print_struct( std::ostream& s, int ind = 0 );
103  static LFSCProof* Make( int v, LFSCProof* pf, bool assm = true, int type=3 ){
104  return new LFSCAssume( v, pf, assm, type );
105  }
106  LFSCProof* clone() { return new LFSCAssume( d_var, d_pf.get(), d_assm, d_type ); }
107  int getNumChildren() { return 1; }
108  LFSCProof* getChild( int n ) { return d_pf.get(); }
109 
110  int checkBoolRes( std::vector< int >& clause ){
111  if( d_type==3 ){
112  d_pf->checkBoolRes( clause );
113  clause.push_back( -d_var );
114  }
115  return 0;
116  }
117 };
118 
119 #endif