7 std::map< Expr, int >
vMap;
25 ostringstream os1, os2;
26 os1 <<
"(satlem _ _ _ ";
27 os2 <<
"(\\ @done @done))" <<
endl;
127 if( vMap.find( pf[0] )==vMap.end() ){
133 std::vector< int > emptyL;
134 std::vector< int > emptyLUsed;
190 emptyL, emptyLUsed,
nullRat,
false, 3 );
209 }
else if( beneath_lc ){
222 emptyLUsed.push_back( val );
226 os <<
"WARNING: Assuming a trusted formula: " << ce <<
std::endl;
228 int valT =
queryM( ce,
true,
true );
235 emptyL.push_back( val );
239 if(
getY( ce, ey ) ){
244 os <<
"WARNING: Beneath a learned clause and Y is not defined for assumption " << pf[1] <<
std::endl;
261 t1->
getL( emptyL, emptyLUsed );
262 t2->
getL( emptyL, emptyLUsed );
282 #ifdef PRINT_MAJOR_METHODS
295 tRetVal =
new TReturn( p.get(), emptyL, emptyLUsed,
nullRat,
false, 1 );
297 }
else if( yMode == 3 ){
309 }
else if( yMode == 0 || yMode==2 ){
311 os1 <<
"(" << (yMode==0 ?
"iff" :
"impl" ) <<
"_trans _ _ _ ";
321 emptyL, emptyLUsed,
nullRat,
false, yMode );
335 t1->
getL( emptyL, emptyLUsed );
336 t2->
getL( emptyL, emptyLUsed );
350 #ifdef PRINT_MAJOR_METHODS
359 tRetVal =
new TReturn( p.get(), emptyL, emptyLUsed,
nullRat,
false, 1 );
375 os1 <<
"(" << (t2->
getProvesY()==0 ?
"iff" :
"impl" ) <<
"_mp _ _ ";
388 t->
getL( emptyL, emptyLUsed );
391 #ifdef PRINT_MAJOR_METHODS
399 tRetVal =
new TReturn( p.
get(), emptyL, emptyLUsed, r,
true, 1 );
415 t1->
getL( emptyL, emptyLUsed );
416 t2->
getL( emptyL, emptyLUsed );
423 #ifdef PRINT_MAJOR_METHODS
428 if( knd1 ==
GT && knd2 ==
GE ){
430 os1 <<
"(>0_to_>=0_Real _";
443 ostringstream os1, os2;
444 os1 <<
"(impl_mp _ _ ";
455 if( pf[1].getKind()==
IFF || pf[1].getKind()==
AND || pf[1].getKind()==
OR &&
getNumNodes( pf )<=3 ){
457 if( pf[1].getKind()==
IFF ){
461 #ifdef PRINT_MAJOR_METHODS
470 tRetVal =
do_bso( pf, beneath_lc, rev_pol, t1, t2, ose );
477 t->
getL( emptyL, emptyLUsed );
479 if( pf[1].isNot() || pf[1].getKind()==
UMINUS ){
480 if( !pf[2][0].isFalse() && !pf[2][0].isTrue() ){
487 }
else if( yMode==3 ){
488 }
else if( yMode==2 ){
491 }
else if( yMode==0 ){
493 os1 <<
"(basic_subst_op0_" <<
kind_to_str( pf[1].getKind() ) <<
" _ _ ";
501 ose <<
"subst0 arity = " << pf.arity() <<
std::endl;
506 if( pf[1].getKind()==
ITE ){
507 #ifdef PRINT_MAJOR_METHODS
508 cout <<
";[M]: optimized_subst_op, ite " <<
std::endl;
513 ostringstream os1, os2;
517 os1 <<
"(refl Real ";
523 for(
int a=3; a<pf.arity(); a++ ){
530 for(
int b=0; b<3; b++ ){
531 if( pe[0]==pf[1][b] )
543 t->
getL( emptyL, emptyLUsed );
546 ostringstream os1, os2;
547 os1 <<
"(optimized_subst_op_";
556 os1 <<
" _ _ _ _ _ _ _ ";
568 }
else if( pf[1].getKind()==
PLUS ){
572 t->
getL( emptyL, emptyLUsed );
582 ostringstream os1, os2;
583 os1 <<
"(canonize_conv _ _ _ _ _ _ ";
586 os1 <<
"@pnt" << pnt1 <<
" @pnt" << pnt2 <<
" ";
594 cout << pf[3][0] <<
" " << pe <<
std::endl;
600 if( pf[1].arity()==pf.arity()-3 ){
601 #ifdef PRINT_MAJOR_METHODS
604 Expr pfn = pf[pf.arity()-1];
605 Expr cf1 = pf[1][pf.arity()-4];
606 Expr cf2 = pf[2][pf.arity()-4];
607 tRetVal =
cvc3_to_lfsc( pf[pf.arity()-1], beneath_lc, rev_pol );
608 for(
int a=(
int)pf.arity()-2; a>=3; a-- ){
609 cf1 =
Expr( pf[1].getKind(), pf[1][a-3], cf1 );
610 cf2 =
Expr( pf[2].getKind(), pf[2][a-3], cf2 );
611 std::vector < Expr > exprs;
613 exprs.push_back( cf1 );
614 exprs.push_back( cf2 );
615 exprs.push_back( pf[a] );
616 exprs.push_back( pfn );
620 tRetVal =
do_bso( pfn, beneath_lc, rev_pol, tc, tRetVal, ose );
623 ose <<
"opt_subst_op arity pv1 = " << pf[1].arity() <<
" " << pf.arity()-3 <<
std::endl;
624 ose <<
"opt_subst_op arity pv2 = " << pf[2].arity() <<
" " << pf.arity()-3 <<
std::endl;
628 for(
int a=0; a<pf.arity(); a++ ){
629 if( a>=3 && pf[a].arity()>0 ){
660 ose <<
"opt_subst_op arity = " << pf.arity() <<
std::endl;
667 t1->
getL( emptyL, emptyLUsed );
668 t2->
getL( emptyL, emptyLUsed );
674 }
else if( yMode==0 ){
675 std::vector< RefPtr< LFSCProof > > pfs;
676 std::vector< string > strs;
677 ostringstream os1, os2, os3;
678 os1 <<
"(trans Real ";
686 strs.push_back( os1.str() );
687 strs.push_back( os2.str() );
688 strs.push_back( os2.str() );
689 strs.push_back( os2.str() );
690 strs.push_back( os2.str() );
691 strs.push_back( os3.str() );
697 t->
getL( emptyL, emptyLUsed );
704 ostringstream os1, os2;
705 os1 <<
"(symm Real _ _ ";
715 t1->
getL( emptyL, emptyLUsed );
716 t2->
getL( emptyL, emptyLUsed );
726 ostringstream os1, os2;
727 os1 <<
"(real_shadow_" <<
kind_to_str( pf[1].getKind() );
732 emptyL, emptyLUsed,
nullRat,
false, 0 );
740 t1->
getL( emptyL, emptyLUsed );
741 t2->
getL( emptyL, emptyLUsed );
746 pf[1].getKind(), pf[2].getKind() ), emptyL, emptyLUsed,
nullRat,
false, 1 );
750 ostringstream os1, os2;
751 os1 <<
"(add_inequalities_" <<
kind_to_str( pf[1].getKind() );
756 emptyL, emptyLUsed,
nullRat,
false, 0 );
762 t1->
getL( emptyL, emptyLUsed );
763 t2->
getL( emptyL, emptyLUsed );
766 ostringstream os1, os2;
767 os1 <<
"(lra_>=_>=_to_= _ _ ";
772 }
else if( yMode==0 || yMode==2 ){
773 ostringstream os1, os2;
774 os1 <<
"(real_shadow_eq _ _";
777 emptyL, emptyLUsed,
nullRat,
false, 0 );
784 int n = ( pf.arity() - 1 )/2 + 1;
785 std::vector < TReturn* > trets;
786 for(
int a=n; a<pf.arity(); a++ ){
792 trets.push_back( t );
793 t->
getL( emptyL, emptyLUsed );
801 for(
int a=1; a<(int)trets.size(); a++ ){
807 currOp = currOp==
GT ?
GT :
GE;
818 t->
getL( emptyL, emptyLUsed );
831 #ifdef PRINT_MAJOR_METHODS
832 cout <<
";[M]: learned clause, not proven false" <<
std::endl;
837 ostringstream os1, os2;
838 os1 <<
"(clausify_false ";
849 std::vector< int > assumes, assumesUsed;
850 t->calcL( assumes, assumesUsed );
851 for(
int a=0; a<(int)assumes.size(); a++ ){
855 for(
int a=0; a<(int)emptyL.size(); a++ ){
868 t->
getL( emptyL, emptyLUsed );
871 int pos = pf[1].getRational().getNumerator().getInt();
879 pf[1].getRational().getNumerator().getInt() );
902 ostringstream os1, os2;
903 os1 <<
"(rewrite_ite_same ";
908 emptyL, emptyLUsed,
nullRat,
false, 0 );
914 if( pf[1].arity()==2 && pf[1][0]==pf[1][1] ){
915 ostringstream os1, os2 ;
916 os1 <<
"(" << ( isAnd ?
"and" :
"or" ) <<
"_redundant ";
920 }
else if(
isFlat( pf[2] ) ){
930 ostringstream os1, os2;
931 os1 <<
"(" << ( isAnd ?
"and" :
"or" ) <<
"_normalize _ ";
966 ostringstream os1, os2;
967 os1 <<
"(" << (isAnd ?
"and" :
"or" ) <<
"_nd _ _ _ ";
974 ostringstream os1, os2;
975 os1 <<
"(rewrite_iff_symm ";
986 t1->
getL( emptyL, emptyLUsed );
987 t2->
getL( emptyL, emptyLUsed );
996 ostringstream os1, os2;
997 os1<<
"(imply_equalities _ _ _ _ _ _ ";
998 os1 <<
"@pnt" <<
abs( m1 ) <<
" @pnt" <<
abs( m2 ) <<
" ";
1007 #ifdef PRINT_MAJOR_METHODS
1011 if( pf[1].arity()==2 && pf[2].arity()==2 && pf[1][1][0].
isRational() && pf[2][1][0].
isRational() )
1019 ostringstream os1, os2;
1024 os1 <<
"(imply_weaker_inequality_" <<
kind_to_str( pf[1].getKind() ) <<
"_" <<
kind_to_str( pf[2].getKind() );
1025 if(pf[1][1].arity() > 2)
1027 vector<Expr> t1_children;
1029 int end_i = pf[1][1].arity();
1030 for(
int i = start_i; i < end_i; i ++) {
1031 const Expr& term = pf[1][1][i];
1032 t1_children.push_back(term);
1046 emptyL, emptyLUsed,
nullRat,
false, 0 );
1051 #ifdef PRINT_MAJOR_METHODS
1055 if( pf[1].arity()==2 && pf[2].arity()==2 && pf[1][1][0].
isRational() && pf[2][1][0].
isRational() )
1063 if(
getRat( pf[1][1][0], r1 ) &&
getRat(pf[2][1][0], r2) ){
1064 Expr ep = pf[1][1][1];
1067 if ( pf[1][1][1].getKind()==
MULT && pf[1][1][1][0].
isRational() && pf[1][1][1][0].getRational()==negOne ){
1069 if(pf[1][1].arity() > 2)
1071 vector<Expr> t1_children;
1073 int end_i = pf[1][1].arity();
1074 for(
int i = start_i; i < end_i; i ++) {
1075 const Expr& term = pf[1][1][i];
1076 t1_children.push_back(term);
1078 ep =
Expr(pf[1][1].getKind(), t1_children);
1082 ep = pf[1][1][1][1];
1087 ostringstream os1, os2;
1088 os1 <<
"(imply_negated_inequality_<" << (isNeg ?
"n" :
"" );
1095 emptyL, emptyLUsed,
nullRat,
false, 0 );
1097 ostringstream os1, os2;
1098 os1 <<
"(imply_negated_inequality_";
1108 emptyL, emptyLUsed,
nullRat,
false, 0 );
1114 ostringstream os1, os2;
1118 os1 <<
"(iff_refl ";
1125 os1 <<
"(rewrite_iff_true_l ";
1131 os1 <<
"(rewrite_iff_false_l ";
1137 os1 <<
"(rewrite_iff_true_r ";
1143 os1 <<
"(rewrite_iff_false_r ";
1148 if(pf[1].isNot() && pf[1][0] == pf[2]){
1149 os1 <<
"(rewrite_iff_not_l ";
1155 if(pf[2].isNot() && pf[2][0] == pf[1]){
1156 os1 <<
"(rewrite_iff_not_r ";
1163 os1 <<
"(rewrite_iff_symm ";
1170 os1 <<
"(iff_refl ";
1181 t->
getL( emptyL, emptyLUsed );
1190 if( yMode==0 || yMode==2 )
1192 ostringstream os1, os2;
1193 os1 <<
"(" << pf[0] << (yMode==2 ?
"_impl" :
"" ) <<
" _ ";
1204 bool hasRat =
false;
1208 r = pf[2][1][1].getRational();
1211 r = pf[2][1][0].getRational();
1215 r = pf[3].getRational();
1221 if( pf[1].getKind()==
EQ && !pf[2].isFalse() ){
1222 if( pf[1][1].getKind()==
MULT &&
getRat( pf[1][1][0], r ) ){
1224 }
else if( pf[1][1].getKind()==
PLUS && pf[1][1][1].getKind()==
MULT &&
getRat( pf[1][1][1][0], r ) ){
1234 ose << pf[0] <<
", Warning: Can't find rational multiplier " <<
std::endl;
1254 ostringstream os1, os2;
1255 os1 <<
"(iff_refl ";
1261 ostringstream os1, os2;
1262 os1 <<
"(refl Real ";
1271 ostringstream os1, os2;
1272 os1 <<
"(flip_inequality_" <<
kind_to_str( pf[1].getKind() );
1273 os1 <<
"_" <<
kind_to_str( pf[2].getKind() ) <<
" ";
1282 ostringstream os1, os2;
1283 os1 <<
"(right_minus_left_" <<
kind_to_str( pf[1].getKind() ) <<
" ";
1292 ostringstream os1, os2;
1293 os1 <<
"(minus_to_plus ";
1302 ostringstream os1, os2;
1303 os1 <<
"(plus_predicate_" <<
kind_to_str( pf[1].getKind() ) <<
" ";
1304 std::vector< string > strs;
1305 std::vector< RefPtr< LFSCProof > > pfs;
1310 std::string spc(
" " );
1311 strs.push_back( os1.str() );
1312 strs.push_back( spc );
1313 strs.push_back( spc );
1314 strs.push_back( os2.str() );
1322 os <<
"(canonize_= _ _ _ ";
1323 os <<
"@pnt" << m <<
")";
1336 os <<
"(canonize_= _ _ _ ";
1337 os <<
"@pnt" << m <<
")";
1344 ostringstream os1, os2;
1345 os1 <<
"(mult_ineqn_" << (r<0 ?
"neg_" :
"");
1357 ostringstream os1, os2;
1358 os1 <<
"(mult_eqn ";
1371 ostringstream os1, os2;
1382 ostringstream os1, os2;
1383 os1 <<
"(rewrite_eq_symm ";
1392 ostringstream os1, os2;
1393 os1 <<
"(rewrite_eq_refl ";
1396 emptyL, emptyLUsed,
nullRat,
false, 0 );
1403 os <<
"(uminus_to_mult ";
1423 os <<
"(canonize_iff _ _ _ _ _ _ @pnt" << m1 <<
" @pnt" << m2 <<
")";
1468 if(
getRat( pf[1][0], r1 ) &&
getRat( pf[1][1], r2 ) ){
1469 #ifdef PRINT_MAJOR_METHODS
1470 cout <<
";[M]: const_pred " <<
kind_to_str( pf[1].getKind() );
1471 cout <<
" " << pf[2].isFalse();
1481 if( pf[1].getKind()==
EQ ){
1499 os <<
"(const_predicate_" <<
kind_to_str( pf[1].getKind() );
1508 emptyL, emptyLUsed,
nullRat,
false, 0 );
1511 ose <<
"ERROR: Could not find rational for const predicate" <<
std::endl;
1515 ose <<
"kind = " <<
kind_to_str( pf[1].getKind() );
1526 ostringstream os1, os2, os3;
1527 os1 <<
"(ite_axiom ";
1530 std::vector< string > strs;
1531 std::vector< RefPtr< LFSCProof > > pfs;
1533 strs.push_back( os1.str() );
1535 strs.push_back( os2.str() );
1537 strs.push_back( os2.str() );
1539 strs.push_back( os3.str() );
1546 ose <<
"WARNING: Unknown proof pattern [" << pfPat <<
"]";
1554 static bool firstTime =
true;
1555 if(pf.arity()>0 && (yMode!=-1 || firstTime ) ){
1557 ose <<
"Unknown proof rule (" <<
d_rules[pf[0]] <<
") " << pf[0] <<
endl;
1561 else if( yMode==-1 )
1570 ose <<
"proof pattern = " << pfPat <<
std::endl;
1583 ostringstream os1, os2;
1584 os1 <<
"[" << pf[0];
1588 os1 <<
"_" << pf[2];
1591 std::vector< int > lv, lvUsed;
1592 tRetVal->
getL( lv, lvUsed );
1666 cout <<
"make let proof..." <<
std::endl;
1673 while(t_lb != t_lbend){
1674 for(
int cvcm=0; cvcm<2; cvcm++ ){
1679 std::vector< int > lv;
1680 std::vector< int > lvUsed;
1682 t->calcL( lv, lvUsed );
1684 t->
getL( lv, lvUsed );
1691 t->getProvesY()!=3, lvUsed );
1708 std::vector< int > emptyL;
1709 std::vector< int > emptyLUsed;
1711 int valT =
queryM( e,
true,
true );
1721 std::vector< int > emptyL;
1722 std::vector< int > emptyLUsed;
1726 t1->
getL( emptyL, emptyLUsed );
1727 t2->
getL( emptyL, emptyLUsed );
1729 if( pf[1].getKind()==
PLUS || pf[1].getKind()==
MINUS ||
1735 if( pf[1].getKind()==
PLUS )
1737 emptyL, emptyLUsed,
nullRat,
false, 1 );
1738 else if( pf[1].getKind()==
MINUS )
1740 emptyL, emptyLUsed,
nullRat,
false, 1 );
1741 else if( pf[1].getKind()==
MULT ){
1742 #ifdef PRINT_MAJOR_METHODS
1743 cout <<
";[M]: basic_subst_op1_* " <<
std::endl;
1746 if(
getRat( pf[1][0], r ) ){
1748 emptyL, emptyLUsed,
nullRat,
false, 1 );
1749 }
else if(
getRat( pf[1][1], r ) ){
1751 emptyL, emptyLUsed,
nullRat,
false, 1 );
1753 print_error(
"Could not find rational mult in basic_subst_op1", cout );
1766 cout <<
"basic_subst_op1: abort, have to normalize to 2, for " <<
kind_to_str( pf[1].getKind() ) <<
std::endl;
1780 if( yMode==0 || yMode==2 )
1782 if( pf[1].getKind()==
OR || pf[1].getKind()==
AND ||
1783 pf[1].getKind()==
IFF || pf[1].getKind()==
PLUS ||
1786 ostringstream os1, os2, os3;
1787 os1 <<
"(basic_subst_op1_";
1793 std::vector< string > strs;
1794 std::vector< RefPtr< LFSCProof > > pfs;
1795 strs.push_back( os1.str() );
1797 strs.push_back( os3.str() );
1799 strs.push_back( os3.str() );
1801 strs.push_back( os3.str() );
1803 strs.push_back( os3.str() );
1805 strs.push_back( os3.str() );
1807 strs.push_back( os2.str() );
1813 ose << pf[0] <<
endl;
1814 for(
int a=0; a<pf.
arity(); a++ ){
1816 ose << a <<
": " << pf[a][0] <<
std::endl;