CVC3

LFSCBoolProof.cpp

Go to the documentation of this file.
00001 #include "LFSCBoolProof.h"
00002 
00003 #include "LFSCUtilProof.h"
00004 
00005 //LFSCBoolRes ...
00006 
00007 void LFSCBoolRes::print_pf( std::ostream& s, int ind ){
00008   if( d_col ){
00009     s << "(cRR _ _ _ _ @a" << abs( d_var );
00010     s << " ";
00011     d_children[0]->print(s, ind+1);
00012     s <<" ";
00013     d_children[1]->print(s, ind+1);
00014     s <<")";
00015   }else{
00016     s <<"(" << (d_var>0 ? "R" : "Q" ) << " _ _ ";
00017     d_children[0]->print(s, ind+1);
00018     s <<" ";
00019     d_children[1]->print(s, ind+1);
00020     s <<" @b" << abs( d_var ) << ")";
00021   }
00022 }
00023 
00024 void LFSCBoolRes::print_struct( std::ostream& s, int ind ){
00025   s << "(res " << d_var;
00026   d_children[0]->print_structure(s, ind+1);
00027   s <<" ";
00028   d_children[1]->print_structure(s, ind+1);
00029   s << ")";
00030 }
00031 
00032 LFSCProof* LFSCBoolRes::Make(LFSCProof* pf1, LFSCProof* pf2, int v, bool col){
00033   if( pf1->isTrivial() )
00034     return pf2;
00035   else if( pf2->isTrivial() )
00036     return pf1;
00037   else
00038     return new LFSCBoolRes( pf1, pf2, v, col );
00039 }
00040 
00041 int LFSCBoolRes::checkBoolRes( std::vector< int >& clause ){
00042   std::vector< int > c[2];
00043   for( int a=0; a<2; a++ ){
00044     d_children[a]->checkBoolRes( c[a] );
00045     bool success = false;
00046     for( int b=0; b<(int)c[a].size(); b++ ){
00047       if( c[a][b]==d_var ){
00048         c[a].erase( c[a].begin() + b, c[a].begin() + b + 1 );
00049         b--;
00050         success = true;
00051       }
00052     }
00053     if( ! success ){
00054       print_error( "A check-in failed ", cout );
00055       return -1;
00056     }
00057     for( int b=0; b<(int)c[a].size(); b++ ){
00058       if( std::find( clause.begin(), clause.end(), c[a][b] )==clause.end() ){
00059         clause.push_back( c[a][b] );
00060       }
00061     }
00062   }
00063   return 0;
00064 }
00065 
00066 LFSCProof* LFSCBoolRes::Make( LFSCProof* p1, LFSCProof* p2, const Expr& res,
00067                                const Expr& pf, bool cascadeOr )
00068 {
00069   Expr cres = cascade_expr( res );
00070   if( cres.getKind()==OR && cascadeOr )
00071   {
00072     return Make( MakeC( p1, cres ), p2, queryM( cres ), true );
00073   }
00074   else if( cres.isNot() && cres[0].getKind()==OR && cascadeOr )
00075   {
00076     return Make( MakeC( p2, cres[0] ), p1, queryM( cres[0] ), true );
00077   }
00078   else if( cres.isNot() && cres[0].isNot() )
00079   {
00080     ostringstream ose;
00081     ose << "Error: Resolving on double negation" << cres;
00082     print_error( ose.str().c_str(), cout );
00083   }
00084   int m = queryM( cres );
00085   //if( abs( m )==13 ){
00086   //  cout << endl;
00087   //  debug_print_res_struct( pf, 0 );
00088   //}
00089   //cout << "res on " << cres << std::endl;
00090   return Make( p1, p2, m, false );
00091 }
00092 
00093 LFSCProof* LFSCBoolRes::MakeC( LFSCProof* p, const Expr& res ){
00094   if( res.isOr() ){
00095     ostringstream os1, os2;
00096     int m = queryM( res[0] );
00097     os1 << "(c" << (m>0 ? "R" : "Q" );
00098     os1 << " _ _ _ _ @a" << abs( m );
00099     os2 << ")";
00100     return LFSCProofGeneric::Make( os1.str(), MakeC( p, res[1] ), os2.str() );
00101   }else{
00102     ostringstream os1, os2;
00103     int m = queryM( res );
00104     os1 << "(c" << (m>0 ? "R" : "Q" );
00105     os1 << "0 _ _ _ @a" << abs( m );
00106     os2 << ")";
00107     return LFSCProofGeneric::Make( os1.str(), p, os2.str() );
00108   }
00109 }
00110 
00111 
00112 // LFSCClausify ...
00113 
00114 void LFSCClausify::print_pf( std::ostream& s, int ind ){
00115   s << "(clausify_form" << (d_var<0 ? "_not" : "") << " _ _ @a" << abs( d_var ) << " ";
00116   d_pf->print( s );
00117   s << ")";
00118 }
00119 
00120 //p should prove e, return a proof that is the clausal form for e
00121 LFSCProof* LFSCClausify::Make( const Expr& e, LFSCProof* p, bool cascadeOr )
00122 {
00123   if( cascadeOr ){
00124     std::vector< Expr > exprs;
00125     Expr end;
00126     if( e.arity()>0 )
00127       end = cascade_expr( e[e.arity()-1] );
00128     return Make_i( cascade_expr( e ), p, exprs, end );
00129   }else{
00130     return Make( queryM( e ), p );
00131   }
00132 }
00133 
00134 LFSCProof* LFSCClausify::Make_i( const Expr& e, LFSCProof* p, std::vector< Expr >& exprs, const Expr& end )
00135 {
00136   if( e.getKind()==OR && e!=end )
00137   {
00138     exprs.push_back( e[0] );
00139     return LFSCAssume::Make( queryM( e[0] ), Make_i( e[1], p, exprs, end ), false );
00140   }
00141   else
00142   {
00143     for( int a=0; a<(int)exprs.size(); a++ ){
00144       ostringstream os1, os2;
00145       os1 << "(or_elim_1 _ _ ";
00146       int m = queryM( exprs[a] );
00147       //introduce double negation to satisfy or_elim requirement
00148       os1 << ( m<0 ? "(not_not_intro _ " : "" );
00149       os1 << "@v" << abs( m );
00150       os1 << ( m<0 ? ")" : "" );
00151       os1 << " ";
00152       os2 << ")";
00153       p = LFSCProofGeneric::Make( os1.str(), p, os2.str() );
00154     }
00155     return Make( queryM( e ), p );
00156   }
00157 }
00158 
00159 // LFSCAssume ...
00160 
00161 void LFSCAssume::print_pf( std::ostream& s, int ind ){
00162   int m = d_assm ? d_var : -d_var;
00163   if( d_type==3 )
00164     s << "(as" << (m>0 ? "t" : "f") << " _ _ _ @a" << abs( m );
00165   else
00166     s << "(th_as" << (m>0 ? "t" : "f") << " _ ";
00167   s << " (\\ @v" << abs( m ) << " ";
00168   d_pf->print( s );
00169   s << "))";
00170 }
00171 
00172 void LFSCAssume::print_struct( std::ostream& s, int ind ){
00173   s << "(as " << ( d_assm ? d_var : -d_var );
00174   d_pf->print_structure( s, ind+1 );
00175   s << ")";
00176 }