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 | |
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
-rw-r--r-- | src/parser/cvc/Cvc.g | 6 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 31 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 30 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 8 | ||||
-rw-r--r-- | src/theory/theory_model.h | 3 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress0/parser/choice.cvc | 10 | ||||
-rw-r--r-- | test/regress/regress0/parser/choice.smt2 | 10 |
9 files changed, 78 insertions, 24 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 033389610..8b3b96cfd 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -114,6 +114,7 @@ tokens { FORALL_TOK = 'FORALL'; EXISTS_TOK = 'EXISTS'; + CHOICE_TOK = 'CHOICE'; PATTERN_TOK = 'PATTERN'; LAMBDA_TOK = 'LAMBDA'; @@ -343,7 +344,8 @@ int getOperatorPrecedence(int type) { case IMPLIES_TOK: return 30;// right-to-left case IFF_TOK: return 31; case FORALL_TOK: - case EXISTS_TOK: return 32; + case EXISTS_TOK: + case CHOICE_TOK: return 32; case ASSIGN_TOK: case IN_TOK: return 33; @@ -1465,7 +1467,7 @@ prefixFormula[CVC4::api::Term& f] api::Term ipl; } /* quantifiers */ - : ( FORALL_TOK { k = api::FORALL; } | EXISTS_TOK { k = api::EXISTS; } ) + : ( FORALL_TOK { k = api::FORALL; } | EXISTS_TOK { k = api::EXISTS; } | CHOICE_TOK { k = api::CHOICE; } ) { PARSER_STATE->pushScope(); } LPAREN boundVarDecl[ids,t] { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 0c42678aa..d0a73ce6a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2312,6 +2312,7 @@ quantOp[CVC4::api::Kind& kind] } : EXISTS_TOK { $kind = api::EXISTS; } | FORALL_TOK { $kind = api::FORALL; } + | CHOICE_TOK { $kind = api::CHOICE; } ; /** @@ -2682,6 +2683,7 @@ ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level'; // operators (NOTE: theory symbols go here) EXISTS_TOK : 'exists'; FORALL_TOK : 'forall'; +CHOICE_TOK : { !PARSER_STATE->strictModeEnabled() }? 'choice'; EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple'; 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 */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 7bfb0e8f3..dae7261e5 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -147,7 +147,7 @@ Node TheoryModel::getValue(TNode n) const Node nn = d_substitutions.apply(n); Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl; //get value in model - nn = getModelValue(nn, false); + nn = getModelValue(nn); if (nn.isNull()) return nn; if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) { //normalize @@ -193,7 +193,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ } } -Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const +Node TheoryModel::getModelValue(TNode n) const { std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n); if (it != d_modelCache.end()) { @@ -220,7 +220,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const std::vector<Node> children; if (n.getKind() == APPLY_UF) { - Node op = getModelValue(n.getOperator(), hasBoundVars); + Node op = getModelValue(n.getOperator()); Debug("model-getvalue-debug") << " operator : " << op << std::endl; children.push_back(op); } @@ -231,7 +231,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // evaluate the children for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; ++i) { - ret = getModelValue(n[i], hasBoundVars); + ret = getModelValue(n[i]); Debug("model-getvalue-debug") << " " << n << "[" << i << "] is " << ret << std::endl; children.push_back(ret); diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index d2ce63ac5..d984fbc6b 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -390,9 +390,8 @@ public: /** Get model value function. * * This function is a helper function for getValue. - * hasBoundVars is whether n may contain bound variables */ - Node getModelValue(TNode n, bool hasBoundVars = false) const; + Node getModelValue(TNode n) const; /** add term internal * * This will do any model-specific processing necessary for n, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a5acd62fb..d843eb5ed 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -610,6 +610,8 @@ set(regress_0_tests regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 regress0/parser/bv_nat.smt2 + regress0/parser/choice.cvc + regress0/parser/choice.smt2 regress0/parser/constraint.smt2 regress0/parser/declarefun-emptyset-uf.smt2 regress0/parser/force_logic_set_logic.smt2 diff --git a/test/regress/regress0/parser/choice.cvc b/test/regress/regress0/parser/choice.cvc new file mode 100644 index 000000000..e0ebac051 --- /dev/null +++ b/test/regress/regress0/parser/choice.cvc @@ -0,0 +1,10 @@ +% EXPECT: sat + +a : INT; +b : INT; +c : INT; + +ASSERT (CHOICE(x: INT): x = a) = 1; +ASSERT (CHOICE(x: INT): x = b) = 2; + +CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/parser/choice.smt2 b/test/regress/regress0/parser/choice.smt2 new file mode 100644 index 000000000..19763e222 --- /dev/null +++ b/test/regress/regress0/parser/choice.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(assert (= (choice ((x Int)) (= x a)) 1)) +(assert (= (choice ((x Int)) (= x b)) 2)) +;(assert (let ((x (choice ((x Int)) true))) (and (distinct a b x)(= x c)))) +(check-sat) + |