projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8f29e55) | patch
Added support for converting unsorted problems to multi-sorted problems via sort...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 2 Oct 2013 19:22:36 +0000 (14:22 -0500)
committerTianyi Liang <tianyi-liang@uiowa.edu>
Thu, 3 Oct 2013 15:55:14 +0000 (10:55 -0500)
commitb663c658c80cee918afe37222e62dd1e5db33f5c
tree0d440c65b6454b03a4e1f4820ed3e34623edc870tree
parent8f29e55e2d508872234fe811bccf68ffc235d5a4commit | diff
Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity.  Minor cleanup.
src/smt/options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
src/util/sort_inference.cpp diff | blob | history
src/util/sort_inference.h diff | blob | history