00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #include "theory_quant.h"
00021 #include "theory_arith.h"
00022 #include "theory_array.h"
00023 #include "typecheck_exception.h"
00024 #include "parser_exception.h"
00025 #include "smtlib_exception.h"
00026 #include "quant_proof_rules.h"
00027 #include "theory_core.h"
00028 #include "command_line_flags.h"
00029 #include "vcl.h"
00030 #include<string>
00031 #include<string.h>
00032 #include <algorithm>
00033 using namespace std;
00034 using namespace CVC3;
00035
00036
00037
00038
00039
00040 static const Expr null_expr;
00041 const int FOUND_FALSE = 1;
00042
00043 Trigger::Trigger(TheoryCore* core, Expr e, Polarity pol, std::set<Expr> boundVars){
00044 trig=e ;
00045 polarity=pol;
00046 head=null_expr;
00047 hasRWOp=false;
00048 hasTrans=false;
00049 hasT2=false;
00050 isSimple=false;
00051 isSuperSimple=false;
00052 isMulti=false;
00053 multiIndex = 99999;
00054 multiId = 99999;
00055 for(std::set<Expr>::const_iterator i=boundVars.begin(),iend=boundVars.end(); i!=iend; ++i)
00056 bvs.push_back(*i);
00057 }
00058
00059 bool Trigger::isPos(){
00060 return (Pos==polarity||PosNeg==polarity);
00061 }
00062
00063 bool Trigger::isNeg(){
00064 return (Neg==polarity || PosNeg==polarity);
00065 }
00066
00067 std::vector<Expr> Trigger::getBVs(){
00068 return bvs;
00069 }
00070
00071 Expr Trigger::getEx(){
00072 return trig;
00073 }
00074
00075 void Trigger::setHead(Expr h){
00076 head=h;
00077 }
00078
00079 Expr Trigger::getHead(){
00080 return head;
00081 }
00082
00083 void Trigger::setRWOp(bool b){
00084 hasRWOp =b ;
00085 }
00086
00087 bool Trigger::hasRW(){
00088 return hasRWOp;
00089 }
00090
00091 void Trigger::setTrans(bool b){
00092 hasTrans =b ;
00093 }
00094
00095 bool Trigger::hasTr(){
00096 return hasTrans;
00097 }
00098
00099 void Trigger::setTrans2(bool b){
00100 hasT2 =b ;
00101 }
00102
00103 bool Trigger::hasTr2(){
00104 return hasT2;
00105 }
00106
00107 void Trigger::setSimp(){
00108 isSimple =true ;
00109 }
00110
00111 bool Trigger::isSimp(){
00112 return isSimple;
00113 }
00114
00115 void Trigger::setSuperSimp(){
00116 isSuperSimple =true ;
00117 }
00118
00119 bool Trigger::isSuperSimp(){
00120 return isSuperSimple;
00121 }
00122
00123 void Trigger::setMultiTrig(){
00124 isMulti = true ;
00125 }
00126
00127 bool Trigger::isMultiTrig(){
00128 return isMulti;
00129 }
00130
00131
00132 dynTrig::dynTrig(Trigger t, ExprMap<Expr> b, size_t id)
00133 :trig(t),
00134 univ_id(id),
00135 binds(b)
00136 {}
00137
00138 TheoryQuant::TheoryQuant(TheoryCore* core)
00139 : Theory(core, "Quantified Expressions"),
00140 d_univs(core->getCM()->getCurrentContext()),
00141 d_rawUnivs(core->getCM()->getCurrentContext()),
00142 d_arrayTrigs(core->getCM()->getCurrentContext()),
00143 d_lastArrayPos(core->getCM()->getCurrentContext(), 0 , 0),
00144 d_lastPredsPos(core->getCM()->getCurrentContext(), 0, 0),
00145 d_lastTermsPos(core->getCM()->getCurrentContext(), 0, 0),
00146 d_lastPartPredsPos(core->getCM()->getCurrentContext(), 0, 0),
00147 d_lastPartTermsPos(core->getCM()->getCurrentContext(), 0, 0),
00148 d_univsPartSavedPos(core->getCM()->getCurrentContext(), 0, 0),
00149 d_lastPartLevel(core->getCM()->getCurrentContext(), 0, 0),
00150 d_usefulGterms(core->getCM()->getCurrentContext()),
00151 d_lastUsefulGtermsPos(core->getCM()->getCurrentContext(), 0, 0),
00152 d_savedTermsPos(core->getCM()->getCurrentContext(), 0, 0),
00153 d_univsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
00154 d_rawUnivsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
00155 d_univsPosFull(core->getCM()->getCurrentContext(), 0, 0),
00156 d_univsContextPos(core->getCM()->getCurrentContext(), 0, 0),
00157 d_instCount(core->getCM()->getCurrentContext(), 0,0),
00158 d_contextTerms(core->getCM()->getCurrentContext()),
00159 d_contextCache(core->getCM()->getCurrentContext()),
00160 d_maxQuantInst(&(core->getFlags()["max-quant-inst"].getInt())),
00161 d_useNew(&(core->getFlags()["quant-new"].getBool())),
00162 d_useLazyInst(&(core->getFlags()["quant-lazy"].getBool())),
00163 d_useSemMatch(&(core->getFlags()["quant-sem-match"].getBool())),
00164 d_useAtomSem(&(core->getFlags()["quant-const-match"].getBool())),
00165 d_translate(&(core->getFlags()["translate"].getBool())),
00166 d_useTrigNew(&(core->getFlags()["quant-trig-new"].getBool())),
00167 d_usePart(&(core->getFlags()["quant-inst-part"].getBool())),
00168 d_useMult(&(core->getFlags()["quant-inst-mult"].getBool())),
00169 d_useInstEnd(&(core->getFlags()["quant-inst-end"].getBool())),
00170 d_useInstLCache(&(core->getFlags()["quant-inst-lcache"].getBool())),
00171 d_useInstGCache(&(core->getFlags()["quant-inst-gcache"].getBool())),
00172 d_useInstTrue(&(core->getFlags()["quant-inst-true"].getBool())),
00173 d_usePullVar(&(core->getFlags()["quant-pullvar"].getBool())),
00174 d_useExprScore(&(core->getFlags()["quant-score"].getBool())),
00175 d_useTrigLoop(&(core->getFlags()["quant-trig-loop"].getInt())),
00176 d_maxInst(&(core->getFlags()["quant-max-inst"].getInt())),
00177 d_useTrans(&(core->getFlags()["quant-trans3"].getBool())),
00178 d_useTrans2(&(core->getFlags()["quant-trans2"].getBool())),
00179 d_useInstAll(&(core->getFlags()["quant-inst-all"].getBool())),
00180 d_usePolarity(&(core->getFlags()["quant-polarity"].getBool())),
00181 d_useEqu(&(core->getFlags()["quant-equ"].getBool())),
00182 d_maxNaiveCall(&(core->getFlags()["quant-naive-num"].getInt())),
00183 d_curMaxExprScore(core->getCM()->getCurrentContext(), (core->getFlags()["quant-max-score"].getInt()),0),
00184 d_arrayIndic(core->getCM()->getCurrentContext()),
00185 d_exprLastUpdatedPos(core->getCM()->getCurrentContext(),0 ,0),
00186 d_trans_found(core->getCM()->getCurrentContext()),
00187 d_trans2_found(core->getCM()->getCurrentContext()),
00188 null_cdlist(core->getCM()->getCurrentContext()),
00189 d_eqs(core->getCM()->getCurrentContext()),
00190 d_eqs_pos(core->getCM()->getCurrentContext(), 0, 0),
00191 d_allInstCount(core->getStatistics().counter("quantifier instantiations")),
00192 d_partCalled(core->getCM()->getCurrentContext(),false,0),
00193 d_instHistory(core->getCM()->getCurrentContext()),
00194 d_alltrig_list(core->getCM()->getCurrentContext())
00195 {
00196 IF_DEBUG(d_univs.setName("CDList[TheoryQuant::d_univs]"));
00197 vector<int> kinds;
00198 d_instCount = 0;
00199 d_cacheThmPos=0;
00200 d_trans_num=0;
00201 d_trans2_num=0;
00202 d_rules=createProofRules();
00203 kinds.push_back(EXISTS);
00204 kinds.push_back(FORALL);
00205 registerTheory(this, kinds);
00206 d_partCalled=false;
00207 d_offset_multi_trig=2;
00208 d_initMaxScore=(theoryCore()->getFlags()["quant-max-score"].getInt());
00209 for(size_t i=0; i<MAX_TRIG_BVS; i++){
00210 d_mybvs[i] = getEM()->newBoundVarExpr("_genbv", int2string(i), Type::anyType(getEM()));
00211 }
00212 }
00213
00214
00215 TheoryQuant::~TheoryQuant() {
00216 if(d_rules != NULL) delete d_rules;
00217 for(std::map<Type, CDList<size_t>* ,TypeComp>::iterator
00218 it = d_contextMap.begin(), iend = d_contextMap.end();
00219 it!= iend; ++it) {
00220 delete it->second;
00221 free(it->second);
00222 }
00223 }
00224
00225 int TheoryQuant::getExprScore(const Expr& e){
00226 return theoryCore()->getQuantLevelForTerm(e);
00227 }
00228
00229 bool isSysPred(const Expr& e){
00230 return ( isLE(e) || isLT(e) || isGE(e) || isGT(e) || e.isEq());
00231 }
00232
00233 bool canGetHead(const Expr& e){
00234 return (e.getKind() == APPLY || e.getKind() == READ || e.getKind() == WRITE);
00235 }
00236
00237 bool isSimpleTrig(const Expr& t){
00238 if(!canGetHead(t)) return false;
00239 for(int i = 0; i < t.arity(); i++){
00240 if (t[i].arity()>0 && t[i].containsBoundVar()) return false;
00241 if (BOUND_VAR == t[i].getKind()){
00242 for(int j = 0; j < i; j++){
00243 if(t[i] == t[j]) return false;
00244 }
00245 }
00246 }
00247 return true;
00248 }
00249
00250 bool isSuperSimpleTrig(const Expr& t){
00251 if(!isSimpleTrig(t)) return false;
00252 for(int i = 0; i < t.arity(); i++){
00253 if (t[i].arity()>0 ) return false;
00254 if (BOUND_VAR != t[i].getKind()){
00255 return false;
00256 }
00257 }
00258 return true;
00259 }
00260
00261
00262 bool usefulInMatch(const Expr& e){
00263 if(e.arity() == 0){
00264 TRACE("usefulInMatch", e.toString()+": ",e.arity(), "");
00265 TRACE("usefulInMatch", e.isRational(), "", "");
00266 }
00267 return ( canGetHead(e) || (isSysPred(e) && (!e.isEq()) ) );
00268 }
00269
00270 void TheoryQuant::setup(const Expr& e) {}
00271
00272 void TheoryQuant::update(const Theorem& t, const Expr& e) {
00273 }
00274
00275 std::string vectorExpr2string(const std::vector<Expr> & vec){
00276 std::string buf;
00277 for(size_t i=0; i<vec.size(); i++){
00278 buf.append(vec[i].toString());
00279 buf.append(" # ");
00280 }
00281 return buf;
00282 }
00283
00284 static void recursiveGetSubTrig(const Expr& e, std::vector<Expr> & res) {
00285 if(e.getFlag())
00286 return;
00287
00288 if(e.isClosure())
00289 return recursiveGetSubTrig(e.getBody(),res);
00290
00291 if (e.isApply()|| isSysPred(e)){
00292 res.push_back(e);
00293 }
00294 else
00295 if ( e.isTerm() && (!e.isVar()) && (e.getKind()!=RATIONAL_EXPR) ) {
00296 res.push_back(e);
00297 }
00298
00299 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00300 recursiveGetSubTrig(*i,res);
00301 }
00302
00303 e.setFlag();
00304 return ;
00305 }
00306
00307 std::vector<Expr> getSubTrig(const Expr& e){
00308 e.clearFlags();
00309 std::vector<Expr> res;
00310 recursiveGetSubTrig(e,res);
00311 e.clearFlags();
00312 TRACE("getsub","e is ", e.toString(),"");
00313 TRACE("getsub","have ", res.size()," subterms");
00314 return res;
00315 }
00316
00317 static void recGetSubTerms(const Expr& e, std::vector<Expr> & res) {
00318 if(e.getFlag())
00319 return;
00320
00321 if(e.isClosure())
00322 return recGetSubTerms(e.getBody(),res);
00323
00324 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00325 recGetSubTerms(*i,res);
00326 }
00327
00328 res.push_back(e);
00329
00330 e.setFlag();
00331 return ;
00332 }
00333
00334 const std::vector<Expr>& TheoryQuant::getSubTerms(const Expr& e){
00335
00336 ExprMap<std::vector<Expr> >::iterator iter= d_subTermsMap.find(e);
00337 if( d_subTermsMap.end() == iter){
00338 e.clearFlags();
00339 std::vector<Expr> res;
00340 recGetSubTerms(e,res);
00341 e.clearFlags();
00342
00343 TRACE("getsubs", "getsubs, e is: ", e, "");
00344 TRACE("getsubs", "e has ", res.size(), " subterms");
00345
00346 d_subTermsMap[e] = res;
00347 return d_subTermsMap[e];
00348 }
00349 else{
00350 return (*iter).second;
00351 }
00352 }
00353
00354 void TheoryQuant::enqueueInst(const Theorem& univ, const vector<Expr>& bind, const Expr& gterm){
00355 static int max_score =-1;
00356
00357 bool partInst=false;
00358 if(bind.size() < univ.getExpr().getVars().size()){
00359 partInst=false;
00360 TRACE("sendinst","partinst",partInst,"");
00361 }
00362
00363 Expr bind_expr(RAW_LIST, bind, getEM());
00364
00365 if (*d_useInstLCache){
00366 const Expr& e = univ.getExpr();
00367 ExprMap<CDMap<Expr,bool>*>::iterator iterCache = d_bindHistory.find(e);
00368 if (iterCache != d_bindHistory.end()){
00369 CDMap<Expr,bool>* cache = (*iterCache).second;
00370 if(cache->find(bind_expr) !=cache->end()){
00371 return ;
00372 }
00373 else{
00374 (*cache)[bind_expr] = true;
00375 }
00376 }
00377 else{
00378 CDMap<Expr,bool>* new_cache = new(true) CDMap<Expr,bool> (theoryCore()->getCM()->getCurrentContext());
00379 (*new_cache)[bind_expr] = true;
00380 }
00381 }
00382
00383 Theorem thm ;
00384 if(null_expr == gterm ){
00385 TRACE("sendinst","gterm",gterm,"");
00386 if(partInst) {
00387 thm = d_rules->partialUniversalInst(univ, bind, 0);
00388 }
00389 else{
00390 thm = d_rules->universalInst(univ, bind, 0);
00391 }
00392 }
00393 else{
00394 int gscore = theoryCore()->getQuantLevelForTerm(gterm);
00395 if(gscore > max_score){
00396 max_score = gscore;
00397
00398 }
00399 if(partInst) {
00400 thm = d_rules->partialUniversalInst(univ, bind, gscore);
00401 }
00402 else{
00403 thm = d_rules->universalInst(univ, bind, gscore);
00404 }
00405 }
00406
00407 Theorem simpThm = simplify(thm.getExpr());
00408
00409 if(*d_useInstTrue){
00410 Expr res = simpThm.getRHS();
00411 if(res.isTrue()){
00412 return;
00413 }
00414 if(res.isFalse() ){
00415 enqueueFact(thm);
00416
00417 d_allInstCount++;
00418 d_instThisRound++;
00419 throw FOUND_FALSE;
00420 }
00421 }
00422
00423 d_simplifiedThmQueue.push(thm);
00424
00425 TRACE("quant sendinst", "=gterm: ",gterm, "");
00426 TRACE("quant sendinst", "==add fact simp =", simplifyExpr(thm.getExpr()), "");
00427 TRACE("quant sendinst", "==add fact org =", thm.getExpr(), "");
00428 TRACE("quant sendinst", "==add fact from= ", univ.getExpr(), "\n===: "+vectorExpr2string(bind));
00429 }
00430
00431
00432 void TheoryQuant::enqueueInst(size_t univ_id , const std::vector<Expr>& bind, const Expr& gterm){
00433 static int max_score =-1;
00434
00435 const Theorem& univ = d_univs[univ_id];
00436
00437 bool partInst=false;
00438 if(bind.size() < univ.getExpr().getVars().size()){
00439 partInst=false;
00440 TRACE("sendinst","partinst",partInst,"");
00441 }
00442
00443 Expr bind_expr(RAW_LIST, bind, getEM());
00444
00445 if (*d_useInstLCache){
00446 const Expr& e = univ.getExpr();
00447 ExprMap<CDMap<Expr,bool>*>::iterator iterCache = d_bindHistory.find(e);
00448 if (iterCache != d_bindHistory.end()){
00449 CDMap<Expr,bool>* cache = (*iterCache).second;
00450 if(cache->find(bind_expr) !=cache->end()){
00451 return ;
00452 }
00453 else{
00454 (*cache)[bind_expr] = true;
00455 }
00456 }
00457 else{
00458 CDMap<Expr,bool>* new_cache = new(true) CDMap<Expr,bool> (theoryCore()->getCM()->getCurrentContext());
00459 (*new_cache)[bind_expr] = true;
00460 }
00461 }
00462
00463 Theorem thm ;
00464 if(null_expr == gterm ){
00465 TRACE("sendinst","gterm",gterm,"");
00466 if(partInst) {
00467 thm = d_rules->partialUniversalInst(univ, bind, 0);
00468 }
00469 else{
00470 thm = d_rules->universalInst(univ, bind, 0);
00471 }
00472 }
00473 else{
00474 int gscore = theoryCore()->getQuantLevelForTerm(gterm);
00475 if(gscore > max_score){
00476 max_score = gscore;
00477
00478 }
00479 if(partInst) {
00480 thm = d_rules->partialUniversalInst(univ, bind, gscore);
00481 }
00482 else{
00483 thm = d_rules->universalInst(univ, bind, gscore);
00484 }
00485 }
00486
00487 Theorem simpThm = simplify(thm.getExpr());
00488
00489 if(*d_useInstTrue){
00490 Expr res = simpThm.getRHS();
00491 if(res.isTrue()){
00492 return;
00493 }
00494 if(res.isFalse() ){
00495 enqueueFact(thm);
00496
00497 d_allInstCount++;
00498 d_instThisRound++;
00499 throw FOUND_FALSE;
00500 }
00501 }
00502
00503 d_simplifiedThmQueue.push(thm);
00504
00505 TRACE("quant sendinst", "=gterm: ",gterm, "");
00506 TRACE("quant sendinst", "==add fact simp =", simplifyExpr(thm.getExpr()), "");
00507 TRACE("quant sendinst", "==add fact org =", thm.getExpr(), "");
00508 TRACE("quant sendinst", "==add fact from= ", univ.getExpr(), "\n===: "+vectorExpr2string(bind));
00509 }
00510
00511
00512 void TheoryQuant::enqueueInst(const Theorem& univ,
00513 Trigger& trig,
00514 const std::vector<Expr>& binds,
00515 const Expr& gterm
00516 ) {
00517 return enqueueInst(univ,binds,gterm);
00518 }
00519
00520 int TheoryQuant::sendInstNew(){
00521 int resNum = 0 ;
00522
00523 while(!d_simplifiedThmQueue.empty()){
00524 const Theorem thm = d_simplifiedThmQueue.front();
00525 d_simplifiedThmQueue.pop();
00526
00527 d_allInstCount++;
00528 d_instThisRound++;
00529 resNum++;
00530 enqueueFact(thm);
00531 }
00532
00533 return resNum;
00534 }
00535
00536 void TheoryQuant::addNotify(const Expr& e){}
00537
00538 int recursiveExprScore(const Expr& e) {
00539 int res=0;
00540 DebugAssert(!(e.isClosure()), "exprScore called on closure");
00541
00542 if(e.arity()== 0){
00543 res = 0;
00544 }
00545 else{
00546 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00547 res += recursiveExprScore(*i);
00548 }
00549 }
00550 res++;
00551 return res;
00552 }
00553
00554 int exprScore(const Expr& e){
00555 return recursiveExprScore(e);
00556 }
00557
00558 Expr getHeadExpr(const Expr& e){
00559 if (e.getKind() == APPLY){
00560 return e.getOp().getExpr();
00561 }
00562
00563 if ( READ == e.getKind() || WRITE == e.getKind() ) {
00564 int kind = e[0].getKind();
00565 if (UCONST==kind) {
00566 return e[0];
00567 }
00568 else if (APPLY==kind || UFUNC == kind || READ == kind || WRITE == kind){
00569 return getHeadExpr(e[0]);
00570 }
00571 else if(e[0].isSkolem()){
00572 return e[0];
00573 }
00574 }
00575
00576 return null_expr;
00577 }
00578
00579 Expr getHead(const Expr& e) {
00580 return getHeadExpr(e);
00581 }
00582
00583
00584 static bool recursiveGetBoundVars(const Expr& e, std::set<Expr>& result) {
00585 bool res(false);
00586 if(e.getFlag()){
00587 return e.containsBoundVar();
00588 }
00589 else if(e.isClosure()){
00590 res = recursiveGetBoundVars(e.getBody(),result);
00591 }
00592 else if (BOUND_VAR == e.getKind() ){
00593 result.insert(e);
00594 e.setContainsBoundVar();
00595 res = true;
00596 }
00597 else {
00598 res = false;
00599 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i){
00600 if(recursiveGetBoundVars(*i,result)){
00601 res = true;
00602 }
00603 }
00604 }
00605
00606 e.setFlag();
00607
00608 if(res) {
00609 e.setContainsBoundVar();
00610 }
00611
00612 return res;
00613 }
00614
00615
00616
00617 std::set<Expr> getBoundVars(const Expr& e){
00618
00619
00620
00621
00622
00623
00624
00625
00626
00627
00628
00629 e.clearFlags();
00630 std::set<Expr> result ;
00631 recursiveGetBoundVars(e,result);
00632 e.clearFlags();
00633
00634 return result;
00635 }
00636
00637 bool isGoodSysPredTrigger(const Expr& e){
00638 if(!isSysPred(e)) return false;
00639 if(usefulInMatch(e[0]) || usefulInMatch(e[1])) return true;
00640 return false;
00641 }
00642
00643 bool isGoodFullTrigger(const Expr& e, const std::vector<Expr>& bVarsThm){
00644 if( !usefulInMatch(e))
00645 return false;
00646
00647 const std::set<Expr>& bvs = getBoundVars(e);
00648
00649 if (bvs.size() >= bVarsThm.size()){
00650 for(size_t i=0; i<bVarsThm.size(); i++) {
00651 if (bvs.find(bVarsThm[i]) == bvs.end()){
00652 return false;
00653 }
00654 }
00655 return true;
00656 }
00657 else {
00658 return false;
00659 }
00660 }
00661
00662 bool isGoodMultiTrigger(const Expr& e, const std::vector<Expr>& bVarsThm, int offset){
00663 if( !usefulInMatch(e) )
00664 return false;
00665
00666 int bvar_missing = 0;
00667 const std::set<Expr>& bvs = getBoundVars(e);
00668
00669 if(bvs.size() <= 0) return false;
00670
00671 for(size_t i=0; i<bVarsThm.size(); i++) {
00672 if (bvs.find(bVarsThm[i]) == bvs.end()){
00673 bvar_missing++;
00674 }
00675 }
00676
00677 if (0 == bvar_missing){
00678 return false;
00679 }
00680
00681 if(bvar_missing <= offset){
00682 if(isSysPred(e)){
00683 if (isGoodSysPredTrigger(e)) {
00684 return true;
00685 }
00686 else {
00687 return false;
00688 }
00689 }
00690 else {
00691 return true;
00692 }
00693 }
00694 return false;
00695 }
00696
00697 bool isGoodPartTrigger(const Expr& e, const std::vector<Expr>& bVarsThm){
00698 if( !usefulInMatch(e) )
00699 return false;
00700
00701 size_t bvar_missing = 0;
00702 const std::set<Expr>& bvs = getBoundVars(e);
00703
00704 for(size_t i=0; i<bVarsThm.size(); i++) {
00705 if (bvs.find(bVarsThm[i]) == bvs.end()){
00706 bvar_missing++;
00707 }
00708 }
00709
00710 if (0 == bvar_missing){
00711 return false;
00712 }
00713
00714 if(0 == bvs.size()){
00715 return false;
00716 }
00717
00718 if(bvar_missing < bVarsThm.size()){
00719 if(isSysPred(e)){
00720 if (isGoodSysPredTrigger(e)) {
00721 return true;
00722 }
00723 else {
00724 return false;
00725 }
00726 }
00727 else {
00728 return true;
00729 }
00730 }
00731 return false;
00732 }
00733
00734
00735 static bool recursiveGetPartTriggers(const Expr& e, std::vector<Expr>& res) {
00736 if(e.getFlag())
00737 return false;
00738
00739 if(e.isClosure())
00740 return recursiveGetPartTriggers(e.getBody(), res);
00741
00742 if(0 == e.arity()){
00743 if(BOUND_VAR == e.getKind()){
00744 return false;
00745 }
00746 else{
00747 return true;
00748 }
00749 }
00750
00751 bool good=true;
00752 bool no_bound =true;
00753
00754 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00755 if(BOUND_VAR == i->getKind()){
00756 no_bound=false;
00757 continue;
00758 }
00759 bool temp = recursiveGetPartTriggers(*i,res);
00760 if(false == temp) {
00761 good=false;
00762 }
00763 }
00764
00765 e.setFlag();
00766
00767 if(good && no_bound) {
00768 return true;
00769 }
00770 else if(good && !no_bound){
00771 res.push_back(e);
00772 return false;
00773 }
00774 else{
00775 return false;
00776 }
00777 }
00778
00779
00780 std::vector<Expr> getPartTriggers(const Expr& e){
00781 e.clearFlags();
00782 std::vector<Expr> res;
00783 recursiveGetPartTriggers(e,res);
00784 e.clearFlags();
00785 return res;
00786 }
00787
00788 int trigInitScore(const Expr& e){
00789 if( isSysPred(e) && !isGoodSysPredTrigger(e)){
00790 return 1;
00791 }
00792 else {
00793 return 0;
00794 }
00795 }
00796
00797 void findPolarity(const Expr& e, ExprMap<Polarity>& res, Polarity pol){
00798 if(!e.getType().isBool()) return;
00799
00800 if(res.count(e)>0){
00801 if ((Neg == res[e] && Pos == pol) || (Neg == res[e] && Pos == pol) ){
00802 res[e]=PosNeg;
00803 }
00804 }
00805 else{
00806 res[e]=pol;
00807 }
00808
00809 if(PosNeg==pol){
00810 for(int i=0; i<e.arity(); i++){
00811 findPolarity(e[i], res, pol);
00812 }
00813 }
00814 else{
00815 Polarity neg_pol=Ukn;
00816 if(Pos == pol) {
00817 neg_pol = Neg;
00818 }
00819 else if(Neg == pol){
00820 neg_pol = Pos;
00821 }
00822
00823 if(e.isImpl()){
00824 findPolarity(e[0], res, neg_pol);
00825 findPolarity(e[1], res, pol);
00826 }
00827 else if(e.isAnd() || e.isOr()){
00828 for(int i=0; i<e.arity(); i++){
00829 findPolarity(e[i], res, pol);
00830 }
00831 }
00832 else if(e.isNot()){
00833 findPolarity(e[0], res, neg_pol);
00834 }
00835 else if(e.isITE()){
00836 findPolarity(e[0], res, PosNeg);
00837 findPolarity(e[1], res, pol);
00838 findPolarity(e[2], res, pol);
00839 }
00840 else if(e.isClosure()){
00841 findPolarity(e.getBody(), res, pol);
00842 }
00843 else if(e.isIff()){
00844 findPolarity(e[0], res, PosNeg);
00845 findPolarity(e[1], res, PosNeg);
00846 }
00847 else if(e.isXor()){
00848 findPolarity(e[0], res, neg_pol);
00849 findPolarity(e[1], res, neg_pol);
00850 }
00851 else if(e.isAtomicFormula()){
00852 return;
00853 }
00854 else{
00855 DebugAssert(false, "Error in find polarity in "+e.toString());
00856 }
00857 }
00858 }
00859
00860 void TheoryQuant::arrayIndexName(const Expr& e){
00861 std::vector<Expr> res;
00862
00863 const std::vector<Expr>& subs=getSubTerms(e);
00864
00865 for(size_t i=0; i<subs.size(); i++){
00866 int kind = subs[i].getKind();
00867 if (READ == kind || WRITE == kind){
00868 const Expr& name = subs[i][0];
00869 const Expr& index = subs[i][1];
00870 if(getBoundVars(name).size() <= 0 && (getBoundVars(index).size() <=0)){
00871 std::vector<Expr> tp = d_arrayIndic[name];
00872 tp.push_back(index);
00873 d_arrayIndic[name]=tp;
00874 }
00875 else {
00876 }
00877 }
00878 }
00879 }
00880
00881 void TheoryQuant::registerTrig(ExprMap<ExprMap<std::vector<dynTrig>* >* >& cur_trig_map,
00882 Trigger trig,
00883 const std::vector<Expr> thmBVs,
00884 size_t univ_id){
00885 {
00886 if(trig.hasRWOp){
00887 ExprMap<Expr> bv_map;
00888 dynTrig newDynTrig(trig, bv_map,univ_id);
00889 d_arrayTrigs.push_back(newDynTrig);
00890 }
00891 }
00892
00893 ExprMap<Expr> bv_map;
00894 for(size_t i = 0; i<thmBVs.size(); i++){
00895 bv_map[thmBVs[i]] = null_expr;
00896 }
00897 const Expr& trig_ex = trig.getEx();
00898
00899 Expr genTrig = generalTrig(trig_ex, bv_map);
00900
00901 dynTrig newDynTrig(trig,bv_map,univ_id);
00902
00903 Expr head = trig.getHead();
00904
00905 ExprMap<ExprMap<vector<dynTrig>* >* >::iterator iter = cur_trig_map.find(head);
00906 if(cur_trig_map.end() == iter){
00907 ExprMap<vector<dynTrig>* >* new_cd_map= new ExprMap<vector<dynTrig>* > ;
00908 cur_trig_map[head] = new_cd_map;
00909 vector<dynTrig>* new_dyntrig_list = new vector<dynTrig>;
00910 (*new_cd_map)[genTrig] = new_dyntrig_list;
00911 (*new_dyntrig_list).push_back(newDynTrig);
00912 }
00913 else{
00914 ExprMap<vector<dynTrig>* >* cd_map = iter->second;
00915 ExprMap<vector<dynTrig>* >::iterator iter_map = cd_map->find(genTrig);
00916 if(cd_map->end() == iter_map){
00917 vector<dynTrig>* new_dyntrig_list = new vector<dynTrig>;
00918 (*cd_map)[genTrig] = new_dyntrig_list;
00919 (*new_dyntrig_list).push_back(newDynTrig);
00920 }
00921 else{
00922
00923 (*(iter_map->second)).push_back(newDynTrig);
00924 }
00925 }
00926 }
00927
00928
00929
00930
00931
00932
00933
00934
00935
00936
00937
00938
00939
00940
00941
00942
00943
00944
00945
00946
00947
00948
00949
00950
00951
00952
00953
00954
00955
00956
00957
00958
00959
00960
00961
00962
00963
00964
00965
00966
00967
00968
00969 Expr TheoryQuant::generalTrig(const Expr& trig, ExprMap<Expr>& bvs){
00970 size_t count =1 ;
00971 Expr res = recGeneralTrig(trig, bvs, count);
00972 getBoundVars(res);
00973 return res;
00974 }
00975
00976 Expr TheoryQuant::recGeneralTrig(const Expr& trig, ExprMap<Expr>& bvs, size_t& mybvs_count){
00977
00978 if (!trig.containsBoundVar()) return trig;
00979 if (BOUND_VAR == trig.getKind()){
00980 if (bvs.find(trig) != bvs.end()){
00981 const Expr& ubv = bvs[trig];
00982 if(null_expr ==ubv){
00983 Expr new_bv = d_mybvs[mybvs_count++];
00984 bvs[trig] = new_bv ;
00985 if((mybvs_count) >= MAX_TRIG_BVS ){
00986 throw "general trig error";
00987 }
00988 else{
00989 return new_bv;
00990 }
00991 }
00992 else{
00993 return bvs[trig];
00994 }
00995 }
00996 else{
00997 return d_mybvs[0];
00998 }
00999 }
01000 else{
01001 vector<Expr> children;
01002 for(Expr::iterator i=trig.begin(), iend=trig.end(); i!=iend; ++i){
01003 Expr repChild;
01004 if(i->containsBoundVar()){
01005 repChild = recGeneralTrig(*i, bvs, mybvs_count);
01006 }
01007 else{
01008 repChild = *i;
01009 }
01010 children.push_back(repChild);
01011 }
01012 return Expr(trig.getOp(), children);
01013 }
01014 }
01015
01016
01017
01018 bool TheoryQuant::canMatch(const Expr& t1, const Expr& t2, ExprMap<Expr>& env){
01019 if(getBaseType(t1) != getBaseType(t2)) return false;
01020
01021 if (BOUND_VAR == t1.getKind() || BOUND_VAR == t2.getKind()) {
01022 return true;
01023 }
01024
01025 if ( (t1.arity() != t2.arity()) || (t1.getKind() != t2.getKind() )) {
01026 return false;
01027 }
01028 if (canGetHead(t1) && canGetHead(t2)) {
01029 if ( getHead(t1) != getHead(t2) ){
01030 return false;
01031 }
01032 for(int i=0; i<t1.arity(); i++){
01033 if (false == canMatch(t1[i], t2[i] , env))
01034 return false;
01035 }
01036 return true;
01037 }
01038 else{
01039 return false;
01040 }
01041 }
01042
01043 bool TheoryQuant::isTransLike (const vector<Expr>& cur_trig){
01044 if(!(*d_useTrans)){
01045 return false;
01046 }
01047 if(3==cur_trig.size()){
01048 const Expr& t1=cur_trig[0];
01049 const Expr& t2=cur_trig[1];
01050 const Expr& t3=cur_trig[2];
01051 if ( canGetHead(t1) && canGetHead(t2) && canGetHead(t3) &&
01052 (getHead(t1) == getHead(t2)) && (getHead(t2) == getHead(t3))){
01053 const std::set<Expr>& ts1 = getBoundVars(t1);
01054 const std::set<Expr>& ts2 = getBoundVars(t2);
01055 const std::set<Expr>& ts3 = getBoundVars(t3);
01056 if ( 2==ts1.size() && 2==ts2.size() && 2==ts2.size() &&
01057 (ts1 != ts2) && (ts2 != ts3) && (ts3 != ts1)){
01058 std::set<Expr> all;
01059 for(set<Expr>::const_iterator i=ts1.begin(), iend = ts1.end(); i != iend; i++){
01060 all.insert(*i);
01061 }
01062 for(set<Expr>::const_iterator i=ts2.begin(), iend = ts2.end(); i != iend; i++){
01063 all.insert(*i);
01064 }
01065 for(set<Expr>::const_iterator i=ts3.begin(), iend = ts3.end(); i != iend; i++){
01066 all.insert(*i);
01067 }
01068 bool res = true;
01069 if(3==all.size()){
01070 for(set<Expr>::const_iterator i=all.begin(), iend = all.end(); i != iend; i++){
01071 if(!i->isVar()) {
01072 res = false;
01073 break;
01074 }
01075 }
01076 if(res) {
01077 }
01078 return res;
01079 }
01080 }
01081 }
01082 }
01083 return false;
01084 }
01085
01086 bool TheoryQuant::isTrans2Like (const std::vector<Expr>& all_terms, const Expr& tr2){
01087 if(!(*d_useTrans2)){
01088 return false;
01089 }
01090 for(size_t i = 0; i < all_terms.size(); i++){
01091 if(all_terms[i].isEq()){
01092 const Expr& cur = all_terms[i];
01093 if(cur[0] != cur[1] && ( (cur[0]==tr2[0] && cur[1]==tr2[1]) || (cur[0]==tr2[1] && cur[1]==tr2[0]))){
01094 return true;
01095 }
01096 }
01097 }
01098 return false;
01099 }
01100
01101
01102 bool goodMultiTriggers(const std::vector<Expr>& exprs, const std::vector<Expr> bVars){
01103 ExprMap<bool> bvar_found;
01104
01105 for( std::vector<Expr>::const_iterator i = bVars.begin(), iend= bVars.end(); i!=iend; i++) {
01106 bvar_found[*i]=false;
01107 }
01108
01109 for (size_t i=0; i< exprs.size();i++){
01110 const std::set<Expr> & bv_in_trig = getBoundVars(exprs[i]);
01111 for(std::set<Expr>::const_iterator j=bv_in_trig.begin(), jend = bv_in_trig.end(); j != jend; j++){
01112 if(bvar_found.find(*j) != bvar_found.end()){
01113 bvar_found[*j]=true;
01114 }
01115 }
01116 }
01117
01118 for( std::vector<Expr>::const_iterator i = bVars.begin(), iend= bVars.end(); i!=iend; i++) {
01119 if(false == bvar_found[*i]){
01120 return false ;
01121 }
01122 }
01123 return true;
01124 }
01125
01126
01127 inline size_t locVar(const vector<Expr>& bvsThm, const Expr& bv){
01128 for(size_t i=0, iend = bvsThm.size(); i < iend; i++){
01129 if (bvsThm[i] == bv){
01130 return i;
01131 }
01132 }
01133 return 999;
01134 }
01135
01136 void TheoryQuant::setupTriggers(const Theorem& thm, size_t univs_id){
01137 }
01138
01139 void TheoryQuant::setupTriggers(ExprMap<ExprMap<vector<dynTrig>* >*>& trig_maps,
01140 const Theorem& thm,
01141 size_t univs_id){
01142 const Expr& e = thm.getExpr();
01143 TRACE("triggers","setup : ",e.toString()," || ");
01144
01145 d_univs.push_back(thm);
01146 const std::vector<Expr>& bVarsThm = e.getVars();
01147 if (d_hasTriggers.count(e) > 0) {
01148 std::vector<Trigger>& new_trigs = d_fullTrigs[e];
01149 for(size_t i=0; i<new_trigs.size(); i++){
01150 registerTrig(trig_maps, new_trigs[i], bVarsThm, univs_id);
01151 }
01152 if(0 == new_trigs.size()){
01153 std::vector<Trigger>& new_mult_trigs = d_multTrigs[e];
01154 for(size_t j=0; j<new_mult_trigs.size(); j++){
01155 registerTrig(trig_maps, new_mult_trigs[j], bVarsThm, univs_id);
01156 }
01157 }
01158 return;
01159 }
01160
01161 d_hasTriggers[e]=true;
01162
01163 const std::vector<Expr>& subterms = getSubTrig(e);
01164
01165 #ifdef DEBUG
01166 if( CVC3::debugger.trace("triggers") ){
01167 cout<<"===========all sub terms =========="<<endl;
01168 for (size_t i=0; i<subterms.size(); i++){
01169 const Expr& sub = subterms[i];
01170 cout<<"i="<< i << " : " << findExpr(sub) << " | " << sub << " and type is " << sub.getType()
01171 << " and kind is " << sub.getEM()->getKindName(sub.getKind()) << endl;
01172 }
01173 }
01174 #endif
01175
01176 ExprMap<Polarity> exprPol;
01177 findPolarity(e, exprPol, Pos);
01178
01179 {
01180 std::vector<Expr> trig_cadt;
01181 for(std::vector<Expr>::const_iterator i = subterms.begin(),iend=subterms.end(); i!=iend; i++){
01182 if(isGoodFullTrigger(*i, bVarsThm)) {
01183 trig_cadt.push_back(*i);
01184 }
01185 }
01186
01187 std::vector<Expr> trig_list;
01188 std::vector<Expr> trig_extra;
01189
01190 for(size_t iter =0; iter < trig_cadt.size(); iter++) {
01191 Expr* i = &(trig_cadt[iter]);
01192 bool notfound = true;
01193
01194 for(size_t index=0; index< trig_list.size(); index++){
01195 if (i->subExprOf(trig_list[index])) {
01196 trig_list[index]=*i;
01197 notfound=false;
01198 break;
01199 }
01200 if (trig_list[index].subExprOf(*i)) {
01201 notfound=false;
01202 break;
01203 }
01204 }
01205 if (notfound) {
01206 trig_list.push_back(*i);
01207 }
01208 }
01209
01210 std::vector<Trigger> trig_ex;
01211
01212 for (size_t i=0; i< trig_list.size();i++){
01213 const Expr& cur = trig_list[i];
01214 const std::set<Expr> cur_bvs = getBoundVars(cur);
01215 int score = trigInitScore(cur);
01216 if(score > 0) continue;
01217
01218
01219
01220
01221 for(size_t j=0; j< trig_cadt.size(); j++){
01222 if (trig_list[i] == trig_cadt[j]) continue;
01223 ExprMap<Expr> null;
01224 if (canMatch(trig_list[i], trig_cadt[j], null)){
01225 if(exprScore(trig_list[i]) < exprScore(trig_cadt[j])){
01226 }
01227 else if(*d_useTrans2 &&
01228 trig_list.size() == 2 &&
01229 trig_list[i].arity() == 2 &&
01230 BOUND_VAR == trig_list[i][0].getKind() &&
01231 BOUND_VAR == trig_list[i][1].getKind() &&
01232 BOUND_VAR == trig_cadt[j][0].getKind() &&
01233 BOUND_VAR == trig_cadt[j][1].getKind() &&
01234 isTrans2Like(subterms, trig_list[i])
01235 ){
01236
01237 score =0;
01238 d_trans2_num++;
01239
01240 DebugAssert(d_trans2_num<=1, "more than 2 trans2 found");
01241 TRACE("triggers", "trans2 found ", trig_list[i], "");
01242
01243 Trigger t(theoryCore(), cur, Neg, cur_bvs);
01244 t.setTrans2(true);
01245 t.setHead(getHeadExpr(cur));
01246 if(isSimpleTrig(cur)){
01247 t.setSimp();
01248 }
01249 if(isSuperSimpleTrig(cur)){
01250 t.setSuperSimp();
01251 }
01252 d_fullTrigs[e].push_back(t);
01253 registerTrig(trig_maps,t, bVarsThm, univs_id);
01254 return;
01255 }
01256 else{
01257 score =0;
01258 }
01259 }
01260 }
01261
01262 Polarity pol= Ukn;
01263
01264 if(cur.getType().isBool()){
01265 DebugAssert(exprPol.count(e)>0,"unknown polarity:"+cur.toString());
01266 pol = exprPol[cur];
01267 }
01268
01269 Trigger* t;
01270 Trigger* t_ex;
01271
01272 if(PosNeg == pol && *d_usePolarity){
01273 t = new Trigger(theoryCore(), cur, Pos, cur_bvs);
01274 t_ex = new Trigger(theoryCore(), cur, Neg, cur_bvs);
01275 if(isSimpleTrig(cur)){
01276 t->setSimp();
01277 t_ex->setSimp();
01278 }
01279 if(isSuperSimpleTrig(cur)){
01280 t->setSuperSimp();
01281 t_ex->setSuperSimp();
01282 }
01283
01284 }
01285 else{
01286 t = new Trigger(theoryCore(), cur, pol, cur_bvs);
01287 if(isSimpleTrig(cur)){
01288 t->setSimp();
01289 }
01290 if(isSuperSimpleTrig(cur)){
01291 t->setSuperSimp();
01292 }
01293 t_ex = NULL;
01294 }
01295
01296 if(canGetHead(cur)) {
01297 t->setHead(getHeadExpr(cur));
01298 if(NULL != t_ex){
01299 t_ex->setHead(getHeadExpr(cur));
01300 }
01301 }
01302 else{
01303 if(!isSysPred(cur)){
01304
01305 DebugAssert(false, "why this is a trigger");
01306 }
01307 }
01308
01309 t->setRWOp(false);
01310
01311 if(READ == cur.getKind() || WRITE == cur.getKind()){
01312 arrayIndexName(cur);
01313 }
01314
01315 if(READ == cur.getKind() && WRITE== cur[0].getKind() && 1 == bVarsThm.size() ){
01316
01317 t->setRWOp(true);
01318 if(t_ex != NULL) t_ex->setRWOp(true);
01319 }
01320
01321 if(t_ex != NULL) {
01322 trig_ex.push_back(*t_ex);
01323 }
01324
01325 d_fullTrigs[e].push_back(*t);
01326 registerTrig(trig_maps,*t, bVarsThm, univs_id);
01327
01328 TRACE("triggers", "new:full triggers:", cur.toString(),"");
01329 TRACE("triggers", "new:full trigger score:", score,"");
01330 TRACE("triggers", "new:full trigger pol:", pol,"");
01331 }
01332
01333 for(size_t i=0; i<trig_ex.size(); i++){
01334 d_fullTrigs[e].push_back(trig_ex[i]);
01335 registerTrig(trig_maps,trig_ex[i], bVarsThm, univs_id);
01336 TRACE("triggers", "new extra :full triggers:", trig_ex[i].getEx().toString(),"");
01337 }
01338
01339 if(d_fullTrigs[e].size() == 0){
01340 TRACE("triggers warning", "no full trig: ", e , "");
01341 }
01342 }
01343
01344 if(0 == d_fullTrigs[e].size() )
01345 {
01346 for( std::vector<Expr>::const_iterator i = subterms.begin(), iend=subterms.end(); i!=iend; i++) {
01347 if(isGoodMultiTrigger(*i, bVarsThm, d_offset_multi_trig)) {
01348 bool notfound = true;
01349 for(size_t index=0; index<d_multTriggers[e].size(); index++){
01350 if (i->subExprOf(d_multTriggers[e][index])) {
01351 (d_multTriggers[e][index])=*i;
01352 notfound=false;
01353 }
01354 }
01355 if (notfound){
01356 d_multTriggers[e].push_back(*i);
01357 }
01358 }
01359 }
01360
01361 std::vector<Expr>& cur_trig = d_multTriggers[e];
01362
01363 if (goodMultiTriggers(cur_trig, bVarsThm)){
01364
01365 TRACE("multi-triggers", "good set of multi triggers","","");
01366 for (size_t i=0; i< d_multTriggers[e].size();i++){
01367
01368 TRACE("multi-triggers", "multi-triggers:", d_multTriggers[e][i].toString(),"");
01369 }
01370 }
01371 else{
01372 cur_trig.clear();
01373
01374 TRACE("multi-triggers", "bad set of multi triggers","","");
01375 }
01376
01377
01378 {
01379 if(isTransLike(cur_trig)){
01380 d_trans_num++;
01381 DebugAssert(d_trans_num <= 1, "more than one trans found");
01382
01383 Expr ex = cur_trig[0];
01384
01385 Trigger* trans_trig = new Trigger(theoryCore(), ex, Neg, getBoundVars(ex));
01386 trans_trig->setHead(getHeadExpr(ex));
01387 if(isSimpleTrig(ex)){
01388 trans_trig->setSimp();
01389 }
01390 if(isSuperSimpleTrig(ex)){
01391 trans_trig->setSuperSimp();
01392 }
01393
01394 trans_trig->setTrans(true);
01395
01396 d_fullTrigs[e].push_back(*trans_trig);
01397 registerTrig(trig_maps,*trans_trig, bVarsThm, univs_id);
01398 cur_trig.clear();
01399 }
01400 }
01401
01402
01403 if(cur_trig.size() >0 ){
01404
01405 std::vector<Expr> posList, negList;
01406 for(size_t k=0; k<cur_trig.size(); k++){
01407 const Expr& cur_item = cur_trig[k];
01408 if (cur_item.getType().isBool()){
01409 Polarity pol = exprPol[cur_item];
01410 if(PosNeg == pol || Pos == pol){
01411 posList.push_back(cur_item);
01412 }
01413 if(PosNeg == pol || Neg == pol){
01414 negList.push_back(cur_item);
01415 }
01416 }
01417 }
01418 if (goodMultiTriggers(posList, bVarsThm)){
01419 TRACE("multi-triggers", "good set of multi triggers pos","","");
01420 for (size_t i=0; i< posList.size();i++){
01421 TRACE("multi-triggers", "multi-triggers:", posList[i].toString(),"");
01422 }
01423 cur_trig.clear();
01424 for(size_t m=0; m<posList.size(); m++){
01425 cur_trig.push_back(posList[m]);
01426 }
01427 }
01428 if (goodMultiTriggers(negList, bVarsThm) && negList.size() < cur_trig.size()){
01429 TRACE("multi-triggers", "good set of multi triggers neg","","");
01430 for (size_t i=0; i< negList.size();i++){
01431 TRACE("multi-triggers", "multi-triggers:", negList[i].toString(),"");
01432 }
01433 cur_trig.clear();
01434 for(size_t m=0; m<negList.size(); m++){
01435 cur_trig.push_back(negList[m]);
01436 }
01437 }
01438
01439 }
01440
01441 {
01442
01443
01444 if( 3 == cur_trig.size() || 4 == cur_trig.size() || 5 == cur_trig.size() || 6 == cur_trig.size() ){
01445 for(size_t i = 0; i < cur_trig.size(); i++){
01446 for(size_t j = 0; j < i; j++){
01447 vector<Expr> tempList;
01448 tempList.clear();
01449 tempList.push_back(cur_trig[i]);
01450 tempList.push_back(cur_trig[j]);
01451
01452
01453 if (goodMultiTriggers(tempList, bVarsThm)){
01454 cur_trig.clear();
01455 cur_trig.push_back(tempList[0]);
01456 cur_trig.push_back(tempList[1]);
01457 break;
01458 }
01459 }
01460 }
01461 }
01462
01463 if(cur_trig.size() != 2){
01464 if( 0 == cur_trig.size()){
01465 return;
01466 }
01467
01468
01469
01470
01471
01472
01473
01474
01475
01476 return;
01477 }
01478
01479 for(size_t i = 0 ; i<cur_trig.size(); i++){
01480 set<Expr> bvs = getBoundVars(cur_trig[i]);
01481 Trigger trig(theoryCore(), cur_trig[i], Ukn, bvs);
01482 trig.setHead(getHead(cur_trig[i]));
01483 trig.setMultiTrig();
01484 trig.multiIndex = i;
01485 trig.multiId=d_all_multTrigsInfo.size();
01486 d_multTrigs[e].push_back(trig);
01487 registerTrig(trig_maps, trig, bVarsThm, univs_id);
01488 }
01489
01490 {
01491 multTrigsInfo multTrigs;
01492 for(size_t i =0, iend = d_multTrigs[e].size(); i<iend; i++){
01493 const std::vector<Expr>& one_set_bvs = d_multTrigs[e][i].bvs;
01494 std::vector<size_t> one_set_pos;
01495
01496 for(size_t v = 0, vend = one_set_bvs.size(); v<vend; v++){
01497 size_t loc = locVar(bVarsThm, one_set_bvs[v]);
01498 if( 999 != loc ){
01499 one_set_pos.push_back(loc);
01500 }
01501 }
01502
01503 sort(one_set_pos.begin(), one_set_pos.end());
01504
01505 for(size_t v = 0, vend = one_set_pos.size(); v<vend; v++){
01506 }
01507
01508 multTrigs.var_pos.push_back(one_set_pos);
01509 }
01510
01511
01512 vector<size_t> common;
01513 std::vector<size_t>& tar1 = multTrigs.var_pos[0];
01514 std::vector<size_t>& tar2 = multTrigs.var_pos[1];
01515 vector<size_t>::iterator t1(tar1.begin()), t2(tar2.begin());
01516 while(t1 != tar1.end() && t2!= tar2.end()){
01517 size_t pos1 = *t1;
01518 size_t pos2 = *t2;
01519 if( pos1 == pos2 ) {
01520 common.push_back(pos1);
01521 t1=tar1.erase(t1);
01522 t2=tar2.erase(t2);
01523 }
01524 else if( pos1 > pos2 ){
01525 t2++;
01526 }
01527 else {
01528 t1++;
01529 }
01530 }
01531 multTrigs.common_pos.push_back(common);
01532
01533 size_t multi_size = d_multTrigs[e].size();
01534 for(size_t i =0; i< multi_size; i++){
01535 multTrigs.var_binds_found.push_back(new (true) CDMap<Expr, bool> (theoryCore()->getCM()->getCurrentContext()));
01536 }
01537 multTrigs.uncomm_list.push_back(new ExprMap<CDList<Expr>* >);
01538 multTrigs.uncomm_list.push_back(new ExprMap<CDList<Expr>* >);
01539 d_multitrigs_maps[e]=multTrigs;
01540 d_all_multTrigsInfo.push_back(multTrigs);
01541 }
01542 }
01543 }
01544
01545
01546 if(*d_usePart)
01547 {
01548 std::vector<Trigger> trig_ex;
01549
01550 trig_ex.clear();
01551 for( std::vector<Expr>::const_iterator i = subterms.begin(), iend=subterms.end(); i!=iend; i++) {
01552 if(isGoodPartTrigger(*i, bVarsThm)) {
01553 bool notfound = true;
01554 for(size_t index=0; index<d_partTriggers[e].size(); index++){
01555 if (i->subExprOf(d_partTriggers[e][index])) {
01556 (d_partTriggers[e][index])=*i;
01557 notfound=false;
01558 }
01559 }
01560 if (notfound)
01561 d_partTriggers[e].push_back(*i);
01562 }
01563 }
01564
01565 for (size_t i=0; i< d_partTriggers[e].size();i++){
01566 TRACE("triggers", "partial triggers:", d_partTriggers[e][i].toString(),"");
01567 }
01568
01569 for (size_t i=0; i< d_partTriggers[e].size();i++){
01570 Polarity pol= Ukn;
01571 const Expr& cur = d_partTriggers[e][i];
01572 const std::set<Expr> cur_bvs = getBoundVars(cur);
01573 if(cur.getType().isBool()){
01574 DebugAssert(exprPol.count(e)>0,"unknown polarity:"+cur.toString());
01575 pol = exprPol[cur];
01576 }
01577
01578 Trigger* t;
01579 Trigger* t_ex;
01580
01581 if(PosNeg == pol && *d_usePolarity){
01582 t = new Trigger(theoryCore(), cur, Pos, cur_bvs);
01583 t_ex = new Trigger(theoryCore(), cur, Neg, cur_bvs);
01584 }
01585 else{
01586 t = new Trigger(theoryCore(), cur, pol, cur_bvs);
01587 t_ex = NULL;
01588 }
01589
01590 if(canGetHead(cur)) {
01591 t->setHead(getHeadExpr(cur));
01592 }
01593
01594 if(t_ex != NULL) trig_ex.push_back(*t_ex);
01595
01596 d_partTrigs[e].push_back(*t);
01597
01598 TRACE("triggers", "new:part trigger pol:", pol,cur.toString());
01599 }
01600
01601 for(size_t i=0; i<trig_ex.size(); i++){
01602 d_partTrigs[e].push_back(trig_ex[i]);
01603 TRACE("triggers", "new extra :part triggers:", trig_ex[i].getEx().toString(),"");
01604 }
01605 }
01606 }
01607
01608
01609
01610
01611 int hasMoreBVs(const Expr& thm){
01612 DebugAssert(thm.isForall(), "hasMoreBVS called by non-forall exprs");
01613
01614 const std::vector<Expr>& bvsOutmost = thm.getVars();
01615 const std::set<Expr>& bvs = getBoundVars(thm);
01616
01617 return int(bvs.size()-bvsOutmost.size());
01618
01619 }
01620
01621
01622
01623
01624
01625
01626
01627 void TheoryQuant::assertFact(const Theorem& thm){
01628
01629 if(*d_translate) return;
01630 TRACE("quant assertfact", "assertFact => ", thm.toString(), "{");
01631 Theorem rule, result;
01632 const Expr& expr = thm.getExpr();
01633
01634
01635 if(expr.isExists()) {
01636 TRACE("quant assertfact", "assertFact => (ignoring existential) }", expr.toString(), "");
01637 return;
01638 }
01639
01640 DebugAssert(expr.isForall() || (expr.isNot() && (expr[0].isExists() || expr[0].isForall())),
01641 "Theory of quantifiers cannot handle expression "
01642 + expr.toString());
01643
01644 if(expr.isNot()) {
01645 if(expr[0].isForall()) {
01646 rule = d_rules->rewriteNotForall(expr);
01647 }
01648 else if(expr[0].isExists()) {
01649 rule = d_rules->rewriteNotExists(expr);
01650 }
01651 result = iffMP(thm, rule);
01652 }
01653 else{
01654 result = thm;
01655 }
01656
01657 result = d_rules->boundVarElim(result);
01658
01659 if(result.getExpr().isForall()){
01660
01661 if(*d_useNew){
01662
01663 if(result.getExpr().getBody().isForall()){
01664 result=d_rules->packVar(result);
01665 }
01666 result = d_rules->boundVarElim(result);
01667
01668 int nBVs = hasMoreBVs(result.getExpr());
01669 if( nBVs >= 1){
01670 d_hasMoreBVs[result.getExpr()]=true;
01671 }
01672 d_rawUnivs.push_back(result);
01673 return;
01674
01675
01676
01677 if(0 == nBVs){
01678 TRACE("quant assertfact", "assertFact => forall enqueueing: ", result.toString(), "}");
01679 d_univs.push_back(result);
01680 setupTriggers(result, d_univs.size()-1);
01681 }
01682 else if(1== nBVs){
01683 d_hasMoreBVs[result.getExpr()]=true;
01684 const Expr& body = result.getExpr().getBody();
01685
01686 if(*d_usePullVar){
01687 if((body.isAnd() && body[1].isForall()) || (body.isImpl() && body[1].isForall()) ){
01688 result=d_rules->pullVarOut(result);
01689
01690 TRACE("quant assertfact", "assertFact => pull-var enqueueing: ", result.toString(), "}");
01691
01692 d_univs.push_back(result);
01693 setupTriggers(result, d_univs.size()-1);
01694 }
01695 }
01696 else{
01697 TRACE("quant assertfact", "debug:not recognized case", result.toString(), thm.toString());
01698
01699 d_univs.push_back(result);
01700 setupTriggers(result, d_univs.size()-1);
01701 return;
01702 }
01703 }
01704 else{
01705 d_hasMoreBVs[result.getExpr()]=true;
01706 d_univs.push_back(result);
01707 setupTriggers(result, d_univs.size()-1);
01708 return;
01709 }
01710 }
01711 else{
01712
01713 TRACE("quant assertfact", "assertFact => old-fashoin enqueueing: ", result.toString(), "}");
01714
01715 d_univs.push_back(result);
01716 }
01717 }
01718 else {
01719
01720 TRACE("quant assertfact", "assertFact => non-forall enqueueing: ", result.toString(), "}");
01721 enqueueFact(result);
01722 }
01723 }
01724
01725 void TheoryQuant::recGoodSemMatch(const Expr& e,
01726 const std::vector<Expr>& bVars,
01727 std::vector<Expr>& newInst,
01728 std::set<std::vector<Expr> >& instSet)
01729 {
01730 size_t curPos = newInst.size();
01731 if (bVars.size() == curPos) {
01732 Expr simpleExpr = simplifyExpr(e.substExpr(bVars,newInst));
01733 if (simpleExpr.hasFind()){
01734 std::vector<Expr> temp = newInst;
01735 instSet.insert(temp);
01736 TRACE("quant yeting", "new inst found for ", e.toString()+" ==> ", simpleExpr.toString());
01737 };
01738 }
01739 else {
01740 Type t = getBaseType(bVars[curPos]);
01741 std::vector<Expr> tyExprs= d_typeExprMap[t];
01742 if (0 == tyExprs.size()) {
01743 return;
01744 }
01745 else{
01746 for (size_t i=0;i<tyExprs.size();i++){
01747 newInst.push_back(tyExprs[i]);
01748 recGoodSemMatch(e,bVars,newInst,instSet);
01749 newInst.pop_back();
01750 }
01751 }
01752 }
01753 }
01754
01755 bool isIntx(const Expr& e, const Rational& x){
01756 if(e.isRational() && e.getRational()==x)
01757 return true;
01758 else return false;
01759 }
01760
01761 Expr getLeft(const Expr& e){
01762 if(e.getKind()!= PLUS) return null_expr;
01763 if(e.arity() != 3) return null_expr;
01764 Expr const_expr, minus ,pos;
01765 int numMinus=0, numPos=0, numConst=0;;
01766 for(int i=0; i<e.arity(); i++){
01767 if((e[i]).getKind() == MULT){
01768 if(isIntx(e[i][0], -1)){
01769 numMinus++;
01770 minus=e[i][1];
01771 }
01772 else{
01773 numPos++;
01774 pos=e[i];
01775 }
01776 }
01777 else if(e[i].isRational()) {
01778 const_expr = e[i];
01779 numConst++;
01780 }
01781 else{
01782 numPos++;
01783 pos=e[i];
01784 }
01785 }
01786 if(1==numPos && 1==numConst && 1==numMinus){
01787 return minus;
01788 }
01789 else{
01790 return null_expr;
01791 }
01792 }
01793
01794 Expr getRight(const Expr& e){
01795 if(e.getKind()!= PLUS) return null_expr;
01796 if(e.arity() != 3) return null_expr;
01797 Expr const_expr, minus ,pos;
01798 int numMinus=0, numPos=0, numConst=0;;
01799
01800 for(int i=0; i<e.arity(); i++){
01801 if((e[i]).getKind() == MULT){
01802 if(isIntx(e[i][0], -1)){
01803 numMinus++;
01804 minus=e[i][1];
01805 }
01806 else{
01807 numPos++;
01808 pos=e[i];
01809 }
01810 }
01811 else if(e[i].isRational()) {
01812 const_expr = e[i];
01813 numConst++;
01814 }
01815 else{
01816 numPos++;
01817 pos=e[i];
01818 }
01819 }
01820
01821 if(1==numPos && 1==numConst && 1==numMinus){
01822 if(isIntx(const_expr,0)){
01823 return pos;
01824 }
01825 else{
01826
01827 return Expr(PLUS, const_expr, pos);
01828 }
01829 }
01830 else{
01831 return null_expr;
01832 }
01833 }
01834
01835 inline void TheoryQuant::add_parent(const Expr& parent){
01836 ExprMap<CDList<Expr>* >::iterator iter;
01837 for(int i=0; i< parent.arity(); i++){
01838 const Expr& child = parent[i];
01839 iter = d_parent_list.find(child);
01840 if(d_parent_list.end() == iter){
01841 d_parent_list[child] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
01842 d_parent_list[child]->push_back(parent);
01843 }
01844 else{
01845 iter->second->push_back(parent);
01846 }
01847 }
01848 }
01849
01850 void TheoryQuant::collectChangedTerms(CDList<Expr>& changed){
01851 ExprMap<bool> eqs_hash;
01852 ExprMap<bool> changed_hash;
01853
01854
01855
01856
01857
01858
01859
01860
01861
01862
01863
01864
01865
01866
01867
01868
01869
01870
01871
01872
01873
01874 for(size_t i=d_eqs_pos; i<d_eqs.size(); i++){
01875 eqs_hash[d_eqs[i]]=true;
01876 }
01877 d_eqs_pos.set(d_eqs.size());
01878 {
01879 for(ExprMap<bool>::iterator iter = eqs_hash.begin(), iter_end = eqs_hash.end(); iter != iter_end; iter++){
01880 const Expr& cur_ex = iter->first;
01881 ExprMap<CDList<Expr>* >::iterator iter_parent = d_parent_list.find(cur_ex);
01882 if(d_parent_list.end() != iter_parent){
01883 CDList<Expr>* cur_parents = iter_parent->second;
01884 for(size_t i=0; i<cur_parents->size(); i++){
01885 changed_hash[(*cur_parents)[i]]=true;
01886 }
01887 }
01888 }
01889 }
01890 {
01891 for(ExprMap<bool>::iterator iter = changed_hash.begin(), iter_end = changed_hash.end(); iter != iter_end; iter++){
01892 changed.push_back(iter->first);
01893 }
01894 }
01895 }
01896
01897 inline bool TheoryQuant::matchChild(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env){
01898 if(gterm.arity() != vterm.arity()) {
01899 return false;
01900 }
01901 for(int i = 0 ; i< gterm.arity(); i++){
01902 const Expr& cur_v = vterm[i];
01903 const Expr& cur_g = gterm[i];
01904 if(BOUND_VAR == cur_v.getKind()){
01905 ExprMap<Expr>::iterator p = env.find(cur_v);
01906 if ( p != env.end()){
01907 if (simplifyExpr(cur_g) != simplifyExpr(p->second)){
01908 return false;
01909 }
01910 }
01911 else {
01912 env[cur_v] = simplifyExpr(cur_g);
01913 }
01914 }
01915 else if (!cur_v.containsBoundVar()){
01916 if(simplifyExpr(cur_v) != simplifyExpr(cur_g)){
01917 return false;
01918 }
01919 }
01920 else{
01921 if (false == recSynMatch(cur_g, cur_v, env)){
01922 return false;
01923 }
01924 }
01925 }
01926 return true;
01927 }
01928
01929 inline void TheoryQuant::matchChild(const Expr& gterm, const Expr& vterm, vector<ExprMap<Expr> >& binds){
01930 ExprMap<Expr> env;
01931 if(gterm.arity() != vterm.arity()) {
01932 return;
01933 }
01934
01935 for(int i = 0 ; i< gterm.arity(); i++){
01936 const Expr& cur_v = vterm[i];
01937 const Expr& cur_g = gterm[i];
01938 if(BOUND_VAR == cur_v.getKind()){
01939 ExprMap<Expr>::iterator p = env.find(cur_v);
01940 if ( p != env.end()){
01941 if (simplifyExpr(cur_g) != simplifyExpr(p->second)){
01942 return;
01943 }
01944 }
01945 else {
01946 env[cur_v] = simplifyExpr(cur_g);
01947 }
01948 }
01949 else if (!cur_v.containsBoundVar()){
01950 if(simplifyExpr(cur_v) != simplifyExpr(cur_g)){
01951 return ;
01952 }
01953 }
01954 else{
01955 if (false == recSynMatch(cur_g, cur_v, env)){
01956 return;
01957 }
01958 }
01959 }
01960 binds.push_back(env);
01961 return;
01962 }
01963
01964
01965
01966
01967 void TheoryQuant::matchListOld(const CDList<Expr>& glist, size_t gbegin, size_t gend){
01968 for(size_t g_index = gbegin; g_index < gend; g_index++){
01969
01970 const Expr& gterm = glist[g_index];
01971 if(gterm.isEq()){
01972 continue;
01973 }
01974
01975 Expr head = getHead(gterm);
01976
01977 ExprMap<CDMap<Expr, CDList<dynTrig>* > *>::iterator iter = d_allmap_trigs.find(head);
01978 if(d_allmap_trigs.end() == iter) continue;
01979 CDMap<Expr, CDList<dynTrig>*>* cd_map = iter->second;
01980
01981
01982
01983
01984
01985 CDMap<Expr, CDList<dynTrig>*>::iterator iter_trig = (*cd_map).begin();
01986 CDMap<Expr, CDList<dynTrig>*>::iterator iter_trig_end = (*cd_map).end();
01987
01988 for(;iter_trig != iter_trig_end; iter_trig++){
01989 CDList<dynTrig>* cur_list = (*iter_trig).second;
01990 if(1 == cur_list->size() || null_expr == head || gterm.getType().isBool()){
01991 for(size_t cur_index =0; cur_index < cur_list->size(); cur_index++){
01992
01993 const Trigger& cur_trig = (*cur_list)[cur_index].trig;
01994 size_t univ_id = (*cur_list)[cur_index].univ_id;
01995 vector<ExprMap<Expr> > binds;
01996 const Expr& vterm = cur_trig.trig;
01997 if ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans && !cur_trig.isMulti) continue;
01998
01999 newTopMatch(gterm, vterm, binds, cur_trig);
02000
02001 for(size_t i=0; i<binds.size(); i++){
02002 ExprMap<Expr>& cur_map = binds[i];
02003 vector<Expr> bind_vec;
02004 const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
02005 for(size_t j=0; j< bVarsThm.size(); j++){
02006 bind_vec.push_back(cur_map[bVarsThm[j]]);
02007 }
02008 synNewInst(univ_id, bind_vec, gterm, cur_trig);
02009 }
02010 }
02011 }
02012 else if ( cur_list->size() > 1){
02013
02014 const Trigger& cur_trig = (*cur_list)[0].trig;
02015 const Expr& general_vterm = (*iter_trig).first;
02016 vector<ExprMap<Expr> > binds;
02017 if ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans && !cur_trig.isMulti) continue;
02018
02019 newTopMatch(gterm, general_vterm, binds, cur_trig);
02020
02021 for(size_t trig_index = 0; trig_index< cur_list->size(); trig_index++){
02022 size_t univ_id = (*cur_list)[trig_index].univ_id;
02023 const ExprMap<Expr>& trig_map = (*cur_list)[trig_index].binds;
02024 const Trigger& ind_cur_trig = (*cur_list)[trig_index].trig;
02025 for(size_t i=0; i<binds.size(); i++){
02026 ExprMap<Expr>& cur_map = binds[i];
02027 vector<Expr> bind_vec;
02028 const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
02029 for(size_t j=0; j< bVarsThm.size(); j++){
02030 const Expr& inter=(*(trig_map.find(bVarsThm[j]))).second;
02031 const Expr& inter2 = cur_map[inter];
02032 bind_vec.push_back(inter2);
02033 }
02034 synNewInst(univ_id, bind_vec, gterm, ind_cur_trig);
02035 }
02036 }
02037 }
02038 else{
02039 FatalAssert(false, "error in matchlistold");
02040 }
02041 }
02042 }
02043 }
02044
02045 void TheoryQuant::delNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs){
02046
02047 ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator i = new_trigs.begin();
02048 ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator iend = new_trigs.end();
02049 for(; i!=iend; i++){
02050 ExprMap<std::vector<dynTrig>*>* cur_new_cd_map = i->second;
02051 ExprMap<vector<dynTrig>* >::iterator j = cur_new_cd_map->begin();
02052 ExprMap<vector<dynTrig>* >::iterator jend = cur_new_cd_map->end();
02053 for(; j!=jend; j++){
02054 Expr general_trig = j->first;
02055 vector<dynTrig>* trigs = j->second;
02056 delete trigs;
02057 }
02058 delete cur_new_cd_map;
02059 }
02060 new_trigs.clear();
02061 }
02062
02063
02064 void TheoryQuant::combineOldNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs){
02065 ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator i = new_trigs.begin();
02066 ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator iend = new_trigs.end();
02067 for(; i!=iend; i++){
02068 ExprMap<std::vector<dynTrig>*>* cur_new_cd_map = i->second;
02069 Expr head = i->first;
02070 ExprMap<CDMap<Expr, CDList<dynTrig>* >* >::iterator old_iter = d_allmap_trigs.find(head);
02071 if(d_allmap_trigs.end() == old_iter){
02072 CDMap<Expr, CDList<dynTrig>* >* old_cd_map =
02073
02074 new(false) CDMap<Expr, CDList<dynTrig>* > (theoryCore()->getCM()->getCurrentContext());
02075 d_allmap_trigs[head] = old_cd_map;
02076 ExprMap<vector<dynTrig>* >::iterator j = cur_new_cd_map->begin();
02077 ExprMap<vector<dynTrig>* >::iterator jend = cur_new_cd_map->end();
02078 for(; j!=jend; j++){
02079 Expr general_trig = j->first;
02080 vector<dynTrig>* trigs = j->second;
02081 CDList<dynTrig>* old_cd_list =
02082
02083 new(false) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
02084 (*old_cd_map)[general_trig] = old_cd_list;
02085 for(size_t k=0; k<trigs->size(); k++){
02086 (*old_cd_list).push_back((*trigs)[k]);
02087
02088 }
02089
02090 }
02091
02092 }
02093 else{
02094 CDMap<Expr, CDList<dynTrig>* >* old_cd_map = old_iter->second;
02095 ExprMap<std::vector<dynTrig>*>::iterator j = cur_new_cd_map->begin();
02096 ExprMap<std::vector<dynTrig>*>::iterator jend = cur_new_cd_map->end();
02097 for(; j!=jend; j++){
02098 Expr general_trig = j->first;
02099 vector<dynTrig>* trigs = j->second;
02100 CDMap<Expr, CDList<dynTrig>* >::iterator old_trigs_iter = old_cd_map->find(general_trig);
02101 CDList<dynTrig>* old_cd_list;
02102 if(old_cd_map->end() == old_trigs_iter){
02103 old_cd_list =
02104
02105 new(false) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
02106 (*old_cd_map)[general_trig] = old_cd_list;
02107 }
02108 else{
02109 old_cd_list = (*old_trigs_iter).second;
02110 }
02111 for(size_t k=0; k<trigs->size(); k++){
02112 (*old_cd_list).push_back((*trigs)[k]);
02113
02114 }
02115
02116 }
02117
02118 }
02119 }
02120 delNewTrigs(new_trigs);
02121
02122 }
02123
02124
02125 void TheoryQuant::matchListNew(ExprMap<ExprMap<vector<dynTrig>*>*>& new_trigs,
02126 const CDList<Expr>& glist,
02127 size_t gbegin,
02128 size_t gend){
02129 for(size_t g_index = gbegin; g_index<gend; g_index++){
02130
02131 const Expr& gterm = glist[g_index];
02132
02133 if(gterm.isEq()){
02134 continue;
02135 }
02136
02137 Expr head = getHead(gterm);
02138
02139 ExprMap<ExprMap<vector<dynTrig>* > *>::iterator iter = new_trigs.find(head);
02140 if(new_trigs.end() == iter) continue;
02141 ExprMap<vector<dynTrig>*>* cd_map = iter->second;
02142
02143
02144
02145
02146
02147 ExprMap<vector<dynTrig>*>::iterator iter_trig = (*cd_map).begin();
02148 ExprMap<vector<dynTrig>*>::iterator iter_trig_end = (*cd_map).end();
02149
02150 for(;iter_trig != iter_trig_end; iter_trig++){
02151
02152 vector<dynTrig>* cur_list = (*iter_trig).second;
02153 if(1 == cur_list->size() || null_expr == head || gterm.getType().isBool()){
02154 for(size_t cur_index =0; cur_index < cur_list->size(); cur_index++){
02155 const Trigger& cur_trig = (*cur_list)[cur_index].trig;
02156
02157
02158
02159 size_t univ_id = (*cur_list)[cur_index].univ_id;
02160 vector<ExprMap<Expr> > binds;
02161 const Expr& vterm = cur_trig.trig;
02162
02163 newTopMatch(gterm, vterm, binds, cur_trig);
02164 for(size_t i=0; i<binds.size(); i++){
02165 ExprMap<Expr>& cur_map = binds[i];
02166 vector<Expr> bind_vec;
02167 const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
02168 for(size_t j=0; j< bVarsThm.size(); j++){
02169 bind_vec.push_back(cur_map[bVarsThm[j]]);
02170 }
02171 synNewInst(univ_id, bind_vec, gterm, cur_trig);
02172 }
02173 }
02174 }
02175 else if ( cur_list->size() > 1){
02176
02177 const Trigger& cur_trig = (*cur_list)[0].trig;
02178
02179
02180 const Expr& general_vterm = (*iter_trig).first;
02181 vector<ExprMap<Expr> > binds;
02182 newTopMatch(gterm, general_vterm, binds, cur_trig);
02183
02184 for(size_t trig_index = 0; trig_index< cur_list->size(); trig_index++){
02185 size_t univ_id = (*cur_list)[trig_index].univ_id;
02186 const Trigger& ind_cur_trig = (*cur_list)[trig_index].trig;
02187 const ExprMap<Expr>& trig_map = (*cur_list)[trig_index].binds;
02188
02189 for(size_t i=0; i<binds.size(); i++){
02190 ExprMap<Expr>& cur_map = binds[i];
02191 vector<Expr> bind_vec;
02192 const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
02193 for(size_t j=0; j< bVarsThm.size(); j++){
02194 const Expr& inter=(*(trig_map.find(bVarsThm[j]))).second;
02195 const Expr& inter2 = cur_map[inter];
02196 bind_vec.push_back(inter2);
02197 }
02198 synNewInst(univ_id, bind_vec, gterm, ind_cur_trig);
02199 }
02200 }
02201 }
02202 else{
02203 FatalAssert(false, "error in matchlistold");
02204 }
02205 }
02206 }
02207 }
02208
02209
02210 void TheoryQuant::newTopMatch(const Expr& gterm,
02211 const Expr& vterm,
02212 vector<ExprMap<Expr> >& binds,
02213 const Trigger& trig){
02214 ExprMap<Expr> cur_bind;
02215 if(trig.isSuperSimple){
02216 for(int i = vterm.arity()-1; i>=0 ; i--){
02217 cur_bind[vterm[i]] = simplifyExpr(gterm[i]);
02218 }
02219 binds.push_back(cur_bind);
02220 return;
02221 }
02222
02223 if(trig.isSimple){
02224 for(int i = vterm.arity()-1; i>=0 ; i--){
02225 if(BOUND_VAR != vterm[i].getKind()){
02226 if(simplifyExpr(gterm[i]) != simplifyExpr(vterm[i])) {
02227 return ;
02228 }
02229 }
02230 else{
02231 cur_bind[vterm[i]] = simplifyExpr(gterm[i]);
02232 }
02233 }
02234 binds.push_back(cur_bind);
02235 return;
02236 }
02237
02238
02239 if(!isSysPred(vterm)){
02240 if(!gterm.getType().isBool()){
02241
02242 matchChild(gterm, vterm, binds);
02243 return;
02244 }
02245
02246 matchChild(gterm, vterm, binds);
02247 return;
02248
02249
02250 if(!*d_usePolarity){
02251
02252 matchChild(gterm, vterm, binds);
02253 return;
02254 }
02255
02256 const bool gtrue = (trueExpr()==findExpr(gterm));
02257
02258 if(gtrue ){
02259 if((Neg==trig.polarity || PosNeg==trig.polarity)) {
02260
02261 matchChild(gterm, vterm, binds);
02262 return;
02263 }
02264 else{
02265
02266 return;
02267 }
02268 }
02269 const bool gfalse = (falseExpr()==findExpr(gterm));
02270
02271 if(gfalse){
02272 if((Pos==trig.polarity || PosNeg==trig.polarity)) {
02273
02274 matchChild(gterm, vterm, binds);
02275 return;
02276 }
02277 else{
02278
02279 return;
02280 }
02281 }
02282
02283
02284
02285
02286
02287
02288
02289
02290
02291 matchChild(gterm, vterm, binds);
02292 return;
02293
02294 return;
02295 }
02296 else{
02297
02298 Expr gl = getLeft(gterm[1]);
02299 Expr gr = getRight(gterm[1]);
02300
02301 if(null_expr == gr || null_expr == gl){
02302 gl = gterm[0];
02303 gr = gterm[1];
02304 }
02305
02306 Expr vr, vl;
02307 Expr tvr, tvl;
02308
02309 tvr=null_expr;
02310 tvl=null_expr;
02311
02312 if(isGE(vterm) || isGT(vterm)){
02313 vr = vterm[0];
02314 vl = vterm[1];
02315 }
02316 else if(isLE(vterm) || isLT(vterm)){
02317 vr = vterm[1];
02318 vl = vterm[0];
02319 }
02320 else{
02321 FatalAssert(false, "impossilbe in toppred");
02322 }
02323
02324 if(isIntx(vl,0)){
02325 tvl = getLeft(vr);
02326 tvr = getRight(vr);
02327 }
02328 else if(isIntx(vr,0)) {
02329 tvl = getLeft(vl);
02330 tvr = getRight(vl);
02331 }
02332
02333 if( (null_expr != tvl) && (null_expr != tvr)){
02334 vl = tvl;
02335 vr = tvr;
02336 }
02337
02338
02339 const bool gtrue = (trueExpr()==findExpr(gterm));
02340 const bool gfalse = (falseExpr()==findExpr(gterm));
02341
02342 TRACE("quant toppred"," vl, gl, vr, gr:", vl.toString()+"::"+gl.toString()+"||", vr.toString()+"::"+gr.toString());
02343
02344
02345
02346 if(!*d_usePolarity){
02347 if((recSynMatch(gl, vl, cur_bind) && recSynMatch(gr, vr, cur_bind))){
02348 binds.push_back(cur_bind);
02349 return;
02350 }
02351 else{
02352 return;
02353 }
02354 }
02355 if((Neg==trig.polarity || PosNeg==trig.polarity)) {
02356 if (( gtrue ) ) {
02357 if (recSynMatch(gl, vl, cur_bind) && recSynMatch(gr, vr, cur_bind)){
02358 binds.push_back(cur_bind);
02359 return;
02360 }
02361 else{
02362 return;
02363 }
02364 }
02365 else {
02366 if(recSynMatch(gl, vr, cur_bind) && recSynMatch(gr, vl, cur_bind)){
02367 binds.push_back(cur_bind);
02368 return;
02369 }
02370 else{
02371 return;
02372 }
02373 }
02374 }
02375 else if((Pos==trig.polarity || PosNeg==trig.polarity)) {
02376 if (( gfalse )) {
02377 if(recSynMatch(gl, vl, cur_bind) && recSynMatch(gr, vr, cur_bind)){
02378 binds.push_back(cur_bind);
02379 return;
02380 }
02381 else{
02382 return;
02383 }
02384 }
02385 else {
02386 if(recSynMatch(gl, vr, cur_bind) && recSynMatch(gr, vl, cur_bind)){
02387 binds.push_back(cur_bind);
02388 return;
02389 }
02390 else{
02391 return;
02392 }
02393 }
02394 }
02395 else {
02396 FatalAssert(false, "impossible polarity for trig");
02397
02398
02399 return;
02400 }
02401 }
02402 }
02403
02404
02405
02406
02407
02408
02409
02410
02411
02412
02413
02414
02415
02416
02417
02418
02419
02420
02421
02422
02423
02424
02425
02426
02427
02428
02429
02430
02431
02432
02433
02434
02435
02436
02437
02438
02439
02440
02441
02442
02443
02444
02445
02446
02447
02448
02449
02450
02451
02452
02453
02454
02455
02456
02457
02458
02459
02460
02461
02462
02463
02464
02465
02466
02467
02468
02469
02470
02471
02472
02473
02474
02475
02476
02477
02478
02479
02480
02481
02482
02483
02484
02485
02486
02487
02488
02489
02490
02491
02492
02493
02494
02495
02496
02497
02498
02499
02500
02501
02502
02503
02504
02505
02506
02507
02508
02509
02510
02511
02512
02513
02514
02515
02516
02517
02518
02519
02520
02521
02522
02523
02524
02525
02526
02527
02528
02529
02530
02531
02532
02533
02534
02535
02536
02537
02538
02539
02540
02541
02542
02543
02544
02545
02546
02547
02548
02549
02550
02551
02552
02553
02554
02555
02556
02557
02558
02559
02560
02561
02562
02563
02564
02565
02566
02567
02568
02569
02570
02571
02572
02573
02574
02575
02576
02577
02578
02579
02580
02581
02582
02583
02584
02585
02586
02587
02588
02589
02590
02591
02592
02593
02594
02595
02596
02597
02598
02599
02600
02601
02602
02603
02604 bool TheoryQuant::recSynMatch(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env){
02605 TRACE("quant match", "gterm:| "+gterm.toString()," vterm:| "+vterm.toString(),"");
02606 DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
02607
02608 if (BOUND_VAR == vterm.getKind() ) {
02609 TRACE("quant match", "bound var found;", vterm.toString(),"");
02610 ExprMap<Expr>::iterator p = env.find(vterm);
02611 if ( p != env.end()){
02612 if (simplifyExpr(gterm) != simplifyExpr(p->second)){
02613 return false;
02614 }
02615 else
02616 return true;
02617 }
02618 else {
02619 env[vterm] = simplifyExpr(gterm);
02620 return true;
02621 }
02622 }
02623 else if (!vterm.containsBoundVar()){
02624
02625
02626 if(simplifyExpr(vterm) == simplifyExpr(gterm)) {
02627 return true;
02628 }
02629 else{
02630 return false;
02631 }
02632 }
02633
02634 else if(false && isSysPred(vterm) && isSysPred(gterm)){
02635
02636 TRACE("quant syspred"," vterm, gterm ", vterm.toString()+" :|: ", gterm.toString());
02637 TRACE("quant syspred"," simplified vterm, gterm ", simplifyExpr(vterm).toString()+" :|: ", simplifyExpr(gterm).toString());
02638 FatalAssert(false, "should not be here in synmatch");
02639 exit(3);
02640 }
02641 else{
02642 if(canGetHead(vterm)){
02643 Expr vhead = getHead(vterm);
02644 TRACE("quant match", "head vterm:", getHead(vterm), "");
02645 if(vterm.isAtomicFormula()){
02646 if (canGetHead(gterm)) {
02647 if ( vhead != getHead(gterm) ){
02648 return false;
02649 }
02650 return matchChild(gterm, vterm, env);
02651
02652
02653
02654
02655
02656 }
02657 else{
02658 return false;
02659 }
02660 }
02661 if ( (canGetHead(gterm)) && vhead == getHead(gterm)){
02662
02663
02664
02665
02666
02667
02668
02669
02670
02671 return matchChild(gterm, vterm, env);
02672 }
02673
02674 if(!*d_useEqu){
02675 return false;
02676 }
02677
02678
02679
02680
02681
02682
02683
02684
02685
02686
02687
02688
02689
02690
02691
02692
02693
02694
02695
02696
02697
02698
02699
02700
02701
02702
02703
02704
02705
02706
02707
02708
02709
02710
02711
02712
02713
02714
02715
02716
02717
02718
02719
02720
02721
02722
02723
02724
02725
02726
02727
02728
02729
02730
02731
02732
02733
02734
02735
02736 if( d_same_head_expr.count(vhead) > 0 ) {
02737 const Expr& findGterm = simplifyExpr(gterm);
02738
02739 TRACE("quant match", "find gterm:", findGterm.toString(),"");
02740 CDList<Expr>* gls = d_same_head_expr[vhead];
02741
02742
02743
02744
02745
02746
02747
02748
02749
02750
02751
02752
02753
02754
02755
02756
02757
02758 for(size_t i = 0; i<gls->size(); i++){
02759 if (simplifyExpr((*gls)[i]) == findGterm){
02760 TRACE("quant match", "find matched gterm:", (*gls)[i].toString(),"");
02761 DebugAssert((*gls)[i].arity() == vterm.arity(), "gls has different arity");
02762
02763 const Expr& newgterm = (*gls)[i];
02764 for(int child=vterm.arity()-1; child >= 0 ; child--){
02765 if (false == recSynMatch(newgterm[child], vterm[child] , env)){
02766 TRACE("quant match", "match false", (*gls)[i][child].toString(), vterm[child].toString());
02767 return false;
02768 }
02769 }
02770 TRACE("quant match", "good match, return true:", gterm, vterm.toString());
02771
02772
02773 return true;
02774 }
02775 }
02776 return false;
02777 }
02778 else {
02779 return false;
02780 }
02781 }
02782 else{
02783 TRACE("quant match more", "match more", gterm.toString()+" # ", vterm.toString());
02784 if( (gterm.getKind() == vterm.getKind()) &&
02785 (gterm.arity() == vterm.arity()) &&
02786 gterm.arity()>0 ){
02787
02788
02789
02790
02791
02792
02793
02794
02795
02796
02797
02798 return matchChild(gterm, vterm, env);
02799 }
02800 else {
02801
02802
02803
02804
02805
02806
02807
02808
02809 return false;
02810 }
02811 }
02812 }
02813 }
02814
02815
02816
02817
02818
02819
02820
02821
02822
02823
02824
02825
02826
02827
02828
02829
02830
02831
02832
02833
02834
02835
02836
02837
02838
02839
02840
02841
02842
02843
02844
02845
02846
02847
02848
02849
02850
02851
02852
02853
02854
02855
02856
02857
02858
02859
02860
02861
02862
02863
02864
02865
02866
02867
02868
02869
02870
02871
02872
02873
02874
02875
02876
02877
02878
02879
02880
02881
02882
02883
02884
02885
02886
02887
02888
02889
02890
02891
02892
02893
02894
02895
02896
02897
02898
02899
02900
02901
02902
02903
02904
02905
02906
02907
02908
02909
02910
02911
02912
02913
02914
02915
02916
02917
02918
02919
02920
02921
02922
02923
02924
02925
02926
02927
02928
02929
02930
02931
02932
02933
02934
02935
02936
02937
02938
02939
02940
02941
02942
02943
02944
02945
02946
02947
02948
02949
02950
02951
02952
02953
02954
02955
02956
02957
02958
02959
02960
02961
02962
02963
02964
02965
02966
02967
02968
02969
02970
02971
02972
02973
02974
02975
02976
02977
02978
02979
02980
02981
02982
02983
02984
02985
02986
02987
02988
02989
02990
02991
02992
02993
02994
02995
02996
02997
02998
02999
03000
03001
03002
03003
03004
03005
03006
03007
03008
03009
03010
03011
03012
03013
03014
03015
03016
03017
03018
03019
03020
03021
03022
03023
03024
03025
03026
03027
03028
03029
03030
03031
03032
03033
03034
03035
03036
03037
03038
03039
03040
03041
03042
03043
03044
03045
03046
03047
03048
03049
03050
03051
03052
03053
03054
03055
03056
03057
03058
03059
03060
03061
03062
03063
03064
03065
03066
03067
03068
03069
03070
03071
03072
03073
03074
03075
03076
03077
03078
03079
03080
03081
03082
03083
03084
03085
03086
03087
03088
03089
03090
03091
03092
03093
03094
03095
03096
03097
03098
03099
03100
03101
03102
03103
03104
03105
03106
03107
03108
03109
03110
03111
03112
03113
03114
03115 void TheoryQuant::goodSynMatch(const Expr& e,
03116 const std::vector<Expr> & boundVars,
03117 std::vector<std::vector<Expr> >& instBinds,
03118 std::vector<Expr>& instGterms,
03119 const CDList<Expr>& allterms,
03120 size_t tBegin){
03121 for (size_t i=tBegin; i<allterms.size(); i++) {
03122 Expr gterm = allterms[i];
03123 if (0 == gterm.arity() )
03124 continue;
03125 TRACE("quant matching", gterm.toString(), "||", e.toString()) ;
03126
03127 if(usefulInMatch(gterm)) {
03128 ExprMap<Expr> env;
03129 env.clear();
03130 bool found = recSynMatch(gterm,e,env);
03131 if(found){
03132
03133 TRACE("quant matching found", " good:",gterm.toString()+" to " , e.toString());
03134 TRACE("quant matching found", " simplified good:",simplifyExpr(gterm).toString()+" to " , simplifyExpr(e).toString());
03135 std::vector<Expr> inst;
03136
03137 DebugAssert((boundVars.size() == env.size()),"bound var size != env.size()");
03138
03139 for(size_t i=0; i<boundVars.size(); i++) {
03140 ExprMap<Expr>::iterator p = env.find(boundVars[i]);
03141 DebugAssert((p!=env.end()),"bound var cannot be found");
03142 inst.push_back(p->second);
03143 }
03144 instBinds.push_back(inst);
03145 instGterms.push_back(gterm);
03146 }
03147 else{
03148 TRACE("quant matching", "bad one",gterm.toString()+" to " , e.toString());
03149 }
03150 }
03151 }
03152 }
03153
03154
03155
03156
03157
03158
03159
03160
03161
03162
03163
03164
03165
03166
03167
03168
03169
03170
03171
03172
03173
03174
03175
03176
03177
03178
03179
03180
03181
03182
03183
03184
03185
03186
03187
03188
03189
03190
03191
03192
03193
03194
03195
03196
03197
03198
03199
03200
03201
03202
03203
03204
03205
03206
03207
03208
03209
03210
03211
03212
03213
03214
03215
03216
03217
03218
03219
03220
03221
03222
03223
03224
03225
03226
03227
03228
03229
03230
03231
03232
03233
03234
03235
03236
03237 int TheoryQuant::loc_gterm(const std::vector<Expr>& border,
03238 const Expr& vterm,
03239 int pos){
03240 const std::vector<Expr>& order = d_mtrigs_bvorder[vterm];
03241 const Expr& var = order[pos];
03242 for(size_t i=0; i<border.size(); i++){
03243 if (border[i] == var) return i;
03244 }
03245
03246 DebugAssert(false, "internal error in loc_germ");
03247 return -1;
03248 }
03249
03250 void TheoryQuant::recSearchCover(const std::vector<Expr>& border,
03251 const std::vector<Expr>& mtrigs,
03252 int cur_depth,
03253 std::vector<std::vector<Expr> >& instSet,
03254 std::vector<Expr>& cur_inst
03255 ){
03256 int max_dep = mtrigs.size();
03257
03258 if(cur_depth >= max_dep) return;
03259
03260 Expr cur_vterm = mtrigs[cur_depth];
03261 if(d_mtrigs_inst.count(cur_vterm) <=0) return;
03262 CDList<std::vector<Expr> >* gterm_list = d_mtrigs_inst[cur_vterm];
03263 for(size_t i=0; i< gterm_list->size(); i++){
03264 const std::vector<Expr>& cur_gterm = (*gterm_list)[i];
03265 std::vector<Expr> new_inst(border.size());
03266
03267 for(size_t j=0; j< border.size(); j++){
03268 new_inst[j]=cur_inst[j];
03269 }
03270
03271 bool has_problem = false;
03272 for(size_t j=0; j< cur_gterm.size(); j++){
03273 int cur_loc_gterm = loc_gterm(border, cur_vterm, j);
03274
03275 if( null_expr == new_inst[cur_loc_gterm]){
03276 new_inst[cur_loc_gterm] = cur_gterm[j];
03277 }
03278 else if (new_inst[cur_loc_gterm] != cur_gterm[j]){
03279 has_problem = true;
03280 break;
03281 }
03282
03283 }
03284
03285 if (has_problem){
03286 continue;
03287 }
03288
03289 bool finished = true;
03290 for(size_t j=0; j< border.size() ;j++){
03291 if(null_expr == new_inst[j]){
03292 finished = false;
03293 break;
03294 }
03295 }
03296
03297 if(finished){
03298 std::vector<Expr> good_inst;
03299 for(size_t j=0; j<border.size(); j++){
03300 good_inst.push_back(new_inst[j]);
03301 }
03302 instSet.push_back(good_inst);
03303 }
03304 else{
03305 recSearchCover(border,
03306 mtrigs,
03307 cur_depth+1,
03308 instSet,
03309 new_inst);
03310 }
03311 }
03312 }
03313
03314 void TheoryQuant::searchCover(const Expr& thm,
03315 const std::vector<Expr>& border,
03316 std::vector<std::vector<Expr> >& instSet
03317 ){
03318 std::vector<Expr> dumy(border.size()) ;
03319 for(size_t j=0; j< border.size() ;j++){
03320 dumy[j]=null_expr;
03321 }
03322 const std::vector<Expr>& mtrigs = d_multTriggers[thm];
03323 recSearchCover(border, mtrigs, 0, instSet, dumy);
03324 }
03325
03326 bool TheoryQuant::hasGoodSynMultiInst(const Expr& thm,
03327 std::vector<Expr> & boundVars,
03328 std::vector<std::vector<Expr> >& instSet,
03329 const CDList<Expr>& allterms,
03330 size_t tBegin){
03331
03332 const std::set<Expr>& bvs = getBoundVars(thm);
03333
03334 boundVars.clear();
03335 for(std::set<Expr>::const_iterator i=bvs.begin(),iend=bvs.end(); i!=iend; ++i)
03336 boundVars.push_back(*i);
03337
03338 instSet.clear();
03339
03340 bool new_match = false;
03341
03342
03343 const std::vector<Expr>& mtrigs = d_multTriggers[thm];
03344
03345 for(std::vector<Expr>::const_iterator i= mtrigs.begin(), iend = mtrigs.end(); i != iend; i++){
03346
03347 if(d_mtrigs_bvorder[*i].empty()){
03348 const std::set<Expr>& trig_bvs = getBoundVars(*i);
03349 for(std::set<Expr>::const_iterator j= trig_bvs.begin(), jend = trig_bvs.end();
03350 j != jend;
03351 j++){
03352 d_mtrigs_bvorder[*i].push_back(*j);
03353 }
03354 }
03355
03356 const std::vector<Expr>& trig_bvorder = d_mtrigs_bvorder[*i];
03357
03358 std::vector<std::vector<Expr> > trig_insts;
03359 trig_insts.clear();
03360
03361 std::vector<Expr> gtms;
03362 goodSynMatch(*i, trig_bvorder, trig_insts, gtms, allterms, tBegin);
03363
03364 if (trig_insts.size() > 0){
03365 new_match=true;
03366 if(d_mtrigs_inst.count(*i) <= 0){
03367 d_mtrigs_inst[*i] = new(true) CDList<std::vector<Expr> > (theoryCore()->getCM()->getCurrentContext());
03368 }
03369 for(std::vector<std::vector<Expr> >::const_iterator j = trig_insts.begin(), jend = trig_insts.end();
03370 j != jend;
03371 j++){
03372
03373 d_mtrigs_inst[*i]->push_back(*j);
03374 for(std::vector<Expr>::const_iterator k = j->begin(), kend = j->end();
03375 k != kend;
03376 k++){
03377 }
03378 }
03379 }
03380 }
03381
03382 for(std::vector<Expr>::const_iterator i= mtrigs.begin(), iend = mtrigs.end(); i != iend; i++){
03383 if (d_mtrigs_inst.count(*i) <=0 ) continue;
03384 for(CDList<std::vector<Expr> >::const_iterator j = d_mtrigs_inst[*i]->begin(),
03385 jend = d_mtrigs_inst[*i]->end();
03386 j != jend;
03387 j++){
03388
03389 for(std::vector<Expr>::const_iterator k = j->begin(), kend = j->end();
03390 k != kend;
03391 k++){
03392 }
03393 }
03394 }
03395 {
03396 if(new_match){
03397 searchCover(thm, boundVars, instSet);
03398 }
03399 }
03400
03401 if(instSet.size() > 0 ) {
03402 return true;
03403 }
03404 else {
03405 return false;
03406 }
03407
03408 }
03409
03410 bool inStrCache(std::set<std::string> cache, std::string str){
03411 return (cache.find(str) != cache.end());
03412 }
03413
03414
03415 bool TheoryQuant::hasGoodSemInst(const Expr& e,
03416 std::vector<Expr> & boundVars,
03417 std::set<std::vector<Expr> >& instSet,
03418 size_t tBegin){
03419 return false;
03420 }
03421
03422 void genPartInstSetThm(const std::vector<Expr>& bVarsThm,
03423 std::vector<Expr>& bVarsTerm,
03424 const std::vector<std::vector<Expr> >& termInst,
03425 std::vector<std::vector<Expr> >& instSetThm){
03426 ExprMap<bool> bVmap;
03427
03428 for(size_t i=0; i< bVarsThm.size(); ++i) {
03429 bVmap[bVarsThm[i]]=true;
03430 }
03431
03432 std::vector<Expr> tempBVterm;
03433 std::vector<int> locTerm;
03434
03435 for (size_t j=0; j<bVarsTerm.size(); j++){
03436 if (bVmap.count(bVarsTerm[j]) > 0){
03437 locTerm.push_back(1);
03438 tempBVterm.push_back(bVarsTerm[j]);
03439 }
03440 else{
03441 locTerm.push_back(0);
03442 }
03443 }
03444
03445 DebugAssert(locTerm.size() == bVarsTerm.size(), "locTerm.size !- bVarsTerm.size()");
03446
03447 for(std::vector<std::vector<Expr> >::const_iterator i=termInst.begin(),
03448 iend=termInst.end();i!=iend; i++) {
03449 std::vector<Expr> buf;
03450 buf.clear();
03451 for(size_t j=0; j< bVarsTerm.size(); ++j){
03452 if(locTerm[j])
03453 buf.push_back((*i)[j]);
03454 }
03455 instSetThm.push_back(buf);
03456 }
03457 bVarsTerm=tempBVterm;
03458 }
03459
03460
03461 void genInstSetThm(const std::vector<Expr>& bVarsThm,
03462 const std::vector<Expr>& bVarsTerm,
03463 const std::vector<std::vector<Expr> >& termInst,
03464 std::vector<std::vector<Expr> >& instSetThm){
03465
03466 std::vector<int> bVmap;
03467
03468 for(size_t i=0; i< bVarsThm.size(); ++i) {
03469 bVmap.push_back(-1);
03470 for (size_t j=0; j<bVarsTerm.size(); j++){
03471 if (bVarsThm[i] == bVarsTerm[j]){
03472 DebugAssert(bVmap[i] == -1, "bVmap[1] != -1");
03473 bVmap[i]=j;
03474 }
03475 }
03476 }
03477
03478 for(size_t i=0; i< bVarsThm.size(); ++i)
03479 if( -1 == bVmap[i]) {
03480 return;
03481 }
03482
03483 for(std::vector<std::vector<Expr> >::const_iterator i=termInst.begin(),
03484 iend=termInst.end();i!=iend; i++) {
03485 std::vector<Expr> buf;
03486 buf.clear();
03487 for(size_t j=0; j< bVarsThm.size(); ++j){
03488 buf.push_back((*i)[bVmap[j]]);
03489 }
03490 instSetThm.push_back(buf);
03491 }
03492 }
03493
03494
03495
03496
03497
03498
03499
03500
03501
03502
03503
03504
03505
03506
03507
03508
03509
03510 inline bool TheoryQuant::transFound(const Expr& comb){
03511 return (d_trans_found.count(comb) > 0);
03512 }
03513
03514 inline void TheoryQuant::setTransFound(const Expr& comb){
03515 d_trans_found[comb] = true;
03516 }
03517
03518 inline bool TheoryQuant::trans2Found(const Expr& comb){
03519 return (d_trans2_found.count(comb) > 0);
03520 }
03521
03522 inline void TheoryQuant::setTrans2Found(const Expr& comb){
03523 d_trans2_found[comb] = true;
03524 }
03525
03526
03527 inline CDList<Expr> & TheoryQuant::backList(const Expr& ex){
03528 if(d_trans_back.count(ex)>0){
03529 return *d_trans_back[ex];
03530 }
03531 else{
03532 return null_cdlist;
03533 }
03534 }
03535
03536 inline CDList<Expr> & TheoryQuant::forwList(const Expr& ex){
03537 if(d_trans_forw.count(ex)>0){
03538 return *d_trans_forw[ex];
03539 }
03540 else{
03541 return null_cdlist;
03542 }
03543 }
03544
03545 inline void TheoryQuant::pushBackList(const Expr& node, Expr ex){
03546 if(d_trans_back.count(node)>0){
03547 d_trans_back[node]->push_back(ex);
03548 }
03549 else{
03550 d_trans_back[node] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
03551 d_trans_back[node]->push_back(ex);
03552 }
03553 }
03554
03555 inline void TheoryQuant::pushForwList(const Expr& node, Expr ex){
03556 if(d_trans_forw.count(node)>0){
03557 d_trans_forw[node]->push_back(ex);
03558 }
03559 else{
03560 d_trans_forw[node] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
03561 d_trans_forw[node]->push_back(ex);
03562 }
03563 }
03564
03565
03566
03567
03568
03569
03570
03571
03572
03573
03574
03575
03576
03577
03578
03579
03580
03581
03582
03583
03584
03585
03586
03587
03588
03589
03590
03591
03592
03593
03594
03595
03596
03597
03598
03599
03600
03601
03602
03603
03604
03605
03606
03607
03608
03609
03610
03611
03612
03613
03614
03615
03616
03617
03618
03619
03620
03621
03622
03623
03624
03625
03626
03627
03628
03629
03630
03631
03632
03633
03634
03635
03636
03637
03638
03639
03640
03641
03642
03643
03644
03645
03646
03647
03648
03649
03650
03651
03652
03653
03654
03655
03656
03657
03658
03659
03660
03661
03662
03663
03664
03665
03666
03667
03668
03669
03670
03671
03672
03673
03674
03675
03676
03677
03678
03679
03680
03681
03682
03683
03684
03685
03686
03687
03688
03689
03690
03691
03692
03693
03694
03695
03696
03697
03698
03699
03700
03701
03702
03703
03704
03705
03706
03707
03708
03709
03710
03711
03712
03713
03714
03715
03716
03717
03718
03719
03720
03721
03722
03723
03724
03725
03726
03727
03728
03729
03730
03731
03732
03733
03734
03735
03736
03737
03738
03739
03740
03741
03742
03743
03744
03745
03746
03747
03748 void TheoryQuant::arrayHeuristic(const Trigger& trig, size_t univ_id){
03749
03750 std::vector<Expr> tp = d_arrayIndic[trig.head];
03751 for(size_t i=0; i<tp.size(); i++){
03752 const Expr& index = tp[i];
03753 std::vector<Expr> temp;
03754 temp.push_back(index);
03755 enqueueInst(univ_id, temp, index);
03756
03757 }
03758 }
03759
03760 void TheoryQuant::synNewInst(size_t univ_id, const vector<Expr>& bind, const Expr& gterm, const Trigger& trig ){
03761 if(trig.isMulti){
03762 const multTrigsInfo& mtriginfo = d_all_multTrigsInfo[trig.multiId];
03763
03764 vector<Expr> actual_bind;
03765 for(size_t i=0, iend=bind.size(); i<iend; i++){
03766 if(null_expr != bind[i]){
03767 actual_bind.push_back(bind[i]);
03768 }
03769 }
03770 Expr actual_bind_expr = Expr(RAW_LIST, actual_bind);
03771
03772 size_t index = trig.multiIndex;
03773 CDMap<Expr,bool> * cur_cd_map = mtriginfo.var_binds_found[index];
03774 CDMap<Expr,bool>::iterator cur_iter = cur_cd_map->find(actual_bind_expr);
03775
03776 if (cur_cd_map->end() != cur_iter){
03777 return;
03778 }
03779
03780 (*cur_cd_map)[actual_bind_expr] = true;
03781
03782 const vector<size_t>& comm_pos = mtriginfo.common_pos[0];
03783 size_t comm_pos_size = comm_pos.size();
03784
03785 Expr comm_expr;
03786 vector<Expr> comm_expr_vec;
03787 for(size_t i = 0; i < comm_pos_size; i++){
03788 comm_expr_vec.push_back(bind[comm_pos[i]]);
03789
03790 }
03791 if(0 == comm_pos_size){
03792 comm_expr = null_expr;
03793 }
03794 else{
03795 comm_expr = Expr(RAW_LIST, comm_expr_vec);
03796 }
03797 Expr uncomm_expr;
03798 vector<Expr> uncomm_expr_vec;
03799
03800 const vector<size_t>& uncomm_pos = mtriginfo.var_pos[index];
03801 size_t uncomm_pos_size = uncomm_pos.size();
03802 for(size_t i = 0; i< uncomm_pos_size; i++){
03803 uncomm_expr_vec.push_back(bind[uncomm_pos[i]]);
03804 }
03805 uncomm_expr = Expr(RAW_LIST, uncomm_expr_vec);
03806
03807 CDList<Expr>* add_into_list ;
03808 CDList<Expr>* iter_list;
03809 ExprMap<CDList<Expr>* >::iterator add_into_iter;
03810 ExprMap<CDList<Expr>* >::iterator iter_iter;
03811
03812 size_t other_index = 0;
03813 if(0 == index){
03814 other_index =1;
03815 }
03816 else if (1 == index){
03817 other_index = 0;
03818 }
03819 else{
03820 FatalAssert(false, "wrong ");
03821 }
03822
03823
03824 add_into_iter = mtriginfo.uncomm_list[index]->find(comm_expr);
03825 iter_iter = mtriginfo.uncomm_list[other_index]->find(comm_expr);
03826
03827 if(mtriginfo.uncomm_list[index]->end() == add_into_iter){
03828 add_into_list = new (true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
03829 (*mtriginfo.uncomm_list[index])[comm_expr] = add_into_list;
03830 }
03831 else{
03832 add_into_list = add_into_iter->second;
03833 }
03834
03835 add_into_list->push_back(uncomm_expr);
03836
03837 if(mtriginfo.uncomm_list[other_index]->end() == iter_iter){
03838 return;
03839 }
03840 else{
03841 iter_list = iter_iter->second;
03842 }
03843
03844 const vector<size_t>& uncomm_iter_pos = mtriginfo.var_pos[other_index];
03845 size_t uncomm_iter_pos_size = uncomm_iter_pos.size();
03846
03847 for(size_t i =0, iend = iter_list->size(); i<iend; i++){
03848 const Expr& cur_iter_expr = (*iter_list)[i];
03849 vector<Expr> new_bind(bind);
03850 for(size_t j=0; j<uncomm_iter_pos_size; j++){
03851 new_bind[uncomm_iter_pos[j]] = cur_iter_expr[j];
03852 }
03853 enqueueInst(univ_id, new_bind, gterm);
03854 }
03855 return;
03856 }
03857
03858 {
03859 if(trig.hasT2){
03860 vector<Expr> actual_bind;
03861 for(size_t i=0; i<bind.size(); i++){
03862 if(bind[i] != null_expr){
03863 actual_bind.push_back(bind[i]);
03864 }
03865 }
03866 if(actual_bind.size() != 2){
03867 cout<<"2 != bind.size()" <<endl;
03868 }
03869
03870 Expr acb1 = simplifyExpr(actual_bind[0]);
03871 Expr acb2 = simplifyExpr(actual_bind[1]);
03872 actual_bind[0]=acb1;
03873 actual_bind[1]=acb2;
03874 if(acb1 != acb2){
03875 Expr comb = Expr(RAW_LIST,acb1, acb2);
03876 if(!trans2Found(comb)){
03877 setTrans2Found(comb);
03878 Expr comb_rev = Expr(RAW_LIST,acb2, acb1);
03879 if(trans2Found(comb_rev)){
03880 enqueueInst(univ_id, actual_bind, gterm);
03881 }
03882 }
03883 }
03884 return;
03885 }
03886 }
03887
03888 {
03889 if(trig.hasTrans){
03890 vector<Expr> actual_bind;
03891 for(size_t i=0; i<bind.size(); i++){
03892 if(bind[i] != null_expr){
03893 actual_bind.push_back(simplifyExpr(bind[i]));
03894 }
03895 }
03896 if(simplifyExpr(actual_bind[0]) != simplifyExpr(actual_bind[1])){
03897 Expr comb = Expr(RAW_LIST,actual_bind[0], actual_bind[1]);
03898
03899 if(!transFound(comb)){
03900 setTransFound(comb);
03901
03902 Expr sr(actual_bind[0]);
03903 Expr dt(actual_bind[1]);
03904
03905 const CDList<Expr>& dtForw = forwList(dt);
03906 const CDList<Expr>& srBack = backList(sr);
03907
03908 for(size_t k=0; k<dtForw.size(); k++){
03909 vector<Expr> tri_bind;
03910 tri_bind.push_back(sr);
03911 tri_bind.push_back(dt);
03912 tri_bind.push_back(dtForw[k]);
03913
03914 enqueueInst(univ_id, tri_bind, gterm);
03915 }
03916
03917 for(size_t k=0; k<srBack.size(); k++){
03918 vector<Expr> tri_bind;
03919 tri_bind.push_back(srBack[k]);
03920 tri_bind.push_back(sr);
03921 tri_bind.push_back(dt);
03922
03923 enqueueInst(univ_id, tri_bind, gterm);
03924
03925
03926 }
03927
03928 pushForwList(sr,dt);
03929 pushBackList(dt,sr);
03930 }
03931 }
03932 return;
03933 }
03934 }
03935
03936 enqueueInst(univ_id, bind, gterm);
03937
03938
03939 }
03940
03941
03942
03943
03944
03945
03946
03947
03948
03949
03950
03951
03952
03953
03954
03955
03956
03957
03958
03959
03960
03961
03962
03963
03964
03965
03966
03967
03968
03969
03970
03971
03972
03973
03974
03975
03976
03977
03978
03979
03980
03981
03982
03983
03984
03985
03986
03987
03988
03989
03990
03991
03992
03993
03994
03995
03996
03997
03998
03999
04000
04001
04002
04003
04004
04005
04006
04007
04008
04009
04010
04011
04012
04013
04014
04015
04016
04017
04018
04019
04020
04021
04022
04023
04024
04025
04026
04027
04028
04029
04030
04031
04032
04033
04034
04035
04036
04037
04038
04039
04040
04041
04042
04043
04044
04045
04046
04047
04048
04049
04050
04051
04052
04053
04054
04055
04056
04057
04058
04059
04060
04061
04062
04063
04064
04065
04066
04067
04068
04069
04070
04071
04072
04073
04074
04075
04076
04077
04078
04079
04080
04081
04082
04083
04084
04085
04086
04087
04088
04089
04090
04091
04092
04093
04094
04095
04096
04097
04098
04099
04100
04101
04102
04103
04104
04105
04106
04107
04108
04109
04110
04111
04112
04113
04114
04115 void TheoryQuant::semInst(const Theorem & univ, size_t tBegin){
04116 }
04117
04118 void TheoryQuant::checkSat(bool fullEffort){
04119 if(*d_translate) return;
04120 if(d_rawUnivs.size() <=0 ) return;
04121
04122 DebugAssert(d_univsQueue.size() == 0, "something left in d_univsQueue");
04123 DebugAssert(d_simplifiedThmQueue.size() == 0, "something left in d_univsQueue");
04124
04125 #ifdef DEBUG
04126 if(fullEffort){
04127 if( CVC3::debugger.trace("quant assertfact") ){
04128 cout<<"===========all cached univs =========="<<endl;
04129
04130
04131
04132
04133
04134
04135 }
04136 if( CVC3::debugger.trace("quant samehead") ){
04137 cout<<"===========all cached =========="<<endl;
04138 for (ExprMap< CDList<Expr>*>::iterator i=d_same_head_expr.begin(), iend=d_same_head_expr.end(); i!=iend; i++){
04139 cout<<"------------------------------------"<<endl;
04140 cout<<(i->first)<<endl;
04141 cout<<"_______________________"<<endl;
04142 CDList<Expr> * terms= i->second;
04143 for(size_t i =0; i<terms->size(); i++){
04144 cout<<(*terms)[i]<<endl;
04145 }
04146 }
04147 }
04148 }
04149 #endif
04150
04151 #ifdef DEBUG
04152 if( CVC3::debugger.trace("quant checksat") ){
04153 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
04154 cout<<"=========== cur pred & terms =========="<<endl;
04155
04156 for (size_t i=d_lastPredsPos; i<allpreds.size(); i++){
04157 cout<<"i="<<allpreds[i].getIndex()<<" :"<<findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
04158 }
04159
04160 const CDList<Expr>& allterms = theoryCore()->getTerms();
04161
04162 for (size_t i=d_lastTermsPos; i<allterms.size(); i++){
04163 cout<<"i="<<allterms[i].getIndex()<<" :"<<findExpr(allterms[i])<<"|"<<allterms[i]<<endl;
04164 }
04165 cout<<"=========== cur quant =========="<<endl;
04166 for (size_t i=0; i<d_univs.size(); i++){
04167 cout<<"i="<<d_univs[i].getExpr().getIndex()<<" :"<<findExpr(d_univs[i].getExpr())<<"|"<<d_univs[i]<<endl;
04168 }
04169 }
04170
04171
04172 if( CVC3::debugger.trace("quant checksat equ") ){
04173 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
04174 cout<<"=========== cur pred equ =========="<<endl;
04175
04176 for (size_t i=d_lastPredsPos; i<allpreds.size(); i++){
04177 if(allpreds[i].isEq()){
04178 cout<<"i="<<allpreds[i].getIndex()<<" :"<<findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
04179 }
04180 }
04181 cout<<"=========== cur pred equ end =========="<<endl;
04182 }
04183
04184 #endif
04185
04186 if((*d_useLazyInst && !fullEffort) ) return;
04187
04188 {
04189 const CDList<Expr>& allterms = theoryCore()->getTerms();
04190 for(size_t i=d_lastTermsPos; i<allterms.size(); i++){
04191 Expr t = allterms[i];
04192 if(canGetHead(t)){
04193 if(d_same_head_expr.count(getHead(t)) >0){
04194 d_same_head_expr[getHead(t)]->push_back(t);
04195 }
04196 else{
04197 d_same_head_expr[getHead(t)]=
04198 new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
04199 d_same_head_expr[getHead(t)]->push_back(t);
04200 }
04201 }
04202 }
04203
04204 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
04205 for(size_t i=d_lastPredsPos; i<allpreds.size(); i++){
04206 Expr t = allpreds[i];
04207 if(canGetHead(t)){
04208 if(d_same_head_expr.count(getHead(t)) >0){
04209 d_same_head_expr[getHead(t)]->push_back(t);
04210 }
04211 else{
04212 d_same_head_expr[getHead(t)]=
04213 new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
04214 d_same_head_expr[getHead(t)]->push_back(t);
04215 }
04216 }
04217 }
04218 }
04219
04220 {
04221 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
04222 for(size_t i=d_lastPredsPos; i<allpreds.size(); i++){
04223 const Expr& t = allpreds[i];
04224 if(t.isEq()){
04225
04226 const Expr lterm = t[0];
04227 const Expr rterm = t[1];
04228 d_eqs.push_back(lterm);
04229 d_eqs.push_back(rterm);
04230
04231
04232
04233
04234
04235
04236
04237
04238
04239
04240
04241
04242
04243
04244
04245
04246
04247
04248
04249
04250
04251
04252 }
04253 }
04254 }
04255
04256
04257 {
04258 const CDList<Expr>& allterms = theoryCore()->getTerms();
04259 for(size_t i=d_lastTermsPos; i<allterms.size(); i++){
04260 const Expr& cur=allterms[i];
04261 if(READ == cur.getKind() || WRITE == cur.getKind()){
04262 arrayIndexName(cur);
04263 }
04264 }
04265 }
04266
04267 d_instThisRound = 0;
04268 d_useMultTrig=*d_useMult;
04269 d_usePartTrig=*d_usePart;
04270 d_useFullTrig=true;
04271
04272 if(fullEffort) {
04273 d_inEnd=true;
04274 }
04275 else{
04276 d_inEnd=false;
04277 }
04278
04279
04280 ExprMap<ExprMap<vector<dynTrig>* >* > new_trigs;
04281 for(size_t i=d_univs.size(); i<d_rawUnivs.size(); i++){
04282 setupTriggers(new_trigs, d_rawUnivs[i], i);
04283 }
04284
04285 try {
04286 if (!(*d_useNew)){
04287 naiveCheckSat(fullEffort);
04288 }
04289 else if (*d_useSemMatch){
04290 semCheckSat(fullEffort);
04291 }
04292 else {
04293 synCheckSat(new_trigs, fullEffort);
04294 }
04295 }
04296
04297 catch (int x){
04298
04299 while(!d_simplifiedThmQueue.empty()){
04300 d_simplifiedThmQueue.pop();
04301 }
04302 d_tempBinds.clear();
04303 saveContext();
04304 delNewTrigs(new_trigs);
04305 return;
04306 }
04307
04308 sendInstNew();
04309
04310 saveContext();
04311
04312 try{
04313 if((*d_useNew) && (0 == d_instThisRound) && fullEffort && theoryCore()->getTerms().size()< (size_t)(*d_maxNaiveCall) ) {
04314
04315 if (0== theoryCore()->getTerms().size()){
04316 static int counter =0;
04317
04318 std::set<Expr> types;
04319 for(size_t i = 0; i<d_univs.size(); i++){
04320 const Expr& cur_quant = d_univs[i].getExpr();
04321 const std::vector<Expr> cur_vars = cur_quant.getVars();
04322 for(size_t j =0; j<cur_vars.size(); j++){
04323 types.insert(cur_vars[j].getType().getExpr());
04324 }
04325 }
04326
04327 std::string base("_naiveInst");
04328 for(std::set<Expr>::iterator i=types.begin(), iend = types.end(); i != iend; i++){
04329 counter++;
04330 std::stringstream tempout;
04331 tempout << counter;
04332 std::string out_str = base + tempout.str();
04333 Expr newExpr = theoryCore()->getEM()->newVarExpr(out_str);
04334
04335 newExpr.setType(Type(*i));
04336
04337 Proof pf;
04338
04339 Expr newExpr2 = theoryCore()->getEM()->newVarExpr(out_str+"extra");
04340 newExpr2.setType(Type(*i));
04341
04342 Expr newConstThm;
04343
04344 if(Type(*i) == theoryCore()->getEM()->newRatExpr(0).getType()){
04345
04346 newConstThm = newExpr.eqExpr(theoryCore()->getEM()->newRatExpr(0));
04347 }
04348 else{
04349 newConstThm = newExpr.eqExpr(newExpr2);
04350 }
04351 Theorem newThm = d_rules->addNewConst(newConstThm);
04352
04353 enqueueFact(newThm);
04354 d_tempBinds.clear();
04355 return;
04356 }
04357
04358 }
04359 naiveCheckSat(fullEffort);
04360 }
04361 }
04362
04363 catch (int x){
04364
04365 while(!d_simplifiedThmQueue.empty()){
04366 d_simplifiedThmQueue.pop();
04367 }
04368 d_tempBinds.clear();
04369 saveContext();
04370 delNewTrigs(new_trigs);
04371 return;
04372 }
04373
04374 if(fullEffort) {
04375 sendInstNew();
04376 }
04377
04378 combineOldNewTrigs(new_trigs);
04379 delNewTrigs(new_trigs);
04380 }
04381
04382 void TheoryQuant::saveContext(){
04383 d_lastArrayPos.set(d_arrayTrigs.size());
04384 d_univsSavedPos.set(d_univs.size());
04385 d_rawUnivsSavedPos.set(d_rawUnivs.size());
04386 d_lastTermsPos.set(theoryCore()->getTerms().size());
04387 d_lastPredsPos.set(theoryCore()->getPredicates().size());
04388 d_lastUsefulGtermsPos.set(d_usefulGterms.size());
04389 }
04390
04391
04392
04393
04394 void TheoryQuant::synCheckSat(ExprMap<ExprMap<vector<dynTrig>* >* >& new_trigs, bool fullEffort){
04395
04396 d_allout=false;
04397
04398 if(fullEffort) {
04399 setIncomplete("Quantifier instantiation");
04400 }
04401
04402 size_t uSize = d_univs.size() ;
04403 const CDList<Expr>& allterms = theoryCore()->getTerms();
04404 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
04405 size_t tSize = allterms.size();
04406 size_t pSize = allpreds.size();
04407
04408 TRACE("quant",uSize, " uSize and univsSavedPOS ", d_univsSavedPos);
04409 TRACE("quant",tSize, " tSize and termsLastPos ", d_lastTermsPos);
04410 TRACE("quant",pSize, " pSize and predsLastPos ", d_lastPredsPos);
04411 TRACE("quant", fullEffort, " fulleffort:scope ",theoryCore()->getCM()->scopeLevel() );
04412
04413 for(size_t i=d_lastTermsPos; i<tSize; i++){
04414 const Expr& cur(allterms[i]);
04415 if(usefulInMatch(cur)){
04416 if(*d_useExprScore){
04417 int score = getExprScore(cur);
04418 if(score <= d_curMaxExprScore && 0 <= score ){
04419 d_usefulGterms.push_back(cur);
04420 add_parent(cur);
04421 }
04422 }
04423 else{
04424 d_usefulGterms.push_back(cur);
04425 add_parent(cur);
04426 }
04427 }
04428 else{
04429 }
04430 }
04431
04432 for(size_t i=d_lastPredsPos; i<pSize; i++){
04433 const Expr& cur=allpreds[i];
04434 if( usefulInMatch(cur)){
04435 if(*d_useExprScore ){
04436 int score = getExprScore(cur);
04437 if(score <= d_curMaxExprScore && 0 <= score){
04438 d_usefulGterms.push_back(cur);
04439 add_parent(cur);
04440 }
04441 }
04442 else{
04443 d_usefulGterms.push_back(cur);
04444 add_parent(cur);
04445 }
04446 }
04447 else{
04448 }
04449 }
04450
04451
04452 if(d_useFullTrig && d_inEnd && *d_useInstEnd ){
04453
04454 if(*d_useExprScore){
04455
04456 matchListOld(d_usefulGterms, d_lastUsefulGtermsPos, d_usefulGterms.size() );
04457 matchListNew(new_trigs, d_usefulGterms, 0, d_usefulGterms.size());
04458
04459 if(sendInstNew() > 0){
04460 TRACE("inend", "debug 1", "" ,"" );
04461 return;
04462 }
04463
04464 d_allout = true;
04465 {
04466 CDList<Expr>* changed_terms = new (false) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
04467 collectChangedTerms(*changed_terms);
04468
04469 matchListOld(*changed_terms, 0, changed_terms->size());
04470 matchListNew(new_trigs, *changed_terms, 0 , changed_terms->size());
04471 delete changed_terms;
04472 }
04473
04474 int n;
04475 if( ( n = sendInstNew()) > 0){
04476 TRACE("inend", "debug 2", " # ",n );
04477 return;
04478 }
04479 d_allout = false;
04480
04481
04482 int numNewTerm=0;
04483 int oldNum=d_usefulGterms.size();
04484
04485 for(size_t i=0; i<tSize; i++){
04486 const Expr& cur(allterms[i]);
04487 if(!(usefulInMatch(cur))) continue;
04488 int score = getExprScore(cur);
04489 if( score > d_curMaxExprScore){
04490 if((d_curMaxExprScore + 1) == score){
04491 d_usefulGterms.push_back(cur);
04492 add_parent(cur);
04493 numNewTerm++;
04494 }
04495 else{
04496 TRACE("inend", "is this good? ", cur.toString()+" #-# " , score);
04497 d_usefulGterms.push_back(cur);
04498 add_parent(cur);
04499 numNewTerm++;
04500 }
04501 }
04502 }
04503
04504 for(size_t i=0; i<pSize; i++){
04505 const Expr& cur(allpreds[i]);
04506 if(!(usefulInMatch(cur))) continue;
04507 int score = getExprScore(cur);
04508 if( score > d_curMaxExprScore){
04509 if((d_curMaxExprScore + 1) == score){
04510 d_usefulGterms.push_back(cur);
04511 add_parent(cur);
04512 numNewTerm++;
04513 }
04514 else{
04515 TRACE("inend", "is this good? ", cur.toString()+" #-# " , score);
04516 d_usefulGterms.push_back(cur);
04517 add_parent(cur);
04518 numNewTerm++;
04519 }
04520 }
04521 }
04522
04523 if(numNewTerm >0 ){
04524
04525 if(d_curMaxExprScore >=0 ){
04526
04527 d_curMaxExprScore = d_curMaxExprScore+1;;
04528 }
04529 else {
04530 d_curMaxExprScore = d_curMaxExprScore+1;
04531 }
04532
04533 matchListOld(d_usefulGterms, oldNum, d_usefulGterms.size() );
04534 matchListNew(new_trigs, d_usefulGterms, oldNum, d_usefulGterms.size());
04535
04536 if(sendInstNew() > 0){
04537 TRACE("inend", "debug 3", "" , "" );
04538 return;
04539 }
04540 }
04541 for(size_t array_index = 0; array_index < d_arrayTrigs.size(); array_index++){
04542 arrayHeuristic(d_arrayTrigs[array_index].trig, d_arrayTrigs[array_index].univ_id);
04543 }
04544
04545 return ;
04546 }
04547
04548 TRACE("inend", "debug 3 0", "", "");
04549 TRACE("quant","this round; ",d_callThisRound,"");
04550
04551 return;
04552 }
04553
04554
04555 if ((uSize == d_univsSavedPos) &&
04556 (tSize == d_lastTermsPos) &&
04557 (pSize == d_lastPredsPos) ) return;
04558
04559
04560 matchListOld(d_usefulGterms, d_lastUsefulGtermsPos,d_usefulGterms.size() );
04561
04562 matchListNew(new_trigs, d_usefulGterms, 0, d_usefulGterms.size() );
04563
04564 for(size_t array_index = d_lastArrayPos; array_index < d_arrayTrigs.size(); array_index++){
04565 arrayHeuristic(d_arrayTrigs[array_index].trig, d_arrayTrigs[array_index].univ_id);
04566 }
04567
04568 TRACE("quant","this round; ",d_callThisRound,"");
04569
04570 return;
04571 }
04572
04573
04574 void TheoryQuant::semCheckSat(bool fullEffort){
04575 }
04576
04577
04578 void TheoryQuant::naiveCheckSat(bool fullEffort){
04579 TRACE("quant", "checkSat ", fullEffort, "{");
04580 IF_DEBUG(int instCount = d_instCount);
04581 size_t uSize = d_univs.size(), stSize = d_savedTerms.size();
04582 if(true || (fullEffort && uSize > 0)) {
04583
04584 setIncomplete("Quantifier instantiation");
04585
04586 if(d_instCount>=*d_maxQuantInst)
04587 return;
04588
04589
04590
04591 bool savedOnly = ((uSize > d_univsSavedPos.get() && stSize > 0) ||
04592 (stSize > d_savedTermsPos.get()));
04593 int origCount = d_instCount;
04594 if(savedOnly)
04595 {
04596 TRACE("quant", "checkSat [saved insts]: univs size = ", uSize , " ");
04597 for(size_t i=0, pos = d_univsSavedPos.get(); i<uSize; i++) {
04598 if(d_instCount>= *d_maxQuantInst)
04599 break;
04600 else
04601 instantiate(d_univs[i], i>=pos, true, d_savedTermsPos.get());
04602 }
04603 d_univsSavedPos.set(d_univs.size());
04604 d_savedTermsPos.set(stSize);
04605 }
04606 if(!savedOnly || d_instCount == origCount)
04607 {
04608 TRACE("quant", "checkSat [context insts]: univs size = ", uSize , " ");
04609 const CDList<Expr>& assertions = theoryCore()->getTerms();
04610 int origSize = d_contextTerms.size();
04611
04612
04613
04614 TRACE("quant", "checkSat terms size = ", assertions.size() , " ");
04615 mapTermsByType(assertions);
04616 for(size_t i=0, pos = d_univsContextPos.get(); i<uSize; i++) {
04617 if(d_instCount>= *d_maxQuantInst)
04618 break;
04619 else
04620 instantiate(d_univs[i], i>=pos, false, origSize);
04621 }
04622 d_univsContextPos.set(d_univs.size());
04623 }
04624 TRACE("quant terse", "checkSat total insts: ",
04625 d_instCount, ", new "+int2string(d_instCount - instCount));
04626 }
04627 TRACE("quant", "checkSat total insts: ", d_instCount, " ");
04628 TRACE("quant", "checkSat new insts: ", d_instCount - instCount, " ");
04629 TRACE("quant", "checkSat effort:", fullEffort, " }");
04630
04631 }
04632
04633
04634
04635
04636
04637
04638
04639
04640
04641
04642 void TheoryQuant::instantiate(Theorem univ, bool all, bool savedMap,
04643 size_t newIndex)
04644 {
04645
04646 if(!all && ((savedMap && newIndex == d_savedTerms.size())
04647 ||(!savedMap && newIndex == d_contextTerms.size())))
04648 return;
04649
04650 TRACE("quant", "instanitate", all , "{");
04651 std::vector<Expr> varReplacements;
04652 recInstantiate(univ, all, savedMap, newIndex, varReplacements);
04653 TRACE("quant", "instanitate", "", "}");
04654
04655 }
04656
04657
04658 void TheoryQuant::recInstantiate(Theorem& univ, bool all, bool savedMap,
04659 size_t newIndex,
04660 std::vector<Expr>& varReplacements)
04661 {
04662 Expr quantExpr = univ.getExpr();
04663 const vector<Expr>& boundVars = quantExpr.getVars();
04664
04665 size_t curPos = varReplacements.size();
04666 TRACE("quant", "recInstantiate: ", boundVars.size() - curPos, "");
04667
04668 if(curPos == boundVars.size()) {
04669 if(!all)
04670 return;
04671 Theorem t = d_rules->universalInst(univ, varReplacements);
04672 d_insts[t.getExpr()] = varReplacements;
04673 TRACE("quant", "recInstantiate => " , t.toString(), "");
04674 if(d_instCount< *d_maxQuantInst) {
04675 d_instCount=d_instCount+1;
04676 enqueueInst(univ, varReplacements, null_expr);
04677
04678
04679 }
04680 return;
04681 }
04682
04683
04684 else {
04685 Type t = getBaseType(boundVars[curPos]);
04686 int iendC=0, iendS=0, iend;
04687 std::vector<size_t>* typeVec = NULL;
04688 CDList<size_t>* typeList = NULL;
04689 if(d_savedMap.count(t) > 0) {
04690 typeVec = &(d_savedMap[t]);
04691 iendS = typeVec->size();
04692 TRACE("quant", "adding from savedMap: ", iendS, "");
04693 }
04694 if(!savedMap) {
04695 if(d_contextMap.count(t) > 0) {
04696 typeList = d_contextMap[t];
04697 iendC = typeList->size();
04698 TRACE("quant", "adding from contextMap:", iendC , "");
04699 }
04700 }
04701 iend = iendC + iendS;
04702 for(int i =0; i<iend; i++) {
04703 TRACE("quant", "I must have gotten here!", "", "");
04704 size_t index;
04705 if(i<iendS){
04706 index = (*typeVec)[i];
04707 varReplacements.push_back(d_savedTerms[index]);
04708 }
04709 else {
04710 index = (*typeList)[i-iendS];
04711 varReplacements.push_back(d_contextTerms[index]);
04712 }
04713 if((index < newIndex) || (!savedMap && i<iendS))
04714 recInstantiate(univ, all, savedMap, newIndex, varReplacements);
04715 else
04716 recInstantiate(univ, true, savedMap, newIndex, varReplacements);
04717 varReplacements.pop_back();
04718 }
04719
04720
04721 }
04722 }
04723
04724
04725
04726
04727
04728
04729 void TheoryQuant::mapTermsByType(const CDList<Expr>& terms)
04730 {
04731 Expr trExpr=trueExpr(), flsExpr = falseExpr();
04732 Type boolT = boolType();
04733 if(d_contextMap.count(boolT) == 0)
04734 {
04735 d_contextMap[boolT] =
04736 new(true) CDList<size_t>(theoryCore()->getCM()->getCurrentContext());
04737 size_t pos = d_contextTerms.size();
04738 d_contextTerms.push_back(trExpr);
04739 d_contextTerms.push_back(flsExpr);
04740 (*d_contextMap[boolT]).push_back(pos);
04741 (*d_contextMap[boolT]).push_back(pos+1);
04742 }
04743 for(size_t i=0; i<terms.size(); i++)
04744 recursiveMap(terms[i]);
04745
04746 for(size_t i=0; i<d_univs.size(); i++)
04747 recursiveMap(d_univs[i].getExpr());
04748 }
04749
04750
04751
04752
04753
04754
04755
04756
04757 bool TheoryQuant::recursiveMap(const Expr& e)
04758 {
04759 if(d_contextCache.count(e)>0) {
04760 return(d_contextCache[e]);
04761 }
04762 if(e.arity()>0) {
04763 for(Expr::iterator it = e.begin(), iend = e.end(); it!=iend; ++it)
04764
04765 if(recursiveMap(*it) == false) {
04766 d_contextCache[e] = false;
04767 }
04768 }
04769 else if(e.getKind() == EXISTS || e.getKind() == FORALL){
04770
04771 if(recursiveMap(e.getBody())==false) {
04772 d_contextCache[e]=false;
04773 }
04774 }
04775
04776 if(d_contextCache.count(e)>0) {
04777 return false;
04778 }
04779
04780 if(d_savedCache.count(e) > 0) {
04781 return true;
04782 }
04783
04784 Type type = getBaseType(e);
04785
04786 if(!type.isBool() && !(e.getKind()==BOUND_VAR)){
04787 TRACE("quant", "recursiveMap: found ",
04788 e.toString() + " of type " + type.toString(), "");
04789 int pos = d_contextTerms.size();
04790 d_contextTerms.push_back(e);
04791 if(d_contextMap.count(type)==0)
04792 d_contextMap[type] =
04793 new(true) CDList<size_t>(theoryCore()->getCM()->getCurrentContext());
04794 (*d_contextMap[type]).push_back(pos);
04795 }
04796
04797 if(e.getKind() == BOUND_VAR) {
04798 d_contextCache[e] = false;
04799 return false;
04800 }
04801 else {
04802 d_contextCache[e] = true;
04803 return true;
04804 }
04805
04806
04807
04808 }
04809
04810
04811
04812
04813 void TheoryQuant::notifyInconsistent(const Theorem& thm){
04814 #ifdef DEBUG
04815
04816 if( CVC3::debugger.trace("quant inscon") ){
04817
04818 cout<<"the one caused incsonsistency"<<endl;
04819 cout<<thm.getAssumptionsRef().toString()<<endl;
04820 std::vector<Expr> assump;
04821 thm.getLeafAssumptions(assump);
04822
04823 cout<<"===========leaf assumptions; =========="<<endl;
04824 for(std::vector<Expr>::iterator i=assump.begin(), iend=assump.end(); i!=iend; i++){
04825 cout<<">>"<<i->toString()<<endl;
04826 }
04827 }
04828 #endif
04829
04830 if(d_univs.size() == 0)
04831 return;
04832 DebugAssert(thm.getExpr().isFalse(), "notifyInconsistent called with"
04833 " theorem: " + thm.toString() + " which is not a derivation of false");
04834 TRACE("quant", "notifyInconsistent: { " , thm.toString(), "}");
04835
04836
04837 TRACE("quant terse", "notifyInconsistent: savedTerms size = ",
04838 d_savedTerms.size(), "");
04839 TRACE("quant terse", "last term: ",
04840 d_savedTerms.size()? d_savedTerms.back() : Expr(), "");
04841 }
04842
04843
04844
04845 void TheoryQuant::findInstAssumptions(const Theorem& thm)
04846 {
04847 if(thm.isNull() || thm.isRefl() || thm.isFlagged())
04848 return;
04849 thm.setFlag();
04850 const Expr& e = thm.getExpr();
04851 if(d_insts.count(e) > 0) {
04852 vector<Expr>& insts = d_insts[e];
04853 int pos;
04854 for(vector<Expr>::iterator it = insts.begin(), iend = insts.end(); it!=iend
04855 ; ++it)
04856 {
04857 if(d_savedCache.count(*it) == 0) {
04858 TRACE("quant", "notifyInconsistent: found:", (*it).toString(), "");
04859 d_savedCache[*it] = true;
04860 pos = d_savedTerms.size();
04861 d_savedTerms.push_back(*it);
04862 d_savedMap[getBaseType(*it)].push_back(pos);
04863 }
04864 }
04865 }
04866 if(thm.isAssump())
04867 return;
04868 const Assumptions& a = thm.getAssumptionsRef();
04869 for(Assumptions::iterator it =a.begin(), iend = a.end(); it!=iend; ++it){
04870 findInstAssumptions(*it);
04871 }
04872 }
04873
04874
04875 void TheoryQuant::computeType(const Expr& e)
04876 {
04877 switch (e.getKind()) {
04878 case FORALL:
04879 case EXISTS: {
04880 if(!e.getBody().getType().isBool())
04881 throw TypecheckException("Type mismatch for expression:\n\n "
04882 + e.getBody().toString()
04883 + "\n\nhas the following type:\n\n "
04884 + e.getBody().getType().toString()
04885 + "\n\nbut the expected type is Boolean:\n\n ");
04886 else
04887
04888 e.setType(e.getBody().getType());
04889 break;
04890 }
04891 default:
04892 DebugAssert(false,"Unexpected kind in Quantifier Theory: "
04893 + e.toString());
04894 break;
04895 }
04896 }
04897
04898
04899
04900
04901
04902
04903
04904
04905
04906 Expr TheoryQuant::computeTCC(const Expr& e) {
04907 DebugAssert(e.isQuantifier(), "Unexpected expression in Quantifier Theory: "
04908 + e.toString());
04909
04910 bool forall(e.getKind() == FORALL);
04911 const Expr& phi = e.getBody();
04912 Expr tcc_phi = getTCC(phi);
04913 Expr forall_tcc = getEM()->newClosureExpr(FORALL, e.getVars(), tcc_phi);
04914 Expr exists_tcc = getEM()->newClosureExpr(EXISTS, e.getVars(),
04915 tcc_phi && (forall? !phi : phi));
04916 return (forall_tcc || exists_tcc);
04917 }
04918
04919
04920 ExprStream&
04921 TheoryQuant::print(ExprStream& os, const Expr& e) {
04922 switch(os.lang()) {
04923 case SIMPLIFY_LANG:
04924 {
04925 switch(e.getKind()){
04926 case FORALL:
04927 case EXISTS: {
04928 if(!e.isQuantifier()) {
04929 e.print(os);
04930 break;
04931 }
04932 os << "(" << ((e.getKind() == FORALL)? "FORALL" : "EXISTS");
04933 const vector<Expr>& vars = e.getVars();
04934 bool first(true);
04935 os << "(" ;
04936 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
04937 i!=iend; ++i) {
04938 if(first) first = false;
04939 else os << " " ;
04940 os << *i;
04941
04942
04943
04944
04945 }
04946 os << ") " << e.getBody() << ")";
04947 }
04948 break;
04949 default:
04950 e.print(os);
04951 break;
04952 }
04953 break;
04954 }
04955
04956 case PRESENTATION_LANG: {
04957 switch(e.getKind()){
04958 case FORALL:
04959 case EXISTS: {
04960 if(!e.isQuantifier()) {
04961 e.print(os);
04962 break;
04963 }
04964 os << "(" << push << ((e.getKind() == FORALL)? "FORALL" : "EXISTS")
04965 << space << push;
04966 const vector<Expr>& vars = e.getVars();
04967 bool first(true);
04968 os << "(" << push;
04969 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
04970 i!=iend; ++i) {
04971 if(first) first = false;
04972 else os << push << "," << pop << space;
04973 os << *i;
04974
04975
04976
04977 if(*d_translate || true){
04978 if(i->isVar())
04979 os << ":" << space << pushdag << (*i).getType() << popdag;
04980 }
04981 }
04982 os << push << "): " << pushdag << push
04983 << e.getBody() << push << ")";
04984 }
04985 break;
04986 default:
04987 e.print(os);
04988 break;
04989 }
04990 break;
04991 }
04992 case SMTLIB_LANG: {
04993 d_theoryUsed = true;
04994 switch(e.getKind()){
04995 case FORALL:
04996 case EXISTS: {
04997 if(!e.isQuantifier()) {
04998 e.print(os);
04999 break;
05000 }
05001 os << "(" << push << ((e.getKind() == FORALL)? "forall" : "exists")
05002 << space;
05003 const vector<Expr>& vars = e.getVars();
05004 bool first(true);
05005
05006 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
05007 i!=iend; ++i) {
05008 if(first) first = false;
05009 else os << space;
05010 os << "(" << push << *i;
05011
05012
05013 if(i->isVar())
05014 os << space << pushdag << (*i).getType() << popdag;
05015 os << push << ")" << pop << pop;
05016 }
05017 os << space << pushdag
05018 << e.getBody() << push << ")";
05019 break;
05020 }
05021 default:
05022 throw SmtlibException("TheoryQuant::print: SMTLIB_LANG: Unexpected expression: "
05023 +getEM()->getKindName(e.getKind()));
05024 break;
05025 }
05026 break;
05027 }
05028 case LISP_LANG: {
05029 switch(e.getKind()){
05030 case FORALL:
05031 case EXISTS: {
05032 if(!e.isQuantifier()) {
05033 e.print(os);
05034 break;
05035 }
05036 os << "(" << push << ((e.getKind() == FORALL)? "FORALL" : "EXISTS")
05037 << space;
05038 const vector<Expr>& vars = e.getVars();
05039 bool first(true);
05040 os << "(" << push;
05041 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
05042 i!=iend; ++i) {
05043 if(first) first = false;
05044 else os << space;
05045 os << "(" << push << *i;
05046
05047
05048 if(i->isVar())
05049 os << space << pushdag << (*i).getType() << popdag;
05050 os << push << ")" << pop << pop;
05051 }
05052 os << push << ")" << pop << pop << pushdag
05053 << e.getBody() << push << ")";
05054 }
05055 break;
05056 default:
05057 e.print(os);
05058 break;
05059 }
05060 break;
05061 }
05062 default:
05063 e.print(os);
05064 break;
05065 }
05066 return os;
05067 }
05068
05069
05070
05071
05072
05073 Expr
05074 TheoryQuant::parseExprOp(const Expr& e) {
05075 TRACE("parser", "TheoryQuant::parseExprOp(", e, ")");
05076
05077
05078 if(RAW_LIST != e.getKind()) return e;
05079
05080 DebugAssert(e.arity() > 0,
05081 "TheoryQuant::parseExprOp:\n e = "+e.toString());
05082
05083 const Expr& c1 = e[0][0];
05084 const string& opName(c1.getString());
05085 int kind = getEM()->getKind(opName);
05086 switch(kind) {
05087 case FORALL:
05088 case EXISTS: {
05089 if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() > 0))
05090 throw ParserException("Bad "+opName+" expression: "+e.toString());
05091
05092 vector<pair<string,Type> > vars;
05093 for(Expr::iterator i=e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
05094 if(i->getKind() != RAW_LIST || i->arity() < 2)
05095 throw ParserException("Bad variable declaration block in "+opName
05096 +" expression: "+i->toString()
05097 +"\n e = "+e.toString());
05098
05099
05100
05101 Type tp(parseExpr((*i)[i->arity()-1]));
05102 if (tp == boolType()) {
05103 throw ParserException("A quantified variable may not be of type BOOLEAN");
05104 }
05105 for(int j=0, jend=i->arity()-1; j<jend; ++j) {
05106 if((*i)[j].getKind() != ID)
05107 throw ParserException("Bad variable declaration in "+opName+""
05108 " expression: "+(*i)[j].toString()+
05109 "\n e = "+e.toString());
05110 vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
05111 }
05112 }
05113
05114 vector<Expr> boundVars;
05115 for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
05116 i!=iend; ++i)
05117 boundVars.push_back(addBoundVar(i->first, i->second));
05118
05119 Expr body(parseExpr(e[2]));
05120
05121 Expr res = getEM()->newClosureExpr((kind == FORALL) ? FORALL : EXISTS,
05122 boundVars, body);
05123 return res;
05124 break;
05125 }
05126 default:
05127 DebugAssert(false,
05128 "TheoryQuant::parseExprOp: invalid command or expression: " + e.toString());
05129 break;
05130 }
05131 return e;
05132 }
05133