GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-18 05:21:57 +03:00
Code Issues Projects Releases Wiki Activity

Hook-in incomplete new solver.

Browse Source
This commit is contained in:
Iavor S. Diatchki 2014-12-04 14:40:09 -08:00
parent 207e3854fc
commit 8d3a7e7b4f
3 changed files with 80 additions and 104 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

136
src/Cryptol/TypeCheck/Solve.hs
View File

@ -25,7 +25,8 @@ import Cryptol.TypeCheck.Solver.Numeric
import Cryptol.TypeCheck.Solver.Class
import Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
import qualified Cryptol.TypeCheck.Solver.Smtlib as SMT
import qualified Cryptol.TypeCheck.Solver.CrySAT as CM
import qualified Cryptol.TypeCheck.Solver.Numeric.AST as Num
import qualified Cryptol.TypeCheck.Solver.CrySAT as Num
import Cryptol.TypeCheck.Defaulting(tryDefaultWith)
@ -51,95 +52,64 @@ checkTypeFunction _ _ = []
-- probably be good to try solving all of these in one big loop.
simplifyAllConstraints :: InferM ()
simplifyAllConstraints =
do mapM_ tryHasGoal =<< getHasGoals
simplifyGoals noFacts =<< getGoals
do mapM_ tryHasGoal =<< getHasGoals
gs <- getGoals
addGoals =<< io (simpGoals gs)
proveImplication :: LQName -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication lname as asmps0 goals =
case assumedOrderModel noFacts (concatMap expandProp asmps0) of
Left (_m,p) -> do recordError (UnusableFunction (thing lname) p)
return emptySubst
Right (m,asmps) ->
do let gs = [ g { goal = q } | g <- goals
, let p = goal g
q = simpType m p
, p `notElem` asmps
, q `notElem` asmps
]
proveImplication lname as ps gs =
do let gs1 = filter ((`notElem` ps) . goal) gs
gs2 <- io (simpGoals gs1)
let gs3 = filter ((`notElem` ps) . goal) gs2
(badClass,numCts) = partitionEithers (map numericRight gs3)
badNum <- case numCts of
[] -> return []
_ -> io $ Num.withSolver $ \s ->
do Num.assumeProps s ps
(nonDef,def) <- Num.checkDefined s numCts
def1 <- Num.simplifyProps s def
return (nonDef ++ def1)
case badClass ++ badClass of
[] -> return ()
us -> recordError $ UnsolvedDelcayedCt
$ DelayedCt { dctSource = lname
, dctForall = as
, dctAsmps = ps
, dctGoals = us
}
return emptySubst
(_,gs1) <- collectGoals (simplifyGoals m gs)
let numAsmps = filter pIsNumeric asmps
(numGs,otherGs) = partition (pIsNumeric . goal) gs1
-- | Class goals go on the left, numeric goals go on the right.
numericRight :: Goal -> Either Goal (Goal, Num.Prop)
numericRight g = case Num.exportProp (goal g) of
Just p -> Right (g, p)
Nothing -> Left g
-- | Assumes that the substitution has been applied to the goals.
simpGoals :: [Goal] -> IO [Goal]
simpGoals gs0 =
do let (unsolvedClassCts,numCts) = solveClassCts gs0
case numCts of
[] -> return unsolvedClassCts
_ -> Num.withSolver $ \s ->
do (nonDef,def) <- Num.checkDefined s numCts
def1 <- Num.simplifyProps s def
return (nonDef ++ unsolvedClassCts ++ def1)
gs2 <- io $ SMT.simpDelayed as m numAsmps numGs
case otherGs ++ gs2 of
[] -> return emptySubst
unsolved ->
-- Last resort, let's try to default something.
do let vs = Set.filter isFreeTV $ fvs $ map goal unsolved
evars <- varsWithAsmps
let candidates = vs `Set.difference` evars
if Set.null vs
then reportErr unsolved >> return emptySubst
else do let (_,uns,su,ws) =
tryDefaultWith m (Set.toList candidates) unsolved
mapM_ recordWarning ws
unless (null uns) (reportErr uns)
return su
where
reportErr us = recordError $ UnsolvedDelcayedCt
DelayedCt { dctSource = lname
, dctForall = as
, dctAsmps = asmps0
, dctGoals = us
}
simpGoals :: [Goal] -> Inferm ()
simpGoals gs =
where
(nonNum,nums) = partitionEithers (map numericRight gs)
numericRight g = case exportProp (goal g) of
Just p -> Right (g, p)
Nothing -> Left g
-- | Assumes that the substitution has been applied to the goals
simplifyGoals :: OrdFacts -> [Goal] -> InferM ()
simplifyGoals initOrd gs1 = solveSomeGoals [] False gs1
where
solveSomeGoals others !changes [] =
if changes
then solveSomeGoals [] False others
else addGoals others
solveSomeGoals others !changes (g : gs) =
do let (m, bad, _) = goalOrderModel initOrd (others ++ gs)
if not (null bad)
then mapM_ (recordError . UnsolvedGoal) bad
else
case makeStep m g of
Unsolved -> solveSomeGoals (g : others) changes gs
Unsolvable ->
do recordError (UnsolvedGoal g)
solveSomeGoals others changes gs
Solved Nothing [] -> solveSomeGoals others changes gs
Solved Nothing subs -> solveSomeGoals others True (subs ++ gs)
Solved (Just su) subs ->
do extendSubst su
solveSomeGoals (apSubst su others) True
(subs ++ apSubst su gs)
makeStep m g = case numericStep m g of
Unsolved -> classStep g
x -> x
solveClassRight g = case classStep g of
Just gs -> Right gs
Nothing -> Left g
-- returns (unsolved class constraints, numeric constraints)
solveClassCts [] = ([], [])
solveClassCts gs =
let (classCts,numCts) = partitionEithers (map numericRight gs)
(unsolved,solveds) = partitionEithers (map solveClassRight classCts)
(unsolved',numCts') = solveClassCts (concat solveds)
in (unsolved ++ unsolved', numCts ++ numCts')

