jukebox 0.3.1 → 0.3.2
raw patch · 4 files changed
+105/−89 lines, 4 files
Files
- jukebox.cabal +1/−1
- src/Jukebox/Options.hs +6/−2
- src/Jukebox/SMTLIB.hs +1/−1
- src/Jukebox/Tools/HornToUnit.hs +97/−85
jukebox.cabal view
@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.3.1+Version: 0.3.2 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone
src/Jukebox/Options.hs view
@@ -354,10 +354,14 @@ -- Running the parser. parseCommandLine :: String -> OptionParser a -> IO a-parseCommandLine description p = do+parseCommandLine description p =+ parseCommandLineWithExtraArgs [] description p++parseCommandLineWithExtraArgs :: [String] -> String -> OptionParser a -> IO a+parseCommandLineWithExtraArgs args0 description p = do name <- getProgName args <- getArgs- parseCommandLineWithArgs name args description p+ parseCommandLineWithArgs name (args0 ++ args) description p parseCommandLineWithArgs :: String -> [String] -> String -> OptionParser a -> IO a parseCommandLineWithArgs name args description p = do
src/Jukebox/SMTLIB.hs view
@@ -86,7 +86,7 @@ , "select" , "subset", "union", "intersect" -- CVC4:- , "concat", "member", "singleton"+ , "concat", "member", "singleton", "card" ] ++ map snd renamings renamings :: [(String, String)]
src/Jukebox/Tools/HornToUnit.hs view
@@ -38,13 +38,14 @@ data HornFlags = HornFlags {- allowNonUnitConjectures :: Bool,+ allowConjunctiveConjectures :: Bool,+ allowDisjunctiveConjectures :: Bool, allowNonGroundConjectures :: Bool, allowCompoundConjectures :: Bool, dropNonHorn :: Bool, passivise :: Bool, multi :: Bool,- extra :: Bool,+ smaller :: Bool, encoding :: Encoding } deriving Show @@ -55,9 +56,12 @@ hornFlags = inGroup "Horn clause encoding options" $ HornFlags <$>- bool "non-unit-conjectures"- ["Allow conjectures to be non-unit clauses (off by default)."]- False <*>+ bool "conjunctive-conjectures"+ ["Allow conjectures to be conjunctions of equations (on by default)."]+ True <*>+ bool "disjunctive-conjectures"+ ["Allow conjectures to be disjunctions of equations (on by default)."]+ True <*> bool "non-ground-conjectures" ["Allow conjectures to be non-ground clauses (on by default)."] True <*>@@ -73,20 +77,20 @@ bool "multi" ["Encode multiple left-hand sides at once (off by default)."] False <*>- bool "extra"- ["Encode Horn axioms (off by default)."]+ bool "smaller"+ ["Swap ordering of certain equations (off by default)"] False <*> encoding where encoding = flag "conditional-encoding"- ["Which method to use to encode conditionals (asymmetric1 by default)."]+ ["Which method to use to encode conditionals (if-then-else by default)."] Asymmetric1 (argOption- [("symmetric", Symmetric),- ("asymmetric1", Asymmetric1),- ("asymmetric2", Asymmetric2),- ("asymmetric3", Asymmetric3)])+ [("if-then", Symmetric),+ ("if-then-else", Asymmetric1),+ ("fresh", Asymmetric2),+ ("if", Asymmetric3)]) hornToUnit :: HornFlags -> Problem Clause -> IO (Either (Input Clause) (Either Answer (Problem Clause))) hornToUnit flags prob = do@@ -99,37 +103,8 @@ fmap (Right . enc) $ eliminateHornClauses flags $ eliminateUnsuitableConjectures flags $- eliminatePredicates $- if passivise flags then passiviseClauses prob else prob--passiviseClauses :: Problem Clause -> Problem Clause-passiviseClauses prob =- [ c { what = clause ls' }- | (n, c@Input{what = Clause (Bind _ ls)}) <- zip [0..] prob,- ls' <- cls n ls ]- where- cls n ls =- case partition pos ls of- (ps, ns) | length ns >= 1 ->- let- ns' = zipWith (toPred ls n) [0..] ns- in- [(map Neg ns' ++ ps)] ++- [[n, Pos n'] | (n, n') <- zip ns ns']- _ ->- [ls]-- toPred :: [Literal] -> Int -> Int -> Literal -> Atomic- toPred ls m n l =- Tru (p :@: map Var vs)- where- p =- variant "$p" [fresh, name m, name n]- ::: FunType (map typ vs) O- vs = intersect (vars (delete l ls)) (vars l)-- fresh = run_ prob $- newName "fresh"+ eliminateMultiplePreconditions flags $+ eliminatePredicates prob eliminatePredicates :: Problem Clause -> Problem Clause eliminatePredicates prob =@@ -145,6 +120,29 @@ true <- newFunction "true" [] bool return (bool, true :@: []) +eliminateMultiplePreconditions :: HornFlags -> Problem Clause -> Problem Clause+eliminateMultiplePreconditions flags prob+ | otherwise =+ map elim prob+ where+ elim inp+ | length negs /= 1 &&+ if null poss then not (allowConjunctiveConjectures flags) else multi flags =+ inp{what = clause (Neg ((tuple tys :@: ts) :=: (tuple tys :@: us)):poss)}+ where+ (poss, negs) = partition pos (toLiterals (what inp))+ ts = [t | l <- negs, let Neg (t :=: _) = l]+ us = [u | l <- negs, let Neg (_ :=: u) = l]+ tys = map typ ts+ elim inp = inp++ tuple = run_ prob $ do+ tupleType <- newName "tuple"+ tuple <- newName "tuple"+ return $ \args ->+ variant tuple args :::+ FunType args (Type (variant tupleType args))+ eliminateUnsuitableConjectures :: HornFlags -> Problem Clause -> Problem Clause eliminateUnsuitableConjectures flags prob | null bad = prob@@ -155,10 +153,12 @@ where (bad, good) = partition unsuitable prob + ngoals = length $ filter (all (not . pos) . toLiterals . what) prob+ unsuitable c = all (not . pos) ls && ((not (allowCompoundConjectures flags) && or [size t > 1 | t <- terms ls]) ||- (not (allowNonUnitConjectures flags) && length ls /= 1) ||+ (not (allowDisjunctiveConjectures flags) && ngoals > 1) || (not (allowNonGroundConjectures flags) && not (ground ls))) where ls = toLiterals (what c)@@ -166,9 +166,9 @@ addConjecture c = clause (Pos (a :=: b):toLiterals c) (a, b) = run_ prob $ do- token <- newType "token"- a <- newFunction "a" [] token- b <- newFunction "b" [] token+ token <- newType "$token"+ a <- newFunction "$a" [] token+ b <- newFunction "$b" [] token return (a :@: [], b :@: []) eliminateHornClauses :: HornFlags -> Problem Clause -> Either (Input Clause) (Problem Clause)@@ -181,14 +181,18 @@ put $! n+1 return (variant base [name (show n)]) + passiveFresh (x ::: ty)+ | passivise flags = fmap (::: ty) (fresh x)+ | otherwise = return (x ::: ty)++ passive (Var x) = Var x+ passive ((f ::: ty) :@: ts) =+ (variant f [passiveName] ::: ty) :@: map passive ts+ elim1 :: Input Clause -> RWST () [Atomic] Int (Either (Input Clause)) [Input Clause] elim1 c = case partition pos (toLiterals (what c)) of ([], _) -> return [c]- ([Pos l], ls)- | encoding flags == Asymmetric2 && multi flags -> runListT $ do- l <- encodeAsymm2 l ls- return c { what = clause [Pos l] } ([Pos l], ls) -> runListT $ do l <- foldM encode l ls return c { what = clause [Pos l] }@@ -198,22 +202,6 @@ else lift $ Left c - encodeAsymm2 :: Atomic -> [Literal] -> ListT (RWST () [Atomic] Int (Either (Input Clause))) Atomic- encodeAsymm2 l ls = do- ifeqName <- fresh ifeqName- let- vs = Set.toList (Set.unions (map free (l:map the ls)))- lhs (t :=: _) = t- rhs (_ :=: u) = u- ifeq =- ifeqName :::- FunType (map (typ . lhs . the) ls ++ map typ vs)- (typ (lhs l))- app ts = ifeq :@: (ts ++ map Var vs)- msum $ map return [- app (map (lhs . the) ls) :=: lhs l,- app (map (rhs . the) ls) :=: rhs l]- encode :: Atomic -> Literal -> ListT (RWST () [Atomic] Int (Either (Input Clause))) Atomic encode (c :=: d) (Neg (a :=: b)) = let@@ -226,43 +214,66 @@ -- ifeq(x, x, y) = y -- ifeq(a, b, c) = ifeq(a, b, d) Symmetric -> do- let ifeq = variant ifeqName [name ty1, name ty2] ::: FunType [ty1, ty1, ty2] ty2- axiom (ifeq :@: [x, x, y] :=: y)- return (ifeq :@: [a, b, c] :=: ifeq :@: [a, b, d])+ ifeq <- passiveFresh (variant ifeqName [name ty1, name ty2] ::: FunType [ty1, ty1, ty2] ty2)+ if passivise flags then do+ axiom (ifeq :@: [x, x, passive c] :=: c)+ axiom (ifeq :@: [x, x, passive d] :=: d)+ return (ifeq :@: [a, b, passive c] :=: ifeq :@: [a, b, passive d])+ else do+ axiom (ifeq :@: [x, x, y] :=: y)+ return (ifeq :@: [a, b, c] :=: ifeq :@: [a, b, d]) -- ifeq(x, x, y, z) = y -- ifeq(a, b, c, d) = d- -- extra: ifeq(x, y, z, z) = z Asymmetric1 -> do- let- ifeq = variant ifeqName [name ty1, name ty2] ::: FunType [ty1, ty1, ty2, ty2] ty2+ ifeq <- passiveFresh (variant ifeqName [name ty1, name ty2] ::: FunType [ty1, ty1, ty2, ty2] ty2) (c :=: d) <- return (swap size (c :=: d))- axiom (ifeq :@: [x, x, y, z] :=: y)- return (ifeq :@: [a, b, c, d] :=: d) `mplus` do- guard (extra flags)- return (ifeq :@: [x, y, z, z] :=: z)+ if passivise flags then do+ axiom (ifeq :@: [x, x, passive c, y] :=: c)+ return (ifeq :@: [a, b, passive c, passive d] :=: d)+ else do+ axiom (ifeq :@: [x, x, y, z] :=: y)+ return (ifeq :@: [a, b, c, d] :=: d) -- f(a, sigma) = c -- f(b, sigma) = d -- where sigma = FV(a, b, c, d) Asymmetric2 -> do ifeqName <- fresh ifeqName+ (a :=: b) <- return (swap size (a :=: b))+ (c :=: d) <- return (swap size (c :=: d)) let- vs = Set.toList (Set.unions (map free [a, b, c, d]))+ vs =+ if passivise flags then+ map passive [a, b, c, d]+ else+ map Var (Set.toList (Set.unions (map free [a, b, c, d]))) ifeq = ifeqName ::: FunType (ty1:map typ vs) ty2- app t = ifeq :@: (t:map Var vs)- msum $ map return [app a :=: c, app b :=: d]+ app t = ifeq :@: (t:vs)+ if smaller flags then do+ axiom (app b :=: d)+ return (app a :=: c)+ else do+ axiom (app a :=: c)+ return (app b :=: d) -- f(a, b, sigma) = c -- f(x, x, sigma) = d -- where sigma = FV(c, d) Asymmetric3 -> do ifeqName <- fresh ifeqName+ (c :=: d) <- return (swap size (c :=: d)) let- vs = Set.toList (Set.unions (map free [c, d]))+ vs =+ if passivise flags then+ map passive [c, d]+ else+ map Var (Set.toList (Set.unions (map free [c, d]))) ifeq = ifeqName ::: FunType (ty1:ty1:map typ vs) ty2- app t u = ifeq :@: (t:u:map Var vs)+ app t u = ifeq :@: (t:u:vs) x = Var (xvar ::: ty1)- msum $ map return [app a b :=: c, app x x :=: d]+ axiom (app x x :=: c)+ return (app a b :=: d) swap f (t :=: u) =+ (\(t :=: u) -> if smaller flags then u :=: t else t :=: u) $ if f t >= f u then (t :=: u) else (u :=: t) axiom l = lift $ tell [l]@@ -274,12 +285,13 @@ source = Unknown, what = clause [Pos l] } - (ifeqName, xvar, yvar, zvar) = run_ prob $ do+ (ifeqName, passiveName, xvar, yvar, zvar) = run_ prob $ do ifeqName <- newName "$ifeq"+ passiveName <- newName "$passive" xvar <- newName "A" yvar <- newName "B" zvar <- newName "C"- return (ifeqName, xvar, yvar, zvar)+ return (ifeqName, passiveName, xvar, yvar, zvar) -- Soundly encode types, but try to erase them if possible. -- Based on the observation that if the input problem is untyped,