summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/equality_infer.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-08-15 16:30:07 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-08-15 16:30:07 -0500
commit20fc32c0c4a2518673e1cbaa0afb3c4fb284ffe6 (patch)
treeb2698ac7cd23f9336d6b82489547caf788f4db59 /src/theory/quantifiers/equality_infer.h
parentbaaab488c597e3e30dd3b929a5a612ba7fd660af (diff)
Expression sharing on demand in LFSC (replace definitionally equivalent child arguments after successful comparison).
Diffstat (limited to 'src/theory/quantifiers/equality_infer.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback