57 for(std::set<Expr>::const_iterator i=boundVars.begin(),iend=boundVars.end(); i!=iend; ++i)
61 bool Trigger::isPos(){
65 bool Trigger::isNeg(){
66 return (
Neg==polarity ||
PosNeg==polarity);
69 std::vector<Expr> Trigger::getBVs(){
77 void Trigger::setHead(
Expr h){
85 void Trigger::setRWOp(
bool b){
89 bool Trigger::hasRW(){
93 void Trigger::setTrans(
bool b){
97 bool Trigger::hasTr(){
101 void Trigger::setTrans2(
bool b){
105 bool Trigger::hasTr2(){
109 void Trigger::setSimp(){
113 bool Trigger::isSimp(){
117 void Trigger::setSuperSimp(){
118 isSuperSimple =true ;
121 bool Trigger::isSuperSimp(){
122 return isSuperSimple;
125 void Trigger::setMultiTrig(){
129 bool Trigger::isMultiTrig(){
141 :
Theory(core,
"Quantified Expressions"),
142 d_univs(core->getCM()->getCurrentContext()),
143 d_rawUnivs(core->getCM()->getCurrentContext()),
144 d_arrayTrigs(core->getCM()->getCurrentContext()),
145 d_lastArrayPos(core->getCM()->getCurrentContext(), 0 , 0),
146 d_lastPredsPos(core->getCM()->getCurrentContext(), 0, 0),
147 d_lastTermsPos(core->getCM()->getCurrentContext(), 0, 0),
148 d_lastPartPredsPos(core->getCM()->getCurrentContext(), 0, 0),
149 d_lastPartTermsPos(core->getCM()->getCurrentContext(), 0, 0),
150 d_univsPartSavedPos(core->getCM()->getCurrentContext(), 0, 0),
151 d_lastPartLevel(core->getCM()->getCurrentContext(), 0, 0),
152 d_partCalled(core->getCM()->getCurrentContext(),false,0),
153 d_maxILReached(core->getCM()->getCurrentContext(),false,0),
154 d_usefulGterms(core->getCM()->getCurrentContext()),
155 d_lastUsefulGtermsPos(core->getCM()->getCurrentContext(), 0, 0),
156 d_savedTermsPos(core->getCM()->getCurrentContext(), 0, 0),
157 d_univsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
158 d_rawUnivsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
159 d_univsPosFull(core->getCM()->getCurrentContext(), 0, 0),
160 d_univsContextPos(core->getCM()->getCurrentContext(), 0, 0),
161 d_instCount(core->getCM()->getCurrentContext(), 0,0),
162 d_contextTerms(core->getCM()->getCurrentContext()),
163 d_contextCache(core->getCM()->getCurrentContext()),
164 d_maxQuantInst(&(core->getFlags()[
"max-quant-inst"].getInt())),
165 d_useNew(&(core->getFlags()[
"quant-new"].getBool())),
166 d_useLazyInst(&(core->getFlags()[
"quant-lazy"].getBool())),
167 d_useSemMatch(&(core->getFlags()[
"quant-sem-match"].getBool())),
168 d_useCompleteInst(&(core->getFlags()[
"quant-complete-inst"].getBool())),
169 d_translate(&(core->getFlags()[
"translate"].getBool())),
172 d_useInstLCache(&(core->getFlags()[
"quant-inst-lcache"].getBool())),
173 d_useInstGCache(&(core->getFlags()[
"quant-inst-gcache"].getBool())),
174 d_useInstThmCache(&(core->getFlags()[
"quant-inst-tcache"].getBool())),
175 d_useInstTrue(&(core->getFlags()[
"quant-inst-true"].getBool())),
176 d_usePullVar(&(core->getFlags()[
"quant-pullvar"].getBool())),
177 d_useExprScore(&(core->getFlags()[
"quant-score"].getBool())),
178 d_maxIL(&(core->getFlags()[
"quant-max-IL"].getInt())),
179 d_useTrans(&(core->getFlags()[
"quant-trans3"].getBool())),
180 d_useTrans2(&(core->getFlags()[
"quant-trans2"].getBool())),
181 d_useManTrig(&(core->getFlags()[
"quant-man-trig"].getBool())),
182 d_useGFact(&(core->getFlags()[
"quant-gfact"].getBool())),
183 d_gfactLimit(&(core->getFlags()[
"quant-glimit"].getInt())),
184 d_usePolarity(&(core->getFlags()[
"quant-polarity"].getBool())),
185 d_useNewEqu(&(core->getFlags()[
"quant-eqnew"].getBool())),
186 d_maxNaiveCall(&(core->getFlags()[
"quant-naive-num"].getInt())),
187 d_useNaiveInst(&(core->getFlags()[
"quant-naive-inst"].getBool())),
188 d_curMaxExprScore(core->getCM()->getCurrentContext(), (core->getFlags()[
"quant-max-score"].getInt()),0),
189 d_arrayIndic(core->getCM()->getCurrentContext()),
190 d_exprLastUpdatedPos(core->getCM()->getCurrentContext(),0 ,0),
191 d_trans_found(core->getCM()->getCurrentContext()),
192 d_trans2_found(core->getCM()->getCurrentContext()),
193 null_cdlist(core->getCM()->getCurrentContext()),
194 d_eqsUpdate(core->getCM()->getCurrentContext()),
195 d_lastEqsUpdatePos(core->getCM()->getCurrentContext(), 0, 0),
196 d_eqs(core->getCM()->getCurrentContext()),
197 d_eqs_pos(core->getCM()->getCurrentContext(), 0, 0),
198 d_allInstCount(core->getStatistics().counter(
"quantifier instantiations")),
199 d_allInstCount2(core->getStatistics().counter(
"quantifier instantiations2")),
200 d_totalInstCount(core->getStatistics().counter(
"quant total instantiations")),
201 d_trueInstCount(core->getStatistics().counter(
"quant true instantiations")),
202 d_abInstCount(core->getStatistics().counter(
"quant abandoned instantiations")),
203 d_instHistory(core->getCM()->getCurrentContext()),
204 d_alltrig_list(core->getCM()->getCurrentContext())
246 for(
size_t i=0; i<vec.size(); i++){
247 buf.append(vec[i].toString());
297 for(
int i = 0; i < t.
arity(); i++){
300 for(
int j = 0; j < i; j++){
301 if(t[i] == t[j])
return false;
313 for(
int i = 0; i < t.
arity(); i++){
314 if (t[i].arity()>0 )
return false;
345 cout<<
"in debug " <<
endl;
347 cout <<
"all gterms " <<
endl;
352 cout <<
" ============= all terms ========================== " <<
endl;
354 for(
size_t gtermIndex =0; gtermIndex < allterms.
size() ; gtermIndex++){
355 const Expr& curGterm = allterms[gtermIndex];
356 cout << gtermIndex <<
" :: " <<
getExprScore(curGterm) <<
" | " << curGterm <<
endl;
360 if(curRep != curGterm){
361 cout<<
"DIFF " <<curRep <<
endl;
372 if(curSig != curGterm){
373 cout<<
"DIFF " <<curSig <<
endl;
383 cout <<
" ============= all preds ========================== " <<
endl;
385 for(
size_t gtermIndex =0; gtermIndex < allpreds.
size() ; gtermIndex++){
386 const Expr& curGterm = allpreds[gtermIndex];
387 cout << gtermIndex <<
" :: " <<
getExprScore(curGterm) <<
" | " << curGterm <<
endl;
391 if(curRep != curGterm){
392 cout<<
"DIFF " <<curRep <<
endl;
403 if(curSig != curGterm){
404 cout<<
"DIFF " <<curSig <<
endl;
413 cout<<
"let us try more"<<
endl;
421 TRACE(
"quant update",
"eqs updated: ", t.
getExpr(),
"");
477 size_t backLen = backL.
size();
478 size_t forwLen = forwL.
size();
479 for(
size_t i =0; i < backLen; i++){
480 for(
size_t j =0; j < forwLen; j++){
488 size_t backLen = backL.
size();
489 size_t forwLen = forwL.
size();
490 for(
size_t i = 0; i < backLen; i++){
491 for(
size_t j = 0; j < forwLen; j++){
522 result.append(
"------ end map ------\n");
540 result.append(
"------ end map ------\n");
550 orgExprMap = newExprMap;
554 std::vector<ExprMap<Expr> > newVectorExprMap;
555 for(
size_t orgVectorIndex = 0; orgVectorIndex < orgVectorExprMap.size(); orgVectorIndex++){
558 newVectorExprMap.push_back(curExprMap);
560 orgVectorExprMap = newVectorExprMap;
588 std::vector<Expr> res;
592 TRACE(
"getsub",
"have ", res.size(),
" subterms");
618 std::vector<Expr> res;
622 TRACE(
"getsubs",
"getsubs, e is: ", e,
"");
623 TRACE(
"getsubs",
"e has ", res.size(),
" subterms");
626 return d_subTermsMap[e];
629 return (*iter).second;
634 static int max_score =-1;
639 TRACE(
"sendinst",
"partinst",partInst,
"");
649 if(cache->
find(bind_expr) !=cache->
end()){
653 (*cache)[bind_expr] =
true;
658 (*new_cache)[bind_expr] =
true;
666 TRACE(
"sendinst",
"gterm",gterm,
"");
677 if(gscore > max_score){
724 TRACE(
"quant sendinst",
"= gterm:",gterm,
"");
727 TRACE(
"quant sendinst",
"= add fact org: ", thm.
getExpr(),
"");
735 TRACE(
"quant sendinst",
"= begin univ id: ", univ_id,
"");
737 TRACE(
"quant sendinst",
"= begin gterm: ", gterm,
"");
746 TRACE(
"sendinst",
"partinst",partInst,
"");
749 vector<Expr> simpBind(orgBind);
750 for(
size_t orgBindIndex = 0; orgBindIndex < orgBind.size(); orgBindIndex++){
751 simpBind [orgBindIndex] =
simplifyExpr(orgBind[orgBindIndex]);
763 vector<Expr> bind(simpBind);
764 Expr bind_expr(simpBindList);
776 if(cache->
find(bind_expr) != cache->
end()){
781 (*cache)[bind_expr] =
true;
786 (*new_cache)[bind_expr] =
true;
796 if(cache->
find(bind_expr) != cache->
end()){
838 if(thm_iter != cache->
end()){
839 thm = thm_iter->second;
844 TRACE(
"sendinst",
"gterm",gterm,
"");
865 (*cache)[bind_expr] = thm;
872 TRACE(
"sendinst",
"gterm",gterm,
"");
894 (*new_cache)[bind_expr] = thm;
901 TRACE(
"sendinst",
"gterm",gterm,
"");
978 TRACE(
"quant sendinst",
"=gterm: ",gterm,
"");
988 TRACE(
"quant sendinst",
"= add fact org: ", thm.
getExpr(),
"");
990 TRACE(
"quant sendinst",
"= end === ",
"=========",
"============");
1016 (*cache)[bind] =
true;
1020 (*new_cache)[bind] =
true;
1159 std::set<Expr> result ;
1170 if ((
Neg == res[e] &&
Pos == pol) || (
Neg == res[e] &&
Pos == pol) ){
1178 TRACE(
"find-polarity", e,
"has ", (
int)pol);
1181 for(
int i=0; i<e.
arity(); i++){
1190 else if(
Neg == pol){
1199 for(
int i=0; i<e.
arity(); i++){
1262 vector<Expr> bVarsOut = thm_expr.
getVars();
1264 const Expr innerExists =outBody[0][1];
1266 vector<Expr> bVarsIn = innerExists.
getVars();
1268 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
1269 bVarsOut.push_back(*i);
1279 return newQuantExpr ;
1285 vector<Expr> bVarsOut = thm_expr.
getVars();
1287 const Expr innerForall=outBody[1];
1289 vector<Expr> bVarsIn = innerForall.
getVars();
1291 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
1292 bVarsOut.push_back(*i);
1297 if(outBody.
isAnd()){
1298 newbody=outBody[0].
andExpr(innerBody);
1300 else if(outBody.
isImpl()){
1301 newbody=outBody[0].
impExpr(innerBody);
1307 return(newQuantExpr);
1316 vector<Expr> bVarsOut = thm_expr.
getVars();
1318 const Expr innerExists = outBody[1];
1320 vector<Expr> bVarsIn = innerExists.
getVars();
1322 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
1323 bVarsOut.push_back(*i);
1327 if(outBody.
isAnd()){
1328 newbody=outBody[0].
andExpr(innerBody);
1330 else if(outBody.
isImpl()){
1331 newbody=outBody[0].
impExpr(innerBody);
1337 return newQuantExpr;
1346 d_quant_rules(quant_rule)
1355 for (
int i = 0 ; i < assert.
arity(); i++){
1402 set<Expr> heads_set;
1404 if (heads_set.count(macro_head) <= 0 ){
1422 bool has_macros =
false;
1423 for (
size_t i = 0 ; i < asserts.size(); i++){
1446 for (
int i = 0; i < macro_lhs.arity(); i++){
1447 if (macro_lhs[i].isBoundVar()){
1448 binding[macro_lhs[i]] = old[i];
1452 vector<Expr> quant_vars = macro_quant.
getVars();
1454 vector<Expr> gterms;
1455 for (
size_t i = 0 ; i < binding.size(); i++){
1456 gterms.push_back(binding[quant_vars[i]]);
1459 return macro_def.
substExpr(quant_vars,gterms);
1467 vector<Expr> children ;
1468 for (
int i = 0 ; i < assert.
arity(); i++){
1482 DebugAssert(
false,
"impossible case in recInstMacros");
1486 if (assert.
isEq() && assert[0] == assert[1]){
1493 cout <<assert<<
endl;
1494 DebugAssert(
false,
"impossible case in simplifyEq");
1504 vector<Expr> children ;
1505 for (
int i = 0 ; i < assert.
arity(); i++){
1519 DebugAssert(
false,
"impossible case in recInstMacros");
1538 DebugAssert(
false,
"impossible case in recInstMacors");
1547 return macro_quant_sub;
1556 for (
int i = 0; i<e.
arity(); i++){
1557 if (e[i].isBoundVar() ){
1565 else if (e.
arity() > 0 ){
1566 for (
int i = 0; i<e.
arity(); i++){
1582 for (
int i = 0; i<e.
arity(); i++){
1584 if ( e[i].containsBoundVar() && ( ! e[i].
isBoundVar() )){
1611 else if (e.
arity() > 0 ){
1612 for (
int i = 0; i<e.
arity(); i++){
1619 else if (e.
arity () == 0){
1622 DebugAssert(
false,
"impossible case in isShield");
1630 if ((
Neg == res[e] &&
Pos == pol) || (
Neg == res[e] &&
Pos == pol) ){
1641 for(
int i=0; i<e.
arity(); i++){
1650 else if(
Neg == pol){
1659 for(
int i=0; i<e.
arity(); i++){
1708 else if (e.
arity() > 0 ) {
1709 vector<Expr> children;
1710 for (
int i = 0 ; i < e.
arity(); i++){
1712 if (new_child.
isNot() && new_child[0].
isNot()){
1713 children.push_back(new_child[0][0]);
1716 children.push_back(new_child);
1720 if (new_expr.
isNot() && new_expr[0].
isNot()){
1721 return new_expr[0][0];
1734 TRACE(
"simp-quant", e ,
"\n ---rewriteNot---> \n", pos_expr);
1740 next_expr = packVarThm.
getExpr();
1743 next_expr = pos_expr;
1751 TRACE(
"simp-quant", e ,
"\n ---skolemize---> \n", ret);
1774 if (
Neg == pol_map[e]){
1788 else if (e.
arity() > 0 ) {
1789 vector<Expr> children;
1791 for (
int i = 0 ; i < e.
arity(); i++){
1793 if (new_child.
isNot() && new_child[0].
isNot()){
1794 children.push_back(new_child[0][0]);
1797 children.push_back(new_child);
1802 if (new_expr.
isNot() && new_expr[0].
isNot()){
1803 return new_expr[0][0];
1809 else if (0 == e.
arity() ){
1834 for (
int i = 0; i<e.
arity(); i++){
1854 else if (e.
arity() > 0 ){
1855 for (
int i = 0; i<e.
arity(); i++){
1866 Expr cur_expr = i->first;
1869 if (
isLE(cur_expr)){
1897 cout <<
" foall is " << forall_quant <<
endl;
1898 DebugAssert(
false,
"impossible case in collect index ");
1901 else if (cur_expr.
isEq()){
1923 DebugAssert(
false,
"impossible case collect index");
1931 DebugAssert(
false,
"impossible case in collect index");
1934 else if (
isLT(cur_expr)){
1962 DebugAssert(
false,
"impossible case in collect index");
1986 const Expr& cur_expr = i->first;
2025 if (bvs.size() <= 0 ) {
2035 iend = cur_expr_pol.
end();
2038 const Expr& cur_expr = i->first;
2056 DebugAssert(
false,
"error, Neg polarity in isGood ");
2061 DebugAssert(
false,
"error, found exists in is good");
2063 DebugAssert(
false,
"error, neg polarity in isGood ");
2115 vector<Expr> bvs = e.
getVars();
2117 for (vector<Expr>::iterator i = bvs.begin(), iend = bvs.end(); i != iend; i++){
2118 if ( !
isInt(i->getType() ) ){
2132 if ((i->first).isAtomicFormula()){
2133 const Expr& cur_expr = i->first;
2143 else if (
isLE(cur_expr) ||
isLT(cur_expr) || cur_expr.
isEq()){
2153 if (
Neg == pol &&
isLE(cur_expr)){
2180 void inst_helper(
int num_vars);
2212 std::vector<Expr>& d_old =
d_exprs, d_new;
2213 while (d_old.size() > 1) {
2214 int old_size = d_old.size();
2215 for (
int i = 0; i < old_size - 1; i += 2) {
2216 d_new.push_back(d_old[i].
andExpr(d_old[i + 1]));
2218 if (old_size % 2 == 1) {
2219 d_new.push_back(d_old[old_size - 1]);
2229 Expr CompleteInstPreProcessor::inst(
const Expr& assert){
2238 if (assert.
arity() > 0){
2239 vector<Expr> children;
2240 for (
int i = 0 ; i < assert.
arity(); i++){
2242 rep_child =
inst(assert[i]);
2243 children.push_back(rep_child);
2257 const vector<Expr>& bvs = forall.getVars();
2259 vector<Expr> and_list;
2265 if(bvs.size() == 1 ) {
2269 vector<Expr> inst_st;
2271 inst_st.push_back(*i);
2279 and_list.push_back(body.
substExpr(bvs,inst_st));
2283 else if (bvs.size() == 2 ){
2289 vector<Expr> inst_st;
2290 inst_st.push_back(*i);
2291 inst_st.push_back(*j);
2301 and_list.push_back(body.
substExpr(bvs,inst_st));
2314 return inster.
inst();
2328 else if (ands.
isNot() && ands[0].
isOr()){
2339 results.push_back(ands);
2347 if ( !
theoryCore()->getFlags()[
"quant-complete-inst"].getBool()){
2352 if (bvs.size() <= 0){
2356 std::vector<Expr> assertList;
2361 if (comp_inst_proc.
hasMacros(assertList)){
2362 for(
size_t i = 0; i < assertList.size();i++){
2364 assertList[i] = comp_inst_proc.
instMacros(assertList[i],
trueExpr().notExpr().notExpr());
2368 for(
size_t i = 0; i < assertList.size() ; i++){
2370 assertList[i] = comp_inst_proc.
simplifyQuant(assertList[i]);
2374 for(
size_t i = 0; i < assertList.size() ; i++){
2375 if ( ! comp_inst_proc.
isGood(assertList[i])){
2382 for(
size_t i = 0; i < assertList.size() ; i++){
2387 vector<Expr> new_asserts;
2388 for(
size_t i = 0; i < assertList.size() ; i++){
2389 Expr new_asser = comp_inst_proc.
inst(assertList[i]);
2395 new_asserts.push_back(new_asser);
2436 for(
size_t i = 0; i < new_asserts.size() ; i++){
2437 new_asserts[i] = comp_inst_proc.
simplifyEq(new_asserts[i]);
2440 for(
size_t i = 0; i < new_asserts.size() ; i++){
2468 if (bvs.size() >= bVarsThm.size()){
2469 for(
size_t i=0; i<bVarsThm.size(); i++) {
2470 if (bvs.find(bVarsThm[i]) == bvs.end()){
2485 int bvar_missing = 0;
2488 if(bvs.size() <= 0)
return false;
2490 for(
size_t i=0; i<bVarsThm.size(); i++) {
2491 if (bvs.find(bVarsThm[i]) == bvs.end()){
2496 if (0 == bvar_missing){
2500 if(bvar_missing <= offset){
2520 size_t bvar_missing = 0;
2523 for(
size_t i=0; i<bVarsThm.size(); i++) {
2524 if (bvs.find(bVarsThm[i]) == bvs.end()){
2529 if (0 == bvar_missing){
2533 if(0 == bvs.size()){
2537 if(bvar_missing < bVarsThm.size()){
2571 bool no_bound =
true;
2586 if(good && no_bound) {
2589 else if(good && !no_bound){
2601 std::vector<Expr> res;
2618 std::vector<Expr> res;
2622 for(
size_t i=0; i<subs.size(); i++){
2623 int kind = subs[i].getKind();
2625 const Expr& name = subs[i][0];
2626 const Expr& index = subs[i][1];
2629 tp.push_back(index);
2640 const std::vector<Expr> thmBVs,
2645 dynTrig newDynTrig(trig, bv_map,univ_id);
2658 for(
size_t i = 0; i<thmBVs.size(); i++){
2659 bv_map[thmBVs[i]] = thmBVs[i];
2666 Expr genTrig = trig_ex;
2669 dynTrig newDynTrig(trig,bv_map,univ_id);
2674 if(cur_trig_map.end() == iter){
2676 cur_trig_map[head] = new_cd_map;
2677 vector<dynTrig>* new_dyntrig_list =
new vector<dynTrig>;
2678 (*new_cd_map)[genTrig] = new_dyntrig_list;
2679 (*new_dyntrig_list).push_back(newDynTrig);
2684 if(cd_map->
end() == iter_map){
2685 vector<dynTrig>* new_dyntrig_list =
new vector<dynTrig>;
2686 (*cd_map)[genTrig] = new_dyntrig_list;
2687 (*new_dyntrig_list).push_back(newDynTrig);
2692 (*(iter_map->second)).push_back(newDynTrig);
2812 for(
int i=0; i<t1.
arity(); i++){
2813 if (
false ==
canMatch(t1[i], t2[i] , env))
2827 if(3==cur_trig.size()){
2828 const Expr& t1=cur_trig[0];
2829 const Expr& t2=cur_trig[1];
2830 const Expr& t3=cur_trig[2];
2836 if ( 2==ts1.size() && 2==ts2.size() && 2==ts2.size() &&
2837 (ts1 != ts2) && (ts2 != ts3) && (ts3 != ts1)){
2839 for(set<Expr>::const_iterator i=ts1.begin(), iend = ts1.end(); i != iend; i++){
2842 for(set<Expr>::const_iterator i=ts2.begin(), iend = ts2.end(); i != iend; i++){
2845 for(set<Expr>::const_iterator i=ts3.begin(), iend = ts3.end(); i != iend; i++){
2850 for(set<Expr>::const_iterator i=all.begin(), iend = all.end(); i != iend; i++){
2870 for(
size_t i = 0; i < all_terms.size(); i++){
2871 if(all_terms[i].isEq()){
2872 const Expr& cur = all_terms[i];
2873 if(cur[0] != cur[1] && ( (cur[0]==tr2[0] && cur[1]==tr2[1]) || (cur[0]==tr2[1] && cur[1]==tr2[0]))){
2885 for( std::vector<Expr>::const_iterator i = bVars.begin(), iend= bVars.end(); i!=iend; i++) {
2886 bvar_found[*i]=
false;
2889 for (
size_t i=0; i< exprs.size();i++){
2890 const std::set<Expr> & bv_in_trig =
getBoundVars(exprs[i]);
2891 for(std::set<Expr>::const_iterator j=bv_in_trig.begin(), jend = bv_in_trig.end(); j != jend; j++){
2892 if(bvar_found.
find(*j) != bvar_found.
end()){
2893 bvar_found[*j]=
true;
2898 for( std::vector<Expr>::const_iterator i = bVars.begin(), iend= bVars.end(); i!=iend; i++) {
2899 if(
false == bvar_found[*i]){
2907 inline size_t locVar(
const vector<Expr>& bvsThm,
const Expr& bv){
2908 for(
size_t i=0, iend = bvsThm.size(); i < iend; i++){
2909 if (bvsThm[i] == bv){
2925 const std::vector<Expr>& bVarsThm = e.
getVars();
2930 for(
size_t i=0; i<new_trigs.size(); i++){
2931 registerTrig(trig_maps, new_trigs[i], bVarsThm, univs_id);
2936 std::vector<Trigger>& new_mult_trigs =
d_multTrigs[e];
2937 for(
size_t j=0; j<new_mult_trigs.size(); j++){
2938 registerTrig(trig_maps, new_mult_trigs[j], bVarsThm, univs_id);
2957 const std::vector<Expr> subterms =
getSubTrig(e);
2975 std::vector<Expr> trig_list;
2976 std::vector<Expr> trig_cadt;
2977 for(std::vector<Expr>::const_iterator i = subterms.begin(),iend=subterms.end(); i!=iend; i++){
2979 trig_cadt.push_back(*i);
2985 std::vector<std::vector<Expr> > man_trigs = e.
getTriggers();
2986 for(std::vector<std::vector<Expr> >::const_iterator i=man_trigs.begin(), iend=man_trigs.end(); i != iend; i++){
2989 trig_list.push_back((*i)[0]);
2998 else if(2 == i->size()){
3000 trig_list.push_back((*i)[0]);
3001 trig_list.push_back((*i)[1]);
3008 for(
size_t iter =0; iter < trig_cadt.size(); iter++) {
3009 Expr* i = &(trig_cadt[iter]);
3010 bool notfound =
true;
3012 for(
size_t index=0; index< trig_list.size(); index++){
3014 trig_list[index]=*i;
3018 if (trig_list[index].subExprOf(*i)) {
3024 trig_list.push_back(*i);
3029 std::vector<Trigger> trig_ex;
3031 for (
size_t i=0; i< trig_list.size();i++){
3032 const Expr& cur = trig_list[i];
3035 if(score > 0)
continue;
3040 for(
size_t j=0; j< trig_cadt.size(); j++){
3041 if (trig_list[i] == trig_cadt[j])
continue;
3043 if (
canMatch(trig_list[i], trig_cadt[j], null)){
3047 trig_list.size() == 2 &&
3048 trig_list[i].arity() == 2 &&
3049 BOUND_VAR == trig_list[i][0].getKind() &&
3050 BOUND_VAR == trig_list[i][1].getKind() &&
3051 BOUND_VAR == trig_cadt[j][0].getKind() &&
3052 BOUND_VAR == trig_cadt[j][1].getKind() &&
3060 TRACE(
"triggers",
"trans2 found ", trig_list[i],
"");
3137 if(t_ex != NULL) t_ex->
setRWOp(
true);
3141 trig_ex.push_back(*t_ex);
3148 TRACE(
"triggers",
"new:full trigger score:", score,
"");
3149 TRACE(
"triggers",
"new:full trigger pol:", pol,
"");
3158 for(
size_t i=0; i<trig_ex.size(); i++){
3160 registerTrig(trig_maps,trig_ex[i], bVarsThm, univs_id);
3161 TRACE(
"triggers",
"new extra :full triggers:", trig_ex[i].getEx().toString(),
"");
3165 TRACE(
"triggers warning",
"no full trig: ", e ,
"");
3174 std::vector<std::vector<Expr> > man_trig = e.
getTriggers();
3176 for(std::vector<std::vector<Expr> >::const_iterator i = man_trig.begin(), iend = man_trig.end(); i != iend; i++){
3178 if (i->size() > 1) count++;
3195 if (1 == count && 2 == man_trig[count-1].size()){
3196 for(std::vector<Expr>::const_iterator j = man_trig[count-1].begin(), jend = man_trig[count-1].end(); j != jend; ++j){
3197 cur_trig.push_back(*j);
3206 for( std::vector<Expr>::const_iterator i = subterms.begin(), iend=subterms.end(); i!=iend; i++) {
3208 bool notfound =
true;
3223 TRACE(
"multi-triggers",
"good set of multi triggers",
"",
"");
3232 TRACE(
"multi-triggers",
"bad set of multi triggers",
"",
"");
3244 Expr ex = cur_trig[0];
3258 registerTrig(trig_maps,*trans_trig, bVarsThm, univs_id);
3260 TRACE(
"triggers",
" trans like found ", ex,
"");
3267 if(cur_trig.size() >0 ){
3269 std::vector<Expr> posList, negList;
3270 for(
size_t k=0; k<cur_trig.size(); k++){
3271 const Expr& cur_item = cur_trig[k];
3275 posList.push_back(cur_item);
3278 negList.push_back(cur_item);
3283 TRACE(
"multi-triggers",
"good set of multi triggers pos",
"",
"");
3284 for (
size_t i=0; i< posList.size();i++){
3285 TRACE(
"multi-triggers",
"multi-triggers:", posList[i].toString(),
"");
3288 for(
size_t m=0; m<posList.size(); m++){
3289 cur_trig.push_back(posList[m]);
3293 TRACE(
"multi-triggers",
"good set of multi triggers neg",
"",
"");
3294 for (
size_t i=0; i< negList.size();i++){
3295 TRACE(
"multi-triggers",
"multi-triggers:", negList[i].toString(),
"");
3298 for(
size_t m=0; m<negList.size(); m++){
3299 cur_trig.push_back(negList[m]);
3308 if( 3 == cur_trig.size() || 4 == cur_trig.size() || 5 == cur_trig.size() || 6 == cur_trig.size() ){
3309 for(
size_t i = 0; i < cur_trig.size(); i++){
3310 for(
size_t j = 0; j < i; j++){
3311 vector<Expr> tempList;
3313 tempList.push_back(cur_trig[i]);
3314 tempList.push_back(cur_trig[j]);
3319 cur_trig.push_back(tempList[0]);
3320 cur_trig.push_back(tempList[1]);
3331 if(cur_trig.size() != 2){
3332 if( 0 == cur_trig.size()){
3348 for(
size_t i = 0 ; i<cur_trig.size(); i++){
3362 for(
size_t i =0, iend =
d_multTrigs[e].size(); i<iend; i++){
3363 const std::vector<Expr>& one_set_bvs =
d_multTrigs[e][i].bvs;
3364 std::vector<size_t> one_set_pos;
3366 for(
size_t v = 0, vend = one_set_bvs.size(); v<vend; v++){
3367 size_t loc =
locVar(bVarsThm, one_set_bvs[v]);
3369 one_set_pos.push_back(loc);
3373 sort(one_set_pos.begin(), one_set_pos.end());
3375 for(
size_t v = 0, vend = one_set_pos.size(); v<vend; v++){
3378 multTrigs.
var_pos.push_back(one_set_pos);
3382 vector<size_t> common;
3383 std::vector<size_t>& tar1 = multTrigs.
var_pos[0];
3384 std::vector<size_t>& tar2 = multTrigs.
var_pos[1];
3385 vector<size_t>::iterator t1(tar1.begin()), t2(tar2.begin());
3386 while(t1 != tar1.end() && t2!= tar2.end()){
3389 if( pos1 == pos2 ) {
3390 common.push_back(pos1);
3394 else if( pos1 > pos2 ){
3404 for(
size_t i =0; i< multi_size; i++){
3486 const std::vector<Expr>& bvsOutmost = thm.
getVars();
3489 return int(bvs.size()-bvsOutmost.size());
3509 TRACE(
"quant assertfact",
"assertFact => ", thm.
toString(),
"{");
3515 TRACE(
"quant assertfact",
"assertFact => (ignoring existential) }", expr.
toString(),
"");
3520 "Theory of quantifiers cannot handle expression "
3524 if(expr[0].isForall()) {
3527 else if(expr[0].isExists()) {
3530 result =
iffMP(thm, rule);
3539 if(result.getExpr().isForall()){
3546 vector<Expr>::const_iterator it = vars.begin(), iend = vars.end();
3547 for (; it != iend; ++it) {
3548 card = (*it).getType().card();
3553 u = (*it).getType().sizeFinite();
3556 if (count == 0 || count > 100) {
3561 bool incomplete =
false;
3562 if (count > 0 && count <= 100) {
3563 vector<Expr> terms(vars.size());
3564 vector<Unsigned> indices(vars.size());
3565 for (
unsigned i = 0; i < vars.size(); ++i) {
3567 terms[i] = vars[i].getType().enumerateFinite(0);
3568 if (terms[i].isNull()) {
3578 while (i < indices.size()) {
3579 indices[i] = indices[i] + 1;
3580 if (indices[i] < vars[i].getType().sizeFinite()) {
3581 terms[i] = vars[i].getType().enumerateFinite(indices[i]);
3582 if (terms[i].isNull()) {
3591 if (i == indices.size())
break;
3592 for (
unsigned j = 0; j < i; ++j) {
3594 terms[j] = vars[j].getType().enumerateFinite(0);
3599 if (!incomplete)
return;
3604 if(result.getExpr().getBody().isForall()){
3616 if(result.getExpr().isForall()){
3665 TRACE(
"quant assertfact",
"assertFact => old-fashoin enqueueing: ", result.toString(),
"}");
3671 TRACE(
"quant assertfact",
"assertFact => non-forall enqueueing: ", result.toString(),
"}");
3701 const std::vector<Expr>& bVars,
3702 std::vector<Expr>& newInst,
3703 std::set<std::vector<Expr> >& instSet)
3705 size_t curPos = newInst.size();
3706 if (bVars.size() == curPos) {
3709 std::vector<Expr> temp = newInst;
3710 instSet.insert(temp);
3717 if (0 == tyExprs.size()) {
3721 for (
size_t i=0;i<tyExprs.size();i++){
3722 newInst.push_back(tyExprs[i]);
3741 Expr const_expr, minus ,pos;
3742 int numMinus=0, numPos=0, numConst=0;;
3743 for(
int i=0; i<e.
arity(); i++){
3744 if((e[i]).getKind() ==
MULT){
3763 if(1==numPos && 1==numConst && 1==numMinus){
3774 Expr const_expr, minus ,pos;
3775 int numMinus=0, numPos=0, numConst=0;;
3777 for(
int i=0; i<e.
arity(); i++){
3778 if((e[i]).getKind() ==
MULT){
3798 if(1==numPos && 1==numConst && 1==numMinus){
3799 if(
isIntx(const_expr,0)){
3804 return Expr(
PLUS, const_expr, pos);
3815 for(
int i=0; i< parent.
arity(); i++){
3816 const Expr& child = parent[i];
3823 iter->second->push_back(parent);
3853 eqs_hash[
d_eqs[i]]=
true;
3858 const Expr& cur_ex = iter->first;
3862 for(
size_t i=0; i<cur_parents->
size(); i++){
3863 changed_hash[(*cur_parents)[i]]=
true;
3952 TRACE(
"multmatch",
"not same kind", gterm , vterm);
3958 vector<Expr> allGterms;
3959 allGterms.push_back(gterm);
3966 while (curCandidateGterm != gterm){
3972 allGterms.push_back(curCandidateGterm);
3980 vector<ExprMap<Expr> > returnBinds;
3981 for(
size_t curGtermIndex =0; curGtermIndex < allGterms.size(); curGtermIndex++)
3983 vector<ExprMap<Expr> > currentBinds(binds);
3985 if(0 == currentBinds.size()){
3987 currentBinds.push_back(emptyEnv);
3990 Expr gterm = allGterms[curGtermIndex];
3992 vector<ExprMap<Expr> > nextBinds;
3994 for(
int i = 0 ; i< gterm.
arity(); i++){
3995 const Expr& curVterm = vterm[i];
3996 const Expr& curGterm = gterm[i];
3998 for(
size_t curEnvIndex =0; curEnvIndex < currentBinds.size(); curEnvIndex++){
4003 if ( iterVterm != curEnv.
end()){
4005 nextBinds.push_back(curEnv);
4010 nextBinds.push_back(curEnv);
4015 nextBinds.push_back(curEnv);
4019 vector<ExprMap<Expr> > newBinds;
4020 newBinds.push_back(curEnv);
4021 bool goodChild =
recMultMatch(curGterm, curVterm, newBinds);
4023 for(vector<
ExprMap<Expr> >::iterator i = newBinds.begin(), iend = newBinds.end(); i != iend; i++){
4024 nextBinds.push_back(*i);
4029 currentBinds = nextBinds;
4032 for(
size_t curBindsIndex=0; curBindsIndex < currentBinds.size(); curBindsIndex++){
4033 returnBinds.push_back(currentBinds[curBindsIndex]);
4039 binds = returnBinds;
4040 return (binds.size() > 0) ?
true :
false;
4046 vector<ExprMap<Expr> > currentBinds(binds);
4048 if(0 == currentBinds.size()){
4050 currentBinds.push_back(emptyEnv);
4053 vector<ExprMap<Expr> > nextBinds;
4055 const Expr& curVterm = vterm;
4056 const Expr& curGterm = gterm;
4058 for(
size_t curEnvIndex =0; curEnvIndex < currentBinds.size(); curEnvIndex++){
4060 vector<ExprMap<Expr> > newBinds;
4061 newBinds.push_back(curEnv);
4062 bool goodChild =
recMultMatch(curGterm, curVterm, newBinds);
4064 for(vector<
ExprMap<Expr> >::iterator i = newBinds.begin(), iend = newBinds.end(); i != iend; i++){
4065 nextBinds.push_back(*i);
4070 return (binds.size() > 0) ?
true :
false;
4076 for(
size_t g_index = gbegin; g_index < gend; g_index++){
4078 const Expr& gterm = glist[g_index];
4107 for(;iter_trig != iter_trig_end; iter_trig++){
4110 for(
size_t cur_index =0; cur_index < cur_list->
size(); cur_index++){
4112 const Trigger& cur_trig = (*cur_list)[cur_index].
trig;
4113 size_t univ_id = (*cur_list)[cur_index].univ_id;
4114 vector<ExprMap<Expr> > binds;
4128 for(
size_t i=0; i<binds.size(); i++){
4130 vector<Expr> bind_vec;
4131 const vector<Expr>& bVarsThm =
d_univs[univ_id].getExpr().getVars();
4132 for(
size_t j=0; j< bVarsThm.size(); j++){
4133 bind_vec.push_back(cur_map[bVarsThm[j]]);
4135 synNewInst(univ_id, bind_vec, gterm, cur_trig);
4139 else if ( cur_list->
size() > 1){
4143 const Expr& general_vterm = (*iter_trig).first;
4148 vector<ExprMap<Expr> > binds;
4156 newTopMatch(gterm, general_vterm, binds, cur_trig);
4158 for(
size_t bindsIndex = 0 ; bindsIndex < binds.size() ; bindsIndex++){
4162 if(binds.size() <= 0)
continue;
4164 for(
size_t trig_index = 0; trig_index< cur_list->
size(); trig_index++){
4165 size_t univ_id = (*cur_list)[trig_index].univ_id;
4166 const ExprMap<Expr>& trig_map = (*cur_list)[trig_index].binds;
4167 const Trigger& ind_cur_trig = (*cur_list)[trig_index].
trig;
4168 for(
size_t i=0; i<binds.size(); i++){
4170 vector<Expr> bind_vec;
4171 const vector<Expr>& bVarsThm =
d_univs[univ_id].getExpr().getVars();
4172 for(
size_t j=0; j< bVarsThm.size(); j++){
4173 const Expr& inter=(*(trig_map.
find(bVarsThm[j]))).second;
4174 const Expr& inter2 = cur_map[inter];
4175 bind_vec.push_back(inter2);
4179 synNewInst(univ_id, bind_vec, gterm, ind_cur_trig);
4195 for(; i!=iend; i++){
4199 for(; j!=jend; j++){
4200 Expr general_trig = j->first;
4201 vector<dynTrig>* trigs = j->second;
4204 delete cur_new_cd_map;
4213 for(; i!=iend; i++){
4215 Expr head = i->first;
4224 for(; j!=jend; j++){
4225 Expr general_trig = j->first;
4226 vector<dynTrig>* trigs = j->second;
4230 (*old_cd_map)[general_trig] = old_cd_list;
4231 for(
size_t k=0; k<trigs->size(); k++){
4243 for(; j!=jend; j++){
4244 Expr general_trig = j->first;
4245 vector<dynTrig>* trigs = j->second;
4248 if(old_cd_map->
end() == old_trigs_iter){
4252 (*old_cd_map)[general_trig] = old_cd_list;
4255 old_cd_list = (*old_trigs_iter).second;
4257 for(
size_t k=0; k<trigs->size(); k++){
4277 for(
size_t g_index = gbegin; g_index<gend; g_index++){
4279 const Expr& gterm = glist[g_index];
4294 if(new_trigs.end() == iter)
continue;
4304 for(;iter_trig != iter_trig_end; iter_trig++){
4306 vector<dynTrig>* cur_list = (*iter_trig).second;
4308 for(
size_t cur_index =0; cur_index < cur_list->size(); cur_index++){
4309 const Trigger& cur_trig = (*cur_list)[cur_index].
trig;
4317 size_t univ_id = (*cur_list)[cur_index].univ_id;
4318 vector<ExprMap<Expr> > binds;
4322 for(
size_t i=0; i<binds.size(); i++){
4324 vector<Expr> bind_vec;
4325 const vector<Expr>& bVarsThm =
d_univs[univ_id].getExpr().getVars();
4326 for(
size_t j=0; j< bVarsThm.size(); j++){
4327 bind_vec.push_back(cur_map[bVarsThm[j]]);
4329 synNewInst(univ_id, bind_vec, gterm, cur_trig);
4333 else if ( cur_list->size() > 1){
4343 const Expr& general_vterm = (*iter_trig).first;
4345 vector<ExprMap<Expr> > binds;
4346 newTopMatch(gterm, general_vterm, binds, cur_trig);
4348 if(binds.size() <= 0)
continue;
4349 for(
size_t trig_index = 0; trig_index< cur_list->size(); trig_index++){
4350 size_t univ_id = (*cur_list)[trig_index].univ_id;
4351 const Trigger& ind_cur_trig = (*cur_list)[trig_index].
trig;
4352 const ExprMap<Expr>& trig_map = (*cur_list)[trig_index].binds;
4354 for(
size_t i=0; i<binds.size(); i++){
4356 vector<Expr> bind_vec;
4357 const vector<Expr>& bVarsThm =
d_univs[univ_id].getExpr().getVars();
4358 for(
size_t j=0; j< bVarsThm.size(); j++){
4359 const Expr& inter=(*(trig_map.
find(bVarsThm[j]))).second;
4360 const Expr& inter2 = cur_map[inter];
4361 bind_vec.push_back(inter2);
4363 synNewInst(univ_id, bind_vec, gterm, ind_cur_trig);
4386 for(
int i = vterm.
arity()-1; i>=0 ; i--){
4389 binds.push_back(cur_bind);
4395 for(
int i = vterm.
arity()-1; i>=0 ; i--){
4408 binds.push_back(cur_bind);
4487 else if(
isLE(vterm) ||
isLT(vterm)){
4617 vector<ExprMap<Expr> > oldBinds;
4619 vector<ExprMap<Expr> > newBinds;
4622 vector<ExprMap<Expr> > oldBindsBack(oldBinds);
4623 vector<ExprMap<Expr> > newBindsBack(newBinds);
4628 if (
false && oldBinds != newBinds){
4630 cout<<
"let us see" <<
endl;
4631 cout<<
"===gterm is : " << gtermOrg <<
endl ;;
4637 cout <<
"\n---gterm sig is: " << sig <<
endl;
4646 for(
size_t oldBindsIndex = 0; oldBindsIndex < oldBinds.size(); oldBindsIndex++){
4647 cout <<
"--O- " << oldBindsIndex <<
endl;
4654 for(
size_t newBindsIndex = 0; newBindsIndex < newBinds.size(); newBindsIndex++){
4655 cout <<
"--N- " << newBindsIndex <<
endl;
4688 for(
int i = vterm.
arity()-1; i>=0 ; i--){
4691 binds.push_back(cur_bind);
4697 for(
int i = vterm.
arity()-1; i>=0 ; i--){
4710 binds.push_back(cur_bind);
4764 cout<<
"impossible here in new top match"<<
endl;
4765 cout<<
"vterm "<<vterm<<
endl;
4766 cout<<
"gterm " <<gterm<<
endl;
4768 cout<<
"gtrue and gfalse: " << gtrue<<
" |and| " <<gfalse<<
endl;
4794 else if(
isLE(vterm) ||
isLT(vterm)){
5295 if(e1.
isNull())
return true;
5296 if(e2.
isNull())
return false;
5312 TRACE(
"quant match", gterm ,
" VS ", vterm);
5315 DebugAssert (binds.size() == 1,
"binds.size() > 1");
5321 if ( iterVterm != curEnv.
end()){
5340 if ( vhead !=
getHead(gterm) ){
5358 vector<ExprMap<Expr> > candidateNewEnvs;
5359 bool newwayResult(
false);
5362 vector<Expr> candidateGterms;
5365 while (curCandidateGterm != gterm){
5369 candidateGterms.push_back(curCandidateGterm);
5376 for(
size_t curGtermIndex = 0 ; curGtermIndex < candidateGterms.size(); curGtermIndex++){
5377 const Expr& curGterm = candidateGterms[curGtermIndex];
5378 if(
getHead(curGterm) == vhead){
5379 vector<ExprMap<Expr> > newBinds;
5380 newBinds.push_back(orginalEnv);
5387 for(
size_t newBindsIndex = 0; newBindsIndex < newBinds.size(); newBindsIndex++){
5388 candidateNewEnvs.push_back(newBinds[newBindsIndex]);
5395 if (candidateNewEnvs.size() >= 1){
5397 newwayResult =
true;
5400 newwayResult =
false;
5405 vector<ExprMap<Expr> > candidateOldEnvs;
5411 for(
size_t i = 0; i < gls->
size(); i++){
5412 const Expr& curGterm = (*gls)[i];
5418 DebugAssert((*gls)[i].arity() == vterm.
arity(),
"gls has different arity");
5420 vector<ExprMap<Expr> > newBinds ;
5421 newBinds.push_back(orginalEnv);
5422 bool goodMatching(
false);
5428 for(
size_t newBindsIndex = 0; newBindsIndex < newBinds.size(); newBindsIndex++){
5429 candidateOldEnvs.push_back(newBinds[newBindsIndex]);
5437 bool oldwayResult(
false);
5439 if(candidateOldEnvs.size() >= 1){
5440 oldwayResult =
true;
5443 oldwayResult =
false;
5448 if( candidateNewEnvs.size() != candidateOldEnvs.size()){
5453 if(oldwayResult != newwayResult){
5459 binds = candidateOldEnvs;
5461 return oldwayResult;
5483 DebugAssert (binds.size() == 1,
"binds.size() > 1");
5489 if ( iterVterm != curEnv.
end()){
5505 if ( vhead !=
getHead(gterm) ){
5518 TRACE(
"quant multmatch",
"-- begin multi equality matching -- ",
"" ,
"");
5519 TRACE(
"quant multmatch",
"vterm: " , vterm,
"");
5520 TRACE(
"quant multmatch",
"gterm: " , gterm,
"");
5524 vector<ExprMap<Expr> > candidateOldEnvs;
5531 for(
size_t i = 0; i < gls->
size(); i++){
5532 const Expr& curGterm = (*gls)[i];
5536 TRACE(
"quant multmatch",
"same head term ", curGterm,
"");
5539 DebugAssert((*gls)[i].arity() == vterm.
arity(),
"gls has different arity");
5540 vector<ExprMap<Expr> > newBinds ;
5541 newBinds.push_back(orginalEnv);
5542 bool goodMatching(
false);
5546 TRACE(
"quant multmatch",
"old curGterm: ", curGterm,
"");
5547 TRACE(
"quant multmatch",
"old simplifed curGterm: ",
simplifyExpr(curGterm),
"");
5548 for(
size_t newBindsIndex = 0; newBindsIndex < newBinds.size(); newBindsIndex++){
5549 candidateOldEnvs.push_back(newBinds[newBindsIndex]);
5551 TRACE(
"quant multmatch",
"pushed oldEnvs " , newBinds.size(),
"");
5557 bool oldwayResult(
false);
5559 if(candidateOldEnvs.size() >= 1){
5560 oldwayResult =
true;
5563 oldwayResult =
false;
5566 TRACE(
"quant multmatch",
"old env size" ,candidateOldEnvs.size(),
"");
5567 binds = candidateOldEnvs;
5568 return oldwayResult;
5588 TRACE(
"quant match", gterm ,
" VS ", vterm);
5591 DebugAssert (binds.size() == 1,
"binds.size() > 1");
5596 if ( iterVterm != curEnv.
end()){
5612 if ( vhead !=
getHead(gterm) ){
5626 TRACE(
"quant multmatch",
"-- begin multi equality matching -- ",
"" ,
"");
5627 TRACE(
"qunat multmatch",
"vterm: " , vterm,
"");
5628 TRACE(
"qunat multmatch",
"gterm: " , gterm,
"");
5631 vector<ExprMap<Expr> > candidateNewEnvs;
5632 bool newwayResult(
false);
5635 vector<Expr> candidateGterms;
5641 while (curCandidateGterm != gterm){
5643 TRACE(
"quant multmatch",
"pushed candidate gterm ",
getExprScore(curCandidateGterm),
" # " + curCandidateGterm.
toString());
5646 candidateGterms.push_back(curCandidateGterm);
5651 for(
size_t curGtermIndex = 0 ; curGtermIndex < candidateGterms.size(); curGtermIndex++){
5652 const Expr& curGterm = candidateGterms[curGtermIndex];
5653 if(
getHead(curGterm) == vhead){
5654 vector<ExprMap<Expr> > newBinds;
5655 newBinds.push_back(orginalEnv);
5658 TRACE(
"quant multmatch",
"found new match: ",
"" ,
"");
5659 TRACE(
"quant multmatch",
"curGterm: ", curGterm ,
"");
5662 for(
size_t newBindsIndex = 0; newBindsIndex < newBinds.size(); newBindsIndex++){
5663 candidateNewEnvs.push_back(newBinds[newBindsIndex]);
5665 TRACE(
"quant multmathc",
"pushed newEnvs ", newBinds.size(),
"");
5670 if (candidateNewEnvs.size() >= 1){
5671 TRACE(
"quant multmacht",
"found more matcings: " , candidateNewEnvs.size(),
"");
5672 newwayResult =
true;
5675 newwayResult =
false;
5679 TRACE(
"quant multmatch",
"new env size " , candidateNewEnvs.size(),
"");
5680 binds = candidateNewEnvs;
5681 return newwayResult;
6693 const Expr& var = order[pos];
6694 for(
size_t i=0; i<border.size(); i++){
6695 if (border[i] == var)
return i;
7215 for(
size_t i=0; i<tp.size(); i++){
7216 const Expr& index = tp[i];
7217 std::vector<Expr> temp;
7218 temp.push_back(index);
7226 for(
size_t k=0; k<dtForw.
size(); k++){
7227 vector<Expr> tri_bind;
7228 tri_bind.push_back(sr);
7229 tri_bind.push_back(dt);
7230 tri_bind.push_back(dtForw[k]);
7237 for(
size_t k=0; k<srBack.
size(); k++){
7238 vector<Expr> tri_bind;
7239 tri_bind.push_back(srBack[k]);
7240 tri_bind.push_back(sr);
7241 tri_bind.push_back(dt);
7249 vector<Expr> result;
7251 for(
int i =0 ; i < org.
arity(); i++){
7262 vector<Expr> actual_bind;
7263 for(
size_t i=0, iend=bind.size(); i<iend; i++){
7265 actual_bind.push_back(bind[i]);
7277 if (oldBindMap->
end() != cur_iter){
7281 (*oldBindMap)[actual_bind_expr] =
true;
7286 const vector<size_t>& comm_pos = mtriginfo.
common_pos[0];
7287 size_t comm_pos_size = comm_pos.size();
7290 vector<Expr> comm_expr_vec;
7291 for(
size_t i = 0; i < comm_pos_size; i++){
7292 comm_expr_vec.push_back(bind[comm_pos[i]]);
7295 if(0 == comm_pos_size){
7303 vector<Expr> uncomm_expr_vec;
7305 const vector<size_t>& uncomm_pos = mtriginfo.
var_pos[index];
7306 size_t uncomm_pos_size = uncomm_pos.size();
7307 for(
size_t i = 0; i< uncomm_pos_size; i++){
7308 uncomm_expr_vec.push_back(bind[uncomm_pos[i]]);
7310 if(0 == uncomm_pos_size){
7322 size_t other_index = 0;
7326 else if (1 == index){
7330 FatalAssert(
false,
"Sorry, only two vterms in a multi-trigger.");
7333 add_into_iter = mtriginfo.
uncomm_list[index]->find(comm_expr);
7335 if(mtriginfo.
uncomm_list[index]->end() == add_into_iter){
7337 (*mtriginfo.
uncomm_list[index])[comm_expr] = add_into_list;
7340 add_into_list = add_into_iter->second;
7356 for(
ExprMap<
CDList<Expr>* >::iterator otherMapIter = otherMapBegin; otherMapIter != otherMapEnd; otherMapIter++){
7359 if(simpCommExpr != otherCommonExpr)
continue;
7368 if(comm_expr != otherMapIter->first) {
7371 iter_list = otherMapIter->second;
7372 const vector<size_t>& uncomm_iter_pos = mtriginfo.
var_pos[other_index];
7373 size_t uncomm_iter_pos_size = uncomm_iter_pos.size();
7375 for(
size_t i =0, iend = iter_list->
size(); i<iend; i++){
7376 const Expr& cur_iter_expr = (*iter_list)[i];
7377 vector<Expr> new_bind(bind);
7378 for(
size_t j=0; j<uncomm_iter_pos_size; j++){
7379 new_bind[uncomm_iter_pos[j]] = cur_iter_expr[j];
7390 vector<Expr> actual_bind;
7391 for(
size_t i=0; i<bind.size(); i++){
7393 actual_bind.push_back(bind[i]);
7396 if(actual_bind.size() != 2){
7402 actual_bind[0]=acb1;
7403 actual_bind[1]=acb2;
7420 vector<Expr> actual_bind;
7421 for(
size_t i=0; i<bind.size(); i++){
7432 Expr sr(actual_bind[0]);
7433 Expr dt(actual_bind[1]);
7438 while (cur_next != dt) {
7447 while (cur_next != sr) {
7672 int numUsefulMultTriger = 0;
7673 for(
size_t i = 0; i < d_all_multTrigsInfo.size(); i++){
7681 if(uncommonMapOne->
size() != 0 || uncommonMapTwo->
size() != 0 ){
7682 numUsefulMultTriger++;
7687 if(uncommonMapOne->
size() == 0 ) {
7699 vector<pair<Expr, CDList<Expr>* > > oneFoundTerms;
7700 for(
ExprMap<
CDList<Expr>* >::iterator iterOne=iterOneBegin; iterOne != iterOneEnd; iterOne++){
7705 oneFoundTerms.push_back(*iterOne);
7711 vector<pair<Expr, CDList<Expr>* > >twoFoundTerms;
7712 for(
ExprMap<
CDList<Expr>* >::iterator iterTwo = iterTwoBegin; iterTwo != iterTwoEnd; iterTwo++){
7716 twoFoundTerms.push_back(*iterTwo);
7720 for(
size_t i= 0 ; i< oneFoundTerms.
size(); i++){
7721 for(
size_t j= 0 ; j< twoFoundTerms.
size(); j++){
7722 pair<Expr, CDList<Expr>* > pairOne = oneFoundTerms[i];
7723 pair<Expr, CDList<Expr>* > pairTwo = twoFoundTerms[j];
7724 if(pairOne.first == pairTwo.first)
continue;
7730 for(
size_t oneIter = 0; oneIter < oneExprList->
size(); oneIter++){
7732 for(
size_t twoIter = 0; twoIter < twoExprList->
size(); twoIter++){
7733 Expr gterm1 = (*oneExprList)[oneIter][0];
7734 Expr gterm2 = (*twoExprList)[twoIter][0];
7738 bind.push_back(gterm1);
7739 bind.push_back(rightTerm);
7740 bind.push_back(gterm2);
7741 size_t univID = curMultiTrigger.
univ_id;
7754 bind.push_back(gterm2);
7755 bind.push_back(rightTerm);
7756 bind.push_back(gterm1);
7812 #ifdef _CVC3_DEBUG_MODE
7814 if( CVC3::debugger.trace(
"quant assertfact") ){
7815 cout<<
"===========all cached univs =========="<<
endl;
7823 if( CVC3::debugger.trace(
"quant samehead") ){
7824 cout<<
"===========all cached =========="<<
endl;
7826 cout<<
"------------------------------------"<<
endl;
7827 cout<<(i->first)<<endl;
7828 cout<<
"_______________________"<<
endl;
7830 for(
size_t i =0; i<terms->
size(); i++){
7831 cout<<(*terms)[i]<<
endl;
7838 #ifdef _CVC3_DEBUG_MODE
7839 if( CVC3::debugger.trace(
"quant checksat") ){
7841 cout<<
"=========== cur pred & terms =========="<<
endl;
7845 cout<<
"i="<<allpreds[i].getIndex()<<
" :"<<
findExpr(allpreds[i])<<
"|"<<allpreds[i]<<
endl;
7851 cout<<
"i="<<allterms[i].getIndex()<<
" :"<<
findExpr(allterms[i])<<
"|"<<allterms[i]<<
endl;
7853 cout<<
"=========== cur quant =========="<<
endl;
7854 for (
size_t i=0; i<
d_univs.size(); i++){
7860 if( CVC3::debugger.trace(
"quant checksat equ") ){
7862 cout<<
"=========== cur pred equ =========="<<
endl;
7865 if(allpreds[i].isEq()){
7866 cout<<
"i="<<allpreds[i].getIndex()<<
" :"<<
findExpr(allpreds[i])<<
"|"<<allpreds[i]<<
endl;
7869 cout<<
"=========== cur pred equ end =========="<<
endl;
7879 Expr t = allterms[i];
7894 Expr t = allpreds[i];
7922 const Expr& t = allpreds[i];
7925 const Expr lterm = t[0];
7926 const Expr rterm = t[1];
7959 const Expr& cur=allterms[i];
7980 if(fullEffort ||
theoryCore()->getCM()->scopeLevel() <= 5 ||
true){
8026 static int counter =0;
8028 std::set<Expr> types;
8029 for(
size_t i = 0; i<
d_univs.size(); i++){
8031 const std::vector<Expr> cur_vars = cur_quant.
getVars();
8032 for(
size_t j =0; j<cur_vars.size(); j++){
8033 types.insert(cur_vars[j].getType().getExpr());
8037 std::string base(
"_naiveInst");
8038 for(std::set<Expr>::iterator i=types.begin(), iend = types.end(); i != iend; i++){
8040 std::stringstream tempout;
8042 std::string out_str = base + tempout.str();
8059 newConstThm = newExpr.
eqExpr(newExpr2);
8127 size_t uSize =
d_univs.size() ;
8130 size_t tSize = allterms.
size();
8131 size_t pSize = allpreds.
size();
8136 TRACE(
"quant", fullEffort,
" fulleffort:scope ",
theoryCore()->getCM()->scopeLevel() );
8139 const Expr& cur(allterms[i]);
8159 const Expr& cur=allpreds[i];
8188 TRACE(
"inend",
"debug 1",
"" ,
"" );
8199 delete changed_terms;
8204 TRACE(
"inend",
"debug 2",
" # ",n );
8208 bool hasMoreGterms(
false);
8212 hasMoreGterms=
false;
8217 for(
size_t i=0; i<tSize; i++){
8218 const Expr& cur(allterms[i]);
8230 hasMoreGterms =
true;
8231 TRACE(
"inend",
"is this good? ", cur.
toString()+
" #-# " , score);
8246 for(
size_t i=0; i<pSize; i++){
8247 const Expr& cur(allpreds[i]);
8259 hasMoreGterms =
true;
8260 TRACE(
"inend",
"is this good? ", cur.
toString()+
" #-# " , score);
8324 TRACE(
"inend",
"debug 3 1",
"" ,
"" );
8342 TRACE(
"inend",
"debug 3 2",
"" ,
"" );
8355 TRACE(
"inend",
"debug 3 0",
"",
"");
8387 TRACE(
"quant",
"checkSat ", fullEffort,
"{");
8390 if(
true || (fullEffort && uSize > 0)) {
8404 TRACE(
"quant",
"checkSat [saved insts]: univs size = ", uSize ,
" ");
8416 TRACE(
"quant",
"checkSat [context insts]: univs size = ", uSize ,
" ");
8422 TRACE(
"quant",
"checkSat terms size = ", assertions.
size() ,
" ");
8432 TRACE(
"quant terse",
"checkSat total insts: ",
8437 TRACE(
"quant",
"checkSat effort:", fullEffort,
" }");
8454 if(!all && ((savedMap && newIndex ==
d_savedTerms.size())
8458 TRACE(
"quant",
"instanitate", all ,
"{");
8459 std::vector<Expr> varReplacements;
8461 TRACE(
"quant",
"instanitate",
"",
"}");
8468 std::vector<Expr>& varReplacements)
8471 const vector<Expr>& boundVars = quantExpr.
getVars();
8473 size_t curPos = varReplacements.size();
8474 TRACE(
"quant",
"recInstantiate: ", boundVars.size() - curPos,
"");
8476 if(curPos == boundVars.size()) {
8494 int iendC=0, iendS=0, iend;
8495 std::vector<size_t>* typeVec = NULL;
8499 iendS = typeVec->size();
8500 TRACE(
"quant",
"adding from savedMap: ", iendS,
"");
8505 iendC = typeList->
size();
8506 TRACE(
"quant",
"adding from contextMap:", iendC ,
"");
8509 iend = iendC + iendS;
8510 for(
int i =0; i<iend; i++) {
8511 TRACE(
"quant",
"I must have gotten here!",
"",
"");
8514 index = (*typeVec)[i];
8518 index = (*typeList)[i-iendS];
8521 if((index < newIndex) || (!savedMap && i<iendS))
8525 varReplacements.pop_back();
8551 for(
size_t i=0; i<terms.
size(); i++)
8554 for(
size_t i=0; i<
d_univs.size(); i++)
8595 TRACE(
"quant",
"recursiveMap: found ",
8622 #ifdef _CVC3_DEBUG_MODE
8624 if( CVC3::debugger.trace(
"quant inscon") ){
8626 cout<<
"the one caused incsonsistency"<<
endl;
8628 std::vector<Expr> assump;
8631 cout<<
"===========leaf assumptions; =========="<<
endl;
8632 for(std::vector<Expr>::iterator i=assump.begin(), iend=assump.end(); i!=iend; i++){
8633 cout<<
">>"<<i->toString()<<
endl;
8641 " theorem: " + thm.
toString() +
" which is not a derivation of false");
8642 TRACE(
"quant",
"notifyInconsistent: { " , thm.
toString(),
"}");
8645 TRACE(
"quant terse",
"notifyInconsistent: savedTerms size = ",
8647 TRACE(
"quant terse",
"last term: ",
8660 vector<Expr>& insts =
d_insts[e];
8662 for(vector<Expr>::iterator it = insts.begin(), iend = insts.end(); it!=iend
8666 TRACE(
"quant",
"notifyInconsistent: found:", (*it).toString(),
"");
8691 +
"\n\nhas the following type:\n\n "
8693 +
"\n\nbut the expected type is Boolean:\n\n ");
8700 DebugAssert(
false,
"Unexpected kind in Quantifier Theory: "
8723 tcc_phi && (forall? !phi : phi));
8724 return (forall_tcc || exists_tcc);
8740 os <<
"(" << ((e.
getKind() ==
FORALL)?
"FORALL" :
"EXISTS");
8741 const vector<Expr>& vars = e.
getVars();
8744 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
8746 if(first) first =
false;
8754 os <<
") " << e.
getBody() <<
")";
8773 const vector<Expr>& vars = e.
getVars();
8776 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
8778 if(first) first =
false;
8781 if(i->isVar()) os <<
": "<< (*i).getType() ;
8783 os <<
"] : (" << e.
getBody() <<
")";
8804 const vector<Expr>& vars = e.
getVars();
8807 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
8809 if(first) first =
false;
8810 else os << push <<
"," <<
pop <<
space;
8823 const vector<vector<Expr> >& triggers = e.
getTriggers();
8824 for (vector<vector<Expr> >::const_iterator i=triggers.begin(), iend=triggers.end(); i != iend; ++i) {
8826 const vector<Expr>& terms = (*i);
8827 if (terms.size() > 0) {
8829 vector<Expr>::const_iterator j=terms.begin(), jend=terms.end();
8831 for(;j!=jend; ++j) {
8858 const vector<Expr>& vars = e.
getVars();
8861 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
8863 if(first) first =
false;
8865 os <<
"(" <<
push << *i;
8877 const vector<vector<Expr> >& triggers = e.
getTriggers();
8878 for (vector<vector<Expr> >::const_iterator i=triggers.begin(), iend=triggers.end(); i != iend; ++i) {
8880 const vector<Expr>& terms = (*i);
8882 if (terms.size() > 0) {
8884 vector<Expr>::const_iterator j=terms.begin(), jend=terms.end();
8886 for(;j!=jend; ++j) {
8889 os << space <<
"}" << space <<
push;
8896 throw SmtlibException(
"TheoryQuant::print: SMTLIB_LANG: Unexpected expression: "
8913 const vector<Expr>& vars = e.
getVars();
8916 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
8918 if(first) first =
false;
8920 os <<
"(" << push << *i;
8925 os << push <<
")" <<
pop <<
pop;
8929 const vector<vector<Expr> >& triggers = e.
getTriggers();
8930 if( !triggers.empty() ) {
8931 os << space << push <<
"(!";
8936 for (vector<vector<Expr> >::const_iterator i=triggers.begin(), iend=triggers.end(); i != iend; ++i) {
8938 const vector<Expr>& terms = (*i);
8939 if (terms.size() > 0) {
8940 os << push << space <<
":pattern" << space << push <<
"(" ;
8941 vector<Expr>::const_iterator j=terms.begin(), jend=terms.end();
8943 for(;j!=jend; ++j) {
8946 os <<
")" << pop <<
space ;
8949 if( !triggers.empty() ) {
8956 throw SmtlibException(
"TheoryQuant::print: SMTLIB_LANG: Unexpected expression: "
8973 const vector<Expr>& vars = e.
getVars();
8976 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
8978 if(first) first =
false;
8980 os <<
"(" << push << *i;
8985 os << push <<
")" <<
pop <<
pop;
8988 << e.
getBody() << push <<
")";
9010 if(
theoryCore()->getFlags()[
"unknown-check-model"].getBool()) {
9011 throw ParserException(
"ERROR: +unknown-check-model unsafe with quantifiers");
9014 TRACE(
"parser",
"TheoryQuant::parseExprOp(", e,
")");
9020 "TheoryQuant::parseExprOp:\n e = "+e.
toString());
9022 const Expr& c1 = e[0][0];
9023 const string& opName(c1.getString());
9035 vector<pair<string,Type> > vars;
9037 if(i->getKind() !=
RAW_LIST || i->arity() < 2)
9039 +
" expression: "+i->toString()
9046 throw ParserException(
"A quantified variable may not be of type BOOLEAN");
9048 for(
int j=0, jend=i->arity()-1; j<jend; ++j) {
9049 if((*i)[j].getKind() !=
ID)
9051 " expression: "+(*i)[j].toString()+
9053 vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
9057 vector<Expr> boundVars;
9058 for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
9060 boundVars.push_back(
addBoundVar(i->first, i->second));
9065 std::vector<std::vector<Expr> > patterns;
9068 for(
int i = 0; i < e[3].
arity(); i++){
9069 const Expr& cur_trig(e[3][i]);
9072 std::vector<Expr> cur_pattern;
9073 for(
int j =0; j < cur_trig.
arity(); j++){
9075 cur_pattern.push_back(
parseExpr(cur_trig[j]));
9080 if(
theoryCore()->getFlags()[
"translate"].getBool()) {
9084 cur_pattern.clear();
9087 if (cur_pattern.size() > 0 ){
9089 patterns.push_back(cur_pattern);
9096 if(3 == e.
arity()) {
9109 "TheoryQuant::parseExprOp: invalid command or expression: " + e.
toString());
virtual Theorem simplify(const Expr &e)
Simplify a term e and return a Theorem(e==e')
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
ExprStream & pop(ExprStream &os)
Restore the indentation.
std::string exprMap2string(const ExprMap< Expr > &vec)
std::queue< Theorem > d_univsQueue
universally quantified formulas to be instantiated, the var bindings is in d_bingQueue and the ground...
const Expr & getExpr() const
CDO< int > d_instCount
number of instantiations made in given context
iterator begin() const
Begin iterator.
bool isGround(const Expr &e)
std::vector< Expr > d_exprs
void findPolarityAtomic(const Expr &e, ExprMap< Polarity > &res, Polarity pol)
ExprStream & nodag(ExprStream &os)
std::vector< std::vector< size_t > > var_pos
TheoryCore * theoryCore()
Get a pointer to theoryCore.
void collectChangedTerms(CDList< Expr > &changed_terms)
void setFlag() const
Set the generic flag.
void newTopMatchNoSig(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
Data structure of expressions in CVC3.
const Theorem & getFind() const
ExprMap< CDMap< Expr, bool > * > d_bindHistory
bool isSuperSimpleTrig(const Expr &t)
typeMap d_savedMap
a map of types to positions in the d_savedTerms vector
QuantProofRules * d_quant_rules
void recGoodSemMatch(const Expr &e, const std::vector< Expr > &bVars, std::vector< Expr > &newInst, std::set< std::vector< Expr > > &instSet)
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
~TheoryQuant()
Destructor.
An exception thrown by the parser.
QuantProofRules * d_rules
quantifier theorem production rules
Expr getHeadExpr(const Expr &e)
void matchListNew(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs, const CDList< Expr > &list, size_t gbegin, size_t gend)
static const Expr null_expr
virtual void setIncomplete(const std::string &reason)
Mark the current decision branch as possibly incomplete.
void findPolarity(const Expr &e, ExprMap< Polarity > &res, Polarity pol)
StatCounter d_totalInstCount
void collect_shield_index(const Expr &e)
bool isUniterpFunc(const Expr &e)
const CLFlags & getFlags() const
void pushBackList(const Expr &node, Expr ex)
const std::set< Expr > & d_all_index
const bool * d_useManTrig
const bool * d_useInstLCache
ExprMap< std::hash_map< Expr, bool > * > d_bindGlobalHistory
CompleteInstPreProcessor(TheoryCore *, QuantProofRules *)
const CDList< Expr > & getPredicates()
Get list of predicates.
bool isGoodFullTrigger(const Expr &e, const std::vector< Expr > &bVarsThm)
TheoryQuant(TheoryCore *core)
categorizes all the terms contained in an expressions by type.
const bool * d_useExprScore
Expr recInstMacros(const Expr &assert)
static bool recursiveGetBoundVars(const Expr &e, std::set< Expr > &result)
get the bound vars in term e,
void combineOldNewTrigs(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)
void newTopMatchSig(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
CDList< Expr > & backList(const Expr &ex)
bool isSimpleTrig(const Expr &t)
Expr instMacros(const Expr &, const Expr)
substitute a macro in assert
An exception to be thrown at typecheck error.
iterator find(const Expr &e)
CDO< size_t > d_univsContextPos
tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed wh...
void clearFlags() const
Clear the generic flag in all Exprs.
std::string exprMap2stringSig(const ExprMap< Expr > &vec)
void set(const T &data, int scope=-1)
static bool recursiveGetPartTriggers(const Expr &e, std::vector< Expr > &res)
struct CVC3::dynTrig dynTrig
Expr substMacro(const Expr &)
void matchListOld(const CDList< Expr > &list, size_t gbegin, size_t gend)
void collectIndex(const Expr &e)
collect index for instantiation
Expr recSkolemize(const Expr &, ExprMap< Polarity > &)
CDList< Expr > null_cdlist
Expr pullVarOut(const Expr &)
ExprMap< CDList< Expr > * > d_parent_list
CDList< Expr > & forwList(const Expr &ex)
const bool * d_usePolarity
void getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const
virtual Theorem addNewConst(const Expr &e)=0
size_t locVar(const vector< Expr > &bvsThm, const Expr &bv)
CDO< size_t > d_savedTermsPos
tracks a possition in the savedTerms map
CDO< int > d_curMaxExprScore
std::map< Type, CDList< size_t > *,TypeComp > d_contextMap
a map of types to posisitions in the d_contextTerms list
virtual Theorem assumpRule(const Expr &a, int scope=-1)=0
void collect_forall_index(const Expr &forall_quant)
Expr recRewriteNot(const Expr &, ExprMap< Polarity > &)
for output in TPTP format
MS C++ specific settings.
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
void debug(int i)
Used to notify the quantifier algorithm of possible instantiations that were used in proving a contex...
virtual Theorem rewriteNotForall(const Expr &e)=0
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
void add_parent(const Expr &parent)
virtual Theorem boundVarElim(const Theorem &t1)=0
From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e where vars' is obtained from vars by remo...
virtual Theorem universalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel, Expr gterm)=0
Instantiate a universally quantified formula.
ExprMap< CDList< Expr > * > d_trans_forw
Expr computeTCC(const Expr &e)
Lisp-like format for automatically generated specs.
std::set< Expr > getBoundVars(const Expr &e)
get bound vars in term e,
Expr eqExpr(const Expr &right) const
const bool * d_useSemMatch
use lazy instantiation
ExprMap< std::vector< Trigger > > d_multTrigs
ExprStream & space(ExprStream &os)
Insert a single white space separator.
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
ExprMap< std::vector< Expr > > d_insts
a map of instantiated universals to a vector of their instantiations
#define DebugAssert(cond, str)
std::string exprMap2stringSimplify(const ExprMap< Expr > &vec)
const bool * d_useInstTrue
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
void assertFact(const Theorem &e)
Theory interface function to assert quantified formulas.
std::vector< std::vector< size_t > > common_pos
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
CDList< Theorem > d_rawUnivs
unsigned getQuantLevelForTerm(const Expr &e)
Get quantification level at which this term was introduced.
std::vector< CDMap< Expr, bool > * > var_binds_found
void simplifyVectorExprMap(std::vector< ExprMap< Expr > > &orgVectorExprMap)
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
const std::vector< std::vector< Expr > > & getTriggers() const
Get the manual triggers of the closure Expr.
bool multMatchChild(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, bool top=false)
void addIndex(const Expr &e)
insert an index
virtual Theorem rewriteNotExists(const Expr &e)=0
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
void setTrans2Found(const Expr &comb)
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
virtual Expr skolemize(const Expr &e)=0
bool isIntx(const Expr &e, const Rational &x)
T & push_back(const T &data, int scope=-1)
bool isPlus(const Expr &e)
iterator find(const key_type &key)
operations
CDList< dynTrig > d_arrayTrigs
Expr d_mybvs[MAX_TRIG_BVS]
Expr andExpr(const Expr &right) const
ExprMap< std::hash_map< Expr, Theorem > * > d_bindGlobalThmHistory
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void inst_helper(int num_vars)
bool isMinus(const Expr &e)
bool isRational(const Expr &e)
const bool * d_translate
Try complete instantiation.
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
ExprStream & pushdag(ExprStream &os)
std::queue< Theorem > d_simplifiedThmQueue
Expr orExpr(const std::vector< Expr > &children)
std::vector< ExprMap< CDList< Expr > * > * > uncomm_list
void recInstantiate(Theorem &univ, bool all, bool savedMap, size_t newIndex, std::vector< Expr > &varReplacements)
does most of the work of the instantiate function.
Context * getCurrentContext()
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
std::vector< Expr > getPartTriggers(const Expr &e)
StatCounter d_allInstCount
Expr impExpr(const Expr &right) const
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
CDO< size_t > d_lastUsefulGtermsPos
tracks the position in d_usefulGterms
CDO< size_t > d_lastArrayPos
Op getOp() const
Get operator from expression.
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
e1 AND (e1 IFF e2) ==> e2
static void recursiveGetSubTrig(const Expr &e, std::vector< Expr > &res)
ExprMap< Expr > d_macro_def
size_t count(const Expr &e) const
std::map< Type, std::vector< Expr >, TypeComp > d_typeExprMap
CommonProofRules * getCommonRules()
Get a pointer to common proof rules.
CDO< size_t > d_univsSavedPos
tracks a possition in the database of universals
CDO< size_t > d_rawUnivsSavedPos
void registerTrig(ExprMap< ExprMap< std::vector< dynTrig > * > * > &cur_trig_map, Trigger trig, const std::vector< Expr > thmBVs, size_t univ_id)
const bool * d_useLazyInst
use new way of instantiation
CDList< Theorem > d_univs
database of universally quantified theorems
int trigInitScore(const Expr &e)
std::vector< Expr > d_savedTerms
a vector of all of the terms that have produced conflicts.
Expr simplifyEq(const Expr &)
simplify a=a to True
Expr newStringExpr(const std::string &s)
int hasMoreBVs(const Expr &thm)
test if a sub-term contains more bounded vars than quantified by out-most quantifier.
int getExprScore(const Expr &e)
ExprMap< CDList< Expr > * > d_trans_back
bool canMatch(const Expr &t1, const Expr &t2, ExprMap< Expr > &env)
Expr minusOne(const Expr &e)
return e-1
const bool * d_useInstGCache
int loc_gterm(const std::vector< Expr > &border, const Expr >erm, int pos)
Identifier is (ID (STRING_EXPR "name"))
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
std::string toString() const
ExprMap< std::set< std::vector< Expr > > > d_tempBinds
std::string toString() const
Print the expression to a string.
Expr simplifyQuant(const Expr &)
put all quants in postive form and then skolemize all exists
Expr inst(const Expr &e)
inst forall quant using index from collectIndex
void notifyInconsistent(const Theorem &thm)
Used to notify the quantifier algorithm of possible instantiations that were used in proving a contex...
int exprScore(const Expr &e)
Main implementation of ValidityChecker for CVC3.
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
std::vector< Expr > getSubTrig(const Expr &e)
const Theorem & getSig() const
virtual Theorem partialUniversalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel)=0
bool isMacro(const Expr &assert)
if assert is a macro definition
const CDList< Expr > & getTerms()
Get list of terms.
void collectHeads(const Expr &assert, std::set< Expr > &heads)
bool isFlagged() const
Check if the flag attribute is set.
Expr iffExpr(const Expr &right) const
const Theorem & getEqNext() const
std::queue< Expr > d_gBindQueue
const Theorem & getRep() const
bool isGoodPartTrigger(const Expr &e, const std::vector< Expr > &bVarsThm)
void flatAnds(const Expr &ands, vector< Expr > &results)
void newTopMatch(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
void synCheckSat(ExprMap< ExprMap< std::vector< dynTrig > * > * > &, bool)
void arrayHeuristic(const Trigger &trig, size_t univid)
int d_initMaxScore
all instantiations
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
ExprMap< CDList< Expr > * > d_same_head_expr
const Expr & getBody() const
Get the body of the closure Expr.
std::string int2string(int n)
Expr simplifyExpr(const Expr &e)
Simplify a term e w.r.t. the current context.
std::string vectorExpr2string(const std::vector< Expr > &vec)
CDMap< Expr, bool > d_trans_found
ExprMap< Expr > d_quant_equiv_map
const Expr & getRHS() const
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
static const size_t MAX_TRIG_BVS
const bool * d_useInstThmCache
TheoryCore * d_theoryCore
Theorem theoryPreprocess(const Expr &e)
Theory-specific preprocessing.
std::string toString() const
CDMap< Expr, bool > d_trans2_found
const Expr & falseExpr()
Return FALSE Expr.
void enqueueInst(const Theorem, const Theorem)
const Expr & trueExpr()
Return TRUE Expr.
Expr addBoundVar(const std::string &name, const Type &type)
Create and add a new bound variable to the stack, for parseExprOp().
void computeType(const Expr &e)
computes the type of a quantified term. Always a boolean.
bool isGoodMultiTrigger(const Expr &e, const std::vector< Expr > &bVarsThm, int offset)
const Assumptions & getAssumptionsRef() const
bool hasShieldVar(const Expr &e)
int d_inEnd
set if the fullEffort = 1
StatCounter d_trueInstCount
void addNotifyEq(Theory *t, const Expr &e)
Register a callback for every equality.
void iterBKList(const Expr &sr, const Expr &dt, size_t univ_id, const Expr >erm)
bool hasMacros(const std::vector< Expr > &asserts)
if there are macros
Expr newRatExpr(const Rational &r)
ExprMap< std::vector< Expr > > d_mtrigs_bvorder
bool recMultMatchDebug(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
CDList< Expr > d_contextTerms
a list of all the terms appearing in the current context
bool getFlag() const
Check if the generic flag is set.
static Type anyType(ExprManager *em)
ExprManager * getEM()
Access to ExprManager.
ExprMap< size_t > d_totalThmCount
const std::vector< Expr > & getSubTerms(const Expr &e)
Expr simpRAWList(const Expr &org)
ExprStream & popdag(ExprStream &os)
bool transFound(const Expr &comb)
void mapTermsByType(const CDList< Expr > &terms)
categorizes all the terms contained in a vector of expressions by type.
CDMap< Expr, std::vector< Expr > > d_arrayIndic
Expr getHead(const Expr &e)
std::vector< multTrigsInfo > d_all_multTrigsInfo
ContextManager * getCM() const
Expr getRight(const Expr &e)
bool isGood(const Expr &e)
if e is a formula in the array property fragment
bool isSysPred(const Expr &e)
bool multMatchTop(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
void pushForwList(const Expr &node, Expr ex)
ExprMap< bool > d_is_macro_def
ExprMap< bool > d_hasTriggers
the score for a full trigger
CDList< Theorem > d_eqsUpdate
StatCounter d_abInstCount
bool isShield(const Expr &e)
if e satisfies the shiled property, that is all bound vars are parameters of uninterpreted functions/...
void setType(const Type &t) const
Set the cached type.
const int * d_maxQuantInst
Command line option.
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
void iterFWList(const Expr &sr, const Expr &dt, size_t univ_id, const Expr >erm)
bool goodMultiTriggers(const std::vector< Expr > &exprs, const std::vector< Expr > bVars)
bool isQuantifier() const
bool d_all_good
if all formulas checked so far are good
CDO< size_t > d_lastEqsUpdatePos
bool isDivide(const Expr &e)
Type boolType()
Return BOOLEAN type.
CDO< bool > d_maxILReached
the max instantiation level reached
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
void simplifyExprMap(ExprMap< Expr > &orgExprMap)
void delNewTrigs(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)
An exception to be thrown by the smtlib translator.
void findInstAssumptions(const Theorem &thm)
A recursive function used to find instantiated universals in the hierarchy of assumptions.
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
bool containsBoundVar() const
void setupTriggers(ExprMap< ExprMap< std::vector< dynTrig > * > * > &trig_maps, const Theorem &thm, size_t univs_id)
void addNotify(const Expr &e)
Expr getLeft(const Expr &e)
const Expr & getLHS() const
ExprMap< bool > d_savedCache
Expr newVarExpr(const std::string &s)
bool isGoodQuant(const Expr &e)
if e is a quant in the array property fragmenet
Expr getTCC(const Expr &e)
Compute the TCC of e, or the subtyping predicate, if e is a type.
Iterator for the Assumptions: points to class Theorem.
bool cmpExpr(Expr e1, Expr e2)
ExprMap< Expr > d_macro_lhs
CDList< Expr > d_usefulGterms
useful gterms for matching
bool recursiveMap(const Expr &term)
categorizes all the terms contained in an expressions by type.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
iterator find(const Key &k) const
Expr rewriteNot(const Expr &)
rewrite neg polarity forall / exists to pos polarity
bool isAtomicFormula() const
Test if e is an atomic formula.
QuantProofRules * createProofRules()
Destructor.
bool subExprOf(const Expr &e) const
Check if the current Expr (*this) is a subexpression of e.
virtual Theorem packVar(const Theorem &t1)=0
std::set< Expr > d_allIndex
Theorem reflexivityRule(const Expr &a)
==> a == a
void setTransFound(const Expr &comb)
Cardinality
Enum for cardinality of types.
bool trans2Found(const Expr &comb)
const bool * d_useNaiveInst
Expr plusOne(const Expr &e)
return e+1
ExprIndex getIndex() const
CDMap< Expr, bool > d_contextCache
bool isTransLike(const std::vector< Expr > &cur_trig)
Expr substExpr(const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const
void synNewInst(size_t univ_id, const std::vector< Expr > &binds, const Expr >erm, const Trigger &trig)
bool isPow(const Expr &e)
recCompleteInster(const Expr &, const std::vector< Expr > &, std::set< Expr > &, Expr)
const int * d_maxNaiveCall
bool isTrans2Like(const std::vector< Expr > &all_terms, const Expr &tr2)
Type getType() const
Get the type. Recursively compute if necessary.
ExprMap< Expr > d_macro_quant
InputLanguage lang() const
Get the current output language.
bool recMultMatch(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
ExprMap< std::vector< Expr > > d_subTermsMap
StatCounter d_allInstCount2
bool isMult(const Expr &e)
void setContainsBoundVar() const
std::string toString() const
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Expr andExpr(const std::vector< Expr > &children)
bool recMultMatchOldWay(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
CDO< size_t > d_lastTermsPos
tracks the possition of terms
ExprMap< CDMap< Expr, CDList< dynTrig > * > * > d_allmap_trigs
bool canGetHead(const Expr &e)
virtual Theorem normalizeQuant(const Expr &e)=0
std::queue< Theorem > d_gUnivQueue
static void recGetSubTerms(const Expr &e, std::vector< Expr > &res)
void instantiate(Theorem univ, bool all, bool savedMap, size_t newIndex)
Queues up all possible instantiations of bound variables.
for output into Simplify format
void arrayIndexName(const Expr &e)
CDO< size_t > d_lastPredsPos
tracks the possition of preds
ExprMap< int > d_thmCount
Nice SAL-like language for manually written specs.
void setFlag() const
Set the flag attribute.
ExprMap< multTrigsInfo > d_multitrigs_maps
ExprMap< std::vector< Trigger > > d_fullTrigs
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
ExprMap< std::vector< Expr > > d_multTriggers
bool usefulInMatch(const Expr &e)
const std::vector< Expr > & d_bvs
std::vector< Expr > d_buff
int recursiveExprScore(const Expr &e)
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
iterator end() const
End iterator.
bool isGoodSysPredTrigger(const Expr &e)