projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9c54375) | patch
SMT-LIBv2 compliance updates:
authorMorgan Deters <mdeters@gmail.com>
Fri, 21 Sep 2012 20:34:19 +0000 (20:34 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 21 Sep 2012 20:34:19 +0000 (20:34 +0000)
commitb5e4b809d1913c9cfc5cf95c04e9fc34c1ca42f3
tree38f605f758581026af28e5c4d4ad72e12b9cb944tree
parent9c543757e459bfae5ce1254322212f72af0d37a4commit | diff
SMT-LIBv2 compliance updates:

* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
  TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default

Also:

* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection

(this commit was certified error- and warning-free by the test-and-commit script.)
16 files changed:
config/readline.m4 diff | blob | history
configure.ac diff | blob | history
src/options/base_options diff | blob | history
src/options/mkoptions diff | blob | history
src/options/options_template.cpp diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_options_template.cpp diff | blob | history
src/theory/builtin/kinds diff | blob | history
src/theory/builtin/theory_builtin_rewriter.cpp diff | blob | history
src/theory/builtin/theory_builtin_rewriter.h diff | blob | history
src/theory/builtin/theory_builtin_type_rules.h diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/bug383.smt2 [new file with mode: 0644] blob