src/theory/theory.h

   1 /*********************                                                        */
   2 /*! \file theory.h
   3  ** \verbatim
   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
  13  **
  14  ** \brief Base of the theory interface.
  15  **
  16  ** Base of the theory interface.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY__THEORY_H
  22 #define __CVC4__THEORY__THEORY_H
  23
  24 #include "expr/node.h"
  25 #include "expr/attribute.h"
  26 #include "theory/output_channel.h"
  27 #include "context/context.h"
  28
  29 #include <deque>
  30 #include <list>
  31
  32 #include <string>
  33 #include <iostream>
  34
  35 namespace CVC4 {
  36
  37 class TheoryEngine;
  38
  39 namespace theory {
  40
  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;
  48
  49 /**
  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
  54  * rewrite behavior.
  55  */
  56 class RewriteResponse {
  57 protected:
  58   enum Status { DONE, REWRITE, REWRITE_FULL };
  59
  60   RewriteResponse(Status s, Node n) : d_status(s), d_node(n) {}
  61
  62 private:
  63   const Status d_status;
  64   const Node d_node;
  65
  66 public:
  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 */
  72
  73 /**
  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.
  77  */
  78 class RewriteComplete : public RewriteResponse {
  79 public:
  80   RewriteComplete(Node n) : RewriteResponse(DONE, n) {}
  81 };/* class RewriteComplete */
  82
  83 /**
  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
  88  * Node's children.
  89  *
  90  * Note that this is the behavior if a theory returns
  91  * RewriteComplete() for a Node belonging to another theory.
  92  */
  93 class RewriteAgain : public RewriteResponse {
  94 public:
  95   RewriteAgain(Node n) : RewriteResponse(REWRITE, n) {}
  96 };/* class RewriteAgain */
  97
  98 /**
  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.)
 112  */
 113 class FullRewriteNeeded : public RewriteResponse {
 114 public:
 115   FullRewriteNeeded(Node n) : RewriteResponse(REWRITE_FULL, n) {}
 116 };/* class FullRewriteNeeded */
 117
 118 /**
 119  * Base class for T-solvers.  Abstract DPLL(T).
 120  *
 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.)
 127  */
 128 class Theory {
 129 private:
 130
 131   friend class ::CVC4::TheoryEngine;
 132
 133   /**
 134    * Disallow default construction.
 135    */
 136   Theory();
 137
 138   /**
 139    * A unique integer identifying the theory
 140    */
 141   int d_id;
 142
 143   /**
 144    * The context for the Theory.
 145    */
 146   context::Context* d_context;
 147
 148   /**
 149    * The assertFact() queue.
 150    *
 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).
 154    *
 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?).
 158    */
 159   std::deque<TNode> d_facts;
 160
 161   /** Helper class to reset the fact queue on pop(). */
 162   class FactsResetter : public context::ContextNotifyObj {
 163     Theory& d_thy;
 164
 165   public:
 166     FactsResetter(Theory& thy) :
 167       context::ContextNotifyObj(thy.d_context),
 168       d_thy(thy) {
 169     }
 170
 171     void notify() {
 172       d_thy.d_facts.clear();
 173     }
 174   } d_factsResetter;
 175
 176   friend class FactsResetter;
 177
 178 protected:
 179
 180   /**
 181    * Construct a Theory.
 182    */
 183   Theory(int id, context::Context* ctxt, OutputChannel& out) throw() :
 184     d_id(id),
 185     d_context(ctxt),
 186     d_facts(),
 187     d_factsResetter(*this),
 188     d_out(&out) {
 189   }
 190
 191   /**
 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()
 198    * too.
 199    */
 200   virtual void shutdown() {
 201     d_facts.clear();
 202   }
 203
 204   /**
 205    * The output channel for the Theory.
 206    */
 207   OutputChannel* d_out;
 208
 209   /**
 210    * Returns true if the assertFact queue is empty
 211    */
 212   bool done() throw() {
 213     return d_facts.empty();
 214   }
 215
 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;
 220
 221   /**
 222    * Returns the next atom in the assertFact() queue.  Guarantees that
 223    * registerTerm() has been called on the theory specific subterms.
 224    *
 225    * @return the next atom in the assertFact() queue.
 226    */
 227   Node get() {
 228     Assert( !d_facts.empty(),
 229             "Theory::get() called with assertion queue empty!" );
 230     Node fact = d_facts.front();
 231     d_facts.pop_front();
 232     Debug("theory") << "Theory::get() => " << fact
 233                     << "(" << d_facts.size() << " left)" << std::endl;
 234     d_out->newFact(fact);
 235     return fact;
 236   }
 237
 238 public:
 239
 240   /**
 241    * Destructs a Theory.  This implementation does nothing, but we
 242    * need a virtual destructor for safety in case subclasses have a
 243    * destructor.
 244    */
 245   virtual ~Theory() {
 246   }
 247
 248   /**
 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
 253    * with MAX_EFFORT.
 254    */
 255   enum Effort {
 256     MIN_EFFORT = 0,
 257     QUICK_CHECK = 10,
 258     STANDARD = 50,
 259     FULL_EFFORT = 100
 260   };/* enum Effort */
 261
 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; }
 269
 270   /**
 271    * Get the id for this Theory.
 272    */
 273   int getId() const {
 274     return d_id;
 275   }
 276
 277   /**
 278    * Get the context associated to this Theory.
 279    */
 280   context::Context* getContext() const {
 281     return d_context;
 282   }
 283
 284   /**
 285    * Set the output channel associated to this theory.
 286    */
 287   void setOutputChannel(OutputChannel& out) {
 288     d_out = &out;
 289   }
 290
 291   /**
 292    * Get the output channel associated to this theory.
 293    */
 294   OutputChannel& getOutputChannel() {
 295     return *d_out;
 296   }
 297
 298   /**
 299    * Get the output channel associated to this theory [const].
 300    */
 301   const OutputChannel& getOutputChannel() const {
 302     return *d_out;
 303   }
 304
 305   /**
 306    * Pre-register a term.  Done one time for a Node, ever.
 307    */
 308   virtual void preRegisterTerm(TNode) = 0;
 309
 310   /**
 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
 315    * memory leakage).
 316    *
 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
 328    * (ITE true x y).
 329    */
 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);
 333   }
 334
 335   /**
 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
 340    * memory leakage).
 341    */
 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);
 345   }
 346
 347   /**
 348    * Register a term.
 349    *
 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.
 353    *
 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.
 357    */
 358   virtual void registerTerm(TNode) = 0;
 359
 360   /**
 361    * Assert a fact in the current context.
 362    */
 363   void assertFact(TNode n) {
 364     Debug("theory") << "Theory::assertFact(" << n << ")" << std::endl;
 365     d_facts.push_back(n);
 366   }
 367
 368   /**
 369    * This method is called to notify a theory that the node n should be considered a "shared term" by this theory
 370    */
 371   virtual void addSharedTerm(TNode n) { }
 372
 373   /**
 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.
 381    */
 382   virtual void notifyEq(TNode lhs, TNode rhs) { }
 383
 384   /**
 385    * Check the current assignment's consistency.
 386    *
 387    * An implementation of check() is required to either:
 388    * - return a conflict on the output channel,
 389    * - be interrupted,
 390    * - throw an exception
 391    * - or call get() until done() is true.
 392    */
 393   virtual void check(Effort level = FULL_EFFORT) = 0;
 394
 395   /**
 396    * T-propagate new literal assignments in the current context.
 397    */
 398   virtual void propagate(Effort level = FULL_EFFORT) = 0;
 399
 400   /**
 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.
 404    */
 405   virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0;
 406
 407   /**
 408    * Identify this theory (for debugging, dynamic configuration,
 409    * etc..)
 410    */
 411   virtual std::string identify() const = 0;
 412
 413   //
 414   // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
 415   //
 416
 417   /**
 418    * Different states at which invariants are checked.
 419    */
 420   enum ReadyState {
 421     ABOUT_TO_PUSH,
 422     ABOUT_TO_POP
 423   };/* enum ReadyState */
 424
 425   /**
 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).
 431    *
 432    * @param s the state about which to check invariants
 433    */
 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");
 438     }
 439
 440     return theoryReady(s);
 441   }
 442
 443 protected:
 444
 445   /**
 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).
 450    *
 451    * @param s the state about which to check invariants
 452    */
 453   virtual bool theoryReady(ReadyState s) {
 454     return true;
 455   }
 456
 457   /**
 458    * Check whether a node is in the pre-rewrite cache or not.
 459    */
 460   static bool inPreRewriteCache(TNode n, bool topLevel) throw() {
 461     if(topLevel) {
 462       return n.hasAttribute(PreRewriteCacheTop());
 463     } else {
 464       return n.hasAttribute(PreRewriteCache());
 465     }
 466   }
 467
 468   /**
 469    * Get the value of the pre-rewrite cache (or Node::null()) if there is
 470    * none).
 471    */
 472   static Node getPreRewriteCache(TNode n, bool topLevel) throw() {
 473     if(topLevel) {
 474       Node out;
 475       if(n.getAttribute(PreRewriteCacheTop(), out)) {
 476         return out.isNull() ? Node(n) : out;
 477       }
 478     } else {
 479       Node out;
 480       if(n.getAttribute(PreRewriteCache(), out)) {
 481         return out.isNull() ? Node(n) : out;
 482       }
 483     }
 484     return Node::null();
 485   }
 486
 487   /**
 488    * Set the value of the pre-rewrite cache.  v cannot be a null Node.
 489    */
 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
 495     if(topLevel) {
 496       n.setAttribute(PreRewriteCacheTop(), n == v ? TNode::null() : v);
 497     } else {
 498       n.setAttribute(PreRewriteCache(), n == v ? TNode::null() : v);
 499     }
 500   }
 501
 502   /**
 503    * Check whether a node is in the post-rewrite cache or not.
 504    */
 505   static bool inPostRewriteCache(TNode n, bool topLevel) throw() {
 506     if(topLevel) {
 507       return n.hasAttribute(PostRewriteCacheTop());
 508     } else {
 509       return n.hasAttribute(PostRewriteCache());
 510     }
 511   }
 512
 513   /**
 514    * Get the value of the post-rewrite cache (or Node::null()) if there is
 515    * none).
 516    */
 517   static Node getPostRewriteCache(TNode n, bool topLevel) throw() {
 518     if(topLevel) {
 519       Node out;
 520       if(n.getAttribute(PostRewriteCacheTop(), out)) {
 521         return out.isNull() ? Node(n) : out;
 522       }
 523     } else {
 524       Node out;
 525       if(n.getAttribute(PostRewriteCache(), out)) {
 526         return out.isNull() ? Node(n) : out;
 527       }
 528     }
 529     return Node::null();
 530   }
 531
 532   /**
 533    * Set the value of the post-rewrite cache.  v cannot be a null Node.
 534    */
 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
 540     if(topLevel) {
 541       n.setAttribute(PostRewriteCacheTop(), n == v ? TNode::null() : v);
 542     } else {
 543       n.setAttribute(PostRewriteCache(), n == v ? TNode::null() : v);
 544     }
 545   }
 546
 547 };/* class Theory */
 548
 549 std::ostream& operator<<(std::ostream& os, Theory::Effort level);
 550
 551 }/* CVC4::theory namespace */
 552
 553 inline std::ostream& operator<<(std::ostream& out, const CVC4::theory::Theory& theory) {
 554   return out << theory.identify();
 555 }
 556
 557 }/* CVC4 namespace */
 558
 559 #endif /* __CVC4__THEORY__THEORY_H */