24
src/Cryptol/TypeCheck/Solver/Class.hs
View File

@ -12,22 +12,24 @@
module Cryptol.TypeCheck.Solver.Class (classStep, expandProp) where
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.InferTypes(Goal(..), Solved(..))
import Cryptol.TypeCheck.InferTypes(Goal(..))
-- | Solve class constraints.
classStep :: Goal -> Solved
-- If not, then we return 'Nothing'.
-- If solved, ther we return 'Just' a list of sub-goals.
classStep :: Goal -> Maybe [Goal]
classStep g = case goal g of
TCon (PC PArith) [ty] -> solveArithInst g (tNoUser ty)
TCon (PC PCmp) [ty] -> solveCmpInst g (tNoUser ty)
_ -> Unsolved
_ -> Nothing
-- | Solve an original goal in terms of the give sub-goals.
solved :: Goal -> [Prop] -> Solved
solved g ps = Solved Nothing [ g { goal = p } | p <- ps ]
solved :: Goal -> [Prop] -> Maybe [Goal]
solved g ps = Just [ g { goal = p } | p <- ps ]
-- | Solve an Arith constraint by instance, if possible.
solveArithInst :: Goal -> Type -> Solved
solveArithInst :: Goal -> Type -> Maybe [Goal]
solveArithInst g ty = case ty of
-- Arith [n]e
@ -42,25 +44,25 @@ solveArithInst g ty = case ty of
-- (Arith a, Arith b) => Arith { x1 : a, x2 : b }
TRec fs -> solved g [ pArith ety | (_,ety) <- fs ]
_ -> Unsolved
_ -> Nothing
-- | Solve an Arith constraint for a sequence. The type passed here is the
-- element type of the sequence.
solveArithSeq :: Goal -> Type -> Type -> Solved
solveArithSeq :: Goal -> Type -> Type -> Maybe [Goal]
solveArithSeq g n ty = case ty of
-- fin n => Arith [n]Bit
TCon (TC TCBit) [] -> solved g [ pFin n ]
-- variables are not solvable.
TVar {} -> Unsolved
TVar {} -> Nothing
-- Arith ty => Arith [n]ty
_ -> solved g [ pArith ty ]
-- | Solve Cmp constraints.
solveCmpInst :: Goal -> Type -> Solved
solveCmpInst :: Goal -> Type -> Maybe [Goal]
solveCmpInst g ty = case ty of
-- Cmp Bit
@ -75,7 +77,7 @@ solveCmpInst g ty = case ty of
-- (Cmp a, Cmp b) => Cmp { x:a, y:b }
TRec fs -> solved g [ pCmp e | (_,e) <- fs ]
_ -> Unsolved
_ -> Nothing
-- | Add propositions that are implied by the given one.

