diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-26 19:26:21 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-26 19:26:21 +0200 |
commit | f07e8a3f06feb789692ede8ad9d25a2e049af769 (patch) | |
tree | bdeb79262056c70c6b5125ed11a392a4fa1864f7 /src/theory/quantifiers/inst_match.cpp | |
parent | 349deb0522c4602b740d96f6a688b644dd84c64f (diff) |
Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 078614509..cb969088d 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -127,6 +127,17 @@ Node InstMatch::get( int i ) { return d_vals[i]; } +void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ){ + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + Node val = get( i ); + if( val.isNull() ){ + Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i ); + val = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + } + inst.push_back( val ); + } +} + void InstMatch::setValue( int i, TNode n ) { d_vals[i] = n; } |