diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-02 09:46:15 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-02 09:46:15 -0500 |
commit | 9720e341d9cda3de7e7b2b0c25afe190cc2021e4 (patch) | |
tree | cb44e6cd092956a05ac00d4104d19bd0e1f36eb4 /src/theory/builtin/theory_builtin.cpp | |
parent | 796703fc72cfd67dc05357b10a5f0311200f2865 (diff) | |
parent | aa6fb6fa3df0b1519e6763e72541c022396ab1dc (diff) |
Merge branch 'master' into rmAliasesrmAliases
Diffstat (limited to 'src/theory/builtin/theory_builtin.cpp')
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 37 |
1 files changed, 33 insertions, 4 deletions
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index b819b883d..8df5a8535 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -15,9 +15,11 @@ **/ #include "theory/builtin/theory_builtin.h" -#include "theory/valuation.h" + #include "expr/kind.h" +#include "theory/builtin/theory_builtin_rewriter.h" #include "theory/theory_model.h" +#include "theory/valuation.h" using namespace std; @@ -25,6 +27,33 @@ namespace CVC4 { namespace theory { namespace builtin { -}/* CVC4::theory::builtin namespace */ -}/* CVC4::theory */ -}/* CVC4 namespace */ +TheoryBuiltin::TheoryBuiltin(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo) + : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) +{ +} + +std::unique_ptr<TheoryRewriter> TheoryBuiltin::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new TheoryBuiltinRewriter()); +} + +std::string TheoryBuiltin::identify() const +{ + return std::string("TheoryBuiltin"); +} + +void TheoryBuiltin::finishInit() +{ + // choice nodes are not evaluated in getModelValue + TheoryModel* theoryModel = d_valuation.getModel(); + Assert(theoryModel != nullptr); + theoryModel->setUnevaluatedKind(kind::CHOICE); +} + +} // namespace builtin +} // namespace theory +} // namespace CVC4 |