From 01a9d18f2b2ce20cf7a0672a865cf0c2873d6f6a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 20 Aug 2020 15:50:38 -0500
Subject: [PATCH] Add TheoryState objects to each Theory (#4920)

This initializes all theories with a TheoryState object (apart from bool and builtin which do not require one).

Two additional theories are known to require special state objects: TheoryArith, which has a custom way of detecting when in conflict, and TheoryQuantifiers, which can leverage a special state object for the purposes of refactoring and splitting apart QuantifiersEngine further. All other theories use default TheoryState objects.

Notice this PR does not update the theories to use these states yet, it simply adds the objects.
---
 src/CMakeLists.txt                            |  4 ++
 src/theory/arith/arith_state.cpp              | 38 +++++++++++++
 src/theory/arith/arith_state.h                | 57 +++++++++++++++++++
 src/theory/arith/theory_arith.cpp             |  6 +-
 src/theory/arith/theory_arith.h               |  7 ++-
 src/theory/arith/theory_arith_private.h       | 15 +++--
 src/theory/arrays/theory_arrays.cpp           |  5 +-
 src/theory/arrays/theory_arrays.h             |  2 +
 src/theory/bv/theory_bv.cpp                   |  6 +-
 src/theory/bv/theory_bv.h                     |  2 +
 src/theory/datatypes/theory_datatypes.cpp     |  6 +-
 src/theory/datatypes/theory_datatypes.h       |  2 +
 src/theory/fp/theory_fp.cpp                   |  5 +-
 src/theory/fp/theory_fp.h                     |  2 +
 src/theory/quantifiers/quantifiers_state.cpp  | 30 ++++++++++
 src/theory/quantifiers/quantifiers_state.h    | 40 +++++++++++++
 src/theory/quantifiers/theory_quantifiers.cpp |  5 +-
 src/theory/quantifiers/theory_quantifiers.h   |  4 +-
 src/theory/sep/theory_sep.cpp                 |  6 +-
 src/theory/sep/theory_sep.h                   |  2 +
 src/theory/uf/theory_uf.cpp                   |  5 +-
 src/theory/uf/theory_uf.h                     |  2 +
 22 files changed, 234 insertions(+), 17 deletions(-)
 create mode 100644 src/theory/arith/arith_state.cpp
 create mode 100644 src/theory/arith/arith_state.h
 create mode 100644 src/theory/quantifiers/quantifiers_state.cpp
 create mode 100644 src/theory/quantifiers/quantifiers_state.h

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index f1e01a7cb..f9d7f833e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -292,6 +292,8 @@ libcvc4_add_sources(
   theory/arith/arith_msum.h
   theory/arith/arith_rewriter.cpp
   theory/arith/arith_rewriter.h
+  theory/arith/arith_state.cpp
+  theory/arith/arith_state.h
   theory/arith/arith_static_learner.cpp
   theory/arith/arith_static_learner.h
   theory/arith/arith_utilities.cpp
@@ -604,6 +606,8 @@ libcvc4_add_sources(
   theory/quantifiers/quantifiers_attributes.h
   theory/quantifiers/quantifiers_rewriter.cpp
   theory/quantifiers/quantifiers_rewriter.h
+  theory/quantifiers/quantifiers_state.cpp
+  theory/quantifiers/quantifiers_state.h
   theory/quantifiers/query_generator.cpp
   theory/quantifiers/query_generator.h
   theory/quantifiers/relevant_domain.cpp
diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp
new file mode 100644
index 000000000..c4678fab1
--- /dev/null
+++ b/src/theory/arith/arith_state.cpp
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file arith_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 Arithmetic theory state.
+ **/
+
+#include "theory/arith/arith_state.h"
+
+#include "theory/arith/theory_arith_private.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+ArithState::ArithState(TheoryArithPrivate& parent,
+                       context::Context* c,
+                       context::UserContext* u,
+                       Valuation val)
+    : TheoryState(c, u, val), d_parent(parent)
+{
+}
+
+bool ArithState::isInConflict() const
+{
+  return d_parent.anyConflict() || d_conflict;
+}
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h
new file mode 100644
index 000000000..5d775755b
--- /dev/null
+++ b/src/theory/arith/arith_state.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file arith_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 Arithmetic theory state.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__ARITH_STATE_H
+#define CVC4__THEORY__ARITH__ARITH_STATE_H
+
+#include "theory/theory_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class TheoryArithPrivate;
+
+/**
+ * The arithmetic state.
+ *
+ * Note this object is intended to use TheoryArithPrivate
+ * as a black box, and moreover the internals of TheoryArithPrivate will not
+ * be refactored to use this state. Instead, the main theory solver TheoryArith
+ * will be refactored to be a standard layer on top of TheoryArithPrivate,
+ * which will include using this state in the standard way.
+ */
+class ArithState : public TheoryState
+{
+ public:
+  ArithState(TheoryArithPrivate& parent,
+             context::Context* c,
+             context::UserContext* u,
+             Valuation val);
+  ~ArithState() {}
+  /** Are we currently in conflict? */
+  bool isInConflict() const override;
+
+ private:
+  /** reference to parent */
+  TheoryArithPrivate& d_parent;
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index b95b5e243..4e0582f50 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -41,9 +41,13 @@ TheoryArith::TheoryArith(context::Context* c,
       d_internal(
           new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
       d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
-      d_proofRecorder(nullptr)
+      d_proofRecorder(nullptr),
+      d_astate(*d_internal, c, u, valuation)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
+
+  // indicate we are using the theory state object
+  d_theoryState = &d_astate;
 }
 
 TheoryArith::~TheoryArith(){
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index ad3b91b07..d0147fe9f 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -17,11 +17,11 @@
 
 #pragma once
 
-#include "theory/theory.h"
 #include "expr/node.h"
 #include "proof/arith_proof_recorder.h"
+#include "theory/arith/arith_state.h"
 #include "theory/arith/theory_arith_private_forward.h"
-
+#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -115,6 +115,9 @@ class TheoryArith : public Theory {
     d_proofRecorder = proofRecorder;
   }
 
+ private:
+  /** The state object wrapping TheoryArithPrivate  */
+  ArithState d_astate;
 };/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 4c4aedf00..d96b5e2d3 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -324,17 +324,20 @@ public:
   /** This is a conflict that is magically known to hold. */
   void raiseBlackBoxConflict(Node bb);
 
-private:
+  /**
+   * Returns true iff a conflict has been raised. This method is public since
+   * it is needed by the ArithState class to know whether we are in conflict.
+   */
+  bool anyConflict() const
+  {
+    return !conflictQueueEmpty() || !d_blackBoxConflict.get().isNull();
+  }
 
+ private:
   inline bool conflictQueueEmpty() const {
     return d_conflicts.empty();
   }
 
-  /** Returns true iff a conflict has been raised. */
-  inline bool anyConflict() const {
-    return !conflictQueueEmpty() || !d_blackBoxConflict.get().isNull();
-  }
-
   /**
    * Outputs the contents of d_conflicts onto d_out.
    * The conditions of anyConflict() must hold.
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 4cc51a87e..9c1e22940 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -82,7 +82,7 @@ TheoryArrays::TheoryArrays(context::Context* c,
           name + "theory::arrays::number of setModelVal conflicts", 0),
       d_ppEqualityEngine(u, name + "theory::arrays::pp", true),
       d_ppFacts(u),
-      //      d_ppCache(u),
+      d_state(c, u, valuation),
       d_literalsToPropagate(c),
       d_literalsToPropagateIndex(c, 0),
       d_isPreRegistered(c),
@@ -132,6 +132,9 @@ TheoryArrays::TheoryArrays(context::Context* c,
   // The preprocessing congruence kinds
   d_ppEqualityEngine.addFunctionKind(kind::SELECT);
   d_ppEqualityEngine.addFunctionKind(kind::STORE);
+
+  // indicate we are using the default theory state object
+  d_theoryState = &d_state;
 }
 
 TheoryArrays::~TheoryArrays() {
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index b69450ac4..2d09c55fe 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -194,6 +194,8 @@ class TheoryArrays : public Theory {
 
   /** The theory rewriter for this theory. */
   TheoryArraysRewriter d_rewriter;
+  /** A (default) theory state object */
+  TheoryState d_state;
 
  public:
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index ced320d92..2c095e198 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -74,7 +74,8 @@ TheoryBV::TheoryBV(context::Context* c,
       d_calledPreregister(false),
       d_needsLastCallCheck(false),
       d_extf_range_infer(u),
-      d_extf_collapse_infer(u)
+      d_extf_collapse_infer(u),
+      d_state(c, u, valuation)
 {
   d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
   d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
@@ -109,6 +110,9 @@ TheoryBV::TheoryBV(context::Context* c,
   }
   d_subtheories.emplace_back(bb_solver);
   d_subtheoryMap[SUB_BITBLAST] = bb_solver;
+
+  // indicate we are using the default theory state object
+  d_theoryState = &d_state;
 }
 
 TheoryBV::~TheoryBV() {}
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 0e8877359..11440cb81 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -275,6 +275,8 @@ class TheoryBV : public Theory {
 
   /** The theory rewriter for this theory. */
   TheoryBVRewriter d_rewriter;
+  /** A (default) theory state object */
+  TheoryState d_state;
 
   friend class LazyBitblaster;
   friend class TLazyBitblaster;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index ee750e646..08ec4322e 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -61,12 +61,16 @@ TheoryDatatypes::TheoryDatatypes(Context* c,
       d_functionTerms(c),
       d_singleton_eq(u),
       d_lemmas_produced_c(u),
-      d_sygusExtension(nullptr)
+      d_sygusExtension(nullptr),
+      d_state(c, u, valuation)
 {
 
   d_true = NodeManager::currentNM()->mkConst( true );
   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
   d_dtfCounter = 0;
+
+  // indicate we are using the default theory state object
+  d_theoryState = &d_state;
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 37848f10e..0465a7788 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -366,6 +366,8 @@ private:
 
   /** The theory rewriter for this theory. */
   DatatypesRewriter d_rewriter;
+  /** A (default) theory state object */
+  TheoryState d_state;
 };/* class TheoryDatatypes */
 
 }/* CVC4::theory::datatypes namespace */
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index ff0855889..82086aafe 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -119,8 +119,11 @@ TheoryFp::TheoryFp(context::Context* c,
       d_toRealMap(u),
       realToFloatMap(u),
       floatToRealMap(u),
-      abstractionMap(u)
+      abstractionMap(u),
+      d_state(c, u, valuation)
 {
+  // indicate we are using the default theory state object
+  d_theoryState = &d_state;
 } /* TheoryFp::TheoryFp() */
 
 TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; }
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 2584d574e..ad052f92a 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -153,6 +153,8 @@ class TheoryFp : public Theory {
 
   /** The theory rewriter for this theory. */
   TheoryFpRewriter d_rewriter;
+  /** A (default) theory state object */
+  TheoryState d_state;
 }; /* class TheoryFp */
 
 }  // namespace fp
diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
new file mode 100644
index 000000000..67fad6f64
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -0,0 +1,30 @@
+/*********************                                                        */
+/*! \file quantifiers_state.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Mathias Preiner
+ ** 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 Utility for quantifiers state
+ **/
+
+#include "theory/quantifiers/quantifiers_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QuantifiersState::QuantifiersState(context::Context* c,
+                                   context::UserContext* u,
+                                   Valuation val)
+    : TheoryState(c, u, val)
+{
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h
new file mode 100644
index 000000000..a6611e734
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_state.h
@@ -0,0 +1,40 @@
+/*********************                                                        */
+/*! \file quantifiers_state.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Mathias Preiner
+ ** 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 Utility for quantifiers state
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
+#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
+
+#include "theory/theory_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * The quantifiers state.
+ */
+class QuantifiersState : public TheoryState
+{
+ public:
+  QuantifiersState(context::Context* c, context::UserContext* u, Valuation val);
+  ~QuantifiersState() {}
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 04e83032b..261fd65e6 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -42,7 +42,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
                                      Valuation valuation,
                                      const LogicInfo& logicInfo,
                                      ProofNodeManager* pnm)
-    : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm)
+    : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm),
+      d_qstate(c, u, valuation)
 {
   out.handleUserAttribute( "fun-def", this );
   out.handleUserAttribute( "sygus", this );
@@ -59,6 +60,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
     // add the proof rules
     d_qChecker.registerTo(pc);
   }
+  // indicate we are using the quantifiers theory state object
+  d_theoryState = &d_qstate;
 }
 
 TheoryQuantifiers::~TheoryQuantifiers() {
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index c378f3537..6f8256c21 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -24,9 +24,9 @@
 #include "theory/output_channel.h"
 #include "theory/quantifiers/proof_checker.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/theory.h"
 #include "theory/valuation.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -69,6 +69,8 @@ class TheoryQuantifiers : public Theory {
   QuantifiersRewriter d_rewriter;
   /** The proof rule checker */
   QuantifiersProofRuleChecker d_qChecker;
+  /** The quantifiers state */
+  QuantifiersState d_qstate;
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index edb5dd0ae..f75eb4472 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -47,6 +47,8 @@ TheorySep::TheorySep(context::Context* c,
                      ProofNodeManager* pnm)
     : Theory(THEORY_SEP, c, u, out, valuation, logicInfo, pnm),
       d_lemmas_produced_c(u),
+      d_bounds_init(false),
+      d_state(c, u, valuation),
       d_notify(*this),
       d_conflict(c, false),
       d_reduce(u),
@@ -56,7 +58,9 @@ TheorySep::TheorySep(context::Context* c,
 {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
-  d_bounds_init = false;
+
+  // indicate we are using the default theory state object
+  d_theoryState = &d_state;
 }
 
 TheorySep::~TheorySep() {
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 40182fc19..b178b97db 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -58,6 +58,8 @@ class TheorySep : public Theory {
   bool d_bounds_init;
 
   TheorySepRewriter d_rewriter;
+  /** A (default) theory state object */
+  TheoryState d_state;
 
   Node mkAnd( std::vector< TNode >& assumptions );
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 7bca9da74..c8ae3d844 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -56,7 +56,8 @@ TheoryUF::TheoryUF(context::Context* c,
       d_ho(nullptr),
       d_conflict(c, false),
       d_functionsTerms(c),
-      d_symb(u, instanceName)
+      d_symb(u, instanceName),
+      d_state(c, u, valuation)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
 
@@ -65,6 +66,8 @@ TheoryUF::TheoryUF(context::Context* c,
   {
     d_ufProofChecker.registerTo(pc);
   }
+  // indicate we are using the default theory state object
+  d_theoryState = &d_state;
 }
 
 TheoryUF::~TheoryUF() {
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 414a2dd6a..4d0a3126f 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -219,6 +219,8 @@ private:
   TheoryUfRewriter d_rewriter;
   /** Proof rule checker */
   UfProofRuleChecker d_ufProofChecker;
+  /** A (default) theory state object */
+  TheoryState d_state;
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */
-- 
2.30.2