Skip to content

add --numsolvers to control the size of the solver pool #232

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

Merged
lefterislazar merged 3 commits into from
Aug 10, 2026
Merged

add --numsolvers to control the size of the solver pool #232

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ee36734
add --numsolvers to control the size of the solver pool
mijovic Aug 4, 2026
453fb34
add numsolvers flag to the docs
anjapetkovic Aug 6, 2026
2a216e8
Comment clean up
lefterislazar Aug 10, 2026
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
1 change: 1 addition & 0 deletions doc/src/equiv.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ act equiv --spec <PATH_TO_SPEC> --code <RUNTIME_BYTECODE> --initcode <CONSTR_BYT
| `--solver` | `cvc5\|z3\|bitwuzla` | `cvc5` | SMT solver to use for verification |
| `--smttimeout` | Integer (ms) | `20000` | Timeout for each SMT query in milliseconds |
| `--debug` | Boolean | `false` | Print verbose output including raw SMT queries |
| `--numsolvers` | Integer | number of cores | Number of solver instances to run in parallel |

<!-- | `--code` | ByteString | - | Runtime bytecode (hexadecimal) for direct verification | -->
<!-- | `--initcode` | ByteString | - | Constructor bytecode (hexadecimal) | -->
Expand Down
13 changes: 8 additions & 5 deletions src/Act/CLI.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,7 @@ data Command w
, solver :: w ::: Maybe Text <?> "SMT solver: cvc5 (default) or z3"
, smttimeout :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 20000)"
, debug :: w ::: Bool <?> "Print verbose SMT output (default: False)"
, numsolvers :: w ::: Maybe Int <?> "Number of solver instances to run in parallel (default: number of cores)"
}
deriving (Generic)

Expand Down Expand Up @@ -132,9 +133,9 @@ main = do
Lean f jsn solver' smttimeout' debug' -> do
solver'' <- parseSolver solver'
lean' f jsn solver'' smttimeout' debug'
Equiv spec' sol' vy' code' initcode' layout' sources' solver' smttimeout' debug' -> do
Equiv spec' sol' vy' code' initcode' layout' sources' solver' smttimeout' debug' numsolvers' -> do
solver'' <- parseSolver solver'
equivCheck spec' sol' vy' code' initcode' layout' sources' solver'' smttimeout' debug'
equivCheck spec' sol' vy' code' initcode' layout' sources' solver'' smttimeout' debug' numsolvers'


---------------------------------
Expand Down Expand Up @@ -199,10 +200,12 @@ lean' f jsn solver' smttimeout' debug' = do
TIO.putStr $ lean spec'


equivCheck :: Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> Maybe String -> Maybe String -> Maybe String -> Maybe FilePath -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
equivCheck actspec sol' vy' code' initcode' layout' sources' solver' timeout debug' = do
equivCheck :: Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> Maybe String -> Maybe String -> Maybe String -> Maybe FilePath -> Solvers.Solver -> Maybe Integer -> Bool -> Maybe Int -> IO ()
equivCheck actspec sol' vy' code' initcode' layout' sources' solver' timeout debug' numsolvers' = do
let config = if debug' then debugActConfig else defaultActConfig
cores <- liftM fromIntegral getNumProcessors
cores <- case numsolvers' of
Just n | n > 0 -> pure (fromIntegral n)
_ -> liftM fromIntegral getNumProcessors
(actspecs, inputsMap) <- processEquivSources sources' actspec sol' vy' code' initcode' layout'
specsContents <- flip zip actspecs <$> mapM readFile actspecs
proceed specsContents (compile specsContents) $ \(Act store contracts, constraints) -> do
Expand Down
Loading