diff --git a/jukebox.cabal b/jukebox.cabal --- a/jukebox.cabal +++ b/jukebox.cabal @@ -1,5 +1,5 @@ Name: jukebox -Version: 0.3.1 +Version: 0.3.2 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone diff --git a/src/Jukebox/Options.hs b/src/Jukebox/Options.hs --- a/src/Jukebox/Options.hs +++ b/src/Jukebox/Options.hs @@ -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 diff --git a/src/Jukebox/SMTLIB.hs b/src/Jukebox/SMTLIB.hs --- a/src/Jukebox/SMTLIB.hs +++ b/src/Jukebox/SMTLIB.hs @@ -86,7 +86,7 @@ , "select" , "subset", "union", "intersect" -- CVC4: - , "concat", "member", "singleton" + , "concat", "member", "singleton", "card" ] ++ map snd renamings renamings :: [(String, String)] diff --git a/src/Jukebox/Tools/HornToUnit.hs b/src/Jukebox/Tools/HornToUnit.hs --- a/src/Jukebox/Tools/HornToUnit.hs +++ b/src/Jukebox/Tools/HornToUnit.hs @@ -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,