1cce09439eb23cf9f9015e8c1027b104a27a3e66
1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): dejan, taking
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 Base of the theory interface.
16 ** Base of the theory interface.
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY__THEORY_H
22 #define __CVC4__THEORY__THEORY_H
24 #include "expr/node.h"
25 #include "expr/attribute.h"
26 #include "theory/output_channel.h"
27 #include "context/context.h"
41 // rewrite cache support
42 template <bool topLevel
> struct PreRewriteCacheTag
{};
43 typedef expr::Attribute
<PreRewriteCacheTag
<true>, Node
> PreRewriteCacheTop
;
44 typedef expr::Attribute
<PreRewriteCacheTag
<false>, Node
> PreRewriteCache
;
45 template <bool topLevel
> struct PostRewriteCacheTag
{};
46 typedef expr::Attribute
<PostRewriteCacheTag
<true>, Node
> PostRewriteCacheTop
;
47 typedef expr::Attribute
<PostRewriteCacheTag
<false>, Node
> PostRewriteCache
;
50 * Instances of this class serve as response codes from
51 * Theory::preRewrite() and Theory::postRewrite(). Instances of
52 * derived classes RewriteComplete(n), RewriteAgain(n), and
53 * FullRewriteNeeded(n) should be used, giving self-documenting
56 class RewriteResponse
{
58 enum Status
{ DONE
, REWRITE
, REWRITE_FULL
};
60 RewriteResponse(Status s
, Node n
) : d_status(s
), d_node(n
) {}
63 const Status d_status
;
67 bool isDone() const { return d_status
== DONE
; }
68 bool needsMoreRewriting() const { return d_status
!= DONE
; }
69 bool needsFullRewriting() const { return d_status
== REWRITE_FULL
; }
70 Node
getNode() const { return d_node
; }
71 };/* class RewriteResponse */
74 * Signal that (pre,post)rewriting of the Node is complete at n. Note
75 * that if theory A returns this, and the Node is in another theory B,
76 * theory B will still be called on to pre- or postrewrite it.
78 class RewriteComplete
: public RewriteResponse
{
80 RewriteComplete(Node n
) : RewriteResponse(DONE
, n
) {}
81 };/* class RewriteComplete */
84 * Return n, but request additional rewriting of it; if this is
85 * returned from preRewrite(), this re-preRewrite()'s the Node. If
86 * this is returned from postRewrite(), this re-postRewrite()'s the
87 * Node, but does NOT re-preRewrite() it, nor does it rewrite the
90 * Note that this is the behavior if a theory returns
91 * RewriteComplete() for a Node belonging to another theory.
93 class RewriteAgain
: public RewriteResponse
{
95 RewriteAgain(Node n
) : RewriteResponse(REWRITE
, n
) {}
96 };/* class RewriteAgain */
99 * Return n, but request an additional complete rewriting pass over
100 * it. This has the same behavior as RewriteAgain() for
101 * pre-rewriting. However, in post-rewriting, FullRewriteNeeded will
102 * _completely_ pre- and post-rewrite the term and the term's children
103 * (though it will use the cache to elide what calls it can). Use
104 * with caution; it has bad effects on performance. This might be
105 * useful if theory A rewrites a term into something quite different,
106 * and certain child nodes might belong to another theory whose normal
107 * form is unknown to theory A. For example, if the builtin theory
108 * post-rewrites (DISTINCT a b c) into pairwise NOT EQUAL expressions,
109 * the theories owning a, b, and c might need to rewrite that EQUAL.
110 * (This came up, but the fix was to rewrite DISTINCT in
111 * pre-rewriting, obviating the problem. See bug #168.)
113 class FullRewriteNeeded
: public RewriteResponse
{
115 FullRewriteNeeded(Node n
) : RewriteResponse(REWRITE_FULL
, n
) {}
116 };/* class FullRewriteNeeded */
119 * Base class for T-solvers. Abstract DPLL(T).
121 * This is essentially an interface class. The TheoryEngine has
122 * pointers to Theory. Note that only one specific Theory type (e.g.,
123 * TheoryUF) can exist per NodeManager, because of how the
124 * RegisteredAttr works. (If you need multiple instances of the same
125 * theory, you'll have to write a multiplexed theory that dispatches
126 * all calls to them.)
131 friend class ::CVC4::TheoryEngine
;
134 * Disallow default construction.
139 * A unique integer identifying the theory
144 * The context for the Theory.
146 context::Context
* d_context
;
149 * The assertFact() queue.
151 * This queue MUST be emptied by ANY call to check() at ANY effort
152 * level. In debug builds, this is checked. On backjump we clear
153 * the fact queue (see FactsResetter, below).
155 * These can safely be TNodes because the literal map maintained in
156 * the SAT solver keeps them live. As an added benefit, if we have
157 * them as TNodes, dtors are cheap (optimized away?).
159 std::deque
<TNode
> d_facts
;
161 /** Helper class to reset the fact queue on pop(). */
162 class FactsResetter
: public context::ContextNotifyObj
{
166 FactsResetter(Theory
& thy
) :
167 context::ContextNotifyObj(thy
.d_context
),
172 d_thy
.d_facts
.clear();
176 friend class FactsResetter
;
181 * Construct a Theory.
183 Theory(int id
, context::Context
* ctxt
, OutputChannel
& out
) throw() :
187 d_factsResetter(*this),
192 * This is called at shutdown time by the TheoryEngine, just before
193 * destruction. It is important because there are destruction
194 * ordering issues between PropEngine and Theory (based on what
195 * hard-links to Nodes are outstanding). As the fact queue might be
196 * nonempty, we ensure here that it's clear. If you overload this,
197 * you must make an explicit call here to this->Theory::shutdown()
200 virtual void shutdown() {
205 * The output channel for the Theory.
207 OutputChannel
* d_out
;
210 * Returns true if the assertFact queue is empty
212 bool done() throw() {
213 return d_facts
.empty();
216 /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
217 struct PreRegistered
{};
218 /** The "preRegisterTerm()-has-been-called" flag on Nodes */
219 typedef CVC4::expr::Attribute
<PreRegistered
, bool> PreRegisteredAttr
;
222 * Returns the next atom in the assertFact() queue. Guarantees that
223 * registerTerm() has been called on the theory specific subterms.
225 * @return the next atom in the assertFact() queue.
228 Assert( !d_facts
.empty(),
229 "Theory::get() called with assertion queue empty!" );
230 Node fact
= d_facts
.front();
232 Debug("theory") << "Theory::get() => " << fact
233 << "(" << d_facts
.size() << " left)" << std::endl
;
234 d_out
->newFact(fact
);
241 * Destructs a Theory. This implementation does nothing, but we
242 * need a virtual destructor for safety in case subclasses have a
249 * Subclasses of Theory may add additional efforts. DO NOT CHECK
250 * equality with one of these values (e.g. if STANDARD xxx) but
251 * rather use range checks (or use the helper functions below).
252 * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
262 // TODO add compiler annotation "constant function" here
263 static bool minEffortOnly(Effort e
) { return e
== MIN_EFFORT
; }
264 static bool quickCheckOrMore(Effort e
) { return e
>= QUICK_CHECK
; }
265 static bool quickCheckOnly(Effort e
) { return e
>= QUICK_CHECK
&& e
< STANDARD
; }
266 static bool standardEffortOrMore(Effort e
) { return e
>= STANDARD
; }
267 static bool standardEffortOnly(Effort e
) { return e
>= STANDARD
&& e
< FULL_EFFORT
; }
268 static bool fullEffort(Effort e
) { return e
>= FULL_EFFORT
; }
271 * Get the id for this Theory.
278 * Get the context associated to this Theory.
280 context::Context
* getContext() const {
285 * Set the output channel associated to this theory.
287 void setOutputChannel(OutputChannel
& out
) {
292 * Get the output channel associated to this theory.
294 OutputChannel
& getOutputChannel() {
299 * Get the output channel associated to this theory [const].
301 const OutputChannel
& getOutputChannel() const {
306 * Pre-register a term. Done one time for a Node, ever.
308 virtual void preRegisterTerm(TNode
) = 0;
311 * Pre-rewrite a term. This default base-class implementation
312 * simply returns RewriteComplete(n). A theory should never
313 * rewrite a term to a strictly larger term that contains itself, as
314 * this will cause a loop of hard Node links in the cache (and thus
317 * Be careful with the return value. If a preRewrite() can return a
318 * sub-expression, and that sub-expression can be a member of the
319 * same theory and could be rewritten, make sure to return
320 * RewriteAgain instead of RewriteComplete. This is an easy mistake
321 * to make, as preRewrite() is often a short-circuiting version of
322 * the same rewrites that occur in postRewrite(); however, in the
323 * postRewrite() case, the subexpressions have all been
324 * post-rewritten. In the preRewrite() case, they have NOT yet been
325 * pre-rewritten. For example, (ITE true (ITE true x y) z) should
326 * pre-rewrite to x; but if the outer preRewrite() returns
327 * RewriteComplete, the result of the pre-rewrite will be
330 virtual RewriteResponse
preRewrite(TNode n
, bool topLevel
) {
331 Debug("theory-rewrite") << "no pre-rewriting to perform for " << n
<< std::endl
;
332 return RewriteComplete(n
);
336 * Post-rewrite a term. This default base-class implementation
337 * simply returns RewriteComplete(n). A theory should never
338 * rewrite a term to a strictly larger term that contains itself, as
339 * this will cause a loop of hard Node links in the cache (and thus
342 virtual RewriteResponse
postRewrite(TNode n
, bool topLevel
) {
343 Debug("theory-rewrite") << "no post-rewriting to perform for " << n
<< std::endl
;
344 return RewriteComplete(n
);
350 * When get() is called to get the next thing off the theory queue,
351 * setup() is called on its subterms (in TheoryEngine). Then setup()
352 * is called on this node.
354 * This is done in a "context escape" -- that is, at context level 0.
355 * setup() MUST NOT MODIFY context-dependent objects that it hasn't
356 * itself just created.
358 virtual void registerTerm(TNode
) = 0;
361 * Assert a fact in the current context.
363 void assertFact(TNode n
) {
364 Debug("theory") << "Theory::assertFact(" << n
<< ")" << std::endl
;
365 d_facts
.push_back(n
);
369 * This method is called to notify a theory that the node n should be considered a "shared term" by this theory
371 virtual void addSharedTerm(TNode n
) { }
374 * This method is called by the shared term manager when a shared term lhs
375 * which this theory cares about (either because it received a previous
376 * addSharedTerm call with lhs or because it received a previous notifyEq call
377 * with lhs as the second argument) becomes equal to another shared term rhs.
378 * This call also serves as notice to the theory that the shared term manager
379 * now considers rhs the representative for this equivalence class of shared
380 * terms, so future notifications for this class will be based on rhs not lhs.
382 virtual void notifyEq(TNode lhs
, TNode rhs
) { }
385 * Check the current assignment's consistency.
387 * An implementation of check() is required to either:
388 * - return a conflict on the output channel,
390 * - throw an exception
391 * - or call get() until done() is true.
393 virtual void check(Effort level
= FULL_EFFORT
) = 0;
396 * T-propagate new literal assignments in the current context.
398 virtual void propagate(Effort level
= FULL_EFFORT
) = 0;
401 * Return an explanation for the literal represented by parameter n
402 * (which was previously propagated by this theory). Report
403 * explanations to an output channel.
405 virtual void explain(TNode n
, Effort level
= FULL_EFFORT
) = 0;
408 * Identify this theory (for debugging, dynamic configuration,
411 virtual std::string
identify() const = 0;
414 // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
418 * Different states at which invariants are checked.
423 };/* enum ReadyState */
426 * Public invariant checker. Assert that this theory is in a valid
427 * state for the (external) system state. This implementation
428 * checks base invariants and then calls theoryReady(). This
429 * function may abort in the case of a failed assert, or return
430 * false (the caller should assert that the return value is true).
432 * @param s the state about which to check invariants
434 bool ready(ReadyState s
) {
435 if(s
== ABOUT_TO_PUSH
) {
436 Assert(d_facts
.empty(), "Theory base code invariant broken: "
437 "fact queue is nonempty on context push");
440 return theoryReady(s
);
446 * Check any invariants at the ReadyState given. Only called by
447 * Theory class, and then only with CVC4_ASSERTIONS enabled. This
448 * function may abort in the case of a failed assert, or return
449 * false (the caller should assert that the return value is true).
451 * @param s the state about which to check invariants
453 virtual bool theoryReady(ReadyState s
) {
458 * Check whether a node is in the pre-rewrite cache or not.
460 static bool inPreRewriteCache(TNode n
, bool topLevel
) throw() {
462 return n
.hasAttribute(PreRewriteCacheTop());
464 return n
.hasAttribute(PreRewriteCache());
469 * Get the value of the pre-rewrite cache (or Node::null()) if there is
472 static Node
getPreRewriteCache(TNode n
, bool topLevel
) throw() {
475 if(n
.getAttribute(PreRewriteCacheTop(), out
)) {
476 return out
.isNull() ? Node(n
) : out
;
480 if(n
.getAttribute(PreRewriteCache(), out
)) {
481 return out
.isNull() ? Node(n
) : out
;
488 * Set the value of the pre-rewrite cache. v cannot be a null Node.
490 static void setPreRewriteCache(TNode n
, bool topLevel
, TNode v
) throw() {
491 AssertArgument(!n
.isNull(), n
, "n cannot be null in setPostRewriteCache()");
492 AssertArgument(!v
.isNull(), v
, "v cannot be null in setPreRewriteCache()");
493 // mappings from n -> n are actually stored as n -> null as a
494 // special case, to avoid cycles in the reference-counting of Nodes
496 n
.setAttribute(PreRewriteCacheTop(), n
== v
? TNode::null() : v
);
498 n
.setAttribute(PreRewriteCache(), n
== v
? TNode::null() : v
);
503 * Check whether a node is in the post-rewrite cache or not.
505 static bool inPostRewriteCache(TNode n
, bool topLevel
) throw() {
507 return n
.hasAttribute(PostRewriteCacheTop());
509 return n
.hasAttribute(PostRewriteCache());
514 * Get the value of the post-rewrite cache (or Node::null()) if there is
517 static Node
getPostRewriteCache(TNode n
, bool topLevel
) throw() {
520 if(n
.getAttribute(PostRewriteCacheTop(), out
)) {
521 return out
.isNull() ? Node(n
) : out
;
525 if(n
.getAttribute(PostRewriteCache(), out
)) {
526 return out
.isNull() ? Node(n
) : out
;
533 * Set the value of the post-rewrite cache. v cannot be a null Node.
535 static void setPostRewriteCache(TNode n
, bool topLevel
, TNode v
) throw() {
536 AssertArgument(!n
.isNull(), n
, "n cannot be null in setPostRewriteCache()");
537 AssertArgument(!v
.isNull(), v
, "v cannot be null in setPostRewriteCache()");
538 // mappings from n -> n are actually stored as n -> null as a
539 // special case, to avoid cycles in the reference-counting of Nodes
541 n
.setAttribute(PostRewriteCacheTop(), n
== v
? TNode::null() : v
);
543 n
.setAttribute(PostRewriteCache(), n
== v
? TNode::null() : v
);
549 std::ostream
& operator<<(std::ostream
& os
, Theory::Effort level
);
551 }/* CVC4::theory namespace */
553 inline std::ostream
& operator<<(std::ostream
& out
, const CVC4::theory::Theory
& theory
) {
554 return out
<< theory
.identify();
557 }/* CVC4 namespace */
559 #endif /* __CVC4__THEORY__THEORY_H */