diff options
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 16 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 1 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 | 8 |
4 files changed, 16 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; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 19ccc91e4..b32f936bd 100644 --- 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 index 000000000..51d3e89ea --- /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) |