1 files changed, 38 insertions, 1 deletions
diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp
index 65ff4cde4..672ca8b76 100644
--- a/src/theory/strings/array_solver.cpp
+++ b/src/theory/strings/array_solver.cpp
@@ -41,10 +41,11 @@ ArraySolver::ArraySolver(Env& env,
       d_termReg(tr),
       d_csolver(cs),
       d_esolver(es),
+      d_coreSolver(env, s, im, tr, cs, es, extt),
       d_eqProc(context())
 {
   NodeManager* nm = NodeManager::currentNM();
-  d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+  d_zero = nm->mkConstInt(Rational(0));
 }
 
 ArraySolver::~ArraySolver() {}
@@ -63,6 +64,32 @@ void ArraySolver::checkArrayConcat()
   checkTerms(SEQ_NTH);
 }
 
+void ArraySolver::checkArray()
+{
+  if (!d_termReg.hasSeqUpdate())
+  {
+    Trace("seq-array") << "No seq.update/seq.nth terms, skipping check..."
+                       << std::endl;
+    return;
+  }
+  Trace("seq-array") << "ArraySolver::checkArray..." << std::endl;
+  d_coreSolver.check(d_currTerms[SEQ_NTH], d_currTerms[STRING_UPDATE]);
+}
+
+void ArraySolver::checkArrayEager()
+{
+  if (!d_termReg.hasSeqUpdate())
+  {
+    Trace("seq-array") << "No seq.update/seq.nth terms, skipping check..."
+                       << std::endl;
+    return;
+  }
+  Trace("seq-array") << "ArraySolver::checkArray..." << std::endl;
+  std::vector<Node> nthTerms = d_esolver.getActive(SEQ_NTH);
+  std::vector<Node> updateTerms = d_esolver.getActive(STRING_UPDATE);
+  d_coreSolver.check(nthTerms, updateTerms);
+}
+
 void ArraySolver::checkTerms(Kind k)
 {
   Assert(k == STRING_UPDATE || k == SEQ_NTH);
@@ -271,6 +298,16 @@ void ArraySolver::checkTerms(Kind k)
   }
 }
 
+const std::map<Node, Node>& ArraySolver::getWriteModel(Node eqc)
+{
+  return d_coreSolver.getWriteModel(eqc);
+}
+
+const std::map<Node, Node>& ArraySolver::getConnectedSequences()
+{
+  return d_coreSolver.getConnectedSequences();
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace cvc5