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" ); }
89  LFSCProof* clone(){ return new LFSCProofGeneric( d_pf, d_str, debug_str ); }
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() {
112  return 10 + d_letPf->get_string_length() + d_pv->get_string_length() + d_body->get_string_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
virtual LFSCProofExpr * AsLFSCProofExpr()
Definition: LFSCUtilProof.h:15
RefPtr< LFSCProof > d_body
Definition: LFSCUtilProof.h:99
Data structure of expressions in CVC3.
Definition: expr.h:133
LFSCProofExpr(const Expr &e, bool isH=false)
static LFSCProof * Make(LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, std::vector< int > &fv)
LFSCProof * getChild(int n)
Definition: LFSCUtilProof.h:58
static LFSCProof * MakeUnk()
Definition: LFSCUtilProof.h:88
void print_pf(std::ostream &s, int ind)
LFSCProof * clone()
Definition: LFSCUtilProof.h:36
long int get_string_length()
Definition: LFSCProof.h:73
LFSCPfLambda(LFSCPfVar *v, LFSCProof *bd, LFSCProof *aVal=NULL)
Definition: LFSCUtilProof.h:46
LFSCProof * getChild(int n)
Definition: LFSCUtilProof.h:91
long int get_length()
Definition: LFSCUtilProof.h:13
RefPtr< LFSCPfVar > pfV
Definition: LFSCUtilProof.h:41
static LFSCProof * Make(const Expr &e, bool isH=false)
Definition: LFSCUtilProof.h:17
string name
Definition: LFSCUtilProof.h:26
virtual LFSCProofGeneric * AsLFSCProofGeneric()
Definition: LFSCUtilProof.h:77
LFSCProofGeneric(vector< RefPtr< LFSCProof > > &d_pfs, vector< string > &d_strs, bool db_str=false)
Definition: LFSCUtilProof.h:67
static LFSCProof * Make(const char *c, int v)
virtual ~LFSCPfVar()
Definition: LFSCUtilProof.h:28
virtual ~LFSCPfLet()
virtual ~LFSCProofExpr()
Definition: LFSCUtilProof.h:12
void print_pf(std::ostream &s, int ind=0)
Definition: LFSCUtilProof.h:32
static LFSCProof * MakeV(int v)
RefPtr< LFSCProof > abstVal
Definition: LFSCUtilProof.h:44
T * get()
Definition: Object.h:56
long int get_length()
Definition: LFSCUtilProof.h:29
LFSCPfVar(string nm)
Definition: LFSCUtilProof.h:27
LFSCProof * clone()
Definition: LFSCUtilProof.h:56
LFSCPfLet(LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, LFSCProof *letPfRpl, LFSCProof *pvRpl)
virtual ~LFSCPfLambda()
Definition: LFSCUtilProof.h:48
static std::map< int, RefPtr< LFSCProof > > vMap
Definition: LFSCUtilProof.h:25
vector< string > d_str
Definition: LFSCUtilProof.h:64
static LFSCProof * Make(vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false)
Definition: LFSCUtilProof.h:80
void fillHoles()
Definition: LFSCUtilProof.h:20
void print_pf(std::ostream &s, int ind=0)
long int get_length()
Definition: LFSCUtilProof.h:49
RefPtr< LFSCProof > body
Definition: LFSCUtilProof.h:42
void print_struct(std::ostream &s, int ind=0)
RefPtr< LFSCProof > d_letPf
Definition: LFSCUtilProof.h:97
static LFSCProof * MakeStr(const char *c, bool db_str=false)
void print_pf(std::ostream &s, int ind=0)
virtual ~LFSCProofGeneric()
Definition: LFSCUtilProof.h:74
RefPtr< LFSCProof > d_letPfRpl
RefPtr< LFSCProof > d_pvRpl
RefPtr< LFSCPfVar > d_pv
Definition: LFSCUtilProof.h:98
void print_struct(std::ostream &s, int ind=0)
Definition: LFSCUtilProof.h:33
static LFSCProof * Make(LFSCPfVar *v, LFSCProof *bd, LFSCProof *aVal=NULL)
Definition: LFSCUtilProof.h:53
vector< RefPtr< LFSCProof > > d_pf
Definition: LFSCUtilProof.h:63
long int get_length()
int getNumChildren()
Definition: LFSCUtilProof.h:57
void print_pf(std::ostream &s, int ind=0)
long int get_length()
LFSCProof * clone()
Definition: LFSCUtilProof.h:18
virtual LFSCPfVar * AsLFSCPfVar()
Definition: LFSCUtilProof.h:31
virtual LFSCPfLambda * AsLFSCPfLambda()
Definition: LFSCUtilProof.h:51
LFSCProof * clone()
Definition: LFSCUtilProof.h:89
virtual LFSCPfLet * AsLFSCPfLet()
LFSCProof * clone()