CVC3 2.2
|
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 //theorrm for minisat proofs, by yeting 00190 Theorem satProof(const Expr& queryExpr, const Proof& satProof); 00191 00192 ///////////////////////////////////////////////////////////////////////// 00193 //// helper functions for CNF (Conjunctive Normal Form) conversion 00194 ///////////////////////////////////////////////////////////////////////// 00195 private: 00196 Theorem opCNFRule(const Theorem& thm, int kind, 00197 const std::string& ruleName); 00198 00199 Expr convertToCNF(const Expr& v, const Expr & phi); 00200 00201 //! checks if phi has v in local cache of opCNFRule, if so reuse v. 00202 /*! similarly for ( ! ... ! (phi)) */ 00203 Expr findInLocalCache(const Expr& i, 00204 ExprMap<Expr>& localCache, 00205 std::vector<Expr>& boundVars); 00206 00207 }; // end of class SearchEngineRules 00208 } // end of namespace CVC3 00209 #endif