CVC3  2.4.1
quant_theorem_producer.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file quant_theorem_producer.h
4  *
5  * Author: Daniel Wichs
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  */
19 /*****************************************************************************/
20 #ifndef _cvc3__quant_theorem_producer_h_
21 #define _cvc3__quant_theorem_producer_h_
22 
23 #include "quant_proof_rules.h"
24 #include "theorem_producer.h"
25 #include "theory_quant.h"
26 
27 namespace CVC3 {
28 
31  std::map<Expr,int> d_typeFound;
32  private:
33 
34  //! find all bound variables in e and maps them to true in boundVars
35  void recFindBoundVars(const Expr& e,
36  ExprMap<bool> & boundVars, ExprMap<bool> &visited);
37  public:
38  //! Constructor
40  TheoremProducer(tm), d_theoryQuant(theoryQuant) { d_typeFound.clear(); }
41 
42  virtual Theorem addNewConst(const Expr& e) ;
43  virtual Theorem newRWThm(const Expr& e, const Expr& newE) ;
44  virtual Theorem normalizeQuant(const Expr& e) ;
45 
46  //! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
47  virtual Theorem rewriteNotExists(const Expr& e);
48  //! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
49  virtual Theorem rewriteNotForall(const Expr& e);
50  //! Instantiate a universally quantified formula
51  /*! From T|-FORALL(var): e generate T|-e' where e' is obtained
52  * from e by instantiating bound variables with terms in
53  * vector<Expr>& terms. The vector of terms should be the same
54  * size as the vector of bound variables in e. Also elements in
55  * each position i need to have matching types.
56  * \param t1 is the quantifier (a Theorem)
57  * \param terms are the terms to instantiate.
58  * \param quantLevel the quantification level for the theorem.
59 
60  */
61 
62  virtual Theorem universalInst(const Theorem& t1,
63  const std::vector<Expr>& terms, int quantLevel ,
64  Expr gterm);
65 
66  virtual Theorem universalInst(const Theorem& t1,
67  const std::vector<Expr>& terms, int quantLevel);
68 
69  virtual Theorem universalInst(const Theorem& t1,
70  const std::vector<Expr>& terms);
71 
72 
73  virtual Theorem partialUniversalInst(const Theorem& t1,
74  const std::vector<Expr>& terms,
75  int quantLevel) ;
76 
77 
78  /*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e
79  * where vars' is obtained from vars by removing all bound variables
80  * not used in e. If vars' is empty the produced theorem is just T|-e
81  */
82  virtual Theorem boundVarElim(const Theorem& t1);
83 
84  virtual Theorem adjustVarUniv(const Theorem& t1,
85  const std::vector<Expr>& newBvs);
86 
87  virtual Theorem packVar(const Theorem& t1);
88 
89  virtual Theorem pullVarOut(const Theorem& t1);
90 
91 
92  };
93 
94 }
95 
96 #endif