00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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 private:
00032
00033 void recFindBoundVars(const Expr& e,
00034 ExprMap<bool> & boundVars, ExprMap<bool> &visited);
00035 public:
00036
00037 QuantTheoremProducer(TheoremManager* tm, TheoryQuant* theoryQuant):
00038 TheoremProducer(tm), d_theoryQuant(theoryQuant) {}
00039
00040 virtual Theorem addNewConst(const Expr& e) ;
00041
00042
00043 virtual Theorem rewriteNotExists(const Expr& e);
00044
00045 virtual Theorem rewriteNotForall(const Expr& e);
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056 virtual Theorem universalInst(const Theorem& t1,
00057 const std::vector<Expr>& terms, int quantLevel);
00058
00059 virtual Theorem universalInst(const Theorem& t1,
00060 const std::vector<Expr>& terms);
00061
00062
00063 virtual Theorem partialUniversalInst(const Theorem& t1,
00064 const std::vector<Expr>& terms,
00065 int quantLevel) ;
00066
00067
00068
00069
00070
00071
00072 virtual Theorem boundVarElim(const Theorem& t1);
00073
00074 virtual Theorem adjustVarUniv(const Theorem& t1,
00075 const std::vector<Expr>& newBvs);
00076
00077 virtual Theorem packVar(const Theorem& t1);
00078
00079 virtual Theorem pullVarOut(const Theorem& t1);
00080
00081
00082 };
00083
00084 }
00085
00086 #endif