Hook in and improve linear relations.

There is still an issue with the encoding of finitness.
For example, if we know:

a = 1 + min b a

And we know that `b`z is finite, we SHOULD know that `a` is finite too,
but apparently we don't.

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 ]
 

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)
+    {- ^ Fully simplified: may mention ORs, and named non-linear terms.
-    -- These are used in the proofs, and may not be translatable back
+    These are what we send to the prover, and we don't attempt to
-    -- into Cryptol.
+    convert them back into Cryptol types. -}
 
   , dpSimpExprProp :: Prop
-    -- ^ Expressions are simplified (no ORs)
+    {- ^ A version of the proposition where just the expression terms
-    -- These should be importable back into Cryptol props.
+    have been simplified.  These should not contain ORs or named non-linear
-    -- XXX: What about `sys` variables?
+    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
+  do logger <- SMT.newLogger
-     let logger = quietLogger
+     -- 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
+{- | The set of unification variables is used to guide ordering of
--- assignments (we prefer assigning to them, as that amounts to doing
+assignments (we prefer assigning to them, as that amounts to doing
--- type inference).
+type inference).
-getImpSubst :: Solver -> Set Name -> IO (Bool,Subst)
+
+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
+     impSu <- cryImproveModel solver uniVars m
-     nlSu  <- getNLSubst s
-     let su  = composeSubst nlSu (toSubst model)
 
-         -- XXX: The improvemnts that are being ignored here could
+     let isNonLinName (SysName {})  = True
-         -- lead to extar, potentially useful, constraints.
+         isNonLinName (UserName {}) = False
-         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
 
-     res <- mapM (checkImpBind s) imps
-     let (agains,eqs) = unzip res
 
-     debugBlock s "after" $
+         keep k e = not (isNonLinName k) &&
-       mapM_ (\(x,e) -> debugLog s (Var x :== e)) (concat eqs)
+                    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

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
+Otherwise returns `Just`, and a substitution for non-linear expressions
-that became linear. -}
+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

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, unfoldr )
-import           Data.List ( partition )
 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
+cryImproveModel solver uniVars m = toSubst `fmap` go Map.empty initialTodo
-  -- XXX: Hook in linRel
   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
+    do mbCounter <- cryMustEqualK solver (Map.keys m) x e
-       if yesK
+       case mbCounter of
-         then go (Map.insert x e done) rest
+         Nothing -> go (Map.insert x e done) rest
-         else goV done [] x e 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
+                           else tryLR
-    | otherwise = goV done ((y,e') : todo) x e more
+
+    | 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
+-- Returns 'Nothing' if the variables must always match the given value.
-cryMustEqualK solver x expr =
+-- 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 Inf     -> getCounterExample solver xs (SMT.const (smtFinName x))
-    K (Nat n) -> checkUnsat solver $
+    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) -} ->
+                 (Nat',Nat') {- ^ Values in one model (x,y) -} ->
-                 (Integer,Integer) {- ^ Values in antoher model (x,y) -} ->
+                 (Nat',Nat') {- ^ Values in antoher model (x,y) -} ->
-                 IO (Maybe (Name,Expr))
+                 IO (Maybe Expr)
 cryCheckLinRel s x y p1 p2 =
-  case linRel p1 p2 of
+  -- First, try to find a linear relation that holds in all finite cases.
-    Nothing -> return Nothing
+  do SMT.push s
-    Just (a,b) ->
+     SMT.assert s (isFin x)
-      do let expr = K (Nat a) :* Var x :+ K (Nat b)
+     SMT.assert s (isFin y)
-         proved <- checkUnsat s $ propToSmtLib $ Not $ Var y :==: expr
+     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)