f492041b8a2db9e121b99df02594eb0dbcd32bbb
1 /********************* */
2 /*! \file theory_bool.h
4 ** Original author: mdeters
5 ** Major contributors: taking
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief The theory of booleans.
16 ** The theory of booleans.
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
22 #define __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
24 #include "theory/theory.h"
25 #include "context/context.h"
31 class TheoryBool
: public Theory
{
33 TheoryBool(int id
, context::Context
* c
, OutputChannel
& out
) :
37 void preRegisterTerm(TNode n
) {
38 Debug("bool") << "bool: begin preRegisterTerm(" << n
<< ")" << std::endl
;
39 Debug("bool") << "bool: end preRegisterTerm(" << n
<< ")" << std::endl
;
41 void registerTerm(TNode n
) {
42 Debug("bool") << "bool: begin preRegisterTerm(" << n
<< ")" << std::endl
;
43 Debug("bool") << "bool: end preRegisterTerm(" << n
<< ")" << std::endl
;
45 void check(Effort e
) { Unimplemented(); }
46 void propagate(Effort e
) { Unimplemented(); }
47 void explain(TNode n
, Effort e
) { Unimplemented(); }
49 RewriteResponse
preRewrite(TNode n
, bool topLevel
);
50 RewriteResponse
postRewrite(TNode n
, bool topLevel
);
52 std::string
identify() const { return std::string("TheoryBool"); }
55 }/* CVC4::theory::booleans namespace */
56 }/* CVC4::theory namespace */
59 #endif /* __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H */