24
src/Cryptol/TypeCheck/Solver/CrySAT.hs
View File

@ -27,22 +27,21 @@ import qualified SimpleSMT as SMT
-- | Check that a bunch of constraints are all defined.
-- If some are not, we return them on the 'Left'.
-- Otherwise, we return the exported props on the 'Right'.
-- Does not modify the set of assumptions.
checkDefined :: Solver -> [(a,Prop)] -> IO (Either [a] [(a,SMTProp)])
-- We return constraints that are not necessarily defined in the first
-- component, and the ones that are defined in the second component.
checkDefined :: Solver -> [(a,Prop)] -> IO ([a], [(a,SMTProp)])
checkDefined s props0 = withScope s $
go False [] [] [ (a, p, prepareProp (cryDefinedProp p)) | (a,p) <- props0 ]
where
-- Everything is defined: keep going.
go _ isDef [] [] = return (Right isDef)
go _ isDef [] [] = return ([], isDef)
-- We have possibly non-defined, but we also added a new fact: go again.
go True isDef isNotDef [] = go False isDef [] isNotDef
-- We have possibly non-defined, and nothing changed: report error.
go False _ isNotDef [] = return (Left [ ct | (ct,_,_) <- isNotDef ])
go False isDef isNotDef [] = return ([ a | (a,_,_) <- isNotDef ], isDef)
-- Process one constraint.
go ch isDef isNotDef ((ct,p,q) : more) =
@ -76,6 +75,10 @@ assumeProps s props =
mapM_ (assert s . prepareProp) (map cryDefinedProp ps ++ ps)
where ps = mapMaybe exportProp props
--------------------------------------------------------------------------------
exportProp :: Cry.Prop -> Maybe Prop
@ -215,8 +218,8 @@ viPop VarInfo { .. } = case otherScopes of
-- | Execute a computation with a fresh solver instance.
withSolver :: (Solver -> IO a) -> IO a
withSolver k =
do l <- SMT.newLogger
solver <- SMT.newSolver "cvc4" ["--lang=smt2", "--incremental"] (Just l)
do _l <- SMT.newLogger
solver <- SMT.newSolver "cvc4" ["--lang=smt2", "--incremental"] Nothing -- (Just l)
SMT.setLogic solver "QF_LIA"
declared <- newIORef viEmpty
a <- k Solver { .. }
@ -245,8 +248,9 @@ declareVar Solver { .. } a =
-- | Add an assertion to the current context.
assert :: Solver -> SMTProp -> IO ()
assert Solver { .. } SMTProp { .. } =
do SMT.assert solver smtpLinPart
assert s@Solver { .. } SMTProp { .. } =
do mapM_ (declareVar s) (Set.toList smtpVars)
SMT.assert solver smtpLinPart
modifyIORef' declared (viAssert smtpNonLinPart)