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 }