From cbd86eb4ed8bafc17f28244b746a376a019462f1 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 6 Nov 2019 17:12:29 -0600
Subject: Move more string utility functions (#3398)

This is work towards splitting a "core solver" object from TheoryStrings.

This moves global functions from TheoryStrings to InferenceManager/SolverState, making them accessible in the future by modules that have references to these objects.

It also corrects an issue where we were maintaining two `d_conflict` fields.
---
 src/theory/strings/solver_state.h | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'src/theory/strings/solver_state.h')

diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index f14b4b4af..a2001bb3b 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -23,6 +23,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/valuation.h"
 
 namespace CVC4 {
 namespace theory {
@@ -87,7 +88,7 @@ class EqcInfo
 class SolverState
 {
  public:
-  SolverState(context::Context* c, eq::EqualityEngine& ee);
+  SolverState(context::Context* c, eq::EqualityEngine& ee, Valuation& v);
   ~SolverState();
   //-------------------------------------- equality information
   /**
@@ -166,12 +167,28 @@ class SolverState
    * for some eqc that is currently equal to z.
    */
   void addEndpointsToEqcInfo(Node t, Node concat, Node eqc);
+  /** Entailment check
+   *
+   * This calls entailmentCheck on the Valuation object of theory of strings.
+   */
+  std::pair<bool, Node> entailmentCheck(TheoryOfMode mode, TNode lit);
+  /** Separate by length
+   *
+   * Separate the string representatives in argument n into a partition cols
+   * whose collections have equal length. The i^th vector in cols has length
+   * lts[i] for all elements in col.
+   */
+  void separateByLength(const std::vector<Node>& n,
+                        std::vector<std::vector<Node> >& cols,
+                        std::vector<Node>& lts);
 
  private:
   /** Pointer to the SAT context object used by the theory of strings. */
   context::Context* d_context;
   /** Reference to equality engine of the theory of strings. */
   eq::EqualityEngine& d_ee;
+  /** Reference to the valuation of the theory of strings */
+  Valuation& d_valuation;
   /** Are we in conflict? */
   context::CDO<bool> d_conflict;
   /** The pending conflict if one exists */
-- 
cgit v1.2.3