projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 594301e) | patch
Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGround...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 16 Mar 2017 16:37:53 +0000 (11:37 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 16 Mar 2017 16:38:09 +0000 (11:38 -0500)
commit966f38dc17ee316fdb069ec2a427c4f79f1f73b2
tree1a1b60435daffa8b59eea589ef04c26b50f8a724tree
parent594301e6f2893ebe9baba5083ff084933b1e9da9commit | diff
Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
24 files changed:
src/expr/datatype.cpp diff | blob | history
src/main/interactive_shell.cpp diff | blob | history
src/main/main.cpp diff | blob | history
src/options/language.cpp diff | blob | history
src/options/language.h diff | blob | history
src/options/language.i diff | blob | history
src/options/options_template.cpp diff | blob | history
src/parser/antlr_input.cpp diff | blob | history
src/parser/cvc/Cvc.g diff | blob | history
src/parser/parser_builder.cpp diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
src/parser/smt2/smt2_input.cpp diff | blob | history
src/printer/printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/util/result.cpp diff | blob | history
src/util/sexpr.cpp diff | blob | history
test/regress/regress0/datatypes/Makefile.am diff | blob | history
test/regress/regress0/datatypes/dt-2.6.smt2 [new file with mode: 0644] blob
test/regress/regress0/datatypes/dt-param-2.6.smt2 [new file with mode: 0644] blob
test/regress/regress0/datatypes/dt-sel-2.6.smt2 [new file with mode: 0644] blob
test/regress/run_regression diff | blob | history