diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 19:27:21 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 19:27:21 -0400 |
| commit | e8021a81993fe5ed201e7fdaf7af007e4d9d012b (patch) | |
| tree | f0fa0cadc16eeda73d32a63b7234238c848e3f73 /src/theory/theory_model.cpp | |
| parent | 96eccb0d6134ccf4ead0134299b2e3750a890083 (diff) | |
cleanup
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 6e0a71641..405fceb6f 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -56,24 +56,14 @@ 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; @@ -240,8 +230,6 @@ 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 { |