diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-19 11:00:48 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-19 11:00:48 -0600 |
commit | 2150eb22aaff94f9d0d9f0ee0854ea44675fd854 (patch) | |
tree | 061ee4c79296a6625d7f42f0ccb2dd1f1bab4fe9 /src/theory/quantifiers | |
parent | f47f24528f5d19ac0affd572f3d34c090e97f9f9 (diff) |
Fixes and improvements for datatypes properties and splitting.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index e874ee5b8..1ae1c3c5f 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -48,11 +48,11 @@ void QuantDSplit::preRegisterQuantifier( Node q ) { }else{ int score = -1; if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ - score = dt.isFinite() ? 1 : -1; - }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ + score = dt.isUFinite() ? 1 : -1; + }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ score = dt.isUFinite() ? 1 : -1; } - Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << std::endl; + Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isUFinite() << " " << dt.isFinite() << ")" << std::endl; if( score>max_score ){ max_index = i; max_score = score; @@ -70,11 +70,12 @@ void QuantDSplit::preRegisterQuantifier( Node q ) { /* whether this module needs to check this round */ bool QuantDSplit::needsCheck( Theory::Effort e ) { - return e>=Theory::EFFORT_FULL; + return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty(); } + /* Call during quantifier engine's check */ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { - //flush lemmas ASAP (they are a reduction) + //add lemmas ASAP (they are a reduction) if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){ std::vector< Node > lemmas; for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) { @@ -92,6 +93,7 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { TNode svar = q[0][it->second]; TypeNode tn = svar.getType(); if( tn.isDatatype() ){ + std::vector< Node > cons; const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); for( unsigned j=0; j<dt.getNumConstructors(); j++ ){ std::vector< Node > vars; @@ -110,8 +112,10 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { if( !bvs_cmb.empty() ){ body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body ); } - disj.push_back( body ); + cons.push_back( body ); } + Node conc = cons.size()==1 ? cons[0] : NodeManager::currentNM()->mkNode( kind::AND, cons ); + disj.push_back( conc ); }else{ Assert( false ); } @@ -124,6 +128,7 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { Trace("quant-dsplit") << "QuantDSplit lemma : " << lemmas[i] << std::endl; d_quantEngine->addLemma( lemmas[i], false ); } + d_quant_to_reduce.clear(); } } |