Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Reducer refactor #211

Merged
merged 6 commits into from
Oct 3, 2023
Merged

Reducer refactor #211

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
07f274a
Defining new, easier to read, functions for combining reducers
Sep 21, 2023
0817c55
Adjusted quasiquote reducer
Sep 21, 2023
899dba7
Cleaning up Reducers
Sep 22, 2023
0eeee9d
Documentation
Sep 25, 2023
f3ea3fa
documentation
Sep 25, 2023
10eeef2
cleanup
Sep 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 5 additions & 8 deletions src/G2/Equiv/G2Calls.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@
import G2.Lib.Printers
import qualified G2.Language.ExprEnv as E
import qualified G2.Language.Stack as S
import qualified G2.Language.Typing as TY

Check warning on line 31 in src/G2/Equiv/G2Calls.hs

View workflow job for this annotation

GitHub Actions / build (9.6.1, 3.10, test-g2q, -support-lh) 

The qualified import of ‘G2.Language.Typing’ is redundant

Check warning on line 31 in src/G2/Equiv/G2Calls.hs

View workflow job for this annotation

GitHub Actions / build (9.6.1, 3.10, test, -support-lh) 

The qualified import of ‘G2.Language.Typing’ is redundant
import G2.Solver
import G2.Equiv.Config

Expand Down Expand Up @@ -90,16 +90,13 @@
state_name = Name "state" Nothing 0 Nothing

