projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ccd1ca4) | patch
Add new symmetry breaking technique for finite model finding. Improvements to bounde...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 27 Sep 2013 14:27:19 +0000 (09:27 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 27 Sep 2013 14:27:29 +0000 (09:27 -0500)
commite277b4d220a1d15ac32f6e4fc5f06e88f55b7f68
tree2a56691dea81453e5f9ba42e859fdc6783fa1545tree
parentccd1ca4c32e8a3eac8b18911a7b2d32b55203707commit | diff
Add new symmetry breaking technique for finite model finding.  Improvements to bounded integer quantifier instantiation.
15 files changed:
src/smt/options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/Makefile.am diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.h diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/symmetry_breaking.cpp [new file with mode: 0755] blob
src/theory/quantifiers/symmetry_breaking.h [new file with mode: 0755] blob
src/theory/quantifiers_engine.cpp [changed mode: 0644->0755] diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/uf/options 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
src/util/sort_inference.cpp diff | blob | history
src/util/sort_inference.h diff | blob | history