CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file quant_theorem_producer.cpp 00004 * 00005 * Author: Daniel Wichs, Yeting Ge 00006 * 00007 * Created: Jul 07 22:22:38 GMT 2003 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 * CLASS: QuantProofRules 00019 * 00020 * 00021 * Description: TRUSTED implementation of arithmetic proof rules. 00022 * 00023 */ 00024 /*****************************************************************************/ 00025 00026 // This code is trusted 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 //! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e 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 ///do not use this rule, this is for debug only 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.getTriggers(); 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 //! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e 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 //build up a conjunction of type predicates for expression 00171 Expr tr = e.getEM()->trueExpr(); 00172 Expr typePred = tr; 00173 // unsigned qlevel, qlevelMax = 0; 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 // qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]); 00183 // if (qlevel > qlevelMax) qlevel = qlevelMax; 00184 } 00185 00186 00187 // Expr inst = e.getBody().substExprQuant(e.getVars(), terms); 00188 Expr inst = e.getBody().substExpr(e.getVars(), terms); 00189 00190 // Expr inst = e.getBody().substExpr(e.getVars(), terms); 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 // es.insert(es.end(), terms.begin(), terms.end()); 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 // Expr inst = e.getBody().substExpr(e.getVars(), terms); 00212 00213 00214 Expr imp; 00215 // if(typePred == tr || true ) //just for a easy life, yeting, change this assp 00216 if(typePred == tr ) //just for a easy life, yeting, change this assp 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 // ret.setQuantLevel(quantLevel+1); 00231 return ret; 00232 } 00233 00234 00235 //! Instantiate a universally quantified formula 00236 /*! From T|-FORALL(var): e generate T|-psi => e' where e' is obtained 00237 * from e by instantiating bound variables with terms in 00238 * vector<Expr>& terms. The vector of terms should be the same 00239 * size as the vector of bound variables in e. Also elements in 00240 * each position i need to have matching base types. psi is the conjunction of 00241 * subtype predicates for the bound variables of the quanitfied expression. 00242 * \param t1 the quantifier (a Theorem) 00243 * \param terms the terms to instantiate. 00244 * \param quantLevel the quantification level for the formula 00245 */ 00246 Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const vector<Expr>& terms, int quantLevel){ 00247 00248 Expr e = t1.getExpr(); 00249 const vector<Expr>& boundVars = e.getVars(); 00250 if(CHECK_PROOFS) { 00251 CHECK_SOUND(boundVars.size() == terms.size(), 00252 "Universal instantiation: size of terms array does " 00253 "not match quanitfied variables array size"); 00254 CHECK_SOUND(e.isForall(), 00255 "universal instantiation: expr must be FORALL:\n" 00256 +e.toString()); 00257 for(unsigned int i=0; i<terms.size(); i++) 00258 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) == 00259 d_theoryQuant->getBaseType(terms[i]), 00260 "Universal instantiation: type mismatch"); 00261 } 00262 00263 //build up a conjunction of type predicates for expression 00264 Expr tr = e.getEM()->trueExpr(); 00265 Expr typePred = tr; 00266 // unsigned qlevel, qlevelMax = 0; 00267 for(unsigned int i=0; i<terms.size(); i++) { 00268 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]); 00269 if(p!=tr) { 00270 if(typePred==tr) 00271 typePred = p; 00272 else 00273 typePred = typePred.andExpr(p); 00274 } 00275 // qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]); 00276 // if (qlevel > qlevelMax) qlevel = qlevelMax; 00277 } 00278 00279 //Expr inst = e.getBody().substExprQuant(e.getVars(), terms); 00280 Expr inst = e.getBody().substExpr(e.getVars(), terms); 00281 00282 00283 // Expr inst = e.getBody().substExpr(e.getVars(), terms); 00284 00285 00286 Proof pf; 00287 if(withProof()) { 00288 vector<Proof> pfs; 00289 vector<Expr> es; 00290 pfs.push_back(t1.getProof()); 00291 es.push_back(e); 00292 es.push_back(Expr(RAW_LIST,terms)); 00293 // es.insert(es.end(), terms.begin(), terms.end()); 00294 es.push_back(inst); 00295 pf= newPf("universal_elimination2", es, pfs); 00296 } 00297 00298 // Expr inst = e.getBody().substExpr(e.getVars(), terms); 00299 00300 00301 Expr imp; 00302 if(typePred == tr) //just for a easy life, yeting, change this assp 00303 imp = inst; 00304 else 00305 imp = typePred.impExpr(inst); 00306 Theorem ret = newTheorem(imp, t1.getAssumptionsRef(), pf); 00307 00308 int thmLevel = t1.getQuantLevel(); 00309 if(quantLevel >= thmLevel) { 00310 ret.setQuantLevel(quantLevel+1); 00311 } 00312 else{ 00313 ret.setQuantLevel(thmLevel+1); 00314 } 00315 00316 // ret.setQuantLevel(quantLevel+1); 00317 return ret; 00318 } 00319 00320 Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const vector<Expr>& terms){ 00321 00322 Expr e = t1.getExpr(); 00323 const vector<Expr>& boundVars = e.getVars(); 00324 if(CHECK_PROOFS) { 00325 CHECK_SOUND(boundVars.size() == terms.size(), 00326 "Universal instantiation: size of terms array does " 00327 "not match quanitfied variables array size"); 00328 CHECK_SOUND(e.isForall(), 00329 "universal instantiation: expr must be FORALL:\n" 00330 +e.toString()); 00331 for(unsigned int i=0; i<terms.size(); i++) 00332 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) == 00333 d_theoryQuant->getBaseType(terms[i]), 00334 "Universal instantiation: type mismatch"); 00335 } 00336 00337 //build up a conjunction of type predicates for expression 00338 Expr tr = e.getEM()->trueExpr(); 00339 Expr typePred = tr; 00340 unsigned qlevel=0, qlevelMax = 0; 00341 for(unsigned int i=0; i<terms.size(); i++) { 00342 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]); 00343 if(p!=tr) { 00344 if(typePred==tr) 00345 typePred = p; 00346 else 00347 typePred = typePred.andExpr(p); 00348 } 00349 qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]); 00350 if (qlevel > qlevelMax) qlevel = qlevelMax; 00351 } 00352 00353 Expr inst = e.getBody().substExpr(e.getVars(), terms); 00354 // Expr inst = e.getBody().substExprQuant(e.getVars(), terms); 00355 00356 00357 // Expr inst = e.getBody().substExpr(e.getVars(), terms); 00358 00359 Proof pf; 00360 if(withProof()) { 00361 vector<Proof> pfs; 00362 vector<Expr> es; 00363 pfs.push_back(t1.getProof()); 00364 es.push_back(e); 00365 es.push_back(Expr(RAW_LIST,terms)); 00366 // es.insert(es.end(), terms.begin(), terms.end()); 00367 es.push_back(inst); 00368 pf= newPf("universal_elimination3", es, pfs); 00369 } 00370 00371 // Expr inst = e.getBody().substExpr(e.getVars(), terms); 00372 00373 Expr imp; 00374 if( typePred == tr ) //just for easy life, yeting, change this asap 00375 imp = inst; 00376 else 00377 imp = typePred.impExpr(inst); 00378 Theorem ret = newTheorem(imp, t1.getAssumptionsRef(), pf); 00379 00380 00381 unsigned thmLevel = t1.getQuantLevel(); 00382 if(qlevel >= thmLevel) { 00383 ret.setQuantLevel(qlevel+1); 00384 } 00385 else{ 00386 // ret.setQuantLevel(thmLevel+1); 00387 ret.setQuantLevel(thmLevel+1); 00388 } 00389 00390 00391 // ret.setQuantLevel(qlevel+1); 00392 return ret; 00393 } 00394 00395 00396 Theorem QuantTheoremProducer::partialUniversalInst(const Theorem& t1, const vector<Expr>& terms, int quantLevel){ 00397 cout<<"error in partial inst" << endl; 00398 Expr e = t1.getExpr(); 00399 const vector<Expr>& boundVars = e.getVars(); 00400 if(CHECK_PROOFS) { 00401 CHECK_SOUND(boundVars.size() >= terms.size(), 00402 "Universal instantiation: size of terms array does " 00403 "not match quanitfied variables array size"); 00404 CHECK_SOUND(e.isForall(), 00405 "universal instantiation: expr must be FORALL:\n" 00406 +e.toString()); 00407 for(unsigned int i=0; i<terms.size(); i++){ 00408 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) == 00409 d_theoryQuant->getBaseType(terms[i]), 00410 "partial Universal instantiation: type mismatch"); 00411 } 00412 } 00413 00414 //build up a conjunction of type predicates for expression 00415 Expr tr = e.getEM()->trueExpr(); 00416 Expr typePred = tr; 00417 for(unsigned int i=0; i<terms.size(); i++) { 00418 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]); 00419 if(p!=tr) { 00420 if(typePred==tr) 00421 typePred = p; 00422 else 00423 typePred = typePred.andExpr(p); 00424 } 00425 } 00426 Proof pf; 00427 if(withProof()) { 00428 vector<Proof> pfs; 00429 vector<Expr> es; 00430 pfs.push_back(t1.getProof()); 00431 es.push_back(e); 00432 es.insert(es.end(), terms.begin(), terms.end()); 00433 pf= newPf("partial_universal_instantiation", es, pfs); 00434 } 00435 00436 00437 if(terms.size() == boundVars.size()){ 00438 Expr inst = e.getBody().substExpr(e.getVars(), terms); 00439 Expr imp; 00440 if(typePred == tr) 00441 imp = inst; 00442 else 00443 imp = typePred.impExpr(inst); 00444 return(newTheorem(imp, t1.getAssumptionsRef(), pf)); 00445 } 00446 else{ 00447 vector<Expr> newBoundVars; 00448 for(size_t i=0; i<terms.size(); i++) { 00449 newBoundVars.push_back(boundVars[i]); 00450 } 00451 00452 vector<Expr>leftBoundVars; 00453 for(size_t i=terms.size(); i<boundVars.size(); i++) { 00454 leftBoundVars.push_back(boundVars[i]); 00455 } 00456 00457 Expr tempinst = e.getBody().substExpr(newBoundVars, terms); 00458 Expr inst = d_theoryQuant->getEM()->newClosureExpr(FORALL, leftBoundVars, tempinst); 00459 00460 Expr imp; 00461 if(typePred == tr) 00462 imp = inst; 00463 else 00464 imp = typePred.impExpr(inst); 00465 00466 Theorem res = (newTheorem(imp, t1.getAssumptionsRef(), pf)); 00467 int thmLevel = t1.getQuantLevel(); 00468 if(quantLevel >= thmLevel) { 00469 res.setQuantLevel(quantLevel+1); 00470 } 00471 else{ 00472 //k ret.setQuantLevel(thmLevel+1); 00473 res.setQuantLevel(thmLevel); 00474 } 00475 return res; 00476 00477 } 00478 } 00479 00480 //! find all bound variables in e and maps them to true in boundVars 00481 void QuantTheoremProducer::recFindBoundVars(const Expr& e, 00482 ExprMap<bool> & boundVars, ExprMap<bool> &visited) 00483 { 00484 if(visited.count(e)>0) 00485 return; 00486 else 00487 visited[e] = true; 00488 if(e.getKind() == BOUND_VAR) 00489 boundVars[e] = true; 00490 if(e.getKind() == EXISTS || e.getKind() == FORALL) 00491 recFindBoundVars(e.getBody(), boundVars, visited); 00492 for(Expr::iterator it = e.begin(); it!=e.end(); ++it) 00493 recFindBoundVars(*it, boundVars, visited); 00494 00495 } 00496 00497 //!adjust the order of bound vars, newBvs begin first 00498 Theorem QuantTheoremProducer::adjustVarUniv(const Theorem& t1, const std::vector<Expr>& newBvs){ 00499 const Expr e=t1.getExpr(); 00500 const Expr body = e.getBody(); 00501 if(CHECK_PROOFS) { 00502 CHECK_SOUND(e.isForall(), 00503 "adjustVarUniv: " 00504 +e.toString()); 00505 } 00506 00507 const vector<Expr>& origVars = e.getVars(); 00508 00509 00510 ExprMap<bool> oldmap; 00511 for(vector<Expr>::const_iterator it = origVars.begin(), 00512 iend=origVars.end(); it!=iend; ++it) { 00513 oldmap[*it]=true; 00514 } 00515 00516 vector<Expr> quantVars; 00517 for(vector<Expr>::const_iterator it = newBvs.begin(), 00518 iend=newBvs.end(); it!=iend; ++it) { 00519 if(oldmap.count(*it) > 0) 00520 quantVars.push_back(*it); 00521 } 00522 00523 if(quantVars.size() == origVars.size()) 00524 return t1; 00525 00526 ExprMap<bool> newmap; 00527 for(vector<Expr>::const_iterator it = newBvs.begin(), 00528 iend=newBvs.end(); it!=iend; ++it) { 00529 newmap[*it]=true; 00530 } 00531 00532 for(vector<Expr>::const_iterator it = origVars.begin(), 00533 iend=origVars.end(); it!=iend; ++it) { 00534 if(newmap.count(*it)<=0){ 00535 quantVars.push_back(*it); 00536 }; 00537 } 00538 00539 Proof pf; 00540 if(withProof()) { 00541 vector<Expr> es; 00542 vector<Proof> pfs; 00543 es.push_back(e); 00544 es.insert(es.end(), quantVars.begin(), quantVars.end()); 00545 pfs.push_back(t1.getProof()); 00546 pf= newPf("adjustVarUniv", es, pfs); 00547 } 00548 00549 Expr newQuantExpr; 00550 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, quantVars, body); 00551 00552 return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf)); 00553 } 00554 00555 //!pack (forall (x) forall (y)) into (forall (x y)) 00556 Theorem QuantTheoremProducer::packVar(const Theorem& t1){ 00557 Expr out_forall =t1.getExpr(); 00558 00559 if(CHECK_PROOFS) { 00560 CHECK_SOUND(out_forall.isForall(), 00561 "packVar: " 00562 +out_forall.toString()); 00563 } 00564 00565 vector<Expr> bVars = out_forall.getVars(); 00566 00567 if(!out_forall.getBody().isForall()){ 00568 return t1; 00569 } 00570 00571 Expr cur_body = out_forall.getBody(); 00572 00573 while(cur_body.isForall()){ 00574 vector<Expr> bVarsLeft = cur_body.getVars(); 00575 for(vector<Expr>::iterator i=bVarsLeft.begin(), iend=bVarsLeft.end(); i!=iend; i++){ 00576 bVars.push_back(*i); 00577 } 00578 cur_body=cur_body.getBody(); 00579 } 00580 00581 Proof pf; 00582 if(withProof()) { 00583 vector<Expr> es; 00584 vector<Proof> pfs; 00585 es.push_back(out_forall); 00586 es.insert(es.end(), bVars.begin(), bVars.end()); 00587 pfs.push_back(t1.getProof()); 00588 pf= newPf("packVar", es, pfs); 00589 } 00590 00591 Expr newQuantExpr; 00592 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, bVars, cur_body); 00593 00594 return (newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf)); 00595 // return (newRWTheorem(t1,newQuantExpr, t1.getAssumptionsRef(), pf)); 00596 } 00597 00598 //! convert (forall (x) ... forall (y)) into (forall (x y)...) 00599 //! convert (exists (x) ... exists (y)) into (exists (x y)...) 00600 Theorem QuantTheoremProducer::pullVarOut(const Theorem& t1){ 00601 const Expr thm_expr=t1.getExpr(); 00602 00603 if(CHECK_PROOFS) { 00604 CHECK_SOUND(thm_expr.isForall() || thm_expr.isExists(), 00605 "pullVarOut: " 00606 +thm_expr.toString()); 00607 } 00608 00609 const Expr outBody = thm_expr.getBody(); 00610 00611 // if(((outBody.isAnd() && outBody[1].isForall()) || 00612 // (outBody.isImpl() && outBody[1].isForall()) || 00613 // (outBody.isNot() && outBody[0].isAnd() && outBody[0][1].isExists()) )){ 00614 // return t1; 00615 // } 00616 00617 if (thm_expr.isForall()){ 00618 if((outBody.isNot() && outBody[0].isAnd() && outBody[0][1].isExists())){ 00619 00620 vector<Expr> bVarsOut = thm_expr.getVars(); 00621 00622 const Expr innerExists =outBody[0][1]; 00623 const Expr innerBody = innerExists.getBody(); 00624 vector<Expr> bVarsIn = innerExists.getVars(); 00625 00626 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){ 00627 bVarsOut.push_back(*i); 00628 } 00629 00630 Proof pf; 00631 if(withProof()) { 00632 vector<Expr> es; 00633 vector<Proof> pfs; 00634 es.push_back(thm_expr); 00635 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end()); 00636 pfs.push_back(t1.getProof()); 00637 pf= newPf("pullVarOut", es, pfs); 00638 } 00639 00640 Expr newbody; 00641 00642 newbody=(outBody[0][0].notExpr()).orExpr(innerBody.notExpr()); 00643 00644 Expr newQuantExpr; 00645 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, bVarsOut, newbody); 00646 00647 return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf)); 00648 } 00649 00650 else if ((outBody.isAnd() && outBody[1].isForall()) || 00651 (outBody.isImpl() && outBody[1].isForall())){ 00652 00653 vector<Expr> bVarsOut = thm_expr.getVars(); 00654 00655 const Expr innerForall=outBody[1]; 00656 const Expr innerBody = innerForall.getBody(); 00657 vector<Expr> bVarsIn = innerForall.getVars(); 00658 00659 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){ 00660 bVarsOut.push_back(*i); 00661 } 00662 00663 Proof pf; 00664 if(withProof()) { 00665 vector<Expr> es; 00666 vector<Proof> pfs; 00667 es.push_back(thm_expr); 00668 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end()); 00669 pfs.push_back(t1.getProof()); 00670 pf= newPf("pullVarOut", es, pfs); 00671 } 00672 00673 Expr newbody; 00674 if(outBody.isAnd()){ 00675 newbody=outBody[0].andExpr(innerBody); 00676 } 00677 else if(outBody.isImpl()){ 00678 newbody=outBody[0].impExpr(innerBody); 00679 } 00680 00681 Expr newQuantExpr; 00682 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, bVarsOut, newbody); 00683 00684 return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf)); 00685 } 00686 return t1; // case cannot be handled now. 00687 } 00688 00689 else if (thm_expr.isExists()){ 00690 if ((outBody.isAnd() && outBody[1].isExists()) || 00691 (outBody.isImpl() && outBody[1].isExists())){ 00692 00693 vector<Expr> bVarsOut = thm_expr.getVars(); 00694 00695 const Expr innerExists = outBody[1]; 00696 const Expr innerBody = innerExists.getBody(); 00697 vector<Expr> bVarsIn = innerExists.getVars(); 00698 00699 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){ 00700 bVarsOut.push_back(*i); 00701 } 00702 00703 Proof pf; 00704 if(withProof()) { 00705 vector<Expr> es; 00706 vector<Proof> pfs; 00707 es.push_back(thm_expr); 00708 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end()); 00709 pfs.push_back(t1.getProof()); 00710 pf= newPf("pullVarOut", es, pfs); 00711 } 00712 00713 Expr newbody; 00714 if(outBody.isAnd()){ 00715 newbody=outBody[0].andExpr(innerBody); 00716 } 00717 else if(outBody.isImpl()){ 00718 newbody=outBody[0].impExpr(innerBody); 00719 } 00720 00721 Expr newQuantExpr; 00722 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(EXISTS, bVarsOut, newbody); 00723 00724 return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf)); 00725 } 00726 } 00727 return t1; 00728 } 00729 00730 00731 00732 /*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e 00733 * where vars' is obtained from vars by removing all bound variables 00734 * not used in e. If vars' is empty the produced theorem is just T|-e 00735 */ 00736 Theorem QuantTheoremProducer::boundVarElim(const Theorem& t1) 00737 { 00738 const Expr e=t1.getExpr(); 00739 const Expr body = e.getBody(); 00740 if(CHECK_PROOFS) { 00741 CHECK_SOUND(e.isForall() || e.isExists(), 00742 "bound var elimination: " 00743 +e.toString()); 00744 } 00745 ExprMap<bool> boundVars; //a mapping of bound variables in the body to true 00746 ExprMap<bool> visited; //to make sure expressions aren't traversed 00747 //multiple times 00748 recFindBoundVars(body, boundVars, visited); 00749 vector<Expr> quantVars; 00750 const vector<Expr>& origVars = e.getVars(); 00751 for(vector<Expr>::const_iterator it = origVars.begin(), 00752 iend=origVars.end(); it!=iend; ++it) 00753 { 00754 if(boundVars.count(*it) > 0) 00755 quantVars.push_back(*it); 00756 } 00757 00758 // If all variables are used, just return the original theorem 00759 if(quantVars.size() == origVars.size()) 00760 return t1; 00761 00762 Proof pf; 00763 if(withProof()) { 00764 vector<Expr> es; 00765 vector<Proof> pfs; 00766 es.push_back(e); 00767 es.insert(es.end(), quantVars.begin(), quantVars.end()); 00768 pfs.push_back(t1.getProof()); 00769 pf= newPf("bound_variable_elimination", es, pfs); 00770 } 00771 if(quantVars.size() == 0) 00772 return(newTheorem(e.getBody(), t1.getAssumptionsRef(), pf)); 00773 00774 Expr newQuantExpr; 00775 if(e.isForall()) 00776 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, quantVars, body); 00777 else 00778 newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(EXISTS, quantVars, body); 00779 00780 return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf)); 00781 }