projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 83ecbc2) | patch
Add simplification option --fo-prop-quant. Add model support for new model-checking...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 10 May 2013 02:39:03 +0000 (21:39 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 10 May 2013 02:39:03 +0000 (21:39 -0500)
commit20cde072ebef5eddfc1562bebdd9438c77a22c8e
treeddb2b5e0d5fe8d4e37d05af6c947298d030fd91dtree
parent83ecbc2357ffbb7d0772804c360302ca1daa2400commit | diff
Add simplification option --fo-prop-quant.  Add model support for new model-checking procedure.  Add run script for casc24-fnt.
contrib/run-script-casc24-fnt [new file with mode: 0755] blob
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/Makefile.am diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/first_order_reasoning.cpp [new file with mode: 0755] blob
src/theory/quantifiers/first_order_reasoning.h [new file with mode: 0755] blob
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/full_model_check.h diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/uf/theory_uf_model.h diff | blob | history