diff options
author | Tim King <taking@cs.nyu.edu> | 2012-09-11 00:20:51 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-09-11 00:20:51 +0000 |
commit | d8883776ce80199096f99d1088910d478fd0cd6e (patch) | |
tree | 1425084ba75c36b00656c74d59dd8ebf5bf88a1a /src/theory/model.cpp | |
parent | 680af6f4dc9e5d6616918e8fde18cd64774d0df5 (diff) |
Partially reverting the changes made in 4308. There is now both an Expr and Node version of getValue() in TheoryModel.
Diffstat (limited to 'src/theory/model.cpp')
-rw-r--r-- | src/theory/model.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 67640c309..dc0ae7877 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -46,12 +46,16 @@ void TheoryModel::reset(){ d_rep_set.clear(); } -Expr TheoryModel::getValue( const Expr& expr ){ - Node n = Node::fromExpr( expr ); +Node TheoryModel::getValue( TNode n ){ //apply substitutions Node nn = d_substitutions.apply( n ); //get value in model - Node ret = getModelValue( nn ); + return getModelValue( nn ); +} + +Expr TheoryModel::getValue( const Expr& expr ){ + Node n = Node::fromExpr( expr ); + Node ret = getValue( n ); return ret.toExpr(); } @@ -553,4 +557,4 @@ Node TheoryEngineModelBuilder::normalizeNode( TheoryModel* m, Node r, std::map< }else{ return r; } -}
\ No newline at end of file +} |