projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 15d36d9) | patch
Work on array pf signature, add working example. Add quantifiers proof signature...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 Mar 2014 19:25:25 +0000 (14:25 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 Mar 2014 19:25:25 +0000 (14:25 -0500)
commit8b41e8d8128752eba75f32f751ec9c095a6b1d87
tree68559af9be49966dedfa877b124f76d3af152b7btree
parent15d36d99363b4ee20754498b566bd315150953fccommit | diff
Work on array pf signature, add working example.  Add quantifiers proof signature. Ignore terms not in current master EE for QCF.  Minor refactoring.  Make --rewrite-rules true by default.
12 files changed:
proofs/signatures/example-arrays.plf [new file with mode: 0755] blob
proofs/signatures/th_arrays.plf diff | blob | history
proofs/signatures/th_quant.plf [new file with mode: 0755] blob
src/theory/quantifiers/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quant_conflict_find.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_engine.cpp diff | blob | history
test/regress/regress0/push-pop/bug326.smt2 diff | blob | history