Split strings finite model finding strategy (#3727)

5 files changed, 261 insertions, 121 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5bb239bd5..81328831a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -690,6 +690,8 @@ libcvc4_add_sources(
   theory/strings/skolem_cache.h
   theory/strings/solver_state.cpp
   theory/strings/solver_state.h
+  theory/strings/strings_fmf.cpp
+  theory/strings/strings_fmf.h
   theory/strings/theory_strings.cpp
   theory/strings/theory_strings.h
   theory/strings/theory_strings_preprocess.cpp
diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp
new file mode 100644
index 000000000..8ca6d2de1
--- /dev/null
+++ b/src/theory/strings/strings_fmf.cpp
@@ -0,0 +1,124 @@
+/*********************                                                        */
+/*! \file strings_fmf.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Implementation of a finite model finding decision strategy for
+ ** strings.
+ **/
+
+#include "theory/strings/strings_fmf.h"
+
+using namespace std;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+StringsFmf::StringsFmf(context::Context* c,
+                       context::UserContext* u,
+                       Valuation valuation,
+                       SkolemCache& skc)
+    : d_sslds(nullptr),
+      d_satContext(c),
+      d_userContext(u),
+      d_valuation(valuation),
+      d_skCache(skc),
+      d_inputVars(u)
+{
+}
+
+StringsFmf::~StringsFmf() {}
+
+void StringsFmf::preRegisterTerm(TNode n)
+{
+  if (!n.getType().isString())
+  {
+    return;
+  }
+  Kind k = n.getKind();
+  // Our decision strategy will minimize the length of this term if it is a
+  // variable but not an internally generated Skolem, or a term that does
+  // not belong to this theory.
+  if (n.isVar() ? !d_skCache.isSkolem(n) : kindToTheoryId(k) != THEORY_STRINGS)
+  {
+    d_inputVars.insert(n);
+    Trace("strings-dstrat-reg") << "input variable: " << n << std::endl;
+  }
+}
+
+void StringsFmf::presolve()
+{
+  d_sslds.reset(new StringSumLengthDecisionStrategy(
+      d_satContext, d_userContext, d_valuation));
+  Trace("strings-dstrat-reg")
+      << "presolve: register decision strategy." << std::endl;
+  std::vector<Node> inputVars;
+  for (NodeSet::const_iterator itr = d_inputVars.begin();
+       itr != d_inputVars.end();
+       ++itr)
+  {
+    inputVars.push_back(*itr);
+  }
+  d_sslds->initialize(inputVars);
+}
+
+DecisionStrategy* StringsFmf::getDecisionStrategy() const
+{
+  return d_sslds.get();
+}
+
+StringsFmf::StringSumLengthDecisionStrategy::StringSumLengthDecisionStrategy(
+    context::Context* c, context::UserContext* u, Valuation valuation)
+    : DecisionStrategyFmf(c, valuation), d_inputVarLsum(u)
+{
+}
+
+bool StringsFmf::StringSumLengthDecisionStrategy::isInitialized()
+{
+  return !d_inputVarLsum.get().isNull();
+}
+
+void StringsFmf::StringSumLengthDecisionStrategy::initialize(
+    const std::vector<Node>& vars)
+{
+  if (d_inputVarLsum.get().isNull() && !vars.empty())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    std::vector<Node> sum;
+    for (const Node& v : vars)
+    {
+      sum.push_back(nm->mkNode(STRING_LENGTH, v));
+    }
+    Node sumn = sum.size() == 1 ? sum[0] : nm->mkNode(PLUS, sum);
+    d_inputVarLsum.set(sumn);
+  }
+}
+
+Node StringsFmf::StringSumLengthDecisionStrategy::mkLiteral(unsigned i)
+{
+  if (d_inputVarLsum.get().isNull())
+  {
+    return Node::null();
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node lit = nm->mkNode(LEQ, d_inputVarLsum.get(), nm->mkConst(Rational(i)));
+  Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit << std::endl;
+  return lit;
+}
+std::string StringsFmf::StringSumLengthDecisionStrategy::identify() const
+{
+  return std::string("string_sum_len");
+}
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/strings/strings_fmf.h b/src/theory/strings/strings_fmf.h
new file mode 100644
index 000000000..375a100ff
--- /dev/null
+++ b/src/theory/strings/strings_fmf.h
@@ -0,0 +1,123 @@
+/*********************                                                        */
+/*! \file strings_fmf.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 finite model finding decision strategy for strings.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__STRINGS_FMF_H
+#define CVC4__THEORY__STRINGS__STRINGS_FMF_H
+
+#include "context/cdhashset.h"
+#include "context/cdo.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/decision_strategy.h"
+#include "theory/strings/skolem_cache.h"
+#include "theory/valuation.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+/** Strings finite model finding
+ *
+ * This class manages the creation of a decision strategy that bounds the
+ * sum of lengths of terms of type string.
+ */
+class StringsFmf
+{
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+  StringsFmf(context::Context* c,
+             context::UserContext* u,
+             Valuation valuation,
+             SkolemCache& skc);
+  ~StringsFmf();
+  /** preRegister term
+   *
+   * This determines if the term n should be added to d_inputVars, the set
+   * of terms of type string whose length we are minimizing with this decision
+   * strategy.
+   */
+  void preRegisterTerm(TNode n);
+  /** presolve
+   *
+   * This initializes a (new copy) of the decision strategy d_sslds.
+   */
+  void presolve();
+  /**
+   * Get the decision strategy, valid after a call to presolve in the duration
+   * of a check-sat call.
+   */
+  DecisionStrategy* getDecisionStrategy() const;
+
+ private:
+  /** String sum of lengths decision strategy
+   *
+   * This decision strategy enforces that len(x_1) + ... + len(x_k) <= n
+   * for a minimal natural number n, where x_1, ..., x_n is the list of
+   * input variables of the problem of type String.
+   *
+   * This decision strategy is enabled by option::stringsFmf().
+   */
+  class StringSumLengthDecisionStrategy : public DecisionStrategyFmf
+  {
+   public:
+    StringSumLengthDecisionStrategy(context::Context* c,
+                                    context::UserContext* u,
+                                    Valuation valuation);
+    /** make literal */
+    Node mkLiteral(unsigned i) override;
+    /** identify */
+    std::string identify() const override;
+    /** is initialized */
+    bool isInitialized();
+    /** initialize */
+    void initialize(const std::vector<Node>& vars);
+
+    /*
+     * Do not hide the zero-argument version of initialize() inherited from the
+     * base class
+     */
+    using DecisionStrategyFmf::initialize;
+
+   private:
+    /**
+     * User-context-dependent node corresponding to the sum of the lengths of
+     * input variables of type string
+     */
+    context::CDO<Node> d_inputVarLsum;
+  };
+  /** an instance of the above class */
+  std::unique_ptr<StringSumLengthDecisionStrategy> d_sslds;
+  /** The SAT search context for the theory of strings. */
+  context::Context* d_satContext;
+  /** The user level assertion context for the theory of strings. */
+  context::UserContext* d_userContext;
+  /** The valuation object */
+  Valuation d_valuation;
+  /** reference to the skolem cache */
+  SkolemCache& d_skCache;
+  /**
+   * The set of terms of type string whose length we are minimizing
+   * with this decision strategy.
+   */
+  NodeSet d_inputVars;
+};
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__STRINGS_FMF_H */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 33bde3162..197f7ac4c 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -84,11 +84,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_bsolver(c, u, d_state, d_im),
       d_csolver(c, u, d_state, d_im, d_sk_cache, d_bsolver),
       d_regexp_solver(*this, d_state, d_im, c, u),
-      d_input_vars(u),
-      d_input_var_lsum(u),
-      d_cardinality_lits(u),
-      d_curr_cardinality(c, 0),
-      d_sslds(nullptr),
+      d_stringsFmf(c, u, valuation, d_sk_cache),
       d_strategy_init(false)
 {
   setupExtTheory();
@@ -405,25 +401,15 @@ void TheoryStrings::presolve() {
   // if strings fmf is enabled, register the strategy
   if (options::stringFMF())
   {
-    d_sslds.reset(new StringSumLengthDecisionStrategy(
-        getSatContext(), getUserContext(), d_valuation));
-    Trace("strings-dstrat-reg")
-        << "presolve: register decision strategy." << std::endl;
-    std::vector<Node> inputVars;
-    for (NodeSet::const_iterator itr = d_input_vars.begin();
-         itr != d_input_vars.end();
-         ++itr)
-    {
-      inputVars.push_back(*itr);
-    }
-    d_sslds->initialize(inputVars);
+    d_stringsFmf.presolve();
     // This strategy is local to a check-sat call, since we refresh the strategy
     // on every call to presolve.
     getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_STRINGS_SUM_LENGTHS,
-        d_sslds.get(),
+        d_stringsFmf.getDecisionStrategy(),
         DecisionManager::STRAT_SCOPE_LOCAL_SOLVE);
   }
+  Debug("strings-presolve") << "Finished presolve" << std::endl;
 }
 
 
@@ -749,17 +735,6 @@ void TheoryStrings::preRegisterTerm(TNode n) {
               }
             }
           }
