CVC3  2.4.1
quant_theorem_producer.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3 * \file quant_theorem_producer.cpp
4  *
5  * Author: Daniel Wichs, Yeting Ge
6  *
7  * Created: Jul 07 22:22:38 GMT 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  * CLASS: QuantProofRules
19  *
20  *
21  * Description: TRUSTED implementation of arithmetic proof rules.
22  *
23  */
24 /*****************************************************************************/
25 
26 // This code is trusted
27 #define _CVC3_TRUSTED_
28 
29 
30 #include "quant_theorem_producer.h"
31 #include "theory_quant.h"
32 #include "theory_core.h"
33 
34 
35 using namespace std;
36 using namespace CVC3;
37 
38 
39 QuantProofRules* TheoryQuant::createProofRules() {
40  return new QuantTheoremProducer(theoryCore()->getTM(), this);
41 }
42 
43 
44 #define CLASS_NAME "CVC3::QuantTheoremProducer"
45 
46 
47 //! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
48 Theorem
49 QuantTheoremProducer::rewriteNotForall(const Expr& e) {
50  if(CHECK_PROOFS) {
51  CHECK_SOUND(e.isNot() && e[0].isForall(),
52  "rewriteNotForall: expr must be NOT FORALL:\n"
53  +e.toString());
54  }
55  Proof pf;
56  if(withProof())
57  pf = newPf("rewrite_not_forall", e);
58  return newRWTheorem(e, e.getEM()->newClosureExpr(EXISTS, e[0].getVars(),
59  !e[0].getBody()),
60  Assumptions::emptyAssump(), pf);
61 }
62 
63 Theorem
64 QuantTheoremProducer::addNewConst(const Expr& e) {
65  Proof pf;
66  if(withProof())
67  pf = newPf("add_new_const", e);
68  return newTheorem(e, Assumptions::emptyAssump(), pf);
69 }
70 
71 ///do not use this rule, this is for debug only
72 Theorem
73 QuantTheoremProducer::newRWThm(const Expr& e, const Expr& newE) {
74  Proof pf;
75  if(withProof())
76  pf = newPf("from cache", e);
77  return newRWTheorem(e, newE,Assumptions::emptyAssump(), pf);
78 }
79 
80 
81 Theorem
82 QuantTheoremProducer::normalizeQuant(const Expr& quant) {
83  if(CHECK_PROOFS) {
84  CHECK_SOUND(quant.isForall()||quant.isExists(),
85  "normalizeQuant: expr must be FORALL or EXISTS\n"
86  +quant.toString());
87  }
88 
89 
90  std::map<Expr,int>::iterator typeIter;
91  std::string base("_BD");
92  int counter(0);
93 
94  vector<Expr> newVars;
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();
98  int typeIndex ;
99 
100  typeIter = d_typeFound.find(t.getExpr());
101 
102  if(d_typeFound.end() == typeIter){
103  typeIndex = d_typeFound.size();
104  d_typeFound[t.getExpr()] = typeIndex;
105  }
106  else{
107  typeIndex = typeIter->second;
108  }
109 
110  counter++;
111  std::stringstream stringType;
112  stringType << counter << "TY" << typeIndex ;
113  std::string out_str = base + stringType.str();
114  Expr newExpr = d_theoryQuant->getEM()->newBoundVarExpr(out_str, int2string(counter));
115  newExpr.setType(t);
116  newVars.push_back(newExpr);
117  }
118 
119  vector<vector<Expr> > trigs = quant.getTriggers();
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);
123  }
124  }
125 
126  Expr normBody = quant.getBody().substExpr(cur_vars,newVars);
127  Expr normQuant = d_theoryQuant->getEM()->newClosureExpr(quant.isForall()?FORALL:EXISTS, newVars, normBody, trigs);
128 
129  Proof pf;
130  if(withProof())
131  pf = newPf("normalizeQuant", quant, normQuant);
132 
133  return newRWTheorem(quant, normQuant, Assumptions::emptyAssump(), pf);
134 
135 }
136 
137 
138 //! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
139 Theorem QuantTheoremProducer::rewriteNotExists(const Expr& e) {
140  if(CHECK_PROOFS) {
141  CHECK_SOUND(e.isNot() && e[0].isExists(),
142  "rewriteNotExists: expr must be NOT FORALL:\n"
143  +e.toString());
144  }
145  Proof pf;
146  if(withProof())
147  pf = newPf("rewrite_not_exists", e);
148  return newRWTheorem(e, e.getEM()->newClosureExpr(FORALL, e[0].getVars(),
149  !e[0].getBody()),
150  Assumptions::emptyAssump(), pf);
151 }
152 
153 
154 Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const vector<Expr>& terms, int quantLevel, Expr gterm){
155  Expr e = t1.getExpr();
156  const vector<Expr>& boundVars = e.getVars();
157 
158  for(unsigned int i=0; i<terms.size(); i++){
159  if (d_theoryQuant->getBaseType(boundVars[i]) !=
160  d_theoryQuant->getBaseType(terms[i])){
161  Proof pf;
162  return newRWTheorem(terms[i],terms[i],
163  Assumptions::emptyAssump(), pf);
164  }
165  //this is the same as return a TRUE theorem, which will be ignored immeridatele. So, this is just return doing nothing.
166  }
167 
168 
169  if(CHECK_PROOFS) {
170  CHECK_SOUND(boundVars.size() == terms.size(),
171  "Universal instantiation: size of terms array does "
172  "not match quanitfied variables array size");
173  CHECK_SOUND(e.isForall(),
174  "universal instantiation: expr must be FORALL:\n"
175  +e.toString());
176 
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");
181  }
182 
183  //build up a conjunction of type predicates for expression
184  Expr tr = e.getEM()->trueExpr();
185  Expr typePred = tr;
186  // unsigned qlevel, qlevelMax = 0;
187  for(unsigned int i=0; i<terms.size(); i++) {
188  Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
189  if(p!=tr) {
190  if(typePred==tr)
191  typePred = p;
192  else
193  typePred = typePred.andExpr(p);
194  }
195  // qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]);
196  // if (qlevel > qlevelMax) qlevel = qlevelMax;
197  }
198 
199 
200  // Expr inst = e.getBody().substExprQuant(e.getVars(), terms);
201  Expr inst = e.getBody().substExpr(e.getVars(), terms);
202 
203  // Expr inst = e.getBody().substExpr(e.getVars(), terms);
204 
205 
206  Proof pf;
207  if(withProof()) {
208  vector<Proof> pfs;
209  vector<Expr> es;
210  pfs.push_back(t1.getProof());
211  es.push_back(e);
212  es.push_back(Expr(RAW_LIST,terms));
213  // es.insert(es.end(), terms.begin(), terms.end());
214  es.push_back(inst);
215  if (gterm.isNull()) {
216  es.push_back( d_theoryQuant->getEM()->newRatExpr(0));
217  }
218  else {es.push_back(gterm);
219  }
220  pf= newPf("universal_elimination1", es, pfs);
221  }
222 
223 
224  // Expr inst = e.getBody().substExpr(e.getVars(), terms);
225 
226 
227  Expr imp;
228  if(typePred == tr ) //just for a easy life, yeting, change this assp
229  imp = inst;
230  else
231  imp = typePred.impExpr(inst);
232  Theorem ret = newTheorem(imp, t1.getAssumptionsRef(), pf);
233 
234  int thmLevel = t1.getQuantLevel();
235  if(quantLevel >= thmLevel) {
236  ret.setQuantLevel(quantLevel+1);
237  }
238  else{
239  ret.setQuantLevel(thmLevel+1);
240  }
241 
242  // ret.setQuantLevel(quantLevel+1);
243  return ret;
244 }
245 
246 
247 //! Instantiate a universally quantified formula
248 /*! From T|-FORALL(var): e generate T|-psi => e' where e' is obtained
249  * from e by instantiating bound variables with terms in
250  * vector<Expr>& terms. The vector of terms should be the same
251  * size as the vector of bound variables in e. Also elements in
252  * each position i need to have matching base types. psi is the conjunction of
253  * subtype predicates for the bound variables of the quanitfied expression.
254  * \param t1 the quantifier (a Theorem)
255  * \param terms the terms to instantiate.
256  * \param quantLevel the quantification level for the formula
257  */
258 Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const vector<Expr>& terms, int quantLevel){
259 
260  Expr e = t1.getExpr();
261  const vector<Expr>& boundVars = e.getVars();
262  if(CHECK_PROOFS) {
263  CHECK_SOUND(boundVars.size() == terms.size(),
264  "Universal instantiation: size of terms array does "
265  "not match quanitfied variables array size");
266  CHECK_SOUND(e.isForall(),
267  "universal instantiation: expr must be FORALL:\n"
268  +e.toString());
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");
273  }
274 
275  //build up a conjunction of type predicates for expression
276  Expr tr = e.getEM()->trueExpr();
277  Expr typePred = tr;
278  // unsigned qlevel, qlevelMax = 0;
279  for(unsigned int i=0; i<terms.size(); i++) {
280  Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
281  if(p!=tr) {
282  if(typePred==tr)
283  typePred = p;
284  else
285  typePred = typePred.andExpr(p);
286  }
287  // qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]);
288  // if (qlevel > qlevelMax) qlevel = qlevelMax;
289  }
290 
291  //Expr inst = e.getBody().substExprQuant(e.getVars(), terms);
292  Expr inst = e.getBody().substExpr(e.getVars(), terms);
293 
294 
295  // Expr inst = e.getBody().substExpr(e.getVars(), terms);
296 
297 
298  Proof pf;
299  if(withProof()) {
300  vector<Proof> pfs;
301  vector<Expr> es;
302  pfs.push_back(t1.getProof());
303  es.push_back(e);
304  es.push_back(Expr(RAW_LIST,terms));
305  // es.insert(es.end(), terms.begin(), terms.end());
306  es.push_back(inst);
307  pf= newPf("universal_elimination2", es, pfs);
308  }
309 
310  // Expr inst = e.getBody().substExpr(e.getVars(), terms);
311 
312 
313  Expr imp;
314  if(typePred == tr) //just for a easy life, yeting, change this assp
315  imp = inst;
316  else
317  imp = typePred.impExpr(inst);
318  Theorem ret = newTheorem(imp, t1.getAssumptionsRef(), pf);
319 
320  int thmLevel = t1.getQuantLevel();
321  if(quantLevel >= thmLevel) {
322  ret.setQuantLevel(quantLevel+1);
323  }
324  else{
325  ret.setQuantLevel(thmLevel+1);
326  }
327 
328  // ret.setQuantLevel(quantLevel+1);
329  return ret;
330 }
331 
332 Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const vector<Expr>& terms){
333 
334  Expr e = t1.getExpr();
335  const vector<Expr>& boundVars = e.getVars();
336  if(CHECK_PROOFS) {
337  CHECK_SOUND(boundVars.size() == terms.size(),
338  "Universal instantiation: size of terms array does "
339  "not match quanitfied variables array size");
340  CHECK_SOUND(e.isForall(),
341  "universal instantiation: expr must be FORALL:\n"
342  +e.toString());
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");
347  }
348 
349  //build up a conjunction of type predicates for expression
350  Expr tr = e.getEM()->trueExpr();
351  Expr typePred = tr;
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]);
355  if(p!=tr) {
356  if(typePred==tr)
357  typePred = p;
358  else
359  typePred = typePred.andExpr(p);
360  }
361  qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]);
362  if (qlevel > qlevelMax) qlevel = qlevelMax;
363  }
364 
365  Expr inst = e.getBody().substExpr(e.getVars(), terms);
366  // Expr inst = e.getBody().substExprQuant(e.getVars(), terms);
367 
368 
369  // Expr inst = e.getBody().substExpr(e.getVars(), terms);
370 
371  Proof pf;
372  if(withProof()) {
373  vector<Proof> pfs;
374  vector<Expr> es;
375  pfs.push_back(t1.getProof());
376  es.push_back(e);
377  es.push_back(Expr(RAW_LIST,terms));
378  // es.insert(es.end(), terms.begin(), terms.end());
379  es.push_back(inst);
380  pf= newPf("universal_elimination3", es, pfs);
381  }
382 
383  // Expr inst = e.getBody().substExpr(e.getVars(), terms);
384 
385  Expr imp;
386  if( typePred == tr ) //just for easy life, yeting, change this asap
387  imp = inst;
388  else
389  imp = typePred.impExpr(inst);
390  Theorem ret = newTheorem(imp, t1.getAssumptionsRef(), pf);
391 
392 
393  unsigned thmLevel = t1.getQuantLevel();
394  if(qlevel >= thmLevel) {
395  ret.setQuantLevel(qlevel+1);
396  }
397  else{
398  // ret.setQuantLevel(thmLevel+1);
399  ret.setQuantLevel(thmLevel+1);
400  }
401 
402 
403  // ret.setQuantLevel(qlevel+1);
404  return ret;
405 }
406 
407 
408 Theorem QuantTheoremProducer::partialUniversalInst(const Theorem& t1, const vector<Expr>& terms, int quantLevel){
409  cout<<"error in partial inst" << endl;
410  Expr e = t1.getExpr();
411  const vector<Expr>& boundVars = e.getVars();
412  if(CHECK_PROOFS) {
413  CHECK_SOUND(boundVars.size() >= terms.size(),
414  "Universal instantiation: size of terms array does "
415  "not match quanitfied variables array size");
416  CHECK_SOUND(e.isForall(),
417  "universal instantiation: expr must be FORALL:\n"
418  +e.toString());
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");
423  }
424  }
425 
426  //build up a conjunction of type predicates for expression
427  Expr tr = e.getEM()->trueExpr();
428  Expr typePred = tr;
429  for(unsigned int i=0; i<terms.size(); i++) {
430  Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
431  if(p!=tr) {
432  if(typePred==tr)
433  typePred = p;
434  else
435  typePred = typePred.andExpr(p);
436  }
437  }
438  Proof pf;
439  if(withProof()) {
440  vector<Proof> pfs;
441  vector<Expr> es;
442  pfs.push_back(t1.getProof());
443  es.push_back(e);
444  es.insert(es.end(), terms.begin(), terms.end());
445  pf= newPf("partial_universal_instantiation", es, pfs);
446  }
447 
448 
449  if(terms.size() == boundVars.size()){
450  Expr inst = e.getBody().substExpr(e.getVars(), terms);
451  Expr imp;
452  if(typePred == tr)
453  imp = inst;
454  else
455  imp = typePred.impExpr(inst);
456  return(newTheorem(imp, t1.getAssumptionsRef(), pf));
457  }
458  else{
459  vector<Expr> newBoundVars;
460  for(size_t i=0; i<terms.size(); i++) {
461  newBoundVars.push_back(boundVars[i]);
462  }
463 
464  vector<Expr>leftBoundVars;
465  for(size_t i=terms.size(); i<boundVars.size(); i++) {
466  leftBoundVars.push_back(boundVars[i]);
467  }
468 
469  Expr tempinst = e.getBody().substExpr(newBoundVars, terms);
470  Expr inst = d_theoryQuant->getEM()->newClosureExpr(FORALL, leftBoundVars, tempinst);
471 
472  Expr imp;
473  if(typePred == tr)
474  imp = inst;
475  else
476  imp = typePred.impExpr(inst);
477 
478  Theorem res = (newTheorem(imp, t1.getAssumptionsRef(), pf));
479  int thmLevel = t1.getQuantLevel();
480  if(quantLevel >= thmLevel) {
481  res.setQuantLevel(quantLevel+1);
482  }
483  else{
484  //k ret.setQuantLevel(thmLevel+1);
485  res.setQuantLevel(thmLevel);
486  }
487  return res;
488 
489  }
490 }
491 
492 //! find all bound variables in e and maps them to true in boundVars
493 void QuantTheoremProducer::recFindBoundVars(const Expr& e,
494  ExprMap<bool> & boundVars, ExprMap<bool> &visited)
495 {
496  if(visited.count(e)>0)
497  return;
498  else
499  visited[e] = true;
500  if(e.getKind() == BOUND_VAR)
501  boundVars[e] = true;
502  if(e.getKind() == EXISTS || e.getKind() == FORALL)
503  recFindBoundVars(e.getBody(), boundVars, visited);
504  for(Expr::iterator it = e.begin(); it!=e.end(); ++it)
505  recFindBoundVars(*it, boundVars, visited);
506 
507 }
508 
509 //!adjust the order of bound vars, newBvs begin first
510 Theorem QuantTheoremProducer::adjustVarUniv(const Theorem& t1, const std::vector<Expr>& newBvs){
511  const Expr e=t1.getExpr();
512  const Expr body = e.getBody();
513  if(CHECK_PROOFS) {
514  CHECK_SOUND(e.isForall(),
515  "adjustVarUniv: "
516  +e.toString());
517  }
518 
519  const vector<Expr>& origVars = e.getVars();
520 
521 
522  ExprMap<bool> oldmap;
523  for(vector<Expr>::const_iterator it = origVars.begin(),
524  iend=origVars.end(); it!=iend; ++it) {
525  oldmap[*it]=true;
526  }
527 
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);
533  }
534 
535  if(quantVars.size() == origVars.size())
536  return t1;
537 
538  ExprMap<bool> newmap;
539  for(vector<Expr>::const_iterator it = newBvs.begin(),
540  iend=newBvs.end(); it!=iend; ++it) {
541  newmap[*it]=true;
542  }
543 
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);
548  };
549  }
550 
551  Proof pf;
552  if(withProof()) {
553  vector<Expr> es;
554  vector<Proof> pfs;
555  es.push_back(e);
556  es.insert(es.end(), quantVars.begin(), quantVars.end());
557  pfs.push_back(t1.getProof());
558  pf= newPf("adjustVarUniv", es, pfs);
559  }
560 
561  Expr newQuantExpr;
562  newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, quantVars, body);
563 
564  return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
565 }
566 
567 //!pack (forall (x) forall (y)) into (forall (x y))
568 Theorem QuantTheoremProducer::packVar(const Theorem& t1){
569  Expr out_forall =t1.getExpr();
570 
571  if(CHECK_PROOFS) {
572  CHECK_SOUND(out_forall.isForall(),
573  "packVar: "
574  +out_forall.toString());
575  }
576 
577  vector<Expr> bVars = out_forall.getVars();
578 
579  if(!out_forall.getBody().isForall()){
580  return t1;
581  }
582 
583  Expr cur_body = out_forall.getBody();
584 
585  while(cur_body.isForall()){
586  vector<Expr> bVarsLeft = cur_body.getVars();
587  for(vector<Expr>::iterator i=bVarsLeft.begin(), iend=bVarsLeft.end(); i!=iend; i++){
588  bVars.push_back(*i);
589  }
590  cur_body=cur_body.getBody();
591  }
592 
593  Proof pf;
594  if(withProof()) {
595  vector<Expr> es;
596  vector<Proof> pfs;
597  es.push_back(out_forall);
598  es.insert(es.end(), bVars.begin(), bVars.end());
599  pfs.push_back(t1.getProof());
600  pf= newPf("packVar", es, pfs);
601  }
602 
603  Expr newQuantExpr;
604  newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, bVars, cur_body);
605 
606  return (newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
607  // return (newRWTheorem(t1,newQuantExpr, t1.getAssumptionsRef(), pf));
608 }
609 
610 //! convert (forall (x) ... forall (y)) into (forall (x y)...)
611 //! convert (exists (x) ... exists (y)) into (exists (x y)...)
612 Theorem QuantTheoremProducer::pullVarOut(const Theorem& t1){
613  const Expr thm_expr=t1.getExpr();
614 
615  if(CHECK_PROOFS) {
616  CHECK_SOUND(thm_expr.isForall() || thm_expr.isExists(),
617  "pullVarOut: "
618  +thm_expr.toString());
619  }
620 
621  const Expr outBody = thm_expr.getBody();
622 
623 // if(((outBody.isAnd() && outBody[1].isForall()) ||
624 // (outBody.isImpl() && outBody[1].isForall()) ||
625 // (outBody.isNot() && outBody[0].isAnd() && outBody[0][1].isExists()) )){
626 // return t1;
627 // }
628 
629  if (thm_expr.isForall()){
630  if((outBody.isNot() && outBody[0].isAnd() && outBody[0][1].isExists())){
631 
632  vector<Expr> bVarsOut = thm_expr.getVars();
633 
634  const Expr innerExists =outBody[0][1];
635  const Expr innerBody = innerExists.getBody();
636  vector<Expr> bVarsIn = innerExists.getVars();
637 
638  for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
639  bVarsOut.push_back(*i);
640  }
641 
642  Proof pf;
643  if(withProof()) {
644  vector<Expr> es;
645  vector<Proof> pfs;
646  es.push_back(thm_expr);
647  es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
648  pfs.push_back(t1.getProof());
649  pf= newPf("pullVarOut", es, pfs);
650  }
651 
652  Expr newbody;
653 
654  newbody=(outBody[0][0].notExpr()).orExpr(innerBody.notExpr());
655 
656  Expr newQuantExpr;
657  newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, bVarsOut, newbody);
658 
659  return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
660  }
661 
662  else if ((outBody.isAnd() && outBody[1].isForall()) ||
663  (outBody.isImpl() && outBody[1].isForall())){
664 
665  vector<Expr> bVarsOut = thm_expr.getVars();
666 
667  const Expr innerForall=outBody[1];
668  const Expr innerBody = innerForall.getBody();
669  vector<Expr> bVarsIn = innerForall.getVars();
670 
671  for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
672  bVarsOut.push_back(*i);
673  }
674 
675  Proof pf;
676  if(withProof()) {
677  vector<Expr> es;
678  vector<Proof> pfs;
679  es.push_back(thm_expr);
680  es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
681  pfs.push_back(t1.getProof());
682  pf= newPf("pullVarOut", es, pfs);
683  }
684 
685  Expr newbody;
686  if(outBody.isAnd()){
687  newbody=outBody[0].andExpr(innerBody);
688  }
689  else if(outBody.isImpl()){
690  newbody=outBody[0].impExpr(innerBody);
691  }
692 
693  Expr newQuantExpr;
694  newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, bVarsOut, newbody);
695 
696  return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
697  }
698  return t1; // case cannot be handled now.
699  }
700 
701  else if (thm_expr.isExists()){
702  if ((outBody.isAnd() && outBody[1].isExists()) ||
703  (outBody.isImpl() && outBody[1].isExists())){
704 
705  vector<Expr> bVarsOut = thm_expr.getVars();
706 
707  const Expr innerExists = outBody[1];
708  const Expr innerBody = innerExists.getBody();
709  vector<Expr> bVarsIn = innerExists.getVars();
710 
711  for(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
712  bVarsOut.push_back(*i);
713  }
714 
715  Proof pf;
716  if(withProof()) {
717  vector<Expr> es;
718  vector<Proof> pfs;
719  es.push_back(thm_expr);
720  es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
721  pfs.push_back(t1.getProof());
722  pf= newPf("pullVarOut", es, pfs);
723  }
724 
725  Expr newbody;
726  if(outBody.isAnd()){
727  newbody=outBody[0].andExpr(innerBody);
728  }
729  else if(outBody.isImpl()){
730  newbody=outBody[0].impExpr(innerBody);
731  }
732 
733  Expr newQuantExpr;
734  newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(EXISTS, bVarsOut, newbody);
735 
736  return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
737  }
738  }
739  return t1;
740 }
741 
742 
743 
744 /*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e
745  * where vars' is obtained from vars by removing all bound variables
746  * not used in e. If vars' is empty the produced theorem is just T|-e
747  */
748 Theorem QuantTheoremProducer::boundVarElim(const Theorem& t1)
749 {
750  const Expr e=t1.getExpr();
751  const Expr body = e.getBody();
752  if(CHECK_PROOFS) {
753  CHECK_SOUND(e.isForall() || e.isExists(),
754  "bound var elimination: "
755  +e.toString());
756  }
757  ExprMap<bool> boundVars; //a mapping of bound variables in the body to true
758  ExprMap<bool> visited; //to make sure expressions aren't traversed
759  //multiple times
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)
765  {
766  if(boundVars.count(*it) > 0)
767  quantVars.push_back(*it);
768  }
769 
770  // If all variables are used, just return the original theorem
771  if(quantVars.size() == origVars.size())
772  return t1;
773 
774  Proof pf;
775  if(withProof()) {
776  vector<Expr> es;
777  vector<Proof> pfs;
778  es.push_back(e);
779  es.insert(es.end(), quantVars.begin(), quantVars.end());
780  pfs.push_back(t1.getProof());
781  pf= newPf("bound_variable_elimination", es, pfs);
782  }
783  if(quantVars.size() == 0)
784  return(newTheorem(e.getBody(), t1.getAssumptionsRef(), pf));
785 
786  Expr newQuantExpr;
787  if(e.isForall())
788  newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, quantVars, body);
789  else
790  newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(EXISTS, quantVars, body);
791 
792  return(newTheorem(newQuantExpr, t1.getAssumptionsRef(), pf));
793 }
bool isNull() const
Definition: expr.h:1223
iterator begin() const
Begin iterator.
Definition: expr.h:1211
Data structure of expressions in CVC3.
Definition: expr.h:133
ExprManager * getEM() const
Definition: expr.h:1156
bool isImpl() const
Definition: expr.h:425
Definition: kinds.h:84
MS C++ specific settings.
Definition: type.h:42
STL namespace.
Definition: kinds.h:85
#define CHECK_SOUND(cond, msg)
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
Definition: expr_manager.h:506
#define CHECK_PROOFS
const std::vector< std::vector< Expr > > & getTriggers() const
Get the manual triggers of the closure Expr.
Definition: expr.h:1116
Expr andExpr(const Expr &right) const
Definition: expr.h:941
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
Expr orExpr(const std::vector< Expr > &children)
Definition: expr.h:955
Expr impExpr(const Expr &right) const
Definition: expr.h:969
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Definition: expr_manager.h:484
const Expr & getExpr() const
Definition: type.h:52
bool isNot() const
Definition: expr.h:420
size_t count(const Expr &e) const
Definition: expr_map.h:173
bool isExists() const
Definition: expr.h:429
Definition: kinds.h:44
void setQuantLevel(unsigned level)
Set the quantification level for this theorem.
Definition: theorem.cpp:504
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
unsigned getQuantLevel() const
Return quantification level for this theorem.
Definition: theorem.cpp:491
int getKind() const
Definition: expr.h:1168
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
std::string int2string(int n)
Definition: cvc_util.h:46
const Expr & trueExpr()
TRUE Expr.
Definition: expr_manager.h:280
Proof getProof() const
Definition: theorem.cpp:402
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
Expr notExpr() const
Definition: expr.h:933
Expr getExpr() const
Definition: theorem.cpp:230
bool isForall() const
Definition: expr.h:428
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Definition: expr.h:1062
Expr substExpr(const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const
Definition: expr.cpp:178
Definition: expr.cpp:35
iterator end() const
End iterator.
Definition: expr.h:1217
bool isAnd() const
Definition: expr.h:421