projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ae5236e) | patch
Initial infrastructure for bounded set quantification (disabled). Refactoring and...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 1 Jun 2016 20:51:39 +0000 (15:51 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 1 Jun 2016 20:51:47 +0000 (15:51 -0500)
commit6edc4fac0e5c868b6c6bad13ffc9112b16c1d5f5
tree2d89d797c3b2cf856be60234013c7dae9efae258tree
parentae5236eeda43ff591b9264d653727d4ae7d1de68commit | diff
Initial infrastructure for bounded set quantification (disabled). Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.
15 files changed:
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.h 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/inst_strategy_e_matching.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/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h 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/strings/theory_strings.cpp diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/bound-int-alt.smt2 [new file with mode: 0644] blob