CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
sat
cnf_rules.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file cnf_rules.h
4
* \brief Abstract proof rules for CNF conversion
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Thu Jan 5 05:24:45 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_rules_h_
23
#define _cvc3__sat__cnf_rules_h_
24
25
namespace
CVC3 {
26
27
class
Theorem;
28
29
/*! \defgroup CNF_Rules Proof Rules for the Search Engines
30
* \ingroup CNF
31
*/
32
//! API to the CNF proof rules
33
/*! \ingroup CNF_Rules */
34
class
CNF_Rules
{
35
/*! \addtogroup CNF_Rules
36
* @{
37
*/
38
public
:
39
//! Destructor
40
virtual
~CNF_Rules
() { }
41
42
// A_1,...,A_n |- B ==> |- (OR !A_1 ... !A_n B)
43
/*! @brief Learned clause rule:
44
\f[\frac{A_1,\ldots,A_n\vdash B}
45
{\vdash\neg A_1\vee\cdots\vee \neg A_n\vee B}\f]
46
*
47
* \param thm is the theorem
48
* \f$ A_1,\ldots,A_n\vdash B\f$
49
* Each \f$A_i\f$ and \f$B\f$ should be literals
50
* \f$B\f$ can also be \f$\mathrm{FALSE}\f$
51
*/
52
virtual
void
learnedClauses
(
const
Theorem
& thm,
53
std::vector<Theorem>&,
54
bool
newLemma) = 0;
55
56
//! |- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
57
virtual
Theorem
ifLiftRule
(
const
Expr
& e,
int
itePos) = 0;
58
virtual
Theorem
CNFAddUnit
(
const
Theorem
& thm) = 0 ;
59
virtual
Theorem
CNFConvert
(
const
Expr
& e,
const
Theorem
& thm) = 0 ;
60
virtual
Theorem
CNFtranslate
(
const
Expr
& before,
61
const
Expr
& after,
62
std::string reason,
63
int
pos,
64
const
std::vector<Theorem>& thms) = 0;
65
66
virtual
Theorem
CNFITEtranslate
(
const
Expr
& before,
67
const
std::vector<Expr>& after,
68
const
std::vector<Theorem>& thms,
69
int
pos) = 0;
70
71
/*! @} */
// end of CNF_Rules
72
};
// end of class CNF_Rules
73
74
}
// end of namespace CVC3
75
76
#endif
Generated on Sat Aug 3 2013 07:58:23 for CVC3 by
1.8.4