-          // if finite model finding is enabled,
-          // then we minimize the length of this term if it is a variable
-          // but not an internally generated Skolem, or a term that does
-          // not belong to this theory.
-          if (options::stringFMF()
-              && (n.isVar() ? !d_sk_cache.isSkolem(n)
-                            : kindToTheoryId(k) != THEORY_STRINGS))
-          {
-            d_input_vars.insert(n);
-            Trace("strings-dstrat-reg") << "input variable: " << n << std::endl;
-          }
           d_equalityEngine.addTerm(n);
         } else if (tn.isBoolean()) {
           // Get triggered for both equal and dis-equal
@@ -783,6 +758,11 @@ void TheoryStrings::preRegisterTerm(TNode n) {
         }
       }
     }
+    // register with finite model finding
+    if (options::stringFMF())
+    {
+      d_stringsFmf.preRegisterTerm(n);
+    }
   }
 }
 
@@ -1932,52 +1912,6 @@ void TheoryStrings::checkCardinality() {
   Trace("strings-card") << "...end check cardinality" << std::endl;
 }
 
-
-//// Finite Model Finding
-
-TheoryStrings::StringSumLengthDecisionStrategy::StringSumLengthDecisionStrategy(
-    context::Context* c, context::UserContext* u, Valuation valuation)
-    : DecisionStrategyFmf(c, valuation), d_input_var_lsum(u)
-{
-}
-
-bool TheoryStrings::StringSumLengthDecisionStrategy::isInitialized()
-{
-  return !d_input_var_lsum.get().isNull();
-}
-
-void TheoryStrings::StringSumLengthDecisionStrategy::initialize(
-    const std::vector<Node>& vars)
-{
-  if (d_input_var_lsum.get().isNull() && !vars.empty())
-  {
-    NodeManager* nm = NodeManager::currentNM();
-    std::vector<Node> sum;
-    for (const Node& v : vars)
-    {
-      sum.push_back(nm->mkNode(STRING_LENGTH, v));
-    }
-    Node sumn = sum.size() == 1 ? sum[0] : nm->mkNode(PLUS, sum);
-    d_input_var_lsum.set(sumn);
-  }
-}
-
-Node TheoryStrings::StringSumLengthDecisionStrategy::mkLiteral(unsigned i)
-{
-  if (d_input_var_lsum.get().isNull())
-  {
-    return Node::null();
-  }
-  NodeManager* nm = NodeManager::currentNM();
-  Node lit = nm->mkNode(LEQ, d_input_var_lsum.get(), nm->mkConst(Rational(i)));
-  Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit << std::endl;
-  return lit;
-}
-std::string TheoryStrings::StringSumLengthDecisionStrategy::identify() const
-{
-  return std::string("string_sum_len");
-}
-
 Node TheoryStrings::ppRewrite(TNode atom) {
   Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
   Node atomElim;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 5e00f9416..960d3ceaa 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -23,7 +23,6 @@
 #include "context/cdlist.h"
 #include "expr/attribute.h"
 #include "expr/node_trie.h"
-#include "theory/decision_manager.h"
 #include "theory/strings/base_solver.h"
 #include "theory/strings/core_solver.h"
 #include "theory/strings/infer_info.h"
@@ -34,6 +33,7 @@
 #include "theory/strings/regexp_solver.h"
 #include "theory/strings/skolem_cache.h"
 #include "theory/strings/solver_state.h"
+#include "theory/strings/strings_fmf.h"
 #include "theory/strings/theory_strings_preprocess.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -461,51 +461,8 @@ private:
   RegExpSolver d_regexp_solver;
   /** regular expression elimination module */
   RegExpElimination d_regexp_elim;
-
-  // Finite Model Finding
- private:
-  NodeSet d_input_vars;
-  context::CDO< Node > d_input_var_lsum;
-  context::CDHashMap< int, Node > d_cardinality_lits;
-  context::CDO< int > d_curr_cardinality;
-  /** String sum of lengths decision strategy
-   *
-   * This decision strategy enforces that len(x_1) + ... + len(x_k) <= n
-   * for a minimal natural number n, where x_1, ..., x_n is the list of
-   * input variables of the problem of type String.
-   *
-   * This decision strategy is enabled by option::stringsFmf().
-   */
-  class StringSumLengthDecisionStrategy : public DecisionStrategyFmf
-  {
-   public:
-    StringSumLengthDecisionStrategy(context::Context* c,
-                                    context::UserContext* u,
-                                    Valuation valuation);
-    /** make literal */
-    Node mkLiteral(unsigned i) override;
-    /** identify */
-    std::string identify() const override;
-    /** is initialized */
-    bool isInitialized();
-    /** initialize */
-    void initialize(const std::vector<Node>& vars);
-
-    /*
-     * Do not hide the zero-argument version of initialize() inherited from the
-     * base class
-     */
-    using DecisionStrategyFmf::initialize;
-
-   private:
-    /**
-     * User-context-dependent node corresponding to the sum of the lengths of
-     * input variables of type string
-     */
-    context::CDO<Node> d_input_var_lsum;
-  };
-  /** an instance of the above class */
-  std::unique_ptr<StringSumLengthDecisionStrategy> d_sslds;
+  /** Strings finite model finding decision strategy */
+  StringsFmf d_stringsFmf;
 
  public:
   // ppRewrite