Do not normalize to representatives for variable equalities in conflict-based instant...

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.

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 89f4f2989d464cfb1e6409a5f7743498e2c973cd..511eb6d7915c7b2527c42663ddae391287ef030d 100644 (file)
--- 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 836bba80e49ba414e19b40ccef5bf5a5632aa373..59da777399b093c82518c2ac10568236f56d9fcc 100644 (file)
--- 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;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 19ccc91e4cac4222b2ae8f3c7562dcdc31cdaa5b..b32f936bd897363f9c3f0fe46109d2804d3c5e58 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -734,6 +734,7 @@ set(regress_0_tests
   regress0/quantifiers/issue2035.smt2
   regress0/quantifiers/issue3655.smt2
   regress0/quantifiers/issue4086-infs.smt2
+  regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
   regress0/quantifiers/macros-real-arg.smt2

diff --git a/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 b/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
new file mode 100644 (file)
index 0000000..51d3e89
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
@@ -0,0 +1,8 @@
+(set-logic UFBV)
+(set-option :cbqi-all true)
+(set-info :status unsat)
+(declare-sort S0 0)
+(declare-const S0-0 S0)
+(declare-const v6 Bool)
+(assert (forall ((q0 (_ BitVec 10)) (q1 S0) (q2 S0) (q3 Bool)) (xor true (and q3 q3 q3 v6 q3 q3) (= q2 q1 S0-0))))
+(check-sat)