CVC3  2.4.1
search_theorem_producer.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search_theorem_producer.h
4  * \brief Implementation API to proof rules for the simple search engine
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Mon Feb 24 14:48:03 2003
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__search__search_theorem_producer_h_
23 #define _cvc3__search__search_theorem_producer_h_
24 
25 #include "theorem_producer.h"
26 #include "search_rules.h"
27 
28 namespace CVC3 {
29 
30 class CommonProofRules;
31 
33  : public SearchEngineRules,
34  public TheoremProducer {
35  private:
37 
38  void verifyConflict(const Theorem& thm, TheoremMap& m);
39 
40  void checkSoundNoSkolems(const Expr& e, ExprMap<bool>& visited,
41  const ExprMap<bool>& skolems);
42  void checkSoundNoSkolems(const Theorem& t, ExprMap<bool>& visited,
43  const ExprMap<bool>& skolems);
44  public:
45 
47  // Destructor
49 
50  // Proof by contradiction: !A |- FALSE ==> |- A. "!A" doesn't
51  // have to be present in the assumptions.
52  virtual Theorem proofByContradiction(const Expr& a,
53  const Theorem& pfFalse);
54 
55  // Similar rule, only negation introduction:
56  // A |- FALSE ==> !A
57  virtual Theorem negIntro(const Expr& not_a, const Theorem& pfFalse);
58 
59  // Case split: u1:A |- C, u2:!A |- C ==> |- C
60  virtual Theorem caseSplit(const Expr& a,
61  const Theorem& a_proves_c,
62  const Theorem& not_a_proves_c);
63 
64 
65 
66 
67 
68  /*! Eliminate skolem axioms:
69  * Gamma, Delta |- false => Gamma|- false
70  * where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)}
71  * and gamma does not contain any of the skolem constants c.
72  */
73  virtual Theorem eliminateSkolemAxioms(const Theorem& tFalse,
74  const std::vector<Theorem>& delta);
75 
76 
77  // Conflict clause rule:
78  // Gamma, A_1,...,A_n |- B ==> Gamma |- (OR B !A_1 ... !A_n)
79  // The assumptions A_i are given by the vector 'lits'.
80  // If B==FALSE, it is omitted from the result.
81 
82  // NOTE: here "!A_i" means an inverse of A_i, not just a negation.
83  // That is, if A_i is NOT C, then !A_i is C.
84 
85  // NOTE: Theorems with same expressions must
86  // be eliminated before passing as lits.
87  virtual Theorem conflictClause(const Theorem& thm,
88  const std::vector<Theorem>& lits,
89  const std::vector<Theorem>& gamma);
90 
91  // "Cut" rule: { G_i |- A_i }; G', { A_i } |- B ==> union(G_i)+G' |- B.
92  virtual Theorem cutRule(const std::vector<Theorem>& thmsA,
93  const Theorem& as_prove_b);
94 
95  // "Unit propagation" rule:
96  // G_j |- !l_j, j in [1..n]-{i}
97  // G |- (OR l_1 ... l_i ... l_n) ==> G, G_j |- l_i
98  virtual Theorem unitProp(const std::vector<Theorem>& thms,
99  const Theorem& clause, unsigned i);
100 
101  // "Conflict" rule (all literals in a clause become FALSE)
102  // { G_j |- !l_j, j in [1..n] } , G |- (OR l_1 ... l_n) ==> FALSE
103  virtual Theorem conflictRule(const std::vector<Theorem>& thms,
104  const Theorem& clause);
105 
106  // Unit propagation for AND
107  virtual Theorem propAndrAF(const Theorem& andr_th,
108  bool left,
109  const Theorem& b_th);
110 
111  virtual Theorem propAndrAT(const Theorem& andr_th,
112  const Theorem& l_th,
113  const Theorem& r_th);
114 
115 
116  virtual void propAndrLRT(const Theorem& andr_th,
117  const Theorem& a_th,
118  Theorem* l_th,
119  Theorem* r_th);
120 
121  virtual Theorem propAndrLF(const Theorem& andr_th,
122  const Theorem& a_th,
123  const Theorem& r_th);
124 
125  virtual Theorem propAndrRF(const Theorem& andr_th,
126  const Theorem& a_th,
127  const Theorem& l_th);
128 
129  // Conflicts for AND
130  virtual Theorem confAndrAT(const Theorem& andr_th,
131  const Theorem& a_th,
132  bool left,
133  const Theorem& b_th);
134 
135  virtual Theorem confAndrAF(const Theorem& andr_th,
136  const Theorem& a_th,
137  const Theorem& l_th,
138  const Theorem& r_th);
139 
140  // Unit propagation for IFF
141  virtual Theorem propIffr(const Theorem& iffr_th,
142  int p,
143  const Theorem& a_th,
144  const Theorem& b_th);
145 
146  // Conflicts for IFF
147  virtual Theorem confIffr(const Theorem& iffr_th,
148  const Theorem& i_th,
149  const Theorem& l_th,
150  const Theorem& r_th);
151 
152  // Unit propagation for ITE
153  virtual Theorem propIterIte(const Theorem& iter_th,
154  bool left,
155  const Theorem& if_th,
156  const Theorem& then_th);
157 
158  virtual void propIterIfThen(const Theorem& iter_th,
159  bool left,
160  const Theorem& ite_th,
161  const Theorem& then_th,
162  Theorem* if_th,
163  Theorem* else_th);
164 
165  virtual Theorem propIterThen(const Theorem& iter_th,
166  const Theorem& ite_th,
167  const Theorem& if_th);
168 
169  // Conflicts for ITE
170  virtual Theorem confIterThenElse(const Theorem& iter_th,
171  const Theorem& ite_th,
172  const Theorem& then_th,
173  const Theorem& else_th);
174 
175  virtual Theorem confIterIfThen(const Theorem& iter_th,
176  bool left,
177  const Theorem& ite_th,
178  const Theorem& if_th,
179  const Theorem& then_th);
180 
181  // CNF Rules
182  Theorem andCNFRule(const Theorem& thm);
183  Theorem orCNFRule(const Theorem& thm);
184  Theorem impCNFRule(const Theorem& thm);
185  Theorem iffCNFRule(const Theorem& thm);
186  Theorem iteCNFRule(const Theorem& thm);
187  Theorem iteToClauses(const Theorem& ite);
188  Theorem iffToClauses(const Theorem& iff);
189 
190  //theorrm for minisat proofs, by yeting
191  Theorem satProof(const Expr& queryExpr, const Proof& satProof);
192 
193  /////////////////////////////////////////////////////////////////////////
194  //// helper functions for CNF (Conjunctive Normal Form) conversion
195  /////////////////////////////////////////////////////////////////////////
196  private:
197  Theorem opCNFRule(const Theorem& thm, int kind,
198  const std::string& ruleName);
199 
200  Expr convertToCNF(const Expr& v, const Expr & phi);
201 
202  //! checks if phi has v in local cache of opCNFRule, if so reuse v.
203  /*! similarly for ( ! ... ! (phi)) */
204  Expr findInLocalCache(const Expr& i,
205  ExprMap<Expr>& localCache,
206  std::vector<Expr>& boundVars);
207 
208  }; // end of class SearchEngineRules
209 } // end of namespace CVC3
210 #endif
virtual void propAndrLRT(const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)
void verifyConflict(const Theorem &thm, TheoremMap &m)
virtual Theorem proofByContradiction(const Expr &a, const Theorem &pfFalse)
Proof by contradiction: .
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Theorem confIterThenElse(const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)
std::map< Theorem, bool, TheoremLess > TheoremMap
Definition: theorem.h:402
virtual Theorem eliminateSkolemAxioms(const Theorem &tFalse, const std::vector< Theorem > &delta)
Expr findInLocalCache(const Expr &i, ExprMap< Expr > &localCache, std::vector< Expr > &boundVars)
checks if phi has v in local cache of opCNFRule, if so reuse v.
Theorem iffToClauses(const Theorem &iff)
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
virtual Theorem propAndrLF(const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)
virtual Theorem cutRule(const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)
Cut rule: .
virtual Theorem propIffr(const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)
virtual Theorem propIterIte(const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)
virtual Theorem caseSplit(const Expr &a, const Theorem &a_proves_c, const Theorem &not_a_proves_c)
Case split: .
Theorem impCNFRule(const Theorem &thm)
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
virtual void propIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)
Abstract proof rules interface to the simple search engine.
virtual Theorem unitProp(const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)
Unit propagation rule: .
static int left(int i)
Definition: minisat_heap.h:53
Theorem orCNFRule(const Theorem &thm)
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
virtual Theorem conflictRule(const std::vector< Theorem > &thms, const Theorem &clause)
"Conflict" rule (all literals in a clause become FALSE)
virtual Theorem confIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)
Theorem opCNFRule(const Theorem &thm, int kind, const std::string &ruleName)
Theorem iteToClauses(const Theorem &ite)
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
virtual Theorem confAndrAF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)
virtual Theorem conflictClause(const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)
Conflict clause rule: .
virtual Theorem propAndrRF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)
Theorem iteCNFRule(const Theorem &thm)
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
virtual Theorem confIffr(const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)
API to the proof rules for the Search Engines.
Definition: search_rules.h:35
virtual Theorem propIterThen(const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)
Definition: expr.cpp:35
Theorem iffCNFRule(const Theorem &thm)
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
Theorem satProof(const Expr &queryExpr, const Proof &satProof)
virtual Theorem propAndrAT(const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)
virtual Theorem negIntro(const Expr &not_a, const Theorem &pfFalse)
Negation introduction: .
virtual Theorem propAndrAF(const Theorem &andr_th, bool left, const Theorem &b_th)
Expr convertToCNF(const Expr &v, const Expr &phi)
produces the CNF for the formula v <==> phi
void checkSoundNoSkolems(const Expr &e, ExprMap< bool > &visited, const ExprMap< bool > &skolems)
Theorem andCNFRule(const Theorem &thm)
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
virtual Theorem confAndrAT(const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)