From ae3e0ea1066e271793c3bae4f4a61deac27acc1c Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Mon, 10 Jul 2017 10:55:49 -0700
Subject: [PATCH] Add some functionality for simple checking of the consistency
 of goals.

---
 src/Cryptol/TypeCheck/Solver/SMT.hs | 30 ++++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/src/Cryptol/TypeCheck/Solver/SMT.hs b/src/Cryptol/TypeCheck/Solver/SMT.hs
index 6b4e1e87..8ce17ae6 100644
--- a/src/Cryptol/TypeCheck/Solver/SMT.hs
+++ b/src/Cryptol/TypeCheck/Solver/SMT.hs
@@ -1,5 +1,5 @@
 {-# Language FlexibleInstances #-}
-module Cryptol.TypeCheck.Solver.SMT (proveImp) where
+module Cryptol.TypeCheck.Solver.SMT (proveImp,checkUnsolvable) where
 
 import           SimpleSMT (SExpr)
 import qualified SimpleSMT as SMT
@@ -34,6 +34,19 @@ proveImp sol ps gs0 =
      SMT.pop s
      return (catMaybes gs' ++ rest)
 
+-- | Check if the given goals are known to be unsolvable.
+checkUnsolvable :: Solver -> [Goal] -> IO Bool
+checkUnsolvable sol gs0 =
+  debugBlock sol "CHECK UNSOLVABLE" $
+  do let s  = rawSolver sol
+         ps = filter isNumeric (map goal gs0)
+         vs = Set.toList (fvs ps)
+     tvs <- debugBlock sol "VARIABLES" $
+       do SMT.push s
+          Map.fromList <$> zipWithM (declareVar s) [ 0 .. ] vs
+     unsolvable sol tvs ps
+
+--------------------------------------------------------------------------------
 
 declareVar :: SMT.Solver -> Int -> TVar -> IO (TVar, SExpr)
 declareVar s x v = do let name = (if isFreeTV v then "fv" else "kv") ++ show x
@@ -57,6 +70,21 @@ prove sol tvs g =
        _         -> return (Just g)
 
 
+-- | Check if some numeric goals are known to be unsolvable.
+unsolvable :: Solver -> TVars -> [Prop] -> IO Bool
+unsolvable sol tvs ps =
+  debugBlock sol "UNSOLVABLE" $
+  do let s = rawSolver sol
+     SMT.push s
+     mapM_ (assume s tvs) ps
+     res <- SMT.check s
+     SMT.pop s
+     case res of
+       SMT.Unsat -> return True
+       _         -> return False
+
+
+
 --------------------------------------------------------------------------------
 
 isNumeric :: Prop -> Bool