src/theory/theory.h

   1 /*********************                                                        */
   2 /*! \file theory.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: dejan
   6  ** Minor contributors (to current version): taking, barrett
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  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/valuation.h"
  27 #include "theory/output_channel.h"
  28 #include "context/context.h"
  29 #include "context/cdlist.h"
  30 #include "context/cdo.h"
  31 #include "util/options.h"
  32
  33 #include <string>
  34 #include <iostream>
  35
  36 namespace CVC4 {
  37
  38 class TheoryEngine;
  39
  40 namespace theory {
  41
  42 /** Tag for the "newFact()-has-been-called-in-this-context" flag on Nodes */
  43 struct AssertedAttrTag {};
  44 /** The "newFact()-has-been-called-in-this-context" flag on Nodes */
  45 typedef CVC4::expr::CDAttribute<AssertedAttrTag, bool> Asserted;
  46
  47 /**
  48  * Base class for T-solvers.  Abstract DPLL(T).
  49  *
  50  * This is essentially an interface class.  The TheoryEngine has
  51  * pointers to Theory.  Note that only one specific Theory type (e.g.,
  52  * TheoryUF) can exist per NodeManager, because of how the
  53  * RegisteredAttr works.  (If you need multiple instances of the same
  54  * theory, you'll have to write a multiplexed theory that dispatches
  55  * all calls to them.)
  56  */
  57 class Theory {
  58 private:
  59
  60   friend class ::CVC4::TheoryEngine;
  61
  62   // Disallow default construction, copy, assignment.
  63   Theory() CVC4_UNUSED;
  64   Theory(const Theory&) CVC4_UNUSED;
  65   Theory& operator=(const Theory&) CVC4_UNUSED;
  66
  67   /**
  68    * A unique integer identifying the theory
  69    */
  70   TheoryId d_id;
  71
  72   /**
  73    * The context for the Theory.
  74    */
  75   context::Context* d_context;
  76
  77   /**
  78    * The assertFact() queue.
  79    *
  80    * These can not be TNodes as some atoms (such as equalities) are sent
  81    * across theories without being stored in a global map.
  82    */
  83   context::CDList<Node> d_facts;
  84
  85   /** Index into the head of the facts list */
  86   context::CDO<unsigned> d_factsHead;
  87
  88 protected:
  89
  90   /**
  91    * Construct a Theory.
  92    */
  93   Theory(TheoryId id, context::Context* ctxt, OutputChannel& out, Valuation valuation) throw() :
  94     d_id(id),
  95     d_context(ctxt),
  96     d_facts(ctxt),
  97     d_factsHead(ctxt, 0),
  98     d_out(&out),
  99     d_valuation(valuation) {
 100   }
 101
 102   /**
 103    * This is called at shutdown time by the TheoryEngine, just before
 104    * destruction.  It is important because there are destruction
 105    * ordering issues between PropEngine and Theory (based on what
 106    * hard-links to Nodes are outstanding).  As the fact queue might be
 107    * nonempty, we ensure here that it's clear.  If you overload this,
 108    * you must make an explicit call here to this->Theory::shutdown()
 109    * too.
 110    */
 111   virtual void shutdown() { }
 112
 113   /**
 114    * The output channel for the Theory.
 115    */
 116   OutputChannel* d_out;
 117
 118   /**
 119    * The valuation proxy for the Theory to communicate back with the
 120    * theory engine (and other theories).
 121    */
 122   Valuation d_valuation;
 123
 124   /**
 125    * Returns the next atom in the assertFact() queue.  Guarantees that
 126    * registerTerm() has been called on the theory specific subterms.
 127    *
 128    * @return the next atom in the assertFact() queue.
 129    */
 130   TNode get() {
 131     Assert( !done(), "Theory::get() called with assertion queue empty!" );
 132     TNode fact = d_facts[d_factsHead];
 133     d_factsHead = d_factsHead + 1;
 134     Debug("theory") << "Theory::get() => " << fact
 135                     << "(" << d_facts.size() << " left)" << std::endl;
 136     d_out->newFact(fact);
 137     return fact;
 138   }
 139
 140   /**
 141    * Provides access to the facts queue, primarily intended for theory
 142    * debugging purposes.
 143    *
 144    * @return the iterator to the beginning of the fact queue
 145    */
 146   context::CDList<Node>::const_iterator facts_begin() const {
 147     return d_facts.begin();
 148   }
 149
 150   /**
 151    * Provides access to the facts queue, primarily intended for theory
 152    * debugging purposes.
 153    *
 154    * @return the iterator to the end of the fact queue
 155    */
 156   context::CDList<Node>::const_iterator facts_end() const {
 157     return d_facts.end();
 158   }
 159
 160 public:
 161
 162   static inline TheoryId theoryOf(TypeNode typeNode) {
 163     if (typeNode.getKind() == kind::TYPE_CONSTANT) {
 164       return typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
 165     } else {
 166       return kindToTheoryId(typeNode.getKind());
 167     }
 168   }
 169
 170   /**
 171    * Returns the theory responsible for the node.
 172    */
 173   static inline TheoryId theoryOf(TNode node) {
 174     if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) {
 175       // Constants, variables, 0-ary constructors
 176       return theoryOf(node.getType());
 177     } else {
 178       // Regular nodes
 179       return kindToTheoryId(node.getKind());
 180     }
 181   }
 182
 183   /**
 184    * Checks if the node is a leaf node of this theory
 185    */
 186   inline bool isLeaf(TNode node) const {
 187     return node.getNumChildren() == 0 || theoryOf(node) != d_id;
 188   }
 189
 190   /**
 191    * Checks if the node is a leaf node of a theory.
 192    */
 193   inline static bool isLeafOf(TNode node, TheoryId theoryId) {
 194     return node.getNumChildren() == 0 || theoryOf(node) != theoryId;
 195   }
 196
 197   /**
 198    * Returns true if the assertFact queue is empty
 199    */
 200   bool done() throw() {
 201     return d_factsHead == d_facts.size();
 202   }
 203
 204   /**
 205    * Destructs a Theory.  This implementation does nothing, but we
 206    * need a virtual destructor for safety in case subclasses have a
 207    * destructor.
 208    */
 209   virtual ~Theory() {
 210   }
 211
 212   /**
 213    * Subclasses of Theory may add additional efforts.  DO NOT CHECK
 214    * equality with one of these values (e.g. if STANDARD xxx) but
 215    * rather use range checks (or use the helper functions below).
 216    * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
 217    * with MAX_EFFORT.
 218    */
 219   enum Effort {
 220     MIN_EFFORT = 0,
 221     QUICK_CHECK = 10,
 222     STANDARD = 50,
 223     FULL_EFFORT = 100
 224   };/* enum Effort */
 225
 226   // simple, useful predicates for effort values
 227   static inline bool minEffortOnly(Effort e) CVC4_CONST_FUNCTION
 228     { return e == MIN_EFFORT; }
 229   static inline bool quickCheckOrMore(Effort e) CVC4_CONST_FUNCTION
 230     { return e >= QUICK_CHECK; }
 231   static inline bool quickCheckOnly(Effort e) CVC4_CONST_FUNCTION
 232     { return e >= QUICK_CHECK && e <  STANDARD; }
 233   static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION
 234     { return e >= STANDARD; }
 235   static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION
 236     { return e >= STANDARD && e <  FULL_EFFORT; }
 237   static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION
 238     { return e >= FULL_EFFORT; }
 239
 240   /**
 241    * Get the id for this Theory.
 242    */
 243   TheoryId getId() const {
 244     return d_id;
 245   }
 246
 247   /**
 248    * Get the context associated to this Theory.
 249    */
 250   context::Context* getContext() const {
 251     return d_context;
 252   }
 253
 254   /**
 255    * Set the output channel associated to this theory.
 256    */
 257   void setOutputChannel(OutputChannel& out) {
 258     d_out = &out;
 259   }
 260
 261   /**
 262    * Get the output channel associated to this theory.
 263    */
 264   OutputChannel& getOutputChannel() {
 265     return *d_out;
 266   }
 267
 268   /**
 269    * Pre-register a term.  Done one time for a Node, ever.
 270    */
 271   virtual void preRegisterTerm(TNode) { }
 272
 273   /**
 274    * Register a term.
 275    *
 276    * When get() is called to get the next thing off the theory queue,
 277    * setup() is called on its subterms (in TheoryEngine).  Then setup()
 278    * is called on this node.
 279    *
 280    * This is done in a "context escape" -- that is, at context level 0.
 281    * setup() MUST NOT MODIFY context-dependent objects that it hasn't
 282    * itself just created.
 283    */
 284   virtual void registerTerm(TNode) { }
 285
 286   /**
 287    * Assert a fact in the current context.
 288    */
 289   void assertFact(TNode node) {
 290     Debug("theory") << "Theory::assertFact(" << node << ")" << std::endl;
 291     d_facts.push_back(node);
 292   }
 293
 294   /**
 295    * This method is called to notify a theory that the node n should
 296    * be considered a "shared term" by this theory
 297    */
 298   virtual void addSharedTerm(TNode n) { }
 299
 300   /**
 301    * This method is called by the shared term manager when a shared
 302    * term lhs which this theory cares about (either because it
 303    * received a previous addSharedTerm call with lhs or because it
 304    * received a previous notifyEq call with lhs as the second
 305    * argument) becomes equal to another shared term rhs.  This call
 306    * also serves as notice to the theory that the shared term manager
 307    * now considers rhs the representative for this equivalence class
 308    * of shared terms, so future notifications for this class will be
 309    * based on rhs not lhs.
 310    */
 311   virtual void notifyEq(TNode lhs, TNode rhs) { }
 312
 313   /**
 314    * Check the current assignment's consistency.
 315    *
 316    * An implementation of check() is required to either:
 317    * - return a conflict on the output channel,
 318    * - be interrupted,
 319    * - throw an exception
 320    * - or call get() until done() is true.
 321    */
 322   virtual void check(Effort level = FULL_EFFORT) { }
 323
 324   /**
 325    * T-propagate new literal assignments in the current context.
 326    */
 327   virtual void propagate(Effort level = FULL_EFFORT) { }
 328
 329   /**
 330    * Return an explanation for the literal represented by parameter n
 331    * (which was previously propagated by this theory).  Report
 332    * explanations to an output channel.
 333    */
 334   virtual void explain(TNode n) {
 335     Unimplemented("Theory %s propagated a node but doesn't implement the "
 336                   "Theory::explain() interface!", identify().c_str());
 337   }
 338
 339   /**
 340    * Return the value of a node (typically used after a ).  If the
 341    * theory supports model generation but has no value for this node,
 342    * it should return Node::null().  If the theory doesn't support
 343    * model generation at all, or usually would but doesn't in its
 344    * current state, it should throw an exception saying so.
 345    *
 346    * The TheoryEngine is passed in so that you can recursively request
 347    * values for the Node's children.  This is important because the
 348    * TheoryEngine takes care of simple cases (metakind CONSTANT,
 349    * Boolean-valued VARIABLES, ...) and can dispatch to other theories
 350    * if that's necessary.  Only call your own getValue() recursively
 351    * if you *know* that you are responsible handle the Node you're
 352    * asking for; other theories can use your types, so be careful
 353    * here!  To be safe, it's best to delegate back to the
 354    * TheoryEngine (by way of the Valuation proxy object, which avoids
 355    * direct dependence on TheoryEngine).
 356    *
 357    * Usually, you need to handle at least the two cases of EQUAL and
 358    * VARIABLE---EQUAL in case a value of yours is on the LHS of an
 359    * EQUAL, and VARIABLE for variables of your types.  You also need
 360    * to support any operators that can survive your rewriter.  You
 361    * don't need to handle constants, as they are handled by the
 362    * TheoryEngine.
 363    *
 364    * There are some gotchas here.  The user may be requesting the
 365    * value of an expression that wasn't part of the satisfiable
 366    * assertion, or has been declared since.  If you don't have a value
 367    * and suspect this situation is the case, return Node::null()
 368    * rather than throwing an exception.
 369    */
 370   virtual Node getValue(TNode n) {
 371     Unimplemented("Theory %s doesn't support Theory::getValue interface",
 372                   identify().c_str());
 373     return Node::null();
 374   }
 375
 376   /**
 377    * The theory should only add (via .operator<< or .append()) to the
 378    * "learned" builder.  It is a conjunction to add to the formula at
 379    * the top-level and may contain other theories' contributions.
 380    */
 381   virtual void staticLearning(TNode in, NodeBuilder<>& learned) { }
 382
 383   /**
 384    * A Theory is called with presolve exactly one time per user
 385    * check-sat.  presolve() is called after preregistration,
 386    * rewriting, and Boolean propagation, (other theories'
 387    * propagation?), but the notified Theory has not yet had its
 388    * check() or propagate() method called.  A Theory may empty its
 389    * assertFact() queue using get().  A Theory can raise conflicts,
 390    * add lemmas, and propagate literals during presolve().
 391    */
 392   virtual void presolve() { }
 393
 394   /**
 395    * Notification sent to the theory wheneven the search restarts.
 396    * Serves as a good time to do some clean-up work, and you can
 397    * assume you're at DL 0 for the purposes of Contexts.  This function
 398    * should not use the output channel.
 399    */
 400   virtual void notifyRestart() { }
 401
 402   /**
 403    * Identify this theory (for debugging, dynamic configuration,
 404    * etc..)
 405    */
 406   virtual std::string identify() const = 0;
 407
 408 };/* class Theory */
 409
 410 std::ostream& operator<<(std::ostream& os, Theory::Effort level);
 411
 412 }/* CVC4::theory namespace */
 413
 414 inline std::ostream& operator<<(std::ostream& out,
 415                                 const CVC4::theory::Theory& theory) {
 416   return out << theory.identify();
 417 }
 418
 419 }/* CVC4 namespace */
 420
 421 #endif /* __CVC4__THEORY__THEORY_H */