diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 15:28:24 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 15:28:24 +0000 |
commit | b11f6d3a27d33b9075e57b37f77ad9d11732fce5 (patch) | |
tree | b00e257f54c8adebe15f92927fc7b51cb61887c7 /src/theory/quantifiers_engine.cpp | |
parent | 19f0a337307ce0e424b12acf6102829d81dbbf99 (diff) |
more updates to inst gen: fixed partial instantiations, recognize duplicate defaults for uf
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4ba5c39e6..4e933a511 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -94,6 +94,9 @@ Valuation& QuantifiersEngine::getValuation(){ void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); + if( e>=Theory::EFFORT_FULL ){ + Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; + } d_hasAddedLemma = false; if( e==Theory::EFFORT_LAST_CALL ){ @@ -116,6 +119,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){ d_te->getModelBuilder()->buildModel( d_model, true ); } + if( e>=Theory::EFFORT_FULL ){ + Trace("quant-engine") << "Finished quantifiers engine check." << std::endl; + } } std::vector<Node> QuantifiersEngine::createInstVariable( std::vector<Node> & vars ){ @@ -311,14 +317,16 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std } } -bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m ){ +bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){ //make sure there are values for each variable we are instantiating m.makeComplete( f, this ); //make it representative, this is helpful for recognizing duplication - m.makeRepresentative( this ); + if( mkRep ){ + m.makeRepresentative( this ); + } Trace("inst-add") << "Add instantiation: " << m << std::endl; //check for duplication modulo equality - if( !d_inst_match_trie[f].addInstMatch( this, f, m, true ) ){ + if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){ Trace("inst-add") << " -> Already exists." << std::endl; ++(d_statistics.d_inst_duplicate); return false; |