1 /********************* */
3 ** Original author: mdeters
4 ** Major contributors: none
5 ** Minor contributors (to current version): none
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
8 ** Courant Institute of Mathematical Sciences
10 ** See the file COPYING in the top-level source directory for licensing
13 ** The theory output channel interface.
16 #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
17 #define __CVC4__THEORY__OUTPUT_CHANNEL_H
19 #include "theory/interrupted.h"
25 * Generic "theory output channel" interface.
28 /** Disallow copying: private constructor */
29 OutputChannel(const OutputChannel
&);
31 /** Disallow assignment: private operator=() */
32 OutputChannel
& operator=(const OutputChannel
&);
37 * Construct an OutputChannel.
43 * Destructs an OutputChannel. This implementation does nothing,
44 * but we need a virtual destructor for safety in case subclasses
47 virtual ~OutputChannel() {
51 * With safePoint(), the theory signals that it is at a safe point
52 * and can be interrupted.
54 virtual void safePoint() throw(Interrupted
) {
58 * Indicate a theory conflict has arisen.
60 * @param n - a conflict at the current decision level. This should
61 * be an AND-kinded node of literals that are TRUE in the current
62 * assignment and are in conflict (i.e., at least one must be
65 * @param safe - whether it is safe to be interrupted
67 virtual void conflict(TNode n
, bool safe
= false) throw(Interrupted
) = 0;
70 * Propagate a theory literal.
72 * @param n - a theory consequence at the current decision level.
74 * @param safe - whether it is safe to be interrupted
76 virtual void propagate(TNode n
, bool safe
= false) throw(Interrupted
) = 0;
79 * Tell the core that a valid theory lemma at decision level 0 has
80 * been detected. (This request a split.)
82 * @param n - a theory lemma valid at decision level 0
83 * @param safe - whether it is safe to be interrupted
85 virtual void lemma(TNode n
, bool safe
= false) throw(Interrupted
) = 0;
88 * Provide an explanation in response to an explanation request.
90 * @param n - an explanation
91 * @param safe - whether it is safe to be interrupted
93 virtual void explanation(TNode n
, bool safe
= false) throw(Interrupted
) = 0;
95 };/* class OutputChannel */
97 }/* CVC4::theory namespace */
100 #endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */