diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-07 15:45:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-07 20:45:39 +0000 |
commit | 8f9f8a79a55a7c478f8d26894f4d2e7023c5a39c (patch) | |
tree | 8ccad126d323167ea5e6615f8163fa7998f19626 /src/theory/uf | |
parent | bd0cf32db7d115e52e243b165a26edb319e91316 (diff) |
Set incomplete if not applying ho extensionality (#6281)
If the user manually disables ho-extensionality via expert option --no-uf-ho-ext, we should answer "unknown" instead of "sat" when applicable.
Fixes #4318.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/ho_extension.cpp | 29 |
1 files changed, 19 insertions, 10 deletions
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index ebbc75e00..ee3753e92 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -202,12 +202,14 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) << isCollectModel << "..." << std::endl; std::map<TypeNode, std::vector<Node> > func_eqcs; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); + bool hasFunctions = false; while (!eqcs_i.isFinished()) { Node eqc = (*eqcs_i); TypeNode tn = eqc.getType(); if (tn.isFunction()) { + hasFunctions = true; // if during collect model, must have an infinite type // if not during collect model, must have a finite type if (tn.isInterpretedFinite() != isCollectModel) @@ -219,6 +221,16 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) } ++eqcs_i; } + if (!options::ufHoExt()) + { + // we are not applying extensionality, thus we are incomplete if functions + // are present + if (hasFunctions) + { + d_im.setIncomplete(); + } + return 0; + } for (std::map<TypeNode, std::vector<Node> >::iterator itf = func_eqcs.begin(); itf != func_eqcs.end(); @@ -403,17 +415,14 @@ unsigned HoExtension::check() } } while (num_facts > 0); - if (options::ufHoExt()) - { - unsigned num_lemmas = 0; + unsigned num_lemmas = 0; - num_lemmas = checkExtensionality(); - if (num_lemmas > 0) - { - Trace("uf-ho") << "...extensionality returned " << num_lemmas - << " lemmas." << std::endl; - return num_lemmas; - } + num_lemmas = checkExtensionality(); + if (num_lemmas > 0) + { + Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas." + << std::endl; + return num_lemmas; } Trace("uf-ho") << "...finished check higher order." << std::endl; |