From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 7 Dec 2020 22:12:47 +0000 (-0600)
Subject: Fix and reenable fact vs lemma optimization in datatypes (#5614)
X-Git-Tag: cvc5-1.0.0~2488
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bbca987e023b2dbf386a62731b94e41c06f32526;p=cvc5.git

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.
---

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
    *
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d0e28f9e5..55fe30b14 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1589,6 +1589,7 @@ set(regress_1_tests
   regress1/quantifiers/cdt-0208-to.smt2
   regress1/quantifiers/const.cvc
   regress1/quantifiers/constfunc.cvc
+  regress1/quantifiers/dt-tc-opt-small.smt2
   regress1/quantifiers/dump-inst-i.smt2
   regress1/quantifiers/dump-inst-proof.smt2
   regress1/quantifiers/dump-inst.smt2
diff --git a/test/regress/regress1/quantifiers/dt-tc-opt-small.smt2 b/test/regress/regress1/quantifiers/dt-tc-opt-small.smt2
new file mode 100644
index 000000000..6cf81e80a
--- /dev/null
+++ b/test/regress/regress1/quantifiers/dt-tc-opt-small.smt2
@@ -0,0 +1,16 @@
+; EXPECT: unknown
+
+; This triggered a failure related to datatypes model building (when symfpu is enabled)
+(set-logic ALL)
+(declare-datatypes ((V 0) (A 0)) (
+  ((I (i Int)) (vec (v A)))
+  ((arr (l Int)))))
+(declare-fun E (V V) Bool)
+(declare-fun eee (A) Bool)
+(declare-fun a () V)
+(declare-fun aa () A)
+(assert (forall ((?y1 A)) (eee ?y1)))
+(assert (E a a))
+(assert (not (E (I 0) (I 0))))
+(assert (= (l aa) (i a)))
+(check-sat)