CVC3  2.4.1
LFSCProof.cpp
Go to the documentation of this file.
1 #include "LFSCProof.h"
2 
3 #include "LFSCBoolProof.h"
4 #include "LFSCUtilProof.h"
5 
7 std::map< LFSCProof*, int > LFSCProof::lambdaMap;
8 std::map< LFSCProof*, LFSCProof* > LFSCProof::lambdaPrintMap;
10 
12 {
13  pf_counter++;
14  printCounter = 0;
15  strLen = -1;
16  rplProof = NULL;
17  chOp = -1;
18  brComputed = false;
19  assumeVar = -1;
20  assumeVarUsed = -1;
21 }
22 
23 void LFSCProof::print( std::ostream& s, int ind ){
25  if( p ){
26  p->print( s, ind );
27  }else{
28  if( lambdaMap.find( this )!=lambdaMap.end() && printCounter>0 ){
29  print_warning( "Warning: printing out lambda abstracted proof more than once");
30 #ifdef IGNORE_PRINT_MULTI_LAMBDA
31  return;
32 #endif
33  }
34  //if( printCounter>0 ){
35  // return;
36  //}
37  printCounter++;
38  indent( s, ind );
39  print_pf( s, ind );
40  }
41 }
42 
43 void LFSCProof::print_structure( std::ostream& s, int ind ){
45  if( p ){
46  p->print( s, ind );
47  }else{
48  indent( s, ind );
49  if( lambdaMap.find( this )!=lambdaMap.end() && printCounter>0 ){
50  //just a warning, print it out in ose
51  print_warning( "ERROR: printing out lambda abstracted proof more than once" );
52 #ifdef IGNORE_PRINT_MULTI_LAMBDA
53  return;
54 #endif
55  }
56  printCounter++;
57  print_struct( s, ind );
58  }
59 }
60 
62  //if( !is_lambda() ){
63  for( int a=0; a<getNumChildren(); a++ ){
64  getChild( a )->fillHoles();
65  }
66  //}
67 }
68 
69 #ifdef OPTIMIZE
70 void LFSCProof::calcL( std::vector< int >& lget, std::vector< int >& lgetu ){
71  for( int a=0; a<getNumChildren(); a++ ){
72  getChild( a )->calcL( lget, lgetu );
73  }
74  if( assumeVar!=-1 && std::find( lget.begin(), lget.end(), assumeVar )==lget.end() ){
75  lget.push_back( assumeVar );
76  }
77  if( assumeVarUsed!=-1 && std::find( lgetu.begin(), lgetu.end(), assumeVarUsed )==lgetu.end() ){
78  lgetu.push_back( assumeVarUsed );
79  }
80 }
81 #endif
82 
84  if( chOp!=-1 )
85  return chOp;
86  if( getNumChildren()==1 )
87  return getChild( 0 )->checkOp();
88  else{
89  int ret = -1;
90  for( int a=0; a<getNumChildren(); a++ ){
91  int o = getChild( a )->checkOp();
92  if( a!=-1 ){
93  if( ret==-1 )
94  ret = a;
95  else
96  return -1;
97  }
98  }
99  //cout << "fail case " << getNumChildren() << std::endl;
100  return ret;
101  }
102 }
103 
104 LFSCProof* LFSCProof::Make_CNF( const Expr& form, const Expr& reason, int pos )
105 {
106  Expr ec = cascade_expr( form );
107 #ifdef PRINT_MAJOR_METHODS
108  cout << ";[M] CNF " << reason << " " << pos << std::endl;
109 #endif
110  int m = queryM( ec );
111  if( m>0 )
112  {
113  ostringstream os1;
114  ostringstream os2;
116  if( reason==d_or_final_s )
117  {
118 #if 0
119  //this is the version that cascades
120  //make the proof for the or
121  p = LFSCPfVar::Make( "@v", abs(m) );
122  //clausify the or statement
123  p = LFSCClausify::Make( ec, p.get(), true );
124  //return
125  return LFSCAssume::Make( m, p.get(), true );
126 #else
127  //this is the version that does not expand the last
128  ostringstream oss1, oss2;
129  p = LFSCPfVar::Make( "@v", abs(m) );
130  for( int a=(form.arity()-2); a>=0; a-- ){
131  int m1 = queryM( form[a] );
132  oss1 << "(or_elim_1 _ _ ";
133  oss1 << ( m1<0 ? "(not_not_intro _ " : "" );
134  oss1 << "@v" << abs( m1 );
135  oss1 << ( m1<0 ? ") " : " " );
136  oss2 << ")";
137  }
138  p = LFSCProofGeneric::Make( oss1.str(), p.get(), oss2.str() );
139  //p = LFSCClausify::Make( form[form.arity()-1], p.get() );
140  p = LFSCClausify::Make( queryM( form[form.arity()-1] ), p.get() );
141  for( int a=0; a<(form.arity()-1); a++ ){
142  p = LFSCAssume::Make( queryM( form[a] ), p.get(), false );
143  }
144  return LFSCAssume::Make( m, p.get() );
145 #endif
146  }
147  else if( reason==d_and_final_s )
148  {
149 #if 1
150  //this is the version that does not expand the last
151  p = LFSCPfVar::Make( "@v", abs(m) );
152  os1 << "(contra _ ";
153  for( int a=0; a<form.arity(); a++ ){
154  if( a<(form.arity()-1))
155  os1 << "(and_intro _ _ ";
156  os1 << "@v" << abs( queryM( form[a] ) );
157  if( a<(form.arity()-1)){
158  os1 << " ";
159  os2 << ")";
160  }
161  }
162  os2 << " @v" << abs(m) << ")";
163  os1 << os2.str();
164  p = LFSCProofGeneric::MakeStr( os1.str().c_str() );
165  for( int a=0; a<form.arity(); a++ ){
166  p = LFSCAssume::Make( queryM( form[a] ), p.get() );
167  }
168  return LFSCAssume::Make( m, p.get(), false );
169 #else
170  //this is the version that cascades
171  std::vector< Expr > assumes;
172  Expr ce = cascade_expr( form );
173  Expr curr = ce;
174  os1 << "(contra _ ";
175  while( curr.getKind()==AND ){
176  os1 << "(and_intro _ _ ";
177  os1 << "@v" << abs( queryM( curr[0] ) ) << " ";
178  os2 << ")";
179  assumes.push_back( curr[0] );
180  curr = curr[1];
181  }
182  os2 << " @v" << abs(m) << ")";
183  p = LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() );
184  for( int a=0; a<(int)assumes.size(); a++ ){
185  p = LFSCAssume::Make( queryM( assumes[a] ), p.get() );
186  }
187  return LFSCAssume::Make( m, p.get(), false );
188 #endif
189  }
190  else if( reason==d_imp_s )
191  {
192  int m1 = queryM( ec[0] );
193  int m2 = queryM( ec[1] );
194  switch( pos )
195  {
196  case 0:
197 
198  break;
199  case 1:
200 
201  break;
202  case 2:
203  {
204  //make a proof of the RHS
205  ostringstream os;
206  os << "(impl_elim _ _ @v" << abs( m1 ) << " @v" << abs( m ) << ")";
207  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
208  //clausify the RHS
209  p = LFSCClausify::Make( form[1], p.get() ); //cascadeOr?
210  p = LFSCAssume::Make( queryM( ec[0] ), p.get() );
211  return LFSCAssume::Make( queryM( ec ), p.get() );
212  }
213  break;
214  }
215  }
216  else if( reason==d_ite_s )
217  {
218  int m1 = queryM( ec[0] );
219  int m2 = queryM( ec[1] );
220  switch( pos )
221  {
222  case 1:
223  {
224  ostringstream os;
225  os << "(ite_elim_2" << (m1<0 ? "n" : "" );
226  os << " _ _ _ @v" << abs( m1 ) << " @v" << abs( m ) << ")";
227  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
228  p = LFSCClausify::Make( form[2], p.get() );
229  p = LFSCAssume::Make( queryM( ec[0] ), p.get(), false );
230  return LFSCAssume::Make( queryM( ec ), p.get() );
231  }
232  break;
233  case 2:
234  {
235  ostringstream os;
236  os << "(not_ite_elim_2 _ _ _ @v" << (m1<0 ? "n" : "" );
237  os << abs( m1 ) << " @v" << abs( m ) << ")";
238  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
239  Expr e = Expr( NOT, form[2] );
240  p = LFSCClausify::Make( e, p.get() );
241  p = LFSCAssume::Make( queryM( ec[0] ), p.get(), false );
242  return LFSCAssume::Make( queryM( ec ), p.get(), false );
243  }
244  break;
245  case 3:
246  {
247  ostringstream os;
248  os << "(not_ite_elim_1 _ _ _ @v" << abs( m1 ) << " @v" << abs( m ) << ")";
249  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
250  Expr e = Expr( NOT, form[1] );
251  p = LFSCClausify::Make( e, p.get() );
252  p = LFSCAssume::Make( queryM( ec[0] ), p.get() );
253  return LFSCAssume::Make( queryM( ec ), p.get(), false );
254  }
255  break;
256  case 4:
257  {
258  ostringstream os;
259  os << "(ite_elim_1";// << (m1<0 ? "n" : "" );
260  os << " _ _ _ @v" << abs( m1 ) << " @v" << abs( m ) << ")";
261  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
262  p = LFSCClausify::Make( form[1], p.get() );
263  p = LFSCAssume::Make( queryM( ec[0] ), p.get() );
264  return LFSCAssume::Make( queryM( ec ), p.get() );
265  }
266  break;
267  case 5:
268  {
269  ostringstream os;
270  os << "(not_ite_elim_3 _ _ _ @v" << abs( m2 ) << " @v" << abs( m ) << ")";
271  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
272  Expr e = Expr( NOT, form[2] );
273  p = LFSCClausify::Make( e, p.get() );
274  p = LFSCAssume::Make( queryM( ec[1] ), p.get() );
275  return LFSCAssume::Make( queryM( ec ), p.get(), false );
276  }
277  break;
278  case 6:
279  {
280  ostringstream os;
281  os << "(ite_elim_3";// << (m1<0 ? "n" : "" );
282  os << " _ _ _ @v" << abs( m2 ) << " @v" << abs( m ) << ")";
283  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
284  p = LFSCClausify::Make( form[2], p.get() );
285  p = LFSCAssume::Make( queryM( ec[1] ), p.get(), false );
286  return LFSCAssume::Make( queryM( ec ), p.get() );
287  }
288  break;
289  }
290  }
291  else if( reason==d_iff_s )
292  {
293  int m1 = queryM( ec[0] );
294  int m2 = queryM( ec[1] );
295  switch( pos )
296  {
297  case 0:
298  {
299  ostringstream os;
300  os << "(not_iff_elim_1 _ _ @v" << abs( m1 ) << " @v" << abs( m ) << ")";
301  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
302  p = LFSCClausify::Make( form[1], p.get() );
303  p = LFSCAssume::Make( queryM( ec[0] ), p.get(), false );
304  return LFSCAssume::Make( queryM( ec ), p.get(), false );
305  }
306  break;
307  case 1:
308  {
309  ostringstream os;
310  os << "(not_iff_elim_2 _ _ @v" << abs( m1 ) << " @v" << abs( m ) << ")";
311  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
312  p = LFSCClausify::Make( Expr( NOT, form[1] ), p.get() );
313  p = LFSCAssume::Make( queryM( ec[0] ), p.get() );
314  return LFSCAssume::Make( queryM( ec ), p.get(), false );
315  }
316  break;
317  case 2:
318  {
319  ostringstream os;
320  os << "(impl_elim _ _ @v" << abs( m1 ) << "(iff_elim_1 _ _ @v" << abs( m ) << "))";
321  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
322  //clausify the RHS
323  p = LFSCClausify::Make( form[1], p.get() ); //cascadeOr?
324  p = LFSCAssume::Make( queryM( ec[0] ), p.get() );
325  return LFSCAssume::Make( queryM( ec ), p.get() );
326  }
327  break;
328  case 3:
329  {
330  ostringstream os;
331  os << "(impl_elim _ _ @v" << abs( m2 ) << "(iff_elim_2 _ _ @v" << abs( m ) << "))";
332  p = LFSCProofGeneric::MakeStr( os.str().c_str() );
333  //clausify the RHS
334  p = LFSCClausify::Make( form[0], p.get() ); //cascadeOr?
335  p = LFSCAssume::Make( queryM( ec[1] ), p.get() );
336  return LFSCAssume::Make( m, p.get() );
337  }
338  break;
339  }
340  }
341  else if( reason==d_or_mid_s )
342  {
343  ostringstream os1, os2;
344  if( form[pos].isNot() )
345  os1 << "(not_not_elim _ ";
346  os1 << "(or_elim" << ( (pos==form.arity()) ? "_end" : "" );
347  os1 << " _ _ " << pos << " ";
348  os2 << ")";
349  if( form[pos].isNot() )
350  os2 << ")";
351  p = LFSCPfVar::Make( "@v", abs( m ) );
352  p = LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() );
353  Expr ea = Expr( NOT, form[pos] );
354  p = LFSCClausify::Make( ea, p.get() );
355  return LFSCAssume::Make( m, p.get(), false );
356  }
357  else if( reason==d_and_mid_s )
358  {
359  //make a proof of the pos-th statement
360  p = LFSCPfVar::Make( "@v", abs( m ) );
361  p = LFSCProof::Make_and_elim( form, p.get(), pos, form[pos] );
362  p = LFSCClausify::Make( form[pos], p.get() );
363  return LFSCAssume::Make( m, p.get() );
364  }
365  }
366  ostringstream ose;
367  ose << "CNF, " << reason << " unknown position = " << pos << std::endl;
368  print_error( ose.str().c_str(), cout );
369  return NULL;
370 }
371 
373 {
374  if( pf.isNot() && pf[0].isNot() ){
375  p = Make_not_not_elim( pf[0][0], p );
376  ostringstream os1, os2;
377  os1 << "(not_not_elim _ ";
378  os2 << ")";
379  p = LFSCProofGeneric::Make( os1.str(), p, os2.str() );
380  }
381  return p;
382 }
383 
384 LFSCProof* LFSCProof::Make_mimic( const Expr& pf, LFSCProof* p, int numHoles )
385 {
386  ostringstream os1, os2;
387  os1 << "(";
388  os1 << pf[0];
389  for( int a=0; a<numHoles; a++ )
390  os1 << " _";
391  os1 << " ";
392  os2 << ")";
393  return LFSCProofGeneric::Make( os1.str(), p, os2.str() );
394 }
395 
396 //input should be in non-cascaded form
397 LFSCProof* LFSCProof::Make_and_elim( const Expr& form, LFSCProof* p, int n, const Expr& expected )
398 {
399  Expr e = cascade_expr( form );
400  for( int a=0; a<n; a++ ){
401  if( e.arity()==2 ){
402  e = e[1];
403  }else{
404  print_error( "WARNING: and elim out of range", cout );
405  }
406  }
407  if( form.arity()>1 )
408  {
409  ostringstream os1, os2;
410  os1 << "(and_elim";
411  if( n==form.arity()-1 )
412  os1 << "_end";
413  os1 << " _ _ " << n << " ";
414  os2 << ")";
415  return LFSCProofGeneric::Make( os1.str(), p, os2.str() );
416  }
417  else
418  {
419  return p;
420  }
421 }
422 
int arity() const
Definition: expr.h:1201
void print_structure(std::ostream &s, int ind=0)
Definition: LFSCProof.cpp:43
static Expr d_or_final_s
Definition: LFSCObject.h:158
Data structure of expressions in CVC3.
Definition: expr.h:133
static int pf_counter
Definition: LFSCProof.h:28
static Expr cascade_expr(const Expr &e)
Definition: LFSCObject.cpp:281
static Expr d_ite_s
Definition: LFSCObject.h:160
static int queryM(const Expr &expr, bool add=true, bool trusted=false)
Definition: LFSCObject.cpp:386
virtual int getNumChildren()
Definition: LFSCProof.h:100
int chOp
Definition: LFSCProof.h:35
static LFSCProof * Make_CNF(const Expr &form, const Expr &reason, int pos)
Definition: LFSCProof.cpp:104
int assumeVar
Definition: LFSCProof.h:36
Definition: kinds.h:66
static Expr d_or_mid_s
Definition: LFSCObject.h:163
static LFSCProof * Make(const char *c, int v)
long int strLen
Definition: LFSCProof.h:34
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void indent(std::ostream &s, int ind=0)
Definition: Object.h:73
bool brComputed
Definition: LFSCProof.h:40
static void print_error(const char *c, std::ostream &s)
Definition: Object.h:95
T * get()
Definition: Object.h:56
bool isNot() const
Definition: expr.h:420
static std::map< LFSCProof *, LFSCProof * > lambdaPrintMap
Definition: LFSCProof.h:30
static LFSCProof * Make(vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false)
Definition: LFSCUtilProof.h:80
static Expr d_and_final_s
Definition: LFSCObject.h:159
static LFSCProof * Make_and_elim(const Expr &form, LFSCProof *p, int n, const Expr &expected)
Definition: LFSCProof.cpp:397
int printCounter
Definition: LFSCProof.h:31
int getKind() const
Definition: expr.h:1168
T abs(T t)
Definition: cvc_util.h:53
static LFSCProof * Make(int v, LFSCProof *pf)
Definition: LFSCBoolProof.h:76
static LFSCProof * MakeStr(const char *c, bool db_str=false)
static Expr d_iff_s
Definition: LFSCObject.h:161
virtual void print_struct(std::ostream &s, int ind=0)
Definition: LFSCProof.h:86
virtual void fillHoles()
Definition: LFSCProof.cpp:61
static int lambdaCounter
Definition: LFSCProof.h:33
virtual LFSCProof * getChild(int n)
Definition: LFSCProof.h:101
LFSCProof * rplProof
Definition: LFSCProof.h:32
void print(std::ostream &s, int ind=0)
Definition: LFSCProof.cpp:23
static Expr d_imp_s
Definition: LFSCObject.h:162
static Expr d_and_mid_s
Definition: LFSCObject.h:164
virtual void print_pf(std::ostream &s, int ind=0)=0
static LFSCProof * Make_not_not_elim(const Expr &pf, LFSCProof *p)
Definition: LFSCProof.cpp:372
int assumeVarUsed
Definition: LFSCProof.h:37
virtual int checkOp()
Definition: LFSCProof.cpp:83
static std::map< LFSCProof *, int > lambdaMap
Definition: LFSCProof.h:29
static LFSCProof * Make_mimic(const Expr &pf, LFSCProof *p, int numHoles)
Definition: LFSCProof.cpp:384
static LFSCProof * Make(int v, LFSCProof *pf, bool assm=true, int type=3)
Definition: kinds.h:67
static void print_warning(const char *c)
Definition: Object.h:104