projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 86ad2ca) | patch
Improvements to --macros-quant. Enable --clause-split by default. Bug fix for cbqi...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 12 Aug 2015 05:33:16 +0000 (07:33 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 12 Aug 2015 05:33:16 +0000 (07:33 +0200)
commita582fa3ea1de3b6419797bbebdcb415ff4d0c0d0
treea81ebb13ad391082ce781c885b9302fe27a30997tree
parent86ad2ca93048844eedcafd2a2dadc43ef85dfb32commit | diff
Improvements to --macros-quant. Enable --clause-split by default. Bug fix for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.
19 files changed:
src/Makefile.am diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.h diff | blob | history
src/theory/quantifiers/macros.cpp diff | blob | history
src/theory/quantifiers/macros.h diff | blob | history
src/theory/quantifiers/modes.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/options_handlers.h diff | blob | history
src/theory/quantifiers/quant_equality_engine.cpp [new file with mode: 0755] blob
src/theory/quantifiers/quant_equality_engine.h [new file with mode: 0755] blob
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/nested-delta.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/nested-inf.smt2 [new file with mode: 0644] blob