Theory "alternates" support
authorMorgan Deters <mdeters@cs.nyu.edu>
Wed, 24 Apr 2013 03:03:37 +0000 (23:03 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Wed, 24 Apr 2013 03:16:58 +0000 (23:16 -0400)
commitb25991f4c2779c34b51cd51b943290a4a3d2a9fd
treeaaec41cf29cc3574288c6110ba246f361d84ec3a
parenta006e7b92327668b76a1ab993007f42fe91052c3
Theory "alternates" support

* This is a feature that Dejan and I want for the upcoming tutorial.
  It allows rapid prototyping of new decision procedure implementations
  (which we may choose to demonstrate), and a new --use-theory command-line
  option to select from different available implementations.  It has no
  affect on the current set of theories, as no "alternates" are defined.

* Also update the new-theory script, which was broken and incomplete.
27 files changed:
configure.ac
contrib/Makefile.am
contrib/alttheoryskel/Makefile [new file with mode: 0644]
contrib/alttheoryskel/Makefile.am [new file with mode: 0644]
contrib/alttheoryskel/README.WHATS-NEXT [new file with mode: 0644]
contrib/alttheoryskel/kinds [new file with mode: 0644]
contrib/alttheoryskel/options [new file with mode: 0644]
contrib/alttheoryskel/options_handlers.h [new file with mode: 0644]
contrib/alttheoryskel/theory_DIR.cpp [new file with mode: 0644]
contrib/alttheoryskel/theory_DIR.h [new file with mode: 0644]
contrib/new-theory
contrib/theoryskel/Makefile.am
contrib/theoryskel/README.WHATS-NEXT
contrib/theoryskel/options [new file with mode: 0644]
contrib/theoryskel/options_handlers.h [new file with mode: 0644]
contrib/theoryskel/theory_DIR.cpp
contrib/theoryskel/theory_DIR.h
src/expr/metakind_template.h
src/expr/mkexpr
src/expr/mkkind
src/expr/mkmetakind
src/smt/smt_engine.cpp
src/theory/mkrewriter
src/theory/mktheorytraits
src/theory/options
src/theory/options_handlers.h
src/theory/theory_traits_template.h