1 /********************* */
2 /*! \file output_channel.h
4 ** Original author: mdeters
5 ** Major contributors: taking
6 ** Minor contributors (to current version): barrett
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 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 * Notify the OutputChannel that a new fact has been received by
60 virtual void newFact(TNode n
) { }
63 * With safePoint(), the theory signals that it is at a safe point
64 * and can be interrupted.
66 virtual void safePoint() throw(Interrupted
, AssertionException
) {
70 * Indicate a theory conflict has arisen.
72 * @param n - a conflict at the current decision level. This should
73 * be an AND-kinded node of literals that are TRUE in the current
74 * assignment and are in conflict (i.e., at least one must be
77 * @param safe - whether it is safe to be interrupted
79 virtual void conflict(TNode n
, bool safe
= false)
80 throw(Interrupted
, AssertionException
) = 0;
83 * Propagate a theory literal.
85 * @param n - a theory consequence at the current decision level.
87 * @param safe - whether it is safe to be interrupted
89 virtual void propagate(TNode n
, bool safe
= false)
90 throw(Interrupted
, AssertionException
) = 0;
93 * Tell the core that a valid theory lemma at decision level 0 has
94 * been detected. (This request a split.)
96 * @param n - a theory lemma valid at decision level 0
97 * @param safe - whether it is safe to be interrupted
99 virtual void lemma(TNode n
, bool safe
= false)
100 throw(Interrupted
, AssertionException
) = 0;
103 * Provide an explanation in response to an explanation request.
105 * @param n - an explanation
106 * @param safe - whether it is safe to be interrupted
108 virtual void explanation(TNode n
, bool safe
= false)
109 throw(Interrupted
, AssertionException
) = 0;
112 * Notification from a theory that it realizes it is incomplete at
113 * this context level. If SAT is later determined by the
114 * TheoryEngine, it should actually return an UNKNOWN result.
116 virtual void setIncomplete()
117 throw(Interrupted
, AssertionException
) = 0;
119 };/* class OutputChannel */
121 }/* CVC4::theory namespace */
122 }/* CVC4 namespace */
124 #endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */