CVC3  2.4.1
LFSCBoolProof.cpp
Go to the documentation of this file.
1 #include "LFSCBoolProof.h"
2 
3 #include "LFSCUtilProof.h"
4 
5 //LFSCBoolRes ...
6 
7 void LFSCBoolRes::print_pf( std::ostream& s, int ind ){
8  if( d_col ){
9  s << "(cRR _ _ _ _ @a" << abs( d_var );
10  s << " ";
11  d_children[0]->print(s, ind+1);
12  s <<" ";
13  d_children[1]->print(s, ind+1);
14  s <<")";
15  }else{
16  s <<"(" << (d_var>0 ? "R" : "Q" ) << " _ _ ";
17  d_children[0]->print(s, ind+1);
18  s <<" ";
19  d_children[1]->print(s, ind+1);
20  s <<" @b" << abs( d_var ) << ")";
21  }
22 }
23 
24 void LFSCBoolRes::print_struct( std::ostream& s, int ind ){
25  s << "(res " << d_var;
26  d_children[0]->print_structure(s, ind+1);
27  s <<" ";
28  d_children[1]->print_structure(s, ind+1);
29  s << ")";
30 }
31 
32 LFSCProof* LFSCBoolRes::Make(LFSCProof* pf1, LFSCProof* pf2, int v, bool col){
33  if( pf1->isTrivial() )
34  return pf2;
35  else if( pf2->isTrivial() )
36  return pf1;
37  else
38  return new LFSCBoolRes( pf1, pf2, v, col );
39 }
40 
41 int LFSCBoolRes::checkBoolRes( std::vector< int >& clause ){
42  std::vector< int > c[2];
43  for( int a=0; a<2; a++ ){
44  d_children[a]->checkBoolRes( c[a] );
45  bool success = false;
46  for( int b=0; b<(int)c[a].size(); b++ ){
47  if( c[a][b]==d_var ){
48  c[a].erase( c[a].begin() + b, c[a].begin() + b + 1 );
49  b--;
50  success = true;
51  }
52  }
53  if( ! success ){
54  print_error( "A check-in failed ", cout );
55  return -1;
56  }
57  for( int b=0; b<(int)c[a].size(); b++ ){
58  if( std::find( clause.begin(), clause.end(), c[a][b] )==clause.end() ){
59  clause.push_back( c[a][b] );
60  }
61  }
62  }
63  return 0;
64 }
65 
67  const Expr& pf, bool cascadeOr )
68 {
69  Expr cres = cascade_expr( res );
70  if( cres.getKind()==OR && cascadeOr )
71  {
72  return Make( MakeC( p1, cres ), p2, queryM( cres ), true );
73  }
74  else if( cres.isNot() && cres[0].getKind()==OR && cascadeOr )
75  {
76  return Make( MakeC( p2, cres[0] ), p1, queryM( cres[0] ), true );
77  }
78  else if( cres.isNot() && cres[0].isNot() )
79  {
80  ostringstream ose;
81  ose << "Error: Resolving on double negation" << cres;
82  print_error( ose.str().c_str(), cout );
83  }
84  int m = queryM( cres );
85  //if( abs( m )==13 ){
86  // cout << endl;
87  // debug_print_res_struct( pf, 0 );
88  //}
89  //cout << "res on " << cres << std::endl;
90  return Make( p1, p2, m, false );
91 }
92 
94  if( res.isOr() ){
95  ostringstream os1, os2;
96  int m = queryM( res[0] );
97  os1 << "(c" << (m>0 ? "R" : "Q" );
98  os1 << " _ _ _ _ @a" << abs( m );
99  os2 << ")";
100  return LFSCProofGeneric::Make( os1.str(), MakeC( p, res[1] ), os2.str() );
101  }else{
102  ostringstream os1, os2;
103  int m = queryM( res );
104  os1 << "(c" << (m>0 ? "R" : "Q" );
105  os1 << "0 _ _ _ @a" << abs( m );
106  os2 << ")";
107  return LFSCProofGeneric::Make( os1.str(), p, os2.str() );
108  }
109 }
110 
111 
112 // LFSCClausify ...
113 
114 void LFSCClausify::print_pf( std::ostream& s, int ind ){
115  s << "(clausify_form" << (d_var<0 ? "_not" : "") << " _ _ @a" << abs( d_var ) << " ";
116  d_pf->print( s );
117  s << ")";
118 }
119 
120 //p should prove e, return a proof that is the clausal form for e
121 LFSCProof* LFSCClausify::Make( const Expr& e, LFSCProof* p, bool cascadeOr )
122 {
123  if( cascadeOr ){
124  std::vector< Expr > exprs;
125  Expr end;
126  if( e.arity()>0 )
127  end = cascade_expr( e[e.arity()-1] );
128  return Make_i( cascade_expr( e ), p, exprs, end );
129  }else{
130  return Make( queryM( e ), p );
131  }
132 }
133 
134 LFSCProof* LFSCClausify::Make_i( const Expr& e, LFSCProof* p, std::vector< Expr >& exprs, const Expr& end )
135 {
136  if( e.getKind()==OR && e!=end )
137  {
138  exprs.push_back( e[0] );
139  return LFSCAssume::Make( queryM( e[0] ), Make_i( e[1], p, exprs, end ), false );
140  }
141  else
142  {
143  for( int a=0; a<(int)exprs.size(); a++ ){
144  ostringstream os1, os2;
145  os1 << "(or_elim_1 _ _ ";
146  int m = queryM( exprs[a] );
147  //introduce double negation to satisfy or_elim requirement
148  os1 << ( m<0 ? "(not_not_intro _ " : "" );
149  os1 << "@v" << abs( m );
150  os1 << ( m<0 ? ")" : "" );
151  os1 << " ";
152  os2 << ")";
153  p = LFSCProofGeneric::Make( os1.str(), p, os2.str() );
154  }
155  return Make( queryM( e ), p );
156  }
157 }
158 
159 // LFSCAssume ...
160 
161 void LFSCAssume::print_pf( std::ostream& s, int ind ){
162  int m = d_assm ? d_var : -d_var;
163  if( d_type==3 )
164  s << "(as" << (m>0 ? "t" : "f") << " _ _ _ @a" << abs( m );
165  else
166  s << "(th_as" << (m>0 ? "t" : "f") << " _ ";
167  s << " (\\ @v" << abs( m ) << " ";
168  d_pf->print( s );
169  s << "))";
170 }
171 
172 void LFSCAssume::print_struct( std::ostream& s, int ind ){
173  s << "(as " << ( d_assm ? d_var : -d_var );
174  d_pf->print_structure( s, ind+1 );
175  s << ")";
176 }