Fix and reenable fact vs lemma optimization in datatypes (#5614)

This corrects an issue where terms internal to datatypes were not getting properly registered e.g. as part of the indices that determine the care graph, due to a context-independent cache being used (when a SAT-context-dependent one was required).

This reenables the fact vs lemma optimization in datatypes, as it is conjectured to be correct.

2 files changed, 14 insertions, 27 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index ff36216c2..010543725 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1504,26 +1504,18 @@ void TheoryDatatypes::collectTerms( Node n ) {
 
 Node TheoryDatatypes::getInstantiateCons(Node n, const DType& dt, int index)
 {
-  std::map< int, Node >::iterator it = d_inst_map[n].find( index );
-  if( it!=d_inst_map[n].end() ){
-    return it->second;
-  }else{
-    Node n_ic;
-    if( n.getKind()==APPLY_CONSTRUCTOR && n.getNumChildren()==0 ){
-      n_ic = n;
-    }else{
-      //add constructor to equivalence class
-      Node k = getTermSkolemFor( n );
-      n_ic = utils::getInstCons(k, dt, index);
-      //Assert( n_ic==Rewriter::rewrite( n_ic ) );
-      n_ic = Rewriter::rewrite( n_ic );
-      collectTerms( n_ic );
-      d_equalityEngine->addTerm(n_ic);
-      Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
-    }
-    d_inst_map[n][index] = n_ic;
-    return n_ic;
+  if( n.getKind()==APPLY_CONSTRUCTOR && n.getNumChildren()==0 ){
+    return n;
   }
+  //add constructor to equivalence class
+  Node k = getTermSkolemFor( n );
+  Node n_ic = utils::getInstCons(k, dt, index);
+  n_ic = Rewriter::rewrite( n_ic );
+  // it may be a new term, so we collect terms and add it to the equality engine
+  collectTerms( n_ic );
+  d_equalityEngine->addTerm(n_ic);
+  Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
+  return n_ic;
 }
 
 void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
@@ -1558,18 +1550,15 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
   }
   eq = tt.eqNode(tt_cons);
   // Determine if the equality must be sent out as a lemma. Notice that
-  // we could potentially keep new equalities from the instantiate rule internal
+  // we  keep new equalities from the instantiate rule internal
   // as long as they are for datatype constructors that have no arguments that
-  // have finite external type, which would correspond to:
+  // have finite external type, which corresponds to:
   //   forceLemma = dt[index].hasFiniteExternalArgType(ttn);
   // Such equalities must be sent because they introduce selector terms that
   // may contribute to conflicts due to cardinality (good examples of this are
   // regress0/datatypes/dt-param-card4-bool-sat.smt2 and
   // regress0/datatypes/list-bool.smt2).
-  // For now, to be conservative, we always send lemmas out, since otherwise
-  // we may encounter conflicts during model building when datatypes adds its
-  // equality engine to the theory model.
-  bool forceLemma = true;
+  bool forceLemma = dt[index].hasFiniteExternalArgType(ttn);
   Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq
                                  << " forceLemma = " << forceLemma << std::endl;
   d_im.addPendingInference(eq, exp, forceLemma, InferId::INST);
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 5bff5d305..8d7f7b52f 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -104,8 +104,6 @@ private:
 private:
   /** information necessary for equivalence classes */
   std::map< Node, EqcInfo* > d_eqc_info;
-  /** map from nodes to their instantiated equivalent for each constructor type */
-  std::map< Node, std::map< int, Node > > d_inst_map;
   //---------------------------------labels
   /** labels for each equivalence class
    *