projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f2bd626) | patch
Ho quant util (#1119)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 4 Oct 2017 23:54:45 +0000 (18:54 -0500)
committerAina Niemetz <aina.niemetz@gmail.com>
Wed, 4 Oct 2017 23:54:45 +0000 (16:54 -0700)
commit01c540202392fad77ee32c65e065257890c8d07e
tree476d5e0bc2a1cac056a7904e381750b9b4f50f8etree
parentf2bd626d6337ca4df70c0bf541d7d9bec4ef5be5commit | diff
Ho quant util (#1119)

Quantifiers utilities for higher-order.

This makes the term indexing mechanisms in Term Database take into account equalities between functions, in which case the term indices for the two functions merges.

Also adds required options and a minor utility for implementing app completion.
src/options/quantifiers_options 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_type_rules.h diff | blob | history