1 /********************* */
2 /*! \file output_channel.h
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): taking, barrett
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 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 output channel interface
16 ** The theory output channel interface.
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
22 #define __CVC4__THEORY__OUTPUT_CHANNEL_H
24 #include "util/Assert.h"
25 #include "theory/interrupted.h"
31 * Generic "theory output channel" interface.
34 /** Disallow copying: private constructor */
35 OutputChannel(const OutputChannel
&) CVC4_UNDEFINED
;
37 /** Disallow assignment: private operator=() */
38 OutputChannel
& operator=(const OutputChannel
&) CVC4_UNDEFINED
;
43 * Construct an OutputChannel.
49 * Destructs an OutputChannel. This implementation does nothing,
50 * but we need a virtual destructor for safety in case subclasses
53 virtual ~OutputChannel() {
57 * With safePoint(), the theory signals that it is at a safe point
58 * and can be interrupted.
60 virtual void safePoint() throw(Interrupted
, AssertionException
) {
64 * Indicate a theory conflict has arisen.
66 * @param n - a conflict at the current decision level. This should
67 * be an AND-kinded node of literals that are TRUE in the current
68 * assignment and are in conflict (i.e., at least one must be
69 * assigned false), or else a literal by itself (in the case of a
70 * unit conflict) which is assigned TRUE (and T-conflicting) in the
73 virtual void conflict(TNode n
) throw(AssertionException
) = 0;
76 * Propagate a theory literal.
78 * @param n - a theory consequence at the current decision level
80 virtual void propagate(TNode n
) throw(AssertionException
) = 0;
83 * Tell the core that a valid theory lemma at decision level 0 has
84 * been detected. (This requests a split.)
86 * @param n - a theory lemma valid at decision level 0
87 * @param removable - whether the lemma can be removed at any point
89 virtual void lemma(TNode n
, bool removable
= false) throw(TypeCheckingExceptionPrivate
, AssertionException
) = 0;
92 * Request a split on a new theory atom. This is equivalent to
93 * calling lemma({OR n (NOT n)}).
95 * @param n - a theory atom; must be of Boolean type
97 void split(TNode n
) throw(TypeCheckingExceptionPrivate
, AssertionException
) {
98 lemma(n
.orNode(n
.notNode()));
102 * Notification from a theory that it realizes it is incomplete at
103 * this context level. If SAT is later determined by the
104 * TheoryEngine, it should actually return an UNKNOWN result.
106 virtual void setIncomplete() throw(AssertionException
) = 0;
108 };/* class OutputChannel */
110 }/* CVC4::theory namespace */
111 }/* CVC4 namespace */
113 #endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */