projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 59b935c) | patch
Minor refactoring of entailment tests and quantifiers util. Initial draft of instanti...
authorajreynol <andrew.j.reynolds@gmail.com>
Sat, 9 Apr 2016 18:07:11 +0000 (13:07 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Sat, 9 Apr 2016 18:07:11 +0000 (13:07 -0500)
commit67623ee1e6d62b36cb598c28ad9b871b6957a9dd
tree3ea7e16b6b1f8e2073ad9265741fa7853b63c0dftree
parent59b935c1af18ec51efacf87b0e45d9134d3aaa1ecommit | diff
Minor refactoring of entailment tests and quantifiers util. Initial draft of instantiation propagator.
15 files changed:
src/Makefile.am diff | blob | history
src/options/quantifiers_options diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/inst_propagator.cpp [new file with mode: 0644] blob
src/theory/quantifiers/inst_propagator.h [new file with mode: 0644] blob
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.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/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.h 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/quantifiers_engine.h diff | blob | history