Fix-up export to SMT to deal correctly with finiteness.

src/Cryptol/TypeCheck/Solver/CrySAT.hs

@@ -313,7 +313,6 @@ declareVar Solver { .. } a =
           let fin_a = smtFinName a
           _  <- SMT.declare solver fin_a SMT.tBool
           SMT.assert solver (SMT.geq e (SMT.int 0))
-          -- SMT.assert solver (SMT.const fin_a)     -- HMM ???
           modifyIORef' declared (viInsert a)
 
 -- | Add an assertion to the current context.

src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs

@@ -49,12 +49,12 @@ isNonLinOp expr =
 
     Div _ y ->
       case y of
-        K _       -> False
+        K (Nat n) -> n /= 0
         _         -> True
 
     Mod _ y ->
       case y of
-        K _       -> False
+        K (Nat n) -> n /= 0
         _         -> True
 
     _ :^^ _       -> True

src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs

@@ -59,10 +59,10 @@ desugarProp prop =
     p :&& q     -> (:&&) `fmap` desugarProp p `ap` desugarProp q
     p :|| q     -> (:||) `fmap` desugarProp p `ap` desugarProp q
     Fin (Var _) -> return prop
-    Fin _       -> unexpected
     x :==: y    -> (:==:) `fmap` desugarExpr x `ap` desugarExpr y
     x :>: y     -> (:>:)  `fmap` desugarExpr x `ap` desugarExpr y
 
+    Fin _     -> unexpected
     _ :== _   -> unexpected
     _ :>= _   -> unexpected
     _ :> _    -> unexpected
@@ -86,9 +86,17 @@ propToSmtLib prop =
     Not p       -> SMT.not (propToSmtLib p)
     p :&& q     -> SMT.and (propToSmtLib p) (propToSmtLib q)
     p :|| q     -> SMT.or  (propToSmtLib p) (propToSmtLib q)
-    Fin (Var x) -> SMT.const (smtFinName x)
+    Fin (Var x) -> fin x
-    x :==: y    -> SMT.eq (exprToSmtLib x) (exprToSmtLib y)
+
-    x :>: y     -> SMT.gt (exprToSmtLib x) (exprToSmtLib y)
+    {- For the linear constraints, if the term is finite, then all of
+       its variables must have been finite.
+
+       XXX: Adding the `fin` decls at the leaves leads to some duplication:
+       We could add them just once for each conjunctoin of simple formulas,
+       but I am not sure how much this matters.
+    -}
+    x :==: y    -> addFin x y $ SMT.eq (exprToSmtLib x) (exprToSmtLib y)
+    x :>: y     -> addFin x y $ SMT.gt (exprToSmtLib x) (exprToSmtLib y)
 
     Fin _       -> unexpected
     _ :== _     -> unexpected
@@ -97,20 +105,24 @@ propToSmtLib prop =
 
   where
   unexpected = panic "desugarProp" [ show (ppProp prop) ]
+  fin x      = SMT.const (smtFinName x)
 
+  addFin x y e = foldr (\x e' -> SMT.and (fin x) e') e
+                   (Set.toList (cryExprFVS x `Set.union` cryExprFVS y))
 
 exprToSmtLib :: Expr -> SExpr
 exprToSmtLib expr =
 
   case expr of
     K (Nat n)           -> SMT.int n
-    K Inf               -> unexpected
     Var a               -> SMT.const (smtName a)
     x :+ y              -> SMT.add (exprToSmtLib x) (exprToSmtLib y)
     x :- y              -> SMT.sub (exprToSmtLib x) (exprToSmtLib y)
     x :* y              -> SMT.mul (exprToSmtLib x) (exprToSmtLib y)
     Div x y             -> SMT.div (exprToSmtLib x) (exprToSmtLib y)
     Mod x y             -> SMT.mod (exprToSmtLib x) (exprToSmtLib y)
+
+    K Inf               -> unexpected
     _ :^^ _             -> unexpected
     Min {}              -> unexpected
     Max {}              -> unexpected

src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs

@@ -22,8 +22,6 @@ import qualified Cryptol.TypeCheck.Solver.InfNat as IN
 import           Cryptol.Utils.Panic( panic )
 import           Cryptol.Utils.Misc ( anyJust )
 
-import           Cryptol.Utils.Debug(trace)
-
 import           Control.Monad ( mplus )
 import           Data.List ( sortBy )
 import           Data.Maybe ( fromMaybe )
@@ -32,15 +30,7 @@ import qualified Data.Set as Set
 
 -- | Simplify a property, if possible.
 crySimplify :: Prop -> Prop
-crySimplify p = trace ("simp: " ++ show (ppProp p)) $
+crySimplify p = fromMaybe p (crySimplifyMaybe p)
-                  case crySimplifyMaybe p of
-                    Nothing -> trace "-> (no change)" p
-                    Just p1 -> trace ("-> " ++ show (ppProp p1)) p1
-
-
--- | Simplify a property, if possible.
-crySimplify' :: Prop -> Prop
-crySimplify' p = crySimplify p -- fromMaybe p (crySimplifyMaybe p)
 
 -- | Simplify a property, if possibly.
 crySimplifyMaybe :: Prop -> Maybe Prop
@@ -49,7 +39,7 @@ crySimplifyMaybe p =
       exprsSimped = fromMaybe p mbSimpExprs
       mbRearrange = tryRearrange exprsSimped
       rearranged  = fromMaybe exprsSimped mbRearrange
-  in crySimplify' `fmap` (crySimpStep rearranged `mplus` mbRearrange
+  in crySimplify `fmap` (crySimpStep rearranged `mplus` mbRearrange
                                                 `mplus` mbSimpExprs)
 
   where
@@ -716,7 +706,6 @@ cryNoInf expr =
 
 
 
-
     -- The rest just propagates
 
     K _     -> return expr