src/search/LFSCConvert.cpp

133   std::vector< int > emptyL;  local
149         tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
156           tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
170 …tRetVal = new TReturn( LFSCClausify::Make( pf[1], t->getLFSCProof(), true ), emptyL, emptyLUsed, n…
175             tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
190                             emptyL, emptyLUsed, nullRat, false, 3 );
235         emptyL.push_back( val );
249       tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, yMode );
261         t1->getL( emptyL, emptyLUsed );
262         t2->getL( emptyL, emptyLUsed );
278 …tRetVal = new TReturn(lfsc_pf.get(), emptyL, emptyLUsed, t1->mult_rational( t2 ), t1->hasRational(…
295             tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
321                               emptyL, emptyLUsed, nullRat, false, yMode );
335         t1->getL( emptyL, emptyLUsed );
336         t2->getL( emptyL, emptyLUsed );
348 …      tRetVal = new TReturn(p.get(), emptyL, emptyLUsed, t2->getRational(), t2->hasRational() , 1);
359             tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
378 …c::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullR…
388       t->getL( emptyL, emptyLUsed );
399           tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, r, true, 1 );
403           tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
408 …tRetVal = new TReturn( LFSCProof::Make_mimic( pf, t->getLFSCProof(), 2 ), emptyL, emptyLUsed, t->g…
415       t1->getL( emptyL, emptyLUsed );
416       t2->getL( emptyL, emptyLUsed );
436           tRetVal = new TReturn(p1.get(), emptyL, emptyLUsed, nullRat, false, 1);
446 …c::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullR…
477         t->getL( emptyL, emptyLUsed );
482 …       tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, t->getRational(), t->hasRational(), 1 );
496 …turn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullR…
543               t->getL( emptyL, emptyLUsed );
566           tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 0 );
572         t->getL( emptyL, emptyLUsed );
591                                   emptyL, emptyLUsed, t->getRational(), t->hasRational(), 0 );
667       t1->getL( emptyL, emptyLUsed );
668       t2->getL( emptyL, emptyLUsed );
673                                               EQ, EQ ), emptyL, emptyLUsed, nullRat, false, 1 );
692 …tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed, nullRat, false, 0 …
697       t->getL( emptyL, emptyLUsed );
700 …tRetVal = new TReturn(LFSCLraMulC::Make(t->getLFSCProof(), Rational( -1 ), EQ), emptyL, emptyLUsed…
707 …turn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullR…
715       t1->getL( emptyL, emptyLUsed );
716       t2->getL( emptyL, emptyLUsed );
722 …n( LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(), op1, op2 ), emptyL, emptyLUsed, nullR…
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 );
756                             emptyL, emptyLUsed, nullRat, false, 0 );
762       t1->getL( emptyL, emptyLUsed );
763       t2->getL( emptyL, emptyLUsed );
771         tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
777                             emptyL, emptyLUsed, nullRat, false, 0 );
793             t->getL( emptyL, emptyLUsed );
810 …tRetVal = new TReturn( LFSCLraContra::Make( p1.get(), GT ), emptyL, emptyLUsed, nullRat, false, 0 …
818         t->getL( emptyL, emptyLUsed );
855           for( int a=0; a<(int)emptyL.size(); a++ ){
856             p = LFSCAssume::Make( emptyL[a], p.get(), true );
859           emptyL.clear();
861           tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
868       t->getL( emptyL, emptyLUsed );
873         tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, t->getRational(), t->hasRational(), 0 );
881         tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
892           tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
908                           emptyL, emptyLUsed, nullRat, false, 0 );
919 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed…
934 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed…
969 …turn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullR…
979 …urn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed, nullR…
986         t1->getL( emptyL, emptyLUsed );
987         t2->getL( emptyL, emptyLUsed );
1000 …c::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullR…
1015           tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, nullRat, false, 1 );
1046                             emptyL, emptyLUsed, nullRat, false, 0 );
1059           tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, nullRat, false, 1 );
1095                                 emptyL, emptyLUsed, nullRat, false, 0 );
1108                                 emptyL, emptyLUsed, nullRat, false, 0 );
1121 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1128 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUse…
1134 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUse…
1140 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUse…
1146 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUse…
1153 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUse…
1159 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUse…
1167 …urn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed, nullR…
1173 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1181       t->getL( emptyL, emptyLUsed );
1195 …new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed,
1248         tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, r, hasRat, 1 );
1258 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1265 …tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1277 …ew TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1287 …ew TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1297 …ew TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1315           tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed,
1325           tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed,
1339           tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed,
1352 …ew TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1364 …ew TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1377 …ew TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1387 …ew TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1396                                                       emptyL, emptyLUsed, nullRat, false, 0 );
1406 …          tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed,
1412 …tRetVal = new TReturn( LFSCProofGeneric::MakeStr( "rewrite_not_true" ), emptyL, emptyLUsed, nullRa…
1416 …tRetVal = new TReturn( LFSCProofGeneric::MakeStr( "rewrite_not_false" ), emptyL, emptyLUsed, nullR…
1426 …tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed, nullRat,…
1435         tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, nullRat, false, 1 );
1444 …tRetVal = new TReturn( LFSCProofGeneric::MakeStr("(rewrite_not_not _)"), emptyL, emptyLUsed, nullR…
1447 …tRetVal = new TReturn( LFSCProofGeneric::MakeStr("(iff_refl _)"), emptyL, emptyLUsed, nullRat, fal…
1449 …tRetVal = new TReturn( LFSCProofGeneric::MakeStr("(rewrite_not_not _)"), emptyL, emptyLUsed, nullR…
1456 …  tRetVal = new TReturn( LFSCLem::Make( queryM( pf[1] ) ), emptyL, emptyLUsed, nullRat, false, 3 );
1493               tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
1508                                 emptyL, emptyLUsed, nullRat, false, 0 );
1542       tRetVal = new TReturn( LFSCClausify::Make( pf[1], p.get() ), emptyL, emptyLUsed,
1574     tRetVal = new TReturn( LFSCProofGeneric::MakeUnk(), emptyL, emptyLUsed, nullRat, false, -1 );
1708   std::vector< int > emptyL;  local
1712     return new TReturn( LFSCPfVar::Make( "@T", valT ), emptyL, emptyLUsed, nullRat, false, 0 );
1714 …return new TReturn( LFSCProofGeneric::MakeStr( "@T-unk" ), emptyL, emptyLUsed, nullRat, false, 0 );
1721   std::vector< int > emptyL;  local
1726   t1->getL( emptyL, emptyLUsed );
1727   t2->getL( emptyL, emptyLUsed );
1737                             emptyL, emptyLUsed, nullRat, false, 1 );
1740                             emptyL, emptyLUsed, nullRat, false, 1 );
1748                               emptyL, emptyLUsed, nullRat, false, 1 );
1751                               emptyL, emptyLUsed, nullRat, false, 1 );
1763         tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
1808 …tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed, nullRat, false, yM…