CVC3  2.4.1
LFSCUtilProof.h
Go to the documentation of this file.
1 #ifndef LFSC_UTIL_PROOF_H_
2 #define LFSC_UTIL_PROOF_H_
3 
4 #include "LFSCProof.h"
5 
6 class LFSCProofExpr : public LFSCProof
7 {
8  bool isHole;
10  LFSCProofExpr( const Expr& e, bool isH = false );
11  void initialize();
12  virtual ~LFSCProofExpr(){}
13  long int get_length() { return 10; }
14 public:
15  virtual LFSCProofExpr* AsLFSCProofExpr(){ return this; }
16  void print_pf( std::ostream& s, int ind );
17  static LFSCProof* Make( const Expr& e, bool isH = false ) { return new LFSCProofExpr( e, isH ); }
18  LFSCProof* clone() { return new LFSCProofExpr( d_e, isHole ); }
19 
20  void fillHoles() { isHole = false; }
21 };
22 
23 class LFSCPfVar : public LFSCProof {
24 private:
25  static std::map< int, RefPtr< LFSCProof > > vMap;
26  string name;
27  LFSCPfVar( string nm ) : LFSCProof(), name( nm ){}
28  virtual ~LFSCPfVar(){}
29  long int get_length() { return name.length(); }
30 public:
31  virtual LFSCPfVar* AsLFSCPfVar(){ return this; }
32  void print_pf( std::ostream& s, int ind = 0 ){ s << name; }
33  void print_struct( std::ostream& s, int ind = 0 ){ s << name; }
34  static LFSCProof* Make( const char* c, int v );
35  static LFSCProof* MakeV( int v );
36  LFSCProof* clone() { return new LFSCPfVar( name ); }
37 };
38 
39 class LFSCPfLambda : public LFSCProof {
40 private:
43  //just a placeholder. This is what the lambda abstracts.
45  //constructor
46  LFSCPfLambda( LFSCPfVar* v, LFSCProof* bd, LFSCProof* aVal = NULL ) : LFSCProof(),
47  pfV( v ), body( bd ), abstVal( aVal ){}
48  virtual ~LFSCPfLambda(){}
49  long int get_length() { return 5 + pfV->get_string_length() + body->get_string_length(); }
50 public:
51  virtual LFSCPfLambda* AsLFSCPfLambda(){ return this; }
52  void print_pf( std::ostream& s, int ind = 0 );
53  static LFSCProof* Make( LFSCPfVar* v, LFSCProof* bd, LFSCProof* aVal = NULL ){
54  return new LFSCPfLambda( v, bd, aVal );
55  }
56  LFSCProof* clone() { return new LFSCPfLambda( pfV.get(), body.get(), abstVal.get() ); }
57  int getNumChildren() { return 2; }
58  LFSCProof* getChild( int n ) { return (n==0) ? (LFSCProof*)pfV.get() : body.get(); }
59 };
60 //
61 class LFSCProofGeneric : public LFSCProof{
62 private:
63  vector< RefPtr< LFSCProof > > d_pf;
64  vector< string > d_str;
65  bool debug_str;
66  //Proof in the form "S1.print(P1).S2.print(P2).....print(Pn).S{n+1}"
67  LFSCProofGeneric( vector< RefPtr< LFSCProof > >& d_pfs, vector< string >& d_strs, bool db_str = false ) : LFSCProof(){
68  for( int a=0; a<(int)d_pfs.size(); a++ )
69  d_pf.push_back( d_pfs[a].get() );
70  for( int a=0; a<(int)d_strs.size(); a++ )
71  d_str.push_back( d_strs[a] );
72  debug_str = db_str;
73  }
74  virtual ~LFSCProofGeneric(){}
75  long int get_length();
76 public:
77  virtual LFSCProofGeneric* AsLFSCProofGeneric(){ return this; }
78  void print_pf( std::ostream& s, int ind = 0 );
79  //Proof in the form "S1.print(P1).S2.print(P2).....print(Pn).S{n+1}"
80  static LFSCProof* Make( vector< RefPtr< LFSCProof > >& d_pfs, std::vector< string >& d_strs, bool db_str = false ){
81  return new LFSCProofGeneric( d_pfs, d_strs, db_str );
82  }
83  //proof printed in the form "S1.print(P1).S2"
84  static LFSCProof* Make( string str_pre, LFSCProof* sub_pf, string str_post, bool db_str = false );
85  //proof printed in the form "S1.print(P1).print(P2).S2"
86  static LFSCProof* Make( string str_pre, LFSCProof* sub_pf1, LFSCProof* sub_pf2, string str_post, bool db_str = false );
87  static LFSCProof* MakeStr( const char* c, bool db_str = false );
88  static LFSCProof* MakeUnk(){ return MakeStr( "unk" ); }
90  int getNumChildren() { return (int)d_pf.size(); }
91  LFSCProof* getChild( int n ) { return d_pf[n].get(); }
92 };
93 
94 
95 class LFSCPfLet : public LFSCProof{
96 private:
100  //this should be equal to d_letPf, although it could be something else based on fv
102  //this by default is d_pv, although it could be something else based on fv
104  bool d_isTh;
105  LFSCPfLet( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body,
106  bool isTh, LFSCProof* letPfRpl, LFSCProof* pvRpl ) : LFSCProof(),
107  d_letPf( letPf ),d_pv( pv ),d_body( body ),d_letPfRpl( letPfRpl ),d_pvRpl( pvRpl ),d_isTh( isTh ){}
108  LFSCPfLet( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body,
109  bool isTh, std::vector< int >& fv );
110  virtual ~LFSCPfLet(){}
111  long int get_length() {
113  }
114 public:
115  virtual LFSCPfLet* AsLFSCPfLet(){ return this; }
116  void print_pf( std::ostream& s, int ind = 0 );
117  void print_struct( std::ostream& s, int ind = 0 );
118  static LFSCProof* Make( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body,
119  bool isTh, std::vector< int >& fv ){
120  return new LFSCPfLet( letPf, pv, body, isTh, fv );
121  }
122  LFSCProof* clone() { return new LFSCPfLet( d_letPf.get(), d_pv.get(), d_body.get(),
123  d_isTh, d_letPfRpl.get(), d_pvRpl.get() ); }
124  //should not be part of the children structure.
125 };
126 
127 
128 #endif