projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a8623b2) | patch
Add additional check to avoid cyclic substitution (#7991)
authorGereon Kremer <gkremer@stanford.edu>
Wed, 2 Feb 2022 18:51:20 +0000 (10:51 -0800)
committerGitHub <noreply@github.com>
Wed, 2 Feb 2022 18:51:20 +0000 (18:51 +0000)
commit9617530df28b3d0ae75da349e956ca427cf02c75
tree86c5847316f7973a4a165f2ed9b4ae6d433a6ed3tree
parenta8623b22f6f8d28191f090f8f5456540d9cb0a18commit | diff
Add additional check to avoid cyclic substitution (#7991)

The substitutions we extract from equalities in the nonlinear solver would sometimes generate cyclic substitutions.
This PR tries harder to avoid such cases.
Fixes cvc5/cvc5-projects#444.
src/theory/arith/nl/equality_substitution.cpp diff | blob | history
src/theory/substitutions.cpp diff | blob | history
src/theory/substitutions.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/proj-issue-444-memout-eqelim.smt2 [new file with mode: 0644] blob