Introduce the theory state object (#4910)

This will be used as a standard way of querying and tracking state information in a Theory. The TheoryState object has a standard role in a number of the new standard templates for Theory:: methods.

The theory state is a collection of 4 Theory members (SAT context, user context, valuation, equality engine), as well as a SAT-context dependent "conflict" flag that indicates whether we have sent a conflict in this SAT conflict. It contains (safe) versions of equality engine queries, which are highly common in many theory solvers.

The next step will be to have the SolverState objects in theory of sets and strings inherit from this class.

5 files changed, 232 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 10cf23fdf..48bd99f44 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -818,6 +818,8 @@ libcvc4_add_sources(
   theory/theory_rewriter.cpp
   theory/theory_rewriter.h
   theory/theory_registrar.h
+  theory/theory_state.cpp
+  theory/theory_state.h
   theory/theory_test_utils.h
   theory/trust_node.cpp
   theory/trust_node.h
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 02f84526f..9669d97e0 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -82,6 +82,7 @@ Theory::Theory(TheoryId id,
       d_valuation(valuation),
       d_equalityEngine(nullptr),
       d_allocEqualityEngine(nullptr),
+      d_theoryState(nullptr),
       d_proofsEnabled(false)
 {
   smtStatisticsRegistry()->registerStat(&d_checkTime);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 78c6e34cb..349f36a57 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -44,6 +44,7 @@
 #include "theory/output_channel.h"
 #include "theory/theory_id.h"
 #include "theory/theory_rewriter.h"
+#include "theory/theory_state.h"
 #include "theory/trust_node.h"
 #include "theory/valuation.h"
 #include "util/statistics_registry.h"
@@ -268,6 +269,11 @@ class Theory {
    */
   std::unique_ptr<eq::EqualityEngine> d_allocEqualityEngine;
   /**
+   * The theory state, which contains contexts, valuation, and equality engine.
+   * Notice the theory is responsible for memory management of this class.
+   */
+  TheoryState* d_theoryState;
+  /**
    * Whether proofs are enabled
    *
    */
diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
new file mode 100644
index 000000000..bc8e53245
--- /dev/null
+++ b/src/theory/theory_state.cpp
@@ -0,0 +1,129 @@
+/*********************                                                        */
+/*! \file theory_state.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A theory state for Theory
+ **/
+
+#include "theory/theory_state.h"
+
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+TheoryState::TheoryState(context::Context* c,
+                         context::UserContext* u,
+                         Valuation val)
+    : d_context(c),
+      d_ucontext(u),
+      d_valuation(val),
+      d_ee(nullptr),
+      d_conflict(c, false)
+{
+}
+
+void TheoryState::finishInit(eq::EqualityEngine* ee) { d_ee = ee; }
+
+context::Context* TheoryState::getSatContext() const { return d_context; }
+
+context::UserContext* TheoryState::getUserContext() const { return d_ucontext; }
+
+bool TheoryState::hasTerm(TNode a) const
+{
+  Assert(d_ee != nullptr);
+  return d_ee->hasTerm(a);
+}
+
+TNode TheoryState::getRepresentative(TNode t) const
+{
+  Assert(d_ee != nullptr);
+  if (d_ee->hasTerm(t))
+  {
+    return d_ee->getRepresentative(t);
+  }
+  return t;
+}
+
+bool TheoryState::areEqual(TNode a, TNode b) const
+{
+  Assert(d_ee != nullptr);
+  if (a == b)
+  {
+    return true;
+  }
+  else if (hasTerm(a) && hasTerm(b))
+  {
+    return d_ee->areEqual(a, b);
+  }
+  return false;
+}
+
+bool TheoryState::areDisequal(TNode a, TNode b) const
+{
+  Assert(d_ee != nullptr);
+  if (a == b)
+  {
+    return false;
+  }
+
+  bool isConst = true;
+  bool hasTerms = true;
+  if (hasTerm(a))
+  {
+    a = d_ee->getRepresentative(a);
+    isConst = a.isConst();
+  }
+  else if (!a.isConst())
+  {
+    // if not constant and not a term in the ee, it cannot be disequal
+    return false;
+  }
+  else
+  {
+    hasTerms = false;
+  }
+
+  if (hasTerm(b))
+  {
+    b = d_ee->getRepresentative(b);
+    isConst = isConst && b.isConst();
+  }
+  else if (!b.isConst())
+  {
+    // same as above, it cannot be disequal
+    return false;
+  }
+  else
+  {
+    hasTerms = false;
+  }
+
+  if (isConst)
+  {
+    // distinct constants are disequal
+    return a != b;
+  }
+  else if (!hasTerms)
+  {
+    return false;
+  }
+  // otherwise there may be an explicit disequality in the equality engine
+  return d_ee->areDisequal(a, b, false);
+}
+
+eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; }
+
+void TheoryState::notifyInConflict() { d_conflict = true; }
+
+bool TheoryState::isInConflict() const { return d_conflict; }
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
new file mode 100644
index 000000000..71197dddc
--- /dev/null
+++ b/src/theory/theory_state.h
@@ -0,0 +1,94 @@
+/*********************                                                        */
+/*! \file theory_state.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A theory state for Theory
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__THEORY_STATE_H
+#define CVC4__THEORY__THEORY_STATE_H
+
+#include "context/cdo.h"
+#include "expr/node.h"
+#include "theory/valuation.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace eq {
+class EqualityEngine;
+}
+
+class TheoryState
+{
+ public:
+  TheoryState(context::Context* c, context::UserContext* u, Valuation val);
+  virtual ~TheoryState() {}
+  /**
+   * Finish initialize, ee is a pointer to the official equality engine
+   * of theory.
+   */
+  virtual void finishInit(eq::EqualityEngine* ee);
+  /** Get the SAT context */
+  context::Context* getSatContext() const;
+  /** Get the user context */
+  context::UserContext* getUserContext() const;
+  //-------------------------------------- equality information
+  /** Is t registered as a term in the equality engine of this class? */
+  virtual bool hasTerm(TNode a) const;
+  /**
+   * Get the representative of t in the equality engine of this class, or t
+   * itself if it is not registered as a term.
+   */
+  virtual TNode getRepresentative(TNode t) const;
+  /**
+   * Are a and b equal according to the equality engine of this class? Also
+   * returns true if a and b are identical.
+   */
+  virtual bool areEqual(TNode a, TNode b) const;
+  /**
+   * Are a and b disequal according to the equality engine of this class? Also
+   * returns true if the representative of a and b are distinct constants.
+   */
+  virtual bool areDisequal(TNode a, TNode b) const;
+  /** get equality engine */
+  eq::EqualityEngine* getEqualityEngine() const;
+  //-------------------------------------- end equality information
+  /**
+   * Set that the current state of the solver is in conflict. This should be
+   * called immediately after a call to conflict(...) on the output channel of
+   * the theory.
+   */
+  virtual void notifyInConflict();
+  /** Are we currently in conflict? */
+  virtual bool isInConflict() const;
+
+ protected:
+  /** Pointer to the SAT context object used by the theory. */
+  context::Context* d_context;
+  /** Pointer to the user context object used by the theory. */
+  context::UserContext* d_ucontext;
+  /**
+   * The valuation proxy for the Theory to communicate back with the
+   * theory engine (and other theories).
+   */
+  Valuation d_valuation;
+  /** Pointer to equality engine of the theory. */
+  eq::EqualityEngine* d_ee;
+  /** Are we in conflict? */
+  context::CDO<bool> d_conflict;
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__SOLVER_STATE_H */