diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 02:01:24 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 17:18:58 -0400 |
commit | 96eccb0d6134ccf4ead0134299b2e3750a890083 (patch) | |
tree | 2dc45e0c86337a1eafa049af42cc02e3743ef14a /src/theory/theory_model.cpp | |
parent | c8b948c37364104bf5f9ca5eca83120247b693a4 (diff) |
fix for sets/mar2014/..317minimized..
Observed behavior:
--check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143))
with different set of elements in the model for representative and the node
itself.
Issue:
The trouble with data structure being mainted to ensure that things
for which lemmas have been generated are not generated again. This
data structure (d_pendingEverInserted) needs to be user context
dependent. The bug was in the sequence of steps from requesting that
a lemma be generated to when it actually was. Sequence was:
addToPending (and also adds to pending ever inserted) ->
isComplete (might remove things from pending if requirment met in other ways) ->
getLemma (actually generated the lemma, if requirement not already met)
Resolution:
adding terms to d_pendingEverInserted was moved from addToPending()
to getLemma().
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 8ec25dffd..6e0a71641 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -56,14 +56,26 @@ void TheoryModel::reset(){ } Node TheoryModel::getValue(TNode n) const { + Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) " + << std::endl; + //apply substitutions Node nn = d_substitutions.apply(n); + Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) post-sub:" + << nn << std::endl; + //get value in model nn = getModelValue(nn); + Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) getmodelvalue: " + << nn << std::endl; + if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) { //normalize nn = Rewriter::rewrite(nn); } + + Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): returning" + << nn << std::endl; return nn; } @@ -228,6 +240,8 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){ /** add substitution */ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ + Debug("model-builder") << "TheoryModel::addSubstitution("<< x << ", " << t + << ", invalidateCache = " << invalidateCache << ")\n"; if( !d_substitutions.hasSubstitution( x ) ){ d_substitutions.addSubstitution( x, t, invalidateCache ); } else { |