projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6ed0dc4) | patch
Do not exhaustive instantiation when FMF is disabled (#6899)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 16 Jul 2021 17:04:39 +0000 (12:04 -0500)
committerGitHub <noreply@github.com>
Fri, 16 Jul 2021 17:04:39 +0000 (17:04 +0000)
commit3d429c1187a2ac7d3270eddbbf5228002ad2740a
treee91884b821d88cddb5b811c02d3a03fa35cb7315tree
parent6ed0dc4e833421e7da9345bda0196c598f852d29commit | diff
Do not exhaustive instantiation when FMF is disabled (#6899)

This makes FMF not handle quantified formulas when FMF options are disabled, apart from those marked internal.

This is required for combinations of sequences + quantified formulas.
src/theory/quantifiers/fmf/model_engine.cpp diff | blob | history
src/theory/quantifiers/fmf/model_engine.h diff | blob | history