CVC3  2.4.1
LFSCUtilProof.cpp
Go to the documentation of this file.
1 #include "LFSCUtilProof.h"
2 
3 #include "LFSCPrinter.h"
4 
5 //LFSCProofExpr ...
6 
9 }
10 
11 void LFSCProofExpr::print_pf( std::ostream& s, int ind ){
12  if( isHole )
13  s << "_";
14  else{
15  //HACK (forces unary minus to be printed properly)
16  //bool prev_cvc3_mimic = cvc3_mimic;
17  //cvc3_mimic = true;
18  printer->print_expr( d_e, s );
19  //cvc3_mimic = prev_cvc3_mimic;
20  }
21 }
22 
23 LFSCProofExpr::LFSCProofExpr( const Expr& e, bool isH ){
24  d_e = cascade_expr( e );
25  initialize();
26  isHole = isH;
27 }
28 
29 //LFSCPfVar ...
30 
31 std::map< int, RefPtr< LFSCProof > > LFSCPfVar::vMap;
32 
33 LFSCProof* LFSCPfVar::Make( const char* c, int v )
34 {
35  ostringstream os;
36  os << c << v;
37  return new LFSCPfVar( os.str() );
38 }
39 
41 {
42  RefPtr< LFSCProof > pf = vMap[v];
43  if( !pf.get() ){
44  pf = Make( "@v", v );
45  vMap[v] = pf.get();
46  }
47  return pf.get();
48 }
49 
50 //LFSCPfLambda ...
51 
52 void LFSCPfLambda::print_pf( std::ostream& s, int ind )
53 {
54  if( abstVal.get() ){
56  }
57  s << "(\\ ";
58  pfV->print( s );
59  //s << " _ (: bottom ";
60  s << " ";
61  body->print( s );
62  s << ")";
63  if( abstVal.get() ){
64  lambdaPrintMap[abstVal.get()] = NULL;
65  }
66 }
67 
68 //LFSCProofGeneric ...
69 
71  long int sum = 0;
72  for( int a=0; a<(int)d_str.size(); a++ ){
73  if( !debug_str )
74  sum += d_str[a].length();
75  if( a<(int)d_pf.size() )
76  sum += d_pf[a]->get_string_length();
77  }
78  return sum;
79 }
80 
81 void LFSCProofGeneric::print_pf( std::ostream& s, int ind ){
82  for( int a=0; a<(int)d_str.size(); a++ ){
83  s << d_str[a];
84  if( a<(int)d_pf.size() ){
85  d_pf[a]->print( s, d_pf.size()<3 ? ind+1 : 0 );
86  }
87  }
88 }
89 
90 LFSCProof* LFSCProofGeneric::Make( string str_pre, LFSCProof* sub_pf, string str_post, bool db_str )
91 {
92  vector< RefPtr< LFSCProof > > d_pfs;
93  d_pfs.push_back( sub_pf );
94  vector< string > d_strs;
95  d_strs.push_back( str_pre );
96  d_strs.push_back( str_post );
97  return new LFSCProofGeneric( d_pfs, d_strs, db_str );
98 }
99 
100 LFSCProof* LFSCProofGeneric::Make( string str_pre, LFSCProof* sub_pf1, LFSCProof* sub_pf2, string str_post, bool db_str )
101 {
102  vector< RefPtr< LFSCProof > > d_pfs;
103  d_pfs.push_back( sub_pf1 );
104  d_pfs.push_back( sub_pf2 );
105  vector< string > d_strs;
106  string str_empty(" ");
107  d_strs.push_back( str_pre );
108  d_strs.push_back( str_empty );
109  d_strs.push_back( str_post );
110  return new LFSCProofGeneric( d_pfs, d_strs, db_str );
111 }
112 
113 LFSCProof* LFSCProofGeneric::MakeStr( const char* c, bool db_str)
114 {
115  vector< RefPtr< LFSCProof > > d_pfs;
116  vector< string > d_strs;
117  string str( c );
118  d_strs.push_back( str );
119  return new LFSCProofGeneric( d_pfs, d_strs, db_str );
120 }
121 
122 //LFSCPfLet
123 
125  bool isTh, std::vector< int >& fv ) : LFSCProof(), d_letPf( letPf ),
126  d_pv( pv ),d_body( body ),d_isTh( isTh ){
127  d_letPfRpl = letPf;
128  d_pvRpl = pv;
129 #ifndef IGNORE_LETPF_VARS
130  //modify letPf and rpl based on fv
131  for(int a=0; a<(int)fv.size(); a++ ){
132  ostringstream os1, os2;
133  //if( d_isTh ){
134  os1 << "(impl_intro _ _ ";
135  os2 << ")";
136  //}else{
137  //}
138  RefPtr< LFSCProof > pv1 = LFSCPfVar::Make( "@@v", abs( fv[a] ) );
139  RefPtr< LFSCProof > pv2 = LFSCPfVar::MakeV( abs( fv[a] ) );
141  d_letPfRpl = LFSCProofGeneric::Make( os1.str(), d_letPfRpl.get(), os2.str() );
142  }
143  for( int a=(int)fv.size()-1; a>=0; a-- ){
144  ostringstream os1, os2;
145  os1 << "(impl_elim _ _ ";
146  os2 << ")";
147  RefPtr< LFSCProof > pv2 = LFSCPfVar::MakeV( abs( fv[a] ) );
148  d_pvRpl = LFSCProofGeneric::Make( os1.str(), pv2.get(), d_pvRpl.get(), os2.str() );
149  }
150 #endif
151 }
152 
153 void LFSCPfLet::print_pf( std::ostream& s, int ind ){
154  //fill holes if this proof is already abstracted
155  if( d_pvRpl.get()!=d_pv.get() ){
157  }
158  s << "(" << (d_isTh ? "th_let_pf _ " : "satlem _ _ _ " );
159  d_letPfRpl->print( s );
160  s << "(\\ ";
161  d_pv->print( s );
162  s << " " << endl;
164  d_body->print( s, ind );
165  lambdaPrintMap[d_letPf.get()]=NULL;
166  s << "))";
167 }
168 
169 void LFSCPfLet::print_struct( std::ostream& s, int ind ){
170  s << "(satlem ";
171  d_letPf->print_structure( s, ind+1 );
172  s << "(\\ ";
173  d_pv->print_structure( s );
174  s << " ";
176  d_body->print_structure( s, ind+1 );
177  lambdaPrintMap[d_letPf.get()]=NULL;
178  s << ")";
179 }
void print_structure(std::ostream &s, int ind=0)
Definition: LFSCProof.cpp:43
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 Expr cascade_expr(const Expr &e)
Definition: LFSCObject.cpp:281
void print_pf(std::ostream &s, int ind)
long int get_string_length()
Definition: LFSCProof.h:73
RefPtr< LFSCPfVar > pfV
Definition: LFSCUtilProof.h:41
void print_expr(const Expr &expr, std::ostream &s)
Definition: LFSCPrinter.h:35
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)
static LFSCPrinter * printer
Definition: LFSCObject.h:16
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
static LFSCProof * MakeV(int v)
RefPtr< LFSCProof > abstVal
Definition: LFSCUtilProof.h:44
T * get()
Definition: Object.h:56
LFSCPfVar(string nm)
Definition: LFSCUtilProof.h:27
LFSCPfLet(LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, LFSCProof *letPfRpl, LFSCProof *pvRpl)
static std::map< LFSCProof *, LFSCProof * > lambdaPrintMap
Definition: LFSCProof.h:30
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 print_pf(std::ostream &s, int ind=0)
RefPtr< LFSCProof > body
Definition: LFSCUtilProof.h:42
T abs(T t)
Definition: cvc_util.h:53
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)
RefPtr< LFSCProof > d_letPfRpl
RefPtr< LFSCProof > d_pvRpl
virtual void fillHoles()
Definition: LFSCProof.cpp:61
RefPtr< LFSCPfVar > d_pv
Definition: LFSCUtilProof.h:98
static LFSCProof * Make(LFSCPfVar *v, LFSCProof *bd, LFSCProof *aVal=NULL)
Definition: LFSCUtilProof.h:53
void set_print_expr(const Expr &expr)
Definition: LFSCPrinter.h:33
vector< RefPtr< LFSCProof > > d_pf
Definition: LFSCUtilProof.h:63
long int get_length()
void print(std::ostream &s, int ind=0)
Definition: LFSCProof.cpp:23
void print_pf(std::ostream &s, int ind=0)