Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement to performance of E-matching.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index f976a0dbf..d58ce14b1 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -43,6 +43,7 @@ void QuantInfo::initialize( Node q, Node qn ) {
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){

     d_var_num[q[0][i]] = i;

     d_vars.push_back( q[0][i] );

+    d_var_types.push_back( q[0][i].getType() );

   }

 

   registerNode( qn, true, true );

@@ -145,6 +146,7 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) {
       Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;

       d_var_num[n] = d_vars.size();

       d_vars.push_back( n );

+      d_var_types.push_back( n.getType() );

       d_match.push_back( TNode::null() );

       d_match_term.push_back( TNode::null() );

       if( n.getKind()==ITE ){

@@ -1524,7 +1526,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
               if( it != d_qn[index]->d_data.end() ) {

                 d_qni.push_back( it );

                 //set the match

-                if( qi->setMatch( p, d_qni_bound[index], it->first ) ){

+                if( it->first.getType().isSubtypeOf( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){

                   Debug("qcf-match-debug") << "       Binding variable" << std::endl;

                   if( d_qn.size()<d_qni_size ){

                     d_qn.push_back( &it->second );