diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs index dff1985b..a78914db 100644 --- a/src/Cryptol/TypeCheck/Solve.hs +++ b/src/Cryptol/TypeCheck/Solve.hs @@ -109,7 +109,7 @@ proveImplicationIO lname as ps gs = -- XXX: Do we need the su? -- XXX: Minimize the goals invovled in the conflict (us,su2) -> - do debugBlock s "2nd su:" (debugLog s su2) + do debugBlock s "FAILED: 2nd su:" (debugLog s su2) return $ Left $ UnsolvedDelcayedCt $ DelayedCt { dctSource = lname @@ -134,7 +134,8 @@ numericRight g = case Num.exportProp (goal g) of _testSimpGoals :: IO () _testSimpGoals = Num.withSolver $ \s -> - do mb <- simpGoals s gs + do Num.assumeProps s asmps + mb <- simpGoals s gs case mb of Just (gs1,su) -> do debugBlock s "Simplified goals" @@ -142,8 +143,9 @@ _testSimpGoals = Num.withSolver $ \s -> debugLog s (show (pp su)) Nothing -> debugLog s "Impossible" where - gs = map fakeGoal [ tv 1 .*. tv 2 >== tv 1 .*. tv 2 ] - + asmps = [ pFin (tv 1) ] + gs = map fakeGoal [ tv 0 =#= (num 1 .+. tMin (tv 1) (tv 0)) ] + -- ?g4 == 1 + min m ?g4 -- [ tv 0 =#= tInf, tMod (num 3) (tv 0) =#= num 4 ] diff --git a/src/Cryptol/TypeCheck/Solver/CrySAT.hs b/src/Cryptol/TypeCheck/Solver/CrySAT.hs index 81dea976..c274a3df 100644 --- a/src/Cryptol/TypeCheck/Solver/CrySAT.hs +++ b/src/Cryptol/TypeCheck/Solver/CrySAT.hs @@ -11,6 +11,8 @@ module Cryptol.TypeCheck.Solver.CrySAT , DebugLog(..) ) where +import Cryptol.Utils.Debug(trace) + import qualified Cryptol.TypeCheck.AST as Cry import Cryptol.TypeCheck.PP(pp) import Cryptol.TypeCheck.InferTypes(Goal(..)) @@ -28,14 +30,16 @@ import MonadLib import Data.Maybe ( mapMaybe, fromMaybe ) import Data.Map ( Map ) import qualified Data.Map as Map +import Data.Foldable ( any, all ) import Data.Traversable ( traverse ) import Data.Set ( Set ) import qualified Data.Set as Set import Data.IORef ( IORef, newIORef, readIORef, modifyIORef', atomicModifyIORef' ) +import Prelude hiding (any,all) import qualified SimpleSMT as SMT -import Text.PrettyPrint(Doc) +import Text.PrettyPrint(Doc,vcat,text) -- | We use this to rememebr what we simplified newtype SimpProp = SimpProp Prop @@ -44,24 +48,24 @@ simpProp :: Prop -> SimpProp simpProp p = SimpProp (crySimplify p) +-- | 'dpSimpProp' and 'dpSimpExprProp' should be logicaly equivalent, +-- to each other, and to whatever 'a' represenets (usually 'a' is a 'Goal'). data DefinedProp a = DefinedProp { dpData :: a -- ^ Optional data to assocate with prop. -- Often, the origianl `Goal` from which the prop was extracted. , dpSimpProp :: SimpProp - -- ^ Fully simplified (may have ORs) - -- These are used in the proofs, and may not be translatable back - -- into Cryptol. + {- ^ Fully simplified: may mention ORs, and named non-linear terms. + These are what we send to the prover, and we don't attempt to + convert them back into Cryptol types. -} , dpSimpExprProp :: Prop - -- ^ Expressions are simplified (no ORs) - -- These should be importable back into Cryptol props. - -- XXX: What about `sys` variables? + {- ^ A version of the proposition where just the expression terms + have been simplified. These should not contain ORs or named non-linear + terms because we want to import them back into Crytpol types. -} } -type ImpMap = Map Name Expr - {- | Check if a collection of things are defined. It does not modify the solver's state. @@ -124,6 +128,7 @@ checkDefined s updCt uniVars props0 = withScope s (go Map.empty [] props0) Nothing -> (g,p) Just p' -> (updCt p' g,p') + -- Try to prove something by unification (e.g., ?x = a * b) findImpByDef _ [] = Nothing findImpByDef qs (p : ps) = case improveByDefn uniVars p of @@ -427,8 +432,8 @@ getNLSubst Solver { .. } = -- | Execute a computation with a fresh solver instance. withSolver :: (Solver -> IO a) -> IO a withSolver k = - do -- logger <- SMT.newLogger - let logger = quietLogger + do logger <- SMT.newLogger + -- let logger = quietLogger solver <- SMT.newSolver "cvc4" [ "--lang=smt2" , "--incremental" @@ -524,40 +529,38 @@ check s@Solver { .. } uniVars = case res of SMT.Unsat -> return (False, Map.empty) SMT.Unknown -> return (True, Map.empty) - SMT.Sat -> debugBlock s "improvements" (getImpSubst s uniVars) + SMT.Sat -> + do impMap <- debugBlock s "improvements" (getImpSubst s uniVars) + return (True, impMap) --- | The set of unification variables is used to guide ordering of --- assignments (we prefer assigning to them, as that amounts to doing --- type inference). -getImpSubst :: Solver -> Set Name -> IO (Bool,Subst) +{- | The set of unification variables is used to guide ordering of +assignments (we prefer assigning to them, as that amounts to doing +type inference). + +Returns an improving substitution, which may mention the names of +non-linear terms. +-} +getImpSubst :: Solver -> Set Name -> IO Subst getImpSubst s@Solver { .. } uniVars = do names <- viUnmarkedNames `fmap` readIORef declared m <- fmap Map.fromList (mapM getVal names) - model <- cryImproveModel solver uniVars m - nlSu <- getNLSubst s - let su = composeSubst nlSu (toSubst model) + impSu <- cryImproveModel solver uniVars m - -- XXX: The improvemnts that are being ignored here could - -- lead to extar, potentially useful, constraints. - su1 = Map.filterWithKey (\k _ -> case k of - SysName {} -> False - _ -> True) su - return (True, su1) -{- - let imps = Map.toList (toSubst model) - debugBlock s "before" $ - mapM_ (\(x,e) -> debugLog s (Var x :== e)) imps + let isNonLinName (SysName {}) = True + isNonLinName (UserName {}) = False - res <- mapM (checkImpBind s) imps - let (agains,eqs) = unzip res - debugBlock s "after" $ - mapM_ (\(x,e) -> debugLog s (Var x :== e)) (concat eqs) + keep k e = not (isNonLinName k) && + all (not . isNonLinName) (cryExprFVS e) + + (easy,tricky) = Map.partitionWithKey keep impSu + dump (x,e) = debugLog s (show (ppProp (Var x :== e))) + + when (not (Map.null tricky)) $ + debugBlock s "Tricky subst" $ mapM_ dump (Map.toList tricky) + + return easy - (possible,more) <- if or agains then check s uniVars - else return (True,Map.empty) - return (possible, Map.union more (Map.fromList (concat eqs))) --} where getVal a = do yes <- isInf a @@ -575,19 +578,11 @@ getImpSubst s@Solver { .. } uniVars = [ "Not a boolean value", show yes ] --- If subst contains: --- x := e(_y) (where _y = e', a NL term) --- we should replace `x` with `e(e'/_y)`, not just e - --- If subst contains: --- _y := e (where _y = e1, a NL term) --- we get that a new equations should always hold: e = e' --- this is "derived" fact in GHC parlance: if we notice that it is --- impossible, then we can be sure +-- XXX: NOT QUITE, I THINK. -- | Given a computed improvement `x = e`, check to see if we can get -- some additional information by interacting with the non-linear assignment. checkImpBind :: Solver -> (Name, Expr) -> IO (Bool, [(Name,Expr)]) @@ -666,26 +661,6 @@ checkImpBind s (x,e) = --- | Convert a bunch of improving equations into an idempotent substitution. --- Assumes that the equations don't have loops. -toSubst :: ImpMap -> Subst -toSubst m = - case normMap (apSubst m) m of - Nothing -> m - Just m1 -> toSubst m1 - - --- | Apply a function to all elements of a map. Returns `Nothing` if nothing --- changed, and @Just new_map@ otherwise. -normMap :: (a -> Maybe a) -> Map k a -> Maybe (Map k a) -normMap f m = mk $ runId $ runStateT False $ traverse upd m - where - mk (a,changes) = if changes then Just a else Nothing - - upd x = case f x of - Just y -> set True >> return y - Nothing -> return x - -------------------------------------------------------------------------------- debugBlock :: Solver -> String -> IO a -> IO a diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs b/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs index 313be799..d5321091 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs @@ -42,8 +42,15 @@ nonLinProp s0 prop = runNL s0 (nonLinPropM prop) {- | Apply a substituin to the non-linear expression database. Returns `Nothing` if nothing was affected. -Otherwise returns `Just`, and a substitutuin for non-linear expressions -that became linear. -} +Otherwise returns `Just`, and a substitution for non-linear expressions +that became linear. + +The definitions of NL terms do not contain other named NL terms, +so it does not matter if the substitution contains bindings like @_a = e@. + +There should be no bindings that mention NL term names in the definitions +of the substition (i.e, things like @x = _a@ are NOT ok). +-} apSubstNL :: Subst -> NonLinS -> Maybe (Subst, NonLinS) apSubstNL su s0 = case runNL s0 (mApSubstNL su) of (Nothing,_) -> Nothing @@ -81,7 +88,7 @@ Otherwise returns `Just`, and a substituion mapping names that used to be non-linear but became linear. Note that we may return `Just empty`, indicating that some non-linear -expressions were update, but they remained non-linear. -} +expressions were updated, but they remained non-linear. -} mApSubstNL :: Subst -> NonLinM (Maybe Subst) mApSubstNL su = do s <- get diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs b/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs index 84cb2a8c..54fa9f6a 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs @@ -10,16 +10,18 @@ module Cryptol.TypeCheck.Solver.Numeric.SMT import Cryptol.TypeCheck.Solver.InfNat import Cryptol.TypeCheck.Solver.Numeric.AST +import Cryptol.TypeCheck.Solver.Numeric.Simplify(crySimplify) +import Cryptol.Utils.Misc ( anyJust ) import Cryptol.Utils.Panic ( panic ) -import Control.Monad ( ap, guard ) -import Data.List ( partition ) +import Data.List ( partition, unfoldr ) import Data.Map ( Map ) import qualified Data.Map as Map import Data.Set ( Set ) import qualified Data.Set as Set import SimpleSMT ( SExpr ) import qualified SimpleSMT as SMT +import MonadLib -------------------------------------------------------------------------------- @@ -113,7 +115,7 @@ propToSmtLib prop = _ :> _ -> unexpected where - unexpected = panic "desugarProp" [ show (ppProp prop) ] + unexpected = panic "propToSmtLib" [ show (ppProp prop) ] fin x = SMT.const (smtFinName x) addFin e = foldr (\x' e' -> SMT.and (fin x') e') e @@ -160,11 +162,43 @@ smtFinName x = "fin_" ++ show (ppName x) -- Models -------------------------------------------------------------------------------- +-- | Get the value for the given variable. +-- Assumes that we are in a SAT state. +getVal :: SMT.Solver -> Name -> IO Expr +getVal s a = + do yes <- isInf a + if yes + then return (K Inf) + else do v <- SMT.getConst s (smtName a) + case v of + SMT.Int x | x >= 0 -> return (K (Nat x)) + _ -> panic "cryCheck.getVal" [ "Not a natural number", show v ] + + where + isInf v = do yes <- SMT.getConst s (smtFinName v) + case yes of + SMT.Bool ans -> return (not ans) + _ -> panic "cryCheck.isInf" + [ "Not a boolean value", show yes ] +-- | Get the values for the given names. +getVals :: SMT.Solver -> [Name] -> IO (Map Name Expr) +getVals s xs = + do es <- mapM (getVal s) xs + return (Map.fromList (zip xs es)) -{- | Given a model, compute a set of equations of the form `x = e`, -that are impleied by the model. These have the form: + +-- | Convert a bunch of improving equations into an idempotent substitution. +-- Assumes that the equations don't have loops. +toSubst :: Map Name Expr -> Subst +toSubst m0 = last (m0 : unfoldr step m0) + where step m = do m1 <- anyJust (apSubst m) m + return (m1,m1) + + +{- | Given a model, compute an improving substitution, implied by the model. +The entries in the substitution look like this: * @x = A@ variable @x@ must equal constant @A@ @@ -177,8 +211,7 @@ that are impleied by the model. These have the form: cryImproveModel :: SMT.Solver -> Set Name -> Map Name Expr -> IO (Map Name Expr) -cryImproveModel solver uniVars m = go Map.empty initialTodo - -- XXX: Hook in linRel +cryImproveModel solver uniVars m = toSubst `fmap` go Map.empty initialTodo where -- Process unification variables first. That way, if we get `x = y`, we'd -- prefer `x` to be a unificaiton variabl. @@ -190,20 +223,42 @@ cryImproveModel solver uniVars m = go Map.empty initialTodo go done ((x,e) : rest) = -- x = K? - do yesK <- cryMustEqualK solver x e - if yesK - then go (Map.insert x e done) rest - else goV done [] x e rest + do mbCounter <- cryMustEqualK solver (Map.keys m) x e + case mbCounter of + Nothing -> go (Map.insert x e done) rest + Just ce -> goV ce done [] x e rest - goV done todo x e ((y,e') : more) + goV ce done todo x e ((y,e') : more) -- x = y? | e == e' = do yesK <- cryMustEqualV solver x y if yesK then go (Map.insert x (Var y) done) (reverse todo ++ more) - else goV done ((y,e'):todo) x e more - | otherwise = goV done ((y,e') : todo) x e more + else tryLR + + | otherwise = next + + where + next = goV ce done ((y,e'):todo) x e more + + tryLR = + case ( x `Set.member` uniVars + , e + , e' + , Map.lookup x ce + , Map.lookup y ce + ) of + (True, K x1, K y1, Just (K x2), Just (K y2)) -> + do mb <- cryCheckLinRel solver y x (y1,x1) (y2,x2) + case mb of + Just r -> go (Map.insert x r done) + (reverse todo ++ more) + Nothing -> next + _ -> next + + + goV _ done todo _ _ [] = go done (reverse todo) + - goV done todo _ _ [] = go done (reverse todo) @@ -217,14 +272,36 @@ checkUnsat s e = return (res == SMT.Unsat) +-- | Try to prove the given expression. +-- If we fail, we try to give a counter example. +-- If the answer is unknown, then we return an empty counter example. +getCounterExample :: SMT.Solver -> [Name] -> SExpr -> IO (Maybe (Map Name Expr)) +getCounterExample s xs e = + do SMT.push s + SMT.assert s e + res <- SMT.check s + ans <- case res of + SMT.Unsat -> return Nothing + SMT.Unknown -> return (Just Map.empty) + SMT.Sat -> Just `fmap` getVals s xs + SMT.pop s + return ans + + + + + -- | Is this the only possible value for the constant, under the current -- assumptions. -- Assumes that we are in a 'Sat' state. -cryMustEqualK :: SMT.Solver -> Name -> Expr -> IO Bool -cryMustEqualK solver x expr = +-- Returns 'Nothing' if the variables must always match the given value. +-- Otherwise, we return a counter-example (which may be empty, if uniknown) +cryMustEqualK :: SMT.Solver -> [Name] -> + Name -> Expr -> IO (Maybe (Map Name Expr)) +cryMustEqualK solver xs x expr = case expr of - K Inf -> checkUnsat solver (SMT.const (smtFinName x)) - K (Nat n) -> checkUnsat solver $ + K Inf -> getCounterExample solver xs (SMT.const (smtFinName x)) + K (Nat n) -> getCounterExample solver xs $ SMT.not $ SMT.and (SMT.const $ smtFinName x) (SMT.eq (SMT.const (smtName x)) (SMT.int n)) @@ -245,25 +322,86 @@ cryMustEqualV solver x y = where fin a = SMT.const (smtFinName a) var a = SMT.const (smtName a) + -- | Try to find a linear relation between the two variables, based -- on two observed data points. -- NOTE: The variable being defined is the SECOND name. cryCheckLinRel :: SMT.Solver -> {- x -} Name {- ^ Definition in terms of this variable. -} -> {- y -} Name {- ^ Define this variable. -} -> - (Integer,Integer) {- ^ Values in one model (x,y) -} -> - (Integer,Integer) {- ^ Values in antoher model (x,y) -} -> - IO (Maybe (Name,Expr)) + (Nat',Nat') {- ^ Values in one model (x,y) -} -> + (Nat',Nat') {- ^ Values in antoher model (x,y) -} -> + IO (Maybe Expr) cryCheckLinRel s x y p1 p2 = - case linRel p1 p2 of - Nothing -> return Nothing - Just (a,b) -> - do let expr = K (Nat a) :* Var x :+ K (Nat b) - proved <- checkUnsat s $ propToSmtLib $ Not $ Var y :==: expr + -- First, try to find a linear relation that holds in all finite cases. + do SMT.push s + SMT.assert s (isFin x) + SMT.assert s (isFin y) + ans <- case (p1,p2) of + ((Nat x1, Nat y1), (Nat x2, Nat y2)) -> + checkLR x1 y1 x2 y2 + + ((Inf, Inf), (Nat x2, Nat y2)) -> + mbGoOn (getFinPt x2) $ \(x1,y1) -> checkLR x1 y1 x2 y2 + + ((Nat x1, Nat y1), (Inf, Inf)) -> + mbGoOn (getFinPt x1) $ \(x2,y2) -> checkLR x1 y1 x2 y2 + + _ -> return Nothing + + SMT.pop s + + -- Next, check the infinite cases: if @y = A * x + B@, then + -- either both @x@ and @y@ must be infinite or they both must be finite. + -- Note that we don't consider relations where A = 0: because they + -- would be handled when we checked that @y@ is a constant. + case ans of + Nothing -> return Nothing + Just e -> + do SMT.push s + SMT.assert s (SMT.not (SMT.eq (isFin x) (isFin y))) + c <- SMT.check s + SMT.pop s + case c of + SMT.Unsat -> return (Just e) + _ -> return Nothing + + where + isFin a = SMT.const (smtFinName a) + + checkLR x1 y1 x2 y2 = + mbGoOn (return (linRel (x1,y1) (x2,y2))) $ \(a,b) -> + do let expr = case a of + 1 -> Var x :+ K (Nat b) + _ -> K (Nat a) :* Var x :+ K (Nat b) + proved <- checkUnsat s $ propToSmtLib $ crySimplify + $ Not $ Var y :==: expr if not proved then return Nothing - else return (Just (y,expr)) + else return (Just expr) + -- Try to get an example of another point, which is finite, and at + -- different @x@ coordinate. + getFinPt otherX = + do SMT.push s + SMT.assert s (SMT.not (SMT.eq (SMT.const (smtName x)) (SMT.int otherX))) + smtAns <- SMT.check s + ans <- case smtAns of + SMT.Sat -> + do vX <- SMT.getConst s (smtName x) + vY <- SMT.getConst s (smtName y) + case (vX, vY) of + (SMT.Int vx, SMT.Int vy) + | vx >= 0 && vy >= 0 -> return (Just (vx,vy)) + _ -> return Nothing + _ -> return Nothing + SMT.pop s + return ans + + mbGoOn m k = do ans <- m + case ans of + Nothing -> return Nothing + Just a -> k a {- | Compute a linear relation through two concrete points. Try to find a relation of the form `y = a * x + b`, where both `a` and `b` @@ -282,7 +420,7 @@ linRel :: (Integer,Integer) {- ^ First point -} -> linRel (x1,y1) (x2,y2) = do guard (x1 /= x2) let (a,r) = divMod (y2 - y1) (x2 - x1) - guard (r == 0 && a >= 0) + guard (r == 0 && a > 0) -- Not interested in A = 0 let b = y1 - a * x1 guard (b >= 0) return (a,b)