CVC3  2.4.1
cnf_theorem_producer.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file cnf_theorem_producer.h
4  *\brief Implementation of CNF_Rules API
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Thu Jan 5 05:33:42 2006
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__sat__cnf_theorem_producer_h_
23 #define _cvc3__sat__cnf_theorem_producer_h_
24 
25 #include "theorem_producer.h"
26 #include "cnf_rules.h"
27 #include "command_line_flags.h"
28 
29 namespace CVC3 {
30 
32  : public CNF_Rules,
33  public TheoremProducer {
34  const CLFlags& d_flags;
35  const bool& d_smartClauses;
36 
37  public:
39  : TheoremProducer(tm), d_flags(flags),
40  d_smartClauses(flags["smart-clauses"].getBool()) { }
42 
43  void getSmartClauses(const Theorem& thm, std::vector<Theorem>& clauses);
44 
45  void learnedClauses(const Theorem& thm, std::vector<Theorem>& clauses,
46  bool newLemma);
47  Theorem CNFAddUnit(const Theorem& thm);
48  Theorem CNFConvert(const Expr & e, const Theorem& thm);
49  Theorem ifLiftRule(const Expr& e, int itePos);
50  Theorem CNFtranslate(const Expr& before,
51  const Expr& after,
52  std::string reason,
53  int pos,
54  const std::vector<Theorem>& thms) ;
55  Theorem CNFITEtranslate(const Expr& before,
56  const std::vector<Expr>& after,
57  const std::vector<Theorem>& thms,
58  int pos) ;
59 
60 
61  }; // end of class CNF_TheoremProducer
62 } // end of namespace CVC3
63 #endif