projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f6d24c5) | patch
Preliminary version of finite model finding over bounded integer quantification....
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 11 May 2013 22:36:07 +0000 (17:36 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 11 May 2013 22:36:07 +0000 (17:36 -0500)
commit24d60fa5654a32b09dc8de79b7704fbf40051478
treed3bce397adceb1407764a54489c191aea06d134atree
parentf6d24c56905449e68ee23a9cea54985eacd24aa3commit | diff
Preliminary version of finite model finding over bounded integer quantification. Minor update to casc script.
15 files changed:
contrib/run-script-casc24-fnt diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history
src/theory/arith/theory_arith_private.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/full_model_check.cpp diff | blob | history
src/theory/quantifiers/model_builder.cpp 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_util.cpp diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/rep_set.h diff | blob | history