diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-02-26 21:24:18 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-02-26 21:24:18 +0000 |
commit | edf6aaa87da179948e6b233d16fa37d2aea58bbb (patch) | |
tree | fc5429ce891f579b6e5daedd52e423c13d4f4ec8 /src/theory/valuation.cpp | |
parent | 5c9af4e1382d32352aae7f8c31795831882931b2 (diff) |
Merge from theory-break-dependences branch to break Theory and TheoryEngine dependences; now, if you touch theory_engine.h, only a few things in theory need be recompiled (TheoryEngine, SharedTermManager, .... but no theory implementations), along with the PropEngine and SmtEngine. If you touch a specific theory's .h file, only that theory must be recompiled (along with the TheoryEngine, since it uses traits, and SmtEngine, since it tells the TheoryEngine which theory implementations to use).
Diffstat (limited to 'src/theory/valuation.cpp')
-rw-r--r-- | src/theory/valuation.cpp | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp new file mode 100644 index 000000000..20d339b52 --- /dev/null +++ b/src/theory/valuation.cpp @@ -0,0 +1,31 @@ +/********************* */ +/*! \file valuation.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A "valuation" proxy for TheoryEngine + ** + ** Implementation of Valuation class. + **/ + +#include "expr/node.h" +#include "theory/valuation.h" +#include "theory/theory_engine.h" + +namespace CVC4 { +namespace theory { + +Node Valuation::getValue(TNode n) { + return d_engine->getValue(n); +} + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |