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

check if what4 adapter is present before setting timeout #1809

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
+38 −10
Draft

check if what4 adapter is present before setting timeout #1809

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
31 changes: 21 additions & 10 deletions src/Cryptol/Symbolic/What4.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -205,6 +205,17 @@ boolectorOnlineAdapter =
AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions
(Proxy :: Proxy (W4.Writer W4.Boolector))

adapterName :: AnAdapter -> String
adapterName adapter = case adapter of
AnAdapter adapter' -> solver_adapter_name adapter'
AnOnlineAdapter nm _ _ _ -> nm

hasAdapter :: W4ProverConfig -> String -> Bool
hasAdapter cfg nm = case cfg of
W4ProverConfig adapter -> adapterName adapter == nm
W4OfflineConfig -> nm == "w4-offline"
W4Portfolio adapterSet -> any ((== nm) . adapterName) adapterSet

allSolvers :: W4ProverConfig
allSolvers = W4Portfolio
$ z3OnlineAdapter :|
Expand Down Expand Up @@ -419,7 +430,7 @@ satProve solverCfg hashConsing warnUninterp timeoutMs pc@ProverCommand {..} =
globalNonceGenerator
setupAdapterOptions solverCfg w4sym
when hashConsing (W4.startCaching w4sym)
when (timeoutMs > 0) (setTimeout (fromIntegral timeoutMs) w4sym)
when (timeoutMs > 0) (setTimeout solverCfg (fromIntegral timeoutMs) w4sym)
pure w4sym

doLog lg () =
Expand Down Expand Up @@ -766,17 +777,17 @@ varShapeToConcrete evalFn v =
VarEnum <$> W4.groundEval evalFn tag
<*> traverse (traverse (varShapeToConcrete evalFn)) cons

symCfg :: (W4.IsExprBuilder sym, W4.Opt t a) => sym -> W4.ConfigOption t -> a -> IO ()
symCfg sym x y =
symCfg :: (W4.IsExprBuilder sym, W4.Opt t a) => W4ProverConfig -> sym -> String -> W4.ConfigOption t -> a -> IO ()
symCfg cfg sym nm x y = when (hasAdapter cfg nm) $
do opt <- W4.getOptionSetting x (W4.getConfiguration sym)
_ <- W4.trySetOpt opt y
pure ()

setTimeout :: W4.IsExprBuilder sym => Integer -> sym -> IO ()
setTimeout s sym =
do symCfg sym W4.z3Timeout (1000 * s)
symCfg sym W4.cvc4Timeout (1000 * s)
symCfg sym W4.cvc5Timeout (1000 * s)
symCfg sym W4.boolectorTimeout (1000 * s)
symCfg sym W4.yicesGoalTimeout s -- N.B. yices takes seconds
setTimeout :: W4.IsExprBuilder sym => W4ProverConfig -> Integer -> sym -> IO ()
setTimeout cfg s sym =
do symCfg cfg sym "Z3" W4.z3Timeout (1000 * s)
symCfg cfg sym "CVC4" W4.cvc4Timeout (1000 * s)
symCfg cfg sym "CVC5" W4.cvc5Timeout (1000 * s)
symCfg cfg sym "Boolector" W4.boolectorTimeout (1000 * s)
symCfg cfg sym "Yices" W4.yicesGoalTimeout s -- N.B. yices takes seconds
Comment on lines +788 to +792
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of having to enumerate all of the solvers and their timeout options, I wonder if we should do the following:

  1. Add a new field to AnOnlineAdapter (of type ConfigOption BaseIntegerType) to represent the timeout option for a particular solver.
  2. In setTimeout, match on cfg and apply the timeout option for each solver that is contained in the W4ProverConfig.

This approach has the advantage that we wouldn't need to remember to keep the implementation of this function in sync whenever Cryptol adds support for a new SMT solver. (In fact, I suspect that this function is already out of sync, since this function doesn't mention the recently-added Bitwuzla solver anywhere.)

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This makes sense to me, although I think we'll need an auxiliary config option for yices to account for the second/millisecond discrepancy vs. the rest of the solvers.

pure ()
11 changes: 11 additions & 0 deletions tests/issues/issue_1807.icry
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
:set proverTimeout=1

:set prover=w4-cvc5
:prove \(x : Rational) (y : Rational) (z : Rational) -> x < y ==> y < z ==> x < z

:l ../../examples/funstuff/NQueens.cry
:set prover=w4-z3
:sat nQueens : (Solution 50)

:set prover=w4-yices
:sat nQueens : (Solution 50)
6 changes: 6 additions & 0 deletions tests/issues/issue_1807.icry.stdout
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
Loading module Cryptol
Solver returned UNKNOWN
Loading module Cryptol
Loading module Main
Solver returned UNKNOWN
Solver returned UNKNOWN
Loading