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 #include "assumptions.h"
00034
00035 using namespace std;
00036 using namespace CVC3;
00037
00038
00039
00040
00041
00042 static const Expr null_expr;
00043 const int FOUND_FALSE = 1;
00044
00045 Trigger::Trigger(TheoryCore* core, Expr e, Polarity pol, std::set<Expr> boundVars){
00046 trig=e ;
00047 polarity=pol;
00048 head=null_expr;
00049 hasRWOp=false;
00050 hasTrans=false;
00051 hasT2=false;
00052 isSimple=false;
00053 isSuperSimple=false;
00054 isMulti=false;
00055 multiIndex = 99999;
00056 multiId = 99999;
00057 for(std::set<Expr>::const_iterator i=boundVars.begin(),iend=boundVars.end(); i!=iend; ++i)
00058 bvs.push_back(*i);
00059 }
00060
00061 bool Trigger::isPos(){
00062 return (Pos==polarity||PosNeg==polarity);
00063 }
00064
00065 bool Trigger::isNeg(){
00066 return (Neg==polarity || PosNeg==polarity);
00067 }
00068
00069 std::vector<Expr> Trigger::getBVs(){
00070 return bvs;
00071 }
00072
00073 Expr Trigger::getEx(){
00074 return trig;
00075 }
00076
00077 void Trigger::setHead(Expr h){
00078 head=h;
00079 }
00080
00081 Expr Trigger::getHead(){
00082 return head;
00083 }
00084
00085 void Trigger::setRWOp(bool b){
00086 hasRWOp =b ;
00087 }
00088
00089 bool Trigger::hasRW(){
00090 return hasRWOp;
00091 }
00092
00093 void Trigger::setTrans(bool b){
00094 hasTrans =b ;
00095 }
00096
00097 bool Trigger::hasTr(){
00098 return hasTrans;
00099 }
00100
00101 void Trigger::setTrans2(bool b){
00102 hasT2 =b ;
00103 }
00104
00105 bool Trigger::hasTr2(){
00106 return hasT2;
00107 }
00108
00109 void Trigger::setSimp(){
00110 isSimple =true ;
00111 }
00112
00113 bool Trigger::isSimp(){
00114 return isSimple;
00115 }
00116
00117 void Trigger::setSuperSimp(){
00118 isSuperSimple =true ;
00119 }
00120
00121 bool Trigger::isSuperSimp(){
00122 return isSuperSimple;
00123 }
00124
00125 void Trigger::setMultiTrig(){
00126 isMulti = true ;
00127 }
00128
00129 bool Trigger::isMultiTrig(){
00130 return isMulti;
00131 }
00132
00133
00134 dynTrig::dynTrig(Trigger t, ExprMap<Expr> b, size_t id)
00135 :trig(t),
00136 univ_id(id),
00137 binds(b)
00138 {}
00139
00140 TheoryQuant::TheoryQuant(TheoryCore* core)
00141 : Theory(core, "Quantified Expressions"),
00142 d_univs(core->getCM()->getCurrentContext()),
00143 d_rawUnivs(core->getCM()->getCurrentContext()),
00144 d_arrayTrigs(core->getCM()->getCurrentContext()),
00145 d_lastArrayPos(core->getCM()->getCurrentContext(), 0 , 0),
00146 d_lastPredsPos(core->getCM()->getCurrentContext(), 0, 0),
00147 d_lastTermsPos(core->getCM()->getCurrentContext(), 0, 0),
00148 d_lastPartPredsPos(core->getCM()->getCurrentContext(), 0, 0),
00149 d_lastPartTermsPos(core->getCM()->getCurrentContext(), 0, 0),
00150 d_univsPartSavedPos(core->getCM()->getCurrentContext(), 0, 0),
00151 d_lastPartLevel(core->getCM()->getCurrentContext(), 0, 0),
00152 d_partCalled(core->getCM()->getCurrentContext(),false,0),
00153 d_maxILReached(core->getCM()->getCurrentContext(),false,0),
00154 d_usefulGterms(core->getCM()->getCurrentContext()),
00155 d_lastUsefulGtermsPos(core->getCM()->getCurrentContext(), 0, 0),
00156 d_savedTermsPos(core->getCM()->getCurrentContext(), 0, 0),
00157 d_univsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
00158 d_rawUnivsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
00159 d_univsPosFull(core->getCM()->getCurrentContext(), 0, 0),
00160 d_univsContextPos(core->getCM()->getCurrentContext(), 0, 0),
00161 d_instCount(core->getCM()->getCurrentContext(), 0,0),
00162 d_contextTerms(core->getCM()->getCurrentContext()),
00163 d_contextCache(core->getCM()->getCurrentContext()),
00164 d_maxQuantInst(&(core->getFlags()["max-quant-inst"].getInt())),
00165 d_useNew(&(core->getFlags()["quant-new"].getBool())),
00166 d_useLazyInst(&(core->getFlags()["quant-lazy"].getBool())),
00167 d_useSemMatch(&(core->getFlags()["quant-sem-match"].getBool())),
00168 d_useCompleteInst(&(core->getFlags()["quant-complete-inst"].getBool())),
00169 d_translate(&(core->getFlags()["translate"].getBool())),
00170
00171
00172 d_useInstLCache(&(core->getFlags()["quant-inst-lcache"].getBool())),
00173 d_useInstGCache(&(core->getFlags()["quant-inst-gcache"].getBool())),
00174 d_useInstThmCache(&(core->getFlags()["quant-inst-tcache"].getBool())),
00175 d_useInstTrue(&(core->getFlags()["quant-inst-true"].getBool())),
00176 d_usePullVar(&(core->getFlags()["quant-pullvar"].getBool())),
00177 d_useExprScore(&(core->getFlags()["quant-score"].getBool())),
00178 d_maxIL(&(core->getFlags()["quant-max-IL"].getInt())),
00179 d_useTrans(&(core->getFlags()["quant-trans3"].getBool())),
00180 d_useTrans2(&(core->getFlags()["quant-trans2"].getBool())),
00181 d_useManTrig(&(core->getFlags()["quant-man-trig"].getBool())),
00182 d_useGFact(&(core->getFlags()["quant-gfact"].getBool())),
00183 d_gfactLimit(&(core->getFlags()["quant-glimit"].getInt())),
00184 d_usePolarity(&(core->getFlags()["quant-polarity"].getBool())),
00185 d_useNewEqu(&(core->getFlags()["quant-eqnew"].getBool())),
00186 d_maxNaiveCall(&(core->getFlags()["quant-naive-num"].getInt())),
00187 d_useNaiveInst(&(core->getFlags()["quant-naive-inst"].getBool())),
00188 d_curMaxExprScore(core->getCM()->getCurrentContext(), (core->getFlags()["quant-max-score"].getInt()),0),
00189 d_arrayIndic(core->getCM()->getCurrentContext()),
00190 d_exprLastUpdatedPos(core->getCM()->getCurrentContext(),0 ,0),
00191 d_trans_found(core->getCM()->getCurrentContext()),
00192 d_trans2_found(core->getCM()->getCurrentContext()),
00193 null_cdlist(core->getCM()->getCurrentContext()),
00194 d_eqsUpdate(core->getCM()->getCurrentContext()),
00195 d_lastEqsUpdatePos(core->getCM()->getCurrentContext(), 0, 0),
00196 d_eqs(core->getCM()->getCurrentContext()),
00197 d_eqs_pos(core->getCM()->getCurrentContext(), 0, 0),
00198 d_allInstCount(core->getStatistics().counter("quantifier instantiations")),
00199 d_allInstCount2(core->getStatistics().counter("quantifier instantiations2")),
00200 d_totalInstCount(core->getStatistics().counter("quant total instantiations")),
00201 d_trueInstCount(core->getStatistics().counter("quant true instantiations")),
00202 d_abInstCount(core->getStatistics().counter("quant abandoned instantiations")),
00203 d_instHistory(core->getCM()->getCurrentContext()),
00204 d_alltrig_list(core->getCM()->getCurrentContext())
00205 {
00206 IF_DEBUG(d_univs.setName("CDList[TheoryQuant::d_univs]");)
00207 vector<int> kinds;
00208 d_instCount = 0;
00209 d_cacheThmPos=0;
00210 d_trans_num=0;
00211 d_trans2_num=0;
00212 d_rules=createProofRules();
00213 kinds.push_back(EXISTS);
00214 kinds.push_back(FORALL);
00215 registerTheory(this, kinds);
00216 d_partCalled=false;
00217 d_offset_multi_trig=2;
00218 d_initMaxScore=(theoryCore()->getFlags()["quant-max-score"].getInt());
00219 for(size_t i=0; i<MAX_TRIG_BVS; i++){
00220 d_mybvs[i] = getEM()->newBoundVarExpr("_genbv", int2string(i), Type::anyType(getEM()));
00221 }
00222 core->addNotifyEq(this, null_expr);
00223 defaultReadExpr = theoryCore()->getEM()->newStringExpr("read");
00224 defaultWriteExpr = theoryCore()->getEM()->newStringExpr("write");
00225 defaultPlusExpr= theoryCore()->getEM()->newStringExpr("+");
00226 defaultMinusExpr= theoryCore()->getEM()->newStringExpr("-");
00227 defaultMultExpr= theoryCore()->getEM()->newStringExpr("*");
00228 defaultDivideExpr= theoryCore()->getEM()->newStringExpr("/");
00229 defaultPowExpr= theoryCore()->getEM()->newStringExpr("pow");
00230
00231 }
00232
00233
00234 TheoryQuant::~TheoryQuant() {
00235 if(d_rules != NULL) delete d_rules;
00236 for(std::map<Type, CDList<size_t>* ,TypeComp>::iterator
00237 it = d_contextMap.begin(), iend = d_contextMap.end();
00238 it!= iend; ++it) {
00239 delete it->second;
00240 free(it->second);
00241 }
00242
00243 }
00244 std::string vectorExpr2string(const std::vector<Expr> & vec){
00245 std::string buf;
00246 for(size_t i=0; i<vec.size(); i++){
00247 buf.append(vec[i].toString());
00248 buf.append(" # ");
00249 }
00250 return buf;
00251 }
00252
00253
00254 Theorem TheoryQuant::rewrite(const Expr& e){
00255
00256
00257 if(e.isForall() || e.isExists() ){
00258 Theorem resThm = d_rules->normalizeQuant(e);
00259
00260 return resThm;
00261 }
00262 else{
00263 if (e.isNot() && e[0].isForall()){
00264
00265 }
00266 else {
00267
00268 }
00269 return reflexivityRule(e);
00270 }
00271 }
00272
00273
00274 int inline TheoryQuant::getExprScore(const Expr& e){
00275 return theoryCore()->getQuantLevelForTerm(e);
00276 }
00277
00278 bool isSysPred(const Expr& e){
00279 return ( isLE(e) || isLT(e) || isGE(e) || isGT(e) || e.isEq());
00280 }
00281
00282 bool canGetHead(const Expr& e){
00283
00284 return (e.getKind() == APPLY
00285 || e.getKind() == READ
00286 || e.getKind() == WRITE
00287 || isPlus(e)
00288 || isMinus(e)
00289 || isMult(e)
00290 || isDivide(e)
00291 || isPow(e)
00292 );
00293 }
00294
00295 bool isSimpleTrig(const Expr& t){
00296 if(!canGetHead(t)) return false;
00297 for(int i = 0; i < t.arity(); i++){
00298 if (t[i].arity()>0 && t[i].containsBoundVar()) return false;
00299 if (BOUND_VAR == t[i].getKind()){
00300 for(int j = 0; j < i; j++){
00301 if(t[i] == t[j]) return false;
00302 }
00303 }
00304 }
00305 return true;
00306 }
00307
00308 bool isSuperSimpleTrig(const Expr& t){
00309 if(!isSimpleTrig(t)) return false;
00310 if(t.getKind() == READ || t.getKind() == WRITE){
00311 return false;
00312 }
00313 for(int i = 0; i < t.arity(); i++){
00314 if (t[i].arity()>0 ) return false;
00315 if (BOUND_VAR != t[i].getKind()){
00316 return false;
00317 }
00318 }
00319 return true;
00320 }
00321
00322
00323 bool usefulInMatch(const Expr& e){
00324 if(e.arity() == 0){
00325 TRACE("usefulInMatch", e.toString()+": ",e.arity(), "");
00326 TRACE("usefulInMatch", e.isRational(), "", "");
00327 }
00328 return ( canGetHead(e) || (isSysPred(e) && (!e.isEq()) ) );
00329 }
00330
00331 void TheoryQuant::setup(const Expr& e) {}
00332
00333 int TheoryQuant::help(int i) {
00334 return d_curMaxExprScore;
00335 }
00336
00337 void TheoryQuant::debug(int i){
00338
00339 cout<<"in debug " << endl;
00340 cout << "max expr score " << d_curMaxExprScore << endl;
00341 cout << "all gterms " << endl;
00342 for(size_t gtermIndex =0; gtermIndex < d_usefulGterms.size() ; gtermIndex++){
00343 cout << gtermIndex << " :: " << getExprScore(d_usefulGterms[gtermIndex]) << " | " << d_usefulGterms[gtermIndex] << endl;
00344 }
00345 cout << " ============= all terms ========================== " << endl;
00346 const CDList<Expr>& allterms = theoryCore()->getTerms();
00347 for(size_t gtermIndex =0; gtermIndex < allterms.size() ; gtermIndex++){
00348 const Expr& curGterm = allterms[gtermIndex];
00349 cout << gtermIndex << " :: " << getExprScore(curGterm) << " | " << curGterm << endl;
00350 cout << "--- ";
00351 if (curGterm.isApply() && curGterm.hasRep()){
00352 Expr curRep = curGterm.getRep().getRHS() ;
00353 if(curRep != curGterm){
00354 cout<<"DIFF " <<curRep << endl;
00355 }
00356 }
00357 else {
00358 cout << "No Rep" ;
00359 }
00360 cout << endl ;
00361
00362 cout << "=== ";
00363 if (curGterm.isApply() && curGterm.hasSig()){
00364 Expr curSig = curGterm.getSig().getRHS() ;
00365 if(curSig != curGterm){
00366 cout<<"DIFF " <<curSig << endl;
00367 }
00368 }
00369 else {
00370 cout << "No Sig" ;
00371 }
00372 cout << endl ;
00373
00374
00375 }
00376 cout << " ============= all preds ========================== " << endl;
00377 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
00378 for(size_t gtermIndex =0; gtermIndex < allpreds.size() ; gtermIndex++){
00379 const Expr& curGterm = allpreds[gtermIndex];
00380 cout << gtermIndex << " :: " << getExprScore(curGterm) << " | " << curGterm << endl;
00381 cout << "--- ";
00382 if (curGterm.isApply() && curGterm.hasRep()){
00383 Expr curRep = curGterm.getRep().getRHS() ;
00384 if(curRep != curGterm){
00385 cout<<"DIFF " <<curRep << endl;
00386 }
00387 }
00388 else {
00389 cout << "No Rep" ;
00390 }
00391 cout << endl ;
00392
00393 cout << "=== ";
00394 if (curGterm.isApply() && curGterm.hasSig()){
00395 Expr curSig = curGterm.getSig().getRHS() ;
00396 if(curSig != curGterm){
00397 cout<<"DIFF " <<curSig << endl;
00398 }
00399 }
00400 else {
00401 cout << "No Sig" ;
00402 }
00403 cout << endl ;
00404 }
00405
00406 cout<<"let us try more"<<endl;
00407
00408
00409
00410 }
00411
00412 void TheoryQuant::update(const Theorem& t, const Expr& e) {
00413
00414 TRACE("quant update", "eqs updated: ", t.getExpr(), "");
00415
00416
00417
00418
00419 d_eqsUpdate.push_back(t);
00420
00421 return;
00422
00423 const Expr& leftTerm = t.getLHS();
00424 const Expr& rightTerm = t.getRHS();
00425
00426
00427
00428
00429
00430
00431
00432
00433
00434
00435
00436
00437
00438
00439
00440
00441
00442
00443
00444
00445
00446
00447
00448
00449
00450
00451
00452
00453
00454
00455
00456
00457
00458
00459
00460
00461
00462
00463
00464
00465 if(false)
00466 {
00467 CDList<Expr>& backL = backList(leftTerm);
00468 CDList<Expr>& forwL = forwList(rightTerm);
00469
00470 size_t backLen = backL.size();
00471 size_t forwLen = forwL.size();
00472 for(size_t i =0; i < backLen; i++){
00473 for(size_t j =0; j < forwLen; j++){
00474
00475 }
00476 }
00477 }
00478 {
00479 CDList<Expr>& backL = backList(rightTerm);
00480 CDList<Expr>& forwL = forwList(leftTerm);
00481 size_t backLen = backL.size();
00482 size_t forwLen = forwL.size();
00483 for(size_t i = 0; i < backLen; i++){
00484 for(size_t j = 0; j < forwLen; j++){
00485
00486 }
00487 }
00488 }
00489
00490 }
00491
00492
00493 std::string TheoryQuant::exprMap2string(const ExprMap<Expr>& vec){
00494 string result;
00495
00496
00497
00498
00499
00500
00501
00502 return result;
00503 }
00504
00505
00506
00507 std::string TheoryQuant::exprMap2stringSimplify(const ExprMap<Expr>& vec){
00508 string result;
00509
00510
00511
00512
00513
00514
00515 result.append("------ end map ------\n");
00516 return result;
00517 }
00518
00519 std::string TheoryQuant::exprMap2stringSig(const ExprMap<Expr>& vec){
00520 string result;
00521
00522
00523
00524
00525
00526
00527
00528
00529
00530
00531
00532
00533 result.append("------ end map ------\n");
00534 return result;
00535 }
00536
00537
00538 void TheoryQuant::simplifyExprMap(ExprMap<Expr>& orgExprMap){
00539 ExprMap<Expr> newExprMap;
00540 for( ExprMap<Expr>::iterator i = orgExprMap.begin(), iend = orgExprMap.end(); i != iend; i++){
00541 newExprMap[(*i).first] = simplifyExpr((*i).second);
00542 }
00543 orgExprMap = newExprMap;
00544 }
00545
00546 void TheoryQuant::simplifyVectorExprMap(vector<ExprMap<Expr> >& orgVectorExprMap){
00547 std::vector<ExprMap<Expr> > newVectorExprMap;
00548 for( size_t orgVectorIndex = 0; orgVectorIndex < orgVectorExprMap.size(); orgVectorIndex++){
00549 ExprMap<Expr> curExprMap = orgVectorExprMap[orgVectorIndex];
00550 simplifyExprMap(curExprMap);
00551 newVectorExprMap.push_back(curExprMap);
00552 }
00553 orgVectorExprMap = newVectorExprMap;
00554 }
00555
00556 static void recursiveGetSubTrig(const Expr& e, std::vector<Expr> & res) {
00557 if(e.getFlag())
00558 return;
00559
00560 if(e.isClosure())
00561 return recursiveGetSubTrig(e.getBody(),res);
00562
00563 if (e.isApply()|| isSysPred(e)){
00564 res.push_back(e);
00565 }
00566 else
00567 if ( e.isTerm() && (!e.isVar()) && (e.getKind()!=RATIONAL_EXPR) ) {
00568 res.push_back(e);
00569 }
00570
00571 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00572 recursiveGetSubTrig(*i,res);
00573 }
00574
00575 e.setFlag();
00576 return ;
00577 }
00578
00579 std::vector<Expr> getSubTrig(const Expr& e){
00580 e.clearFlags();
00581 std::vector<Expr> res;
00582 recursiveGetSubTrig(e,res);
00583 e.clearFlags();
00584 TRACE("getsub","e is ", e.toString(),"");
00585 TRACE("getsub","have ", res.size()," subterms");
00586 return res;
00587 }
00588
00589 static void recGetSubTerms(const Expr& e, std::vector<Expr> & res) {
00590 if(e.getFlag())
00591 return;
00592
00593 if(e.isClosure())
00594 return recGetSubTerms(e.getBody(),res);
00595
00596 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00597 recGetSubTerms(*i,res);
00598 }
00599
00600 res.push_back(e);
00601
00602 e.setFlag();
00603 return ;
00604 }
00605
00606 const std::vector<Expr>& TheoryQuant::getSubTerms(const Expr& e){
00607
00608 ExprMap<std::vector<Expr> >::iterator iter= d_subTermsMap.find(e);
00609 if( d_subTermsMap.end() == iter){
00610 e.clearFlags();
00611 std::vector<Expr> res;
00612 recGetSubTerms(e,res);
00613 e.clearFlags();
00614
00615 TRACE("getsubs", "getsubs, e is: ", e, "");
00616 TRACE("getsubs", "e has ", res.size(), " subterms");
00617
00618 d_subTermsMap[e] = res;
00619 return d_subTermsMap[e];
00620 }
00621 else{
00622 return (*iter).second;
00623 }
00624 }
00625
00626 void TheoryQuant::enqueueInst(const Theorem& univ, const vector<Expr>& bind, const Expr& gterm){
00627 static int max_score =-1;
00628
00629 bool partInst=false;
00630 if(bind.size() < univ.getExpr().getVars().size()){
00631 partInst=false;
00632 TRACE("sendinst","partinst",partInst,"");
00633 }
00634
00635 Expr bind_expr(RAW_LIST, bind, getEM());
00636
00637 if (*d_useInstLCache){
00638 const Expr& e = univ.getExpr();
00639 ExprMap<CDMap<Expr,bool>*>::iterator iterCache = d_bindHistory.find(e);
00640 if (iterCache != d_bindHistory.end()){
00641 CDMap<Expr,bool>* cache = (*iterCache).second;
00642 if(cache->find(bind_expr) !=cache->end()){
00643 return ;
00644 }
00645 else{
00646 (*cache)[bind_expr] = true;
00647 }
00648 }
00649 else{
00650 CDMap<Expr,bool>* new_cache = new(true) CDMap<Expr,bool> (theoryCore()->getCM()->getCurrentContext());
00651 (*new_cache)[bind_expr] = true;
00652 d_bindHistory[e] = new_cache;
00653 }
00654
00655 }
00656
00657 Theorem thm ;
00658 if(null_expr == gterm ){
00659 TRACE("sendinst","gterm",gterm,"");
00660 if(partInst) {
00661 thm = d_rules->partialUniversalInst(univ, bind, 0);
00662 }
00663 else{
00664
00665 thm = d_rules->universalInst(univ, bind, 0, gterm);
00666 }
00667 }
00668 else{
00669 int gscore = theoryCore()->getQuantLevelForTerm(gterm);
00670 if(gscore > max_score){
00671 max_score = gscore;
00672
00673 }
00674 if(partInst) {
00675 thm = d_rules->partialUniversalInst(univ, bind, gscore);
00676 }
00677 else{
00678
00679 thm = d_rules->universalInst(univ, bind, gscore, gterm);
00680 }
00681 }
00682
00683 d_totalInstCount++;
00684 d_totalThmCount[thm.getExpr()]++;
00685 Theorem simpThm = simplify(thm.getExpr());
00686
00687 if(*d_useInstTrue){
00688 Expr res = simpThm.getRHS();
00689 if(res.isTrue()){
00690 d_trueInstCount++;
00691 return;
00692 }
00693 if(res.isFalse() ){
00694 d_thmCount[thm.getExpr()]++;
00695
00696
00697 if(*d_useGFact || d_thmCount[thm.getExpr()] > *d_gfactLimit){
00698
00699
00700 enqueueFact(thm);
00701 }
00702 else{
00703 enqueueFact(thm);
00704 }
00705
00706
00707
00708 d_allInstCount++;
00709 d_instThisRound++;
00710
00711 throw FOUND_FALSE;
00712 }
00713 }
00714
00715 d_simplifiedThmQueue.push(thm);
00716
00717 TRACE("quant sendinst", "= gterm:",gterm, "");
00718
00719 TRACE("quant sendinst", "= add fact simp: ", simplifyExpr(thm.getExpr()), "");
00720 TRACE("quant sendinst", "= add fact org: ", thm.getExpr(), "");
00721 TRACE("quant sendinst", "= add fact from: ", univ.getExpr(), "\n===: "+vectorExpr2string(bind));
00722 }
00723
00724
00725
00726 void TheoryQuant::enqueueInst(size_t univ_id , const std::vector<Expr>& orgBind, const Expr& gterm){
00727
00728 TRACE("quant sendinst", "= begin univ id: ", univ_id, "");
00729 TRACE("quant sendinst", "= begin bind: ", vectorExpr2string(orgBind), "");
00730 TRACE("quant sendinst", "= begin gterm: ", gterm, "");
00731 const Theorem& univ = d_univs[univ_id];
00732
00733
00734
00735
00736 bool partInst=false;
00737 if(orgBind.size() < univ.getExpr().getVars().size()){
00738 partInst=false;
00739 TRACE("sendinst","partinst",partInst,"");
00740 }
00741
00742 vector<Expr> simpBind(orgBind);
00743 for(size_t orgBindIndex = 0; orgBindIndex < orgBind.size(); orgBindIndex++){
00744 simpBind [orgBindIndex] = simplifyExpr(orgBind[orgBindIndex]);
00745 }
00746
00747 Expr orgBindList(RAW_LIST, orgBind, getEM());
00748 Expr simpBindList(RAW_LIST, simpBind, getEM());
00749
00750
00751
00752
00753
00754
00755
00756 vector<Expr> bind(simpBind);
00757 Expr bind_expr(simpBindList);
00758
00759
00760
00761
00762 TRACE("quant sendinst", "==add fact from= ", univ.getExpr(), "\n===: "+vectorExpr2string(bind));
00763
00764 if (*d_useInstLCache){
00765 const Expr& e = univ.getExpr();
00766 ExprMap<CDMap<Expr,bool>*>::iterator iterCache = d_bindHistory.find(e);
00767 if (iterCache != d_bindHistory.end()){
00768 CDMap<Expr,bool>* cache = (*iterCache).second;
00769 if(cache->find(bind_expr) != cache->end()){
00770
00771 return ;
00772 }
00773 else{
00774 (*cache)[bind_expr] = true;
00775 }
00776 }
00777 else{
00778 CDMap<Expr,bool>* new_cache = new(true) CDMap<Expr,bool> (theoryCore()->getCM()->getCurrentContext());
00779 (*new_cache)[bind_expr] = true;
00780 d_bindHistory[e] = new_cache;
00781 }
00782 }
00783
00784 if (*d_useInstGCache){
00785 const Expr& e = univ.getExpr();
00786 ExprMap<std::hash_map<Expr,bool>*>::iterator iterCache = d_bindGlobalHistory.find(e);
00787 if (iterCache != d_bindGlobalHistory.end()){
00788 std::hash_map<Expr,bool>* cache = (*iterCache).second;
00789 if(cache->find(bind_expr) != cache->end()){
00790
00791
00792
00793
00794
00795
00796
00797
00798
00799
00800
00801
00802
00803 d_allInstCount2++;
00804 return ;
00805 }
00806
00807
00808
00809
00810
00811
00812
00813
00814
00815
00816
00817
00818
00819 }
00820 }
00821
00822 Theorem thm ;
00823
00824 if (*d_useInstThmCache){
00825 const Expr& e = univ.getExpr();
00826 ExprMap<std::hash_map<Expr,Theorem>* >::iterator iterCache = d_bindGlobalThmHistory.find(e);
00827 if (iterCache != d_bindGlobalThmHistory.end()){
00828 std::hash_map<Expr,Theorem>* cache = (*iterCache).second;
00829 std::hash_map<Expr,Theorem>::iterator thm_iter = cache->find(bind_expr);
00830
00831 if(thm_iter != cache->end()){
00832 thm = thm_iter->second;
00833 }
00834 else{
00835 {
00836 if(null_expr == gterm ){
00837 TRACE("sendinst","gterm",gterm,"");
00838 if(partInst) {
00839 thm = d_rules->partialUniversalInst(univ, bind, 0);
00840 }
00841 else{
00842
00843 thm = d_rules->universalInst(univ, bind, 0, gterm);
00844 }
00845 }
00846 else{
00847 int gscore = theoryCore()->getQuantLevelForTerm(gterm);
00848 if(partInst) {
00849 thm = d_rules->partialUniversalInst(univ, bind, gscore);
00850 }
00851 else{
00852
00853 thm = d_rules->universalInst(univ, bind, gscore, gterm);
00854 }
00855 }
00856 }
00857
00858 (*cache)[bind_expr] = thm;
00859 d_allInstCount2++;
00860 }
00861 }
00862 else{
00863 {
00864 if(null_expr == gterm ){
00865 TRACE("sendinst","gterm",gterm,"");
00866 if(partInst) {
00867 thm = d_rules->partialUniversalInst(univ, bind, 0);
00868 }
00869 else{
00870
00871 thm = d_rules->universalInst(univ, bind, 0, gterm);
00872 }
00873 }
00874 else{
00875 int gscore = theoryCore()->getQuantLevelForTerm(gterm);
00876 if(partInst) {
00877 thm = d_rules->partialUniversalInst(univ, bind, gscore);
00878 }
00879 else{
00880
00881 thm = d_rules->universalInst(univ, bind, gscore, gterm);
00882 }
00883 }
00884 }
00885
00886 std::hash_map<Expr,Theorem>* new_cache = new std::hash_map<Expr,Theorem> ;
00887 (*new_cache)[bind_expr] = thm;
00888 d_bindGlobalThmHistory[e] = new_cache;
00889 d_allInstCount2++;
00890 }
00891 }
00892 else{
00893 if(null_expr == gterm ){
00894 TRACE("sendinst","gterm",gterm,"");
00895 if(partInst) {
00896 thm = d_rules->partialUniversalInst(univ, bind, 0);
00897 }
00898 else{
00899
00900 thm = d_rules->universalInst(univ, bind, 0, gterm);
00901 }
00902 }
00903 else{
00904 int gscore = theoryCore()->getQuantLevelForTerm(gterm);
00905
00906
00907
00908
00909
00910
00911 if(partInst) {
00912 thm = d_rules->partialUniversalInst(univ, bind, gscore);
00913 }
00914 else{
00915
00916 thm = d_rules->universalInst(univ, bind, gscore, gterm);
00917 }
00918 }
00919 }
00920
00921 d_totalInstCount++;
00922 d_totalThmCount[thm.getExpr()]++;
00923 Theorem simpThm = simplify(thm.getExpr());
00924
00925 if(*d_useInstTrue){
00926 Expr res = simpThm.getRHS();
00927 if(res.isTrue()){
00928 d_trueInstCount++;
00929
00930
00931
00932
00933
00934
00935 return;
00936 }
00937 if(res.isFalse() ){
00938 d_thmCount[thm.getExpr()]++;
00939
00940
00941 if(*d_useGFact || d_thmCount[thm.getExpr()] > *d_gfactLimit ){
00942
00943
00944
00945 enqueueFact(thm);
00946 }
00947 else{
00948 enqueueFact(thm);
00949 }
00950
00951
00952
00953 d_allInstCount++;
00954 d_instThisRound++;
00955
00956
00957
00958
00959
00960
00961
00962 throw FOUND_FALSE;
00963 }
00964 }
00965
00966 d_simplifiedThmQueue.push(thm);
00967 d_gUnivQueue.push(univ);
00968 d_gBindQueue.push(bind_expr);
00969
00970
00971 TRACE("quant sendinst", "=gterm: ",gterm, "");
00972
00973
00974
00975
00976
00977
00978
00979
00980 TRACE("quant sendinst", "= add fact simp: ", simplifyExpr(thm.getExpr()), "");
00981 TRACE("quant sendinst", "= add fact org: ", thm.getExpr(), "");
00982 TRACE("quant sendinst", "= add fact from: ", univ.getExpr(), "\n===: "+vectorExpr2string(bind));
00983 TRACE("quant sendinst", "= end === ", "=========", "============");
00984 }
00985
00986
00987 void TheoryQuant::enqueueInst(const Theorem& univ, Trigger& trig, const std::vector<Expr>& binds, const Expr& gterm) {
00988 return enqueueInst(univ,binds,gterm);
00989 }
00990
00991 int TheoryQuant::sendInstNew(){
00992 int resNum = 0 ;
00993
00994 while(!d_simplifiedThmQueue.empty()){
00995 const Theorem thm = d_simplifiedThmQueue.front();
00996 d_simplifiedThmQueue.pop();
00997
00998 d_allInstCount++;
00999 d_instThisRound++;
01000 resNum++;
01001 if (*d_useInstGCache){
01002 const Theorem & univ = d_gUnivQueue.front();
01003 const Expr & bind = d_gBindQueue.front();
01004
01005 const Expr& e = univ.getExpr();
01006 ExprMap<std::hash_map<Expr,bool>*>::iterator iterCache = d_bindGlobalHistory.find(e);
01007 if (iterCache != d_bindGlobalHistory.end()){
01008 std::hash_map<Expr,bool>* cache = (*iterCache).second;
01009 (*cache)[bind] = true;
01010 }
01011 else{
01012 std::hash_map<Expr,bool>* new_cache = new std::hash_map<Expr,bool> ;
01013 (*new_cache)[bind] = true;
01014 d_bindGlobalHistory[e] = new_cache;
01015 }
01016 }
01017 d_thmCount[thm.getExpr()]++;
01018
01019 if(*d_useGFact || d_thmCount[thm.getExpr()] > *d_gfactLimit ){
01020
01021 enqueueFact(thm);
01022 }
01023 else{
01024 enqueueFact(thm);
01025 }
01026
01027
01028 }
01029
01030 return resNum;
01031 }
01032
01033 void TheoryQuant::addNotify(const Expr& e){}
01034
01035 int recursiveExprScore(const Expr& e) {
01036 int res=0;
01037 DebugAssert(!(e.isClosure()), "exprScore called on closure");
01038
01039 if(e.arity()== 0){
01040 res = 0;
01041 }
01042 else{
01043 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
01044 res += recursiveExprScore(*i);
01045 }
01046 }
01047 res++;
01048 return res;
01049 }
01050
01051
01052 int exprScore(const Expr& e){
01053 return recursiveExprScore(e);
01054 }
01055
01056 Expr TheoryQuant::getHeadExpr(const Expr& e){
01057 if (e.getKind() == APPLY){
01058 return e.getOp().getExpr();
01059 }
01060
01061 if ( READ == e.getKind() ){
01062 return defaultReadExpr;
01063 }
01064 if ( WRITE == e.getKind() ){
01065 return defaultWriteExpr;
01066 }
01067 if (isPlus(e)){
01068 return defaultPlusExpr;
01069 }
01070 if (isMinus(e)){
01071 return defaultMinusExpr;
01072 }
01073 if (isMult(e)){
01074 return defaultMultExpr;
01075 }
01076 if (isDivide(e)){
01077 return defaultDivideExpr;
01078 }
01079 if (isPow(e)){
01080 return defaultPowExpr;
01081 }
01082
01083
01084
01085
01086
01087
01088
01089
01090
01091
01092
01093
01094
01095
01096 return null_expr;
01097 }
01098
01099 Expr TheoryQuant::getHead(const Expr& e) {
01100 return getHeadExpr(e);
01101 }
01102
01103
01104 static bool recursiveGetBoundVars(const Expr& e, std::set<Expr>& result) {
01105 bool res(false);
01106 if(e.getFlag()){
01107 return e.containsBoundVar();
01108 }
01109 else if(e.isClosure()){
01110 res = recursiveGetBoundVars(e.getBody(),result);
01111 }
01112 else if (BOUND_VAR == e.getKind() ){
01113 result.insert(e);
01114 e.setContainsBoundVar();
01115 res = true;
01116 }
01117 else {
01118 res = false;
01119 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i){
01120 if(recursiveGetBoundVars(*i,result)){
01121 res = true;
01122 }
01123 }
01124 }
01125
01126 e.setFlag();
01127
01128 if(res) {
01129 e.setContainsBoundVar();
01130 }
01131
01132 return res;
01133 }
01134
01135
01136
01137 std::set<Expr> getBoundVars(const Expr& e){
01138
01139
01140
01141
01142
01143
01144
01145
01146
01147
01148
01149
01150
01151 e.clearFlags();
01152 std::set<Expr> result ;
01153 recursiveGetBoundVars(e,result);
01154 e.clearFlags();
01155
01156 return result;
01157 }
01158
01159 void findPolarity(const Expr& e, ExprMap<Polarity>& res, Polarity pol){
01160 if(!e.getType().isBool()) return;
01161
01162 if(res.count(e)>0){
01163 if ((Neg == res[e] && Pos == pol) || (Neg == res[e] && Pos == pol) ){
01164 res[e]=PosNeg;
01165 }
01166 }
01167 else{
01168 res[e]=pol;
01169 }
01170
01171 TRACE("find-polarity", e, "has ", (int)pol);
01172
01173 if(PosNeg==pol){
01174 for(int i=0; i<e.arity(); i++){
01175 findPolarity(e[i], res, pol);
01176 }
01177 }
01178 else{
01179 Polarity neg_pol=Ukn;
01180 if(Pos == pol) {
01181 neg_pol = Neg;
01182 }
01183 else if(Neg == pol){
01184 neg_pol = Pos;
01185 }
01186
01187 if(e.isImpl()){
01188 findPolarity(e[0], res, neg_pol);
01189 findPolarity(e[1], res, pol);
01190 }
01191 else if(e.isAnd() || e.isOr()){
01192 for(int i=0; i<e.arity(); i++){
01193 findPolarity(e[i], res, pol);
01194 }
01195 }
01196 else if(e.isNot()){
01197 findPolarity(e[0], res, neg_pol);
01198 }
01199 else if(e.isITE()){
01200 findPolarity(e[0], res, PosNeg);
01201 findPolarity(e[1], res, pol);
01202 findPolarity(e[2], res, pol);
01203 }
01204 else if(e.isClosure()){
01205 findPolarity(e.getBody(), res, pol);
01206 }
01207 else if(e.isIff()){
01208 findPolarity(e[0], res, PosNeg);
01209 findPolarity(e[1], res, PosNeg);
01210 }
01211 else if(e.isXor()){
01212 findPolarity(e[0], res, neg_pol);
01213 findPolarity(e[1], res, neg_pol);
01214 }
01215 else if(e.isAtomicFormula()){
01216 return;
01217 }
01218 else{
01219
01220 }
01221 }
01222 }
01223
01224 bool isUniterpFunc(const Expr & e){
01225 if ( e.isApply() && e.getOpKind() == UFUNC){
01226 return true;
01227 }
01228 return false;
01229 }
01230
01231
01232
01233
01234
01235
01236 bool isGround(const Expr& e){
01237
01238
01239 return ! e.containsBoundVar();
01240 }
01241
01242 Expr CompleteInstPreProcessor::pullVarOut(const Expr& thm_expr){
01243
01244 const Expr outBody = thm_expr.getBody();
01245
01246
01247
01248
01249
01250
01251
01252 if (thm_expr.isForall()){
01253 if((outBody.isNot() && outBody[0].isAnd() && outBody[0][1].isExists())){
01254
01255 vector<Expr> bVarsOut = thm_expr.getVars();
01256
01257 const Expr innerExists =outBody[0][1];
01258 const Expr innerBody = innerExists.getBody();
01259 vector<Expr> bVarsIn = innerExists.getVars();
01260
01261 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
01262 bVarsOut.push_back(*i);
01263 }
01264
01265 Expr newbody;
01266
01267 newbody=(outBody[0][0].notExpr()).orExpr(innerBody.notExpr());
01268
01269 Expr newQuantExpr;
01270 newQuantExpr = d_theoryCore->getEM()->newClosureExpr(FORALL, bVarsOut, newbody);
01271
01272 return newQuantExpr ;
01273 }
01274
01275 else if ((outBody.isAnd() && outBody[1].isForall()) ||
01276 (outBody.isImpl() && outBody[1].isForall())){
01277
01278 vector<Expr> bVarsOut = thm_expr.getVars();
01279
01280 const Expr innerForall=outBody[1];
01281 const Expr innerBody = innerForall.getBody();
01282 vector<Expr> bVarsIn = innerForall.getVars();
01283
01284 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
01285 bVarsOut.push_back(*i);
01286 }
01287
01288
01289 Expr newbody;
01290 if(outBody.isAnd()){
01291 newbody=outBody[0].andExpr(innerBody);
01292 }
01293 else if(outBody.isImpl()){
01294 newbody=outBody[0].impExpr(innerBody);
01295 }
01296
01297 Expr newQuantExpr;
01298 newQuantExpr = d_theoryCore->getEM()->newClosureExpr(FORALL, bVarsOut, newbody);
01299
01300 return(newQuantExpr);
01301 }
01302 return thm_expr;
01303 }
01304
01305 else if (thm_expr.isExists()){
01306 if ((outBody.isAnd() && outBody[1].isExists()) ||
01307 (outBody.isImpl() && outBody[1].isExists())){
01308
01309 vector<Expr> bVarsOut = thm_expr.getVars();
01310
01311 const Expr innerExists = outBody[1];
01312 const Expr innerBody = innerExists.getBody();
01313 vector<Expr> bVarsIn = innerExists.getVars();
01314
01315 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
01316 bVarsOut.push_back(*i);
01317 }
01318
01319 Expr newbody;
01320 if(outBody.isAnd()){
01321 newbody=outBody[0].andExpr(innerBody);
01322 }
01323 else if(outBody.isImpl()){
01324 newbody=outBody[0].impExpr(innerBody);
01325 }
01326
01327 Expr newQuantExpr;
01328 newQuantExpr = d_theoryCore->getEM()->newClosureExpr(EXISTS, bVarsOut, newbody);
01329
01330 return newQuantExpr;
01331 }
01332 }
01333 return thm_expr;
01334 }
01335
01336
01337 CompleteInstPreProcessor::CompleteInstPreProcessor(TheoryCore * core, QuantProofRules* quant_rule):
01338 d_theoryCore(core),
01339 d_quant_rules(quant_rule)
01340 {}
01341
01342
01343 void CompleteInstPreProcessor::collectHeads(const Expr& assert, set<Expr>& heads){
01344 if ( ! assert.getType().isBool()){
01345 return;
01346 }
01347 else if ( ! assert.isAbsAtomicFormula()){
01348 for (int i = 0 ; i < assert.arity(); i++){
01349 collectHeads(assert[i], heads);
01350 }
01351 return;
01352 }
01353 else if (assert.isClosure()){
01354 collectHeads(assert.getBody(), heads);
01355 }
01356 else if (assert.isAtomicFormula()){
01357 if (isUniterpFunc(assert)){
01358 heads.insert(assert.getOp().getExpr());
01359 }
01360 }
01361 else{
01362
01363 }
01364 }
01365
01366 bool CompleteInstPreProcessor::isMacro(const Expr& assert){
01367 if (d_is_macro_def.count(assert) > 0 ) {
01368 return true;
01369 }
01370
01371 if (assert.isForall()){
01372 Expr body = assert.getBody();
01373 if (body.isIff()){
01374 Expr right = body[0];
01375 Expr left = body[1];
01376 if ((isUniterpFunc(right) && left.isForall())
01377 || (right.isForall() && isUniterpFunc(left) )){
01378 Expr macro_lhs ;
01379 Expr macro_def;
01380 if (isUniterpFunc(right)){
01381 macro_lhs = right;
01382 macro_def = left;
01383 }
01384 else{
01385 macro_lhs = left;
01386 macro_def = right;
01387 }
01388
01389 Expr test_def_exists = d_theoryCore->getEM()->newClosureExpr(EXISTS, assert.getVars(), macro_def);
01390
01391 Expr test_def_sko = d_theoryCore->getCommonRules()->skolemize(test_def_exists);
01392
01393 if (isGoodQuant(test_def_sko)){
01394 Expr macro_head = macro_lhs.getOp().getExpr();
01395 set<Expr> heads_set;
01396 collectHeads(macro_def, heads_set);
01397 if (heads_set.count(macro_head) <= 0 ){
01398 d_is_macro_def[assert] = true;
01399 d_macro_quant[macro_head] = assert;
01400 d_macro_def[macro_head] = macro_def;
01401 d_macro_lhs[macro_head] = macro_lhs;
01402 return true;
01403 }
01404 }
01405 else {
01406
01407 }
01408 }
01409 }
01410 }
01411 return false;
01412 }
01413
01414 bool CompleteInstPreProcessor::hasMacros(const vector<Expr>& asserts){
01415 bool has_macros = false;
01416 for (size_t i = 0 ; i < asserts.size(); i++){
01417 if (isMacro(asserts[i])){
01418 has_macros = true;
01419 }
01420 }
01421 return has_macros;
01422 }
01423
01424
01425 Expr CompleteInstPreProcessor::substMacro(const Expr& old){
01426 Expr head = old.getOp().getExpr();
01427
01428 DebugAssert(d_macro_lhs.count(head)>0, "macro lhs not found");
01429 DebugAssert(d_macro_def.count(head)>0, "macro def not found");
01430 DebugAssert(d_macro_quant.count(head)>0, "macro quant not found");
01431
01432 Expr macro_lhs = d_macro_lhs[head];
01433 Expr macro_def = d_macro_def[head];
01434 Expr macro_quant = d_macro_quant[head];
01435
01436 DebugAssert(head == macro_lhs.getOp().getExpr(), "impossible in substMacro");
01437
01438 ExprMap<Expr> binding;
01439 for (int i = 0; i < macro_lhs.arity(); i++){
01440 if (macro_lhs[i].isBoundVar()){
01441 binding[macro_lhs[i]] = old[i];
01442 }
01443 }
01444
01445 vector<Expr> quant_vars = macro_quant.getVars();
01446
01447 vector<Expr> gterms;
01448 for (size_t i = 0 ; i < binding.size(); i++){
01449 gterms.push_back(binding[quant_vars[i]]);
01450 }
01451
01452 return macro_def.substExpr(quant_vars,gterms);
01453 }
01454
01455 Expr CompleteInstPreProcessor::simplifyEq(const Expr& assert){
01456 if ( ! assert.getType().isBool()){
01457 return assert;
01458 }
01459 else if ( ! assert.isAbsAtomicFormula()){
01460 vector<Expr> children ;
01461 for (int i = 0 ; i < assert.arity(); i++){
01462 children.push_back(simplifyEq(assert[i]));
01463 }
01464 return Expr(assert.getOp(),children);
01465 }
01466 else if (assert.isClosure()){
01467 Expr new_body = simplifyEq(assert.getBody());
01468 if (assert.isForall()){
01469 d_theoryCore->getEM()->newClosureExpr(FORALL, assert.getVars(), new_body);
01470 }
01471 else if (assert.isExists()){
01472 d_theoryCore->getEM()->newClosureExpr(EXISTS, assert.getVars(), new_body);
01473 }
01474 else{
01475 DebugAssert(false, "impossible case in recInstMacros");
01476 }
01477 }
01478 else if (assert.isAtomicFormula()){
01479 if (assert.isEq() && assert[0] == assert[1]){
01480 return d_theoryCore->trueExpr();
01481 }
01482 else {
01483 return assert;
01484 }
01485 }
01486 cout <<assert<<endl;
01487 DebugAssert(false, "impossible case in simplifyEq");
01488 return assert;
01489 }
01490
01491
01492 Expr CompleteInstPreProcessor::recInstMacros(const Expr& assert){
01493 if ( ! assert.getType().isBool()){
01494 return assert;
01495 }
01496 else if ( ! assert.isAbsAtomicFormula()){
01497 vector<Expr> children ;
01498 for (int i = 0 ; i < assert.arity(); i++){
01499 children.push_back(recInstMacros(assert[i]));
01500 }
01501 return Expr(assert.getOp(),children);
01502 }
01503 else if (assert.isClosure()){
01504 Expr new_body = recInstMacros(assert.getBody());
01505 if (assert.isForall()){
01506 d_theoryCore->getEM()->newClosureExpr(FORALL, assert.getVars(), new_body);
01507 }
01508 else if (assert.isExists()){
01509 d_theoryCore->getEM()->newClosureExpr(EXISTS, assert.getVars(), new_body);
01510 }
01511 else{
01512 DebugAssert(false, "impossible case in recInstMacros");
01513 }
01514 }
01515 else if (assert.isAtomicFormula()){
01516
01517 if (isUniterpFunc(assert)){
01518 Expr assert_op = assert.getOp().getExpr();
01519 if ( d_macro_def.count(assert_op) > 0 ){
01520 return substMacro(assert);
01521 }
01522 else{
01523 return assert;
01524 }
01525 }
01526 else {
01527 return assert;
01528 }
01529 }
01530
01531 DebugAssert(false, "impossible case in recInstMacors");
01532 return assert;
01533
01534 }
01535
01536
01537 Expr CompleteInstPreProcessor::instMacros(const Expr& assert, const Expr macro_quant_sub ){
01538
01539 if (isMacro(assert)){
01540 return macro_quant_sub;
01541 }
01542
01543 return recInstMacros(assert);
01544 }
01545
01546
01547 bool CompleteInstPreProcessor::isShield(const Expr& e){
01548 if (isGround(e)){
01549 return true;
01550 }
01551 else if (isUniterpFunc(e) && e.arity() > 0 ){
01552 for (int i = 0; i<e.arity(); i++){
01553
01554 if ( e[i].containsBoundVar() && ( ! e[i].isBoundVar() )){
01555 return false;
01556 }
01557 }
01558 return true;
01559 }
01560 else if (e.getKind() == READ){
01561 if ( isShield(e[0])
01562
01563 && (e[1].isBoundVar() || isGround(e[1]))){
01564 return true;
01565 }
01566 else {
01567 return false;
01568 }
01569 }
01570 else if (e.getKind() == WRITE){
01571 if ( isShield( e[0] )
01572
01573 && (e[1].isBoundVar() || isGround( e[1] ))
01574 && ( isGround( e[2] ))){
01575 return true;
01576 }
01577 else {
01578 return false;
01579 }
01580 }
01581 else if (e.arity() > 0 ){
01582 for (int i = 0; i<e.arity(); i++){
01583 if (!isShield(e[i])){
01584 return false;
01585 }
01586 }
01587 return true;
01588 }
01589 else if (e.arity () == 0){
01590 return true;
01591 }
01592 DebugAssert(false, "impossible case in isShield");
01593 return false;
01594 }
01595
01596 void findPolarityAtomic(const Expr& e, ExprMap<Polarity>& res, Polarity pol){
01597 if(!e.getType().isBool()) return;
01598
01599 if(res.count(e)>0){
01600 if ((Neg == res[e] && Pos == pol) || (Neg == res[e] && Pos == pol) ){
01601 res[e]=PosNeg;
01602 }
01603 }
01604 else{
01605 res[e]=pol;
01606 }
01607
01608
01609
01610 if(PosNeg == pol){
01611 for(int i=0; i<e.arity(); i++){
01612 findPolarityAtomic(e[i], res, pol);
01613 }
01614 }
01615 else{
01616 Polarity neg_pol=Ukn;
01617 if(Pos == pol) {
01618 neg_pol = Neg;
01619 }
01620 else if(Neg == pol){
01621 neg_pol = Pos;
01622 }
01623
01624 if(e.isImpl()){
01625 findPolarityAtomic(e[0], res, neg_pol);
01626 findPolarityAtomic(e[1], res, pol);
01627 }
01628 else if(e.isAnd() || e.isOr()){
01629 for(int i=0; i<e.arity(); i++){
01630 findPolarityAtomic(e[i], res, pol);
01631 }
01632 }
01633 else if(e.isNot()){
01634 findPolarityAtomic(e[0], res, neg_pol);
01635 }
01636 else if(e.isITE()){
01637 findPolarityAtomic(e[0], res, PosNeg);
01638 findPolarityAtomic(e[1], res, pol);
01639 findPolarityAtomic(e[2], res, pol);
01640 }
01641 else if(e.isClosure()){
01642
01643
01644
01645 }
01646 else if(e.isIff()){
01647 findPolarityAtomic(e[0], res, PosNeg);
01648 findPolarityAtomic(e[1], res, PosNeg);
01649 }
01650 else if(e.isXor()){
01651 findPolarityAtomic(e[0], res, neg_pol);
01652 findPolarityAtomic(e[1], res, neg_pol);
01653 }
01654 else if(e.isAtomicFormula()){
01655 return;
01656 }
01657 else{
01658 DebugAssert(false, "Error in find polarity in "+e.toString());
01659 }
01660 }
01661 }
01662
01663 Expr CompleteInstPreProcessor::recSkolemize(const Expr& e, ExprMap<Polarity>& pol_map){
01664
01665 if ( ! e.getType().isBool()){
01666 return e;
01667 }
01668 else if (e.isClosure()){
01669 if (e.isForall()) {
01670 return e;
01671 }
01672 else if (e.isExists() && Pos == pol_map[e]){
01673 Expr new_body = recSkolemize(e.getBody(), pol_map);
01674 Expr new_quant = d_theoryCore->getEM()->newClosureExpr(EXISTS, e.getVars(), new_body);
01675 return d_theoryCore->getCommonRules()->skolemize(new_quant);
01676 }
01677 }
01678 else if (e.arity() > 0 ) {
01679 vector<Expr> children;
01680 for (int i = 0 ; i < e.arity(); i++){
01681 Expr new_child = recSkolemize(e[i], pol_map);
01682 if (new_child.isNot() && new_child[0].isNot()){
01683 children.push_back(new_child[0][0]);
01684 }
01685 else{
01686 children.push_back(new_child);
01687 }
01688 }
01689 Expr new_expr = Expr(e.getOp(), children);
01690 if (new_expr.isNot() && new_expr[0].isNot()){
01691 return new_expr[0][0];
01692 }
01693 else {
01694 return new_expr;
01695 }
01696 }
01697
01698 return e;
01699 }
01700
01701 Expr CompleteInstPreProcessor::simplifyQuant(const Expr& e){
01702
01703 Expr pos_expr = rewriteNot(e);
01704 TRACE("simp-quant", e , "\n ---rewriteNot---> \n", pos_expr);
01705
01706 Expr next_expr;
01707 if(e.isForall()){
01708 Theorem atoa = d_theoryCore->getCommonRules()->assumpRule(pos_expr);
01709 Theorem packVarThm = d_quant_rules->packVar(atoa);
01710 next_expr = packVarThm.getExpr();
01711 }
01712 else{
01713 next_expr = pos_expr;
01714 }
01715
01716 ExprMap<Polarity> pol_map;
01717
01718 findPolarity(next_expr, pol_map, Pos);
01719
01720 Expr ret = recSkolemize(next_expr, pol_map);
01721 TRACE("simp-quant", e , "\n ---skolemize---> \n", ret);
01722 return ret;
01723 }
01724
01725
01726 Expr CompleteInstPreProcessor::rewriteNot(const Expr& e){
01727 ExprMap<Polarity> pol_map;
01728 findPolarity(e, pol_map, Pos);
01729 set<Expr> t = getBoundVars(e);
01730 return recRewriteNot(e, pol_map);
01731 }
01732
01733 Expr CompleteInstPreProcessor::recRewriteNot(const Expr & e, ExprMap<Polarity>& pol_map){
01734 if ( ! e.getType().isBool()){
01735 return e;
01736 }
01737
01738 if (isGround(e)){
01739 return e;
01740 }
01741
01742 if (e.isClosure()){
01743 DebugAssert(pol_map.find(e) != pol_map.end(), "cannot find polarity" );
01744 if ( Neg == pol_map[e]){
01745 Expr body = recRewriteNot(e.getBody(), pol_map);
01746 Expr new_body = body.notExpr();
01747 Kind new_kind = e.isForall() ? EXISTS : FORALL;
01748 Expr new_quant = d_theoryCore->getEM()->newClosureExpr(new_kind,e.getVars(),new_body);
01749 Expr new_expr = new_quant.notExpr();
01750 return new_expr;
01751 }
01752 else {
01753
01754
01755 return e;
01756 }
01757 }
01758 else if (e.arity() > 0 ) {
01759 vector<Expr> children;
01760
01761 for (int i = 0 ; i < e.arity(); i++){
01762 Expr new_child = recRewriteNot(e[i], pol_map);
01763 if (new_child.isNot() && new_child[0].isNot()){
01764 children.push_back(new_child[0][0]);
01765 }
01766 else{
01767 children.push_back(new_child);
01768 }
01769 }
01770
01771 Expr new_expr = Expr(e.getOp(), children);
01772 if (new_expr.isNot() && new_expr[0].isNot()){
01773 return new_expr[0][0];
01774 }
01775 else {
01776 return new_expr;
01777 }
01778 }
01779 else if (0 == e.arity() ){
01780 return e;
01781 }
01782
01783 DebugAssert(false, "impossible in rewriteNot");
01784 return e;
01785 }
01786
01787 void CompleteInstPreProcessor::addIndex(const Expr& e){
01788 if ( ! isInt(e.getType())) return;
01789 d_allIndex.insert(d_theoryCore->simplifyExpr(e));
01790 }
01791
01792 Expr CompleteInstPreProcessor::plusOne(const Expr& e){
01793 Expr one = d_theoryCore->getEM()->newRatExpr(1);
01794 return Expr(PLUS, e, one);
01795 }
01796
01797 Expr CompleteInstPreProcessor::minusOne(const Expr& e){
01798 Expr one = d_theoryCore->getEM()->newRatExpr(1);
01799 return Expr(MINUS, e, one);
01800 }
01801
01802 void CompleteInstPreProcessor::collect_shield_index(const Expr& e){
01803 if (isUniterpFunc(e) && e.arity() > 0 ){
01804 for (int i = 0; i<e.arity(); i++){
01805 if ( isGround(e[i])){
01806 addIndex(e[i]);
01807 }
01808 }
01809 }
01810 else if (e.getKind() == READ){
01811 collect_shield_index(e[0]);
01812 if (isGround(e[1])){
01813 addIndex(e[1]);
01814 }
01815 }
01816 else if (e.getKind() == WRITE){
01817 collect_shield_index(e[0]);
01818 if ( isGround( e[1] )){
01819 addIndex(e[1]);
01820 addIndex(plusOne(e[1]));
01821 addIndex(minusOne(e[1]));
01822 }
01823 }
01824 else if (e.arity() > 0 ){
01825 for (int i = 0; i<e.arity(); i++){
01826 collect_shield_index(e[i]);
01827 }
01828 }
01829 }
01830
01831 void CompleteInstPreProcessor::collect_forall_index(const Expr& forall_quant){
01832 ExprMap<Polarity> cur_expr_pol;
01833 findPolarity(forall_quant, cur_expr_pol, Pos);
01834
01835 for (ExprMap<Polarity>::iterator i = cur_expr_pol.begin(), iend = cur_expr_pol.end(); i != iend ; i++){
01836 Expr cur_expr = i->first;
01837 Polarity pol = i->second;
01838
01839 if (isLE(cur_expr)){
01840 const Expr& left = cur_expr[0];
01841 const Expr& right = cur_expr[1];
01842 if (left.isBoundVar() && isGround(right)){
01843 if (Pos == pol || PosNeg == pol){
01844 addIndex(plusOne(right));
01845 }
01846 if (Neg == pol || PosNeg == pol){
01847 addIndex(right);
01848 }
01849 }
01850 else if (right.isBoundVar() && isGround(left)){
01851 if (Pos == pol || PosNeg == pol){
01852 addIndex(plusOne(left));
01853 }
01854 if (Neg == pol || PosNeg == pol){
01855 addIndex(left);
01856 }
01857 }
01858 else if (left.isBoundVar() && right.isBoundVar()){
01859
01860 }
01861
01862 else if (isShield(left) && isShield(right)){
01863 collect_shield_index(left);
01864 collect_shield_index(right);
01865 }
01866 else{
01867 cout << " foall is " << forall_quant << endl;
01868 DebugAssert(false, "impossible case in collect index ");
01869 }
01870 }
01871 else if (cur_expr.isEq()){
01872 const Expr& left = cur_expr[0];
01873 const Expr& right = cur_expr[1];
01874 if (left.isBoundVar() && isGround(right)){
01875 if (Pos == pol || PosNeg == pol){
01876 addIndex(minusOne(right));
01877 addIndex(plusOne(right));
01878 }
01879 if (Neg == pol || PosNeg == pol){
01880 addIndex(minusOne(right));
01881 }
01882 }
01883 else if (right.isBoundVar() && isGround(left)){
01884 if (Pos == pol || PosNeg == pol){
01885 addIndex(minusOne(left));
01886 addIndex(plusOne(left));
01887 }
01888 if (Neg == pol || PosNeg == pol){
01889 addIndex(left);
01890 }
01891 }
01892 else if (left.isBoundVar() && right.isBoundVar()){
01893 DebugAssert(false, "impossible case collect index");
01894 }
01895
01896 else if (isShield(left) && isShield(right)){
01897 collect_shield_index(left);
01898 collect_shield_index(right);
01899 }
01900 else{
01901 DebugAssert(false, "impossible case in collect index");
01902 }
01903 }
01904 else if (isLT(cur_expr)){
01905 const Expr& left = cur_expr[0];
01906 const Expr& right = cur_expr[1];
01907 if (left.isBoundVar() && isGround(right)){
01908 if (Pos == pol || PosNeg == pol){
01909 addIndex(plusOne(right));
01910 }
01911 if (Neg == pol || PosNeg == pol){
01912 addIndex(right);
01913 }
01914 }
01915 else if (right.isBoundVar() && isGround(left)){
01916 if (Pos == pol || PosNeg == pol){
01917 addIndex(plusOne(left));
01918 }
01919 if (Neg == pol || PosNeg == pol){
01920 addIndex(left);
01921 }
01922 }
01923 else if (left.isBoundVar() && right.isBoundVar()){
01924
01925 }
01926
01927 else if (isShield(left) && isShield(right)){
01928 collect_shield_index(left);
01929 collect_shield_index(right);
01930 }
01931 else{
01932 DebugAssert(false, "impossible case in collect index");
01933 }
01934 }
01935 else{
01936 collect_shield_index(cur_expr);
01937 }
01938 }
01939 }
01940
01941
01942 void CompleteInstPreProcessor::collectIndex(const Expr& assert){
01943
01944
01945 if(isGround(assert)){
01946 collect_shield_index(assert);
01947 return;
01948 }
01949
01950
01951 ExprMap<Polarity> cur_expr_pol;
01952 findPolarityAtomic(assert, cur_expr_pol, Pos);
01953
01954 for(ExprMap<Polarity>::iterator i = cur_expr_pol.begin(), iend = cur_expr_pol.end(); i != iend; i++) {
01955
01956 const Expr& cur_expr = i->first;
01957 Polarity pol = i->second;
01958
01959 if (cur_expr.isAtomicFormula()){
01960 if (cur_expr.containsBoundVar()){
01961 DebugAssert(false, "error in collecting ");
01962 return;
01963 }
01964 collect_shield_index(cur_expr);
01965 }
01966 else if (cur_expr.isForall()){
01967 if (Pos != pol){
01968 DebugAssert(false, "error in polarity ");
01969 return;
01970 }
01971 Expr newQuant = pullVarOut(cur_expr);
01972 collect_forall_index(newQuant);
01973
01974 d_quant_equiv_map[cur_expr] = newQuant;
01975 }
01976 else if (cur_expr.isExists()){
01977 if (Pos != pol){
01978 DebugAssert(false, "error in polarity " );
01979 return;
01980 }
01981 Expr newQuant = pullVarOut(cur_expr);
01982 Expr sko_expr = d_theoryCore->getCommonRules()->skolemize(newQuant);
01983 collect_forall_index(sko_expr);
01984
01985 d_quant_equiv_map[cur_expr] = sko_expr;
01986 }
01987 }
01988 return;
01989 }
01990
01991
01992 bool CompleteInstPreProcessor::isGood(const Expr& assert){
01993
01994 const std::set<Expr>& bvs = getBoundVars(assert);
01995 if (bvs.size() <= 0 ) {
01996
01997
01998 return true;
01999 }
02000
02001 ExprMap<Polarity> cur_expr_pol;
02002 findPolarityAtomic(assert, cur_expr_pol, Pos);
02003
02004 for(ExprMap<Polarity>::iterator i = cur_expr_pol.begin(),
02005 iend = cur_expr_pol.end();
02006 i != iend; i++) {
02007
02008 const Expr& cur_expr = i->first;
02009 Polarity pol = i->second;
02010
02011
02012
02013 if(cur_expr.isForall()) {
02014 if (Pos == pol){
02015 if( isGoodQuant(cur_expr)){
02016 }
02017 else{
02018 d_all_good = false;
02019 return false;
02020 }
02021 }
02022 else {
02023 DebugAssert(false, "error, Neg polarity in isGood ");
02024 return false;
02025 }
02026 }
02027 else if (cur_expr.isExists()){
02028 DebugAssert(false, "error, found exists in is good");
02029 if (Neg == pol || PosNeg == pol){
02030 DebugAssert(false, "error, neg polarity in isGood ");
02031 return false;
02032 }
02033 }
02034 }
02035 return true;
02036 }
02037
02038
02039
02040
02041
02042
02043
02044
02045
02046
02047
02048
02049
02050
02051
02052
02053
02054
02055
02056
02057
02058
02059
02060
02061
02062
02063
02064
02065
02066
02067
02068
02069
02070 bool CompleteInstPreProcessor::isGoodQuant(const Expr& e){
02071
02072
02073
02074
02075
02076
02077
02078
02079
02080
02081
02082 vector<Expr> bvs = e.getVars();
02083
02084 for (vector<Expr>::iterator i = bvs.begin(), iend = bvs.end(); i != iend; i++){
02085 if ( ! isInt(i->getType() ) ){
02086 return false;
02087 }
02088 }
02089
02090
02091
02092
02093
02094
02095 ExprMap<Polarity> body_pol ;
02096 findPolarity(e, body_pol, Pos);
02097
02098 for(ExprMap<Polarity>::iterator i = body_pol.begin(), iend = body_pol.end(); i != iend; i++) {
02099 if ((i->first).isAtomicFormula()){
02100 const Expr& cur_expr = i->first;
02101 Polarity pol = i->second;
02102
02103
02104 if (!cur_expr.containsBoundVar()){
02105 continue;
02106 }
02107 else if (isShield(cur_expr)){
02108 continue;
02109 }
02110 else if (isLE(cur_expr) || isLT(cur_expr) || cur_expr.isEq()){
02111 const Expr& left = cur_expr[0];
02112 const Expr& right = cur_expr[1];
02113 if (left.isBoundVar() && !right.containsBoundVar()){
02114 continue;
02115 }
02116 else if (right.isBoundVar() && !left.containsBoundVar()){
02117 continue;
02118 }
02119 else if (left.isBoundVar() && right.isBoundVar()){
02120 if (Neg == pol && isLE(cur_expr)){
02121 continue;
02122 }
02123 }
02124
02125 else if (isShield(left) && isShield(right)){
02126 continue;
02127 }
02128
02129 return false;
02130 }
02131 else{
02132
02133 return false;
02134 }
02135 }
02136 }
02137 return true;
02138 }
02139
02140 class recCompleteInster{
02141 const Expr& d_body;
02142 const std::vector<Expr>& d_bvs;
02143 std::vector<Expr> d_buff;
02144 const std::set<Expr>& d_all_index;
02145 Expr d_result;
02146 void inst_helper(int num_vars);
02147 public:
02148 recCompleteInster(const Expr&, const std::vector<Expr>&, std::set<Expr>& , Expr);
02149 Expr inst();
02150 };
02151
02152 recCompleteInster::recCompleteInster(const Expr& body, const std::vector<Expr>& bvs, std::set<Expr>& all_index, Expr res): d_body(body),d_bvs(bvs), d_all_index(all_index),d_result(res){}
02153
02154 Expr recCompleteInster::inst(){
02155 d_buff.resize(d_bvs.size());
02156
02157 inst_helper(d_bvs.size());
02158 return d_result;
02159 }
02160
02161 void recCompleteInster::inst_helper(int num_vars){
02162 if (1 == num_vars){
02163 for (set<Expr>::const_iterator i = d_all_index.begin(), iend = d_all_index.end(); i != iend; i++ ){
02164 d_buff[num_vars-1] = *i;
02165 d_result = d_result.andExpr(d_body.substExpr(d_bvs,d_buff));
02166 }
02167 }
02168 else{
02169 for (set<Expr>::const_iterator i = d_all_index.begin(), iend = d_all_index.end(); i != iend; i++ ){
02170 d_buff[num_vars-1] = *i;
02171 inst_helper(num_vars-1);
02172 }
02173 }
02174 }
02175
02176 Expr CompleteInstPreProcessor::inst(const Expr& assert){
02177 if(isGround(assert)){
02178 return assert;
02179 }
02180 else if (assert.isExists()){
02181 DebugAssert(d_quant_equiv_map.count(assert) > 0,"assert not found" ) ;
02182 return d_quant_equiv_map[assert];
02183 }
02184 else if( ! assert.isForall()){
02185 if (assert.arity() > 0){
02186 vector<Expr> children;
02187 for (int i = 0 ; i < assert.arity(); i++){
02188 Expr rep_child;
02189 rep_child = inst(assert[i]);
02190 children.push_back(rep_child);
02191 }
02192 return Expr(assert.getOp(), children);
02193 }
02194 else{
02195 DebugAssert(false, "error in inst");
02196 return assert;
02197 }
02198 }
02199
02200 DebugAssert(assert.isForall(), "not a forall");
02201 DebugAssert(d_quant_equiv_map.count(assert) > 0, "assert not found" ) ;
02202 Expr forall = d_quant_equiv_map[assert];
02203
02204 const vector<Expr>& bvs = forall.getVars();
02205 const Expr body = forall.getBody();
02206 vector<Expr> and_list;
02207
02208 if(d_allIndex.size() == 0){
02209 addIndex(d_theoryCore->getEM()->newRatExpr(0));
02210 }
02211
02212 if(bvs.size() == 1 ) {
02213
02214 for (set<Expr>::const_iterator i = d_allIndex.begin(), iend = d_allIndex.end();
02215 i != iend; i++ ){
02216 vector<Expr> inst_st;
02217
02218 inst_st.push_back(*i);
02219
02220
02221
02222
02223
02224
02225
02226 and_list.push_back(body.substExpr(bvs,inst_st));
02227 }
02228 return Expr(AND,and_list);
02229 }
02230 else if (bvs.size() == 2 ){
02231
02232 for (set<Expr>::const_iterator i = d_allIndex.begin(), iend = d_allIndex.end();
02233 i != iend; i++ ){
02234 for (set<Expr>::const_iterator j = d_allIndex.begin(), jend = d_allIndex.end();
02235 j != jend; j++ ){
02236 vector<Expr> inst_st;
02237 inst_st.push_back(*i);
02238 inst_st.push_back(*j);
02239
02240
02241
02242
02243
02244
02245
02246
02247
02248 and_list.push_back(body.substExpr(bvs,inst_st));
02249
02250 }
02251 }
02252
02253 return Expr(AND,and_list);
02254 }
02255
02256 else{
02257 Expr init_expr = d_theoryCore->trueExpr();
02258
02259 recCompleteInster inster(body, bvs, d_allIndex, init_expr);
02260
02261 return inster.inst();
02262 }
02263
02264
02265
02266 return assert;
02267 }
02268
02269 void flatAnds(const Expr& ands, vector<Expr>& results){
02270 if (ands.isAnd()){
02271 for(Expr::iterator i=ands.begin(), iend=ands.end(); i!=iend; ++i) {
02272 flatAnds(*i,results);
02273 }
02274 }
02275 else if (ands.isNot() && ands[0].isOr()){
02276 for(Expr::iterator i=ands[0].begin(), iend=ands[0].end(); i!=iend; ++i) {
02277 if(i->isNot()){
02278 flatAnds((*i)[0], results);
02279 }
02280 else{
02281 flatAnds(i->notExpr(), results);
02282 }
02283 }
02284 }
02285 else{
02286 results.push_back(ands);
02287 }
02288 }
02289
02290 Theorem TheoryQuant::theoryPreprocess(const Expr& e){
02291
02292
02293 if ( ! theoryCore()->getFlags()["quant-complete-inst"].getBool()){
02294 return reflexivityRule(e);
02295 }
02296
02297 const std::set<Expr>& bvs = getBoundVars(e);
02298 if (bvs.size() <= 0){
02299 return reflexivityRule(e);
02300 }
02301
02302 std::vector<Expr> assertList;
02303 flatAnds(e, assertList);
02304
02305 CompleteInstPreProcessor comp_inst_proc(theoryCore(), d_rules);
02306
02307 if (comp_inst_proc.hasMacros(assertList)){
02308 for(size_t i = 0; i < assertList.size();i++){
02309
02310 assertList[i] = comp_inst_proc.instMacros(assertList[i], trueExpr().notExpr().notExpr());
02311 }
02312 }
02313
02314 for(size_t i = 0; i < assertList.size() ; i++){
02315
02316 assertList[i] = comp_inst_proc.simplifyQuant(assertList[i]);
02317
02318 }
02319
02320 for(size_t i = 0; i < assertList.size() ; i++){
02321 if ( ! comp_inst_proc.isGood(assertList[i])){
02322
02323
02324 return reflexivityRule(e);
02325 }
02326 }
02327
02328 for(size_t i = 0; i < assertList.size() ; i++){
02329
02330 comp_inst_proc.collectIndex(assertList[i]);
02331 }
02332
02333 vector<Expr> new_asserts;
02334 for(size_t i = 0; i < assertList.size() ; i++){
02335 Expr new_asser = comp_inst_proc.inst(assertList[i]);
02336 getBoundVars(new_asser);
02337 if (new_asser.containsBoundVar()){
02338 return reflexivityRule(e);
02339 }
02340 else{
02341 new_asserts.push_back(new_asser);
02342 }
02343 }
02344
02345
02346
02347
02348
02349
02350
02351
02352
02353
02354
02355
02356
02357
02358
02359
02360
02361
02362
02363
02364
02365
02366
02367
02368
02369
02370
02371
02372
02373
02374
02375
02376
02377
02378
02379
02380
02381
02382 for(size_t i = 0; i < new_asserts.size() ; i++){
02383 new_asserts[i] = comp_inst_proc.simplifyEq(new_asserts[i]);
02384 }
02385
02386 for(size_t i = 0; i < new_asserts.size() ; i++){
02387
02388
02389 }
02390
02391
02392
02393 Expr res = Expr(AND, new_asserts);
02394 Theorem ret_thm = d_rules->addNewConst(e.iffExpr(res));
02395
02396 return ret_thm;
02397 }
02398
02399
02400
02401
02402 bool isGoodSysPredTrigger(const Expr& e){
02403 if(!isSysPred(e)) return false;
02404 if(usefulInMatch(e[0]) || usefulInMatch(e[1])) return true;
02405 return false;
02406 }
02407
02408 bool isGoodFullTrigger(const Expr& e, const std::vector<Expr>& bVarsThm){
02409 if( !usefulInMatch(e))
02410 return false;
02411
02412 const std::set<Expr>& bvs = getBoundVars(e);
02413
02414 if (bvs.size() >= bVarsThm.size()){
02415 for(size_t i=0; i<bVarsThm.size(); i++) {
02416 if (bvs.find(bVarsThm[i]) == bvs.end()){
02417 return false;
02418 }
02419 }
02420 return true;
02421 }
02422 else {
02423 return false;
02424 }
02425 }
02426
02427 bool isGoodMultiTrigger(const Expr& e, const std::vector<Expr>& bVarsThm, int offset){
02428 if( !usefulInMatch(e) )
02429 return false;
02430
02431 int bvar_missing = 0;
02432 const std::set<Expr>& bvs = getBoundVars(e);
02433
02434 if(bvs.size() <= 0) return false;
02435
02436 for(size_t i=0; i<bVarsThm.size(); i++) {
02437 if (bvs.find(bVarsThm[i]) == bvs.end()){
02438 bvar_missing++;
02439 }
02440 }
02441
02442 if (0 == bvar_missing){
02443 return false;
02444 }
02445
02446 if(bvar_missing <= offset){
02447 if(isSysPred(e)){
02448 if (isGoodSysPredTrigger(e)) {
02449 return true;
02450 }
02451 else {
02452 return false;
02453 }
02454 }
02455 else {
02456 return true;
02457 }
02458 }
02459 return false;
02460 }
02461
02462 bool isGoodPartTrigger(const Expr& e, const std::vector<Expr>& bVarsThm){
02463 if( !usefulInMatch(e) )
02464 return false;
02465
02466 size_t bvar_missing = 0;
02467 const std::set<Expr>& bvs = getBoundVars(e);
02468
02469 for(size_t i=0; i<bVarsThm.size(); i++) {
02470 if (bvs.find(bVarsThm[i]) == bvs.end()){
02471 bvar_missing++;
02472 }
02473 }
02474
02475 if (0 == bvar_missing){
02476 return false;
02477 }
02478
02479 if(0 == bvs.size()){
02480 return false;
02481 }
02482
02483 if(bvar_missing < bVarsThm.size()){
02484 if(isSysPred(e)){
02485 if (isGoodSysPredTrigger(e)) {
02486 return true;
02487 }
02488 else {
02489 return false;
02490 }
02491 }
02492 else {
02493 return true;
02494 }
02495 }
02496 return false;
02497 }
02498
02499
02500 static bool recursiveGetPartTriggers(const Expr& e, std::vector<Expr>& res) {
02501 if(e.getFlag())
02502 return false;
02503
02504 if(e.isClosure())
02505 return recursiveGetPartTriggers(e.getBody(), res);
02506
02507 if(0 == e.arity()){
02508 if(BOUND_VAR == e.getKind()){
02509 return false;
02510 }
02511 else{
02512 return true;
02513 }
02514 }
02515
02516 bool good=true;
02517 bool no_bound =true;
02518
02519 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
02520 if(BOUND_VAR == i->getKind()){
02521 no_bound=false;
02522 continue;
02523 }
02524 bool temp = recursiveGetPartTriggers(*i,res);
02525 if(false == temp) {
02526 good=false;
02527 }
02528 }
02529
02530 e.setFlag();
02531
02532 if(good && no_bound) {
02533 return true;
02534 }
02535 else if(good && !no_bound){
02536 res.push_back(e);
02537 return false;
02538 }
02539 else{
02540 return false;
02541 }
02542 }
02543
02544
02545 std::vector<Expr> getPartTriggers(const Expr& e){
02546 e.clearFlags();
02547 std::vector<Expr> res;
02548 recursiveGetPartTriggers(e,res);
02549 e.clearFlags();
02550 return res;
02551 }
02552
02553 int trigInitScore(const Expr& e){
02554 if( isSysPred(e) && !isGoodSysPredTrigger(e)){
02555 return 1;
02556 }
02557 else {
02558 return 0;
02559 }
02560 }
02561
02562
02563 void TheoryQuant::arrayIndexName(const Expr& e){
02564 std::vector<Expr> res;
02565
02566 const std::vector<Expr>& subs=getSubTerms(e);
02567
02568 for(size_t i=0; i<subs.size(); i++){
02569 int kind = subs[i].getKind();
02570 if (READ == kind || WRITE == kind){
02571 const Expr& name = subs[i][0];
02572 const Expr& index = subs[i][1];
02573 if(getBoundVars(name).size() <= 0 && (getBoundVars(index).size() <=0)){
02574 std::vector<Expr> tp = d_arrayIndic[name];
02575 tp.push_back(index);
02576 d_arrayIndic[name]=tp;
02577 }
02578 else {
02579 }
02580 }
02581 }
02582 }
02583
02584 void TheoryQuant::registerTrig(ExprMap<ExprMap<std::vector<dynTrig>* >* >& cur_trig_map,
02585 Trigger trig,
02586 const std::vector<Expr> thmBVs,
02587 size_t univ_id){
02588 {
02589 if(trig.hasRWOp){
02590 ExprMap<Expr> bv_map;
02591 dynTrig newDynTrig(trig, bv_map,univ_id);
02592 d_arrayTrigs.push_back(newDynTrig);
02593 }
02594 }
02595
02596 ExprMap<Expr> bv_map;
02597
02598
02599
02600
02601
02602
02603
02604 for(size_t i = 0; i<thmBVs.size(); i++){
02605 bv_map[thmBVs[i]] = thmBVs[i];
02606 }
02607
02608
02609
02610 const Expr& trig_ex = trig.getEx();
02611
02612 Expr genTrig = trig_ex;
02613
02614
02615 dynTrig newDynTrig(trig,bv_map,univ_id);
02616
02617 Expr head = trig.getHead();
02618
02619 ExprMap<ExprMap<vector<dynTrig>* >* >::iterator iter = cur_trig_map.find(head);
02620 if(cur_trig_map.end() == iter){
02621 ExprMap<vector<dynTrig>* >* new_cd_map= new ExprMap<vector<dynTrig>* > ;
02622 cur_trig_map[head] = new_cd_map;
02623 vector<dynTrig>* new_dyntrig_list = new vector<dynTrig>;
02624 (*new_cd_map)[genTrig] = new_dyntrig_list;
02625 (*new_dyntrig_list).push_back(newDynTrig);
02626 }
02627 else{
02628 ExprMap<vector<dynTrig>* >* cd_map = iter->second;
02629 ExprMap<vector<dynTrig>* >::iterator iter_map = cd_map->find(genTrig);
02630 if(cd_map->end() == iter_map){
02631 vector<dynTrig>* new_dyntrig_list = new vector<dynTrig>;
02632 (*cd_map)[genTrig] = new_dyntrig_list;
02633 (*new_dyntrig_list).push_back(newDynTrig);
02634 }
02635 else{
02636
02637
02638 (*(iter_map->second)).push_back(newDynTrig);
02639 }
02640 }
02641 }
02642
02643
02644
02645
02646
02647
02648
02649
02650
02651
02652
02653
02654
02655
02656
02657
02658
02659
02660
02661
02662
02663
02664
02665
02666
02667
02668
02669
02670
02671
02672
02673
02674
02675
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
02737
02738
02739
02740
02741
02742
02743
02744 bool TheoryQuant::canMatch(const Expr& t1, const Expr& t2, ExprMap<Expr>& env){
02745 if(getBaseType(t1) != getBaseType(t2)) return false;
02746
02747 if (BOUND_VAR == t1.getKind() || BOUND_VAR == t2.getKind()) {
02748 return true;
02749 }
02750
02751 if ( (t1.arity() != t2.arity()) || (t1.getKind() != t2.getKind() )) {
02752 return false;
02753 }
02754 if (canGetHead(t1) && canGetHead(t2)) {
02755 if ( getHead(t1) != getHead(t2) ){
02756 return false;
02757 }
02758 for(int i=0; i<t1.arity(); i++){
02759 if (false == canMatch(t1[i], t2[i] , env))
02760 return false;
02761 }
02762 return true;
02763 }
02764 else{
02765 return false;
02766 }
02767 }
02768
02769 bool TheoryQuant::isTransLike (const vector<Expr>& cur_trig){
02770 if(!(*d_useTrans)){
02771 return false;
02772 }
02773 if(3==cur_trig.size()){
02774 const Expr& t1=cur_trig[0];
02775 const Expr& t2=cur_trig[1];
02776 const Expr& t3=cur_trig[2];
02777 if ( canGetHead(t1) && canGetHead(t2) && canGetHead(t3) &&
02778 (getHead(t1) == getHead(t2)) && (getHead(t2) == getHead(t3))){
02779 const std::set<Expr>& ts1 = getBoundVars(t1);
02780 const std::set<Expr>& ts2 = getBoundVars(t2);
02781 const std::set<Expr>& ts3 = getBoundVars(t3);
02782 if ( 2==ts1.size() && 2==ts2.size() && 2==ts2.size() &&
02783 (ts1 != ts2) && (ts2 != ts3) && (ts3 != ts1)){
02784 std::set<Expr> all;
02785 for(set<Expr>::const_iterator i=ts1.begin(), iend = ts1.end(); i != iend; i++){
02786 all.insert(*i);
02787 }
02788 for(set<Expr>::const_iterator i=ts2.begin(), iend = ts2.end(); i != iend; i++){
02789 all.insert(*i);
02790 }
02791 for(set<Expr>::const_iterator i=ts3.begin(), iend = ts3.end(); i != iend; i++){
02792 all.insert(*i);
02793 }
02794 bool res = true;
02795 if(3==all.size()){
02796 for(set<Expr>::const_iterator i=all.begin(), iend = all.end(); i != iend; i++){
02797 if(!i->isVar()) {
02798 res = false;
02799 break;
02800 }
02801 }
02802 if(res) {
02803 }
02804 return res;
02805 }
02806 }
02807 }
02808 }
02809 return false;
02810 }
02811
02812 bool TheoryQuant::isTrans2Like (const std::vector<Expr>& all_terms, const Expr& tr2){
02813 if(!(*d_useTrans2)){
02814 return false;
02815 }
02816 for(size_t i = 0; i < all_terms.size(); i++){
02817 if(all_terms[i].isEq()){
02818 const Expr& cur = all_terms[i];
02819 if(cur[0] != cur[1] && ( (cur[0]==tr2[0] && cur[1]==tr2[1]) || (cur[0]==tr2[1] && cur[1]==tr2[0]))){
02820 return true;
02821 }
02822 }
02823 }
02824 return false;
02825 }
02826
02827
02828 bool goodMultiTriggers(const std::vector<Expr>& exprs, const std::vector<Expr> bVars){
02829 ExprMap<bool> bvar_found;
02830
02831 for( std::vector<Expr>::const_iterator i = bVars.begin(), iend= bVars.end(); i!=iend; i++) {
02832 bvar_found[*i]=false;
02833 }
02834
02835 for (size_t i=0; i< exprs.size();i++){
02836 const std::set<Expr> & bv_in_trig = getBoundVars(exprs[i]);
02837 for(std::set<Expr>::const_iterator j=bv_in_trig.begin(), jend = bv_in_trig.end(); j != jend; j++){
02838 if(bvar_found.find(*j) != bvar_found.end()){
02839 bvar_found[*j]=true;
02840 }
02841 }
02842 }
02843
02844 for( std::vector<Expr>::const_iterator i = bVars.begin(), iend= bVars.end(); i!=iend; i++) {
02845 if(false == bvar_found[*i]){
02846 return false ;
02847 }
02848 }
02849 return true;
02850 }
02851
02852
02853 inline size_t locVar(const vector<Expr>& bvsThm, const Expr& bv){
02854 for(size_t i=0, iend = bvsThm.size(); i < iend; i++){
02855 if (bvsThm[i] == bv){
02856 return i;
02857 }
02858 }
02859 return 999;
02860 }
02861
02862
02863 void TheoryQuant::setupTriggers(ExprMap<ExprMap<vector<dynTrig>* >*>& trig_maps, const Theorem& thm, size_t univs_id){
02864
02865
02866 const Expr& e = thm.getExpr();
02867
02868 TRACE("triggers", "setup : "+int2string(e.getIndex()), " | " , e.toString());
02869
02870 d_univs.push_back(thm);
02871 const std::vector<Expr>& bVarsThm = e.getVars();
02872 if (d_hasTriggers.count(e) > 0 ) {
02873
02874 if(d_fullTrigs.count(e)>0){
02875 std::vector<Trigger>& new_trigs = d_fullTrigs[e];
02876 for(size_t i=0; i<new_trigs.size(); i++){
02877 registerTrig(trig_maps, new_trigs[i], bVarsThm, univs_id);
02878 }
02879 }
02880
02881 if( d_multTrigs.count(e) > 0){
02882 std::vector<Trigger>& new_mult_trigs = d_multTrigs[e];
02883 for(size_t j=0; j<new_mult_trigs.size(); j++){
02884 registerTrig(trig_maps, new_mult_trigs[j], bVarsThm, univs_id);
02885 }
02886 }
02887 return;
02888 }
02889
02890 if (*d_useManTrig ) {
02891 if(e.getTrigs().size() > 0) {
02892
02893
02894 }
02895 }
02896
02897 d_hasTriggers[e]=true;
02898
02899 TRACE("triggers-new", "setup : "+int2string(e.getIndex()), " | " , e.toString());
02900
02901
02902
02903 const std::vector<Expr> subterms = getSubTrig(e);
02904
02905
02906
02907
02908
02909
02910
02911
02912
02913
02914
02915
02916
02917 ExprMap<Polarity> exprPol;
02918 findPolarity(e, exprPol, Pos);
02919
02920 {
02921 std::vector<Expr> trig_list;
02922 std::vector<Expr> trig_cadt;
02923 for(std::vector<Expr>::const_iterator i = subterms.begin(),iend=subterms.end(); i!=iend; i++){
02924 if(isGoodFullTrigger(*i, bVarsThm)) {
02925 trig_cadt.push_back(*i);
02926 }
02927 }
02928
02929
02930 if(*d_useManTrig && e.getTrigs().size() > 0 ){
02931 std::vector<std::vector<Expr> > man_trigs = e.getTrigs();
02932 for(std::vector<std::vector<Expr> >::const_iterator i=man_trigs.begin(), iend=man_trigs.end(); i != iend; i++){
02933
02934 if(1 == i->size()){
02935 trig_list.push_back((*i)[0]);
02936
02937 }
02938
02939 else if(2 == i->size()){
02940 if (isGoodFullTrigger((*i)[0], bVarsThm) && isGoodFullTrigger((*i)[1], bVarsThm)){
02941 trig_list.push_back((*i)[0]);
02942 trig_list.push_back((*i)[1]);
02943 break;
02944 }
02945 }
02946 }
02947 }
02948 else{
02949 for(size_t iter =0; iter < trig_cadt.size(); iter++) {
02950 Expr* i = &(trig_cadt[iter]);
02951 bool notfound = true;
02952
02953 for(size_t index=0; index< trig_list.size(); index++){
02954 if (i->subExprOf(trig_list[index])) {
02955 trig_list[index]=*i;
02956 notfound=false;
02957 break;
02958 }
02959 if (trig_list[index].subExprOf(*i)) {
02960 notfound=false;
02961 break;
02962 }
02963 }
02964 if (notfound) {
02965 trig_list.push_back(*i);
02966 }
02967 }
02968 }
02969
02970 std::vector<Trigger> trig_ex;
02971
02972 for (size_t i=0; i< trig_list.size();i++){
02973 const Expr& cur = trig_list[i];
02974 const std::set<Expr> cur_bvs = getBoundVars(cur);
02975 int score = trigInitScore(cur);
02976 if(score > 0) continue;
02977
02978
02979
02980
02981 for(size_t j=0; j< trig_cadt.size(); j++){
02982 if (trig_list[i] == trig_cadt[j]) continue;
02983 ExprMap<Expr> null;
02984 if (canMatch(trig_list[i], trig_cadt[j], null)){
02985 if(exprScore(trig_list[i]) < exprScore(trig_cadt[j])){
02986 }
02987 else if(*d_useTrans2 &&
02988 trig_list.size() == 2 &&
02989 trig_list[i].arity() == 2 &&
02990 BOUND_VAR == trig_list[i][0].getKind() &&
02991 BOUND_VAR == trig_list[i][1].getKind() &&
02992 BOUND_VAR == trig_cadt[j][0].getKind() &&
02993 BOUND_VAR == trig_cadt[j][1].getKind() &&
02994 isTrans2Like(subterms, trig_list[i])
02995 ){
02996
02997 score =0;
02998 d_trans2_num++;
02999
03000 DebugAssert(d_trans2_num<=1, "more than 2 trans2 found");
03001 TRACE("triggers", "trans2 found ", trig_list[i], "");
03002
03003 Trigger t(theoryCore(), cur, Neg, cur_bvs);
03004 t.setTrans2(true);
03005 t.setHead(getHeadExpr(cur));
03006 if(isSimpleTrig(cur)){
03007 t.setSimp();
03008 }
03009 if(isSuperSimpleTrig(cur)){
03010 t.setSuperSimp();
03011 }
03012 d_fullTrigs[e].push_back(t);
03013 registerTrig(trig_maps,t, bVarsThm, univs_id);
03014 return;
03015 }
03016 else{
03017 score =0;
03018 }
03019 }
03020 }
03021
03022 Polarity pol= Ukn;
03023
03024 if(cur.getType().isBool()){
03025 DebugAssert(exprPol.count(e)>0,"unknown polarity:"+cur.toString());
03026 pol = exprPol[cur];
03027 }
03028
03029 Trigger* t;
03030 Trigger* t_ex;
03031
03032 if(PosNeg == pol && *d_usePolarity){
03033 t = new Trigger(theoryCore(), cur, Pos, cur_bvs);
03034 t_ex = new Trigger(theoryCore(), cur, Neg, cur_bvs);
03035 if(isSimpleTrig(cur)){
03036 t->setSimp();
03037 t_ex->setSimp();
03038 }
03039 if(isSuperSimpleTrig(cur)){
03040 t->setSuperSimp();
03041 t_ex->setSuperSimp();
03042 }
03043
03044 }
03045 else{
03046 t = new Trigger(theoryCore(), cur, pol, cur_bvs);
03047 if(isSimpleTrig(cur)){
03048 t->setSimp();
03049 }
03050 if(isSuperSimpleTrig(cur)){
03051 t->setSuperSimp();
03052 }
03053 t_ex = NULL;
03054 }
03055
03056 if(canGetHead(cur)) {
03057 t->setHead(getHeadExpr(cur));
03058 if(NULL != t_ex){
03059 t_ex->setHead(getHeadExpr(cur));
03060 }
03061 }
03062 else{
03063 if(!isSysPred(cur)){
03064
03065
03066 }
03067 }
03068
03069 t->setRWOp(false);
03070
03071 if(READ == cur.getKind() || WRITE == cur.getKind()){
03072 arrayIndexName(cur);
03073 }
03074
03075 if(READ == cur.getKind() && WRITE== cur[0].getKind() && 1 == bVarsThm.size() ){
03076
03077 t->setRWOp(true);
03078 if(t_ex != NULL) t_ex->setRWOp(true);
03079 }
03080
03081 if(t_ex != NULL) {
03082 trig_ex.push_back(*t_ex);
03083 }
03084
03085 d_fullTrigs[e].push_back(*t);
03086 registerTrig(trig_maps,*t, bVarsThm, univs_id);
03087
03088 TRACE("triggers", "new:full triggers:", cur.toString(),"");
03089 TRACE("triggers", "new:full trigger score:", score,"");
03090 TRACE("triggers", "new:full trigger pol:", pol,"");
03091 }
03092
03093 if(e.getTrigs().size() > 0) {
03094
03095
03096 }
03097
03098
03099 for(size_t i=0; i<trig_ex.size(); i++){
03100 d_fullTrigs[e].push_back(trig_ex[i]);
03101 registerTrig(trig_maps,trig_ex[i], bVarsThm, univs_id);
03102 TRACE("triggers", "new extra :full triggers:", trig_ex[i].getEx().toString(),"");
03103 }
03104
03105 if(d_fullTrigs[e].size() == 0){
03106 TRACE("triggers warning", "no full trig: ", e , "");
03107 }
03108 }
03109
03110
03111 if(0 == d_fullTrigs[e].size())
03112 {
03113 std::vector<Expr>& cur_trig = d_multTriggers[e];
03114 if(*d_useManTrig && e.getTrigs().size() > 0 ){
03115 std::vector<std::vector<Expr> > man_trig = e.getTrigs();
03116 int count(0);
03117 for(std::vector<std::vector<Expr> >::const_iterator i = man_trig.begin(), iend = man_trig.end(); i != iend; i++){
03118
03119 if (i->size() > 1) count++;
03120
03121 }
03122
03123 if(count > 1){
03124
03125
03126 }
03127
03128 if(man_trig[count-1].size() != 2){
03129
03130
03131
03132
03133
03134
03135 }
03136
03137 for(std::vector<Expr>::const_iterator j = man_trig[count-1].begin(), jend = man_trig[count-1].end(); j != jend; ++j){
03138 cur_trig.push_back(*j);
03139 }
03140 }
03141 else{
03142 for( std::vector<Expr>::const_iterator i = subterms.begin(), iend=subterms.end(); i!=iend; i++) {
03143 if(isGoodMultiTrigger(*i, bVarsThm, d_offset_multi_trig)) {
03144 bool notfound = true;
03145 for(size_t index=0; index<d_multTriggers[e].size(); index++){
03146 if (i->subExprOf(d_multTriggers[e][index])) {
03147 (d_multTriggers[e][index])=*i;
03148 notfound=false;
03149 }
03150 }
03151 if (notfound){
03152 d_multTriggers[e].push_back(*i);
03153 }
03154 }
03155 }
03156
03157 if (goodMultiTriggers(cur_trig, bVarsThm)){
03158
03159 TRACE("multi-triggers", "good set of multi triggers","","");
03160 for (size_t i=0; i< d_multTriggers[e].size();i++){
03161
03162 TRACE("multi-triggers", "multi-triggers:", d_multTriggers[e][i].toString(),"");
03163 }
03164 }
03165 else{
03166 cur_trig.clear();
03167
03168 TRACE("multi-triggers", "bad set of multi triggers","","");
03169 return;
03170 }
03171
03172 }
03173
03174
03175 {
03176 if(isTransLike(cur_trig)){
03177 d_trans_num++;
03178 DebugAssert(d_trans_num <= 1, "more than one trans found");
03179
03180 Expr ex = cur_trig[0];
03181
03182 Trigger* trans_trig = new Trigger(theoryCore(), ex, Neg, getBoundVars(ex));
03183 trans_trig->setHead(getHeadExpr(ex));
03184 if(isSimpleTrig(ex)){
03185 trans_trig->setSimp();
03186 }
03187 if(isSuperSimpleTrig(ex)){
03188 trans_trig->setSuperSimp();
03189 }
03190
03191 trans_trig->setTrans(true);
03192
03193 d_fullTrigs[e].push_back(*trans_trig);
03194 registerTrig(trig_maps,*trans_trig, bVarsThm, univs_id);
03195 cur_trig.clear();
03196 TRACE("triggers", " trans like found ", ex, "");
03197 d_transThm = thm;
03198 }
03199 }
03200
03201
03202
03203 if(cur_trig.size() >0 ){
03204
03205 std::vector<Expr> posList, negList;
03206 for(size_t k=0; k<cur_trig.size(); k++){
03207 const Expr& cur_item = cur_trig[k];
03208 if (cur_item.getType().isBool()){
03209 Polarity pol = exprPol[cur_item];
03210 if(PosNeg == pol || Pos == pol){
03211 posList.push_back(cur_item);
03212 }
03213 if(PosNeg == pol || Neg == pol){
03214 negList.push_back(cur_item);
03215 }
03216 }
03217 }
03218 if (goodMultiTriggers(posList, bVarsThm)){
03219 TRACE("multi-triggers", "good set of multi triggers pos","","");
03220 for (size_t i=0; i< posList.size();i++){
03221 TRACE("multi-triggers", "multi-triggers:", posList[i].toString(),"");
03222 }
03223 cur_trig.clear();
03224 for(size_t m=0; m<posList.size(); m++){
03225 cur_trig.push_back(posList[m]);
03226 }
03227 }
03228 if (goodMultiTriggers(negList, bVarsThm) && negList.size() < cur_trig.size()){
03229 TRACE("multi-triggers", "good set of multi triggers neg","","");
03230 for (size_t i=0; i< negList.size();i++){
03231 TRACE("multi-triggers", "multi-triggers:", negList[i].toString(),"");
03232 }
03233 cur_trig.clear();
03234 for(size_t m=0; m<negList.size(); m++){
03235 cur_trig.push_back(negList[m]);
03236 }
03237 }
03238 }
03239
03240 {
03241
03242 if(!(*d_useManTrig) || e.getTrigs().size() <= 0){
03243
03244 if( 3 == cur_trig.size() || 4 == cur_trig.size() || 5 == cur_trig.size() || 6 == cur_trig.size() ){
03245 for(size_t i = 0; i < cur_trig.size(); i++){
03246 for(size_t j = 0; j < i; j++){
03247 vector<Expr> tempList;
03248 tempList.clear();
03249 tempList.push_back(cur_trig[i]);
03250 tempList.push_back(cur_trig[j]);
03251
03252
03253 if (goodMultiTriggers(tempList, bVarsThm)){
03254 cur_trig.clear();
03255 cur_trig.push_back(tempList[0]);
03256 cur_trig.push_back(tempList[1]);
03257 break;
03258 }
03259 }
03260 }
03261 }
03262 }
03263
03264 if(cur_trig.size() != 2){
03265 if( 0 == cur_trig.size()){
03266 return;
03267 }
03268
03269
03270
03271
03272
03273
03274
03275
03276
03277 return;
03278 }
03279
03280
03281 for(size_t i = 0 ; i<cur_trig.size(); i++){
03282 set<Expr> bvs = getBoundVars(cur_trig[i]);
03283 Trigger trig(theoryCore(), cur_trig[i], Ukn, bvs);
03284
03285 trig.setHead(getHead(cur_trig[i]));
03286 trig.setMultiTrig();
03287 trig.multiIndex = i;
03288 trig.multiId=d_all_multTrigsInfo.size();
03289 d_multTrigs[e].push_back(trig);
03290 registerTrig(trig_maps, trig, bVarsThm, univs_id);
03291 }
03292
03293 {
03294 multTrigsInfo multTrigs;
03295 for(size_t i =0, iend = d_multTrigs[e].size(); i<iend; i++){
03296 const std::vector<Expr>& one_set_bvs = d_multTrigs[e][i].bvs;
03297 std::vector<size_t> one_set_pos;
03298
03299 for(size_t v = 0, vend = one_set_bvs.size(); v<vend; v++){
03300 size_t loc = locVar(bVarsThm, one_set_bvs[v]);
03301 if( 999 != loc ){
03302 one_set_pos.push_back(loc);
03303 }
03304 }
03305
03306 sort(one_set_pos.begin(), one_set_pos.end());
03307
03308 for(size_t v = 0, vend = one_set_pos.size(); v<vend; v++){
03309 }
03310
03311 multTrigs.var_pos.push_back(one_set_pos);
03312 }
03313
03314
03315 vector<size_t> common;
03316 std::vector<size_t>& tar1 = multTrigs.var_pos[0];
03317 std::vector<size_t>& tar2 = multTrigs.var_pos[1];
03318 vector<size_t>::iterator t1(tar1.begin()), t2(tar2.begin());
03319 while(t1 != tar1.end() && t2!= tar2.end()){
03320 size_t pos1 = *t1;
03321 size_t pos2 = *t2;
03322 if( pos1 == pos2 ) {
03323 common.push_back(pos1);
03324 t1=tar1.erase(t1);
03325 t2=tar2.erase(t2);
03326 }
03327 else if( pos1 > pos2 ){
03328 t2++;
03329 }
03330 else {
03331 t1++;
03332 }
03333 }
03334 multTrigs.common_pos.push_back(common);
03335
03336 size_t multi_size = d_multTrigs[e].size();
03337 for(size_t i =0; i< multi_size; i++){
03338 multTrigs.var_binds_found.push_back(new (true) CDMap<Expr, bool> (theoryCore()->getCM()->getCurrentContext()));
03339 }
03340 multTrigs.uncomm_list.push_back(new ExprMap<CDList<Expr>* >);
03341 multTrigs.uncomm_list.push_back(new ExprMap<CDList<Expr>* >);
03342 multTrigs.univThm = thm;
03343 multTrigs.univ_id = univs_id;
03344 d_multitrigs_maps[e] = multTrigs;
03345 d_all_multTrigsInfo.push_back(multTrigs);
03346 }
03347 }
03348 }
03349
03350
03351
03352
03353
03354
03355
03356
03357
03358
03359
03360
03361
03362
03363
03364
03365
03366
03367
03368
03369
03370
03371
03372
03373
03374
03375
03376
03377
03378
03379
03380
03381
03382
03383
03384
03385
03386
03387
03388
03389
03390
03391
03392
03393
03394
03395
03396
03397
03398
03399
03400
03401
03402
03403
03404
03405
03406
03407
03408
03409
03410
03411
03412 }
03413
03414
03415
03416 int hasMoreBVs(const Expr& thm){
03417 DebugAssert(thm.isForall(), "hasMoreBVS called by non-forall exprs");
03418
03419 const std::vector<Expr>& bvsOutmost = thm.getVars();
03420 const std::set<Expr>& bvs = getBoundVars(thm);
03421
03422 return int(bvs.size()-bvsOutmost.size());
03423
03424 }
03425
03426
03427
03428
03429
03430
03431
03432
03433
03434
03435 void TheoryQuant::assertFact(const Theorem& thm){
03436
03437 if(d_maxILReached){
03438 return;
03439 }
03440 if(*d_translate) return;
03441
03442 TRACE("quant assertfact", "assertFact => ", thm.toString(), "{");
03443 Theorem rule, result;
03444 const Expr& expr = thm.getExpr();
03445
03446
03447 if(expr.isExists()) {
03448 TRACE("quant assertfact", "assertFact => (ignoring existential) }", expr.toString(), "");
03449 return;
03450 }
03451
03452 DebugAssert(expr.isForall() || (expr.isNot() && (expr[0].isExists() || expr[0].isForall())),
03453 "Theory of quantifiers cannot handle expression "
03454 + expr.toString());
03455
03456 if(expr.isNot()) {
03457 if(expr[0].isForall()) {
03458 rule = d_rules->rewriteNotForall(expr);
03459 }
03460 else if(expr[0].isExists()) {
03461 rule = d_rules->rewriteNotExists(expr);
03462 }
03463 result = iffMP(thm, rule);
03464 }
03465 else{
03466 result = thm;
03467 }
03468
03469 result = d_rules->boundVarElim(result);
03470
03471
03472 if(result.getExpr().isForall()){
03473 if(*d_useNew){
03474
03475 if(result.getExpr().getBody().isForall()){
03476 result=d_rules->packVar(result);
03477 }
03478 result = d_rules->boundVarElim(result);
03479
03480
03481
03482
03483
03484
03485 if(result.getExpr().isForall()){
03486 d_rawUnivs.push_back(result);
03487 }
03488 else{
03489 enqueueFact(result);
03490 }
03491 return;
03492
03493
03494
03495
03496
03497
03498
03499
03500
03501
03502
03503
03504
03505
03506
03507
03508
03509
03510
03511
03512
03513
03514
03515
03516
03517
03518
03519
03520
03521
03522
03523
03524
03525
03526
03527
03528
03529
03530
03531 }
03532 else{
03533
03534 TRACE("quant assertfact", "assertFact => old-fashoin enqueueing: ", result.toString(), "}");
03535
03536 d_univs.push_back(result);
03537 }
03538 }
03539 else {
03540 TRACE("quant assertfact", "assertFact => non-forall enqueueing: ", result.toString(), "}");
03541 if(*d_useGFact || true ){
03542
03543 enqueueFact(result);
03544 }
03545 else{
03546 enqueueFact(result);
03547
03548 }
03549
03550
03551
03552
03553
03554
03555
03556
03557
03558
03559
03560
03561
03562
03563
03564
03565
03566 }
03567 }
03568
03569 void TheoryQuant::recGoodSemMatch(const Expr& e,
03570 const std::vector<Expr>& bVars,
03571 std::vector<Expr>& newInst,
03572 std::set<std::vector<Expr> >& instSet)
03573 {
03574 size_t curPos = newInst.size();
03575 if (bVars.size() == curPos) {
03576 Expr simpleExpr = simplifyExpr(e.substExpr(bVars,newInst));
03577 if (simpleExpr.hasFind()){
03578 std::vector<Expr> temp = newInst;
03579 instSet.insert(temp);
03580 TRACE("quant yeting", "new inst found for ", e.toString()+" ==> ", simpleExpr.toString());
03581 };
03582 }
03583 else {
03584 Type t = getBaseType(bVars[curPos]);
03585 std::vector<Expr> tyExprs= d_typeExprMap[t];
03586 if (0 == tyExprs.size()) {
03587 return;
03588 }
03589 else{
03590 for (size_t i=0;i<tyExprs.size();i++){
03591 newInst.push_back(tyExprs[i]);
03592 recGoodSemMatch(e,bVars,newInst,instSet);
03593 newInst.pop_back();
03594 }
03595 }
03596 }
03597 }
03598
03599
03600 bool isIntx(const Expr& e, const Rational& x){
03601 if(e.isRational() && e.getRational()==x)
03602 return true;
03603 else return false;
03604 }
03605
03606
03607 Expr getLeft(const Expr& e){
03608 if(e.getKind()!= PLUS) return null_expr;
03609 if(e.arity() != 3) return null_expr;
03610 Expr const_expr, minus ,pos;
03611 int numMinus=0, numPos=0, numConst=0;;
03612 for(int i=0; i<e.arity(); i++){
03613 if((e[i]).getKind() == MULT){
03614 if(isIntx(e[i][0], -1)){
03615 numMinus++;
03616 minus=e[i][1];
03617 }
03618 else{
03619 numPos++;
03620 pos=e[i];
03621 }
03622 }
03623 else if(e[i].isRational()) {
03624 const_expr = e[i];
03625 numConst++;
03626 }
03627 else{
03628 numPos++;
03629 pos=e[i];
03630 }
03631 }
03632 if(1==numPos && 1==numConst && 1==numMinus){
03633 return minus;
03634 }
03635 else{
03636 return null_expr;
03637 }
03638 }
03639
03640 Expr getRight(const Expr& e){
03641 if(e.getKind()!= PLUS) return null_expr;
03642 if(e.arity() != 3) return null_expr;
03643 Expr const_expr, minus ,pos;
03644 int numMinus=0, numPos=0, numConst=0;;
03645
03646 for(int i=0; i<e.arity(); i++){
03647 if((e[i]).getKind() == MULT){
03648 if(isIntx(e[i][0], -1)){
03649 numMinus++;
03650 minus=e[i][1];
03651 }
03652 else{
03653 numPos++;
03654 pos=e[i];
03655 }
03656 }
03657 else if(e[i].isRational()) {
03658 const_expr = e[i];
03659 numConst++;
03660 }
03661 else{
03662 numPos++;
03663 pos=e[i];
03664 }
03665 }
03666
03667 if(1==numPos && 1==numConst && 1==numMinus){
03668 if(isIntx(const_expr,0)){
03669 return pos;
03670 }
03671 else{
03672
03673 return Expr(PLUS, const_expr, pos);
03674 }
03675 }
03676 else{
03677 return null_expr;
03678 }
03679 return null_expr;
03680 }
03681
03682 inline void TheoryQuant::add_parent(const Expr& parent){
03683 ExprMap<CDList<Expr>* >::iterator iter;
03684 for(int i=0; i< parent.arity(); i++){
03685 const Expr& child = parent[i];
03686 iter = d_parent_list.find(child);
03687 if(d_parent_list.end() == iter){
03688 d_parent_list[child] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
03689 d_parent_list[child]->push_back(parent);
03690 }
03691 else{
03692 iter->second->push_back(parent);
03693 }
03694 }
03695 }
03696
03697 void TheoryQuant::collectChangedTerms(CDList<Expr>& changed){
03698 ExprMap<bool> eqs_hash;
03699 ExprMap<bool> changed_hash;
03700
03701
03702
03703
03704
03705
03706
03707
03708
03709
03710
03711
03712
03713
03714
03715
03716
03717
03718
03719
03720
03721 for(size_t i=d_eqs_pos; i<d_eqs.size(); i++){
03722 eqs_hash[d_eqs[i]]=true;
03723 }
03724 d_eqs_pos.set(d_eqs.size());
03725 {
03726 for(ExprMap<bool>::iterator iter = eqs_hash.begin(), iter_end = eqs_hash.end(); iter != iter_end; iter++){
03727 const Expr& cur_ex = iter->first;
03728 ExprMap<CDList<Expr>* >::iterator iter_parent = d_parent_list.find(cur_ex);
03729 if(d_parent_list.end() != iter_parent){
03730 CDList<Expr>* cur_parents = iter_parent->second;
03731 for(size_t i=0; i<cur_parents->size(); i++){
03732 changed_hash[(*cur_parents)[i]]=true;
03733 }
03734 }
03735 }
03736 }
03737 {
03738 for(ExprMap<bool>::iterator iter = changed_hash.begin(), iter_end = changed_hash.end(); iter != iter_end; iter++){
03739 changed.push_back(iter->first);
03740 }
03741 }
03742 }
03743
03744
03745
03746
03747
03748
03749
03750
03751
03752
03753
03754
03755
03756
03757
03758
03759
03760
03761
03762
03763
03764
03765
03766
03767
03768
03769
03770
03771
03772
03773
03774
03775
03776
03777
03778
03779
03780
03781
03782
03783
03784
03785
03786
03787
03788
03789
03790
03791
03792
03793
03794
03795
03796
03797
03798
03799
03800
03801
03802
03803
03804
03805
03806
03807
03808
03809
03810
03811
03812
03813
03814
03815
03816
03817
03818
03819 inline bool TheoryQuant::multMatchChild(const Expr& gterm, const Expr& vterm, vector<ExprMap<Expr> >& binds, bool top){
03820 if(gterm.arity() != vterm.arity()) {
03821 TRACE("multmatch", "not same kind", gterm , vterm);
03822 return false;
03823 }
03824
03825
03826
03827 vector<Expr> allGterms;
03828 allGterms.push_back(gterm);
03829
03830
03831 if(!gterm.getSig().isNull() ){
03832 Expr gtermSig = gterm.getSig().getRHS();
03833 if(!top && gterm.hasFind() && !gterm.isAtomicFormula() ) {
03834 Expr curCandidateGterm = gterm.getEqNext().getRHS();
03835 while (curCandidateGterm != gterm){
03836 if(getHead(curCandidateGterm) == getHead(gterm)
03837 && !curCandidateGterm.getSig().isNull()
03838 && curCandidateGterm.getSig().getRHS() != gtermSig
03839 && getExprScore(curCandidateGterm) <= d_curMaxExprScore
03840 ){
03841 allGterms.push_back(curCandidateGterm);
03842 }
03843 curCandidateGterm = curCandidateGterm.getEqNext().getRHS();
03844 }
03845 }
03846 }
03847
03848
03849 vector<ExprMap<Expr> > returnBinds;
03850 for(size_t curGtermIndex =0; curGtermIndex < allGterms.size(); curGtermIndex++)
03851 {
03852 vector<ExprMap<Expr> > currentBinds(binds);
03853
03854 if(0 == currentBinds.size()){
03855 ExprMap<Expr> emptyEnv;
03856 currentBinds.push_back(emptyEnv);
03857 }
03858
03859 Expr gterm = allGterms[curGtermIndex];
03860
03861 vector<ExprMap<Expr> > nextBinds;
03862
03863 for(int i = 0 ; i< gterm.arity(); i++){
03864 const Expr& curVterm = vterm[i];
03865 const Expr& curGterm = gterm[i];
03866
03867 for(size_t curEnvIndex =0; curEnvIndex < currentBinds.size(); curEnvIndex++){
03868
03869 ExprMap<Expr>& curEnv(currentBinds[curEnvIndex]);
03870 if(BOUND_VAR == curVterm.getKind()){
03871 ExprMap<Expr>::iterator iterVterm = curEnv.find(curVterm);
03872 if ( iterVterm != curEnv.end()){
03873 if (simplifyExpr(curGterm) == simplifyExpr(iterVterm->second)){
03874 nextBinds.push_back(curEnv);
03875 }
03876 }
03877 else {
03878 curEnv[curVterm] = simplifyExpr(curGterm);
03879 nextBinds.push_back(curEnv);
03880 }
03881 }
03882 else if (!curVterm.containsBoundVar()){
03883 if(simplifyExpr(curVterm) == simplifyExpr(curGterm)){
03884 nextBinds.push_back(curEnv);
03885 }
03886 }
03887 else{
03888 vector<ExprMap<Expr> > newBinds;
03889 newBinds.push_back(curEnv);
03890 bool goodChild = recMultMatch(curGterm, curVterm, newBinds);
03891 if(goodChild){
03892 for(vector<ExprMap<Expr> >::iterator i = newBinds.begin(), iend = newBinds.end(); i != iend; i++){
03893 nextBinds.push_back(*i);
03894 }
03895 }
03896 }
03897 }
03898 currentBinds = nextBinds;
03899 nextBinds.clear();
03900 }
03901 for(size_t curBindsIndex=0; curBindsIndex < currentBinds.size(); curBindsIndex++){
03902 returnBinds.push_back(currentBinds[curBindsIndex]);
03903 }
03904
03905 }
03906
03907
03908 binds = returnBinds;
03909 return (binds.size() > 0) ? true : false;
03910 }
03911
03912
03913
03914 inline bool TheoryQuant::multMatchTop(const Expr& gterm, const Expr& vterm, vector<ExprMap<Expr> >& binds){
03915 vector<ExprMap<Expr> > currentBinds(binds);
03916
03917 if(0 == currentBinds.size()){
03918 ExprMap<Expr> emptyEnv;
03919 currentBinds.push_back(emptyEnv);
03920 }
03921
03922 vector<ExprMap<Expr> > nextBinds;
03923
03924 const Expr& curVterm = vterm;
03925 const Expr& curGterm = gterm;
03926
03927 for(size_t curEnvIndex =0; curEnvIndex < currentBinds.size(); curEnvIndex++){
03928 ExprMap<Expr>& curEnv(currentBinds[curEnvIndex]);
03929 vector<ExprMap<Expr> > newBinds;
03930 newBinds.push_back(curEnv);
03931 bool goodChild = recMultMatch(curGterm, curVterm, newBinds);
03932 if(goodChild){
03933 for(vector<ExprMap<Expr> >::iterator i = newBinds.begin(), iend = newBinds.end(); i != iend; i++){
03934 nextBinds.push_back(*i);
03935 }
03936 }
03937 }
03938 binds = nextBinds;
03939 return (binds.size() > 0) ? true : false;
03940 }
03941
03942
03943
03944 void TheoryQuant::matchListOld(const CDList<Expr>& glist, size_t gbegin, size_t gend){
03945 for(size_t g_index = gbegin; g_index < gend; g_index++){
03946
03947 const Expr& gterm = glist[g_index];
03948
03949 if(gterm.isEq()){
03950 continue;
03951 }
03952
03953 if(gterm.getSig().isNull() ){
03954 if ( ! ( (gterm.hasFind() && !canGetHead(gterm.getFind().getRHS())) || gterm.getType().isBool() ) ){
03955
03956
03957
03958 continue;
03959 }
03960 }
03961
03962 Expr head = getHead(gterm);
03963
03964 ExprMap<CDMap<Expr, CDList<dynTrig>* > *>::iterator iter = d_allmap_trigs.find(head);
03965 if(d_allmap_trigs.end() == iter) continue;
03966 CDMap<Expr, CDList<dynTrig>*>* cd_map = iter->second;
03967
03968
03969
03970
03971
03972
03973 CDMap<Expr, CDList<dynTrig>*>::iterator iter_trig = (*cd_map).begin();
03974 CDMap<Expr, CDList<dynTrig>*>::iterator iter_trig_end = (*cd_map).end();
03975
03976 for(;iter_trig != iter_trig_end; iter_trig++){
03977 CDList<dynTrig>* cur_list = (*iter_trig).second;
03978 if(1 == cur_list->size() || null_expr == head || gterm.getType().isBool() ){
03979 for(size_t cur_index =0; cur_index < cur_list->size(); cur_index++){
03980
03981 const Trigger& cur_trig = (*cur_list)[cur_index].trig;
03982 size_t univ_id = (*cur_list)[cur_index].univ_id;
03983 vector<ExprMap<Expr> > binds;
03984 const Expr& vterm = cur_trig.trig;
03985 if(vterm.getKind() != gterm.getKind()) continue;
03986
03987
03988
03989
03990
03991
03992 if ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans && !cur_trig.isMulti) continue;
03993
03994
03995 newTopMatch(gterm, vterm, binds, cur_trig);
03996
03997 for(size_t i=0; i<binds.size(); i++){
03998 ExprMap<Expr>& cur_map = binds[i];
03999 vector<Expr> bind_vec;
04000 const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
04001 for(size_t j=0; j< bVarsThm.size(); j++){
04002 bind_vec.push_back(cur_map[bVarsThm[j]]);
04003 }
04004 synNewInst(univ_id, bind_vec, gterm, cur_trig);
04005 }
04006 }
04007 }
04008 else if ( cur_list->size() > 1){
04009
04010 const Trigger& cur_trig = (*cur_list)[0].trig;
04011
04012 const Expr& general_vterm = (*iter_trig).first;
04013
04014
04015
04016 if(general_vterm.getKind() != gterm.getKind()) continue;
04017 vector<ExprMap<Expr> > binds;
04018
04019
04020
04021
04022 if ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans && !cur_trig.isMulti) continue;
04023
04024
04025 newTopMatch(gterm, general_vterm, binds, cur_trig);
04026
04027 for(size_t bindsIndex = 0 ; bindsIndex < binds.size() ; bindsIndex++){
04028
04029 }
04030
04031 if(binds.size() <= 0) continue;
04032
04033 for(size_t trig_index = 0; trig_index< cur_list->size(); trig_index++){
04034 size_t univ_id = (*cur_list)[trig_index].univ_id;
04035 const ExprMap<Expr>& trig_map = (*cur_list)[trig_index].binds;
04036 const Trigger& ind_cur_trig = (*cur_list)[trig_index].trig;
04037 for(size_t i=0; i<binds.size(); i++){
04038 ExprMap<Expr>& cur_map = binds[i];
04039 vector<Expr> bind_vec;
04040 const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
04041 for(size_t j=0; j< bVarsThm.size(); j++){
04042 const Expr& inter=(*(trig_map.find(bVarsThm[j]))).second;
04043 const Expr& inter2 = cur_map[inter];
04044 bind_vec.push_back(inter2);
04045 }
04046
04047
04048 synNewInst(univ_id, bind_vec, gterm, ind_cur_trig);
04049 }
04050
04051 }
04052 }
04053 else{
04054 FatalAssert(false, "error in matchlistold");
04055 }
04056 }
04057 }
04058 }
04059
04060 void TheoryQuant::delNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs){
04061
04062 ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator i = new_trigs.begin();
04063 ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator iend = new_trigs.end();
04064 for(; i!=iend; i++){
04065 ExprMap<std::vector<dynTrig>*>* cur_new_cd_map = i->second;
04066 ExprMap<vector<dynTrig>* >::iterator j = cur_new_cd_map->begin();
04067 ExprMap<vector<dynTrig>* >::iterator jend = cur_new_cd_map->end();
04068 for(; j!=jend; j++){
04069 Expr general_trig = j->first;
04070 vector<dynTrig>* trigs = j->second;
04071 delete trigs;
04072 }
04073 delete cur_new_cd_map;
04074 }
04075 new_trigs.clear();
04076 }
04077
04078
04079 void TheoryQuant::combineOldNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs){
04080 ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator i = new_trigs.begin();
04081 ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator iend = new_trigs.end();
04082 for(; i!=iend; i++){
04083 ExprMap<std::vector<dynTrig>*>* cur_new_cd_map = i->second;
04084 Expr head = i->first;
04085 ExprMap<CDMap<Expr, CDList<dynTrig>* >* >::iterator old_iter = d_allmap_trigs.find(head);
04086 if(d_allmap_trigs.end() == old_iter){
04087 CDMap<Expr, CDList<dynTrig>* >* old_cd_map =
04088
04089 new(false) CDMap<Expr, CDList<dynTrig>* > (theoryCore()->getCM()->getCurrentContext());
04090 d_allmap_trigs[head] = old_cd_map;
04091 ExprMap<vector<dynTrig>* >::iterator j = cur_new_cd_map->begin();
04092 ExprMap<vector<dynTrig>* >::iterator jend = cur_new_cd_map->end();
04093 for(; j!=jend; j++){
04094 Expr general_trig = j->first;
04095 vector<dynTrig>* trigs = j->second;
04096 CDList<dynTrig>* old_cd_list =
04097
04098 new(false) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
04099 (*old_cd_map)[general_trig] = old_cd_list;
04100 for(size_t k=0; k<trigs->size(); k++){
04101 (*old_cd_list).push_back((*trigs)[k]);
04102
04103 }
04104
04105 }
04106
04107 }
04108 else{
04109 CDMap<Expr, CDList<dynTrig>* >* old_cd_map = old_iter->second;
04110 ExprMap<std::vector<dynTrig>*>::iterator j = cur_new_cd_map->begin();
04111 ExprMap<std::vector<dynTrig>*>::iterator jend = cur_new_cd_map->end();
04112 for(; j!=jend; j++){
04113 Expr general_trig = j->first;
04114 vector<dynTrig>* trigs = j->second;
04115 CDMap<Expr, CDList<dynTrig>* >::iterator old_trigs_iter = old_cd_map->find(general_trig);
04116 CDList<dynTrig>* old_cd_list;
04117 if(old_cd_map->end() == old_trigs_iter){
04118 old_cd_list =
04119
04120 new(false) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
04121 (*old_cd_map)[general_trig] = old_cd_list;
04122 }
04123 else{
04124 old_cd_list = (*old_trigs_iter).second;
04125 }
04126 for(size_t k=0; k<trigs->size(); k++){
04127 (*old_cd_list).push_back((*trigs)[k]);
04128
04129 }
04130
04131 }
04132
04133 }
04134 }
04135 delNewTrigs(new_trigs);
04136 new_trigs.clear();
04137 }
04138
04139
04140 void TheoryQuant::matchListNew(ExprMap<ExprMap<vector<dynTrig>*>*>& new_trigs,
04141 const CDList<Expr>& glist,
04142 size_t gbegin,
04143 size_t gend){
04144
04145
04146 for(size_t g_index = gbegin; g_index<gend; g_index++){
04147
04148 const Expr& gterm = glist[g_index];
04149
04150 if(gterm.isEq()){
04151 continue;
04152 }
04153
04154 if(gterm.getSig().isNull()){
04155
04156
04157
04158 }
04159
04160 Expr head = getHead(gterm);
04161
04162 ExprMap<ExprMap<vector<dynTrig>* > *>::iterator iter = new_trigs.find(head);
04163 if(new_trigs.end() == iter) continue;
04164 ExprMap<vector<dynTrig>*>* cd_map = iter->second;
04165
04166
04167
04168
04169
04170 ExprMap<vector<dynTrig>*>::iterator iter_trig = (*cd_map).begin();
04171 ExprMap<vector<dynTrig>*>::iterator iter_trig_end = (*cd_map).end();
04172
04173 for(;iter_trig != iter_trig_end; iter_trig++){
04174
04175 vector<dynTrig>* cur_list = (*iter_trig).second;
04176 if(1 == cur_list->size() || null_expr == head || gterm.getType().isBool() ){
04177 for(size_t cur_index =0; cur_index < cur_list->size(); cur_index++){
04178 const Trigger& cur_trig = (*cur_list)[cur_index].trig;
04179
04180
04181
04182
04183
04184 if ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans) continue;
04185
04186 size_t univ_id = (*cur_list)[cur_index].univ_id;
04187 vector<ExprMap<Expr> > binds;
04188 const Expr& vterm = cur_trig.trig;
04189 if(vterm.getKind() != gterm.getKind()) continue;
04190 newTopMatch(gterm, vterm, binds, cur_trig);
04191 for(size_t i=0; i<binds.size(); i++){
04192 ExprMap<Expr>& cur_map = binds[i];
04193 vector<Expr> bind_vec;
04194 const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
04195 for(size_t j=0; j< bVarsThm.size(); j++){
04196 bind_vec.push_back(cur_map[bVarsThm[j]]);
04197 }
04198 synNewInst(univ_id, bind_vec, gterm, cur_trig);
04199 }
04200 }
04201 }
04202 else if ( cur_list->size() > 1){
04203
04204 const Trigger& cur_trig = (*cur_list)[0].trig;
04205
04206
04207
04208
04209
04210
04211
04212 const Expr& general_vterm = (*iter_trig).first;
04213 if(general_vterm.getKind() != gterm.getKind()) continue;
04214 vector<ExprMap<Expr> > binds;
04215 newTopMatch(gterm, general_vterm, binds, cur_trig);
04216
04217 if(binds.size() <= 0) continue;
04218 for(size_t trig_index = 0; trig_index< cur_list->size(); trig_index++){
04219 size_t univ_id = (*cur_list)[trig_index].univ_id;
04220 const Trigger& ind_cur_trig = (*cur_list)[trig_index].trig;
04221 const ExprMap<Expr>& trig_map = (*cur_list)[trig_index].binds;
04222
04223 for(size_t i=0; i<binds.size(); i++){
04224 ExprMap<Expr>& cur_map = binds[i];
04225 vector<Expr> bind_vec;
04226 const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
04227 for(size_t j=0; j< bVarsThm.size(); j++){
04228 const Expr& inter=(*(trig_map.find(bVarsThm[j]))).second;
04229 const Expr& inter2 = cur_map[inter];
04230 bind_vec.push_back(inter2);
04231 }
04232 synNewInst(univ_id, bind_vec, gterm, ind_cur_trig);
04233 }
04234 }
04235 }
04236 else{
04237 FatalAssert(false, "error in matchlistnew");
04238 }
04239 }
04240 }
04241 }
04242
04243
04244
04245
04246 void TheoryQuant::newTopMatchNoSig(const Expr& gterm,
04247 const Expr& vterm,
04248 vector<ExprMap<Expr> >& binds,
04249 const Trigger& trig){
04250
04251
04252
04253 if(trig.isSuperSimple){
04254 ExprMap<Expr> cur_bind;
04255 for(int i = vterm.arity()-1; i>=0 ; i--){
04256 cur_bind[vterm[i]] = simplifyExpr(gterm[i]);
04257 }
04258 binds.push_back(cur_bind);
04259 return;
04260 }
04261
04262 if(trig.isSimple){
04263 ExprMap<Expr> cur_bind;
04264 for(int i = vterm.arity()-1; i>=0 ; i--){
04265 if(BOUND_VAR != vterm[i].getKind()){
04266 if(simplifyExpr(gterm[i]) != simplifyExpr(vterm[i])) {
04267 return ;
04268 }
04269 }
04270 else{
04271 if(getBaseType(vterm[i]) == (getBaseType(gterm[i]))){
04272 cur_bind[vterm[i]] = simplifyExpr(gterm[i]);
04273 }
04274 else return;
04275 }
04276 }
04277 binds.push_back(cur_bind);
04278 return;
04279 }
04280
04281 if(!isSysPred(vterm)){
04282 if(!gterm.getType().isBool()){
04283
04284 multMatchChild(gterm, vterm, binds, true);
04285 return;
04286 }
04287
04288
04289
04290 multMatchChild(gterm, vterm, binds, true);
04291 return;
04292
04293 if(!*d_usePolarity){
04294
04295 multMatchChild(gterm, vterm, binds);
04296 return;
04297 }
04298
04299 const bool gtrue = (trueExpr()==findExpr(gterm));
04300
04301 if(gtrue ){
04302 if((Neg==trig.polarity || PosNeg==trig.polarity)) {
04303
04304 multMatchChild(gterm, vterm, binds);
04305 return;
04306 }
04307 else{
04308
04309 return;
04310 }
04311 }
04312 const bool gfalse = (falseExpr()==findExpr(gterm));
04313
04314 if(gfalse){
04315 if((Pos==trig.polarity || PosNeg==trig.polarity)) {
04316
04317 multMatchChild(gterm, vterm, binds);
04318 return;
04319 }
04320 else{
04321
04322 return;
04323 }
04324 }
04325
04326
04327
04328
04329
04330
04331
04332 multMatchChild(gterm, vterm, binds);
04333
04334 return;
04335 }
04336 else{
04337
04338 Expr gl = getLeft(gterm[1]);
04339 Expr gr = getRight(gterm[1]);
04340
04341 if(null_expr == gr || null_expr == gl){
04342 gl = gterm[0];
04343 gr = gterm[1];
04344 }
04345
04346 Expr vr, vl;
04347 Expr tvr, tvl;
04348
04349 tvr=null_expr;
04350 tvl=null_expr;
04351
04352 if(isGE(vterm) || isGT(vterm)){
04353 vr = vterm[0];
04354 vl = vterm[1];
04355 }
04356 else if(isLE(vterm) || isLT(vterm)){
04357 vr = vterm[1];
04358 vl = vterm[0];
04359 }
04360 else{
04361 FatalAssert(false, "impossilbe in toppred");
04362 }
04363
04364 if(isIntx(vl,0)){
04365 tvl = getLeft(vr);
04366 tvr = getRight(vr);
04367 }
04368 else if(isIntx(vr,0)) {
04369 tvl = getLeft(vl);
04370 tvr = getRight(vl);
04371 }
04372
04373 if( (null_expr != tvl) && (null_expr != tvr)){
04374 vl = tvl;
04375 vr = tvr;
04376 }
04377
04378
04379 const bool gtrue = (trueExpr()==findExpr(gterm));
04380 const bool gfalse = (falseExpr()==findExpr(gterm));
04381
04382 TRACE("quant toppred"," vl, gl, vr, gr:", vl.toString()+"::"+gl.toString()+"||", vr.toString()+"::"+gr.toString());
04383
04384
04385
04386 if(!*d_usePolarity){
04387 if((multMatchTop(gl, vl, binds) && multMatchTop(gr, vr, binds))){
04388 return;
04389 }
04390 else{
04391 return;
04392 }
04393 }
04394 if((Neg==trig.polarity || PosNeg==trig.polarity)) {
04395 if (( gtrue ) ) {
04396 if (multMatchTop(gl, vl, binds) && multMatchTop(gr, vr, binds)){
04397 return;
04398 }
04399 else{
04400 return;
04401 }
04402 }
04403 else {
04404 if(multMatchTop(gl, vr, binds) && multMatchTop(gr, vl, binds)){
04405 return;
04406 }
04407 else{
04408 return;
04409 }
04410 }
04411 }
04412 else if((Pos==trig.polarity || PosNeg==trig.polarity)) {
04413 if (( gfalse )) {
04414 if(multMatchTop(gl, vl, binds) && multMatchTop(gr, vr, binds)){
04415 return;
04416 }
04417 else{
04418 return;
04419 }
04420 }
04421 else {
04422 if(multMatchTop(gl, vr, binds) && multMatchTop(gr, vl, binds)){
04423 return;
04424 }
04425 else{
04426 return;
04427 }
04428 }
04429 }
04430 else {
04431 if((multMatchTop(gl, vl, binds) && multMatchTop(gr, vr, binds))){
04432
04433 return;
04434 }
04435 else{
04436 return;
04437 }
04438 return;
04439 }
04440 }
04441 }
04442
04443
04444
04445
04446
04447
04448
04449
04450
04451
04452
04453
04454
04455
04456
04457
04458
04459
04460
04461 void TheoryQuant::newTopMatch(const Expr& gtermOrg,
04462 const Expr& vterm,
04463 vector<ExprMap<Expr> >& binds,
04464 const Trigger& trig){
04465
04466
04467
04468 return newTopMatchNoSig(gtermOrg,vterm, binds, trig);
04469
04470
04471
04472
04473
04474
04475
04476
04477
04478
04479
04480
04481
04482
04483
04484
04485
04486 vector<ExprMap<Expr> > oldBinds;
04487 newTopMatchNoSig(gtermOrg,vterm, oldBinds, trig);
04488 vector<ExprMap<Expr> > newBinds;
04489 newTopMatchSig(gtermOrg,vterm, newBinds, trig);
04490
04491 vector<ExprMap<Expr> > oldBindsBack(oldBinds);
04492 vector<ExprMap<Expr> > newBindsBack(newBinds);
04493
04494 simplifyVectorExprMap(oldBinds);
04495 simplifyVectorExprMap(newBinds);
04496
04497 if (false && oldBinds != newBinds){
04498
04499 cout<<"let us see" << endl;
04500 cout<< "===gterm is : " << gtermOrg << endl ;;
04501
04502
04503
04504 if(gtermOrg.isApply() && gtermOrg.hasSig()){
04505 Expr sig = gtermOrg.getSig().getRHS();
04506 cout << "\n---gterm sig is: " << sig << endl;
04507
04508
04509
04510 }
04511
04512
04513
04514
04515 for(size_t oldBindsIndex = 0; oldBindsIndex < oldBinds.size(); oldBindsIndex++){
04516 cout << "--O- " << oldBindsIndex << endl;
04517 cout << exprMap2string(oldBindsBack[oldBindsIndex]) << endl;
04518 cout << exprMap2string(oldBinds[oldBindsIndex]) << endl;
04519 cout << exprMap2stringSimplify(oldBinds[oldBindsIndex]) << endl;
04520 cout << exprMap2stringSig(oldBinds[oldBindsIndex]) << endl;
04521 }
04522
04523 for(size_t newBindsIndex = 0; newBindsIndex < newBinds.size(); newBindsIndex++){
04524 cout << "--N- " << newBindsIndex << endl;
04525 cout << exprMap2string(newBindsBack[newBindsIndex]) << endl;
04526 cout << exprMap2string(newBinds[newBindsIndex]) << endl;
04527 cout << exprMap2stringSimplify(newBinds[newBindsIndex]) << endl;
04528 cout << exprMap2stringSig(newBinds[newBindsIndex]) << endl;
04529 }
04530
04531 }
04532
04533
04534
04535
04536 binds = oldBinds;
04537 return;
04538 }
04539
04540 void TheoryQuant::newTopMatchSig(const Expr& gtermOrg,
04541 const Expr& vterm,
04542 vector<ExprMap<Expr> >& binds,
04543 const Trigger& trig){
04544
04545
04546 Expr gterm;
04547 if(gtermOrg.isApply() && gtermOrg.hasSig()){
04548 gterm = gtermOrg.getSig().getRHS();
04549 }
04550 else{
04551 gterm = gtermOrg;
04552 }
04553
04554
04555 if(trig.isSuperSimple){
04556 ExprMap<Expr> cur_bind;
04557 for(int i = vterm.arity()-1; i>=0 ; i--){
04558 cur_bind[vterm[i]] = simplifyExpr(gterm[i]);
04559 }
04560 binds.push_back(cur_bind);
04561 return;
04562 }
04563
04564 if(trig.isSimple){
04565 ExprMap<Expr> cur_bind;
04566 for(int i = vterm.arity()-1; i>=0 ; i--){
04567 if(BOUND_VAR != vterm[i].getKind()){
04568 if(simplifyExpr(gterm[i]) != simplifyExpr(vterm[i])) {
04569 return ;
04570 }
04571 }
04572 else{
04573 if (getBaseType(vterm[i])==getBaseType(gterm[i])){
04574 cur_bind[vterm[i]] = simplifyExpr(gterm[i]);
04575 }
04576 else return;
04577 }
04578 }
04579 binds.push_back(cur_bind);
04580 return;
04581 }
04582
04583 if(!isSysPred(vterm)){
04584 if(!gterm.getType().isBool()){
04585
04586 multMatchChild(gterm, vterm, binds);
04587 return;
04588 }
04589
04590
04591
04592
04593
04594
04595
04596
04597
04598 if(!*d_usePolarity || d_useManTrig){
04599
04600 multMatchChild(gterm, vterm, binds);
04601 return;
04602 }
04603
04604 const bool gtrue = (trueExpr()==findExpr(gterm));
04605
04606 if(gtrue ){
04607 if((Neg==trig.polarity || PosNeg==trig.polarity)) {
04608
04609 multMatchChild(gterm, vterm, binds);
04610 return;
04611 }
04612 else{
04613
04614 return;
04615 }
04616 }
04617 const bool gfalse = (falseExpr()==findExpr(gterm));
04618
04619 if(gfalse){
04620 if((Pos==trig.polarity || PosNeg==trig.polarity)) {
04621
04622 multMatchChild(gterm, vterm, binds);
04623 return;
04624 }
04625 else{
04626
04627 return;
04628 }
04629 }
04630
04631
04632 FatalAssert(false, "impossible");
04633 cout<<"impossible here in new top match"<<endl;
04634 cout<<"vterm "<<vterm<<endl;
04635 cout<<"gterm " <<gterm<<endl;
04636 cout<<trig.polarity<<endl;
04637 cout<<"gtrue and gfalse: " << gtrue<<" |and| " <<gfalse<<endl;
04638 return;
04639 multMatchChild(gterm, vterm, binds);
04640
04641 return;
04642 }
04643 else{
04644
04645 Expr gl = getLeft(gterm[1]);
04646 Expr gr = getRight(gterm[1]);
04647
04648 if(null_expr == gr || null_expr == gl){
04649 gl = gterm[0];
04650 gr = gterm[1];
04651 }
04652
04653 Expr vr, vl;
04654 Expr tvr, tvl;
04655
04656 tvr=null_expr;
04657 tvl=null_expr;
04658
04659 if(isGE(vterm) || isGT(vterm)){
04660 vr = vterm[0];
04661 vl = vterm[1];
04662 }
04663 else if(isLE(vterm) || isLT(vterm)){
04664 vr = vterm[1];
04665 vl = vterm[0];
04666 }
04667 else{
04668 FatalAssert(false, "impossilbe in toppred");
04669 }
04670
04671 if(isIntx(vl,0)){
04672 tvl = getLeft(vr);
04673 tvr = getRight(vr);
04674 }
04675 else if(isIntx(vr,0)) {
04676 tvl = getLeft(vl);
04677 tvr = getRight(vl);
04678 }
04679
04680 if( (null_expr != tvl) && (null_expr != tvr)){
04681 vl = tvl;
04682 vr = tvr;
04683 }
04684
04685
04686 const bool gtrue = (trueExpr()==findExpr(gterm));
04687 const bool gfalse = (falseExpr()==findExpr(gterm));
04688
04689 TRACE("quant toppred"," vl, gl, vr, gr:", vl.toString()+"::"+gl.toString()+"||", vr.toString()+"::"+gr.toString());
04690
04691
04692
04693 if(!*d_usePolarity){
04694 if((multMatchTop(gl, vl, binds) && multMatchTop(gr, vr, binds))){
04695 return;
04696 }
04697 else{
04698 return;
04699 }
04700 }
04701 if((Neg==trig.polarity || PosNeg==trig.polarity)) {
04702 if (( gtrue ) ) {
04703 if (multMatchTop(gl, vl, binds) && multMatchTop(gr, vr, binds)){
04704 return;
04705 }
04706 else{
04707 return;
04708 }
04709 }
04710 else {
04711 if(multMatchTop(gl, vr, binds) && multMatchTop(gr, vl, binds)){
04712 return;
04713 }
04714 else{
04715 return;
04716 }
04717 }
04718 }
04719 else if((Pos==trig.polarity || PosNeg==trig.polarity)) {
04720 if (( gfalse )) {
04721 if(multMatchTop(gl, vl, binds) && multMatchTop(gr, vr, binds)){
04722 return;
04723 }
04724 else{
04725 return;
04726 }
04727 }
04728 else {
04729 if(multMatchTop(gl, vr, binds) && multMatchTop(gr, vl, binds)){
04730 return;
04731 }
04732 else{
04733 return;
04734 }
04735 }
04736 }
04737 else {
04738 if((multMatchTop(gl, vl, binds) && multMatchTop(gr, vr, binds))){
04739
04740 return;
04741 }
04742 else{
04743 return;
04744 }
04745 return;
04746 }
04747 }
04748 }
04749
04750
04751
04752
04753
04754
04755
04756
04757
04758
04759
04760
04761
04762
04763
04764
04765
04766
04767
04768
04769
04770
04771
04772
04773
04774
04775
04776
04777
04778
04779
04780
04781
04782
04783
04784
04785
04786
04787
04788
04789
04790
04791
04792
04793
04794
04795
04796
04797
04798
04799
04800
04801
04802
04803
04804
04805
04806
04807
04808
04809
04810
04811
04812
04813
04814
04815
04816
04817
04818
04819
04820
04821
04822
04823
04824
04825
04826
04827
04828
04829
04830
04831
04832
04833
04834
04835
04836
04837
04838
04839
04840
04841
04842
04843
04844
04845
04846
04847
04848
04849
04850
04851
04852
04853
04854
04855
04856
04857
04858
04859
04860
04861
04862
04863
04864
04865
04866
04867
04868
04869
04870
04871
04872
04873
04874
04875
04876
04877
04878
04879
04880
04881
04882
04883
04884
04885
04886
04887
04888
04889
04890
04891
04892
04893
04894
04895
04896
04897
04898
04899
04900
04901
04902
04903
04904
04905
04906
04907
04908
04909
04910
04911
04912
04913
04914
04915
04916
04917
04918
04919
04920
04921
04922
04923
04924
04925
04926
04927
04928
04929
04930
04931
04932
04933
04934
04935
04936
04937
04938
04939
04940
04941
04942
04943
04944
04945
04946
04947
04948
04949
04950
04951
04952
04953
04954
04955
04956
04957
04958
04959
04960
04961
04962
04963
04964
04965
04966
04967
04968
04969
04970
04971
04972
04973
04974
04975
04976
04977
04978
04979
04980
04981
04982
04983
04984
04985
04986
04987
04988
04989
04990
04991
04992
04993
04994
04995
04996
04997
04998
04999
05000
05001
05002
05003
05004
05005
05006
05007
05008
05009
05010
05011
05012
05013
05014
05015
05016
05017
05018
05019
05020
05021
05022
05023
05024
05025
05026
05027
05028
05029
05030
05031
05032
05033
05034
05035
05036
05037
05038
05039
05040
05041
05042
05043
05044
05045
05046
05047
05048
05049
05050
05051
05052
05053
05054
05055
05056
05057
05058
05059
05060
05061
05062
05063
05064
05065
05066
05067
05068
05069
05070
05071
05072
05073
05074
05075
05076
05077
05078
05079
05080
05081
05082
05083
05084
05085
05086
05087
05088
05089
05090
05091
05092
05093
05094
05095
05096
05097
05098
05099
05100
05101
05102
05103
05104
05105
05106
05107
05108
05109
05110
05111
05112
05113
05114
05115
05116
05117
05118
05119
05120
05121
05122
05123
05124
05125
05126
05127
05128
05129
05130
05131
05132
05133
05134
05135
05136
05137
05138
05139
05140
05141
05142
05143
05144
05145
05146
05147
05148
05149
05150
05151
05152
05153
05154
05155
05156
05157
05158
05159
05160
05161
05162 bool cmpExpr( Expr e1, Expr e2){
05163
05164 if(e1.isNull()) return true;
05165 if(e2.isNull()) return false;
05166 return (e1.getIndex() < e2.getIndex());
05167 }
05168
05169
05170
05171
05172
05173
05174
05175
05176
05177
05178
05179 bool TheoryQuant::recMultMatchDebug(const Expr& gterm,const Expr& vterm, vector<ExprMap<Expr> >& binds){
05180
05181 TRACE("quant match", gterm , " VS ", vterm);
05182 DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
05183 DebugAssert (!isSysPred(vterm) && !isSysPred(gterm), "pred found in recMultMatch");
05184 DebugAssert (binds.size() == 1, "binds.size() > 1");
05185
05186
05187 if (BOUND_VAR == vterm.getKind() ) {
05188 ExprMap<Expr>& curEnv = binds[0];
05189 ExprMap<Expr>::iterator iterVterm = curEnv.find(vterm);
05190 if ( iterVterm != curEnv.end()){
05191 return (simplifyExpr(gterm) == simplifyExpr(iterVterm->second)) ? true : false ;
05192 }
05193 else {
05194 curEnv[vterm] = simplifyExpr(gterm);
05195 return true;
05196 }
05197 }
05198 else if (!vterm.containsBoundVar()){
05199 return (simplifyExpr(vterm) == simplifyExpr(gterm)) ? true : false ;
05200 }
05201 else{
05202 if(canGetHead(vterm)){
05203 Expr vhead = getHead(vterm);
05204 if(vterm.isAtomicFormula()){
05205
05206
05207
05208 if (canGetHead(gterm)) {
05209 if ( vhead != getHead(gterm) ){
05210 return false;
05211 }
05212 return multMatchChild(gterm, vterm, binds);
05213 }
05214 else{
05215 return false;
05216 }
05217 }
05218 if ( (canGetHead(gterm)) && vhead == getHead(gterm)){
05219 return multMatchChild(gterm, vterm, binds);
05220 }
05221
05222
05223
05224
05225
05226 ExprMap<Expr> orginalEnv = binds[0];
05227 vector<ExprMap<Expr> > candidateNewEnvs;
05228 bool newwayResult(false);
05229
05230 if(*d_useNewEqu){
05231 vector<Expr> candidateGterms;
05232 {
05233 Expr curCandidateGterm = gterm.getEqNext().getRHS();
05234 while (curCandidateGterm != gterm){
05235 DebugAssert(simplifyExpr(curCandidateGterm) == simplifyExpr(gterm), "curCandidateGterm != gterm");
05236
05237 if(getExprScore(curCandidateGterm) <= d_curMaxExprScore || true){
05238 candidateGterms.push_back(curCandidateGterm);
05239 }
05240 curCandidateGterm = curCandidateGterm.getEqNext().getRHS();
05241 }
05242 }
05243
05244
05245 for(size_t curGtermIndex = 0 ; curGtermIndex < candidateGterms.size(); curGtermIndex++){
05246 const Expr& curGterm = candidateGterms[curGtermIndex];
05247 if(getHead(curGterm) == vhead){
05248 vector<ExprMap<Expr> > newBinds;
05249 newBinds.push_back(orginalEnv);
05250 bool res = multMatchChild(curGterm, vterm, newBinds);
05251 if (res) {
05252
05253
05254
05255
05256 for(size_t newBindsIndex = 0; newBindsIndex < newBinds.size(); newBindsIndex++){
05257 candidateNewEnvs.push_back(newBinds[newBindsIndex]);
05258 }
05259
05260 }
05261 }
05262 }
05263
05264 if (candidateNewEnvs.size() >= 1){
05265
05266 newwayResult = true;
05267 }
05268 else{
05269 newwayResult = false;
05270 }
05271 }
05272
05273
05274 vector<ExprMap<Expr> > candidateOldEnvs;
05275
05276 if( d_same_head_expr.count(vhead) > 0 ) {
05277 const Expr& findGterm = simplifyExpr(gterm);
05278
05279 CDList<Expr>* gls = d_same_head_expr[vhead];
05280 for(size_t i = 0; i < gls->size(); i++){
05281 const Expr& curGterm = (*gls)[i];
05282 if(getExprScore(curGterm)> d_curMaxExprScore){
05283 continue;
05284 }
05285
05286 if (simplifyExpr(curGterm) == findGterm){
05287 DebugAssert((*gls)[i].arity() == vterm.arity(), "gls has different arity");
05288
05289 vector<ExprMap<Expr> > newBinds ;
05290 newBinds.push_back(orginalEnv);
05291 bool goodMatching(false);
05292 goodMatching = multMatchChild(curGterm, vterm, newBinds);
05293
05294 if(goodMatching){
05295
05296
05297 for(size_t newBindsIndex = 0; newBindsIndex < newBinds.size(); newBindsIndex++){
05298 candidateOldEnvs.push_back(newBinds[newBindsIndex]);
05299 }
05300
05301 }
05302 }
05303 }
05304 }
05305
05306 bool oldwayResult(false);
05307
05308 if(candidateOldEnvs.size() >= 1){
05309 oldwayResult = true;
05310 }
05311 else{
05312 oldwayResult = false;
05313 }
05314
05315
05316
05317 if( candidateNewEnvs.size() != candidateOldEnvs.size()){
05318 ;
05319
05320 }
05321
05322 if(oldwayResult != newwayResult){
05323 ;
05324
05325 }
05326
05327
05328 binds = candidateOldEnvs;
05329
05330 return oldwayResult;
05331 }
05332 else{
05333 if( (gterm.getKind() == vterm.getKind()) &&
05334 (gterm.arity() == vterm.arity()) &&
05335 gterm.arity()>0 ){
05336
05337 return multMatchChild(gterm, vterm, binds);
05338 }
05339 else {
05340 return false;
05341 }
05342 }
05343 }
05344 return false;
05345 }
05346
05347 bool TheoryQuant::recMultMatchOldWay(const Expr& gterm,const Expr& vterm, vector<ExprMap<Expr> >& binds){
05348
05349 TRACE("quant match", "==recMultMatch\n", "---"+gterm.toString(), "\n+++"+vterm.toString());
05350 DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
05351 DebugAssert (!isSysPred(vterm) && !isSysPred(gterm), "pred found in recMultMatch");
05352 DebugAssert (binds.size() == 1, "binds.size() > 1");
05353
05354
05355 if (BOUND_VAR == vterm.getKind() ) {
05356 ExprMap<Expr>& curEnv = binds[0];
05357 ExprMap<Expr>::iterator iterVterm = curEnv.find(vterm);
05358 if ( iterVterm != curEnv.end()){
05359 return (simplifyExpr(gterm) == simplifyExpr(iterVterm->second)) ? true : false ;
05360 }
05361 else {
05362 curEnv[vterm] = simplifyExpr(gterm);
05363 return true;
05364 }
05365 }
05366 else if (!vterm.containsBoundVar()){
05367 return (simplifyExpr(vterm) == simplifyExpr(gterm)) ? true : false ;
05368 }
05369 else{
05370 if(canGetHead(vterm)){
05371 Expr vhead = getHead(vterm);
05372 if(vterm.isAtomicFormula()){
05373 if (canGetHead(gterm)) {
05374 if ( vhead != getHead(gterm) ){
05375 return false;
05376 }
05377 return multMatchChild(gterm, vterm, binds);
05378 }
05379 else{
05380 return false;
05381 }
05382 }
05383 if ( (canGetHead(gterm)) && vhead == getHead(gterm)){
05384 return multMatchChild(gterm, vterm, binds);
05385 }
05386
05387 TRACE("quant multmatch", "-- begin multi equality matching -- ", "" ,"");
05388 TRACE("quant multmatch", "vterm: " , vterm, "");
05389 TRACE("quant multmatch", "gterm: " , gterm, "");
05390
05391 ExprMap<Expr> orginalEnv = binds[0];
05392
05393 vector<ExprMap<Expr> > candidateOldEnvs;
05394
05395 if( d_same_head_expr.count(vhead) > 0 ) {
05396 const Expr& findGterm = simplifyExpr(gterm);
05397 TRACE("quant multmatch", "simp gterm: " , simplifyExpr(gterm), "");
05398
05399 CDList<Expr>* gls = d_same_head_expr[vhead];
05400 for(size_t i = 0; i < gls->size(); i++){
05401 const Expr& curGterm = (*gls)[i];
05402 if(getExprScore(curGterm)> d_curMaxExprScore){
05403 continue;
05404 }
05405 TRACE("quant multmatch", "same head term ", curGterm, "");
05406 TRACE("quant multmatch", "simp same head term ", simplifyExpr(curGterm), "");
05407 if (simplifyExpr(curGterm) == findGterm){
05408 DebugAssert((*gls)[i].arity() == vterm.arity(), "gls has different arity");
05409 vector<ExprMap<Expr> > newBinds ;
05410 newBinds.push_back(orginalEnv);
05411 bool goodMatching(false);
05412 goodMatching = multMatchChild(curGterm, vterm, newBinds);
05413
05414 if(goodMatching){
05415 TRACE("quant multmatch", "old curGterm: ", curGterm, "");
05416 TRACE("quant multmatch", "old simplifed curGterm: ", simplifyExpr(curGterm), "");
05417 for(size_t newBindsIndex = 0; newBindsIndex < newBinds.size(); newBindsIndex++){
05418 candidateOldEnvs.push_back(newBinds[newBindsIndex]);
05419 }
05420 TRACE("quant multmatch", "pushed oldEnvs " , newBinds.size(), "");
05421 }
05422 }
05423 }
05424 }
05425
05426 bool oldwayResult(false);
05427
05428 if(candidateOldEnvs.size() >= 1){
05429 oldwayResult = true;
05430 }
05431 else{
05432 oldwayResult = false;
05433 }
05434
05435 TRACE("quant multmatch", "old env size" ,candidateOldEnvs.size(), "");
05436 binds = candidateOldEnvs;
05437 return oldwayResult;
05438 }
05439 else{
05440 if( (gterm.getKind() == vterm.getKind()) &&
05441 (gterm.arity() == vterm.arity()) &&
05442 gterm.arity()>0 ){
05443 return multMatchChild(gterm, vterm, binds);
05444 }
05445 else {
05446 return false;
05447 }
05448 }
05449 }
05450 return false;
05451 }
05452
05453
05454
05455
05456 bool TheoryQuant::recMultMatch(const Expr& gterm,const Expr& vterm, vector<ExprMap<Expr> >& binds){
05457 TRACE("quant match", gterm , " VS ", vterm);
05458 DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
05459 DebugAssert (!isSysPred(vterm) && !isSysPred(gterm), "pred found in recMultMatch");
05460 DebugAssert (binds.size() == 1, "binds.size() > 1");
05461
05462 if (BOUND_VAR == vterm.getKind() ) {
05463 ExprMap<Expr>& curEnv = binds[0];
05464 ExprMap<Expr>::iterator iterVterm = curEnv.find(vterm);
05465 if ( iterVterm != curEnv.end()){
05466 return (simplifyExpr(gterm) == simplifyExpr(iterVterm->second)) ? true : false ;
05467 }
05468 else {
05469 curEnv[vterm] = simplifyExpr(gterm);
05470 return true;
05471 }
05472 }
05473 else if (!vterm.containsBoundVar()){
05474 return (simplifyExpr(vterm) == simplifyExpr(gterm)) ? true : false ;
05475 }
05476 else{
05477 if(canGetHead(vterm)){
05478 Expr vhead = getHead(vterm);
05479 if(vterm.isAtomicFormula()){
05480 if (canGetHead(gterm)) {
05481 if ( vhead != getHead(gterm) ){
05482 return false;
05483 }
05484 return multMatchChild(gterm, vterm, binds);
05485 }
05486 else{
05487 return false;
05488 }
05489 }
05490 if ( (canGetHead(gterm)) && vhead == getHead(gterm)){
05491
05492 return multMatchChild(gterm, vterm, binds);
05493 }
05494
05495 TRACE("quant multmatch", "-- begin multi equality matching -- ", "" ,"");
05496 TRACE("qunat multmatch", "vterm: " , vterm, "");
05497 TRACE("qunat multmatch", "gterm: " , gterm, "");
05498
05499 ExprMap<Expr> orginalEnv = binds[0];
05500 vector<ExprMap<Expr> > candidateNewEnvs;
05501 bool newwayResult(false);
05502
05503 if(*d_useNewEqu){
05504 vector<Expr> candidateGterms;
05505 {
05506 if(!gterm.hasFind()) {
05507 return false;
05508 }
05509 Expr curCandidateGterm = gterm.getEqNext().getRHS();
05510 while (curCandidateGterm != gterm){
05511 DebugAssert(simplifyExpr(curCandidateGterm) == simplifyExpr(gterm), "curCandidateGterm != gterm");
05512 TRACE("quant multmatch", "pushed candidate gterm ", getExprScore(curCandidateGterm), " # " + curCandidateGterm.toString());
05513
05514 if(getExprScore(curCandidateGterm) <= d_curMaxExprScore || true ){
05515 candidateGterms.push_back(curCandidateGterm);
05516 }
05517 curCandidateGterm = curCandidateGterm.getEqNext().getRHS();
05518 }
05519 }
05520 for(size_t curGtermIndex = 0 ; curGtermIndex < candidateGterms.size(); curGtermIndex++){
05521 const Expr& curGterm = candidateGterms[curGtermIndex];
05522 if(getHead(curGterm) == vhead){
05523 vector<ExprMap<Expr> > newBinds;
05524 newBinds.push_back(orginalEnv);
05525 bool res = multMatchChild(curGterm, vterm, newBinds, true);
05526 if (res) {
05527 TRACE("quant multmatch", "found new match: ", "" ,"");
05528 TRACE("quant multmatch", "curGterm: ", curGterm , "");
05529 TRACE("quant multmatch", "simplified Gterm: ", simplifyExpr(gterm), "" );
05530 TRACE("quant multmatch", "simplified curGterm: ", simplifyExpr(curGterm), "");
05531 for(size_t newBindsIndex = 0; newBindsIndex < newBinds.size(); newBindsIndex++){
05532 candidateNewEnvs.push_back(newBinds[newBindsIndex]);
05533 }
05534 TRACE("quant multmathc", "pushed newEnvs ", newBinds.size(), "");
05535 }
05536 }
05537 }
05538
05539 if (candidateNewEnvs.size() >= 1){
05540 TRACE("quant multmacht", "found more matcings: " , candidateNewEnvs.size(), "");
05541 newwayResult = true;
05542 }
05543 else{
05544 newwayResult = false;
05545 }
05546 }
05547
05548 TRACE("quant multmatch", "new env size " , candidateNewEnvs.size(), "");
05549 binds = candidateNewEnvs;
05550 return newwayResult;
05551 }
05552 else{
05553 if ( (gterm.getKind() == vterm.getKind()) &&
05554 (gterm.arity() == vterm.arity()) &&
05555 gterm.arity()>0 )
05556 {
05557 return multMatchChild(gterm, vterm, binds);
05558 }
05559 else {
05560 return false;
05561 }
05562 }
05563 }
05564 return false;
05565 }
05566
05567
05568
05569
05570
05571
05572
05573
05574
05575
05576
05577
05578
05579
05580
05581
05582
05583
05584
05585
05586
05587
05588
05589
05590
05591
05592
05593
05594
05595
05596
05597
05598
05599
05600
05601
05602
05603
05604
05605
05606
05607
05608
05609
05610
05611
05612
05613
05614
05615
05616
05617
05618
05619
05620
05621
05622
05623
05624
05625
05626
05627
05628
05629
05630
05631
05632
05633
05634
05635
05636
05637
05638
05639
05640
05641
05642
05643
05644
05645
05646
05647
05648
05649
05650
05651
05652
05653
05654
05655
05656
05657
05658
05659
05660
05661
05662
05663
05664
05665
05666
05667
05668
05669
05670
05671
05672
05673
05674
05675
05676
05677
05678
05679
05680
05681
05682
05683
05684
05685
05686
05687
05688
05689
05690
05691
05692
05693
05694
05695
05696
05697
05698
05699
05700
05701
05702
05703
05704
05705
05706
05707
05708
05709
05710
05711
05712
05713
05714
05715
05716
05717
05718
05719
05720
05721
05722
05723
05724
05725
05726
05727
05728
05729
05730
05731
05732
05733
05734
05735
05736
05737
05738
05739
05740
05741
05742
05743
05744
05745
05746
05747
05748
05749
05750
05751
05752
05753
05754
05755
05756
05757
05758
05759
05760
05761
05762
05763
05764
05765
05766
05767
05768
05769
05770
05771
05772
05773
05774
05775
05776
05777
05778
05779
05780
05781
05782
05783
05784
05785
05786
05787
05788
05789
05790
05791
05792
05793
05794
05795
05796
05797
05798
05799
05800
05801
05802
05803
05804
05805
05806
05807
05808
05809
05810
05811
05812
05813
05814
05815
05816
05817
05818
05819
05820
05821
05822
05823
05824
05825
05826
05827
05828
05829
05830
05831
05832
05833
05834
05835
05836
05837
05838
05839
05840
05841
05842
05843
05844
05845
05846
05847
05848
05849
05850
05851
05852
05853
05854
05855
05856
05857
05858
05859
05860
05861
05862
05863
05864
05865
05866
05867
05868
05869
05870
05871
05872
05873
05874
05875
05876
05877
05878
05879
05880
05881
05882
05883
05884
05885
05886
05887
05888
05889
05890
05891
05892
05893
05894
05895
05896
05897
05898
05899
05900
05901
05902
05903
05904
05905
05906
05907
05908
05909
05910
05911
05912
05913
05914
05915
05916
05917
05918
05919
05920
05921
05922
05923
05924
05925
05926
05927
05928
05929
05930
05931
05932
05933
05934
05935
05936
05937
05938
05939
05940
05941
05942
05943
05944
05945
05946
05947
05948
05949
05950
05951
05952
05953
05954
05955
05956
05957
05958
05959
05960
05961
05962
05963
05964
05965
05966
05967
05968
05969
05970
05971
05972
05973
05974
05975
05976
05977
05978
05979
05980
05981
05982
05983
05984
05985
05986
05987
05988
05989
05990
05991
05992
05993
05994
05995
05996
05997
05998
05999
06000
06001
06002
06003
06004
06005
06006
06007
06008
06009
06010
06011
06012
06013
06014
06015
06016
06017
06018
06019
06020
06021
06022
06023
06024
06025
06026
06027
06028
06029
06030
06031
06032
06033
06034
06035
06036
06037
06038
06039
06040
06041
06042
06043
06044
06045
06046
06047
06048
06049
06050
06051
06052
06053
06054
06055
06056
06057
06058
06059
06060
06061
06062
06063
06064
06065
06066
06067
06068
06069
06070
06071
06072
06073
06074
06075
06076
06077
06078
06079
06080
06081
06082
06083
06084
06085
06086
06087
06088
06089
06090
06091
06092
06093
06094
06095
06096
06097
06098
06099
06100
06101
06102
06103
06104
06105
06106
06107
06108
06109
06110
06111
06112
06113
06114
06115
06116
06117
06118
06119
06120
06121
06122
06123
06124
06125
06126
06127
06128
06129
06130
06131
06132
06133
06134
06135
06136
06137
06138
06139
06140
06141
06142
06143
06144
06145
06146
06147
06148
06149
06150
06151
06152
06153
06154
06155
06156
06157
06158
06159
06160
06161
06162
06163
06164
06165
06166
06167
06168
06169
06170
06171
06172
06173
06174
06175
06176
06177
06178
06179
06180
06181
06182
06183
06184
06185
06186
06187
06188
06189
06190
06191
06192
06193
06194
06195
06196
06197
06198
06199
06200
06201
06202
06203
06204
06205
06206
06207
06208
06209
06210
06211
06212
06213
06214
06215
06216
06217
06218
06219
06220
06221
06222
06223
06224
06225
06226
06227
06228
06229
06230
06231
06232
06233
06234
06235
06236
06237
06238
06239
06240
06241
06242
06243
06244
06245
06246
06247
06248
06249
06250
06251
06252
06253
06254
06255
06256
06257
06258
06259
06260
06261
06262
06263
06264
06265
06266
06267
06268
06269
06270
06271
06272
06273
06274
06275
06276
06277
06278
06279
06280
06281
06282
06283
06284
06285
06286
06287
06288
06289
06290
06291
06292
06293
06294
06295
06296
06297
06298
06299
06300
06301
06302
06303
06304
06305
06306
06307
06308
06309
06310
06311
06312
06313
06314
06315
06316
06317
06318
06319
06320
06321
06322
06323
06324
06325
06326
06327
06328
06329
06330
06331
06332
06333
06334
06335
06336
06337
06338
06339
06340
06341
06342
06343
06344
06345
06346
06347
06348
06349
06350
06351
06352
06353
06354
06355
06356
06357
06358
06359
06360
06361
06362
06363
06364
06365
06366
06367
06368
06369
06370
06371
06372
06373
06374
06375
06376
06377
06378
06379
06380
06381
06382
06383
06384
06385
06386
06387
06388
06389
06390
06391
06392
06393
06394
06395
06396
06397
06398
06399
06400
06401
06402
06403
06404
06405
06406
06407
06408
06409
06410
06411
06412
06413
06414
06415
06416
06417
06418
06419
06420
06421
06422
06423
06424
06425
06426
06427
06428
06429
06430
06431
06432
06433
06434
06435
06436
06437
06438
06439
06440
06441
06442
06443
06444
06445
06446
06447
06448
06449
06450
06451
06452
06453
06454
06455
06456
06457
06458
06459
06460
06461
06462
06463
06464
06465
06466
06467
06468
06469
06470
06471
06472
06473
06474
06475
06476
06477
06478
06479
06480
06481
06482
06483
06484
06485
06486
06487
06488
06489
06490
06491
06492
06493
06494
06495
06496
06497
06498
06499
06500
06501
06502
06503
06504
06505
06506
06507
06508
06509
06510
06511
06512
06513
06514
06515
06516
06517
06518
06519
06520
06521
06522
06523
06524
06525
06526
06527
06528
06529
06530
06531
06532
06533
06534
06535
06536
06537
06538
06539
06540
06541
06542
06543
06544
06545
06546
06547
06548
06549
06550
06551
06552
06553
06554
06555
06556
06557
06558 int TheoryQuant::loc_gterm(const std::vector<Expr>& border,
06559 const Expr& vterm,
06560 int pos){
06561 const std::vector<Expr>& order = d_mtrigs_bvorder[vterm];
06562 const Expr& var = order[pos];
06563 for(size_t i=0; i<border.size(); i++){
06564 if (border[i] == var) return i;
06565 }
06566
06567 DebugAssert(false, "internal error in loc_germ");
06568 return -1;
06569 }
06570
06571
06572
06573
06574
06575
06576
06577
06578
06579
06580
06581
06582
06583
06584
06585
06586
06587
06588
06589
06590
06591
06592
06593
06594
06595
06596
06597
06598
06599
06600
06601
06602
06603
06604
06605
06606
06607
06608
06609
06610
06611
06612
06613
06614
06615
06616
06617
06618
06619
06620
06621
06622
06623
06624
06625
06626
06627
06628
06629
06630
06631
06632
06633
06634
06635
06636
06637
06638
06639
06640
06641
06642
06643
06644
06645
06646
06647
06648
06649
06650
06651
06652
06653
06654
06655
06656
06657
06658
06659
06660
06661
06662
06663
06664
06665
06666
06667
06668
06669
06670
06671
06672
06673
06674
06675
06676
06677
06678
06679
06680
06681
06682
06683
06684
06685
06686
06687
06688
06689
06690
06691
06692
06693
06694
06695
06696
06697
06698
06699
06700
06701
06702
06703
06704
06705
06706
06707
06708
06709
06710
06711
06712
06713
06714
06715
06716
06717
06718
06719
06720
06721
06722
06723
06724
06725
06726
06727
06728
06729
06730
06731
06732
06733
06734
06735
06736
06737
06738
06739
06740
06741
06742
06743
06744
06745
06746
06747
06748
06749
06750
06751
06752
06753
06754
06755
06756
06757
06758
06759
06760
06761
06762
06763
06764
06765
06766
06767
06768
06769
06770
06771
06772
06773
06774
06775
06776
06777
06778
06779
06780
06781
06782
06783
06784
06785
06786
06787
06788
06789
06790
06791
06792
06793
06794
06795
06796
06797
06798
06799
06800
06801
06802
06803
06804
06805
06806
06807
06808
06809
06810
06811
06812
06813
06814
06815
06816
06817
06818
06819
06820
06821
06822
06823
06824
06825
06826
06827
06828
06829
06830
06831
06832
06833
06834
06835
06836
06837
06838
06839
06840
06841
06842 inline bool TheoryQuant::transFound(const Expr& comb){
06843 return (d_trans_found.count(comb) > 0);
06844 }
06845
06846 inline void TheoryQuant::setTransFound(const Expr& comb){
06847 d_trans_found[comb] = true;
06848 }
06849
06850 inline bool TheoryQuant::trans2Found(const Expr& comb){
06851 return (d_trans2_found.count(comb) > 0);
06852 }
06853
06854 inline void TheoryQuant::setTrans2Found(const Expr& comb){
06855 d_trans2_found[comb] = true;
06856 }
06857
06858
06859 inline CDList<Expr> & TheoryQuant::backList(const Expr& ex){
06860 if(d_trans_back.count(ex)>0){
06861 return *d_trans_back[ex];
06862 }
06863 else{
06864 return null_cdlist;
06865 }
06866 }
06867
06868 inline CDList<Expr> & TheoryQuant::forwList(const Expr& ex){
06869 if(d_trans_forw.count(ex)>0){
06870 return *d_trans_forw[ex];
06871 }
06872 else{
06873 return null_cdlist;
06874 }
06875 }
06876
06877 inline void TheoryQuant::pushBackList(const Expr& node, Expr ex){
06878 if(d_trans_back.count(node)>0){
06879 d_trans_back[node]->push_back(ex);
06880 }
06881 else{
06882 d_trans_back[node] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
06883 d_trans_back[node]->push_back(ex);
06884 }
06885 }
06886
06887 inline void TheoryQuant::pushForwList(const Expr& node, Expr ex){
06888 if(d_trans_forw.count(node)>0){
06889 d_trans_forw[node]->push_back(ex);
06890 }
06891 else{
06892 d_trans_forw[node] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
06893 d_trans_forw[node]->push_back(ex);
06894 }
06895 }
06896
06897
06898
06899
06900
06901
06902
06903
06904
06905
06906
06907
06908
06909
06910
06911
06912
06913
06914
06915
06916
06917
06918
06919
06920
06921
06922
06923
06924
06925
06926
06927
06928
06929
06930
06931
06932
06933
06934
06935
06936
06937
06938
06939
06940
06941
06942
06943
06944
06945
06946
06947
06948
06949
06950
06951
06952
06953
06954
06955
06956
06957
06958
06959
06960
06961
06962
06963
06964
06965
06966
06967
06968
06969
06970
06971
06972
06973
06974
06975
06976
06977
06978
06979
06980
06981
06982
06983
06984
06985
06986
06987
06988
06989
06990
06991
06992
06993
06994
06995
06996
06997
06998
06999
07000
07001
07002
07003
07004
07005
07006
07007
07008
07009
07010
07011
07012
07013
07014
07015
07016
07017
07018
07019
07020
07021
07022
07023
07024
07025
07026
07027
07028
07029
07030
07031
07032
07033
07034
07035
07036
07037
07038
07039
07040
07041
07042
07043
07044
07045
07046
07047
07048
07049
07050
07051
07052
07053
07054
07055
07056
07057
07058
07059
07060
07061
07062
07063
07064
07065
07066
07067
07068
07069
07070
07071
07072
07073
07074
07075
07076
07077
07078
07079
07080
07081 void TheoryQuant::arrayHeuristic(const Trigger& trig, size_t univ_id){
07082 return;
07083 std::vector<Expr> tp = d_arrayIndic[trig.head];
07084 for(size_t i=0; i<tp.size(); i++){
07085 const Expr& index = tp[i];
07086 std::vector<Expr> temp;
07087 temp.push_back(index);
07088 enqueueInst(univ_id, temp, index);
07089
07090 }
07091 }
07092
07093 void inline TheoryQuant::iterFWList(const Expr& sr, const Expr& dt, size_t univ_id, const Expr& gterm){
07094 const CDList<Expr>& dtForw = forwList(dt);
07095 for(size_t k=0; k<dtForw.size(); k++){
07096 vector<Expr> tri_bind;
07097 tri_bind.push_back(sr);
07098 tri_bind.push_back(dt);
07099 tri_bind.push_back(dtForw[k]);
07100 enqueueInst(univ_id, tri_bind, gterm);
07101 }
07102 }
07103
07104 void inline TheoryQuant::iterBKList(const Expr& sr, const Expr& dt, size_t univ_id, const Expr& gterm){
07105 const CDList<Expr>& srBack = backList(sr);
07106 for(size_t k=0; k<srBack.size(); k++){
07107 vector<Expr> tri_bind;
07108 tri_bind.push_back(srBack[k]);
07109 tri_bind.push_back(sr);
07110 tri_bind.push_back(dt);
07111 enqueueInst(univ_id, tri_bind, gterm);
07112 }
07113 }
07114
07115
07116
07117 Expr TheoryQuant::simpRAWList(const Expr& org){
07118 vector<Expr> result;
07119 if(null_expr == org) return null_expr;
07120 for(int i =0 ; i < org.arity(); i++){
07121 result.push_back(simplifyExpr(org[i]));
07122 }
07123 return Expr(RAW_LIST,result);
07124 }
07125
07126
07127 void TheoryQuant::synNewInst(size_t univ_id, const vector<Expr>& bind, const Expr& gterm, const Trigger& trig ){
07128 if(trig.isMulti){
07129 const multTrigsInfo& mtriginfo = d_all_multTrigsInfo[trig.multiId];
07130
07131 vector<Expr> actual_bind;
07132 for(size_t i=0, iend=bind.size(); i<iend; i++){
07133 if(null_expr != bind[i]){
07134 actual_bind.push_back(bind[i]);
07135 }
07136 }
07137
07138 Expr actual_bind_expr = Expr(RAW_LIST, actual_bind);
07139
07140 size_t index = trig.multiIndex;
07141
07142
07143 CDMap<Expr,bool> * oldBindMap = mtriginfo.var_binds_found[index];
07144 CDMap<Expr,bool>::iterator cur_iter = oldBindMap->find(actual_bind_expr);
07145
07146 if (oldBindMap->end() != cur_iter){
07147 return;
07148 }
07149 else{
07150 (*oldBindMap)[actual_bind_expr] = true;
07151 }
07152
07153
07154
07155 const vector<size_t>& comm_pos = mtriginfo.common_pos[0];
07156 size_t comm_pos_size = comm_pos.size();
07157
07158 Expr comm_expr;
07159 vector<Expr> comm_expr_vec;
07160 for(size_t i = 0; i < comm_pos_size; i++){
07161 comm_expr_vec.push_back(bind[comm_pos[i]]);
07162 }
07163
07164 if(0 == comm_pos_size){
07165 comm_expr = null_expr;
07166 }
07167 else{
07168 comm_expr = Expr(RAW_LIST, comm_expr_vec);
07169 }
07170
07171 Expr uncomm_expr;
07172 vector<Expr> uncomm_expr_vec;
07173
07174 const vector<size_t>& uncomm_pos = mtriginfo.var_pos[index];
07175 size_t uncomm_pos_size = uncomm_pos.size();
07176 for(size_t i = 0; i< uncomm_pos_size; i++){
07177 uncomm_expr_vec.push_back(bind[uncomm_pos[i]]);
07178 }
07179 if(0 == uncomm_pos_size){
07180 uncomm_expr = null_expr;
07181 }
07182 else{
07183 uncomm_expr = Expr(RAW_LIST, uncomm_expr_vec);
07184 }
07185
07186 CDList<Expr>* add_into_list ;
07187 CDList<Expr>* iter_list;
07188 ExprMap<CDList<Expr>* >::iterator add_into_iter;
07189 ExprMap<CDList<Expr>* >::iterator iter_iter;
07190
07191 size_t other_index = 0;
07192 if(0 == index){
07193 other_index =1;
07194 }
07195 else if (1 == index){
07196 other_index = 0;
07197 }
07198 else{
07199 FatalAssert(false, "Sorry, only two vterms in a multi-trigger.");
07200 }
07201
07202 add_into_iter = mtriginfo.uncomm_list[index]->find(comm_expr);
07203
07204 if(mtriginfo.uncomm_list[index]->end() == add_into_iter){
07205 add_into_list = new (true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
07206 (*mtriginfo.uncomm_list[index])[comm_expr] = add_into_list;
07207 }
07208 else{
07209 add_into_list = add_into_iter->second;
07210 }
07211
07212 add_into_list->push_back(uncomm_expr);
07213
07214
07215 Expr simpCommExpr = simpRAWList(comm_expr);
07216
07217
07218
07219
07220 {
07221 ExprMap<CDList<Expr>* >* otherMap = mtriginfo.uncomm_list[other_index];
07222
07223
07224 ExprMap<CDList<Expr>* >::iterator otherMapBegin = otherMap->begin(), otherMapEnd = otherMap->end();
07225 for(ExprMap<CDList<Expr>* >::iterator otherMapIter = otherMapBegin; otherMapIter != otherMapEnd; otherMapIter++){
07226
07227 Expr otherCommonExpr = simpRAWList(otherMapIter->first);
07228 if(simpCommExpr != otherCommonExpr) continue;
07229
07230
07231
07232
07233
07234
07235
07236
07237 if(comm_expr != otherMapIter->first) {
07238 }
07239
07240 iter_list = otherMapIter->second;
07241 const vector<size_t>& uncomm_iter_pos = mtriginfo.var_pos[other_index];
07242 size_t uncomm_iter_pos_size = uncomm_iter_pos.size();
07243
07244 for(size_t i =0, iend = iter_list->size(); i<iend; i++){
07245 const Expr& cur_iter_expr = (*iter_list)[i];
07246 vector<Expr> new_bind(bind);
07247 for(size_t j=0; j<uncomm_iter_pos_size; j++){
07248 new_bind[uncomm_iter_pos[j]] = cur_iter_expr[j];
07249 }
07250 enqueueInst(univ_id, new_bind, gterm);
07251 }
07252 }
07253 }
07254 return;
07255 }
07256
07257 {
07258 if(trig.hasT2){
07259 vector<Expr> actual_bind;
07260 for(size_t i=0; i<bind.size(); i++){
07261 if(bind[i] != null_expr){
07262 actual_bind.push_back(bind[i]);
07263 }
07264 }
07265 if(actual_bind.size() != 2){
07266
07267 }
07268
07269 Expr acb1 = simplifyExpr(actual_bind[0]);
07270 Expr acb2 = simplifyExpr(actual_bind[1]);
07271 actual_bind[0]=acb1;
07272 actual_bind[1]=acb2;
07273 if(acb1 != acb2){
07274 Expr comb = Expr(RAW_LIST,acb1, acb2);
07275 if(!trans2Found(comb)){
07276 setTrans2Found(comb);
07277 Expr comb_rev = Expr(RAW_LIST,acb2, acb1);
07278 if(trans2Found(comb_rev)){
07279 enqueueInst(univ_id, actual_bind, gterm);
07280 }
07281 }
07282 }
07283 return;
07284 }
07285 }
07286
07287 {
07288 if(trig.hasTrans){
07289 vector<Expr> actual_bind;
07290 for(size_t i=0; i<bind.size(); i++){
07291 if(bind[i] != null_expr){
07292 actual_bind.push_back(simplifyExpr(bind[i]));
07293 }
07294 }
07295 if(simplifyExpr(actual_bind[0]) != simplifyExpr(actual_bind[1])){
07296 Expr comb = Expr(RAW_LIST,actual_bind[0], actual_bind[1]);
07297
07298 if(!transFound(comb)){
07299 setTransFound(comb);
07300
07301 Expr sr(actual_bind[0]);
07302 Expr dt(actual_bind[1]);
07303
07304 iterFWList(sr, dt, univ_id, gterm);
07305 if(*d_useNewEqu){
07306 Expr cur_next = dt.getEqNext().getRHS();
07307 while (cur_next != dt) {
07308 iterFWList(sr, cur_next, univ_id, gterm);
07309 cur_next = cur_next.getEqNext().getRHS();
07310 }
07311 }
07312
07313 iterBKList(sr, dt, univ_id, gterm);
07314 if(*d_useNewEqu){
07315 Expr cur_next = sr.getEqNext().getRHS();
07316 while (cur_next != sr) {
07317 iterBKList(cur_next, dt, univ_id, gterm);
07318 cur_next = cur_next.getEqNext().getRHS();
07319 }
07320 }
07321 pushForwList(sr,dt);
07322 pushBackList(dt,sr);
07323 }
07324 }
07325 return;
07326 }
07327 }
07328
07329
07330 enqueueInst(univ_id, bind, gterm);
07331
07332
07333 }
07334
07335
07336
07337
07338
07339
07340
07341
07342
07343
07344
07345
07346
07347
07348
07349
07350
07351
07352
07353
07354
07355
07356
07357
07358
07359
07360
07361
07362
07363
07364
07365
07366
07367
07368
07369
07370
07371
07372
07373
07374
07375
07376
07377
07378
07379
07380
07381
07382
07383
07384
07385
07386
07387
07388
07389
07390
07391
07392
07393
07394
07395
07396
07397
07398
07399
07400
07401
07402
07403
07404
07405
07406
07407
07408
07409
07410
07411
07412
07413
07414
07415
07416
07417
07418
07419
07420
07421
07422
07423
07424
07425
07426
07427
07428
07429
07430
07431
07432
07433
07434
07435
07436
07437
07438
07439
07440
07441
07442
07443
07444
07445
07446
07447
07448
07449
07450
07451
07452
07453
07454
07455
07456
07457
07458
07459
07460
07461
07462
07463
07464
07465
07466
07467
07468
07469
07470
07471
07472
07473
07474
07475
07476
07477
07478
07479
07480
07481
07482
07483
07484
07485
07486
07487
07488
07489
07490
07491
07492
07493
07494
07495
07496
07497
07498
07499
07500
07501
07502
07503
07504
07505
07506
07507
07508
07509
07510
07511
07512
07513
07514
07515
07516 void TheoryQuant::checkSat(bool fullEffort){
07517 if(*d_translate) return;
07518 if(d_rawUnivs.size() <=0 ) return;
07519 if (d_maxILReached) {
07520
07521 return;
07522 }
07523 else{
07524 }
07525
07526 DebugAssert(d_univsQueue.size() == 0, "something left in d_univsQueue");
07527 DebugAssert(d_simplifiedThmQueue.size() == 0, "something left in d_univsQueue");
07528
07529 if( false ) {
07530
07531
07532 for(size_t eqs_index = d_lastEqsUpdatePos; eqs_index < d_eqsUpdate.size(); eqs_index++){
07533
07534 Theorem eqThm = d_eqsUpdate[eqs_index];
07535
07536 const Expr& rightTerm = eqThm.getRHS();
07537
07538 std::vector<multTrigsInfo> d_all_multTrigsInfo;
07539
07540 int numUsefulMultTriger = 0;
07541 for(size_t i = 0; i < d_all_multTrigsInfo.size(); i++){
07542 multTrigsInfo& curMultiTrigger = d_all_multTrigsInfo[i];
07543 if(curMultiTrigger.uncomm_list.size() != 2 ){
07544 FatalAssert(false, "error in ");
07545 }
07546 ExprMap<CDList<Expr>* >* uncommonMapOne = curMultiTrigger.uncomm_list[0];
07547 ExprMap<CDList<Expr>* >* uncommonMapTwo = curMultiTrigger.uncomm_list[1];
07548
07549 if(uncommonMapOne->size() != 0 || uncommonMapTwo->size() != 0 ){
07550 numUsefulMultTriger++;
07551 }
07552
07553
07554
07555 if(uncommonMapOne->size() == 0 ) {
07556 continue;
07557 }
07558
07559
07560
07561
07562 ExprMap<CDList<Expr>* >::iterator iterOneBegin(uncommonMapOne->begin()), iterOneEnd(uncommonMapOne->end());
07563
07564
07565
07566
07567 vector<pair<Expr, CDList<Expr>* > > oneFoundTerms;
07568 for(ExprMap<CDList<Expr>* >::iterator iterOne=iterOneBegin; iterOne != iterOneEnd; iterOne++){
07569
07570 if(simplifyExpr((iterOne->first)[0]) == simplifyExpr(rightTerm)){
07571
07572
07573 oneFoundTerms.push_back(*iterOne);
07574 }
07575 }
07576
07577 ExprMap<CDList<Expr>* >::iterator iterTwoBegin(uncommonMapTwo->begin()), iterTwoEnd(uncommonMapTwo->end());
07578
07579 vector<pair<Expr, CDList<Expr>* > >twoFoundTerms;
07580 for(ExprMap<CDList<Expr>* >::iterator iterTwo = iterTwoBegin; iterTwo != iterTwoEnd; iterTwo++){
07581 if(simplifyExpr((iterTwo->first)[0]) == simplifyExpr(rightTerm)){
07582
07583
07584 twoFoundTerms.push_back(*iterTwo);
07585 }
07586 }
07587 {
07588 for(size_t i= 0 ; i< oneFoundTerms.size(); i++){
07589 for(size_t j= 0 ; j< twoFoundTerms.size(); j++){
07590 pair<Expr, CDList<Expr>* > pairOne = oneFoundTerms[i];
07591 pair<Expr, CDList<Expr>* > pairTwo = twoFoundTerms[j];
07592 if(pairOne.first == pairTwo.first) continue;
07593
07594
07595 CDList<Expr>* oneExprList = pairOne.second;
07596 CDList<Expr>* twoExprList = pairTwo.second;
07597
07598 for(size_t oneIter = 0; oneIter < oneExprList->size(); oneIter++){
07599
07600 for(size_t twoIter = 0; twoIter < twoExprList->size(); twoIter++){
07601 Expr gterm1 = (*oneExprList)[oneIter][0];
07602 Expr gterm2 = (*twoExprList)[twoIter][0];
07603
07604
07605 vector<Expr> bind ;
07606 bind.push_back(gterm1);
07607 bind.push_back(rightTerm);
07608 bind.push_back(gterm2);
07609 size_t univID = curMultiTrigger.univ_id;
07610
07611 if(d_univs[univID] != curMultiTrigger.univThm) {
07612
07613
07614
07615 exit(3);
07616 }
07617
07618 enqueueInst(curMultiTrigger.univ_id, bind, rightTerm);
07619
07620
07621 bind.clear();
07622 bind.push_back(gterm2);
07623 bind.push_back(rightTerm);
07624 bind.push_back(gterm1);
07625 enqueueInst(curMultiTrigger.univ_id, bind, rightTerm);
07626
07627
07628 }
07629 }
07630 }
07631 }
07632 }
07633 }
07634
07635 }
07636 }
07637
07638 sendInstNew();
07639
07640
07641
07642
07643
07644
07645
07646
07647
07648
07649
07650
07651
07652
07653
07654
07655
07656
07657
07658
07659
07660
07661
07662
07663
07664
07665
07666
07667
07668
07669
07670
07671
07672
07673
07674
07675
07676
07677
07678
07679
07680 #ifdef _CVC3_DEBUG_MODE
07681 if(fullEffort){
07682 if( CVC3::debugger.trace("quant assertfact") ){
07683 cout<<"===========all cached univs =========="<<endl;
07684
07685
07686
07687
07688
07689
07690 }
07691 if( CVC3::debugger.trace("quant samehead") ){
07692 cout<<"===========all cached =========="<<endl;
07693 for (ExprMap< CDList<Expr>*>::iterator i=d_same_head_expr.begin(), iend=d_same_head_expr.end(); i!=iend; i++){
07694 cout<<"------------------------------------"<<endl;
07695 cout<<(i->first)<<endl;
07696 cout<<"_______________________"<<endl;
07697 CDList<Expr> * terms= i->second;
07698 for(size_t i =0; i<terms->size(); i++){
07699 cout<<(*terms)[i]<<endl;
07700 }
07701 }
07702 }
07703 }
07704 #endif
07705
07706 #ifdef _CVC3_DEBUG_MODE
07707 if( CVC3::debugger.trace("quant checksat") ){
07708 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
07709 cout<<"=========== cur pred & terms =========="<<endl;
07710
07711 for (size_t i=d_lastPredsPos; i<allpreds.size(); i++){
07712
07713 cout<<"i="<<allpreds[i].getIndex()<<" :"<<findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
07714 }
07715
07716 const CDList<Expr>& allterms = theoryCore()->getTerms();
07717
07718 for (size_t i=d_lastTermsPos; i<allterms.size(); i++){
07719 cout<<"i="<<allterms[i].getIndex()<<" :"<<findExpr(allterms[i])<<"|"<<allterms[i]<<endl;
07720 }
07721 cout<<"=========== cur quant =========="<<endl;
07722 for (size_t i=0; i<d_univs.size(); i++){
07723 cout<<"i="<<d_univs[i].getExpr().getIndex()<<" :"<<findExpr(d_univs[i].getExpr())<<"|"<<d_univs[i]<<endl;
07724 }
07725 }
07726
07727
07728 if( CVC3::debugger.trace("quant checksat equ") ){
07729 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
07730 cout<<"=========== cur pred equ =========="<<endl;
07731
07732 for (size_t i=d_lastPredsPos; i<allpreds.size(); i++){
07733 if(allpreds[i].isEq()){
07734 cout<<"i="<<allpreds[i].getIndex()<<" :"<<findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
07735 }
07736 }
07737 cout<<"=========== cur pred equ end =========="<<endl;
07738 }
07739
07740 #endif
07741
07742 if((*d_useLazyInst && !fullEffort) ) return;
07743
07744 if(false) {
07745 const CDList<Expr>& allterms = theoryCore()->getTerms();
07746 for(size_t i=d_lastTermsPos; i<allterms.size(); i++){
07747 Expr t = allterms[i];
07748 if(canGetHead(t)){
07749 if(d_same_head_expr.count(getHead(t)) >0){
07750 d_same_head_expr[getHead(t)]->push_back(t);
07751 }
07752 else{
07753 d_same_head_expr[getHead(t)]=
07754 new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
07755 d_same_head_expr[getHead(t)]->push_back(t);
07756 }
07757 }
07758 }
07759
07760 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
07761 for(size_t i=d_lastPredsPos; i<allpreds.size(); i++){
07762 Expr t = allpreds[i];
07763 if(canGetHead(t)){
07764 if(d_same_head_expr.count(getHead(t)) >0){
07765 d_same_head_expr[getHead(t)]->push_back(t);
07766 }
07767 else{
07768 d_same_head_expr[getHead(t)]=
07769 new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
07770 d_same_head_expr[getHead(t)]->push_back(t);
07771 }
07772 }
07773 }
07774 }
07775
07776 if(false){
07777 for(size_t eqs_index = d_lastEqsUpdatePos; eqs_index < d_eqsUpdate.size(); eqs_index++){
07778
07779 const Expr lTerm = d_eqsUpdate[eqs_index].getLHS();
07780 const Expr rTerm = d_eqsUpdate[eqs_index].getRHS();
07781
07782 d_eqs.push_back(lTerm);
07783 d_eqs.push_back(rTerm);
07784 }
07785 }
07786
07787 if(false) {
07788 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
07789 for(size_t i=d_lastPredsPos; i<allpreds.size(); i++){
07790 const Expr& t = allpreds[i];
07791 if(t.isEq()){
07792
07793 const Expr lterm = t[0];
07794 const Expr rterm = t[1];
07795 d_eqs.push_back(lterm);
07796 d_eqs.push_back(rterm);
07797
07798
07799
07800
07801
07802
07803
07804
07805
07806
07807
07808
07809
07810
07811
07812
07813
07814
07815
07816
07817
07818
07819 }
07820 }
07821 }
07822
07823
07824 {
07825 const CDList<Expr>& allterms = theoryCore()->getTerms();
07826 for(size_t i=d_lastTermsPos; i<allterms.size(); i++){
07827 const Expr& cur=allterms[i];
07828 if(READ == cur.getKind() || WRITE == cur.getKind()){
07829 arrayIndexName(cur);
07830 }
07831 }
07832 }
07833
07834 d_instThisRound = 0;
07835
07836
07837 d_useFullTrig=true;
07838
07839 if(fullEffort) {
07840 d_inEnd=true;
07841 }
07842 else{
07843 d_inEnd=false;
07844 }
07845
07846
07847 ExprMap<ExprMap<vector<dynTrig>* >* > new_trigs;
07848 if(fullEffort || theoryCore()->getCM()->scopeLevel() <= 5 || true){
07849 for(size_t i=d_univs.size(); i<d_rawUnivs.size(); i++){
07850 setupTriggers(new_trigs, d_rawUnivs[i], i);
07851 }
07852 }
07853 try {
07854 if (!(*d_useNew)){
07855 naiveCheckSat(fullEffort);
07856 }
07857 else if (*d_useSemMatch){
07858 semCheckSat(fullEffort);
07859 }
07860 else {
07861 synCheckSat(new_trigs, fullEffort);
07862 }
07863 }
07864
07865 catch (int x){
07866
07867 while(!d_simplifiedThmQueue.empty()){
07868 d_simplifiedThmQueue.pop();
07869 d_abInstCount++;
07870 }
07871 while(!d_gUnivQueue.empty()){
07872 d_gUnivQueue.pop();
07873 }
07874 while(!d_gBindQueue.empty()){
07875 d_gBindQueue.pop();
07876 }
07877
07878
07879
07880 d_tempBinds.clear();
07881 saveContext();
07882 delNewTrigs(new_trigs);
07883 return;
07884 }
07885
07886 sendInstNew();
07887
07888 saveContext();
07889
07890 try{
07891 if((*d_useNaiveInst) && (*d_useNew) && (0 == d_instThisRound) && fullEffort && theoryCore()->getTerms().size() < (size_t)(*d_maxNaiveCall )) {
07892
07893 if (0== theoryCore()->getTerms().size()){
07894 static int counter =0;
07895
07896 std::set<Expr> types;
07897 for(size_t i = 0; i<d_univs.size(); i++){
07898 const Expr& cur_quant = d_univs[i].getExpr();
07899 const std::vector<Expr> cur_vars = cur_quant.getVars();
07900 for(size_t j =0; j<cur_vars.size(); j++){
07901 types.insert(cur_vars[j].getType().getExpr());
07902 }
07903 }
07904
07905 std::string base("_naiveInst");
07906 for(std::set<Expr>::iterator i=types.begin(), iend = types.end(); i != iend; i++){
07907 counter++;
07908 std::stringstream tempout;
07909 tempout << counter;
07910 std::string out_str = base + tempout.str();
07911 Expr newExpr = theoryCore()->getEM()->newVarExpr(out_str);
07912
07913 newExpr.setType(Type(*i));
07914
07915 Proof pf;
07916
07917 Expr newExpr2 = theoryCore()->getEM()->newVarExpr(out_str+"extra");
07918 newExpr2.setType(Type(*i));
07919
07920 Expr newConstThm;
07921
07922 if(Type(*i) == theoryCore()->getEM()->newRatExpr(0).getType()){
07923
07924 newConstThm = newExpr.eqExpr(theoryCore()->getEM()->newRatExpr(0));
07925 }
07926 else{
07927 newConstThm = newExpr.eqExpr(newExpr2);
07928 }
07929 Theorem newThm = d_rules->addNewConst(newConstThm);
07930
07931 if(*d_useGFact){
07932
07933 enqueueFact(newThm);
07934 }
07935 else{
07936 enqueueFact(newThm);
07937 }
07938
07939
07940 d_tempBinds.clear();
07941 return;
07942 }
07943
07944 }
07945 naiveCheckSat(fullEffort);
07946 }
07947 }
07948
07949 catch (int x){
07950
07951 while(!d_simplifiedThmQueue.empty()){
07952 d_simplifiedThmQueue.pop();
07953 d_abInstCount++;
07954 }
07955 while(!d_gUnivQueue.empty()){
07956 d_gUnivQueue.pop();
07957 }
07958 while(!d_gBindQueue.empty()){
07959 d_gBindQueue.pop();
07960 }
07961
07962
07963 d_tempBinds.clear();
07964 saveContext();
07965 delNewTrigs(new_trigs);
07966 return;
07967 }
07968
07969 if(fullEffort) {
07970 sendInstNew();
07971 }
07972
07973 combineOldNewTrigs(new_trigs);
07974 delNewTrigs(new_trigs);
07975 }
07976
07977 void TheoryQuant::saveContext(){
07978 d_lastArrayPos.set(d_arrayTrigs.size());
07979 d_univsSavedPos.set(d_univs.size());
07980 d_rawUnivsSavedPos.set(d_rawUnivs.size());
07981 d_lastTermsPos.set(theoryCore()->getTerms().size());
07982 d_lastPredsPos.set(theoryCore()->getPredicates().size());
07983 d_lastUsefulGtermsPos.set(d_usefulGterms.size());
07984 d_lastEqsUpdatePos.set(d_eqsUpdate.size());
07985 }
07986
07987 void TheoryQuant::synCheckSat(ExprMap<ExprMap<vector<dynTrig>* >* >& new_trigs, bool fullEffort){
07988
07989 d_allout=false;
07990
07991 if(fullEffort) {
07992 setIncomplete("Quantifier instantiation");
07993 }
07994
07995 size_t uSize = d_univs.size() ;
07996 const CDList<Expr>& allterms = theoryCore()->getTerms();
07997 const CDList<Expr>& allpreds = theoryCore()->getPredicates();
07998 size_t tSize = allterms.size();
07999 size_t pSize = allpreds.size();
08000
08001 TRACE("quant",uSize, " uSize and univsSavedPOS ", d_univsSavedPos);
08002 TRACE("quant",tSize, " tSize and termsLastPos ", d_lastTermsPos);
08003 TRACE("quant",pSize, " pSize and predsLastPos ", d_lastPredsPos);
08004 TRACE("quant", fullEffort, " fulleffort:scope ",theoryCore()->getCM()->scopeLevel() );
08005
08006 for(size_t i=d_lastTermsPos; i<tSize; i++){
08007 const Expr& cur(allterms[i]);
08008
08009 if(usefulInMatch(cur)){
08010 if(*d_useExprScore){
08011 int score = getExprScore(cur);
08012 if(score <= d_curMaxExprScore && 0 <= score ){
08013 d_usefulGterms.push_back(cur);
08014 add_parent(cur);
08015 }
08016 }
08017 else{
08018 d_usefulGterms.push_back(cur);
08019 add_parent(cur);
08020 }
08021 }
08022 else{
08023 }
08024 }
08025
08026 for(size_t i=d_lastPredsPos; i<pSize; i++){
08027 const Expr& cur=allpreds[i];
08028
08029 if( usefulInMatch(cur)){
08030 if(*d_useExprScore ){
08031 int score = getExprScore(cur);
08032 if(score <= d_curMaxExprScore && 0 <= score){
08033 d_usefulGterms.push_back(cur);
08034 add_parent(cur);
08035 }
08036 }
08037 else{
08038 d_usefulGterms.push_back(cur);
08039 add_parent(cur);
08040 }
08041 }
08042 else{
08043 }
08044 }
08045
08046
08047
08048 if(d_useFullTrig && d_inEnd ){
08049
08050 if(*d_useExprScore){
08051
08052 matchListOld(d_usefulGterms, d_lastUsefulGtermsPos, d_usefulGterms.size() );
08053 matchListNew(new_trigs, d_usefulGterms, 0, d_usefulGterms.size());
08054
08055 if(sendInstNew() > 0){
08056 TRACE("inend", "debug 1", "" ,"" );
08057 return;
08058 }
08059
08060 d_allout = true;
08061 {
08062 CDList<Expr>* changed_terms = new (false) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
08063 collectChangedTerms(*changed_terms);
08064
08065 matchListOld(*changed_terms, 0, changed_terms->size());
08066 matchListNew(new_trigs, *changed_terms, 0 , changed_terms->size());
08067 delete changed_terms;
08068 }
08069 d_allout = false;
08070 int n;
08071 if( ( n = sendInstNew()) > 0){
08072 TRACE("inend", "debug 2", " # ",n );
08073 return;
08074 }
08075
08076 bool hasMoreGterms(false);
08077
08078 do {
08079
08080 hasMoreGterms=false;
08081
08082 int numNewTerm=0;
08083 int oldNum=d_usefulGterms.size();
08084
08085 for(size_t i=0; i<tSize; i++){
08086 const Expr& cur(allterms[i]);
08087
08088 if(!(usefulInMatch(cur)) ) continue;
08089 int score = getExprScore(cur);
08090 if( score > d_curMaxExprScore){
08091 if((d_curMaxExprScore + 1) == score){
08092
08093 d_usefulGterms.push_back(cur);
08094 add_parent(cur);
08095 numNewTerm++;
08096 }
08097 else{
08098 hasMoreGterms = true;
08099 TRACE("inend", "is this good? ", cur.toString()+" #-# " , score);
08100
08101 if(*d_useGFact && false ){
08102 d_usefulGterms.push_back(cur);
08103 add_parent(cur);
08104 numNewTerm++;
08105 }
08106
08107
08108
08109 }
08110 }
08111 }
08112
08113
08114 for(size_t i=0; i<pSize; i++){
08115 const Expr& cur(allpreds[i]);
08116
08117 if(!(usefulInMatch(cur)) ) continue;
08118 int score = getExprScore(cur);
08119 if( score > d_curMaxExprScore){
08120 if((d_curMaxExprScore + 1) == score){
08121
08122 d_usefulGterms.push_back(cur);
08123 add_parent(cur);
08124 numNewTerm++;
08125 }
08126 else{
08127 hasMoreGterms = true;
08128 TRACE("inend", "is this good? ", cur.toString()+" #-# " , score);
08129
08130 if(*d_useGFact && false ){
08131 d_usefulGterms.push_back(cur);
08132 add_parent(cur);
08133 numNewTerm++;
08134 }
08135
08136
08137
08138 }
08139 }
08140 }
08141
08142
08143
08144
08145
08146
08147
08148
08149
08150
08151
08152
08153
08154
08155
08156
08157
08158
08159
08160
08161
08162
08163
08164
08165
08166
08167
08168
08169
08170
08171
08172
08173
08174 if(d_curMaxExprScore >= 0 && d_curMaxExprScore <= *d_maxIL ){
08175 d_curMaxExprScore = d_curMaxExprScore+1;;
08176 }
08177 else {
08178 d_curMaxExprScore = d_curMaxExprScore+1;
08179
08180 d_maxILReached = true;
08181
08182 }
08183
08184
08185
08186
08187 if(numNewTerm >0 ){
08188 matchListOld(d_usefulGterms, oldNum, d_usefulGterms.size() );
08189 matchListNew(new_trigs, d_usefulGterms, oldNum, d_usefulGterms.size());
08190
08191 if(sendInstNew() > 0){
08192 TRACE("inend", "debug 3 1", "" , "" );
08193 return;
08194 }
08195 }
08196
08197 if(hasMoreGterms){
08198 ;
08199
08200
08201
08202 }
08203
08204 } while(hasMoreGterms && d_curMaxExprScore <= *d_maxIL);
08205
08206 d_allout = true;
08207 matchListOld(d_usefulGterms, 0, d_usefulGterms.size() );
08208 matchListNew(new_trigs, d_usefulGterms, 0, d_usefulGterms.size());
08209 if(sendInstNew() > 0){
08210 TRACE("inend", "debug 3 2", "" , "" );
08211 return;
08212 }
08213 d_allout = false;
08214
08215
08216
08217
08218
08219
08220 return ;
08221 }
08222
08223 TRACE("inend", "debug 3 0", "", "");
08224 TRACE("quant","this round; ",d_callThisRound,"");
08225
08226 return;
08227 }
08228
08229
08230 if ((uSize == d_univsSavedPos) &&
08231 (tSize == d_lastTermsPos) &&
08232 (pSize == d_lastPredsPos) ) return;
08233
08234
08235 matchListOld(d_usefulGterms, d_lastUsefulGtermsPos,d_usefulGterms.size() );
08236
08237 matchListNew(new_trigs, d_usefulGterms, 0, d_usefulGterms.size() );
08238
08239 for(size_t array_index = d_lastArrayPos; array_index < d_arrayTrigs.size(); array_index++){
08240 arrayHeuristic(d_arrayTrigs[array_index].trig, d_arrayTrigs[array_index].univ_id);
08241 }
08242
08243 TRACE("quant","this round; ",d_callThisRound,"");
08244
08245 return;
08246 }
08247
08248
08249 void TheoryQuant::semCheckSat(bool fullEffort){
08250 }
08251
08252
08253 void TheoryQuant::naiveCheckSat(bool fullEffort){
08254 d_univsSavedPos.set(0);
08255 TRACE("quant", "checkSat ", fullEffort, "{");
08256 IF_DEBUG(int instCount = d_instCount;)
08257 size_t uSize = d_univs.size(), stSize = d_savedTerms.size();
08258 if(true || (fullEffort && uSize > 0)) {
08259
08260 setIncomplete("Quantifier instantiation");
08261
08262 if(d_instCount>=*d_maxQuantInst)
08263 return;
08264
08265
08266
08267 bool savedOnly = ((uSize > d_univsSavedPos.get() && stSize > 0) ||
08268 (stSize > d_savedTermsPos.get()));
08269 int origCount = d_instCount;
08270 if(savedOnly)
08271 {
08272 TRACE("quant", "checkSat [saved insts]: univs size = ", uSize , " ");
08273 for(size_t i=0, pos = d_univsSavedPos.get(); i<uSize; i++) {
08274 if(d_instCount>= *d_maxQuantInst)
08275 break;
08276 else
08277 instantiate(d_univs[i], i>=pos, true, d_savedTermsPos.get());
08278 }
08279 d_univsSavedPos.set(d_univs.size());
08280 d_savedTermsPos.set(stSize);
08281 }
08282 if(!savedOnly || d_instCount == origCount)
08283 {
08284 TRACE("quant", "checkSat [context insts]: univs size = ", uSize , " ");
08285 const CDList<Expr>& assertions = theoryCore()->getTerms();
08286 int origSize = d_contextTerms.size();
08287
08288
08289
08290 TRACE("quant", "checkSat terms size = ", assertions.size() , " ");
08291 mapTermsByType(assertions);
08292 for(size_t i=0, pos = d_univsContextPos.get(); i<uSize; i++) {
08293 if(d_instCount>= *d_maxQuantInst)
08294 break;
08295 else
08296 instantiate(d_univs[i], i>=pos, false, origSize);
08297 }
08298 d_univsContextPos.set(d_univs.size());
08299 }
08300 TRACE("quant terse", "checkSat total insts: ",
08301 d_instCount, ", new "+int2string(d_instCount - instCount));
08302 }
08303 TRACE("quant", "checkSat total insts: ", d_instCount, " ");
08304 TRACE("quant", "checkSat new insts: ", d_instCount - instCount, " ");
08305 TRACE("quant", "checkSat effort:", fullEffort, " }");
08306
08307 }
08308
08309
08310
08311
08312
08313
08314
08315
08316
08317
08318 void TheoryQuant::instantiate(Theorem univ, bool all, bool savedMap,
08319 size_t newIndex)
08320 {
08321
08322 if(!all && ((savedMap && newIndex == d_savedTerms.size())
08323 ||(!savedMap && newIndex == d_contextTerms.size())))
08324 return;
08325
08326 TRACE("quant", "instanitate", all , "{");
08327 std::vector<Expr> varReplacements;
08328 recInstantiate(univ, all, savedMap, newIndex, varReplacements);
08329 TRACE("quant", "instanitate", "", "}");
08330
08331 }
08332
08333
08334 void TheoryQuant::recInstantiate(Theorem& univ, bool all, bool savedMap,
08335 size_t newIndex,
08336 std::vector<Expr>& varReplacements)
08337 {
08338 Expr quantExpr = univ.getExpr();
08339 const vector<Expr>& boundVars = quantExpr.getVars();
08340
08341 size_t curPos = varReplacements.size();
08342 TRACE("quant", "recInstantiate: ", boundVars.size() - curPos, "");
08343
08344 if(curPos == boundVars.size()) {
08345 if(!all)
08346 return;
08347 Theorem t = d_rules->universalInst(univ, varReplacements);
08348 d_insts[t.getExpr()] = varReplacements;
08349 TRACE("quant", "recInstantiate => " , t.toString(), "");
08350 if(d_instCount< *d_maxQuantInst) {
08351 d_instCount=d_instCount+1;
08352 enqueueInst(univ, varReplacements, null_expr);
08353
08354
08355 }
08356 return;
08357 }
08358
08359
08360 else {
08361 Type t = getBaseType(boundVars[curPos]);
08362 int iendC=0, iendS=0, iend;
08363 std::vector<size_t>* typeVec = NULL;
08364 CDList<size_t>* typeList = NULL;
08365 if(d_savedMap.count(t) > 0) {
08366 typeVec = &(d_savedMap[t]);
08367 iendS = typeVec->size();
08368 TRACE("quant", "adding from savedMap: ", iendS, "");
08369 }
08370 if(!savedMap) {
08371 if(d_contextMap.count(t) > 0) {
08372 typeList = d_contextMap[t];
08373 iendC = typeList->size();
08374 TRACE("quant", "adding from contextMap:", iendC , "");
08375 }
08376 }
08377 iend = iendC + iendS;
08378 for(int i =0; i<iend; i++) {
08379 TRACE("quant", "I must have gotten here!", "", "");
08380 size_t index;
08381 if(i<iendS){
08382 index = (*typeVec)[i];
08383 varReplacements.push_back(d_savedTerms[index]);
08384 }
08385 else {
08386 index = (*typeList)[i-iendS];
08387 varReplacements.push_back(d_contextTerms[index]);
08388 }
08389 if((index < newIndex) || (!savedMap && i<iendS))
08390 recInstantiate(univ, all, savedMap, newIndex, varReplacements);
08391 else
08392 recInstantiate(univ, true, savedMap, newIndex, varReplacements);
08393 varReplacements.pop_back();
08394 }
08395
08396
08397 }
08398 }
08399
08400
08401
08402
08403
08404
08405 void TheoryQuant::mapTermsByType(const CDList<Expr>& terms)
08406 {
08407 Expr trExpr=trueExpr(), flsExpr = falseExpr();
08408 Type boolT = boolType();
08409 if(d_contextMap.count(boolT) == 0)
08410 {
08411 d_contextMap[boolT] =
08412 new(true) CDList<size_t>(theoryCore()->getCM()->getCurrentContext());
08413 size_t pos = d_contextTerms.size();
08414 d_contextTerms.push_back(trExpr);
08415 d_contextTerms.push_back(flsExpr);
08416 (*d_contextMap[boolT]).push_back(pos);
08417 (*d_contextMap[boolT]).push_back(pos+1);
08418 }
08419 for(size_t i=0; i<terms.size(); i++)
08420 recursiveMap(terms[i]);
08421
08422 for(size_t i=0; i<d_univs.size(); i++)
08423 recursiveMap(d_univs[i].getExpr());
08424 }
08425
08426
08427
08428
08429
08430
08431
08432
08433 bool TheoryQuant::recursiveMap(const Expr& e)
08434 {
08435 if(d_contextCache.count(e)>0) {
08436 return(d_contextCache[e]);
08437 }
08438 if(e.arity()>0) {
08439 for(Expr::iterator it = e.begin(), iend = e.end(); it!=iend; ++it)
08440
08441 if(recursiveMap(*it) == false) {
08442 d_contextCache[e] = false;
08443 }
08444 }
08445 else if(e.getKind() == EXISTS || e.getKind() == FORALL){
08446
08447 if(recursiveMap(e.getBody())==false) {
08448 d_contextCache[e]=false;
08449 }
08450 }
08451
08452 if(d_contextCache.count(e)>0) {
08453 return false;
08454 }
08455
08456 if(d_savedCache.count(e) > 0) {
08457 return true;
08458 }
08459
08460 Type type = getBaseType(e);
08461
08462 if(!type.isBool() && !(e.getKind()==BOUND_VAR)){
08463 TRACE("quant", "recursiveMap: found ",
08464 e.toString() + " of type " + type.toString(), "");
08465 int pos = d_contextTerms.size();
08466 d_contextTerms.push_back(e);
08467 if(d_contextMap.count(type)==0)
08468 d_contextMap[type] =
08469 new(true) CDList<size_t>(theoryCore()->getCM()->getCurrentContext());
08470 (*d_contextMap[type]).push_back(pos);
08471 }
08472
08473 if(e.getKind() == BOUND_VAR) {
08474 d_contextCache[e] = false;
08475 return false;
08476 }
08477 else {
08478 d_contextCache[e] = true;
08479 return true;
08480 }
08481
08482
08483
08484 }
08485
08486
08487
08488
08489 void TheoryQuant::notifyInconsistent(const Theorem& thm){
08490 #ifdef _CVC3_DEBUG_MODE
08491
08492 if( CVC3::debugger.trace("quant inscon") ){
08493
08494 cout<<"the one caused incsonsistency"<<endl;
08495 cout<<thm.getAssumptionsRef().toString()<<endl;
08496 std::vector<Expr> assump;
08497 thm.getLeafAssumptions(assump);
08498
08499 cout<<"===========leaf assumptions; =========="<<endl;
08500 for(std::vector<Expr>::iterator i=assump.begin(), iend=assump.end(); i!=iend; i++){
08501 cout<<">>"<<i->toString()<<endl;
08502 }
08503 }
08504 #endif
08505
08506 if(d_univs.size() == 0)
08507 return;
08508 DebugAssert(thm.getExpr().isFalse(), "notifyInconsistent called with"
08509 " theorem: " + thm.toString() + " which is not a derivation of false");
08510 TRACE("quant", "notifyInconsistent: { " , thm.toString(), "}");
08511
08512
08513 TRACE("quant terse", "notifyInconsistent: savedTerms size = ",
08514 d_savedTerms.size(), "");
08515 TRACE("quant terse", "last term: ",
08516 d_savedTerms.size()? d_savedTerms.back() : Expr(), "");
08517 }
08518
08519
08520
08521 void TheoryQuant::findInstAssumptions(const Theorem& thm)
08522 {
08523 if(thm.isNull() || thm.isRefl() || thm.isFlagged())
08524 return;
08525 thm.setFlag();
08526 const Expr& e = thm.getExpr();
08527 if(d_insts.count(e) > 0) {
08528 vector<Expr>& insts = d_insts[e];
08529 int pos;
08530 for(vector<Expr>::iterator it = insts.begin(), iend = insts.end(); it!=iend
08531 ; ++it)
08532 {
08533 if(d_savedCache.count(*it) == 0) {
08534 TRACE("quant", "notifyInconsistent: found:", (*it).toString(), "");
08535 d_savedCache[*it] = true;
08536 pos = d_savedTerms.size();
08537 d_savedTerms.push_back(*it);
08538 d_savedMap[getBaseType(*it)].push_back(pos);
08539 }
08540 }
08541 }
08542 if(thm.isAssump())
08543 return;
08544 const Assumptions& a = thm.getAssumptionsRef();
08545 for(Assumptions::iterator it =a.begin(), iend = a.end(); it!=iend; ++it){
08546 findInstAssumptions(*it);
08547 }
08548 }
08549
08550
08551 void TheoryQuant::computeType(const Expr& e)
08552 {
08553 switch (e.getKind()) {
08554 case FORALL:
08555 case EXISTS: {
08556 if(!e.getBody().getType().isBool())
08557 throw TypecheckException("Type mismatch for expression:\n\n "
08558 + e.getBody().toString()
08559 + "\n\nhas the following type:\n\n "
08560 + e.getBody().getType().toString()
08561 + "\n\nbut the expected type is Boolean:\n\n ");
08562 else
08563
08564 e.setType(e.getBody().getType());
08565 break;
08566 }
08567 default:
08568 DebugAssert(false,"Unexpected kind in Quantifier Theory: "
08569 + e.toString());
08570 break;
08571 }
08572 }
08573
08574
08575
08576
08577
08578
08579
08580
08581
08582 Expr TheoryQuant::computeTCC(const Expr& e) {
08583 DebugAssert(e.isQuantifier(), "Unexpected expression in Quantifier Theory: "
08584 + e.toString());
08585
08586 bool forall(e.getKind() == FORALL);
08587 const Expr& phi = e.getBody();
08588 Expr tcc_phi = getTCC(phi);
08589 Expr forall_tcc = getEM()->newClosureExpr(FORALL, e.getVars(), tcc_phi);
08590 Expr exists_tcc = getEM()->newClosureExpr(EXISTS, e.getVars(),
08591 tcc_phi && (forall? !phi : phi));
08592 return (forall_tcc || exists_tcc);
08593 }
08594
08595
08596 ExprStream&
08597 TheoryQuant::print(ExprStream& os, const Expr& e) {
08598 switch(os.lang()) {
08599 case SIMPLIFY_LANG:
08600 {
08601 switch(e.getKind()){
08602 case FORALL:
08603 case EXISTS: {
08604 if(!e.isQuantifier()) {
08605 e.print(os);
08606 break;
08607 }
08608 os << "(" << ((e.getKind() == FORALL)? "FORALL" : "EXISTS");
08609 const vector<Expr>& vars = e.getVars();
08610 bool first(true);
08611 os << "(" ;
08612 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
08613 i!=iend; ++i) {
08614 if(first) first = false;
08615 else os << " " ;
08616 os << *i;
08617
08618
08619
08620
08621 }
08622 os << ") " << e.getBody() << ")";
08623 }
08624 break;
08625 default:
08626 e.print(os);
08627 break;
08628 }
08629 break;
08630 }
08631 case TPTP_LANG:
08632 {
08633 switch(e.getKind()){
08634 case FORALL:
08635 case EXISTS: {
08636 if(!e.isQuantifier()) {
08637 e.print(os);
08638 break;
08639 }
08640 os << ((e.getKind() == FORALL)? " ! " : " ? ");
08641 const vector<Expr>& vars = e.getVars();
08642 bool first(true);
08643 os << "[" ;
08644 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
08645 i!=iend; ++i) {
08646 if(first) first = false;
08647 else os << "," ;
08648 os << *i ;
08649 if(i->isVar()) os << ": "<< (*i).getType() ;
08650 }
08651 os << "] : (" << e.getBody() <<")";
08652 }
08653 break;
08654 default:
08655 e.print(os);
08656 break;
08657 }
08658 break;
08659 }
08660
08661
08662 case PRESENTATION_LANG: {
08663 switch(e.getKind()){
08664 case FORALL:
08665 case EXISTS: {
08666 if(!e.isQuantifier()) {
08667 e.print(os);
08668 break;
08669 }
08670 os << "(" << push << ((e.getKind() == FORALL)? "FORALL" : "EXISTS")
08671 << space << push;
08672 const vector<Expr>& vars = e.getVars();
08673 bool first(true);
08674 os << "(" << push;
08675 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
08676 i!=iend; ++i) {
08677 if(first) first = false;
08678 else os << push << "," << pop << space;
08679 os << *i;
08680
08681
08682
08683 if(*d_translate || true){
08684 if(i->isVar())
08685 os << ":" << space << pushdag << (*i).getType() << popdag;
08686 }
08687 }
08688 os << push << ") " << pushdag << push;
08689
08690
08691 const vector<vector<Expr> >& triggers = e.getTrigs();
08692 for (vector<vector<Expr> >::const_iterator i=triggers.begin(), iend=triggers.end(); i != iend; ++i) {
08693
08694 const vector<Expr>& terms = (*i);
08695 if (terms.size() > 0) {
08696 os << push << ": PATTERN (" << pushdag << push;
08697 vector<Expr>::const_iterator j=terms.begin(), jend=terms.end();
08698 os << nodag << pushdag << *j << popdag; ++j;
08699 for(;j!=jend; ++j) {
08700 os << push << ", " << pop << space << pushdag << *j << popdag;
08701 }
08702 os << ") " << push;
08703 }
08704 }
08705
08706 os << ": " << pushdag << e.getBody() << push << ")";
08707 }
08708 break;
08709 default:
08710 e.print(os);
08711 break;
08712 }
08713 break;
08714 }
08715 case SMTLIB_LANG: {
08716 d_theoryUsed = true;
08717 switch(e.getKind()){
08718 case FORALL:
08719 case EXISTS: {
08720 if(!e.isQuantifier()) {
08721 e.print(os);
08722 break;
08723 }
08724 os << "(" << push << ((e.getKind() == FORALL)? "forall" : "exists")
08725 << space;
08726 const vector<Expr>& vars = e.getVars();
08727 bool first(true);
08728
08729 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
08730 i!=iend; ++i) {
08731 if(first) first = false;
08732 else os << space;
08733 os << "(" << push << *i;
08734
08735
08736 if(i->isVar())
08737 os << space << pushdag << (*i).getType() << popdag;
08738 os << push << ")" << pop << pop;
08739 }
08740 os << space << pushdag
08741 << e.getBody() << push;
08742
08743
08744 const vector<vector<Expr> >& triggers = e.getTrigs();
08745 for (vector<vector<Expr> >::const_iterator i=triggers.begin(), iend=triggers.end(); i != iend; ++i) {
08746
08747 const vector<Expr>& terms = (*i);
08748 if (terms.size() > 0) {
08749 os << push << space << ":pat {" << space << pushdag << push;
08750 vector<Expr>::const_iterator j=terms.begin(), jend=terms.end();
08751 os << nodag << pushdag << *j << popdag; ++j;
08752 for(;j!=jend; ++j) {
08753 os << space << pushdag << *j << popdag;
08754 }
08755 os << space << "}" << space << push;
08756 }
08757 }
08758 os << push << ")";
08759 break;
08760 }
08761 default:
08762 throw SmtlibException("TheoryQuant::print: SMTLIB_LANG: Unexpected expression: "
08763 +getEM()->getKindName(e.getKind()));
08764 break;
08765 }
08766 break;
08767 }
08768 case LISP_LANG: {
08769 switch(e.getKind()){
08770 case FORALL:
08771 case EXISTS: {
08772 if(!e.isQuantifier()) {
08773 e.print(os);
08774 break;
08775 }
08776 os << "(" << push << ((e.getKind() == FORALL)? "FORALL" : "EXISTS")
08777 << space;
08778 const vector<Expr>& vars = e.getVars();
08779 bool first(true);
08780 os << "(" << push;
08781 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
08782 i!=iend; ++i) {
08783 if(first) first = false;
08784 else os << space;
08785 os << "(" << push << *i;
08786
08787
08788 if(i->isVar())
08789 os << space << pushdag << (*i).getType() << popdag;
08790 os << push << ")" << pop << pop;
08791 }
08792 os << push << ")" << pop << pop << pushdag
08793 << e.getBody() << push << ")";
08794 }
08795 break;
08796 default:
08797 e.print(os);
08798 break;
08799 }
08800 break;
08801 }
08802 default:
08803 e.print(os);
08804 break;
08805 }
08806 return os;
08807 }
08808
08809
08810
08811
08812
08813 Expr
08814 TheoryQuant::parseExprOp(const Expr& e) {
08815 TRACE("parser", "TheoryQuant::parseExprOp(", e, ")");
08816
08817
08818 if(RAW_LIST != e.getKind()) return e;
08819
08820 DebugAssert(e.arity() > 0,
08821 "TheoryQuant::parseExprOp:\n e = "+e.toString());
08822
08823 const Expr& c1 = e[0][0];
08824 const string& opName(c1.getString());
08825 int kind = getEM()->getKind(opName);
08826 switch(kind) {
08827 case FORALL:
08828 case EXISTS: {
08829 if(!( (e.arity() == 3 || 4 == e.arity()) &&
08830 e[1].getKind() == RAW_LIST &&
08831 e[1].arity() > 0))
08832 throw ParserException("Bad "+opName+" expression: "+e.toString());
08833
08834
08835
08836 vector<pair<string,Type> > vars;
08837 for(Expr::iterator i=e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
08838 if(i->getKind() != RAW_LIST || i->arity() < 2)
08839 throw ParserException("Bad variable declaration block in "+opName
08840 +" expression: "+i->toString()
08841 +"\n e = "+e.toString());
08842
08843
08844
08845 Type tp(parseExpr((*i)[i->arity()-1]));
08846 if (tp == boolType()) {
08847 throw ParserException("A quantified variable may not be of type BOOLEAN");
08848 }
08849 for(int j=0, jend=i->arity()-1; j<jend; ++j) {
08850 if((*i)[j].getKind() != ID)
08851 throw ParserException("Bad variable declaration in "+opName+""
08852 " expression: "+(*i)[j].toString()+
08853 "\n e = "+e.toString());
08854 vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
08855 }
08856 }
08857
08858 vector<Expr> boundVars;
08859 for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
08860 i!=iend; ++i)
08861 boundVars.push_back(addBoundVar(i->first, i->second));
08862
08863 Expr body(parseExpr(e[2]));
08864
08865
08866 std::vector<std::vector<Expr> > patterns;
08867 if(e.arity() == 4){
08868 DebugAssert ((RAW_LIST == e[3].getKind()),"Unknown type for patterns"+e[3].toString());
08869 for(int i = 0; i < e[3].arity(); i++){
08870 const Expr& cur_trig(e[3][i]);
08871 DebugAssert ((RAW_LIST == cur_trig.getKind()),"Unknown type for cur_trig"+cur_trig.toString());
08872
08873 std::vector<Expr> cur_pattern;
08874 for(int j =0; j < cur_trig.arity(); j++){
08875 try {
08876 cur_pattern.push_back(parseExpr(cur_trig[j]));
08877 }
08878 catch (Exception e){
08879
08880
08881 cur_pattern.clear();
08882 }
08883 }
08884 if (cur_pattern.size() > 0 ){
08885
08886 patterns.push_back(cur_pattern);
08887 }
08888 }
08889 }
08890
08891
08892 Expr res;
08893 if(3 == e.arity()) {
08894 res = getEM()->newClosureExpr((kind == FORALL) ? FORALL : EXISTS,boundVars, body);
08895 }
08896 else{
08897 res = getEM()->newClosureExpr((kind == FORALL) ? FORALL : EXISTS,boundVars, body, patterns );
08898
08899
08900 }
08901 return res;
08902 break;
08903 }
08904 default:
08905 DebugAssert(false,
08906 "TheoryQuant::parseExprOp: invalid command or expression: " + e.toString());
08907 break;
08908 }
08909 return e;
08910 }
08911