summaryrefslogtreecommitdiff
path: root/test/regress/regress2/sygus/real-grammar-neg.sy
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2020-03-21 12:57:22 -0700
committerGitHub <noreply@github.com>2020-03-21 14:57:22 -0500
commita507aa5f1904055782e1ba01083faf1fd0fb86f7 (patch)
treee31fb4ce520c26efecd1f92b5b14231c46321f59 /test/regress/regress2/sygus/real-grammar-neg.sy
parentd80192cf77c7beeb26c783a2f53064e2eddb654b (diff)
Simplify heuristic in `processNEqc` (#4129)
This commit removes a special case in `CoreSolver::processNEqc()` where we stopped looking for inferences for a given normal form as soon as we found the highest priority inference (currently that an element in the normal form is empty). This effectively elevates the priority of this inference to the other inferences that are done immediately instead of being added to the `pinfer` vector that holds the possible inferences. The experiments that I've run seem to confirm that it is unnecessary to have this special case.
Diffstat (limited to 'test/regress/regress2/sygus/real-grammar-neg.sy')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback