CVC3  2.4.1
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
RefPtr< LFSCProof > d_pf
Definition: LFSCBoolProof.h:93
void print_struct(std::ostream &s, int ind=0)
RefPtr< LFSCProof > d_pf
Definition: LFSCBoolProof.h:65
virtual ~LFSCLem()
Definition: LFSCBoolProof.h:44
LFSCClausify(int v, LFSCProof *pf)
Definition: LFSCBoolProof.h:66
Data structure of expressions in CVC3.
Definition: expr.h:133
long int get_length()
Definition: LFSCBoolProof.h:68
LFSCBoolRes(LFSCProof *pf1, LFSCProof *pf2, int v, bool col)
Definition: LFSCBoolProof.h:12
int checkBoolRes(std::vector< int > &clause)
virtual LFSCLem * AsLFSCLem()
Definition: LFSCBoolProof.h:47
void print_pf(std::ostream &s, int ind=0)
LFSCProof * clone()
long int get_string_length()
Definition: LFSCProof.h:73
void print_struct(std::ostream &s, int ind=0)
Definition: LFSCBoolProof.h:49
LFSCAssume(int v, LFSCProof *pf, bool assm, int type)
Definition: LFSCBoolProof.h:96
LFSCProof * clone()
Definition: LFSCBoolProof.h:80
int getNumChildren()
Definition: LFSCBoolProof.h:33
void print_struct(std::ostream &s, int ind=0)
Definition: LFSCBoolProof.h:74
virtual ~LFSCBoolRes()
Definition: LFSCBoolProof.h:17
long int get_length()
Definition: LFSCBoolProof.h:98
void print_pf(std::ostream &s, int ind=0)
Definition: LFSCBoolProof.h:48
T * get()
Definition: Object.h:56
int checkBoolRes(std::vector< int > &clause)
Definition: LFSCBoolProof.h:83
virtual LFSCAssume * AsLFSCAssume()
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int v, bool col)
virtual ~LFSCClausify()
Definition: LFSCBoolProof.h:67
static LFSCProof * Make_i(const Expr &e, LFSCProof *p, std::vector< Expr > &exprs, const Expr &end)
void print_pf(std::ostream &s, int ind=0)
long int get_length()
Definition: LFSCBoolProof.h:45
virtual int checkBoolRes(std::vector< int > &clause)
Definition: LFSCProof.h:105
int getNumChildren()
T abs(T t)
Definition: cvc_util.h:53
void print_struct(std::ostream &s, int ind=0)
static LFSCProof * Make(int v, LFSCProof *pf)
Definition: LFSCBoolProof.h:76
RefPtr< LFSCProof > d_children[2]
Definition: LFSCBoolProof.h:9
LFSCLem(int v)
Definition: LFSCBoolProof.h:42
virtual LFSCBoolRes * AsLFSCBoolRes()
Definition: LFSCBoolProof.h:22
void print_pf(std::ostream &s, int ind=0)
LFSCProof * getChild(int n)
LFSCProof * clone()
Definition: LFSCBoolProof.h:32
LFSCProof * clone()
Definition: LFSCBoolProof.h:52
int checkBoolRes(std::vector< int > &clause)
virtual ~LFSCAssume()
Definition: LFSCBoolProof.h:97
int getNumChildren()
Definition: LFSCBoolProof.h:81
bool IsTrivial()
Definition: LFSCBoolProof.h:51
LFSCProof * getChild(int n)
Definition: LFSCBoolProof.h:82
int checkBoolRes(std::vector< int > &clause)
Definition: LFSCBoolProof.h:53
static LFSCProof * Make(int v)
Definition: LFSCBoolProof.h:50
LFSCProof * getChild(int n)
Definition: LFSCBoolProof.h:34
virtual LFSCClausify * AsLFSCClausify()
Definition: LFSCBoolProof.h:72
static LFSCProof * Make(int v, LFSCProof *pf, bool assm=true, int type=3)
static LFSCProof * MakeC(LFSCProof *p, const Expr &res)
long int get_length()
Definition: LFSCBoolProof.h:18