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.

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 consistency of constraints before evaluating a pattern #4013

Closed
wants to merge 25 commits into from
Closed
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
99988c1
implment isSat
goodlyrottenapple Jun 27, 2024
f368038
Check constraints for consistency in evaluatePattern'
geo2a Aug 1, 2024
32b08b7
Do not fail on Unknown pattern constraints
geo2a Aug 1, 2024
59bd44b
Ignore prelude check result when running with noSolver
geo2a Aug 1, 2024
fd3ea50
Set FEATURE_SERVER_OPTS to '' if it's unbound
geo2a Aug 1, 2024
bb6a765
Emit more logs from evaluatePattern'
geo2a Aug 1, 2024
29524b8
Check consistency of the pattern before rewriting
geo2a Aug 1, 2024
8852282
Move log message out
geo2a Aug 2, 2024
8f13183
Remove bad hardResetSolver
geo2a Aug 2, 2024
1948b15
Hard reset in the beginning of isSat
geo2a Aug 2, 2024
8bef12a
Update integration test output
geo2a Aug 2, 2024
432ff02
pretty: print substitution as bindings, separate imports
geo2a Aug 5, 2024
7fe9293
Update outputs of booster/test/rpc-integration/test-substitution
geo2a Aug 5, 2024
2483a57
Run test-substitutions with booster-dev
geo2a Aug 5, 2024
25afc73
Use the same code to update SMT options on retries
geo2a Aug 5, 2024
c9f107d
Factor-out and unify failBecauseUnknown
geo2a Aug 5, 2024
2ef21ab
Update comments
geo2a Aug 5, 2024
64147e3
Factor-out duration
geo2a Aug 5, 2024
24b8126
comment
geo2a Aug 5, 2024
10f6b18
Pass initial simplifier cache to performRewrite
geo2a Aug 5, 2024
7f7d667
Correct comments
geo2a Aug 5, 2024
80d1675
Fix unit tests
geo2a Aug 5, 2024
1fce254
Use record field punning to access the constraints
geo2a Aug 6, 2024
d82576f
Improve control-flow in evaluatePattern'
geo2a Aug 6, 2024
575428c
Rename test case
geo2a Aug 6, 2024
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
Prev Previous commit
Next Next commit
Correct comments
  • Loading branch information
geo2a committed Aug 5, 2024
commit 7f7d667f6c7dc2890d565a5315e036d1e67d934b
2 changes: 1 addition & 1 deletion booster/library/Booster/JsonRpc.hs
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,7 @@ respond stateVar request =

case evaluatedInitialPattern of
(Left ApplyEquations.SideConditionFalse{}, _) -> do
-- input pattern's constrains are Bottom, return Bottom
-- input pattern's constraints are Bottom, return Vacuous
stop <- liftIO $ getTime Monotonic
pure $
execResponse
Expand Down
6 changes: 3 additions & 3 deletions booster/library/Booster/Pattern/ApplyEquations.hs
Original file line number Diff line number Diff line change
Expand Up @@ -463,7 +463,7 @@ evaluatePattern' ::
EquationT io Pattern
evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
solver <- (.smtSolver) <$> getConfig
-- check initial constraints for consistency, reporting an error if they are Bottom
-- check the pattern's constraints for consistency, reporting an error if they are Bottom
withContext CtxConstraint
. withContext CtxDetail
. withTermContext (coerce $ collapseAndBools pat.constraints)
Expand All @@ -479,15 +479,15 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
throw . SideConditionFalse . collapseAndBools $ pat.constraints
Left SMT.SMTSolverUnknown{} -> do
-- unlikely case of an Unknown response to a consistency check.
-- What to do here? continue for now to preserver the old behaviour.
-- continue to preserver the old behaviour.
withContext CtxConstraint . logWarn . Text.pack $
"Constraints consistency UNKNOWN: " <> show consistent
continue
Left other ->
-- fail hard on SMT error other than @SMT.SMTSolverUnknown@
liftIO $ Exception.throw other
Right True -> do
-- constrains are consistent, continue
-- constraints are consistent, continue
continue
where
continue = do
Expand Down
Loading