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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 15 Nov 2017 01:06:49 +0000 (19:06 -0600)
committer	GitHub <noreply@github.com>
	Wed, 15 Nov 2017 01:06:49 +0000 (19:06 -0600)
commit	85df7998e4362e0a9c796146d07d7b9e91045a31
tree	0ab2e33e807651386cd041257c1abff2bb769057	tree
parent	748e20967ae7698f6b545a5128633865701aeb2d	commit \| diff

Make QEffort an enum (#1366)

* Make QEffort an enum.

* Format

* Minor

* Fix

34 files changed:

src/theory/quantifiers/anti_skolem.cpp		diff \| blob \| history
src/theory/quantifiers/anti_skolem.h		diff \| blob \| history
src/theory/quantifiers/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/ce_guided_instantiation.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_instantiation.h		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.h		diff \| blob \| history
src/theory/quantifiers/fun_def_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_engine.h		diff \| blob \| history
src/theory/quantifiers/inst_propagator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_propagator.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.h		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.h		diff \| blob \| history
src/theory/quantifiers/local_theory_ext.cpp		diff \| blob \| history
src/theory/quantifiers/local_theory_ext.h		diff \| blob \| history
src/theory/quantifiers/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/model_engine.h		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/quant_equality_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quant_equality_engine.h		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.h		diff \| blob \| history
src/theory/quantifiers/quant_util.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.h		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.cpp		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history

RSS Atom