projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 50c8533) | patch
Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 10 Nov 2015 13:35:25 +0000 (14:35 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 10 Nov 2015 13:35:37 +0000 (14:35 +0100)
commit81dca680f6c88d10b56a0ed065d470d907766e21
tree4410fa473ecb6848f7976b2b6a00188ac5e44775tree
parent50c8533760bfd5b1f803d52bc4318c544521e6afcommit | diff
Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
29 files changed:
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/type_enumerator.cpp diff | blob | history
src/theory/quantifiers/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/candidate_generator.h diff | blob | history
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.h diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.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/trigger.cpp diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/util/datatype.cpp diff | blob | history
src/util/datatype.h diff | blob | history
test/regress/regress0/datatypes/Makefile.am diff | blob | history
test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/matching-lia-1arg.smt2 [new file with mode: 0644] blob
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/dt-test-ns.sy [new file with mode: 0644] blob