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.

4 files changed, 14 insertions, 10 deletions

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index f9cabe62b..06d11f70f 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -122,7 +122,7 @@ option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode
 
 option quantConflictFind --quant-cf bool :read-write :default false
  enable conflict find mechanism for quantifiers
-option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_CONFLICT_ONLY :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h"
+option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h"
  what effort to apply conflict find mechanism
 option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h"
  when to invoke conflict find mechanism for quantifiers
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 492155e02..9892009a3 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -122,17 +122,17 @@ std-h \n\
 static const std::string qcfModeHelp = "\
 Quantifier conflict find modes currently supported by the --quant-cf option:\n\
 \n\
-conflict \n\
-+ Default, apply conflict finding for finding conflicts only.\n\
-\n\
 prop-eq \n\
-+ Apply QCF to propagate equalities as well. \n\
++ Default, apply QCF algorithm to propagate equalities as well as conflicts. \n\
+\n\
+conflict \n\
++ Apply QCF algorithm to find conflicts only.\n\
 \n\
 partial \n\
-+ Apply QCF to instantiate heuristically as well. \n\
++ Apply QCF algorithm to instantiate heuristically as well. \n\
 \n\
 mc \n\
-+ Apply QCF in a complete way, so that a model is ensured when it fails. \n\
++ Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\
 \n\
 ";
 static const std::string userPatModeHelp = "\
@@ -259,9 +259,9 @@ inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, S
   }
 }
 inline QcfMode stringToQcfMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "default" || optarg ==  "conflict") {
+  if(optarg ==  "conflict") {
     return QCF_CONFLICT_ONLY;
-  } else if(optarg == "prop-eq") {
+  } else if(optarg ==  "default" || optarg == "prop-eq") {
     return QCF_PROP_EQ;
   } else if(optarg == "partial") {
     return QCF_PARTIAL;
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;

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 0452278f2..952f3409a 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -190,7 +190,7 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
       bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] );
       //the negative occurrence adds the term to the domain
       if( !hasPol || !pol ){
-        rds[varCh]->addTerm( n[oCh] );
+        rds[varCh]->addTerm( n[oCh], ng );
       }
       //the positive occurence adds other terms
       if( ( !hasPol || pol ) && n[0].getType().isInteger() ){