27 #define _CVC3_TRUSTED_
44 #define CLASS_NAME "CVC3::QuantTheoremProducer"
49 QuantTheoremProducer::rewriteNotForall(
const Expr& e) {
52 "rewriteNotForall: expr must be NOT FORALL:\n"
57 pf = newPf(
"rewrite_not_forall", e);
60 Assumptions::emptyAssump(), pf);
64 QuantTheoremProducer::addNewConst(
const Expr& e) {
67 pf = newPf(
"add_new_const", e);
68 return newTheorem(e, Assumptions::emptyAssump(), pf);
73 QuantTheoremProducer::newRWThm(
const Expr& e,
const Expr& newE) {
76 pf = newPf(
"from cache", e);
77 return newRWTheorem(e, newE,Assumptions::emptyAssump(), pf);
82 QuantTheoremProducer::normalizeQuant(
const Expr& quant) {
85 "normalizeQuant: expr must be FORALL or EXISTS\n"
90 std::map<Expr,int>::iterator typeIter;
91 std::string base(
"_BD");
95 const std::vector<Expr>& cur_vars = quant.
getVars();
96 for(
size_t j =0; j<cur_vars.size(); j++){
97 Type t = cur_vars[j].getType();
100 typeIter = d_typeFound.find(t.
getExpr());
102 if(d_typeFound.end() == typeIter){
103 typeIndex = d_typeFound.size();
104 d_typeFound[t.
getExpr()] = typeIndex;
107 typeIndex = typeIter->second;
111 std::stringstream stringType;
112 stringType << counter <<
"TY" << typeIndex ;
113 std::string out_str = base + stringType.str();
116 newVars.push_back(newExpr);
120 for(
size_t i = 0 ; i < trigs.size(); i++){
121 for(
size_t j = 0 ; j < trigs[i].size(); j++){
122 trigs[i][j] = trigs[i][j].substExpr(cur_vars,newVars);
131 pf = newPf(
"normalizeQuant", quant, normQuant);
133 return newRWTheorem(quant, normQuant, Assumptions::emptyAssump(), pf);
142 "rewriteNotExists: expr must be NOT FORALL:\n"
147 pf = newPf(
"rewrite_not_exists", e);
150 Assumptions::emptyAssump(), pf);
154 Theorem QuantTheoremProducer::universalInst(
const Theorem& t1,
const vector<Expr>& terms,
int quantLevel,
Expr gterm){
156 const vector<Expr>& boundVars = e.
getVars();
158 for(
unsigned int i=0; i<terms.size(); i++){
159 if (d_theoryQuant->getBaseType(boundVars[i]) !=
160 d_theoryQuant->getBaseType(terms[i])){
162 return newRWTheorem(terms[i],terms[i],
163 Assumptions::emptyAssump(), pf);
171 "Universal instantiation: size of terms array does "
172 "not match quanitfied variables array size");
174 "universal instantiation: expr must be FORALL:\n"
177 for(
unsigned int i=0; i<terms.size(); i++)
178 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) ==
179 d_theoryQuant->getBaseType(terms[i]),
180 "Universal instantiation: type mismatch");
187 for(
unsigned int i=0; i<terms.size(); i++) {
188 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
193 typePred = typePred.
andExpr(p);
216 es.push_back( d_theoryQuant->getEM()->newRatExpr(0));
218 else {es.push_back(gterm);
220 pf= newPf(
"universal_elimination1", es, pfs);
235 if(quantLevel >= thmLevel) {
258 Theorem QuantTheoremProducer::universalInst(
const Theorem& t1,
const vector<Expr>& terms,
int quantLevel){
261 const vector<Expr>& boundVars = e.
getVars();
264 "Universal instantiation: size of terms array does "
265 "not match quanitfied variables array size");
267 "universal instantiation: expr must be FORALL:\n"
269 for(
unsigned int i=0; i<terms.size(); i++)
270 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) ==
271 d_theoryQuant->getBaseType(terms[i]),
272 "Universal instantiation: type mismatch");
279 for(
unsigned int i=0; i<terms.size(); i++) {
280 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
285 typePred = typePred.
andExpr(p);
307 pf= newPf(
"universal_elimination2", es, pfs);
321 if(quantLevel >= thmLevel) {
332 Theorem QuantTheoremProducer::universalInst(
const Theorem& t1,
const vector<Expr>& terms){
335 const vector<Expr>& boundVars = e.
getVars();
338 "Universal instantiation: size of terms array does "
339 "not match quanitfied variables array size");
341 "universal instantiation: expr must be FORALL:\n"
343 for(
unsigned int i=0; i<terms.size(); i++)
344 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) ==
345 d_theoryQuant->getBaseType(terms[i]),
346 "Universal instantiation: type mismatch");
352 unsigned qlevel=0, qlevelMax = 0;
353 for(
unsigned int i=0; i<terms.size(); i++) {
354 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
359 typePred = typePred.
andExpr(p);
361 qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]);
362 if (qlevel > qlevelMax) qlevel = qlevelMax;
380 pf= newPf(
"universal_elimination3", es, pfs);
394 if(qlevel >= thmLevel) {
408 Theorem QuantTheoremProducer::partialUniversalInst(
const Theorem& t1,
const vector<Expr>& terms,
int quantLevel){
409 cout<<
"error in partial inst" <<
endl;
411 const vector<Expr>& boundVars = e.
getVars();
414 "Universal instantiation: size of terms array does "
415 "not match quanitfied variables array size");
417 "universal instantiation: expr must be FORALL:\n"
419 for(
unsigned int i=0; i<terms.size(); i++){
420 CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) ==
421 d_theoryQuant->getBaseType(terms[i]),
422 "partial Universal instantiation: type mismatch");
429 for(
unsigned int i=0; i<terms.size(); i++) {
430 Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
435 typePred = typePred.
andExpr(p);
444 es.insert(es.end(), terms.begin(), terms.end());
445 pf= newPf(
"partial_universal_instantiation", es, pfs);
449 if(terms.size() == boundVars.size()){
459 vector<Expr> newBoundVars;
460 for(
size_t i=0; i<terms.size(); i++) {
461 newBoundVars.push_back(boundVars[i]);
464 vector<Expr>leftBoundVars;
465 for(
size_t i=terms.size(); i<boundVars.size(); i++) {
466 leftBoundVars.push_back(boundVars[i]);
480 if(quantLevel >= thmLevel) {
493 void QuantTheoremProducer::recFindBoundVars(
const Expr& e,
496 if(visited.
count(e)>0)
503 recFindBoundVars(e.
getBody(), boundVars, visited);
505 recFindBoundVars(*it, boundVars, visited);
510 Theorem QuantTheoremProducer::adjustVarUniv(
const Theorem& t1,
const std::vector<Expr>& newBvs){
519 const vector<Expr>& origVars = e.
getVars();
523 for(vector<Expr>::const_iterator it = origVars.begin(),
524 iend=origVars.end(); it!=iend; ++it) {
528 vector<Expr> quantVars;
529 for(vector<Expr>::const_iterator it = newBvs.begin(),
530 iend=newBvs.end(); it!=iend; ++it) {
531 if(oldmap.
count(*it) > 0)
532 quantVars.push_back(*it);
535 if(quantVars.size() == origVars.size())
539 for(vector<Expr>::const_iterator it = newBvs.begin(),
540 iend=newBvs.end(); it!=iend; ++it) {
544 for(vector<Expr>::const_iterator it = origVars.begin(),
545 iend=origVars.end(); it!=iend; ++it) {
546 if(newmap.
count(*it)<=0){
547 quantVars.push_back(*it);
556 es.insert(es.end(), quantVars.begin(), quantVars.end());
558 pf= newPf(
"adjustVarUniv", es, pfs);
577 vector<Expr> bVars = out_forall.
getVars();
586 vector<Expr> bVarsLeft = cur_body.
getVars();
587 for(vector<Expr>::iterator i=bVarsLeft.begin(), iend=bVarsLeft.end(); i!=iend; i++){
597 es.push_back(out_forall);
598 es.insert(es.end(), bVars.begin(), bVars.end());
600 pf= newPf(
"packVar", es, pfs);
632 vector<Expr> bVarsOut = thm_expr.
getVars();
634 const Expr innerExists =outBody[0][1];
636 vector<Expr> bVarsIn = innerExists.
getVars();
638 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
639 bVarsOut.push_back(*i);
646 es.push_back(thm_expr);
647 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
649 pf= newPf(
"pullVarOut", es, pfs);
665 vector<Expr> bVarsOut = thm_expr.
getVars();
667 const Expr innerForall=outBody[1];
669 vector<Expr> bVarsIn = innerForall.
getVars();
671 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
672 bVarsOut.push_back(*i);
679 es.push_back(thm_expr);
680 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
682 pf= newPf(
"pullVarOut", es, pfs);
687 newbody=outBody[0].
andExpr(innerBody);
689 else if(outBody.
isImpl()){
690 newbody=outBody[0].
impExpr(innerBody);
705 vector<Expr> bVarsOut = thm_expr.
getVars();
707 const Expr innerExists = outBody[1];
709 vector<Expr> bVarsIn = innerExists.
getVars();
711 for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
712 bVarsOut.push_back(*i);
719 es.push_back(thm_expr);
720 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
722 pf= newPf(
"pullVarOut", es, pfs);
727 newbody=outBody[0].
andExpr(innerBody);
729 else if(outBody.
isImpl()){
730 newbody=outBody[0].
impExpr(innerBody);
754 "bound var elimination: "
760 recFindBoundVars(body, boundVars, visited);
761 vector<Expr> quantVars;
762 const vector<Expr>& origVars = e.
getVars();
763 for(vector<Expr>::const_iterator it = origVars.begin(),
764 iend=origVars.end(); it!=iend; ++it)
766 if(boundVars.
count(*it) > 0)
767 quantVars.push_back(*it);
771 if(quantVars.size() == origVars.size())
779 es.insert(es.end(), quantVars.begin(), quantVars.end());
781 pf= newPf(
"bound_variable_elimination", es, pfs);
783 if(quantVars.size() == 0)