mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-30 23:45:23 +03:00
Redo the export to SMT story in a much simpler way.
This commit is contained in:
Iavor S. Diatchki
parent
de770d5aed
commit
41131fe7ed
@ -14,7 +14,7 @@ Build-type: Simple
|
||||
Cabal-version: >= 1.18
|
||||
extra-source-files: bench/data/*.cry
|
||||
|
||||
data-files: *.cry Cryptol/*.cry
|
||||
data-files: *.cry Cryptol/*.cry *.z3
|
||||
data-dir: lib
|
||||
|
||||
source-repository head
|
||||
@ -63,7 +63,7 @@ library
|
||||
random >= 1.0.1,
|
||||
sbv >= 5.15,
|
||||
smtLib >= 1.0.7,
|
||||
simple-smt >= 0.6.0,
|
||||
simple-smt >= 0.7.0,
|
||||
syb >= 0.4,
|
||||
text >= 1.1,
|
||||
template-haskell,
|
||||
@ -127,6 +127,7 @@ library
|
||||
Cryptol.TypeCheck.Sanity,
|
||||
|
||||
Cryptol.TypeCheck.Solver.Types,
|
||||
Cryptol.TypeCheck.Solver.SMT,
|
||||
Cryptol.TypeCheck.Solver.InfNat,
|
||||
Cryptol.TypeCheck.Solver.Class,
|
||||
Cryptol.TypeCheck.Solver.Selector,
|
||||
|
||||
217
lib/CryptolTC.z3
Normal file
217
lib/CryptolTC.z3
Normal file
@ -0,0 +1,217 @@
|
||||
|
||||
(declare-datatypes ()
|
||||
( (InfNat (mk-infnat (value Int) (isFin Bool) (isErr Bool)))
|
||||
)
|
||||
)
|
||||
|
||||
(declare-datatypes ()
|
||||
( (MaybeBool (mk-mb (prop Bool) (isErrorProp Bool)))
|
||||
)
|
||||
)
|
||||
|
||||
(define-fun cryBool ((x Bool)) MaybeBool
|
||||
(mk-mb x false)
|
||||
)
|
||||
|
||||
(define-fun cryErrProp () MaybeBool
|
||||
(mk-mb false true)
|
||||
)
|
||||
|
||||
(define-fun cryInf () InfNat
|
||||
(mk-infnat 0 false false)
|
||||
)
|
||||
|
||||
(define-fun cryNat ((x Int)) InfNat
|
||||
(mk-infnat x true false)
|
||||
)
|
||||
|
||||
(define-fun cryErr () InfNat
|
||||
(mk-infnat 0 false true)
|
||||
)
|
||||
|
||||
; ------------------------------------------------------------
|
||||
|
||||
(define-fun cryEq ((x InfNat) (y InfNat)) MaybeBool
|
||||
(ite (or (isErr x) (isErr y)) cryErrProp (cryBool
|
||||
(ite (isFin x)
|
||||
(ite (isFin y) (= (value x) (value y)) false)
|
||||
(not (isFin y))
|
||||
)))
|
||||
)
|
||||
|
||||
(define-fun cryFin ((x InfNat)) MaybeBool
|
||||
(ite (isErr x) cryErrProp (cryBool
|
||||
(isFin x)))
|
||||
)
|
||||
|
||||
(define-fun cryGeq ((x InfNat) (y InfNat)) MaybeBool
|
||||
(ite (or (isErr x) (isErr y)) cryErrProp (cryBool
|
||||
(ite (isFin x)
|
||||
(ite (isFin y) (>= (value x) (value y)) false)
|
||||
true
|
||||
)))
|
||||
)
|
||||
|
||||
(define-fun cryAnd ((x MaybeBool) (y MaybeBool)) MaybeBool
|
||||
(ite (or (isErrorProp x) (isErrorProp y)) cryErrProp
|
||||
(cryBool (and (prop x) (prop y)))
|
||||
)
|
||||
)
|
||||
|
||||
(define-fun cryTrue () MaybeBool
|
||||
(cryBool true)
|
||||
)
|
||||
|
||||
; -----------------------------------------------------
|
||||
|
||||
(define-fun cryVar ((x InfNat)) Bool
|
||||
(and (not (isErr x)) (>= (value x) 0))
|
||||
)
|
||||
|
||||
(define-fun cryAssume ((x MaybeBool)) Bool
|
||||
(ite (isErrorProp x) true (prop x))
|
||||
)
|
||||
|
||||
(declare-fun cryUnknown () Bool)
|
||||
|
||||
(define-fun cryProve ((x MaybeBool)) Bool
|
||||
(ite (isErrorProp x) cryUnknown (not (prop x)))
|
||||
)
|
||||
|
||||
; ------------------------------------------------------------
|
||||
|
||||
(define-fun cryAdd ((x InfNat) (y InfNat)) InfNat
|
||||
(ite (or (isErr x) (isErr y)) cryErr
|
||||
(ite (isFin x)
|
||||
(ite (isFin y) (cryNat (+ (value x) (value y))) cryInf)
|
||||
cryInf
|
||||
))
|
||||
)
|
||||
|
||||
(define-fun crySub ((x InfNat) (y InfNat)) InfNat
|
||||
(ite (or (isErr x) (isErr y) (not (isFin y))) cryErr
|
||||
(ite (isFin x)
|
||||
(ite (>= (value x) (value y)) (cryNat (- (value x) (value y))) cryErr)
|
||||
cryInf
|
||||
))
|
||||
)
|
||||
|
||||
(define-fun cryMul ((x InfNat) (y InfNat)) InfNat
|
||||
(ite (or (isErr x) (isErr y)) cryErr
|
||||
(ite (isFin x)
|
||||
(ite (isFin y) (cryNat (* (value x) (value y)))
|
||||
(ite (= (value x) 0) (cryNat 0) cryInf))
|
||||
(ite (and (isFin y) (= (value y) 0)) (cryNat 0) cryInf)
|
||||
))
|
||||
)
|
||||
|
||||
(define-fun cryDiv ((x InfNat) (y InfNat)) InfNat
|
||||
(ite (or (isErr x) (isErr y) (not (isFin x))) cryErr
|
||||
(ite (isFin y)
|
||||
(ite (= (value y) 0) cryErr (cryNat (div (value x) (value y))))
|
||||
(cryNat 0)
|
||||
))
|
||||
)
|
||||
|
||||
(define-fun cryMod ((x InfNat) (y InfNat)) InfNat
|
||||
(ite (or (isErr x) (isErr y) (not (isFin x))) cryErr
|
||||
(ite (isFin y)
|
||||
(ite (= (value y) 0) cryErr (cryNat (mod (value x) (value y))))
|
||||
x
|
||||
))
|
||||
)
|
||||
|
||||
|
||||
|
||||
(define-fun cryMin ((x InfNat) (y InfNat)) InfNat
|
||||
(ite (or (isErr x) (isErr y)) cryErr
|
||||
(ite (isFin x)
|
||||
(ite (isFin y)
|
||||
(ite (<= (value x) (value y)) x y)
|
||||
x)
|
||||
y
|
||||
))
|
||||
)
|
||||
|
||||
(define-fun cryMax ((x InfNat) (y InfNat)) InfNat
|
||||
(ite (or (isErr x) (isErr y)) cryErr
|
||||
(ite (isFin x)
|
||||
(ite (isFin y)
|
||||
(ite (<= (value x) (value y)) y x)
|
||||
y)
|
||||
x
|
||||
))
|
||||
)
|
||||
|
||||
(declare-fun cryWidthUnknown (Int) Int)
|
||||
|
||||
(define-fun cryWidthTable ((x Int)) Int
|
||||
(ite (< x 1) 0
|
||||
(ite (< x 2) 1
|
||||
(ite (< x 4) 2
|
||||
(ite (< x 8) 3
|
||||
(ite (< x 16) 4
|
||||
(ite (< x 32) 5
|
||||
(ite (< x 64) 6
|
||||
(ite (< x 128) 7
|
||||
(ite (< x 256) 8
|
||||
(ite (< x 512) 9
|
||||
(ite (< x 1024) 10
|
||||
(cryWidthUnknown x))))))))))))
|
||||
)
|
||||
|
||||
(define-fun cryWidth ((x InfNat)) InfNat
|
||||
(ite (isErr x) cryErr
|
||||
(ite (isFin x) (cryNat (cryWidthTable (value x)))
|
||||
cryInf
|
||||
))
|
||||
)
|
||||
|
||||
(declare-fun cryExpUnknown (Int Int) Int)
|
||||
|
||||
(define-fun cryExpTable ((x Int) (y Int)) Int
|
||||
(ite (= y 0) 1
|
||||
(ite (= y 1) x
|
||||
(ite (= x 0) 0
|
||||
(cryExpUnknown x y))))
|
||||
)
|
||||
|
||||
(define-fun cryExp ((x InfNat) (y InfNat)) InfNat
|
||||
(ite (or (isErr x) (isErr y)) cryErr
|
||||
(ite (isFin x)
|
||||
(ite (isFin y)
|
||||
(cryNat (cryExpTable (value x) (value y)))
|
||||
(ite (< (value x) 2) x cryInf))
|
||||
(ite (isFin y)
|
||||
(ite (= (value y) 0) (cryNat 1) cryInf)
|
||||
cryInf)
|
||||
))
|
||||
)
|
||||
|
||||
(define-fun cryLenFromThenTo ((x InfNat) (y InfNat) (z InfNat)) InfNat
|
||||
(ite (or (isErr x) (not (isFin x))
|
||||
(isErr y) (not (isFin y))
|
||||
(isErr z) (not (isFin z))
|
||||
(= (value x) (value y))) cryErr (cryNat
|
||||
(ite (> (value x) (value y))
|
||||
(ite (> (value z) (value x)) 0 (+ (div (- (value x) (value z))
|
||||
(- (value x) (value y))) 1))
|
||||
(ite (< (value z) (value x)) 0 (+ (div (- (value z) (value x))
|
||||
(- (value y) (value x))) 1))
|
||||
)))
|
||||
)
|
||||
|
||||
|
||||
(define-fun cryLenFromThen ((x InfNat) (y InfNat) (z InfNat)) InfNat
|
||||
(ite (or (isErr x) (not (isFin x))
|
||||
(isErr y) (not (isFin y))
|
||||
(isErr z) (not (isFin z))
|
||||
(= (value x) (value y))) cryErr
|
||||
(ite (< (value y) (value x)) (cryLenFromThenTo x y (cryNat 0))
|
||||
(cryLenFromThenTo x y (cryNat (- (cryExpTable 2 (value z)) 1))))
|
||||
)
|
||||
)
|
||||
|
||||
; -------------------
|
||||
|
||||
|
||||
@ -434,6 +434,7 @@ genInferInput r prims env = do
|
||||
monoBinds <- getMonoBinds
|
||||
cfg <- getSolverConfig
|
||||
supply <- getSupply
|
||||
searchPath <- getSearchPath
|
||||
|
||||
-- TODO: include the environment needed by the module
|
||||
return T.InferInput
|
||||
@ -444,6 +445,7 @@ genInferInput r prims env = do
|
||||
, T.inpNameSeeds = seeds
|
||||
, T.inpMonoBinds = monoBinds
|
||||
, T.inpSolverConfig = cfg
|
||||
, T.inpSearchPath = searchPath
|
||||
, T.inpSupply = supply
|
||||
, T.inpPrimNames = prims
|
||||
}
|
||||
|
||||
@ -41,6 +41,10 @@ import MonadLib hiding (mapM)
|
||||
|
||||
import Data.IORef
|
||||
|
||||
import System.FilePath((</>))
|
||||
import System.Directory(doesFileExist)
|
||||
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
|
||||
@ -59,6 +63,8 @@ data InferInput = InferInput
|
||||
-- signatures be monomorphized?
|
||||
|
||||
, inpSolverConfig :: SolverConfig -- ^ Options for the constraint solver
|
||||
, inpSearchPath :: [FilePath]
|
||||
-- ^ Where to look for Cryptol theory file.
|
||||
|
||||
, inpPrimNames :: !PrimMap -- ^ The mapping from 'Ident' to 'Name',
|
||||
-- for names that the typechecker
|
||||
@ -96,7 +102,8 @@ bumpCounter = do RO { .. } <- IM ask
|
||||
|
||||
runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
|
||||
runInferM info (IM m) = CrySAT.withSolver (inpSolverConfig info) $ \solver ->
|
||||
do coutner <- newIORef 0
|
||||
do loadCryTCPrel solver (inpSearchPath info)
|
||||
coutner <- newIORef 0
|
||||
rec ro <- return RO { iRange = inpRange info
|
||||
, iVars = Map.map ExtVar (inpVars info)
|
||||
, iTVars = []
|
||||
@ -160,6 +167,14 @@ runInferM info (IM m) = CrySAT.withSolver (inpSolverConfig info) $ \solver ->
|
||||
-- The actual order does not matter
|
||||
cmpRange (Range x y z) (Range a b c) = compare (x,y,z) (a,b,c)
|
||||
|
||||
loadCryTCPrel _ [] = panic "Failed to find file" [] -- return ()
|
||||
loadCryTCPrel s (p : ps) =
|
||||
do let file = p </> "CryptolTC.z3"
|
||||
yes <- doesFileExist file
|
||||
if yes then CrySAT.loadFile s file
|
||||
else loadCryTCPrel s ps
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@ -17,7 +17,6 @@ module Cryptol.TypeCheck.Solve
|
||||
, defaultReplExpr
|
||||
) where
|
||||
|
||||
import Cryptol.Parser.Position (emptyRange)
|
||||
import Cryptol.TypeCheck.PP(pp)
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Monad
|
||||
@ -31,17 +30,18 @@ import Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
|
||||
import Cryptol.TypeCheck.SimpType(tMax)
|
||||
|
||||
|
||||
import Cryptol.TypeCheck.Solver.SMT(proveImp)
|
||||
import Cryptol.TypeCheck.Solver.Improve(improveProp,improveProps)
|
||||
import Cryptol.TypeCheck.Solver.Numeric.Interval
|
||||
import qualified Cryptol.TypeCheck.Solver.Numeric.AST as Num
|
||||
import qualified Cryptol.TypeCheck.Solver.Numeric.ImportExport as Num
|
||||
import qualified Cryptol.TypeCheck.Solver.CrySAT as Num
|
||||
import Cryptol.TypeCheck.Solver.CrySAT (debugBlock, DebugLog(..))
|
||||
import Cryptol.TypeCheck.Solver.CrySAT
|
||||
import Cryptol.Utils.PP (text,vcat,(<+>))
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.Patterns(matchMaybe)
|
||||
|
||||
import Control.Monad (unless, guard, mzero)
|
||||
import Control.Monad (guard, mzero)
|
||||
import Control.Applicative ((<|>))
|
||||
import Data.Either(partitionEithers)
|
||||
import Data.Maybe(catMaybes)
|
||||
@ -180,26 +180,49 @@ proveImplicationIO s f varsInEnv ps asmps0 gs0 =
|
||||
do let ctxt = assumptionIntervals Map.empty asmps
|
||||
res <- quickSolverIO ctxt gs
|
||||
case res of
|
||||
Left err -> return (Left (UnsolvedGoal True err), emptySubst)
|
||||
Left bad -> return (Left (UnsolvedGoal True bad), emptySubst)
|
||||
Right (su,[]) -> return (Right [], su)
|
||||
Right (su,gs1) ->
|
||||
do (res3,su1) <- proveImplicationWithExtSolver
|
||||
s f varsInEnv ps asmps gs1
|
||||
case res3 of
|
||||
Left err -> return (Left (cleanupError err), emptySubst)
|
||||
Right ws -> return (Right ws, su1 @@ su)
|
||||
|
||||
|
||||
do gs2 <- proveImp s asmps gs1
|
||||
case gs2 of
|
||||
[] -> return (Right [], su)
|
||||
gs3 ->
|
||||
do let free = Set.toList
|
||||
$ Set.difference (fvs (map goal gs3)) varsInEnv
|
||||
case improveByDefaultingWithPure free gs3 of
|
||||
(_,_,newSu,_)
|
||||
| isEmptySubst newSu -> return (err gs3, su) -- XXX: Old?
|
||||
(_,newGs,newSu,ws) ->
|
||||
do let su1 = newSu @@ su
|
||||
(res1,su2) <- proveImplicationIO s f varsInEnv ps
|
||||
(apSubst su1 asmps0) newGs
|
||||
let su3 = su2 @@ su1
|
||||
case res1 of
|
||||
Left bad -> return (Left bad, su3)
|
||||
Right ws1 -> return (Right (ws++ws1),su3)
|
||||
where
|
||||
err us = Left $ cleanupError
|
||||
$ UnsolvedDelayedCt
|
||||
$ DelayedCt { dctSource = f
|
||||
, dctForall = ps
|
||||
, dctAsmps = asmps0
|
||||
, dctGoals = us
|
||||
}
|
||||
|
||||
|
||||
|
||||
(asmps,gs) =
|
||||
case matchMaybe (improveProps True Map.empty asmps0) of
|
||||
Nothing -> (asmps0,gs0)
|
||||
Just (newSu,newAsmps) ->
|
||||
( [ TVar x =#= t | (x,t) <- substToList newSu ]
|
||||
++ newAsmps
|
||||
, [ g { goal = apSubst newSu (goal g) } | g <- gs0
|
||||
, not (goal g `elem` asmps0) ]
|
||||
)
|
||||
let gs1 = [ g { goal = p } | g <- gs0, p <- pSplitAnd (goal g)
|
||||
, notElem p asmps0 ]
|
||||
in case matchMaybe (improveProps True Map.empty asmps0) of
|
||||
Nothing -> (asmps0,gs1)
|
||||
Just (newSu,newAsmps) ->
|
||||
( [ TVar x =#= t | (x,t) <- substToList newSu ]
|
||||
++ newAsmps
|
||||
, [ g { goal = apSubst newSu (goal g) } | g <- gs1 ]
|
||||
)
|
||||
|
||||
|
||||
|
||||
|
||||
cleanupError :: Error -> Error
|
||||
@ -216,118 +239,7 @@ cleanupError err =
|
||||
|
||||
|
||||
|
||||
proveImplicationWithExtSolver
|
||||
:: Num.Solver
|
||||
-> Name -- ^ Checking this function
|
||||
-> Set TVar -- ^ These appear in the environment, and we should
|
||||
-- not try to default the
|
||||
-> [TParam] -- ^ Type parameters
|
||||
-> [Prop] -- ^ Assumed constraint
|
||||
-> [Goal] -- ^ Collected constraints
|
||||
-> IO (Either Error [Warning], Subst)
|
||||
proveImplicationWithExtSolver s lname varsInEnv as ps gs =
|
||||
debugBlock s "proveImplicationIO" $
|
||||
|
||||
do debugBlock s "assumes" (debugLog s ps)
|
||||
debugBlock s "shows" (debugLog s gs)
|
||||
debugLog s "1. ------------------"
|
||||
|
||||
|
||||
_simpPs <- Num.assumeProps s ps
|
||||
|
||||
mbImps <- Num.check s
|
||||
debugLog s "2. ------------------"
|
||||
|
||||
|
||||
case mbImps of
|
||||
|
||||
Nothing ->
|
||||
do debugLog s "(contradiction in assumptions)"
|
||||
return (Left $ UnusableFunction lname ps, emptySubst)
|
||||
|
||||
Just (imps,extra) ->
|
||||
do let su = importImps imps
|
||||
gs0 = apSubst su gs
|
||||
|
||||
debugBlock s "improvement from assumptions:" $ debugLog s su
|
||||
|
||||
let (scs,invalid) = importSideConds extra
|
||||
unless (null invalid) $
|
||||
panic "proveImplicationIO" ( "Unable to import all side conditions:"
|
||||
: map (show . Num.ppProp) invalid )
|
||||
|
||||
let gs1 = filter ((`notElem` ps) . goal) gs0
|
||||
|
||||
debugLog s "3. ---------------------"
|
||||
let ctxt = assumptionIntervals Map.empty ps
|
||||
(mb,su1) <- simpGoals' s ctxt (scs ++ gs1)
|
||||
|
||||
case mb of
|
||||
Left badGs -> reportUnsolved badGs (su1 @@ su)
|
||||
Right [] -> return (Right [], su1 @@ su)
|
||||
|
||||
Right us ->
|
||||
-- Last hope: try to default stuff
|
||||
do let vs = Set.filter isFreeTV $ fvs $ map goal us
|
||||
dVars = Set.toList (vs `Set.difference` varsInEnv)
|
||||
-- (_,us1,su2,ws) <- improveByDefaultingWith s dVars us
|
||||
(_,us1,su2,ws) = improveByDefaultingWithPure dVars us
|
||||
|
||||
Right (su3,us2) <- quickSolverIO ctxt us1
|
||||
|
||||
case us2 of
|
||||
[] -> return (Right ws, su3 @@ su2 @@ su1 @@ su)
|
||||
_ -> reportUnsolved us1 (su3 @@ su2 @@ su1 @@ su)
|
||||
where
|
||||
reportUnsolved us su =
|
||||
return ( Left $ UnsolvedDelayedCt
|
||||
$ DelayedCt { dctSource = lname
|
||||
, dctForall = as
|
||||
, dctAsmps = ps
|
||||
, dctGoals = us
|
||||
}, su)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
{- Constraints and satisfiability:
|
||||
|
||||
1. [Satisfiable] A collection of constraints is _satisfiable_, if there is an
|
||||
assignment for the variables that make all constraints true.
|
||||
|
||||
2. [Valid] If a constraint is satisfiable for any assignment of its free
|
||||
variables, then it is _valid_, and may be ommited.
|
||||
|
||||
3. [Partial] A constraint may _partial_, which means that under some
|
||||
assignment it is neither true nor false. For example:
|
||||
`x - y > 5` is true for `{ x = 15, y = 3 }`, it is false for
|
||||
`{ x = 5, y = 4 }`, and it is neither for `{ x = 1, y = 2 }`.
|
||||
|
||||
Note that constraints that are always true or undefined are NOT
|
||||
valid, as there are assignemntes for which they are not true.
|
||||
An example of such constraint is `x - y >= 0`.
|
||||
|
||||
4. [Provability] Instead of thinking of three possible values for
|
||||
satisfiability (i.e., true, false, and unknown), we could instead
|
||||
think of asking: "Is constraint C provable". This essentailly
|
||||
maps "true" to "true", and "false,unknown" to "false", if we
|
||||
treat constraints with malformed parameters as unprovable.
|
||||
-}
|
||||
|
||||
|
||||
{-
|
||||
The plan:
|
||||
1. Start with a set of constraints, CS
|
||||
2. Compute its well-defined closure, DS.
|
||||
3. Simplify constraints: evaluate terms in constraints as much as possible
|
||||
4. Solve: eliminate constraints that are true
|
||||
5. Check for consistency
|
||||
6. Compute improvements
|
||||
7. For each type in the improvements, add well-defined constraints
|
||||
8. Instantiate constraints with substitution
|
||||
9. Goto 3
|
||||
-}
|
||||
|
||||
simpGoals' :: Num.Solver -> Ctxt -> [Goal] -> IO (Either [Goal] [Goal], Subst)
|
||||
simpGoals' s asmps gs0 = go emptySubst [] (wellFormed gs0 ++ gs0)
|
||||
@ -490,29 +402,6 @@ importSplitImps = mk . partitionEithers . map imp . Map.toList
|
||||
|
||||
|
||||
|
||||
-- | Import an improving substitution into a Cryptol substitution.
|
||||
-- The substitution will contain both unification and skolem variables,
|
||||
-- so this should be used when processing *givens*.
|
||||
importImps :: Map Num.Name Num.Expr -> Subst
|
||||
importImps = listSubst . map imp . Map.toList
|
||||
where
|
||||
imp (x,e) = case (x, Num.importType e) of
|
||||
(Num.UserName tv, Just ty) -> (tv,ty)
|
||||
_ -> panic "importImps" [ "Failed to import:", show x, show e ]
|
||||
|
||||
|
||||
|
||||
importSideConds :: [Num.Prop] -> ([Goal],[Num.Prop])
|
||||
importSideConds = go [] []
|
||||
where
|
||||
go ok bad [] = ([ Goal CtImprovement emptyRange g | g <- ok], bad)
|
||||
go ok bad (p:ps) = case Num.importProp p of
|
||||
Just p' -> go (p' ++ ok) bad ps
|
||||
Nothing -> go ok (p:bad) ps
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -21,6 +21,8 @@ module Cryptol.TypeCheck.Solver.CrySAT
|
||||
, DebugLog(..)
|
||||
, knownDefined, numericRight
|
||||
, minimizeContradictionSimpDef
|
||||
, loadFile
|
||||
, rawSolver
|
||||
) where
|
||||
|
||||
import qualified Cryptol.TypeCheck.AST as Cry
|
||||
@ -282,6 +284,19 @@ data Solver = Solver
|
||||
-- ^ For debugging
|
||||
}
|
||||
|
||||
loadFile :: Solver -> FilePath -> IO ()
|
||||
loadFile s file = do -- txt <- readFile file
|
||||
-- mapM_ putStrLn (lines txt)
|
||||
go =<< readFile file
|
||||
where
|
||||
go txt = case SMT.readSExpr txt of
|
||||
Just (e,rest) -> SMT.command (solver s) e >> go rest
|
||||
Nothing -> return ()
|
||||
|
||||
rawSolver :: Solver -> SMT.Solver
|
||||
rawSolver = solver
|
||||
|
||||
|
||||
|
||||
-- | Keeps track of declared variables and non-linear terms.
|
||||
data VarInfo = VarInfo
|
||||
@ -418,7 +433,7 @@ withSolver SolverConfig { .. } k =
|
||||
let smtDbg = if solverVerbose > 1 then Just logger else Nothing
|
||||
solver <- SMT.newSolver solverPath solverArgs smtDbg
|
||||
_ <- SMT.setOptionMaybe solver ":global-decls" "false"
|
||||
SMT.setLogic solver "QF_LIA"
|
||||
-- SMT.setLogic solver "QF_LIA"
|
||||
declared <- newIORef viEmpty
|
||||
a <- k Solver { .. }
|
||||
_ <- SMT.stop solver
|
||||
|
||||
135
src/Cryptol/TypeCheck/Solver/SMT.hs
Normal file
135
src/Cryptol/TypeCheck/Solver/SMT.hs
Normal file
@ -0,0 +1,135 @@
|
||||
{-# Language FlexibleInstances #-}
|
||||
module Cryptol.TypeCheck.Solver.SMT (proveImp) where
|
||||
|
||||
import SimpleSMT (SExpr)
|
||||
import qualified SimpleSMT as SMT
|
||||
import Data.Map ( Map )
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import Data.Maybe(catMaybes)
|
||||
import Data.List(partition)
|
||||
import Control.Monad(msum,zipWithM)
|
||||
|
||||
import Cryptol.TypeCheck.Type
|
||||
import Cryptol.TypeCheck.Solver.CrySAT
|
||||
import Cryptol.TypeCheck.InferTypes
|
||||
import Cryptol.TypeCheck.TypePat hiding ((~>),(~~>))
|
||||
import Cryptol.Utils.Panic
|
||||
|
||||
|
||||
-- | Returns goals that were not proved
|
||||
proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]
|
||||
proveImp sol ps gs0 =
|
||||
debugBlock sol "PROVE IMP" $
|
||||
do let s = rawSolver sol
|
||||
let (gs,rest) = partition (isNumeric . goal) gs0
|
||||
numAsmp = filter isNumeric ps
|
||||
vs = Set.toList (fvs (numAsmp, map goal gs))
|
||||
tvs <- debugBlock sol "VARIABLES" $
|
||||
do SMT.push s
|
||||
Map.fromList <$> zipWithM (declareVar s) [ 0 .. ] vs
|
||||
debugBlock sol "ASSUMPTIONS" $
|
||||
mapM_ (assume s tvs) numAsmp
|
||||
gs' <- mapM (prove sol tvs) gs
|
||||
SMT.pop s
|
||||
return (catMaybes gs' ++ rest)
|
||||
|
||||
|
||||
declareVar :: SMT.Solver -> Int -> TVar -> IO (TVar, SExpr)
|
||||
declareVar s x v = do let name = (if isFreeTV v then "fv" else "kv") ++ show x
|
||||
e <- SMT.declare s name cryInfNat
|
||||
SMT.assert s (SMT.fun "cryVar" [ e ])
|
||||
return (v,e)
|
||||
|
||||
assume :: SMT.Solver -> TVars -> Prop -> IO ()
|
||||
assume s tvs p = SMT.assert s (SMT.fun "cryAssume" [ toSMT tvs p ])
|
||||
|
||||
prove :: Solver -> TVars -> Goal -> IO (Maybe Goal)
|
||||
prove sol tvs g =
|
||||
debugBlock sol "PROVE" $
|
||||
do let s = rawSolver sol
|
||||
SMT.push s
|
||||
SMT.assert s (SMT.fun "cryProve" [ toSMT tvs (goal g) ])
|
||||
res <- SMT.check s
|
||||
SMT.pop s
|
||||
case res of
|
||||
SMT.Unsat -> return Nothing
|
||||
_ -> return (Just g)
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
isNumeric :: Prop -> Bool
|
||||
isNumeric ty = matchDefault False
|
||||
$ msum [ is (|=|), is (|>=|), is aFin, is aTrue, andNum ty ]
|
||||
where
|
||||
andNum t = anAdd t >>= \(x,y) -> return (isNumeric x && isNumeric y)
|
||||
is f = f ty >> return True
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
type TVars = Map TVar SExpr
|
||||
|
||||
cryInfNat :: SExpr
|
||||
cryInfNat = SMT.const "InfNat"
|
||||
|
||||
|
||||
toSMT :: TVars -> Type -> SExpr
|
||||
toSMT tvs ty = matchDefault (panic "toSMT" [ "Unexpected type", show ty ])
|
||||
$ msum $ map (\f -> f tvs ty)
|
||||
[ aInf ~> "cryInf"
|
||||
, aNat ~> "cryNat"
|
||||
|
||||
, aFin ~> "cryFin"
|
||||
, (|=|) ~> "cryEq"
|
||||
, (|>=|) ~> "cryGeq"
|
||||
, aAnd ~> "cryAnd"
|
||||
, aTrue ~> "cryTrue"
|
||||
|
||||
, anAdd ~> "cryAdd"
|
||||
, (|-|) ~> "crySub"
|
||||
, aMul ~> "cryMul"
|
||||
, (|^|) ~> "cryExp"
|
||||
, (|/|) ~> "cryDiv"
|
||||
, (|%|) ~> "cryMod"
|
||||
, aMin ~> "cryMin"
|
||||
, aMax ~> "cryMax"
|
||||
, aWidth ~> "cryWidth"
|
||||
, aLenFromThen ~> "cryLenFromThen"
|
||||
, aLenFromThenTo ~> "cryLenFromThenTo"
|
||||
|
||||
, aTVar ~> "(unused)"
|
||||
]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
(~>) :: Mk a => (Type -> Match a) -> String -> TVars -> Type -> Match SExpr
|
||||
(m ~> f) tvs t = m t >>= \a -> return (mk tvs f a)
|
||||
|
||||
class Mk t where
|
||||
mk :: TVars -> String -> t -> SExpr
|
||||
|
||||
instance Mk () where
|
||||
mk _ f _ = SMT.const f
|
||||
|
||||
instance Mk Integer where
|
||||
mk _ f x = SMT.fun f [ SMT.int x ]
|
||||
|
||||
instance Mk TVar where
|
||||
mk tvs _ x = tvs Map.! x
|
||||
|
||||
instance Mk Type where
|
||||
mk tvs f x = SMT.fun f [toSMT tvs x]
|
||||
|
||||
instance Mk (Type,Type) where
|
||||
mk tvs f (x,y) = SMT.fun f [ toSMT tvs x, toSMT tvs y]
|
||||
|
||||
instance Mk (Type,Type,Type) where
|
||||
mk tvs f (x,y,z) = SMT.fun f [ toSMT tvs x, toSMT tvs y, toSMT tvs z ]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user