Bug fix for QCF algorithm, was missing instantiations. Make prop-eq the default...

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index f9cabe62be72710ae0104d166e7f49de37d8d413..06d11f70f42bcfddb348c70d4c49e0dcad678ee7 100644 (file)
--- 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 492155e02136a45596d616512c3eee900e2702e6..9892009a3987c0199aa1ddebb6bdd5a8be362d22 100644 (file)
--- 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 1a47b3a02eebd37b10f0536cbe08a782349477de..ced4e1997e816c2aa2442a367ff2518b62c824cd 100755 (executable)
--- 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;\r
               }\r
             }else{\r
+              qi->d_match[ itb->second ] = TNode::null();\r
+              qi->d_match_term[ itb->second ] = TNode::null();\r
               Debug("qcf-match-debug") << "       Bind next variable, no more variables to bind" << std::endl;\r
             }\r
           }else{\r
@@ -1898,6 +1900,7 @@ void QuantConflictFind::computeRelevantEqr() {
     }else{\r
       d_eqcs[rtn].push_back( r );\r
     }\r
+    /*\r
     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
     while( !eqc_i.isFinished() ){\r
       TNode n = (*eqc_i);\r
@@ -1907,6 +1910,7 @@ void QuantConflictFind::computeRelevantEqr() {
       }\r
       ++eqc_i;\r
     }\r
+    */\r
 \r
     //if( r.getType().isInteger() ){\r
     //  Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;\r

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 0452278f28f7f93351e6150b75fa69c2967bd1cc..952f3409ab4f280e075f3f5e8c6fa77c725c5078 100644 (file)
--- 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() ){