summaryrefslogtreecommitdiff
path: root/src/theory/rep_set.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-10-04 18:54:45 -0500
committerAina Niemetz <aina.niemetz@gmail.com>2017-10-04 16:54:45 -0700
commit01c540202392fad77ee32c65e065257890c8d07e (patch)
tree476d5e0bc2a1cac056a7904e381750b9b4f50f8e /src/theory/rep_set.h
parentf2bd626d6337ca4df70c0bf541d7d9bec4ef5be5 (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.
Diffstat (limited to 'src/theory/rep_set.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback