ab94fbcc8309ee1246d170d53791b31f0f2072b7
1 /********************* */
2 /*! \file output_channel.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 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
&);
37 /** Disallow assignment: private operator=() */
38 OutputChannel
& operator=(const OutputChannel
&);
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) throw(Interrupted
, AssertionException
) = 0;
82 * Propagate a theory literal.
84 * @param n - a theory consequence at the current decision level.
86 * @param safe - whether it is safe to be interrupted
88 virtual void propagate(TNode n
, bool safe
= false) throw(Interrupted
, AssertionException
) = 0;
91 * Tell the core that a valid theory lemma at decision level 0 has
92 * been detected. (This request a split.)
94 * @param n - a theory lemma valid at decision level 0
95 * @param safe - whether it is safe to be interrupted
97 virtual void lemma(TNode n
, bool safe
= false) throw(Interrupted
, AssertionException
) = 0;
100 * Tell the core to add the following valid lemma as if it were a user assertion.
101 * This should NOT be called during solving, only preprocessing.
103 * @param n - a theory lemma valid to be asserted
104 * @param safe - whether it is safe to be interrupted
106 virtual void augmentingLemma(TNode n
, bool safe
= false) throw(Interrupted
, AssertionException
) = 0;
109 * Provide an explanation in response to an explanation request.
111 * @param n - an explanation
112 * @param safe - whether it is safe to be interrupted
114 virtual void explanation(TNode n
, bool safe
= false) throw(Interrupted
, AssertionException
) = 0;
116 };/* class OutputChannel */
118 }/* CVC4::theory namespace */
119 }/* CVC4 namespace */
121 #endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */