Skip to content

Commit

Permalink
Make auto gas configurable
Browse files Browse the repository at this point in the history
  • Loading branch information
isovector committed Apr 24, 2021
1 parent 828c0fc commit 0156bac
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion plugins/hls-tactics-plugin/src/Wingman/Auto.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@

module Wingman.Auto where

import Control.Monad.Reader.Class (asks)
import Control.Monad.State (gets)
import qualified Data.Set as S
import Refinery.Tactic
Expand All @@ -17,13 +19,14 @@ auto :: TacticsM ()
auto = do
jdg <- goal
skolems <- gets ts_skolems
gas <- asks $ cfg_auto_gas . ctxConfig
current <- getCurrentDefinitions
traceMX "goal" jdg
traceMX "ctx" current
traceMX "skolems" skolems
commit knownStrategies
. tracing "auto"
. localTactic (auto' 4)
. localTactic (auto' gas)
. disallowing RecursiveCall
. S.fromList
$ fmap fst current
Expand Down

0 comments on commit 0156bac

Please sign in to comment.