m_logger = fmap SomeReducer $ getLogger config
some_std_red = enforceProgressRed :== NoProgress --> stdRed share retReplaceSymbFuncVar solver simplifier
extra_red = symbolicSwapperRed h_opp track_opp ~> concSymReducer use_labels ~> labeledErrorsRed
red = equivReducer :== NoProgress .--> extra_red :== NoProgress .--> some_std_red
in
(case m_logger of
Just logger -> SomeReducer (
(stdRed share retReplaceSymbFuncVar solver simplifier <~?
enforceProgressRed) <~? labeledErrorsRed <~ concSymReducer use_labels <~ symbolicSwapperRed h_opp track_opp) .<~?
(logger .<~ SomeReducer equivReducer)
Nothing -> SomeReducer (
((stdRed share retReplaceSymbFuncVar solver simplifier <~?
enforceProgressRed) <~? labeledErrorsRed <~ concSymReducer use_labels <~ symbolicSwapperRed h_opp track_opp) <~?
equivReducer)
Just logger -> logger .~> red
Nothing -> red
, SomeHalter
(discardIfAcceptedTagHalter state_name
<~> enforceProgressHalter
Expand Down
6 changes: 2 additions & 4 deletions src/G2/Execution/Interface.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,14 +10,12 @@ import G2.Execution.Reducer
import G2.Execution.Rules
import G2.Language.Support

import Control.Monad.IO.Class

{-# INLINE runExecutionToProcessed #-}
runExecutionToProcessed :: (MonadIO m, Ord b) => Reducer m rv t -> Halter m hv t -> Orderer sov b t -> State t -> Bindings -> m (Processed (State t), Bindings)
runExecutionToProcessed :: (Monad m, Ord b) => Reducer m rv t -> Halter m hv t -> Orderer sov b t -> State t -> Bindings -> m (Processed (State t), Bindings)
runExecutionToProcessed = runReducer

{-# INLINE runExecution #-}
runExecution :: (MonadIO m, Ord b) => Reducer m rv t -> Halter m hv t -> Orderer sov b t -> State t -> Bindings -> m ([State t], Bindings)
runExecution :: (Monad m, Ord b) => Reducer m rv t -> Halter m hv t -> Orderer sov b t -> State t -> Bindings -> m ([State t], Bindings)
runExecution r h ord s b = do
(pr, b') <- runReducer r h ord s b
return (accepted pr, b')
214 changes: 115 additions & 99 deletions src/G2/Execution/Reducer.hs
View file
Open in desktop

Large diffs are not rendered by default.

23 changes: 9 additions & 14 deletions src/G2/Interface/Interface.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -262,24 +262,22 @@ initRedHaltOrd solver simplifier config =
state_name = Name "state" Nothing 0 Nothing

m_logger = fmap SomeReducer $ getLogger config

logger_std_red f = case m_logger of
Just logger -> logger .~> SomeReducer (stdRed share f solver simplifier)
Nothing -> SomeReducer (stdRed share f solver simplifier)
in
case higherOrderSolver config of
AllFuncs ->
(SomeReducer (nonRedPCRed)
.<~| (case m_logger of
Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier) .<~ logger
Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier))
( logger_std_red retReplaceSymbFuncVar .== Finished .--> SomeReducer nonRedPCRed
, SomeHalter
(switchEveryNHalter 20
<~> maxOutputsHalter (maxOutputs config)
<~> zeroHalter (steps config)
<~> acceptIfViolatedHalter)
, SomeOrderer $ pickLeastUsedOrderer)
SingleFunc ->
( SomeReducer (nonRedPCRed <~| taggerRed state_name)
.<~| (case m_logger of
Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier) .<~ logger
Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier))
( logger_std_red retReplaceSymbFuncVar .== Finished .--> taggerRed state_name :== Finished --> nonRedPCRed
, SomeHalter
(discardIfAcceptedTagHalter state_name
<~> switchEveryNHalter 20
Expand All @@ -288,10 +286,7 @@ initRedHaltOrd solver simplifier config =
<~> acceptIfViolatedHalter)
, SomeOrderer $ pickLeastUsedOrderer)
SymbolicFunc ->
(SomeReducer (nonRedPCRed)
.<~| (case m_logger of
Just logger -> SomeReducer (stdRed share retReplaceSymbFuncTemplate solver simplifier) .<~ logger
Nothing -> SomeReducer (stdRed share retReplaceSymbFuncTemplate solver simplifier))
( logger_std_red retReplaceSymbFuncTemplate .== Finished .--> SomeReducer nonRedPCRed
, SomeHalter
(switchEveryNHalter 20
<~> maxOutputsHalter (maxOutputs config)
Expand Down Expand Up @@ -437,7 +432,7 @@ runG2WithSomes red hal ord solver simplifier mem state bindings =
runG2Pre :: ( Named t
, ASTContainer t Expr
, ASTContainer t Type) => MemConfig -> State t -> Bindings -> (State t, Bindings)
runG2Pre mem s@(State { known_values = kv, type_classes = tc }) bindings =
runG2Pre mem s bindings =
let
(swept, bindings') = markAndSweepPreserving mem s bindings
in
Expand Down Expand Up @@ -470,7 +465,7 @@ runG2Post red hal ord solver simplifier is bindings = do
, Ord b) => Reducer (SM.StateT PrettyGuide IO) rv t -> Halter (SM.StateT PrettyGuide IO) hv t -> Orderer sov b t ->
MemConfig -> State t -> Bindings -> SM.StateT PrettyGuide IO ([State t], Bindings) #-}
runG2ThroughExecution ::
( MonadIO m
( Monad m
, Named t
, ASTContainer t Expr
, ASTContainer t Type
Expand Down
12 changes: 6 additions & 6 deletions src/G2/Liquid/G2Calls.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@ checkAbstracted' g2call solver simplifier share s bindings abs_fc@(FuncCall { fu

let pres = HS.fromList $ namesList s' ++ namesList bindings
(er, bindings') <- g2call
(SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~ hitsLibError))
(SomeReducer (hitsLibError ~> stdRed share retReplaceSymbFuncVar solver simplifier))
(SomeHalter (swhnfHalter <~> acceptOnlyOneHalter <~> switchEveryNHalter 200))
(SomeOrderer (incrAfterN 2000 (adtSizeOrderer 0 Nothing)))
solver simplifier
Expand Down Expand Up @@ -181,8 +181,8 @@ getAbstracted g2call solver simplifier share s bindings abs_fc@(FuncCall { funcN
, track = ([] :: [FuncCall], False)}

(er, bindings') <- g2call
(SomeReducer ((nonRedPCRed .|. nonRedPCRedConst)
<~| (stdRed share retReplaceSymbFuncVar solver simplifier <~ hitsLibErrorGatherer)))
(((hitsLibErrorGatherer ~> stdRed share retReplaceSymbFuncVar solver simplifier) :== Finished
--> (nonRedPCRed .|. nonRedPCRedConst) ))
(SomeHalter (swhnfHalter <~> acceptOnlyOneHalter <~> switchEveryNHalter 200))
(SomeOrderer (incrAfterN 2000 (adtSizeOrderer 0 Nothing)))
solver simplifier
Expand Down Expand Up @@ -325,7 +325,7 @@ reduceCalls g2call solver simplifier config bindings er = do

reduceViolated :: (Solver solver, Simplifier simplifier) => G2Call solver simplifier -> solver -> simplifier -> Sharing -> Bindings -> ExecRes LHTracker -> IO (Bindings, ExecRes LHTracker)
reduceViolated g2call solver simplifier share bindings er@(ExecRes { final_state = s, violated = Just v }) = do
let red = SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| redArbErrors)
let red = redArbErrors :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
(s', bindings', v') <- reduceFuncCall g2call red solver simplifier s bindings v
-- putStrLn $ "v = " ++ show v
-- putStrLn $ "v' = " ++ show v'
Expand All @@ -337,7 +337,7 @@ reduceViolated _ _ _ _ b er = return (b, er)
reduceAbstracted :: (Solver solver, Simplifier simplifier) => G2Call solver simplifier -> solver -> simplifier -> Sharing -> Bindings -> ExecRes LHTracker -> IO (Bindings, ExecRes LHTracker)
reduceAbstracted g2call solver simplifier share bindings
er@(ExecRes { final_state = (s@State { track = lht}) }) = do
let red = SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| redArbErrors)
let red = redArbErrors :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
fcs = abstract_calls lht

((s', bindings'), fcs') <- mapAccumM (\(s_, b_) fc -> do
Expand Down Expand Up @@ -375,7 +375,7 @@ reduceFuncCallMaybeList :: ( ASTContainer t Expr
, Solver solver
, Simplifier simplifier) => G2Call solver simplifier -> solver -> simplifier -> Sharing -> Bindings -> State t -> [FuncCall] -> IO (State t, Bindings, [FuncCall])
reduceFuncCallMaybeList g2call solver simplifier share bindings st fcs = do
let red = SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| redArbErrors)
let red = redArbErrors :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
((s', b'), fcs') <- mapAccumM (\(s, b) fc -> do
s_b_fc <- reduceFuncCallMaybe g2call red solver simplifier s b fc
case s_b_fc of
Expand Down
47 changes: 26 additions & 21 deletions src/G2/Liquid/Inference/G2Calls.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -412,11 +412,12 @@ gatherReducerHalterOrderer infconfig config lhconfig solver simplifier = do

timer_halter <- stdTimerHalter (timeout_se infconfig * 3)

let red = case m_logger of
Just logger -> logger .~> SomeReducer (gathererReducer ~> stdRed share retReplaceSymbFuncVar solver simplifier)
Nothing -> SomeReducer (gathererReducer ~> stdRed share retReplaceSymbFuncVar solver simplifier)

return
(SomeReducer (nonRedPCRed <~| taggerRed state_name)
.<~| (case m_logger of
Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~ gathererReducer) .<~ logger
Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~ gathererReducer))
(red .== Finished .--> (taggerRed state_name :== Finished --> nonRedPCRed)
, SomeHalter
(discardIfAcceptedTagHalter state_name
<~> switchEveryNHalter (switch_after lhconfig)
Expand Down Expand Up @@ -542,19 +543,20 @@ inferenceReducerHalterOrderer infconfig config lhconfig solver simplifier entry
<~> lhSWHNFHalter
<~> timer_halter
<~> lh_timer_halter
let some_red = SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier
<~ higherOrderCallsRed
<~ allCallsRed
<~| redArbErrors
<~| lhRed cfn
<~? existentialInstRed)
let some_red = existentialInstRed :== NoProgress .-->
lhRed cfn :== Finished .-->
redArbErrors :== Finished .-->
SomeReducer (allCallsRed ~>
higherOrderCallsRed ~>
stdRed share retReplaceSymbFuncVar solver simplifier)

return $
(SomeReducer (nonRedAbstractReturnsRed <~| taggerRed abs_ret_name)
.<~| (SomeReducer (nonRedPCRed <~| taggerRed state_name))
.<~| (case m_logger of
Just logger -> some_red .<~ logger
Nothing -> some_red)
(
(case m_logger of
Just logger -> logger .~> some_red
Nothing -> some_red) .== Finished .-->
(taggerRed state_name :== Finished --> nonRedPCRed) .== Finished .-->
(taggerRed abs_ret_name :== Finished --> nonRedAbstractReturnsRed)
, SomeHalter
(discardIfAcceptedTagHalter state_name <~> halter)
, SomeOrderer (incrAfterN 2000 (quotTrueAssert (ordComb (+) (pcSizeOrderer 0) (adtSizeOrderer 0 (Just instFuncTickName))))))
Expand Down Expand Up @@ -626,13 +628,16 @@ realCExReducerHalterOrderer infconfig config lhconfig entry modname solver simpl
<~> zeroHalter (0 + extra_depth)
<~> lhAcceptIfViolatedHalter
<~> timer_halter

lh_std_red = lhRed cfn :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
log_opt_red = case m_logger of
Just logger -> logger .~> lh_std_red
Nothing -> lh_std_red

return $
(SomeReducer (nonRedAbstractReturnsRed <~| taggerRed abs_ret_name)
.<~| (SomeReducer (nonRedPCRed <~| taggerRed state_name))
.<~| (case m_logger of
Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn) .<~ logger
Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn))
(log_opt_red .== Finished .-->
(taggerRed state_name :== Finished --> nonRedPCRed) .== Finished .-->
(taggerRed abs_ret_name :== Finished --> nonRedAbstractReturnsRed)
, SomeHalter
(discardIfAcceptedTagHalter state_name <~> halter)
, SomeOrderer (incrAfterN 1000 (adtSizeOrderer 0 Nothing)))
Expand Down Expand Up @@ -1095,7 +1100,7 @@ genericG2CallLogging config solver s bindings lg = do
let simplifier = IdSimplifier
share = sharing config

fslb <- runG2WithSomes (SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~ prettyLogger lg))
fslb <- runG2WithSomes (SomeReducer (prettyLogger lg ~> stdRed share retReplaceSymbFuncVar solver simplifier))
(SomeHalter swhnfHalter)
(SomeOrderer nextOrderer)
solver simplifier PreserveAllMC s bindings
Expand Down
21 changes: 11 additions & 10 deletions src/G2/Liquid/Interface.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -445,13 +445,16 @@ lhReducerHalterOrderer config lhconfig solver simplifier entry mb_modname cfn st
non_red = nonRedPCRed .|. nonRedPCRedConst

m_logger = fmap SomeReducer $ getLogger config

lh_std_red = existentialInstRed :== NoProgress .--> lhRed cfn :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
opt_logger_red = case m_logger of
Just logger -> logger .~> lh_std_red
Nothing -> lh_std_red
in
if higherOrderSolver config == AllFuncs then
( SomeReducer non_red
.<~| (SomeReducer (nonRedAbstractReturnsRed <~| taggerRed abs_ret_name))
.<~| (case m_logger of
Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn <~? existentialInstRed) .<~ logger
Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn <~? existentialInstRed))
(opt_logger_red .== Finished .-->
(taggerRed abs_ret_name :== Finished --> nonRedAbstractReturnsRed) .== Finished .-->
SomeReducer non_red
, SomeHalter
(maxOutputsHalter (maxOutputs config)
<~> zeroHalter (steps config)
Expand All @@ -461,11 +464,9 @@ lhReducerHalterOrderer config lhconfig solver simplifier entry mb_modname cfn st
<~> lhAcceptIfViolatedHalter)
, SomeOrderer lhLimitByAcceptedOrderer)
else
(SomeReducer (nonRedAbstractReturnsRed <~| taggerRed abs_ret_name)
.<~| (SomeReducer (non_red <~| taggerRed state_name))
.<~| (case m_logger of
Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn <~? existentialInstRed) .<~ logger
Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn <~? existentialInstRed))
(opt_logger_red .== Finished .-->
((taggerRed state_name :== Finished --> non_red)) .== Finished .-->
(taggerRed abs_ret_name :== Finished --> nonRedAbstractReturnsRed)
, SomeHalter
(discardIfAcceptedTagHalter state_name
<~> discardIfAcceptedTagHalter abs_ret_name
Expand Down
4 changes: 1 addition & 3 deletions src/G2/QuasiQuotes/QuasiQuotes.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -277,9 +277,7 @@ qqRedHaltOrd config solver simplifier =

state_name = G2.Name "state" Nothing 0 Nothing
in
( SomeReducer
(nonRedPCRed <~| taggerRed state_name)
.<~| (SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier))
( taggerRed state_name :== Finished .--> nonRedPCRed :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
, SomeHalter
(discardIfAcceptedTagHalter state_name
<~> acceptIfViolatedHalter)
Expand Down
Loading