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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 22 May 2013 22:34:23 +0000 (17:34 -0500)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 22 May 2013 22:34:23 +0000 (17:34 -0500)
commit	2bf0735176e0ff5fb9720bfb255ca22443584dcc
tree	16926686e86f182e383efd8153b7d0e11bbc694a	tree
parent	b48a369333f077fa7cce117976f760cd6332691a	commit \| diff

Significant work on bounded integer quantification to handle non-trivial bounds. Refactoring of InstConstantAttribute to be internal to TermDb.

32 files changed:

src/smt/options		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/quantifiers/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		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_gen.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp		diff \| blob \| history
src/theory/quantifiers/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/model_builder.h		diff \| blob \| history
src/theory/quantifiers/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/options		diff \| blob \| history
src/theory/quantifiers/quant_util.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/trigger.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/rep_set.cpp		diff \| blob \| history
src/theory/rep_set.h		diff \| blob \| history
src/theory/rewriterules/rr_inst_match.cpp		diff \| blob \| history
src/theory/rewriterules/rr_inst_match.h		diff \| blob \| history
src/theory/rewriterules/rr_trigger.cpp		diff \| blob \| history
src/theory/rewriterules/rr_trigger.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_rules.cpp		diff \| blob \| history

RSS Atom