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, 94 insertions, 0 deletions

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 */