projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 341794b) | patch
minor bug fixes for quantifiers, added sort inference module (not ready to be used...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 12 Nov 2012 16:46:51 +0000 (16:46 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 12 Nov 2012 16:46:51 +0000 (16:46 +0000)
commit0ba075e240b2083163ab35a3580547cae6927b6c
tree47be765d608aff213ee58749adab458f315fcf89tree
parent341794b1cbd5693010c78b9f5bfe232ee90404b0commit | diff
minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver
14 files changed:
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/rep_set.h diff | blob | history
src/theory/uf/options diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
src/util/Makefile.am diff | blob | history
src/util/sort_inference.cpp [new file with mode: 0755] blob
src/util/sort_inference.h [new file with mode: 0755] blob