1 files changed, 32 insertions, 3 deletions
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index f0b4a74c6..d0589be90 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -19,10 +19,13 @@
 
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
+#include "expr/proof_node_manager.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/output_channel.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/sequences_stats.h"
 #include "theory/strings/skolem_cache.h"
+#include "theory/strings/solver_state.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
@@ -46,12 +49,34 @@ class TermRegistry
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
  public:
-  TermRegistry(context::Context* c,
-               context::UserContext* u,
+  TermRegistry(SolverState& s,
                eq::EqualityEngine& ee,
                OutputChannel& out,
-               SequencesStatistics& statistics);
+               SequencesStatistics& statistics,
+               ProofNodeManager* pnm);
   ~TermRegistry();
+  /** The eager reduce routine
+   *
+   * Constructs a lemma for t that is incomplete, but communicates pertinent
+   * information about t. This is analogous to StringsPreprocess::reduce.
+   *
+   * In practice, we send this lemma eagerly, as soon as t is registered.
+   *
+   * @param t The node to reduce,
+   * @param sc The Skolem cache to use for new variables,
+   * @return The eager reduction for t.
+   */
+  static Node eagerReduce(Node t, SkolemCache* sc);
+  /**
+   * Returns a lemma indicating that the length of a term t whose type is
+   * string-like has positive length. The exact form of this lemma depends
+   * on what works best in practice, currently:
+   *   (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
+   *
+   * @param t The node to reduce,
+   * @return The positive length lemma for t.
+   */
+  static Node lengthPositive(Node t);
   /**
    * Preregister term, called when TheoryStrings::preRegisterTerm(n) is called.
    * This does the following:
@@ -184,6 +209,8 @@ class TermRegistry
   Node d_negOne;
   /** the cardinality of the alphabet */
   uint32_t d_cardSize;
+  /** Reference to the solver state of the theory of strings. */
+  SolverState& d_state;
   /** Reference to equality engine of the theory of strings. */
   eq::EqualityEngine& d_ee;
   /** Reference to the output channel of the theory of strings. */
@@ -224,6 +251,8 @@ class TermRegistry
   NodeNodeMap d_proxyVarToLength;
   /** List of terms that we have register length for */
   NodeSet d_lengthLemmaTermsCache;
+  /** Proof generator, manages proofs for lemmas generated by this class */
+  std::unique_ptr<EagerProofGenerator> d_epg;
   /** Register type
    *
    * Ensures the theory solver is setup to handle string-like type tn. In