Bug fix for QCF algorithm, was missing instantiations. Make prop-eq the default QCF setting. Bug fix to prevent non-ground terms from entering relevant domains.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 1a47b3a02..ced4e1997 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1277,6 +1277,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
                 invalidMatch = true;

               }

             }else{

+              qi->d_match[ itb->second ] = TNode::null();

+              qi->d_match_term[ itb->second ] = TNode::null();

               Debug("qcf-match-debug") << "       Bind next variable, no more variables to bind" << std::endl;

             }

           }else{

@@ -1898,6 +1900,7 @@ void QuantConflictFind::computeRelevantEqr() {
     }else{

       d_eqcs[rtn].push_back( r );

     }

+    /*

     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );

     while( !eqc_i.isFinished() ){

       TNode n = (*eqc_i);

@@ -1907,6 +1910,7 @@ void QuantConflictFind::computeRelevantEqr() {
       }

       ++eqc_i;

     }

+    */

 

     //if( r.getType().isInteger() ){

     //  Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;