git.libre-soc.org Git - cvc5.git/commit

projects / cvc5.git / commit

summary | shortlog | log | commit | commitdiff | tree
(parent: 3eaf02c) | patch

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 24 Jun 2013 17:52:07 +0000 (12:52 -0500)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 24 Jun 2013 17:52:21 +0000 (12:52 -0500)
commit	30d21b25af6ee619e5f53d1ca8821b710fad4cb7
tree	409009a6ab55986308cc73d030db53489beef26d	tree
parent	3eaf02c01e74a2a43b2eff7638d6c16171a11a13	commit \| diff

Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine

14 files changed:

src/theory/quantifiers/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_generator.h		diff \| blob \| history
src/theory/quantifiers/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/full_model_check.h		diff \| blob \| history
src/theory/quantifiers/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_generator.h		diff \| blob \| history
src/theory/quantifiers/options		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.cpp		diff \| blob \| history
src/theory/quantifiers/trigger.cpp		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