diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2014-08-18 22:02:25 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2014-10-02 13:28:22 -0700 |
| commit | 3df8013300486129fc06f3a20d43def1f34a221a (patch) | |
| tree | 3b1cc75aa596820336f15d5ae7ff64d3048e290d /src/theory/valuation.cpp | |
| parent | 7388ddece082dc254f4b04ce5109427cd340fde4 (diff) | |
Better getEqualityStatus for arrays, smarter combination of theories
Diffstat (limited to 'src/theory/valuation.cpp')
| -rw-r--r-- | src/theory/valuation.cpp | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 72d878782..b2d7f4b21 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -88,13 +88,7 @@ Node Valuation::getModelValue(TNode var) { } Node Valuation::ensureLiteral(TNode n) { - Debug("ensureLiteral") << "rewriting: " << n << std::endl; - Node rewritten = Rewriter::rewrite(n); - Debug("ensureLiteral") << " got: " << rewritten << std::endl; - Node preprocessed = d_engine->preprocess(rewritten); - Debug("ensureLiteral") << "preproced: " << preprocessed << std::endl; - d_engine->getPropEngine()->ensureLiteral(preprocessed); - return preprocessed; + return d_engine->ensureLiteral(n); } bool Valuation::isDecision(Node lit) const { |