quant_theorem_producer.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file quant_theorem_producer.h
00004  * 
00005  * Author: Daniel Wichs
00006  * 
00007  * Created: Jul 07 22:22:38 GMT 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 #ifndef _cvc3__quant_theorem_producer_h_
00021 #define _cvc3__quant_theorem_producer_h_
00022 
00023 #include "quant_proof_rules.h"
00024 #include "theorem_producer.h"
00025 #include "theory_quant.h"
00026 
00027 namespace CVC3 {
00028   
00029   class QuantTheoremProducer: public QuantProofRules, public TheoremProducer {
00030     TheoryQuant* d_theoryQuant;
00031     std::map<Expr,int> d_typeFound;
00032   private:
00033 
00034     //! find all bound variables in e and maps them to true in boundVars
00035     void recFindBoundVars(const Expr& e, 
00036         ExprMap<bool> & boundVars, ExprMap<bool> &visited);
00037   public:
00038     //! Constructor
00039     QuantTheoremProducer(TheoremManager* tm, TheoryQuant* theoryQuant):
00040       TheoremProducer(tm), d_theoryQuant(theoryQuant) { d_typeFound.clear(); }
00041 
00042     virtual Theorem addNewConst(const Expr& e) ;
00043     virtual Theorem newRWThm(const Expr& e, const Expr& newE) ;
00044     virtual Theorem normalizeQuant(const Expr& e) ;
00045 
00046     //! ==> NOT EXISTS (vars): e  IFF FORALL (vars) NOT e
00047     virtual Theorem rewriteNotExists(const Expr& e);
00048     //! ==> NOT FORALL (vars): e  IFF EXISTS (vars) NOT e 
00049     virtual Theorem rewriteNotForall(const Expr& e);
00050     //! Instantiate a  universally quantified formula
00051     /*! From T|-FORALL(var): e generate T|-e' where e' is obtained
00052      * from e by instantiating bound variables with terms in
00053      * vector<Expr>& terms.  The vector of terms should be the same
00054      * size as the vector of bound variables in e. Also elements in
00055      * each position i need to have matching types.
00056      * \param t1 is the quantifier (a Theorem)
00057      * \param terms are the terms to instantiate.
00058      * \param quantLevel the quantification level for the theorem.
00059 
00060      */
00061 
00062     virtual Theorem universalInst(const Theorem& t1, 
00063           const std::vector<Expr>& terms, int quantLevel ,
00064           Expr gterm);
00065 
00066     virtual Theorem universalInst(const Theorem& t1,
00067           const std::vector<Expr>& terms, int quantLevel);
00068 
00069     virtual Theorem universalInst(const Theorem& t1,
00070           const std::vector<Expr>& terms);
00071 
00072 
00073     virtual Theorem partialUniversalInst(const Theorem& t1,
00074            const std::vector<Expr>& terms,
00075            int quantLevel) ;
00076 
00077     
00078     /*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e
00079      * where vars' is obtained from vars by removing all bound variables
00080      *  not used in e. If vars' is empty the produced theorem is just T|-e
00081      */
00082     virtual Theorem boundVarElim(const Theorem& t1);
00083 
00084     virtual Theorem adjustVarUniv(const Theorem& t1, 
00085           const std::vector<Expr>& newBvs);
00086 
00087     virtual Theorem packVar(const Theorem& t1);
00088 
00089     virtual Theorem pullVarOut(const Theorem& t1);
00090 
00091 
00092   }; 
00093 
00094 } 
00095 
00096 #endif

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2