diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-27 08:34:59 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-27 08:35:14 -0600 |
commit | 251fd73a759a8e5e94103e9b76a06491a92e425b (patch) | |
tree | 193cd049c7422b30c6a65ce119f1ac18615037f9 | |
parent | 7a6c462b0ce3adf52a9d44a5f98c53065fedc33d (diff) |
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.
-rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 16 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 2 |
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() ){ |