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.

1 files changed, 129 insertions, 0 deletions

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