projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1eb3c6c) | patch
Refactoring and fixes of set defaults for quantifiers (#7120)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 7 Sep 2021 03:41:04 +0000 (22:41 -0500)
committerGitHub <noreply@github.com>
Tue, 7 Sep 2021 03:41:04 +0000 (03:41 +0000)
commit4376ff5bd3df8dabb847d4cd99465f894230fb60
treed6e2b754ac973990606937af9163723ffb48125dtree
parent1eb3c6c8eb3da95cababcc0b1705c0299eee099ccommit | diff
Refactoring and fixes of set defaults for quantifiers (#7120)

This PR further refactors set defaults for incompatibility issues related to quantifiers.

It adds a new restriction that was discovered recently: --nl-rlv should not be used in quantified logics. Some regressions are modified that are impacted by this restriction.

Also does minor rearrangements to the order in which default options are set.
src/smt/set_defaults.cpp diff | blob | history
src/smt/set_defaults.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 diff | blob | history
test/regress/regress1/nl/issue3647.smt2 diff | blob | history
test/regress/regress1/sygus/issue3648.smt2 diff | blob | history