From e2e4d7b2bbd9aa01e1888ace96071e5669e54a64 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Tue, 21 Nov 2023 09:33:10 -0800 Subject: [PATCH] Fix #672 --- Data/SBV/Control/Utils.hs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs index 861843146..5f48861b1 100644 --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -1136,9 +1136,10 @@ getAllSatResult = do queryDebug ["*** Checking Satisfiability, all solutions.."] , "*** Please use a solver that supports this feature." ] - topState@State{rUsedKinds, rPartitionVars} <- queryState + topState@State{rUsedKinds, rPartitionVars, rProgInfo} <- queryState - ki <- liftIO $ readIORef rUsedKinds + progInfo <- liftIO $ readIORef rProgInfo + ki <- liftIO $ readIORef rUsedKinds allModelInputs <- getTopLevelInputs allUninterpreteds <- getUIs @@ -1197,17 +1198,19 @@ getAllSatResult = do queryDebug ["*** Checking Satisfiability, all solutions.."] -- We can go fast using the disjoint model trick if things are simple enough: -- - No uninterpreted functions (uninterpreted values are OK) -- - No uninterpreted sorts + -- - No quantifiers -- -- Why can't we support the above? -- - Uninterpreted functions: There is no (standard) way to define a function as a literal in SMTLib. -- Some solvers support lambda, but this isn't common/reliable yet. -- - Uninterpreted sort: There's no way to access the value the solver assigns to an uninterpreted sort. + -- - Quantifiers: Too complicated! -- -- So, if these two things are present, we go the "slow" route, by repeatedly rejecting the -- previous model and asking for a new one. If they don't exist (which is the common case anyhow) -- we use an idea due to z3 folks -- which splits the search space into disjoint models and can produce results much more quickly. - let isSimple = null allUiFuns && null usorts + let isSimple = null allUiFuns && null usorts && not (hasQuants progInfo) start = AllSatResult { allSatMaxModelCountReached = False , allSatSolverReturnedUnknown = False