diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-04 22:14:44 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-04 22:14:44 +0200 |
| commit | 97032ee3decc7bed2f2c9e8c32dff99676b658f2 (patch) | |
| tree | a74ca1f09d9fb0acd655d71256b6009fb4e2fc1a /source/Checking/Declaration.hs | |
| parent | 7131eee1a37a8a08f833b33620b2b0dfda32eb4a (diff) | |
Restore implicit set construction routing
Diffstat (limited to 'source/Checking/Declaration.hs')
| -rw-r--r-- | source/Checking/Declaration.hs | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs index 65b7675..f95286c 100644 --- a/source/Checking/Declaration.hs +++ b/source/Checking/Declaration.hs @@ -2817,20 +2817,14 @@ prepareVampireObligationWith globalType builder selection - let (globalMode, localPolicy) = + let premiseSelection = case selection of VampireImplicitPremises -> - ( Backend.ImplicitFofPremises - , Backend.FirstOrderLocals - ) + Backend.ImplicitPremiseSelection VampireExplicitPremises{} -> - ( Backend.ExplicitGlobalPremises - , Backend.FirstOrderLocals - ) + Backend.ExplicitGlobalPremiseSelection VampireLocalPremises -> - ( Backend.NoGlobalPremises - , Backend.AllLocals - ) + Backend.LocalOnlyPremiseSelection propositionDependencies = foundationAxiomDependencies . Backend.supportedPropositionTerm @@ -2846,7 +2840,7 @@ prepareVampireObligationWith (propositionDependencies . Backend.typedLocalPremiseProposition) (Backend.selectTypedLocalPremises - localPolicy + premiseSelection locals) ) auxiliaries = @@ -2861,8 +2855,7 @@ prepareVampireObligationWith claim locals auxiliaries - globalMode - localPolicy) + premiseSelection) task <- first VampireObligationEncodingFailed (Provers.prepareTypedProverTask |