projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: deb3045) | patch
added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumera...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 24 Feb 2013 22:37:46 +0000 (16:37 -0600)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 24 Feb 2013 22:37:46 +0000 (16:37 -0600)
commitc71ec272d5ef58bfa147507bdbb370f2e288d154
tree8bf3b84a476fa7fff798158e6b58697399c7b966tree
parentdeb304550fbb6e19346319ec24d83e0650c64e91commit | diff
added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
18 files changed:
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/options diff | blob | history
src/theory/arrays/theory_arrays_rewriter.h diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/uf/options diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.h diff | blob | history