Do not normalize to representatives for variable equalities in conflict-based instantiation (#4280)

Conflict-based instantiation would sometimes initialize a match x -> getRepresentative(t) when a quantified formula contained x = t. This leads to issues where getRepresentative(t) is an illegal term (say, in combination with CEGQI). This makes it so the representative is accessed when necessary instead of being set as part of the match.

Fixes #4275.

2 files changed, 7 insertions, 10 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 89f4f2989..511eb6d79 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1194,9 +1194,6 @@ bool MatchGen::reset_round(QuantConflictFind* p)
       return false;
     }
   }
-  for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
-    d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
-  }
   if( d_type==typ_ground ){
     // int e = p->evaluate( d_n );
     // if( e==1 ){
@@ -1324,14 +1321,15 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     if( d_type==typ_pred ){
       nn[0] = qi->getCurrentValue( d_n );
       vn[0] = qi->getCurrentRepVar( qi->getVarNum( nn[0] ) );
-      nn[1] = p->getRepresentative( d_tgt ? p->d_true : p->d_false );
+      nn[1] = d_tgt ? p->d_true : p->d_false;
       vn[1] = -1;
       d_tgt = true;
     }else{
       for( unsigned i=0; i<2; i++ ){
         TNode nc;
-        std::map< int, TNode >::iterator it = d_qni_gterm_rep.find( i );
-        if( it!=d_qni_gterm_rep.end() ){
+        std::map<int, TNode>::iterator it = d_qni_gterm.find(i);
+        if (it != d_qni_gterm.end())
+        {
           nc = it->second;
         }else{
           nc = d_n[i];
@@ -1698,14 +1696,14 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
           }else{
             Debug("qcf-match-debug") << "       Match " << index << " is ground term" << std::endl;
             Assert(d_qni_gterm.find(index) != d_qni_gterm.end());
-            Assert(d_qni_gterm_rep.find(index) != d_qni_gterm_rep.end());
-            val = d_qni_gterm_rep[index];
+            val = d_qni_gterm[index];
             Assert(!val.isNull());
           }
           if( !val.isNull() ){
+            Node valr = p->getRepresentative(val);
             //constrained by val
             std::map<TNode, TNodeTrie>::iterator it =
-                d_qn[index]->d_data.find(val);
+                d_qn[index]->d_data.find(valr);
             if( it!=d_qn[index]->d_data.end() ){
               Debug("qcf-match-debug") << "       Match" << std::endl;
               d_qni.push_back( it );
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 836bba80e..59da77739 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -52,7 +52,6 @@ private:
   unsigned d_qni_size;
   std::map< int, int > d_qni_var_num;
   std::map< int, TNode > d_qni_gterm;
-  std::map< int, TNode > d_qni_gterm_rep;
   std::map< int, int > d_qni_bound;
   std::vector< int > d_qni_bound_except;
   std::map< int, TNode > d_qni_bound_cons;