Add option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference.
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 15 Dec 2015 11:37:23 +0000 (12:37 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 15 Dec 2015 11:37:23 +0000 (12:37 +0100)
commite600773f0e189d22c5f28ee1d443ba38e5fa72e8
tree6c12ccb1a9a633a3ae7c6ce11091fde41a7bfc49
parent90e3b73fbd1b2eb262a7a7e2e72d701c8f9e3600
Add option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference.
src/options/uf_options
src/smt/smt_engine.cpp
src/theory/sort_inference.cpp
src/theory/sort_inference.h
src/theory/uf/theory_uf_strong_solver.cpp
src/theory/uf/theory_uf_strong_solver.h
src/theory/uf/theory_uf_type_rules.h