projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 318e836) | patch
Abstract values for SMT-LIB.
authorMorgan Deters <mdeters@gmail.com>
Wed, 10 Oct 2012 21:20:40 +0000 (21:20 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 10 Oct 2012 21:20:40 +0000 (21:20 +0000)
commit7b2dd1927731b894f5ef610528649a2d1fc555f2
tree6d8ad29a1ec8783601787f4b9216fa6409bb9780tree
parent318e836ed5f6bd76d378dfce1c707b9908a1c5e1commit | diff
Abstract values for SMT-LIB.
Also fix bug 421 relating to incrementality and models.

(this commit was certified error- and warning-free by the test-and-commit script.)
17 files changed:
src/expr/node.cpp diff | blob | history
src/expr/node.h diff | blob | history
src/expr/node_builder.h diff | blob | history
src/options/base_options diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
src/smt/options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/theory/builtin/kinds diff | blob | history
src/theory/builtin/theory_builtin_type_rules.h diff | blob | history
src/theory/substitutions.cpp diff | blob | history
src/util/Makefile.am diff | blob | history
src/util/abstract_value.cpp [new file with mode: 0644] blob
src/util/abstract_value.h [new file with mode: 0644] blob
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/bug421.smt2 [new file with mode: 0644] blob