CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
sat
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
31
class
CNF_TheoremProducer
32
:
public
CNF_Rules
,
33
public
TheoremProducer
{
34
const
CLFlags
&
d_flags
;
35
const
bool
&
d_smartClauses
;
36
37
public
:
38
CNF_TheoremProducer
(
TheoremManager
* tm,
const
CLFlags
& flags)
39
:
TheoremProducer
(tm),
d_flags
(flags),
40
d_smartClauses
(flags[
"smart-clauses"
].getBool()) { }
41
~CNF_TheoremProducer
() { }
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
Generated on Tue May 14 2013 15:43:24 for CVC3 by
1.8.3.1