From 4ad0191e20e4d812d9a5dc3a733153cb10f6d728 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 7 Nov 2014 17:38:53 +0100 Subject: [PATCH] Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement to performance of E-matching. --- src/smt/smt_engine.cpp | 6 +++++- src/theory/quantifiers/inst_match_generator.cpp | 7 +++++-- src/theory/quantifiers/inst_match_generator.h | 4 ++++ src/theory/quantifiers/options | 2 +- src/theory/quantifiers/quant_conflict_find.cpp | 4 +++- src/theory/quantifiers/quant_conflict_find.h | 1 + src/theory/quantifiers_engine.cpp | 1 + 7 files changed, 20 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 577fa7413..c59d87d40 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1358,7 +1358,11 @@ void SmtEngine::setDefaults() { options::finiteModelFind.set( true ); } } - + if( options::finiteModelFind() ){ + if( !options::quantConflictFind.wasSetByUser() ){ + options::quantConflictFind.set( false ); + } + } //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index c78ea7b01..4a5197fc8 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -36,6 +36,7 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){ Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); d_pattern = pat; d_match_pattern = pat; + d_match_pattern_type = pat.getType(); d_next = NULL; d_matchPolicy = MATCH_GEN_DEFAULT; } @@ -92,6 +93,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat } } } + d_match_pattern_type = d_match_pattern.getType(); Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; d_match_pattern_op = qe->getTermDatabase()->getOperator( d_match_pattern ); @@ -315,7 +317,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* t = d_cg->getNextCandidate(); Trace("matching-debug2") << "Matching candidate : " << t << std::endl; //if t not null, try to fit it into match m - if( !t.isNull() && t.getType().isSubtypeOf( d_match_pattern.getType() ) ){ + if( !t.isNull() && t.getType().isSubtypeOf( d_match_pattern_type ) ){ success = getMatch( f, t, m, qe ); } }while( !success && !t.isNull() ); @@ -675,6 +677,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f if( d_match_pattern[i].getKind()==INST_CONSTANT ){ d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute()); } + d_match_pattern_arg_types.push_back( d_match_pattern[i].getType() ); } } @@ -713,7 +716,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin Node t = it->first; Node prev = m.get( v ); //using representatives, just check if equal - if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern[argIndex].getType() ) ){ + if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern_arg_types[argIndex] ) ){ m.setValue( v, t); addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); m.setValue( v, prev); diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index aa5d37713..850affe56 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -96,6 +96,8 @@ public: Node d_pattern; /** match pattern */ Node d_match_pattern; + /** match pattern type */ + TypeNode d_match_pattern_type; /** match pattern op */ Node d_match_pattern_op; public: @@ -204,6 +206,8 @@ private: Node d_f; /** match term */ Node d_match_pattern; + /** match pattern arg types */ + std::vector< TypeNode > d_match_pattern_arg_types; /** operator */ Node d_op; /** to indicies */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 8cb693117..97a43a96d 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -143,7 +143,7 @@ option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" policy for instantiating axioms -option quantConflictFind --quant-cf bool :read-write :default false +option quantConflictFind --quant-cf bool :read-write :default true enable conflict find mechanism for quantifiers 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 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; id_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()second ); diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 93e1f72a6..b2dc680f2 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -118,6 +118,7 @@ public: QuantInfo() : d_mg( NULL ) {} ~QuantInfo() { delete d_mg; } std::vector< TNode > d_vars; + std::vector< TypeNode > d_var_types; std::map< TNode, int > d_var_num; std::vector< int > d_tsym_vars; std::map< TNode, bool > d_inMatchConstraint; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 46995653f..eabba85bf 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -524,6 +524,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std for( int i=0; i<(int)terms.size(); i++ ){ Trace("inst") << " " << terms[i]; Trace("inst") << std::endl; + Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) ); } if( options::cbqi() ){ for( int i=0; i<(int)terms.size(); i++ ){ -- 2.30.2