projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ae1d4e4) | patch
Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 30 Jun 2017 14:02:51 +0000 (09:02 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 30 Jun 2017 14:03:20 +0000 (09:03 -0500)
commit303b91f3f5b8df1a884566a7d433ced17f0cd352
treeebe6334ca8a415a4d5a24a83ee40441419c93876tree
parentae1d4e4f05fdc2db61d7de7efee5bd567363ceefcommit | diff
Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
19 files changed:
contrib/run-script-casc26-fnt diff | blob | history
contrib/run-script-casc26-fof diff | blob | history
contrib/run-script-casc26-tfa diff | blob | history
src/parser/tptp/Tptp.g diff | blob | history
src/theory/arrays/theory_arrays_type_rules.h diff | blob | history
src/theory/datatypes/theory_datatypes_type_rules.h diff | blob | history
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/macros.cpp diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history
src/theory/sets/theory_sets_type_rules.h diff | blob | history
src/theory/uf/theory_uf_type_rules.h diff | blob | history
test/regress/regress0/quantifiers/macro-subtype-param.smt2 diff | blob | history
test/regress/regress0/quantifiers/macros-real-arg.smt2 diff | blob | history
test/regress/regress0/quantifiers/subtype-param-unk.smt2 diff | blob | history
test/regress/regress0/quantifiers/subtype-param.smt2 diff | blob | history
test/regress/regress0/sets/sets-poly-nonint.smt2 diff | blob | history
test/regress/regress0/sets/sets-tuple-poly.cvc diff | blob | history