projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 50edf18) | patch
Do not handle universal quantification on functions in model-based FMF (#4226)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 2 Jun 2020 17:22:17 +0000 (12:22 -0500)
committerGitHub <noreply@github.com>
Tue, 2 Jun 2020 17:22:17 +0000 (12:22 -0500)
commite4926117ce53433e59f4b1a86892ea43a01f709d
tree87e12c44b133a4998f38a5988610fe4fdffb82d9tree
parent50edf184492d20f4acb7b8d82f3843f3146f77d5commit | diff
Do not handle universal quantification on functions in model-based FMF (#4226)

Fixes #4225, fixes CVC4/cvc4-projects#159, fixes CVC4/cvc4-projects#157, fixes #4289, fixes #4483.

This makes it so that the main model-based instantiation algorithm is not applied to quantified formulas with universally quantified functions.

Identation changed in a FMF function, this was refactored to conform to guidelines, and further cleaned.
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
src/theory/quantifiers/fmf/full_model_check.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/fmf/issue4225-univ-fun.smt2 [new file with mode: 0644] blob