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 "expr/command.h"
  27 #include "theory/valuation.h"
  28 #include "theory/substitutions.h"
  29 #include "theory/output_channel.h"
  30 #include "context/context.h"
  31 #include "context/cdlist.h"
  32 #include "context/cdo.h"
  33 #include "util/options.h"
  34 #include "util/dump.h"
  35
  36 #include <string>
  37 #include <iostream>
  38
  39 namespace CVC4 {
  40
  41 class TheoryEngine;
  42
  43 namespace theory {
  44
  45 /**
  46  * Information about an assertion for the theories.
  47  */
  48 struct Assertion {
  49
  50   /** The assertion */
  51   Node assertion;
  52   /** Has this assertion been preregistered with this theory */
  53   bool isPreregistered;
  54
  55   Assertion(TNode assertion, bool isPreregistered)
  56   : assertion(assertion), isPreregistered(isPreregistered) {}
  57
  58   /**
  59    * Convert the assertion to a TNode.
  60    */
  61   operator TNode () const {
  62     return assertion;
  63   }
  64
  65   /**
  66    * Convert the assertion to a Node.
  67    */
  68   operator Node () const {
  69     return assertion;
  70   }
  71 };
  72
  73 /**
  74  * A pair of terms a theory cares about.
  75  */
  76 struct CarePair {
  77   TNode a, b;
  78   TheoryId theory;
  79   CarePair(TNode a, TNode b, TheoryId theory)
  80   : a(a), b(b), theory(theory) {}
  81 };
  82
  83 /**
  84  * A set of care pairs.
  85  */
  86 typedef std::vector<CarePair> CareGraph;
  87
  88 /**
  89  * Base class for T-solvers.  Abstract DPLL(T).
  90  *
  91  * This is essentially an interface class.  The TheoryEngine has
  92  * pointers to Theory.  Note that only one specific Theory type (e.g.,
  93  * TheoryUF) can exist per NodeManager, because of how the
  94  * RegisteredAttr works.  (If you need multiple instances of the same
  95  * theory, you'll have to write a multiplexed theory that dispatches
  96  * all calls to them.)
  97  */
  98 class Theory {
  99 private:
 100
 101   friend class ::CVC4::TheoryEngine;
 102
 103   // Disallow default construction, copy, assignment.
 104   Theory() CVC4_UNUSED;
 105   Theory(const Theory&) CVC4_UNUSED;
 106   Theory& operator=(const Theory&) CVC4_UNUSED;
 107
 108   /**
 109    * An integer identifying the type of the theory
 110    */
 111   TheoryId d_id;
 112
 113   /**
 114    * The context for the Theory.
 115    */
 116   context::Context* d_context;
 117
 118   /**
 119    * The user context for the Theory.
 120    */
 121   context::UserContext* d_userContext;
 122
 123   /**
 124    * The assertFact() queue.
 125    *
 126    * These can not be TNodes as some atoms (such as equalities) are sent
 127    * across theories without being stored in a global map.
 128    */
 129   context::CDList<Assertion> d_facts;
 130
 131   /** Index into the head of the facts list */
 132   context::CDO<unsigned> d_factsHead;
 133
 134   /**
 135    * Add shared term to the theory.
 136    */
 137   void addSharedTermInternal(TNode node);
 138
 139   /**
 140    * Indices for splitting on the shared terms.
 141    */
 142   context::CDO<unsigned> d_sharedTermsIndex;
 143
 144 protected:
 145
 146   /**
 147    * A list of shared terms that the theory has.
 148    */
 149   context::CDList<TNode> d_sharedTerms;
 150
 151   /**
 152    * Construct a Theory.
 153    */
 154   Theory(TheoryId id, context::Context* context, context::UserContext* userContext,
 155          OutputChannel& out, Valuation valuation) throw() :
 156     d_id(id),
 157     d_context(context),
 158     d_userContext(userContext),
 159     d_facts(context),
 160     d_factsHead(context, 0),
 161     d_sharedTermsIndex(context, 0),
 162     d_sharedTerms(context),
 163     d_out(&out),
 164     d_valuation(valuation)
 165   {
 166   }
 167
 168   /**
 169    * This is called at shutdown time by the TheoryEngine, just before
 170    * destruction.  It is important because there are destruction
 171    * ordering issues between PropEngine and Theory (based on what
 172    * hard-links to Nodes are outstanding).  As the fact queue might be
 173    * nonempty, we ensure here that it's clear.  If you overload this,
 174    * you must make an explicit call here to this->Theory::shutdown()
 175    * too.
 176    */
 177   virtual void shutdown() { }
 178
 179   /**
 180    * The output channel for the Theory.
 181    */
 182   OutputChannel* d_out;
 183
 184   /**
 185    * The valuation proxy for the Theory to communicate back with the
 186    * theory engine (and other theories).
 187    */
 188   Valuation d_valuation;
 189
 190   /**
 191    * Returns the next assertion in the assertFact() queue.
 192    *
 193    * @return the next assertion in the assertFact() queue
 194    */
 195   Assertion get() {
 196     Assert( !done(), "Theory`() called with assertion queue empty!" );
 197
 198     // Get the assertion
 199     Assertion fact = d_facts[d_factsHead];
 200     d_factsHead = d_factsHead + 1;
 201     Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
 202     if(Dump.isOn("state")) {
 203       Dump("state") << AssertCommand(fact.assertion.toExpr());
 204     }
 205
 206     return fact;
 207   }
 208
 209   /**
 210    * The theory that owns the uninterpreted sort.
 211    */
 212   static TheoryId s_uninterpretedSortOwner;
 213
 214   void printFacts(std::ostream& os) const;
 215
 216
 217 public:
 218
 219   /**
 220    * Return the ID of the theory responsible for the given type.
 221    */
 222   static inline TheoryId theoryOf(TypeNode typeNode) {
 223     Trace("theory") << "theoryOf(" << typeNode << ")" << std::endl;
 224     TheoryId id;
 225     while (typeNode.isPredicateSubtype()) {
 226       typeNode = typeNode.getSubtypeBaseType();
 227     }
 228     if (typeNode.getKind() == kind::TYPE_CONSTANT) {
 229       id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
 230     } else {
 231       id = kindToTheoryId(typeNode.getKind());
 232     }
 233     if (id == THEORY_BUILTIN) {
 234       Trace("theory") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl;
 235       return s_uninterpretedSortOwner;
 236     }
 237     return id;
 238   }
 239
 240
 241   /**
 242    * Returns the ID of the theory responsible for the given node.
 243    */
 244   static inline TheoryId theoryOf(TNode node) {
 245     Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl;
 246     // Constants, variables, 0-ary constructors
 247     if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) {
 248       return theoryOf(node.getType());
 249     }
 250     // Equality is owned by the theory that owns the domain
 251     if (node.getKind() == kind::EQUAL) {
 252       return theoryOf(node[0].getType());
 253     }
 254     // Regular nodes are owned by the kind
 255     return kindToTheoryId(node.getKind());
 256   }
 257
 258   /**
 259    * Set the owner of the uninterpreted sort.
 260    */
 261   static void setUninterpretedSortOwner(TheoryId theory) {
 262     s_uninterpretedSortOwner = theory;
 263   }
 264
 265   /**
 266    * Checks if the node is a leaf node of this theory
 267    */
 268   inline bool isLeaf(TNode node) const {
 269     return node.getNumChildren() == 0 || theoryOf(node) != d_id;
 270   }
 271
 272   /**
 273    * Checks if the node is a leaf node of a theory.
 274    */
 275   inline static bool isLeafOf(TNode node, TheoryId theoryId) {
 276     return node.getNumChildren() == 0 || theoryOf(node) != theoryId;
 277   }
 278
 279   /**
 280    * Returns true if the assertFact queue is empty
 281    */
 282   bool done() throw() {
 283     return d_factsHead == d_facts.size();
 284   }
 285
 286   /**
 287    * Destructs a Theory.  This implementation does nothing, but we
 288    * need a virtual destructor for safety in case subclasses have a
 289    * destructor.
 290    */
 291   virtual ~Theory() {
 292   }
 293
 294   /**
 295    * Subclasses of Theory may add additional efforts.  DO NOT CHECK
 296    * equality with one of these values (e.g. if STANDARD xxx) but
 297    * rather use range checks (or use the helper functions below).
 298    * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
 299    * with FULL_EFFORT.
 300    */
 301   enum Effort {
 302     /**
 303      * Standard effort where theory need not do anything
 304      */
 305     EFFORT_STANDARD = 50,
 306     /**
 307      * Full effort requires the theory make sure its assertions are satisfiable or not
 308      */
 309     EFFORT_FULL = 100,
 310     /**
 311      * Combination effort means that the individual theories are already satisfied, and
 312      * it is time to put some effort into propagation of shared term equalities
 313      */
 314     EFFORT_COMBINATION = 150
 315   };/* enum Effort */
 316
 317   static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION
 318     { return e >= EFFORT_STANDARD; }
 319   static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION
 320     { return e >= EFFORT_STANDARD && e <  EFFORT_FULL; }
 321   static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION
 322     { return e == EFFORT_FULL; }
 323   static inline bool combination(Effort e) CVC4_CONST_FUNCTION
 324     { return e == EFFORT_COMBINATION; }
 325
 326   /**
 327    * Get the id for this Theory.
 328    */
 329   TheoryId getId() const {
 330     return d_id;
 331   }
 332
 333   /**
 334    * Get the context associated to this Theory.
 335    */
 336   context::Context* getContext() const {
 337     return d_context;
 338   }
 339
 340   /**
 341    * Get the context associated to this Theory.
 342    */
 343   context::UserContext* getUserContext() const {
 344     return d_userContext;
 345   }
 346
 347   /**
 348    * Set the output channel associated to this theory.
 349    */
 350   void setOutputChannel(OutputChannel& out) {
 351     d_out = &out;
 352   }
 353
 354   /**
 355    * Get the output channel associated to this theory.
 356    */
 357   OutputChannel& getOutputChannel() {
 358     return *d_out;
 359   }
 360
 361   /**
 362    * Pre-register a term.  Done one time for a Node, ever.
 363    */
 364   virtual void preRegisterTerm(TNode) { }
 365
 366   /**
 367    * Assert a fact in the current context.
 368    */
 369   void assertFact(TNode assertion, bool isPreregistered) {
 370     Trace("theory") << "Theory<" << getId() << ">::assertFact[" << d_context->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl;
 371     d_facts.push_back(Assertion(assertion, isPreregistered));
 372   }
 373
 374   /**
 375    * This method is called to notify a theory that the node n should
 376    * be considered a "shared term" by this theory
 377    */
 378   virtual void addSharedTerm(TNode n) { }
 379
 380   /**
 381    * The function should compute the care graph over the shared terms.
 382    * The default function returns all the pairs among the shared variables.
 383    */
 384   virtual void computeCareGraph(CareGraph& careGraph);
 385
 386   /**
 387    * Return the status of two terms in the current context. Should be implemented in
 388    * sub-theories to enable more efficient theory-combination.
 389    */
 390   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; }
 391
 392   /**
 393    * This method is called by the shared term manager when a shared
 394    * term lhs which this theory cares about (either because it
 395    * received a previous addSharedTerm call with lhs or because it
 396    * received a previous notifyEq call with lhs as the second
 397    * argument) becomes equal to another shared term rhs.  This call
 398    * also serves as notice to the theory that the shared term manager
 399    * now considers rhs the representative for this equivalence class
 400    * of shared terms, so future notifications for this class will be
 401    * based on rhs not lhs.
 402    */
 403   virtual void notifyEq(TNode lhs, TNode rhs) { }
 404
 405   /**
 406    * Check the current assignment's consistency.
 407    *
 408    * An implementation of check() is required to either:
 409    * - return a conflict on the output channel,
 410    * - be interrupted,
 411    * - throw an exception
 412    * - or call get() until done() is true.
 413    */
 414   virtual void check(Effort level = EFFORT_FULL) { }
 415
 416   /**
 417    * T-propagate new literal assignments in the current context.
 418    */
 419   virtual void propagate(Effort level = EFFORT_FULL) { }
 420
 421   /**
 422    * Return an explanation for the literal represented by parameter n
 423    * (which was previously propagated by this theory).
 424    */
 425   virtual Node explain(TNode n) {
 426     Unimplemented("Theory %s propagated a node but doesn't implement the "
 427                   "Theory::explain() interface!", identify().c_str());
 428   }
 429
 430   /**
 431    * Return the value of a node (typically used after a ).  If the
 432    * theory supports model generation but has no value for this node,
 433    * it should return Node::null().  If the theory doesn't support
 434    * model generation at all, or usually would but doesn't in its
 435    * current state, it should throw an exception saying so.
 436    *
 437    * The TheoryEngine is passed in so that you can recursively request
 438    * values for the Node's children.  This is important because the
 439    * TheoryEngine takes care of simple cases (metakind CONSTANT,
 440    * Boolean-valued VARIABLES, ...) and can dispatch to other theories
 441    * if that's necessary.  Only call your own getValue() recursively
 442    * if you *know* that you are responsible handle the Node you're
 443    * asking for; other theories can use your types, so be careful
 444    * here!  To be safe, it's best to delegate back to the
 445    * TheoryEngine (by way of the Valuation proxy object, which avoids
 446    * direct dependence on TheoryEngine).
 447    *
 448    * Usually, you need to handle at least the two cases of EQUAL and
 449    * VARIABLE---EQUAL in case a value of yours is on the LHS of an
 450    * EQUAL, and VARIABLE for variables of your types.  You also need
 451    * to support any operators that can survive your rewriter.  You
 452    * don't need to handle constants, as they are handled by the
 453    * TheoryEngine.
 454    *
 455    * There are some gotchas here.  The user may be requesting the
 456    * value of an expression that wasn't part of the satisfiable
 457    * assertion, or has been declared since.  If you don't have a value
 458    * and suspect this situation is the case, return Node::null()
 459    * rather than throwing an exception.
 460    */
 461   virtual Node getValue(TNode n) {
 462     Unimplemented("Theory %s doesn't support Theory::getValue interface",
 463                   identify().c_str());
 464     return Node::null();
 465   }
 466
 467   /**
 468    * Statically learn from assertion "in," which has been asserted
 469    * true at the top level.  The theory should only add (via
 470    * ::operator<< or ::append()) to the "learned" builder---it should
 471    * *never* clear it.  It is a conjunction to add to the formula at
 472    * the top-level and may contain other theories' contributions.
 473    */
 474   virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned) { }
 475
 476   enum PPAssertStatus {
 477     /** Atom has been solved  */
 478     PP_ASSERT_STATUS_SOLVED,
 479     /** Atom has not been solved */
 480     PP_ASSERT_STATUS_UNSOLVED,
 481     /** Atom is inconsistent */
 482     PP_ASSERT_STATUS_CONFLICT
 483   };
 484
 485   /**
 486    * Given a literal, add the solved substitutions to the map, if any.
 487    * The method should return true if the literal can be safely removed.
 488    */
 489   virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
 490     if (in.getKind() == kind::EQUAL) {
 491       if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
 492         outSubstitutions.addSubstitution(in[0], in[1]);
 493         return PP_ASSERT_STATUS_SOLVED;
 494       }
 495       if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
 496         outSubstitutions.addSubstitution(in[1], in[0]);
 497         return PP_ASSERT_STATUS_SOLVED;
 498       }
 499       if (in[0].getMetaKind() == kind::metakind::CONSTANT && in[1].getMetaKind() == kind::metakind::CONSTANT) {
 500         if (in[0] != in[1]) {
 501           return PP_ASSERT_STATUS_CONFLICT;
 502         }
 503       }
 504     }
 505
 506     return PP_ASSERT_STATUS_UNSOLVED;
 507   }
 508
 509   /**
 510    * Given an atom of the theory coming from the input formula, this
 511    * method can be overridden in a theory implementation to rewrite
 512    * the atom into an equivalent form.  This is only called just
 513    * before an input atom to the engine.
 514    */
 515   virtual Node ppRewrite(TNode atom) { return atom; }
 516
 517   /**
 518    * A Theory is called with presolve exactly one time per user
 519    * check-sat.  presolve() is called after preregistration,
 520    * rewriting, and Boolean propagation, (other theories'
 521    * propagation?), but the notified Theory has not yet had its
 522    * check() or propagate() method called.  A Theory may empty its
 523    * assertFact() queue using get().  A Theory can raise conflicts,
 524    * add lemmas, and propagate literals during presolve().
 525    */
 526   virtual void presolve() { }
 527
 528   /**
 529    * A Theory is called with postsolve exactly one time per user
 530    * check-sat.  postsolve() is called after the query has completed
 531    * (regardless of whether sat, unsat, or unknown), and after any
 532    * model-querying related to the query has been performed.
 533    * After this call, the theory will not get another check() or
 534    * propagate() call until presolve() is called again.  A Theory
 535    * cannot raise conflicts, add lemmas, or propagate literals during
 536    * postsolve().
 537    */
 538   virtual void postsolve() { }
 539
 540   /**
 541    * Notification sent to the theory wheneven the search restarts.
 542    * Serves as a good time to do some clean-up work, and you can
 543    * assume you're at DL 0 for the purposes of Contexts.  This function
 544    * should not use the output channel.
 545    */
 546   virtual void notifyRestart() { }
 547
 548   /**
 549    * Identify this theory (for debugging, dynamic configuration,
 550    * etc..)
 551    */
 552   virtual std::string identify() const = 0;
 553
 554   /** A set of theories */
 555   typedef uint32_t Set;
 556
 557   /** A set of all theories */
 558   static const Set AllTheories = (1 << theory::THEORY_LAST) - 1;
 559
 560   /** Add the theory to the set. If no set specified, just returns a singleton set */
 561   static inline Set setInsert(TheoryId theory, Set set = 0) {
 562     return set | (1 << theory);
 563   }
 564
 565   /** Check if the set contains the theory */
 566   static inline bool setContains(TheoryId theory, Set set) {
 567     return set & (1 << theory);
 568   }
 569
 570   static inline Set setComplement(Set a) {
 571     return (~a) & AllTheories;
 572   }
 573
 574   static inline Set setIntersection(Set a, Set b) {
 575     return a & b;
 576   }
 577
 578   static inline Set setUnion(Set a, Set b) {
 579     return a | b;
 580   }
 581
 582   /** a - b  */
 583   static inline Set setDifference(Set a, Set b) {
 584     return ((~b) & AllTheories) & a;
 585   }
 586
 587   static inline std::string setToString(theory::Theory::Set theorySet) {
 588     std::stringstream ss;
 589     ss << "[";
 590     for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
 591       if (theory::Theory::setContains((theory::TheoryId)theoryId, theorySet)) {
 592         ss << (theory::TheoryId) theoryId << " ";
 593       }
 594     }
 595     ss << "]";
 596     return ss.str();
 597   }
 598
 599   /**
 600    * Provides access to the facts queue, primarily intended for theory
 601    * debugging purposes.
 602    *
 603    * @return the iterator to the beginning of the fact queue
 604    */
 605   context::CDList<Assertion>::const_iterator facts_begin() const {
 606     return d_facts.begin();
 607   }
 608
 609   /**
 610    * Provides access to the facts queue, primarily intended for theory
 611    * debugging purposes.
 612    *
 613    * @return the iterator to the end of the fact queue
 614    */
 615   context::CDList<Assertion>::const_iterator facts_end() const {
 616     return d_facts.end();
 617   }
 618
 619   /**
 620    * Provides access to the shared terms, primarily intended for theory
 621    * debugging purposes.
 622    *
 623    * @return the iterator to the beginning of the shared terms list
 624    */
 625   context::CDList<TNode>::const_iterator shared_terms_begin() const {
 626     return d_sharedTerms.begin();
 627   }
 628
 629   /**
 630    * Provides access to the facts queue, primarily intended for theory
 631    * debugging purposes.
 632    *
 633    * @return the iterator to the end of the shared terms list
 634    */
 635   context::CDList<TNode>::const_iterator shared_terms_end() const {
 636     return d_sharedTerms.end();
 637   }
 638
 639 };/* class Theory */
 640
 641 std::ostream& operator<<(std::ostream& os, Theory::Effort level);
 642
 643 }/* CVC4::theory namespace */
 644
 645 inline std::ostream& operator<<(std::ostream& out,
 646                                 const CVC4::theory::Theory& theory) {
 647   return out << theory.identify();
 648 }
 649
 650 inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertStatus status) {
 651   switch (status) {
 652   case theory::Theory::PP_ASSERT_STATUS_SOLVED:
 653     out << "SOLVE_STATUS_SOLVED"; break;
 654   case theory::Theory::PP_ASSERT_STATUS_UNSOLVED:
 655     out << "SOLVE_STATUS_UNSOLVED"; break;
 656   case theory::Theory::PP_ASSERT_STATUS_CONFLICT:
 657     out << "SOLVE_STATUS_CONFLICT"; break;
 658   default:
 659     Unhandled();
 660   }
 661   return out;
 662 }
 663
 664 }/* CVC4 namespace */
 665
 666 #endif /* __CVC4__THEORY__THEORY_H */