projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6685187) | patch
Make alpha equivalence user context dependent (#7889)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 6 Jan 2022 23:42:14 +0000 (17:42 -0600)
committerGitHub <noreply@github.com>
Thu, 6 Jan 2022 23:42:14 +0000 (23:42 +0000)
commitdfb4a4a988ffcc39f41c5cb9c74c7ffc9ed74513
treecad840d536deef5285f173dc778cd388f40a2112tree
parent668518797aa22f2cb905b4e63397da304ed22967commit | diff
Make alpha equivalence user context dependent (#7889)

Fixes #5373

Issues were occurring due to using quantified formulas in alpha equivalence that were stale.

This also removes spurious warnings from quantifier elimination (dropping the "strict" requirement, which unnecessarily warns if we are in a non-arithmetic logic).
src/api/cpp/cvc5.cpp diff | blob | history
src/smt/solver_engine.cpp diff | blob | history
src/smt/solver_engine.h diff | blob | history
src/theory/quantifiers/alpha_equivalence.cpp diff | blob | history
src/theory/quantifiers/alpha_equivalence.h diff | blob | history
src/theory/quantifiers/cegqi/nested_qe.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_qe_preproc.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/issue5373-1-qe-inc.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/issue5373-2.smt2 [new file with mode: 0644] blob