projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3c2fc39) | 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)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 2 Oct 2013 19:22:46 +0000 (14:22 -0500)
commit5953c950bef395488d76d63ebabefce98814a06d
treed1c0c7d617a81bdea3197247584dfcd9169a0bb5tree
parent3c2fc39e3b8b53466705bfd82818c442f6eb22e5commit | 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