search_theorem_producer.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file search_theorem_producer.h
00004  * \brief Implementation API to proof rules for the simple search engine
00005  * 
00006  * Author: Sergey Berezin
00007  * 
00008  * Created: Mon Feb 24 14:48:03 2003
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__search__search_theorem_producer_h_
00023 #define _cvc3__search__search_theorem_producer_h_
00024 
00025 #include "theorem_producer.h"
00026 #include "search_rules.h"
00027 
00028 namespace CVC3 {
00029 
00030 class CommonProofRules;
00031 
00032   class SearchEngineTheoremProducer
00033     : public SearchEngineRules,
00034       public TheoremProducer {
00035   private:
00036     CommonProofRules* d_commonRules;
00037 
00038     void verifyConflict(const Theorem& thm, TheoremMap& m);
00039      
00040     void checkSoundNoSkolems(const Expr& e, ExprMap<bool>& visited, 
00041                              const ExprMap<bool>& skolems);
00042     void checkSoundNoSkolems(const Theorem& t, ExprMap<bool>& visited, 
00043                              const ExprMap<bool>& skolems);
00044   public:
00045     SearchEngineTheoremProducer(TheoremManager* tm);
00046     // Destructor
00047     virtual ~SearchEngineTheoremProducer() { }
00048     
00049     // Proof by contradiction: !A |- FALSE ==> |- A.  "!A" doesn't
00050     // have to be present in the assumptions.
00051     virtual Theorem proofByContradiction(const Expr& a,
00052            const Theorem& pfFalse);
00053     
00054     // Similar rule, only negation introduction:
00055     // A |- FALSE ==> !A
00056     virtual Theorem negIntro(const Expr& not_a, const Theorem& pfFalse);
00057     
00058     // Case split: u1:A |- C, u2:!A |- C  ==>  |- C
00059     virtual Theorem caseSplit(const Expr& a,
00060             const Theorem& a_proves_c,
00061             const Theorem& not_a_proves_c);
00062 
00063 
00064    
00065 
00066     
00067     /*! Eliminate skolem axioms: 
00068      * Gamma, Delta |- false => Gamma|- false 
00069      * where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)}
00070      * and gamma does not contain any of the skolem constants c.
00071      */
00072     virtual Theorem eliminateSkolemAxioms(const Theorem& tFalse, 
00073             const std::vector<Theorem>& delta);
00074  
00075 
00076     // Conflict clause rule: 
00077     // Gamma, A_1,...,A_n |- B ==> Gamma |- (OR B !A_1 ... !A_n)
00078     // The assumptions A_i are given by the vector 'lits'.
00079     // If B==FALSE, it is omitted from the result.
00080     
00081     // NOTE: here "!A_i" means an inverse of A_i, not just a negation.
00082     // That is, if A_i is NOT C, then !A_i is C.
00083 
00084     // NOTE: Theorems with same expressions must 
00085     // be eliminated before passing as lits.
00086     virtual Theorem conflictClause(const Theorem& thm,
00087            const std::vector<Theorem>& lits, 
00088            const std::vector<Theorem>& gamma);
00089 
00090     // "Cut" rule: { G_i |- A_i };  G', { A_i } |- B ==> union(G_i)+G' |- B.
00091     virtual Theorem cutRule(const std::vector<Theorem>& thmsA,
00092           const Theorem& as_prove_b);
00093 
00094     // "Unit propagation" rule:
00095     // G_j |- !l_j, j in [1..n]-{i}
00096     // G |- (OR l_1 ... l_i ... l_n) ==> G, G_j |- l_i
00097     virtual Theorem unitProp(const std::vector<Theorem>& thms,
00098            const Theorem& clause, unsigned i);
00099 
00100     // "Conflict" rule (all literals in a clause become FALSE)
00101     // { G_j |- !l_j, j in [1..n] } , G |- (OR l_1 ... l_n) ==> FALSE
00102     virtual Theorem conflictRule(const std::vector<Theorem>& thms,
00103          const Theorem& clause);
00104  
00105     // Unit propagation for AND
00106     virtual Theorem propAndrAF(const Theorem& andr_th,
00107              bool left,
00108              const Theorem& b_th);
00109 
00110     virtual Theorem propAndrAT(const Theorem& andr_th,
00111              const Theorem& l_th,
00112              const Theorem& r_th);
00113     
00114 
00115     virtual void propAndrLRT(const Theorem& andr_th,
00116            const Theorem& a_th,
00117            Theorem* l_th,
00118            Theorem* r_th);
00119 
00120     virtual Theorem propAndrLF(const Theorem& andr_th,
00121              const Theorem& a_th,
00122              const Theorem& r_th);
00123 
00124     virtual Theorem propAndrRF(const Theorem& andr_th,
00125              const Theorem& a_th,
00126              const Theorem& l_th);
00127 
00128     // Conflicts for AND
00129     virtual Theorem confAndrAT(const Theorem& andr_th,
00130              const Theorem& a_th,
00131              bool left,
00132              const Theorem& b_th);
00133 
00134     virtual Theorem confAndrAF(const Theorem& andr_th,
00135              const Theorem& a_th,
00136              const Theorem& l_th,
00137              const Theorem& r_th);
00138 
00139     // Unit propagation for IFF
00140     virtual Theorem propIffr(const Theorem& iffr_th,
00141            int p,
00142            const Theorem& a_th,
00143            const Theorem& b_th);
00144 
00145     // Conflicts for IFF
00146     virtual Theorem confIffr(const Theorem& iffr_th,
00147            const Theorem& i_th,
00148            const Theorem& l_th,
00149            const Theorem& r_th);
00150 
00151     // Unit propagation for ITE
00152     virtual Theorem propIterIte(const Theorem& iter_th,
00153         bool left,
00154         const Theorem& if_th,
00155         const Theorem& then_th);
00156 
00157     virtual void propIterIfThen(const Theorem& iter_th,
00158         bool left,
00159         const Theorem& ite_th,
00160         const Theorem& then_th,
00161         Theorem* if_th,
00162         Theorem* else_th);
00163 
00164     virtual Theorem propIterThen(const Theorem& iter_th,
00165          const Theorem& ite_th,
00166          const Theorem& if_th);
00167 
00168     // Conflicts for ITE
00169     virtual Theorem confIterThenElse(const Theorem& iter_th,
00170              const Theorem& ite_th,
00171              const Theorem& then_th,
00172              const Theorem& else_th);
00173 
00174     virtual Theorem confIterIfThen(const Theorem& iter_th,
00175            bool left,
00176            const Theorem& ite_th,
00177            const Theorem& if_th,
00178            const Theorem& then_th);
00179 
00180     // CNF Rules
00181     Theorem andCNFRule(const Theorem& thm);
00182     Theorem orCNFRule(const Theorem& thm);
00183     Theorem impCNFRule(const Theorem& thm);
00184     Theorem iffCNFRule(const Theorem& thm);
00185     Theorem iteCNFRule(const Theorem& thm);
00186     Theorem iteToClauses(const Theorem& ite);
00187     Theorem iffToClauses(const Theorem& iff);
00188 
00189     /////////////////////////////////////////////////////////////////////////
00190     //// helper functions for CNF (Conjunctive Normal Form) conversion
00191     /////////////////////////////////////////////////////////////////////////
00192     private:
00193     Theorem opCNFRule(const Theorem& thm, int kind,
00194           const std::string& ruleName);
00195     
00196     Expr convertToCNF(const Expr& v, const Expr & phi);      
00197 
00198     //! checks if phi has v in local cache of opCNFRule, if so reuse v.
00199     /*! similarly for ( ! ... ! (phi)) */
00200     Expr findInLocalCache(const Expr& i, 
00201         ExprMap<Expr>& localCache,
00202         std::vector<Expr>& boundVars);
00203 
00204   }; // end of class SearchEngineRules
00205 } // end of namespace CVC3
00206 #endif

Generated on Tue Jul 3 14:33:38 2007 for CVC3 by  doxygen 1.5.1