Simplify quantifiers strategy for when to apply last call effort check with fmfBound...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 30 Jun 2020 16:12:39 +0000 (11:12 -0500)
committerGitHub <noreply@github.com>
Tue, 30 Jun 2020 16:12:39 +0000 (11:12 -0500)
commitf9e61ad68d6e5811c7471fa36061b50709ab2fa3
tree88515d22b969dc8c69486517050b4071b7ae6a93
parent724d8cf23ae74158b36b408643298c49c3b20833
Simplify quantifiers strategy for when to apply last call effort check with fmfBound (#4673)

There was a strategy in place for alternating which rounds quantifier instantiation would run on when --fmf-bound is enabled.

However, this made it so that in some cases, no instantiation strategy would be applied, if e.g. fmfBound was enabled but no quantified formulas were handled by that strategy.

It is not clear if this strategy is a good idea, considering all use cases of quantifiers, and hence this PR deletes this block of code.

This makes it so that several eqrange benchmarks are answered "unsat" quickly.
src/theory/quantifiers_engine.cpp
test/regress/CMakeLists.txt
test/regress/regress1/quantifiers/eqrange_ex_1.smt2 [new file with mode: 0644]