00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027 #define _CVC3_TRUSTED_
00028
00029
00030 #include "quant_theorem_producer.h"
00031 #include "theory_quant.h"
00032 #include "theory_core.h"
00033
00034
00035 using namespace std;
00036 using namespace CVC3;
00037
00038
00039 QuantProofRules* TheoryQuant::createProofRules() {
00040 return new QuantTheoremProducer(theoryCore()->getTM(), this);
00041 }
00042
00043
00044 #define CLASS_NAME "CVC3::QuantTheoremProducer"
00045
00046
00047
00048 Theorem
00049 QuantTheoremProducer::rewriteNotForall(const Expr& e) {
00050 if(CHECK_PROOFS) {
00051 CHECK_SOUND(e.isNot() && e[0].isForall(),
00052 "rewriteNotForall: expr must be NOT FORALL:\n"
00053 +e.toString());
00054 }
00055 Proof pf;
00056 if(withProof())
00057 pf = newPf("rewrite_not_forall", e);
00058 return newRWTheorem(e, e.getEM()->newClosureExpr(EXISTS, e[0].getVars(),
00059 !e[0].getBody()),
00060 Assumptions::emptyAssump(), pf);
00061 }
00062
00063 Theorem
00064 QuantTheoremProducer::addNewConst(const Expr& e) {
00065 Proof pf;
00066 if(withProof())
00067 pf = newPf("add_new_const", e);
00068 return newTheorem(e, Assumptions::emptyAssump(), pf);
00069 }
00070
00071
00072 Theorem
00073 QuantTheoremProducer::newRWThm(const Expr& e, const Expr& newE) {
00074 Proof pf;
00075 if(withProof())
00076 pf = newPf("from cache", e);
00077 return newRWTheorem(e, newE,Assumptions::emptyAssump(), pf);
00078 }
00079
00080
00081 Theorem
00082 QuantTheoremProducer::normalizeQuant(const Expr& quant) {
00083 if(CHECK_PROOFS) {
00084 CHECK_SOUND(quant.isForall()||quant.isExists(),
00085 "normalizeQuant: expr must be FORALL or EXISTS\n"
00086 +quant.toString());
00087 }
00088
00089
00090 std::map<Expr,int>::iterator typeIter;
00091 std::string base("_BD");
00092 int counter(0);
00093
00094 vector<Expr> newVars;
00095 const std::vector<Expr>& cur_vars = quant.getVars();
00096 for(size_t j =0; j<cur_vars.size(); j++){
00097 Type t = cur_vars[j].getType();
00098 int typeIndex ;
00099
00100 typeIter = d_typeFound.find(t.getExpr());
00101
00102 if(d_typeFound.end() == typeIter){
00103 typeIndex = d_typeFound.size();
00104 d_typeFound[t.getExpr()] = typeIndex;
00105 }
00106 else{
00107 typeIndex = typeIter->second;
00108 }
00109
00110 counter++;
00111 std::stringstream stringType;
00112 stringType << counter << "TY" << typeIndex ;
00113 std::string out_str = base + stringType.str();
00114 Expr newExpr = d_theoryQuant->getEM()->newBoundVarExpr(out_str, int2string(counter));
00115 newExpr.setType(t);
00116 newVars.push_back(newExpr);
00117 }
00118
00119 vector<vector<Expr> > trigs = quant.getTrigs();
00120 for(size_t i = 0 ; i < trigs.size(); i++){
00121 for(size_t j = 0 ; j < trigs[i].size(); j++){
00122 trigs[i][j] = trigs[i][j].substExpr(cur_vars,newVars);
00123 }
00124 }
00125
00126 Expr normBody = quant.getBody().substExpr(cur_vars,newVars);
00127 Expr normQuant = d_theoryQuant->getEM()->newClosureExpr(quant.isForall()?FORALL:EXISTS, newVars, normBody, trigs);
00128
00129 Proof pf;
00130 if(withProof())
00131 pf = newPf("normalizeQuant", quant, normQuant);
00132
00133 return newRWTheorem(quant, normQuant, Assumptions::emptyAssump(), pf);
00134
00135 }
00136
00137
00138
00139 Theorem QuantTheoremProducer::rewriteNotExists(const Expr& e) {
00140 if(CHECK_PROOFS) {
00141 CHECK_SOUND(e.isNot() && e[0].isExists(),
00142 "rewriteNotExists: expr must be NOT FORALL:\n"
00143 +e.toString());
00144 }
00145 Proof pf;
00146 if(withProof())
00147 pf = newPf("rewrite_not_exists", e);
00148 return newRWTheorem(e, e.getEM()->newClosureExpr(FORALL, e[0].getVars(),
00149 !e[0].getBody()),
00150 Assumptions::emptyAssump(), pf);
00151 }
00152
00153
00154 Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const vector<Expr>& terms, int quantLevel, Expr gterm){
00155 Expr e = t1.getExpr();
00156 const vector<Expr>& boundVars = e.getVars();
00157 if(CHECK_PROOFS) {
00158 CHECK_SOUND(boundVars.size() == terms.size(),
00159 "Universal instantiation: size of terms array does "
00160 "not match quanitfied variables array size");
00161 CHECK_SOUND(e.isForall(),
00162 "universal instantiation: expr must be FORALL:\n"
00163 +e.toString());
00164 for(unsigned int i=0; i<terms.size(); i++)
00165 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) ==
00166 d_theoryQuant->getBaseType(terms[i]),
00167 "Universal instantiation: type mismatch");
00168 }
00169
00170
00171 Expr tr = e.getEM()->trueExpr();
00172 Expr typePred = tr;
00173
00174 for(unsigned int i=0; i<terms.size(); i++) {
00175 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
00176 if(p!=tr) {
00177 if(typePred==tr)
00178 typePred = p;
00179 else
00180 typePred = typePred.andExpr(p);
00181 }
00182
00183
00184 }
00185
00186
00187
00188 Expr inst = e.getBody().substExpr(e.getVars(), terms);
00189
00190
00191
00192
00193 Proof pf;
00194 if(withProof()) {
00195 vector<Proof> pfs;
00196 vector<Expr> es;
00197 pfs.push_back(t1.getProof());
00198 es.push_back(e);
00199 es.push_back(Expr(RAW_LIST,terms));
00200
00201 es.push_back(inst);
00202 if (gterm.isNull()) {
00203 es.push_back( d_theoryQuant->getEM()->newRatExpr(0));
00204 }
00205 else {es.push_back(gterm);
00206 }
00207 pf= newPf("universal_elimination1", es, pfs);
00208 }
00209
00210
00211
00212
00213
00214 Expr imp;
00215
00216 if(typePred == tr )
00217 imp = inst;
00218 else
00219 imp = typePred.impExpr(inst);
00220 Theorem ret = newTheorem(imp, t1.getAssumptionsRef(), pf);
00221
00222 int thmLevel = t1.getQuantLevel();
00223 if(quantLevel >= thmLevel) {
00224 ret.setQuantLevel(quantLevel+1);
00225 }
00226 else{
00227 ret.setQuantLevel(thmLevel+1);
00228 }
00229
00230
00231 return ret;
00232 }
00233
00234
00235
00236
00237
00238
00239
00240
00241
00242
00243
00244
00245 Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const vector<Expr>& terms, int quantLevel){
00246
00247 Expr e = t1.getExpr();
00248 const vector<Expr>& boundVars = e.getVars();
00249 if(CHECK_PROOFS) {
00250 CHECK_SOUND(boundVars.size() == terms.size(),
00251 "Universal instantiation: size of terms array does "
00252 "not match quanitfied variables array size");
00253 CHECK_SOUND(e.isForall(),
00254 "universal instantiation: expr must be FORALL:\n"
00255 +e.toString());
00256 for(unsigned int i=0; i<terms.size(); i++)
00257 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) ==
00258 d_theoryQuant->getBaseType(terms[i]),
00259 "Universal instantiation: type mismatch");
00260 }
00261
00262
00263 Expr tr = e.getEM()->trueExpr();
00264 Expr typePred = tr;
00265
00266 for(unsigned int i=0; i<terms.size(); i++) {
00267 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
00268 if(p!=tr) {
00269 if(typePred==tr)
00270 typePred = p;
00271 else
00272 typePred = typePred.andExpr(p);
00273 }
00274
00275
00276 }
00277
00278
00279 Expr inst = e.getBody().substExpr(e.getVars(), terms);
00280
00281
00282
00283
00284
00285 Proof pf;
00286 if(withProof()) {
00287 vector<Proof> pfs;
00288 vector<Expr> es;
00289 pfs.push_back(t1.getProof());
00290 es.push_back(e);
00291 es.push_back(Expr(RAW_LIST,terms));
00292
00293 es.push_back(inst);
00294 pf= newPf("universal_elimination2", es, pfs);
00295 }
00296
00297
00298
00299
00300 Expr imp;
00301 if(typePred == tr)
00302 imp = inst;
00303 else
00304 imp = typePred.impExpr(inst);
00305 Theorem ret = newTheorem(imp, t1.getAssumptionsRef(), pf);
00306
00307 int thmLevel = t1.getQuantLevel();
00308 if(quantLevel >= thmLevel) {
00309 ret.setQuantLevel(quantLevel+1);
00310 }
00311 else{
00312 ret.setQuantLevel(thmLevel+1);
00313 }
00314
00315
00316 return ret;
00317 }
00318
00319 Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const vector<Expr>& terms){
00320
00321 Expr e = t1.getExpr();
00322 const vector<Expr>& boundVars = e.getVars();
00323 if(CHECK_PROOFS) {
00324 CHECK_SOUND(boundVars.size() == terms.size(),
00325 "Universal instantiation: size of terms array does "
00326 "not match quanitfied variables array size");
00327 CHECK_SOUND(e.isForall(),
00328 "universal instantiation: expr must be FORALL:\n"
00329 +e.toString());
00330 for(unsigned int i=0; i<terms.size(); i++)
00331 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) ==
00332 d_theoryQuant->getBaseType(terms[i]),
00333 "Universal instantiation: type mismatch");
00334 }
00335
00336
00337 Expr tr = e.getEM()->trueExpr();
00338 Expr typePred = tr;
00339 unsigned qlevel=0, qlevelMax = 0;
00340 for(unsigned int i=0; i<terms.size(); i++) {
00341 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
00342 if(p!=tr) {
00343 if(typePred==tr)
00344 typePred = p;
00345 else
00346 typePred = typePred.andExpr(p);
00347 }
00348 qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]);
00349 if (qlevel > qlevelMax) qlevel = qlevelMax;
00350 }
00351
00352 Expr inst = e.getBody().substExpr(e.getVars(), terms);
00353
00354
00355
00356
00357
00358 Proof pf;
00359 if(withProof()) {
00360 vector<Proof> pfs;
00361 vector<Expr> es;
00362 pfs.push_back(t1.getProof());
00363 es.push_back(e);
00364 es.push_back(Expr(RAW_LIST,terms));
00365
00366 es.push_back(inst);
00367 pf= newPf("universal_elimination3", es, pfs);
00368 }
00369
00370
00371
00372 Expr imp;
00373 if( typePred == tr )
00374 imp = inst;
00375 else
00376 imp = typePred.impExpr(inst);
00377 Theorem ret = newTheorem(imp, t1.getAssumptionsRef(), pf);
00378
00379
00380 unsigned thmLevel = t1.getQuantLevel();
00381 if(qlevel >= thmLevel) {
00382 ret.setQuantLevel(qlevel+1);
00383 }
00384 else{
00385
00386 ret.setQuantLevel(thmLevel+1);
00387 }
00388
00389
00390
00391 return ret;
00392 }
00393
00394
00395 Theorem QuantTheoremProducer::partialUniversalInst(const Theorem& t1, const vector<Expr>& terms, int quantLevel){
00396 cout<<"error in partial inst" << endl;
00397 Expr e = t1.getExpr();
00398 const vector<Expr>& boundVars = e.getVars();
00399 if(CHECK_PROOFS) {
00400 CHECK_SOUND(boundVars.size() >= terms.size(),
00401 "Universal instantiation: size of terms array does "
00402 "not match quanitfied variables array size");
00403 CHECK_SOUND(e.isForall(),
00404 "universal instantiation: expr must be FORALL:\n"
00405 +e.toString());
00406 for(unsigned int i=0; i<terms.size(); i++){
00407 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) ==
00408 d_theoryQuant->getBaseType(terms[i]),
00409 "partial Universal instantiation: type mismatch");
00410 }
00411 }
00412
00413
00414 Expr tr = e.getEM()->trueExpr();
00415 Expr typePred = tr;
00416 for(unsigned int i=0; i<terms.size(); i++) {
00417 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
00418 if(p!=tr) {
00419 if(typePred==tr)
00420 typePred = p;
00421 else
00422 typePred = typePred.andExpr(p);
00423 }
00424 }
00425 Proof pf;
00426 if(withProof()) {
00427 vector<Proof> pfs;
00428 vector<Expr> es;
00429 pfs.push_back(t1.getProof());
00430 es.push_back(e);
00431 es.insert(es.end(), terms.begin(), terms.end());
00432 pf= newPf("partial_universal_instantiation", es, pfs);
00433 }
00434
00435
00436 if(terms.size() == boundVars.size()){
00437 Expr inst = e.getBody().substExpr(e.getVars(), terms);
00438 Expr imp;
00439 if(typePred == tr)
00440 imp = inst;
00441 else
00442 imp = typePred.impExpr(inst);
00443 return(newTheorem(imp, t1.getAssumptionsRef(), pf));
00444 }
00445 else{
00446 vector<Expr> newBoundVars;
00447 for(size_t i=0; i<terms.size(); i++) {
00448 newBoundVars.push_back(boundVars[i]);
00449 }
00450
00451 vector<Expr>leftBoundVars;
00452 for(size_t i=terms.size(); i<boundVars.size(); i++) {
00453 leftBoundVars.push_back(boundVars[i]);
00454 }
00455
00456 Expr tempinst = e.getBody().substExpr(newBoundVars, terms);
00457 Expr inst = d_theoryQuant->getEM()->newClosureExpr(FORALL, leftBoundVars, tempinst);
00458
00459 Expr imp;
00460 if(typePred == tr)
00461 imp = inst;
00462 else
00463 imp = typePred.impExpr(inst);
00464
00465 Theorem res = (newTheorem(imp, t1.getAssumptionsRef(), pf));
00466 int thmLevel = t1.getQuantLevel();
00467 if(quantLevel >= thmLevel) {
00468 res.setQuantLevel(quantLevel+1);
00469 }
00470 else{
00471
00472 res.setQuantLevel(thmLevel);
00473 }
00474 return res;
00475
00476 }
00477 }
00478
00479
00480 void QuantTheoremProducer::recFindBoundVars(const Expr& e,
00481 ExprMap<bool> & boundVars, ExprMap<bool> &visited)
00482 {
00483 if(visited.count(e)>0)
00484 return;
00485 else
00486 visited[e] = true;
00487 if(e.getKind() == BOUND_VAR)
00488 boundVars[e] = true;
00489 if(e.getKind() == EXISTS || e.getKind() == FORALL)
00490 recFindBoundVars(e.getBody(), boundVars, visited);
00491 for(Expr::iterator it = e.begin(); it!=e.end(); ++it)
00492 recFindBoundVars(*it, boundVars, visited);
00493
00494 }
00495
00496
00497 Theorem QuantTheoremProducer::adjustVarUniv(const Theorem& t1, const std::vector<Expr>& newBvs){
00498 const Expr e=t1.getExpr();
00499 const Expr body = e.getBody();
00500 if(CHECK_PROOFS) {
00501 CHECK_SOUND(e.isForall(),
00502 "adjustVarUniv: "
00503 +e.toString());
00504 }
00505
00506 const vector<Expr>& origVars = e.getVars();
00507
00508
00509 ExprMap<bool> oldmap;
00510 for(vector<Expr>::const_iterator it = origVars.begin(),
00511 iend=origVars.end(); it!=iend; ++it) {
00512 oldmap[*it]=true;
00513 }
00514
00515 vector<Expr> quantVars;
00516 for(vector<Expr>::const_iterator it = newBvs.begin(),
00517 iend=newBvs.end(); it!=iend; ++it) {
00518 if(oldmap.count(*it) > 0)
00519 quantVars.push_back(*it);
00520 }
00521
00522 if(quantVars.size() == origVars.size())
00523 return t1;
00524
00525 ExprMap<bool> newmap;
00526 for(vector<Expr>::const_iterator it = newBvs.begin(),
00527 iend=newBvs.end(); it!=iend; ++it) {
00528 newmap[*it]=true;
00529 }
00530
00531 for(vector<Expr>::const_iterator it = origVars.begin(),
00532 iend=origVars.end(); it!=iend; ++it) {
00533 if(newmap.count(*it)<=0){
00534 quantVars.push_back(*it);
00535 };
00536 }
00537
00538 Proof pf;
00539 if(withProof()) {
00540 vector<Expr> es;
00541 vector<Proof> pfs;
00542 es.push_back(e);
00543 es.insert(es.end(), quantVars.begin(), quantVars.end());
00544 pfs.push_back(t1.getProof());
00545 pf= newPf("adjustVarUniv", es, pfs);
00546 }
00547
00548 Expr newQuantExpr;
00549 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, quantVars, body);
00550
00551 return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
00552 }
00553
00554
00555 Theorem QuantTheoremProducer::packVar(const Theorem& t1){
00556 Expr out_forall =t1.getExpr();
00557
00558 if(CHECK_PROOFS) {
00559 CHECK_SOUND(out_forall.isForall(),
00560 "packVar: "
00561 +out_forall.toString());
00562 }
00563
00564 vector<Expr> bVars = out_forall.getVars();
00565
00566 if(!out_forall.getBody().isForall()){
00567 return t1;
00568 }
00569
00570 Expr cur_body = out_forall.getBody();
00571
00572 while(cur_body.isForall()){
00573 vector<Expr> bVarsLeft = cur_body.getVars();
00574 for(vector<Expr>::iterator i=bVarsLeft.begin(), iend=bVarsLeft.end(); i!=iend; i++){
00575 bVars.push_back(*i);
00576 }
00577 cur_body=cur_body.getBody();
00578 }
00579
00580 Proof pf;
00581 if(withProof()) {
00582 vector<Expr> es;
00583 vector<Proof> pfs;
00584 es.push_back(out_forall);
00585 es.insert(es.end(), bVars.begin(), bVars.end());
00586 pfs.push_back(t1.getProof());
00587 pf= newPf("packVar", es, pfs);
00588 }
00589
00590 Expr newQuantExpr;
00591 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, bVars, cur_body);
00592
00593 return (newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
00594
00595 }
00596
00597
00598
00599 Theorem QuantTheoremProducer::pullVarOut(const Theorem& t1){
00600 const Expr thm_expr=t1.getExpr();
00601
00602 if(CHECK_PROOFS) {
00603 CHECK_SOUND(thm_expr.isForall() || thm_expr.isExists(),
00604 "pullVarOut: "
00605 +thm_expr.toString());
00606 }
00607
00608 const Expr outBody = thm_expr.getBody();
00609
00610
00611
00612
00613
00614
00615
00616 if (thm_expr.isForall()){
00617 if((outBody.isNot() && outBody[0].isAnd() && outBody[0][1].isExists())){
00618
00619 vector<Expr> bVarsOut = thm_expr.getVars();
00620
00621 const Expr innerExists =outBody[0][1];
00622 const Expr innerBody = innerExists.getBody();
00623 vector<Expr> bVarsIn = innerExists.getVars();
00624
00625 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
00626 bVarsOut.push_back(*i);
00627 }
00628
00629 Proof pf;
00630 if(withProof()) {
00631 vector<Expr> es;
00632 vector<Proof> pfs;
00633 es.push_back(thm_expr);
00634 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
00635 pfs.push_back(t1.getProof());
00636 pf= newPf("pullVarOut", es, pfs);
00637 }
00638
00639 Expr newbody;
00640
00641 newbody=(outBody[0][0].notExpr()).orExpr(innerBody.notExpr());
00642
00643 Expr newQuantExpr;
00644 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, bVarsOut, newbody);
00645
00646 return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
00647 }
00648
00649 else if ((outBody.isAnd() && outBody[1].isForall()) ||
00650 (outBody.isImpl() && outBody[1].isForall())){
00651
00652 vector<Expr> bVarsOut = thm_expr.getVars();
00653
00654 const Expr innerForall=outBody[1];
00655 const Expr innerBody = innerForall.getBody();
00656 vector<Expr> bVarsIn = innerForall.getVars();
00657
00658 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
00659 bVarsOut.push_back(*i);
00660 }
00661
00662 Proof pf;
00663 if(withProof()) {
00664 vector<Expr> es;
00665 vector<Proof> pfs;
00666 es.push_back(thm_expr);
00667 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
00668 pfs.push_back(t1.getProof());
00669 pf= newPf("pullVarOut", es, pfs);
00670 }
00671
00672 Expr newbody;
00673 if(outBody.isAnd()){
00674 newbody=outBody[0].andExpr(innerBody);
00675 }
00676 else if(outBody.isImpl()){
00677 newbody=outBody[0].impExpr(innerBody);
00678 }
00679
00680 Expr newQuantExpr;
00681 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, bVarsOut, newbody);
00682
00683 return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
00684 }
00685 return t1;
00686 }
00687
00688 else if (thm_expr.isExists()){
00689 if ((outBody.isAnd() && outBody[1].isExists()) ||
00690 (outBody.isImpl() && outBody[1].isExists())){
00691
00692 vector<Expr> bVarsOut = thm_expr.getVars();
00693
00694 const Expr innerExists = outBody[1];
00695 const Expr innerBody = innerExists.getBody();
00696 vector<Expr> bVarsIn = innerExists.getVars();
00697
00698 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
00699 bVarsOut.push_back(*i);
00700 }
00701
00702 Proof pf;
00703 if(withProof()) {
00704 vector<Expr> es;
00705 vector<Proof> pfs;
00706 es.push_back(thm_expr);
00707 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
00708 pfs.push_back(t1.getProof());
00709 pf= newPf("pullVarOut", es, pfs);
00710 }
00711
00712 Expr newbody;
00713 if(outBody.isAnd()){
00714 newbody=outBody[0].andExpr(innerBody);
00715 }
00716 else if(outBody.isImpl()){
00717 newbody=outBody[0].impExpr(innerBody);
00718 }
00719
00720 Expr newQuantExpr;
00721 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(EXISTS, bVarsOut, newbody);
00722
00723 return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
00724 }
00725 }
00726 return t1;
00727 }
00728
00729
00730
00731
00732
00733
00734
00735 Theorem QuantTheoremProducer::boundVarElim(const Theorem& t1)
00736 {
00737 const Expr e=t1.getExpr();
00738 const Expr body = e.getBody();
00739 if(CHECK_PROOFS) {
00740 CHECK_SOUND(e.isForall() || e.isExists(),
00741 "bound var elimination: "
00742 +e.toString());
00743 }
00744 ExprMap<bool> boundVars;
00745 ExprMap<bool> visited;
00746
00747 recFindBoundVars(body, boundVars, visited);
00748 vector<Expr> quantVars;
00749 const vector<Expr>& origVars = e.getVars();
00750 for(vector<Expr>::const_iterator it = origVars.begin(),
00751 iend=origVars.end(); it!=iend; ++it)
00752 {
00753 if(boundVars.count(*it) > 0)
00754 quantVars.push_back(*it);
00755 }
00756
00757
00758 if(quantVars.size() == origVars.size())
00759 return t1;
00760
00761 Proof pf;
00762 if(withProof()) {
00763 vector<Expr> es;
00764 vector<Proof> pfs;
00765 es.push_back(e);
00766 es.insert(es.end(), quantVars.begin(), quantVars.end());
00767 pfs.push_back(t1.getProof());
00768 pf= newPf("bound_variable_elimination", es, pfs);
00769 }
00770 if(quantVars.size() == 0)
00771 return(newTheorem(e.getBody(), t1.getAssumptionsRef(), pf));
00772
00773 Expr newQuantExpr;
00774 if(e.isForall())
00775 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, quantVars, body);
00776 else
00777 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(EXISTS, quantVars, body);
00778
00779 return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
00780 }