diff options
author | mudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu> | 2020-03-30 09:04:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-30 09:04:52 -0500 |
commit | 0060de329173c0b75c02778d003371f59cc11eff (patch) | |
tree | 92bec1579d0301a4c91e45c349c381a9bd2f1b17 /src/theory/builtin | |
parent | 01b257084a0a8ee70bff32e011704330d1544c01 (diff) |
Frontend support for the choice operator (#4175)
Added the operator choice to Smt2.g and Cvc.g.
Removed the unused parameter hasBoundVars from TheoryModel::getModelValue
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 31 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 30 |
2 files changed, 45 insertions, 16 deletions
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index b819b883d..505aa503f 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -15,9 +15,10 @@ **/ #include "theory/builtin/theory_builtin.h" -#include "theory/valuation.h" + #include "expr/kind.h" #include "theory/theory_model.h" +#include "theory/valuation.h" using namespace std; @@ -25,6 +26,28 @@ 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::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 diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 8a7d1bf7b..6e99ef040 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -25,17 +25,23 @@ namespace CVC4 { namespace theory { namespace builtin { -class TheoryBuiltin : public Theory { -public: - TheoryBuiltin(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {} - std::string identify() const override { return std::string("TheoryBuiltin"); } -};/* class TheoryBuiltin */ - -}/* CVC4::theory::builtin namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +class TheoryBuiltin : public Theory +{ + public: + TheoryBuiltin(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo); + + std::string identify() const override; + + /** finish initialization */ + void finishInit() override; +}; /* class TheoryBuiltin */ + +} // namespace builtin +} // namespace theory +} // namespace CVC4 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */ |