projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2ee190b) | patch
Remove support for inst closure (#5874)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 8 Feb 2021 18:29:58 +0000 (12:29 -0600)
committerGitHub <noreply@github.com>
Mon, 8 Feb 2021 18:29:58 +0000 (12:29 -0600)
commit57919ba7271a6c2b36173f2ba0f580b84f962b1b
tree492fb2ae81e3e29e5ee08a36300a878671d0175ftree
parent2ee190b7b4ead29ef34e3eb115457ff3e21afbabcommit | diff
Remove support for inst closure (#5874)

This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database.

It also simplifies the TermDatabase::addTerm method (which changed indentation).
14 files changed:
src/api/cvc4cpp.cpp diff | blob | history
src/api/cvc4cppkind.h diff | blob | history
src/options/quantifiers_options.toml diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/theory/quantifiers/ematching/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/equality_query.cpp diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/kinds diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers/theory_quantifiers.cpp diff | blob | history
src/theory/quantifiers/theory_quantifiers_type_rules.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history