projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 01b2570) | patch
Frontend support for the choice operator (#4175)
authormudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu>
Mon, 30 Mar 2020 14:04:52 +0000 (09:04 -0500)
committerGitHub <noreply@github.com>
Mon, 30 Mar 2020 14:04:52 +0000 (09:04 -0500)
commit0060de329173c0b75c02778d003371f59cc11eff
tree92bec1579d0301a4c91e45c349c381a9bd2f1b17tree
parent01b257084a0a8ee70bff32e011704330d1544c01commit | 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
src/parser/cvc/Cvc.g diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/theory/builtin/theory_builtin.cpp diff | blob | history
src/theory/builtin/theory_builtin.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/parser/choice.cvc [new file with mode: 0644] blob
test/regress/regress0/parser/choice.smt2 [new file with mode: 0644] blob