diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-27 08:34:52 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-27 08:34:52 -0600 |
| commit | e179e62b57eb207d41647a6bbd50ef0f8c723e96 (patch) | |
| tree | 9a768eeae815f2851f34dc3fbb3fd3661e939c8d /src/theory/quantifiers/full_model_check.cpp | |
| parent | d0add0eb12cac4e9cbcf09fe60724d280889002d (diff) | |
More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index c7d7b7415..d542e878c 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -672,12 +672,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, } }else{ //just add the instance - InstMatch m; - for( unsigned j=0; j<inst.size(); j++) { - m.set( d_qe, f, j, inst[j] ); - } d_triedLemmas++; - if( d_qe->addInstantiation( f, m ) ){ + if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; }else{ @@ -792,13 +788,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size(); Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index]; if (ev!=d_true) { - InstMatch m; - for( unsigned i=0; i<inst.size(); i++ ){ - m.set( d_qe, f, i, inst[i] ); - } Trace("fmc-exh-debug") << ", add!"; //add as instantiation - if( d_qe->addInstantiation( f, m ) ){ + if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-exh-debug") << " ...success."; addedLemmas++; }else{ |