projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1694c6b) | patch
Fixes for relational triggers (#2967)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 9 May 2019 14:33:22 +0000 (09:33 -0500)
committerGitHub <noreply@github.com>
Thu, 9 May 2019 14:33:22 +0000 (09:33 -0500)
commit9e26baaaa717a5075984c63878e8bc1aa4e78b16
tree91a0297c538928289b068e28550cbb98602c492ftree
parent1694c6b45dfa02ca22146755c89078bfa6b851efcommit | diff
Fixes for relational triggers (#2967)
15 files changed:
src/options/quantifiers_options.toml diff | blob | history
src/theory/quantifiers/ematching/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.h diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/nl-pow-trick.smt2 diff | blob | history
test/regress/regress1/quantifiers/seu169+1.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/var-eq-trigger-simple.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/var-eq-trigger.smt2 [new file with mode: 0644] blob
test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2 [new file with mode: 0644] blob