projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 256d409) | patch
Improvements for CBQI (#1478)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 4 Jan 2018 23:30:25 +0000 (17:30 -0600)
committerAina Niemetz <aina.niemetz@gmail.com>
Thu, 4 Jan 2018 23:30:25 +0000 (15:30 -0800)
commite1df8f68a90c7ba548b2746704b978555ec4283f
treeb3bcea5160fdb6fa38252e20eea7f759a9bfae85tree
parent256d4093ab6ac3b792c6f1f11131124d1ae6b069commit | diff
Improvements for CBQI (#1478)

Includes:

- Basic rewriting for choice functions in the builtin rewriter,
- Do not consider more than one equal term in ceg instantiator (helps cases where we have a
  repeated pattern of duplicate instantiations),
- Do not introduce dummy extract equalities in the cbqi-bv-rm-extract pass (dummy concat
  equalities suffice).
- Do not consider extracts in nested quantified formulas in the cbqi-bv-rm-extract pass.
src/theory/builtin/theory_builtin_rewriter.cpp diff | blob | history
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.h diff | blob | history