src/theory/theory_state.h

   1 /*********************                                                        */
   2 /*! \file theory_state.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief A theory state for Theory
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__THEORY_STATE_H
  18 #define CVC4__THEORY__THEORY_STATE_H
  19
  20 #include "context/cdo.h"
  21 #include "expr/node.h"
  22 #include "theory/valuation.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 namespace eq {
  28 class EqualityEngine;
  29 }
  30
  31 class TheoryState
  32 {
  33  public:
  34   TheoryState(context::Context* c, context::UserContext* u, Valuation val);
  35   virtual ~TheoryState() {}
  36   /**
  37    * Set equality engine, where ee is a pointer to the official equality engine
  38    * of theory.
  39    */
  40   void setEqualityEngine(eq::EqualityEngine* ee);
  41   /** Get the SAT context */
  42   context::Context* getSatContext() const;
  43   /** Get the user context */
  44   context::UserContext* getUserContext() const;
  45   //-------------------------------------- equality information
  46   /** Is t registered as a term in the equality engine of this class? */
  47   virtual bool hasTerm(TNode a) const;
  48   /**
  49    * Get the representative of t in the equality engine of this class, or t
  50    * itself if it is not registered as a term.
  51    */
  52   virtual TNode getRepresentative(TNode t) const;
  53   /**
  54    * Are a and b equal according to the equality engine of this class? Also
  55    * returns true if a and b are identical.
  56    */
  57   virtual bool areEqual(TNode a, TNode b) const;
  58   /**
  59    * Are a and b disequal according to the equality engine of this class? Also
  60    * returns true if the representative of a and b are distinct constants.
  61    */
  62   virtual bool areDisequal(TNode a, TNode b) const;
  63   /** get list of members in the equivalence class of a */
  64   virtual void getEquivalenceClass(Node a, std::vector<Node>& eqc) const;
  65   /** get equality engine */
  66   eq::EqualityEngine* getEqualityEngine() const;
  67   //-------------------------------------- end equality information
  68   /**
  69    * Set that the current state of the solver is in conflict. This should be
  70    * called immediately after a call to conflict(...) on the output channel of
  71    * the theory.
  72    */
  73   virtual void notifyInConflict();
  74   /** Are we currently in conflict? */
  75   virtual bool isInConflict() const;
  76
  77   /** Returns true if lit is a SAT literal. */
  78   virtual bool isSatLiteral(TNode lit) const;
  79   /**
  80    * Returns pointer to model. This model is only valid during last call effort
  81    * check.
  82    */
  83   TheoryModel* getModel();
  84
  85   /** Returns true if n has a current SAT assignment and stores it in value. */
  86   virtual bool hasSatValue(TNode n, bool& value) const;
  87
  88   /** Get the underlying valuation class */
  89   Valuation& getValuation();
  90
  91  protected:
  92   /** Pointer to the SAT context object used by the theory. */
  93   context::Context* d_context;
  94   /** Pointer to the user context object used by the theory. */
  95   context::UserContext* d_ucontext;
  96   /**
  97    * The valuation proxy for the Theory to communicate back with the
  98    * theory engine (and other theories).
  99    */
 100   Valuation d_valuation;
 101   /** Pointer to equality engine of the theory. */
 102   eq::EqualityEngine* d_ee;
 103   /** Are we in conflict? */
 104   context::CDO<bool> d_conflict;
 105 };
 106
 107 }  // namespace theory
 108 }  // namespace CVC4
 109
 110 #endif /* CVC4__THEORY__SOLVER_STATE_H */