Skip to content

Make WarnDecidePredicateUnknown an error #1939

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
merged 6 commits into from
Jul 2, 2020
Merged

Make WarnDecidePredicateUnknown an error #1939

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
0975744
Redo everything
andreiburdusa Jul 1, 2020
0b690e7
Add renamed module
andreiburdusa Jul 1, 2020
24d4aa6
Merge branch 'master' into WarnDecidePredicateUnknown-error
andreiburdusa Jul 2, 2020
442d18a
Merge remote-tracking branch 'upstream/master' into WarnDecidePredica…
andreiburdusa Jul 2, 2020
4d92717
Merge branch 'WarnDecidePredicateUnknown-error' of github.com:andreib…
andreiburdusa Jul 2, 2020
79d033e
Stylish
andreiburdusa Jul 2, 2020
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
27 changes: 14 additions & 13 deletions ...rc/Kore/Log/WarnDecidePredicateUnknown.hs → ...c/Kore/Log/ErrorDecidePredicateUnknown.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,9 @@ License : NCSA

-}

module Kore.Log.WarnDecidePredicateUnknown
( WarnDecidePredicateUnknown (..)
, warnDecidePredicateUnknown
module Kore.Log.ErrorDecidePredicateUnknown
( ErrorDecidePredicateUnknown (..)
, errorDecidePredicateUnknown
) where

import Prelude.Kore
Expand All @@ -27,14 +27,14 @@ import Pretty
)
import qualified Pretty

newtype WarnDecidePredicateUnknown =
WarnDecidePredicateUnknown
newtype ErrorDecidePredicateUnknown =
ErrorDecidePredicateUnknown
{ predicates :: NonEmpty (Predicate VariableName)
}
deriving (Show)

instance Pretty WarnDecidePredicateUnknown where
pretty WarnDecidePredicateUnknown { predicates } =
instance Pretty ErrorDecidePredicateUnknown where
pretty ErrorDecidePredicateUnknown { predicates } =
Pretty.vsep
( ["Failed to decide predicate:", Pretty.indent 4 (unparse predicate)]
++ do
Expand All @@ -44,16 +44,17 @@ instance Pretty WarnDecidePredicateUnknown where
where
predicate :| sideConditions = predicates

instance Entry WarnDecidePredicateUnknown where
entrySeverity _ = Warning
helpDoc _ = "warn when the solver cannot decide satisfiability of a formula"
instance Entry ErrorDecidePredicateUnknown where
entrySeverity _ = Error
helpDoc _ =
"errors raised when the solver cannot decide satisfiability of a formula"

warnDecidePredicateUnknown
errorDecidePredicateUnknown
:: MonadLog log
=> InternalVariable variable
=> NonEmpty (Predicate variable)
-> log ()
warnDecidePredicateUnknown predicates' =
logEntry WarnDecidePredicateUnknown { predicates }
errorDecidePredicateUnknown predicates' =
logEntry ErrorDecidePredicateUnknown { predicates }
where
predicates = Predicate.mapVariables (pure toVariableName) <$> predicates'
8 changes: 4 additions & 4 deletions kore/src/Kore/Log/Registry.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,9 @@ import Kore.Log.DebugUnification
import Kore.Log.ErrorBottomTotalFunction
( ErrorBottomTotalFunction
)
import Kore.Log.ErrorDecidePredicateUnknown
( ErrorDecidePredicateUnknown
)
import Kore.Log.ErrorException
( ErrorException
)
Expand All @@ -80,9 +83,6 @@ import Kore.Log.InfoAttemptUnification
import Kore.Log.InfoReachability
( InfoReachability
)
import Kore.Log.WarnDecidePredicateUnknown
( WarnDecidePredicateUnknown
)
import Kore.Log.WarnFunctionWithoutEvaluators
( WarnFunctionWithoutEvaluators
)
Expand Down Expand Up @@ -132,7 +132,7 @@ entryHelpDocs :: [Pretty.Doc ()]
, mk $ Proxy @DebugAppliedRewriteRules
, mk $ Proxy @DebugSubstitutionSimplifier
, mk $ Proxy @ErrorBottomTotalFunction
, mk $ Proxy @WarnDecidePredicateUnknown
, mk $ Proxy @ErrorDecidePredicateUnknown
, mk $ Proxy @WarnFunctionWithoutEvaluators
, mk $ Proxy @WarnSymbolSMTRepresentation
, mk $ Proxy @DebugEvaluateCondition
Expand Down
6 changes: 3 additions & 3 deletions kore/src/Kore/Step/SMT/Evaluator.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,8 +66,8 @@ import Kore.Log.DebugEvaluateCondition
( debugEvaluateConditionResult
, whileDebugEvaluateCondition
)
import Kore.Log.WarnDecidePredicateUnknown
( warnDecidePredicateUnknown
import Kore.Log.ErrorDecidePredicateUnknown
( errorDecidePredicateUnknown
)
import qualified Kore.Profiler.Profile as Profile
( smtDecision
Expand Down Expand Up @@ -191,7 +191,7 @@ decidePredicate predicates =
Unsat -> return False
Sat -> empty
Unknown -> do
warnDecidePredicateUnknown predicates
errorDecidePredicateUnknown predicates
empty

translatePredicate
Expand Down