Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
base fork: jwaldmann/satchmo-smt
base: 68b6b693dd
...
head fork: jwaldmann/satchmo-smt
compare: 60b8ba663a
  • 3 commits
  • 19 files changed
  • 0 commit comments
  • 1 contributor
View
23 Main.hs
@@ -6,6 +6,7 @@
-- Accepts input logic QF_LIA, QF_LRA, QF_IDL
-- but actually all variables are assumed to be non-negative integers.
+-- (also QF_Arctic, QF_Tropical, QF_Fuzzy)
-- Assumption: input contains exactly one (check-sat)
-- followed by (get-value) for all global names.
@@ -13,6 +14,7 @@
import Satchmo.SMT.Config
import Satchmo.SMT.Solve
+
import Language.SMTLIB
import qualified Data.Map as M
@@ -30,25 +32,8 @@ main = do
mapM_ print $ case output of
Nothing -> [ Cs_response Unknown ]
- Just m -> [ Cs_response Sat
- , Gv_response $ do
- (k,v) <- M.toList m
- return ( sym2term k , case v of
- Value_Integer i -> int2term i
- Value_Bool b -> bool2term b
- )
+ Just values -> [ Cs_response Sat
+ , Gv_response values
]
-sym2term fun =
- Term_qual_identifier ( Qual_identifier ( Identifier fun ))
-
-int2term int =
- if int >= 0
- then Term_spec_constant ( Spec_constant_numeral int )
- else Term_qual_identifier_ ( Qual_identifier ( Identifier "-"))
- [ int2term $ negate int ]
-
-bool2term b =
- Term_qual_identifier $ Qual_identifier $ Identifier $ case b of
- False -> "false" ; True -> "true"
View
30 Satchmo/SMT/Config.hs
@@ -2,24 +2,42 @@ module Satchmo.SMT.Config where
import System.Console.GetOpt
-data Encoding = Unary { bits :: Int }
- | Binary { bits :: Int }
- deriving Show
+data Encoding = Unary | Binary deriving Show
+data Unary_Addition = Odd_Even_Merge | Bitonic_Sort | Quadratic deriving Show
+data Extension = Fixed | Flexible deriving Show
data Config =
Config { encoding :: Encoding
+ , unary_addition :: Unary_Addition
+ , bits :: Int
+ , extension :: Extension
}
deriving Show
-config0 = Config { encoding = Unary 8 }
+config0 = Config { encoding = Unary, unary_addition = Quadratic, bits = 5, extension = Fixed }
options =
[ Option "u" [ "unary" ]
- ( ReqArg ( \ s conf -> conf { encoding = Unary { bits = read s }}) "INT")
+ ( ReqArg ( \ s conf -> conf { encoding = Unary , bits = read s }) "INT")
"use unary encoding with given number of bits"
+ , Option "o" [ "odd-even" ]
+ ( NoArg $ \ conf -> conf { unary_addition = Odd_Even_Merge } )
+ "unary addition via odd-even-merge"
+ , Option "n" [ "bitonic" ]
+ ( NoArg $ \ conf -> conf { unary_addition = Bitonic_Sort } )
+ "unary addition via bitonic sort"
+ , Option "q" [ "quadratic" ]
+ ( NoArg $ \ conf -> conf { unary_addition = Quadratic } )
+ "unary addition via bitonic sort"
, Option "b" [ "binary" ]
- ( ReqArg ( \ s conf -> conf { encoding = Binary { bits = read s }}) "INT")
+ ( ReqArg ( \ s conf -> conf { encoding = Binary , bits = read s }) "INT")
"use binary encoding with given number of bits"
+ , Option "i" [ "fixed" ]
+ ( NoArg $ \ conf -> conf { extension = Fixed } )
+ "fixed bit width (also for intermediate results)"
+ , Option "l" [ "flexible" ]
+ ( NoArg $ \ conf -> conf { extension = Flexible } )
+ "flexible bit width (increase as needed for intermediates)"
]
parse_options argv = case getOpt Permute options argv of
View
69 Satchmo/SMT/Exotic/Arctic.hs
@@ -0,0 +1,69 @@
+{-# language FlexibleInstances #-}
+{-# language FlexibleContexts #-}
+{-# language MultiParamTypeClasses #-}
+
+module Satchmo.SMT.Exotic.Arctic where
+
+import Satchmo.SMT.Exotic.Dict
+import Language.SMTLIB
+
+import qualified Data.Map as M
+
+import qualified Satchmo.Unary.Op.Flexible as X
+import qualified Satchmo.Unary as N
+import qualified Satchmo.Boolean as B
+
+import Satchmo.Code
+import Satchmo.SAT.Mini (SAT)
+import Control.Monad (forM, guard, when)
+
+import qualified Satchmo.SMT.Exotic.Semiring.Arctic as A
+
+
+data Arctic = Arctic { contents :: N.Number
+ }
+
+minus_infinite = B.not . head . N.bits . contents
+
+instance ( Decode m B.Boolean Bool )
+ => Decode m Arctic ( A.Arctic Integer ) where
+ decode a = do
+ c <- decode $ contents a
+ return $ if 0 == c then A.Minus_Infinite else A.Finite (c-1)
+
+make c = do
+ return $ Arctic { contents = c }
+
+dict :: Int
+ -> Dict SAT ( A.Arctic Integer ) Arctic B.Boolean
+dict bits = Dict { domain = Proof.Arctic
+ , fresh = do
+ c <- N.number bits
+ make c
+ , finite = \ x -> return $ B.not $ minus_infinite x
+ , ge = \ l r -> N.ge ( contents l ) ( contents r )
+ , gg = \ l r ->
+ B.monadic B.or [ return $ minus_infinite r
+ , N.gt ( contents l ) ( contents r )
+ ]
+ , plus = \ xs -> do
+ c <- X.maximum $ map contents xs
+ make c
+ , times = \ [s,t] -> do
+ m <- B.or [ minus_infinite s, minus_infinite t ]
+ let a = contents s ; b = contents t
+ let width = length $ N.bits a
+ when ( length ( N.bits b ) /= width )
+ $ error "Arctic.times: different bit widths"
+ pairs <- sequence $ do
+ (i,x) <- zip [0 .. ] $ N.bits a
+ (j,y) <- zip [0 .. ] $ N.bits b
+ guard $ i+j <= width
+ return $ do z <- B.and [x,y] ; return (i+j, [z])
+ cs <- forM ( map snd $ M.toAscList $ M.fromListWith (++) pairs ) B.or
+ -- overflow is not allowed
+ B.assert [ B.not $ last cs ]
+ ds <- forM (init cs) $ \ c -> B.and [ B.not m, c ]
+ make $ N.make ds
+ }
+
View
84 Satchmo/SMT/Exotic/Check.hs
@@ -0,0 +1,84 @@
+{-# language FlexibleInstances #-}
+{-# language UndecidableInstances #-}
+{-# language FlexibleContexts #-}
+{-# language MultiParamTypeClasses #-}
+
+module Exotic.Check where
+
+import Exotic.Dict
+
+import Language.SMTLIB
+import qualified Data.Map as M
+
+import qualified Semiring.Fuzzy as F
+import qualified Semiring as S
+
+import Control.Monad ( forM_, forM )
+import Control.Monad.State.Strict
+
+import System.IO
+
+execute :: (Eq a, Show a, S.Semiring a)
+ => M.Map String a -> Script -> IO ( )
+execute m (Script cs) =
+ evalStateT ( forM_ cs command ) m
+
+command c = case c of
+ Set_option ( Produce_models True ) -> return ()
+ Set_logic l -> return () -- UNCHECKED
+ Set_info _ -> return ()
+ Declare_fun f [] ( Sort_identifier ( Identifier s )) -> return ()
+ Define_fun f [] (Sort_identifier ( Identifier s) ) x -> do
+ a <- term x
+ m <- get ; let a' = m M.! f
+ when ( a /= a' ) $ error $ unlines
+ [ "Exotic.Check.command: conflict"
+ , "command: " ++ show c
+ , "computed: " ++ show a
+ , "stored: " ++ show a'
+ ]
+ Assert f -> do
+ v <- formula f
+ when ( v /= True ) $ error $ unlines
+ [ "Exotic.Check.assert: conflict"
+ , "formula: " ++ show c
+ , "computed: " ++ show v
+ ]
+ Check_sat -> return ()
+ Get_value _ -> return ()
+ _ -> error $ "cannot handle command " ++ show c
+
+formula :: (S.Semiring a, MonadState (M.Map Symbol a) m) => Term -> m Bool
+formula f = case f of
+ Term_attributes f [ Attribute_s_expr ":named" _ ] -> formula f
+ Term_qual_identifier (Qual_identifier (Identifier "true")) -> do
+ return $ True
+ Term_qual_identifier (Qual_identifier (Identifier "false")) -> do
+ return $ False
+ Term_qual_identifier_ ( Qual_identifier ( Identifier fun )) args ->
+ case fun of
+ "and" -> do xs <- forM args formula ; return $ and xs
+ "or" -> do xs <- forM args formula ; return $ or xs
+ ">=" -> do [l,r] <- forM args term ; return $ S.ge l r
+ ">>" -> do [l,r] <- forM args term ; return $ S.gt l r
+ "finite" -> do
+ [x] <- forM args term
+ return $ S.strictly_positive x
+ _ -> error $ "Exotic.Check.formula.1: " ++ show f
+ _ -> error $ "Exotic.Check.formula.2: " ++ show f
+
+
+term :: (S.Semiring a, MonadState (M.Map Symbol a) m) => Term -> m a
+term t = case t of
+ Term_qual_identifier ( Qual_identifier ( Identifier fun )) -> do
+ m <- get
+ case M.lookup fun m of
+ Just x -> return x
+ _ -> error $ "Exotic.Check.term: not bound: " ++ show t
+ Term_qual_identifier_ ( Qual_identifier ( Identifier fun )) args ->
+ case fun of
+ "+" -> do xs <- forM args term ; return $ foldr (S.plus) S.zero xs
+ "*" -> do xs <- forM args term ; return $ foldr (S.times) S.one xs
+ _ -> error $ "Exotic.Check.term.1: " ++ show t
+ _ -> error $ "Exotic.Check.term.2: " ++ show t
+
View
13 Satchmo/SMT/Exotic/Dict.hs
@@ -0,0 +1,13 @@
+module Satchmo.SMT.Exotic.Dict where
+
+data Dict m d e b = Dict
+ { fresh :: m e
+ , finite :: e -> m b
+ , gg :: e -> e -> m b
+ , ge :: e -> e -> m b
+ , plus :: [e] -> m e
+ , times :: [e] -> m e
+ }
+
+logic dict = "QF_" ++ show ( domain dict )
+
View
63 Satchmo/SMT/Exotic/Fuzzy.hs
@@ -0,0 +1,63 @@
+{-# language FlexibleInstances #-}
+{-# language FlexibleContexts #-}
+{-# language MultiParamTypeClasses #-}
+
+module Satchmo.SMT.Exotic.Fuzzy where
+
+import Satchmo.SMT.Exotic.Dict
+
+import qualified Satchmo.Unary.Op.Flexible as X
+import qualified Satchmo.Unary as N
+import qualified Satchmo.Boolean as B
+
+import Satchmo.Code
+
+import Language.SMTLIB
+import qualified Data.Map as M
+import qualified Satchmo.SMT.Exotic.Semiring as S
+import qualified Satchmo.SMT.Exotic.Semiring.Fuzzy as F
+
+
+import Satchmo.SAT.Mini ( SAT)
+
+data Fuzzy = Fuzzy { contents :: N.Number }
+
+minus_infinite f = B.not $ head $ N.bits $ contents f
+plus_infinite f = last $ N.bits $ contents f
+
+make = \ c -> do
+ return $ Fuzzy { contents = c }
+
+
+instance ( Decode m B.Boolean Bool, Decode m N.Number Integer )
+ => Decode m Fuzzy ( F.Fuzzy Integer ) where
+ decode a = do
+ p <- decode $ plus_infinite a
+ c <- decode $ contents a
+ m <- decode $ minus_infinite a
+ return $ if p then F.Plus_Infinite
+ else if m then F.Minus_Infinite
+ else F.Finite c
+
+dict :: Int -> Dict SAT ( F.Fuzzy Integer ) Fuzzy B.Boolean
+dict bits = Dict { domain = Proof.Fuzzy
+ , fresh = do
+ c <- N.number bits
+ make c
+ , finite = \ x -> return $ B.not $ plus_infinite x
+ , ge = \ l r ->
+ B.monadic B.or [ return $ plus_infinite l
+ , return $ minus_infinite r
+ , N.gt ( contents l ) ( contents r )
+ ]
+ , gg = \ l r ->
+ B.monadic B.or [ return $ plus_infinite l
+ , N.gt ( contents l ) ( contents r )
+ ]
+ , plus = \ xs -> do -- min
+ c <- X.minimum $ map contents xs
+ make c
+ , times = \ xs -> do -- max
+ c <- X.maximum $ map contents xs
+ make c
+ }
View
196 Satchmo/SMT/Exotic/Generate.hs
@@ -0,0 +1,196 @@
+{-# language FlexibleContexts #-}
+{-# language RankNTypes #-}
+
+module Exotic.Generate where
+
+import Strategy
+import Remove ( Prover, Processor )
+import Claim
+import qualified Proof
+import qualified Matrix
+import Config hiding ( domain )
+
+import Exotic.Dict ( Dict ,logic, domain )
+import qualified Exotic.Solve
+import qualified Exotic.Check
+
+import qualified SMT.Meta
+import SMT.Util
+import Prelude hiding ( and, or )
+
+import qualified Semiring as S
+
+import Satchmo.SAT.Mini ( SAT)
+import Satchmo.Code ( Decode )
+import qualified Satchmo.Boolean as B
+
+import TPDB.Pretty
+import qualified TPDB.Data as T
+import Language.SMTLIB
+
+import Control.Monad.RWS hiding ( mplus, All )
+import Control.Monad.Trans
+
+import qualified Data.Set as S
+import qualified Data.Map as M
+import Data.List ( nub, transpose )
+
+symbolic :: ( S.Semiring d, Pretty d, Eq d, Show d
+ , Pretty a, Ord a, Pretty ( T.SRS a )
+ , Decode SAT e d )
+ => Dict SAT d e B.Boolean
+ -> Config
+ -> Claim a
+ -> IO ( Maybe ( Proof.Interpretation a ))
+symbolic dict conf c = do
+ let ( decoder, _, w) = runRWS ( claim dict conf c ) () 0
+ s = Script w
+ out <-
+ if True
+ then do
+ out_sat <- SMT.Meta.logged conf
+ ( Exotic.Solve.execute dict ) s
+ return -- $ fmap ( M.map $ fmap fromInteger )
+ $ out_sat
+ else do
+ let ( sc, back ) = undefined -- transform dict s
+ out_z3 <- SMT.Meta.solve ( solvers conf ) sc
+ return $ fmap back out_z3
+
+ case out of
+ Just m -> Exotic.Check.execute m s
+ Nothing -> return ()
+ return $ fmap decoder out
+
+
+claim :: ( S.Semiring d, Pretty d, Pretty a, Ord a, Decode SAT e d )
+ => Dict SAT d e B.Boolean
+ -> Config
+ -> Claim a
+ -> Sym ( M.Map Symbol d -> Proof.Interpretation a )
+claim dict conf c = do
+ let [dim] = dims conf
+ tell [ Set_option $ Produce_models True ]
+ when (unsatcore conf) $ do
+ tell [ Set_option $ Produce_unsat_cores True ]
+ tell [ Set_logic $ logic dict ]
+ tell [ Set_info $ Attribute_s_expr ":source"
+ $ S_expr_symbol
+ $ "|remove " ++ show (remove conf) ++ " strict rules from\n"
+ ++ show (pretty $ system c)
+ ++ "\nby matrix interpretation with dimension " ++ show dim ++ "|"
+ ]
+
+ let sig = Data.List.nub $ do
+ u <- T.rules $ system c ; T.lhs u ++ T.rhs u
+ int <- interpretation dict sig dim
+ tell [ Assert $ monotone (property c) int ]
+
+ rs <- forM ( T.rules $ system c ) $ \ u -> do
+ l <- eval dict int $ T.lhs u
+ r <- eval dict int $ T.rhs u
+ return ( T.strict u, (l, r))
+
+ case remove conf of
+ Some -> do
+ assert $ and $ for rs $ \ ( s, (l,r)) -> weakly_greater l r
+ assert $ or $ for (filter fst rs) $ \ ( True, (l,r)) ->
+ strictly_greater l r
+ All -> assert $ and $ for rs $ \ ( s, (l,r)) ->
+ let rel = if s then strictly_greater else weakly_greater
+ in rel l r
+ tell [ Check_sat ]
+
+ case unsatcore conf of
+ True -> tell [ Get_unsat_core ]
+ False -> do
+ top <- get
+ tell [ Get_value $ do
+ k <- [ 0 .. top-1 ]
+ -- FIXME ("f" cannot be right)
+ return $ sym2term $ "f" ++ show k
+ ]
+
+ return $ decode dict dim int
+
+decode dict dim int m =
+ let int' = flip M.map int $ \ l ->
+ let get ( Term_qual_identifier ( Qual_identifier ( Identifier f))) = m M.! f
+ c = for ( coeff l ) $ \ row -> for row get
+ a = for ( absolute l ) $ \ row -> for row get
+ in Matrix.Matrix $ zipWith (++)
+ ( c ++ [ replicate dim S.zero ] )
+ ( a ++ [[ S.one ]] )
+ in Proof.Interpretation ( Exotic.Dict.domain dict ) int'
+
+
+type Matrix = [[ Term ]]
+
+data Linear = Linear { coeff :: Matrix , absolute :: Matrix }
+
+matrices l = [ coeff l , absolute l ]
+
+-- linear :: Dict d -> Int -> Sym Linear
+linear dict dim = do
+ m <- matrix dict (dim,dim)
+ a <- matrix dict (dim,1)
+ return $ Linear m a
+
+-- matrix :: Dict d -> (Int,Int) -> Sym Matrix
+matrix dict (height, width) =
+ forM [ 1 .. height ] $ \ i -> forM [ 1 .. width ] $ \ j ->
+ declare $ show $ domain dict
+
+-- interpretation :: Ord a => Dict d -> [a] -> Int -> Sym ( M.Map a Linear )
+interpretation dict sig dim = do
+ pairs <- forM sig $ \ a -> do m <- linear dict dim ; return ( a, m )
+ return $ M.fromList pairs
+
+-- times :: Dict d -> Linear -> Linear -> Sym Linear
+times dict f g = do
+ c <- mtimes dict ( coeff f ) ( coeff g )
+ a <- mtimes dict ( coeff f ) ( absolute g )
+ b <- mplus dict ( absolute f ) a
+ return $ Linear c b
+
+-- mtimes :: Dict d -> Matrix -> Matrix -> Sym Matrix
+mtimes dict a b = forM a $ \ row ->
+ forM ( transpose b ) $ \ col ->
+ manifest dict $ dot row col
+
+-- mplus :: Dict d -> Matrix -> Matrix -> Sym Matrix
+mplus dict a b = forM ( zip a b) $ \ (c,d) ->
+ forM ( zip c d) $ \ (x,y) ->
+ manifest dict $ apply "+" [x,y]
+
+dot :: [Term] -> [Term] -> Term
+dot xs ys = apply "+" $ for ( zip xs ys ) $ \ (x,y) -> apply "*" [x,y]
+
+-- manifest :: Dict d -> Term -> Sym Term
+manifest dict x = do
+ define ( show $ domain dict ) x
+
+eval dict int w = foldM1 (flip $ times dict)
+ $ for ( reverse w ) $ \ a -> int M.! a
+foldM1 f (z : zs) = foldM f z zs
+
+strictly_greater :: Linear -> Linear -> Term
+strictly_greater f g =
+ and $ for ( zip ( matrices f ) ( matrices g ) ) $ \ (a,b) ->
+ and $ for ( zip a b ) $ \ (r,s) ->
+ and $ for ( zip r s ) $ \ (x,y) -> apply ">>" [x,y]
+
+weakly_greater :: Linear -> Linear -> Term
+weakly_greater f g =
+ and $ for ( zip ( matrices f ) ( matrices g ) ) $ \ (a,b) ->
+ and $ for ( zip a b ) $ \ (r,s) ->
+ and $ for ( zip r s ) $ \ (x,y) -> apply ">=" [x,y]
+
+monotone prop int =
+ and $ for (M.elems int) $ \ l -> ( case prop of
+ Top_Termination ->
+ \ f -> or [ apply "finite" [ head $ head $ absolute l ]
+ , f ]
+ Termination -> id
+ ) $ apply "finite" [ head $ head $ coeff l ]
+
View
10 Satchmo/SMT/Exotic/Semiring.hs
@@ -0,0 +1,10 @@
+{-# language TypeSynonymInstances, FlexibleInstances, UndecidableInstances #-}
+
+module Satchmo.SMT.Exotic.Semiring
+
+( module Satchmo.SMT.Exotic.Semiring.Class )
+
+where
+
+import Satchmo.SMT.Exotic.Semiring.Class
+
View
28 Satchmo/SMT/Exotic/Semiring/Arctic.hs
@@ -0,0 +1,28 @@
+module Satchmo.SMT.Exotic.Semiring.Arctic where
+
+import Satchmo.SMT.Exotic.Semiring.Class
+
+data Arctic a = Minus_Infinite | Finite a deriving (Eq, Ord)
+
+instance Functor Arctic where
+ fmap f a = case a of
+ Minus_Infinite -> Minus_Infinite
+ Finite x -> Finite $ f x
+
+instance Show a => Show ( Arctic a ) where
+ show a = case a of
+ Minus_Infinite -> "-"
+ Finite x -> show x
+
+instance (Ord a, Num a) => Semiring (Arctic a) where
+ strictness _ = Half
+ nonnegative a = True -- ??
+ strictly_positive a = case a of Finite x -> x >= 0 ; _ -> False
+ ge = (>=)
+ gt x y = y == Minus_Infinite || (x > y)
+ plus = max
+ zero = Minus_Infinite
+ times x y = case (x,y) of
+ (Finite a, Finite b) -> Finite (a+b)
+ _ -> Minus_Infinite
+ one = Finite 0
View
18 Satchmo/SMT/Exotic/Semiring/Class.hs
@@ -0,0 +1,18 @@
+{-# language TypeSynonymInstances, FlexibleInstances, UndecidableInstances #-}
+
+module Satchmo.SMT.Exotic.Semiring.Class where
+
+data Strictness = Full | Half deriving ( Eq, Ord, Show )
+
+class Semiring a where
+ strictness :: a -> Strictness
+ nonnegative :: a -> Bool
+ strictly_positive :: a -> Bool
+ ge :: a -> a -> Bool
+ gt :: a -> a -> Bool
+ plus :: a -> a -> a
+ zero :: a
+ times :: a -> a -> a
+ one :: a
+
+
View
28 Satchmo/SMT/Exotic/Semiring/Fuzzy.hs
@@ -0,0 +1,28 @@
+module Satchmo.SMT.Exotic.Semiring.Fuzzy where
+
+import Satchmo.SMT.Exotic.Semiring.Class
+
+data Fuzzy a = Minus_Infinite | Finite a | Plus_Infinite deriving (Eq, Ord)
+
+instance Functor Fuzzy where
+ fmap f a = case a of
+ Minus_Infinite -> Minus_Infinite
+ Finite x -> Finite $ f x
+ Plus_Infinite -> Plus_Infinite
+
+instance Show a => Show ( Fuzzy a ) where
+ show a = case a of
+ Minus_Infinite -> "-"
+ Finite x -> show x
+ Plus_Infinite -> "+"
+
+instance (Ord a, Num a) => Semiring (Fuzzy a) where
+ strictness _ = Half
+ nonnegative a = case a of Plus_Infinite -> False ; _ -> True
+ strictly_positive = nonnegative -- CHECK
+ ge x y = x == Plus_Infinite || (x > y) || y == Minus_Infinite
+ gt x y = x == Plus_Infinite || (x > y)
+ plus = min
+ zero = Plus_Infinite
+ times = max
+ one = Minus_Infinite
View
9 Satchmo/SMT/Exotic/Semiring/Integer.hs
@@ -0,0 +1,9 @@
+module Semiring.Integer where
+
+import Semiring.Class
+
+instance Semiring Integer where
+ strictness _ = Full
+ nonnegative x = x >= 0 ; strictly_positive x = x >= 1
+ ge = (>=) ; gt = (>)
+ plus = (+) ; zero = 0 ; times = (*) ; one = 1
View
13 Satchmo/SMT/Exotic/Semiring/Rational.hs
@@ -0,0 +1,13 @@
+{-# language TypeSynonymInstances #-}
+{-# language FlexibleInstances #-}
+
+module Semiring.Rational where
+
+import Data.Ratio
+import Semiring.Class
+
+instance Semiring Rational where
+ strictness _ = Full
+ nonnegative x = x >= 0 ; strictly_positive x = x >= 1
+ ge = (>=) ; gt = (>)
+ plus = (+) ; zero = 0 ; times = (*) ; one = 1
View
28 Satchmo/SMT/Exotic/Semiring/Tropical.hs
@@ -0,0 +1,28 @@
+module Satchmo.SMT.Exotic.Semiring.Tropical where
+
+import Satchmo.SMT.Exotic.Semiring.Class
+
+data Tropical a = Finite a | Plus_Infinite deriving (Eq, Ord)
+
+instance Functor Tropical where
+ fmap f a = case a of
+ Finite x -> Finite $ f x
+ Plus_Infinite -> Plus_Infinite
+
+instance Show a => Show ( Tropical a ) where
+ show a = case a of
+ Plus_Infinite -> "+"
+ Finite x -> show x
+
+instance (Ord a, Num a) => Semiring (Tropical a) where
+ strictness _ = Half
+ nonnegative a = True -- ??
+ strictly_positive a = case a of Finite x -> x >= 0 ; _ -> False
+ ge = (>=)
+ gt x y = x == Plus_Infinite || (x > y)
+ plus = min
+ zero = Plus_Infinite
+ times x y = case (x,y) of
+ (Finite a, Finite b) -> Finite (a+b)
+ _ -> Plus_Infinite
+ one = Finite 0
View
113 Satchmo/SMT/Exotic/Solve.hs
@@ -0,0 +1,113 @@
+{-# language FlexibleInstances #-}
+{-# language UndecidableInstances #-}
+{-# language FlexibleContexts #-}
+{-# language MultiParamTypeClasses #-}
+{-# language PatternSignatures #-}
+
+module Exotic.Solve where
+
+import qualified Exotic.Check as C
+import Exotic.Dict
+
+import qualified Satchmo.Unary.Op.Flexible as X
+import qualified Satchmo.Unary as N
+
+-- import qualified Satchmo.Binary as N
+-- import qualified Satchmo.Binary.Op.Fixed as X
+
+import qualified Satchmo.Boolean as B
+import qualified Satchmo.SAT.Mini
+import Satchmo.SAT.Mini (SAT)
+import Satchmo.Code
+
+import Language.SMTLIB
+import qualified Data.Map as M
+import qualified Semiring as S
+
+
+import Control.Monad ( forM_, forM )
+import Control.Monad.State
+import System.IO
+import Control.Exception
+import Control.Concurrent.MVar
+import Control.Concurrent
+
+
+-- execute :: Int -> Script -> IO ( Maybe ( M.Map String ( F.Fuzzy Integer )))
+execute dict s = do
+ out <- execute0 dict s
+ -- print ( "Solve", out )
+ case out of { Just m -> C.execute m s ; Nothing -> return () }
+ -- print ( "Solve", out )
+ return out
+
+-- execute0 :: Int -> Script -> IO ( Maybe ( M.Map String ( F.Fuzzy Integer ) ))
+execute0 dict (Script cs) = do
+ out <- newEmptyMVar
+ pid <- forkIO $ do
+ result <- Satchmo.SAT.Mini.solve $ flip evalStateT M.empty $ do
+ forM_ cs $ command dict
+ m <- get
+ return $ decode m
+ putMVar out result
+ takeMVar out `Control.Exception.catch` \ (e::AsyncException) -> do
+ hPutStrLn stderr "caught Exception in execute0"
+ forkIO $ killThread pid
+ return Nothing
+
+-- command :: Dict d e -> Command -> SAT ()
+command dict c = case c of
+ Set_option ( Produce_models _ ) -> return ()
+ Set_option ( Produce_unsat_cores _ ) -> return ()
+ Set_logic l | l == logic dict -> return ()
+ Set_info _ -> return ()
+ Declare_fun f [] ( Sort_identifier ( Identifier s )) | s == show ( domain dict ) -> do
+ m <- get
+ a <- lift $ fresh dict
+ put $ M.insertWith ( error "Exotic.Solve.command: conflict" ) f a m
+ Define_fun f [] (Sort_identifier ( Identifier s) ) x | s == show ( domain dict ) -> do
+ a <- term dict x
+ m <- get
+ put $ M.insertWith ( error "Exotic.Solve.command: conflict" ) f a m
+ Assert f -> do
+ v <- formula dict f
+ lift $ B.assert [ v ]
+ Check_sat -> return ()
+ Get_unsat_core -> return ()
+ Get_value _ -> return ()
+ _ -> error $ "cannot handle command " ++ show c
+
+-- formula :: Dict d e -> Term -> SAT B.Boolean
+formula dict f = case f of
+ Term_attributes f [ Attribute_s_expr ":named" _ ] -> do
+ formula dict f
+ Term_qual_identifier (Qual_identifier (Identifier "true")) -> do
+ lift $ B.constant True
+ Term_qual_identifier (Qual_identifier (Identifier "false")) -> do
+ lift $ B.constant False
+ Term_qual_identifier_ ( Qual_identifier ( Identifier fun )) args ->
+ case fun of
+ "and" -> do xs <- forM args $ formula dict ; lift $ B.and xs
+ "or" -> do xs <- forM args $ formula dict ; lift $ B.or xs
+ ">=" -> do [l,r] <- forM args $ term dict ; lift $ ge dict l r
+ ">>" -> do [l,r] <- forM args $ term dict ; lift $ gg dict l r
+ "finite" -> do
+ [x] <- forM args $ term dict
+ lift $ finite dict x
+ _ -> error $ "Fuzzy.Solve.formula.1: " ++ show f
+ _ -> error $ "Fuzzy.Solve.formula.2: " ++ show f
+
+-- term :: Dict d e -> Term -> SAT e
+term dict t = case t of
+ Term_qual_identifier ( Qual_identifier ( Identifier fun )) -> do
+ m <- get
+ case M.lookup fun m of
+ Just x -> return x
+ _ -> error $ "Fuzzy.Solve.term: not bound: " ++ show t
+ Term_qual_identifier_ ( Qual_identifier ( Identifier fun )) args ->
+ case fun of
+ "+" -> do xs <- forM args $ term dict ; lift $ plus dict xs
+ "*" -> do xs <- forM args $ term dict ; lift $ times dict xs
+ _ -> error $ "Fuzzy.Solve.term.1: " ++ show t
+ _ -> error $ "Fuzzy.Solve.term.2: " ++ show t
+
View
153 Satchmo/SMT/Exotic/Transform.hs
@@ -0,0 +1,153 @@
+module Exotic.Transform where
+
+import Prelude hiding ( and, or )
+
+import Language.SMTLIB
+import SMT.Util
+
+import qualified Data.Map as M
+
+import Control.Monad.RWS
+import Control.Monad ( forM, forM_ )
+import Data.Functor ( (<$>) )
+
+import qualified Semiring as S
+
+import Data.Ratio
+
+(sort, logic) = ("Int" , "QF_IDL")
+
+
+transform :: Script
+ -> ( Script, M.Map Symbol Term -> M.Map Symbol (F.Fuzzy Integer))
+transform sc =
+ let ( a, s, w ) = runRWS ( script sc ) () 0
+ in ( Script w, a )
+
+script (Script cs) = do
+ forM_ cs command
+ let ks = do
+ Get_value vs <- cs
+ v <- vs
+ case v of
+ Term_qual_identifier ( Qual_identifier (Identifier k)) -> [k]
+ Term_qual_identifier_ ( Qual_identifier (Identifier k)) v -> [k]
+ _ -> []
+ return $ \ m -> M.fromList $ do
+ let pi = integer $ m M.! "plus_infinity"
+ mi = integer $ m M.! "minus_infinity"
+ k <- ks
+ return $ let v = integer $ m M.! k
+ in case ( compare mi v, compare v pi ) of
+ ( EQ, LT ) -> ( k, F.Minus_Infinite )
+ ( LT, LT ) -> ( k, F.Finite v )
+ ( LT, EQ ) -> ( k, F.Plus_Infinite )
+ e -> error $ " Fuzzy.Simplified_IDL.script: missing case " ++ show e
+
+
+
+newtype Fuzzy = Fuzzy { contents :: Term }
+
+-- contents = sym2term . contents_
+
+plus_infinite f = apply "=" [ plus_infinity, contents f ]
+minus_infinite f = apply "=" [ minus_infinity, contents f ]
+finite x = apply ">" [ plus_infinity, contents x ]
+plus_infinity = sym2term "plus_infinity"
+minus_infinity = sym2term "minus_infinity"
+
+command c = case c of
+ Set_option o -> case o of
+ Produce_models True -> tell [c]
+ Produce_unsat_cores True -> tell [c]
+
+ -- HACK: because sometimes parsing (lexing?) fails
+ Option_attribute (Attribute_s_expr ":produce-models" (S_expr_symbol "true")) ->
+ tell [ Set_option (Produce_models True) ]
+ Option_attribute (Attribute_s_expr ":produce-unsat-cores" (S_expr_symbol "true")) ->
+ tell [ Set_option (Produce_unsat_cores True) ]
+ _ -> error $ "Fuzzy.Simplified_IDL.command.set_option: " ++ show c
+ Set_logic "QF_Fuzzy" -> do
+ tell [ Set_logic logic ]
+ Set_info _ -> do
+ tell [c]
+ tell [ Declare_fun "plus_infinity" [] (Sort_identifier (Identifier sort))
+ , Declare_fun "minus_infinity" [] (Sort_identifier (Identifier sort))
+ , Assert $ apply "<" [ minus_infinity, plus_infinity ]
+ ]
+ Declare_fun f [] ( Sort_identifier ( Identifier "Fuzzy" )) -> do
+ tell [ Declare_fun f [] (Sort_identifier (Identifier sort))
+ , Assert $ apply "<=" [ minus_infinity, sym2term f ]
+ , Assert $ apply "<=" [ sym2term f, plus_infinity ]
+ ]
+ Define_fun f [] (Sort_identifier ( Identifier "Fuzzy") ) x -> do
+ a <- term x
+ tell [ Define_fun f []
+ (Sort_identifier (Identifier sort) ) ( contents a )
+ ]
+ Assert f -> do
+ v <- formula f
+ tell [ Assert v ]
+ Check_sat -> tell [ Check_sat ]
+ Get_value vs -> tell $ return $ Get_value $ [ plus_infinity, minus_infinity ] ++ do
+ Term_qual_identifier (Qual_identifier (Identifier f)) <- vs
+ return $ sym2term $ f
+ Get_unsat_core -> tell [ c ]
+ _ -> error $ "Fuzzy.Simplified_IDL.command: " ++ show c
+
+term :: Term -> RWS () [ Command ] Int Fuzzy
+term t = case t of
+ Term_qual_identifier ( Qual_identifier ( Identifier fun )) -> do
+ return $ Fuzzy t
+ Term_qual_identifier_ ( Qual_identifier ( Identifier fun )) args ->
+ case fun of
+ "+" -> do -- min, really
+ xs <- forM args term
+ y <- Fuzzy <$> declare sort
+ tell [ Assert $ and $ for xs $ \ x -> apply "<=" [contents y, contents x]
+ , Assert $ or $ for xs $ \ x -> apply "=" [ contents y, contents x]
+ ]
+ return $ y
+ "*" -> do -- max, really
+ xs <- forM args term
+ y <- Fuzzy <$> declare sort
+ tell [ Assert $ and $ for xs $ \ x -> apply ">=" [contents y, contents x]
+ , Assert $ or $ for xs $ \ x -> apply "=" [ contents y, contents x]
+ ]
+ return $ y
+ _ -> error $ "Fuzzy.Simplified_IDL.term.1: " ++ show t
+ _ -> error $ "Fuzzy.Simplified_IDL.term.2: " ++ show t
+
+formula f = case f of
+ Term_attributes g atts -> case atts of
+ [ Attribute_s_expr ":named" _ ] -> do
+ h <- formula g
+ return $ Term_attributes h atts
+ _ -> error $ "Fuzzy.Simplified_IDL.formula.3: " ++ show f
+ Term_qual_identifier (Qual_identifier (Identifier "true")) -> do
+ return f
+ Term_qual_identifier (Qual_identifier (Identifier "false")) -> do
+ return f
+ Term_qual_identifier_ ( Qual_identifier ( Identifier fun )) args ->
+ case fun of
+ "and" -> do xs <- forM args formula ; return $ and xs
+ "or" -> do xs <- forM args formula ; return $ or xs
+ ">=" -> do
+ [l,r] <- forM args term
+ return $ or
+ [ plus_infinite l
+ , apply ">" [ contents l, contents r ]
+ , minus_infinite r
+ ]
+ ">>" -> do
+ [l,r] <- forM args term
+ return $ or
+ [ plus_infinite l
+ , apply ">" [ contents l, contents r ]
+ ]
+ "finite" -> do
+ [x] <- forM args term
+ return $ finite x
+ _ -> error $ "Fuzzy.Simplified_IDL.formula.1: " ++ show f
+ _ -> error $ "Fuzzy.Simplified_IDL.formula.2: " ++ show f
+
View
78 Satchmo/SMT/Exotic/Tropical.hs
@@ -0,0 +1,78 @@
+-- | fixed bit width tropical numbers,
+-- table lookup for ring multiplication
+
+{-# language FlexibleInstances #-}
+{-# language FlexibleContexts #-}
+{-# language MultiParamTypeClasses #-}
+
+module Satchmo.SMT.Exotic.Tropical where
+
+import Satchmo.SMT.Exotic.Dict
+import Language.SMTLIB
+
+import qualified Data.Map as M
+
+-- see below (implementation of "times") for switching to Fixed
+-- import qualified Satchmo.Unary.Op.Flexible as X
+import qualified Satchmo.Unary.Op.Fixed as X
+import qualified Satchmo.Unary as N
+
+import qualified Satchmo.Boolean as B
+
+import Satchmo.Code
+import Satchmo.SAT.Mini (SAT)
+import Satchmo.SMT.Exotic.Util ( for )
+
+import Control.Monad ( foldM, forM, guard, when )
+
+import qualified Satchmo.SMT.Exotic.Semiring.Tropical as T
+
+
+data Tropical = Tropical { contents :: N.Number }
+
+plus_infinite = last . N.bits . contents
+
+instance ( Decode m B.Boolean Bool )
+ => Decode m Tropical ( T.Tropical Integer ) where
+ decode a = do
+ p <- decode $ plus_infinite a
+ c <- decode $ contents a
+ return $ if p then T.Plus_Infinite else T.Finite c
+
+make c = do
+ return $ Tropical { contents = c }
+
+dict :: Int
+ -> Dict SAT ( T.Tropical Integer ) Tropical B.Boolean
+dict bits = Dict { domain = Proof.Tropical
+ , fresh = do
+ c <- N.number bits
+ make c
+ , finite = \ x -> return $ B.not $ plus_infinite x
+ , ge = \ l r -> N.ge ( contents l ) ( contents r )
+ , gg = \ l r ->
+ B.monadic B.or [ return $ plus_infinite l
+ , N.gt ( contents l ) ( contents r )
+ ]
+ , plus = \ xs -> do
+ c <- X.minimum $ for xs contents
+ make c
+ , times = \ [s,t] -> do
+ p <- B.or [ plus_infinite s, plus_infinite t ]
+ let a = contents s ; b = contents t
+ let width = length $ N.bits a
+ when ( length ( N.bits b ) /= width )
+ $ error "Tropical.times: different bit widths"
+ t <- B.constant True
+ pairs <- sequence $ do
+ (i,x) <- zip [0 .. ] $ t : N.bits a
+ (j,y) <- zip [0 .. ] $ t : N.bits b
+ guard $ i+j > 0
+ guard $ i+j <= width
+ return $ do z <- B.and [x,y] ; return (i+j, [z])
+ cs <- forM ( map snd $ M.toAscList $ M.fromListWith (++) pairs ) B.or
+ -- if result is not plus_inf, then overflow is not allowed
+ B.assert [ p , B.not $ last cs ]
+ make $ N.make cs
+ }
+
View
64 Satchmo/SMT/Exotic/Util.hs
@@ -0,0 +1,64 @@
+module Satchmo.SMT.Exotic.Util where
+
+import Language.SMTLIB
+
+import Control.Monad.RWS hiding ( mplus )
+import Control.Monad.Trans
+
+import Data.Char ( toLower )
+
+type Sym a = RWS () [ Command ] Int a
+
+assert :: Term -> Sym ()
+assert f = case f of
+ Term_qual_identifier_ (Qual_identifier (Identifier "and")) args ->
+ void $ forM args assert
+ _ -> do
+ c <- get ; put $ succ c
+ let a = Attribute_s_expr ":named" $ S_expr_symbol $ "assert" ++ show c
+ tell [ Assert $ Term_attributes f [ a ] ]
+
+fresh :: String -> Sym Symbol
+fresh s = do
+ c <- get
+ put $ succ c
+ return $ s ++ show c
+
+declare :: String -> Sym Term
+declare sort = do
+ f <- fresh $ take 1 $ map toLower sort
+ tell [ Declare_fun f [] ( Sort_identifier ( Identifier sort )) ]
+ return $ Term_qual_identifier $ Qual_identifier $ Identifier f
+
+define :: String -> Term -> Sym Term
+define sort x = do
+ f <- fresh $ take 1 $ map toLower sort
+ tell [ Define_fun f [] ( Sort_identifier ( Identifier sort )) x ]
+ return $ Term_qual_identifier $ Qual_identifier $ Identifier f
+
+apply :: Symbol -> [Term ] -> Term
+apply fun args =
+ Term_qual_identifier_ ( Qual_identifier ( Identifier fun )) args
+
+and xs = case length xs of
+ 0 -> sym2term "true"
+ 1 -> head xs
+ _ -> apply "and" xs
+
+or xs = case length xs of
+ 0 -> sym2term "false"
+ 1 -> head xs
+ _ -> apply "or" xs
+
+for = flip map
+
+sym2term fun =
+ Term_qual_identifier ( Qual_identifier ( Identifier fun ))
+
+integer e = case e of
+ Term_spec_constant (Spec_constant_numeral i) ->
+ fromIntegral i
+ Term_qual_identifier_ (Qual_identifier (Identifier "-")) [ arg ] ->
+ negate $ integer arg
+ e -> error $ " Fuzzy.Simplified_IDL.script: missing case " ++ show e
+
View
160 Satchmo/SMT/Solve.hs
@@ -4,6 +4,7 @@
{-# language FlexibleContexts #-}
{-# language MultiParamTypeClasses #-}
{-# language ConstraintKinds #-}
+{-# language ExistentialQuantification #-}
module Satchmo.SMT.Solve where
@@ -11,14 +12,10 @@ import Prelude hiding ( and, or, not )
import qualified Prelude
import Satchmo.SMT.Config
+import Satchmo.SMT.Dictionary
+import Satchmo.SMT.ToTerm
-import qualified Satchmo.Unary.Op.Fixed
-import qualified Satchmo.Unary.Op.Flexible
-import qualified Satchmo.Unary as Un
-
-import qualified Satchmo.Binary as Bin
-import qualified Satchmo.Binary.Op.Fixed
-import qualified Satchmo.Binary.Op.Flexible
+import Satchmo.SAT.Mini (SAT)
import qualified Satchmo.Boolean as B
import qualified Satchmo.SAT.Mini
@@ -27,6 +24,11 @@ import Satchmo.Code
import Language.SMTLIB
import qualified Data.Map as M
+-- import qualified Satchmo.SMT.Exotic.Arctic as A
+-- import qualified Satchmo.SMT.Exotic.Tropical as T
+-- import qualified Satchmo.SMT.Exotic.Fuzzy as F
+import Satchmo.SMT.Integer
+
import Control.Monad ( forM_, forM )
import Control.Monad.Reader
import Control.Monad.Error
@@ -39,62 +41,21 @@ import Control.Concurrent.MVar
import Control.Concurrent
-data Value = Value_Integer Integer
+data Value n = Value_Number n
| Value_Bool Bool
-data Code n b = Code_Integer n
- | Code_Bool b
+data Code n = Code_Number n
+ | Code_Bool B.Boolean
+
-instance SolverC m n b
- => Decode m (Code n b) Value where
+instance (Decode m B.Boolean Bool, Decode m n v, Functor m)
+ => Decode m (Code n ) (Value v) where
decode c = case c of
- Code_Integer i -> Value_Integer <$> decode i
+ Code_Number i -> Value_Number <$> decode i
Code_Bool b -> Value_Bool <$> decode b
-data Dictionary m num bool = Dictionary
- { number :: m num
- , nconstant :: Integer -> m num
- , add :: num -> num -> m num
- , gt :: num -> num -> m bool
- , ge :: num -> num -> m bool
- , neq :: num -> num -> m bool
- , boolean :: m bool
- , bconstant :: Bool -> m bool
- , and :: [ bool ] -> m bool
- , or :: [ bool ] -> m bool
- , not :: bool -> bool
- , beq :: bool -> bool -> m bool
- , assert :: [ bool ] -> m ()
- }
-
-unary_fixed :: Int -> Dictionary Satchmo.SAT.Mini.SAT Un.Number B.Boolean
-unary_fixed bits = Dictionary
- { number = Un.number bits
- , nconstant = Un.constant
- , boolean = B.boolean
- , bconstant = B.constant
- , add = Satchmo.Unary.Op.Fixed.add
- , gt = Un.gt
- , ge = Un.ge
- , neq = Un.eq
- , and = B.and, or = B.or, not = B.not, beq = B.equals2, assert = B.assert
- }
-
-binary_fixed :: Int -> Dictionary Satchmo.SAT.Mini.SAT Bin.Number B.Boolean
-binary_fixed bits = Dictionary
- { number = Bin.number bits
- , nconstant = Bin.constant
- , boolean = B.boolean
- , bconstant = B.constant
- , add = Satchmo.Binary.Op.Fixed.add
- , gt = Bin.gt
- , ge = Bin.ge
- , neq = Bin.eq
- , and = B.and, or = B.or, not = B.not, beq = B.equals2, assert = B.assert
- }
-
-execute :: Config -> Script -> IO ( Maybe ( M.Map String Value ))
+-- execute :: Config -> Script -> IO ( Maybe ( M.Map String Value ))
execute conf s = do
out <- execute0 conf s
-- print ( "Solve", out )
@@ -102,7 +63,7 @@ execute conf s = do
-- print ( "Solve", out )
return out
-execute0 :: Config -> Script -> IO ( Maybe ( M.Map String Value ))
+-- execute0 :: Config -> Script -> IO ( Maybe ( M.Map String Value ))
execute0 conf s = do
out <- newEmptyMVar
pid <- forkIO $ do
@@ -113,33 +74,50 @@ execute0 conf s = do
forkIO $ killThread pid
return Nothing
+data D = forall n . Decode SAT n Integer => D (Dictionary SAT n Integer)
+solve_script conf s = do
+ let b = bits conf ; a = unary_addition conf
+ dict = case (encoding conf, extension conf) of
+ (Unary, Fixed) -> D $ unary_fixed b a
+ (Unary, Flexible) -> D $ unary_flexible b a
+ (Binary, Fixed) -> D $ binary_fixed b
+ (Binary, Flexible) -> D $ binary_flexible b
+ case dict of
+ D d -> do
+ hPutStrLn stderr $ info d
+ Satchmo.SAT.Mini.solve $ evalStateT (script d s) M.empty
-solve_script conf s = Satchmo.SAT.Mini.solve $
- case encoding conf of
- Unary { bits = b } ->
- evalStateT (script (unary_fixed b) s)
- ( M.empty :: M.Map Symbol ( Code Un.Number B.Boolean ))
- Binary { bits = b } ->
- evalStateT (script (binary_fixed b) s)
- ( M.empty :: M.Map Symbol ( Code Bin.Number B.Boolean ))
-
+type Solver m n = StateT (M.Map Symbol ( Code n )) m
+type SolverC m n v =
+ ( Functor m, Monad m, Decode m n v, Decode m B.Boolean Bool, ToTerm v )
-type Solver m n b = StateT (M.Map Symbol ( Code n b )) m
-type SolverC m n b =
- ( Functor m, Monad m, Decode m n Integer, Decode m b Bool )
-
-script :: SolverC m n b
- => Dictionary m n b -> Script -> Solver m n b (m (M.Map Symbol Value))
-script dict (Script cs) = do
+script :: ( SolverC m n v )
+ => Dictionary m n v -> Script -> Solver m n (m [( Term, Term)] )
+script (dict :: Dictionary m n v) (Script cs) = do
forM_ cs $ command dict
m <- get
- return $ decode m
+ return $ do
+ m <- decode m
+ return $ do (k , v ) <- M.toList m
+ return ( sym2term k , case v of
+ Value_Number (n :: v) -> toTerm n
+ Value_Bool b -> bool2term b
+ )
+
+sym2term fun =
+ Term_qual_identifier ( Qual_identifier ( Identifier fun ))
+
+
+bool2term b =
+ Term_qual_identifier $ Qual_identifier $ Identifier $ case b of
+ False -> "false" ; True -> "true"
+
-command :: SolverC m n b
- => Dictionary m n b -> Command -> Solver m n b ()
+command :: SolverC m n v
+ => Dictionary m n v -> Command -> Solver m n ()
command dict c = case c of
Set_option ( Produce_models True ) -> return ()
@@ -156,7 +134,7 @@ command dict c = case c of
m <- get
a <- lift $ number dict
put $ M.insertWith ( error "LIA.Satchmo.command: conflict" )
- f ( Code_Integer a ) m
+ f ( Code_Number a ) m
Declare_fun f [] ( Sort_bool ) -> do
m <- get
@@ -165,10 +143,10 @@ command dict c = case c of
f ( Code_Bool a ) m
Define_fun f [] (Sort_identifier ( Identifier s) ) x | s `elem` [ "Int", "Real" ] -> do
- Code_Integer a <- term dict x
+ Code_Number a <- term dict x
m <- get
put $ M.insertWith ( error "LIA.Satchmo.command: conflict" )
- f (Code_Integer a) m
+ f (Code_Number a) m
Define_fun f [] ( Sort_bool ) x -> do
Code_Bool a <- term dict x
@@ -187,14 +165,14 @@ command dict c = case c of
_ -> error $ "cannot handle command " ++ show c
-term :: SolverC m n b
- => Dictionary m n b -> Term -> Solver m n b ( Code n b )
+term :: SolverC m n v
+ => Dictionary m n v -> Term -> Solver m n ( Code n )
term dict f = case f of
Term_attributes f [ Attribute_s_expr ":named" _ ] -> do
term dict f
Term_spec_constant ( Spec_constant_numeral n ) -> do
c <- lift $ nconstant dict n
- return $ Code_Integer c
+ return $ Code_Number c
Term_qual_identifier ( Qual_identifier ( Identifier "true" )) -> do
b <- lift $ bconstant dict True
return $ Code_Bool b
@@ -225,30 +203,30 @@ term dict f = case f of
"or" -> do xs <- forM args $ term dict
fmap Code_Bool $ lift $ or dict $ map unbool xs
- ">=" -> do [Code_Integer l, Code_Integer r] <- forM args $ term dict
+ ">=" -> do [Code_Number l, Code_Number r] <- forM args $ term dict
fmap Code_Bool $ lift $ ge dict l r
- "<=" -> do [Code_Integer l, Code_Integer r] <- forM args $ term dict
+ "<=" -> do [Code_Number l, Code_Number r] <- forM args $ term dict
fmap Code_Bool $ lift $ ge dict r l
- ">" -> do [Code_Integer l, Code_Integer r] <- forM args $ term dict
+ ">" -> do [Code_Number l, Code_Number r] <- forM args $ term dict
fmap Code_Bool $ lift $ gt dict l r
- "<" -> do [Code_Integer l, Code_Integer r] <- forM args $ term dict
+ "<" -> do [Code_Number l, Code_Number r] <- forM args $ term dict
fmap Code_Bool $ lift $ gt dict r l
"=" -> do
[l,r] <- forM args $ term dict
fmap Code_Bool $ lift $ case (l,r) of
- (Code_Integer a, Code_Integer b) -> neq dict a b
+ (Code_Number a, Code_Number b) -> neq dict a b
(Code_Bool a, Code_Bool b) -> beq dict a b
"+" -> do xs <- forM args $ term dict
- fmap Code_Integer $ lift $ plus dict $ map unint xs
+ fmap Code_Number $ lift $ plus dict $ map unint xs
"-" -> do xs <- forM args $ term dict
- fmap Code_Integer $ lift $ minus dict $ map unint xs
+ fmap Code_Number $ lift $ minus dict $ map unint xs
"*" -> do let [ num , arg ] = args
val <- term dict arg
- fmap Code_Integer $ lift
+ fmap Code_Number $ lift
$ mul_by_const dict (integer num) $ unint val
_ -> error $ "Satchmo.SMT.Solve.term.1: " ++ show f
@@ -256,7 +234,7 @@ term dict f = case f of
unbool (Code_Bool b) = b
-unint ( Code_Integer i ) = i
+unint ( Code_Number i ) = i
integer t = case t of
Term_spec_constant ( Spec_constant_numeral n ) -> n

No commit comments for this range

Something went wrong with that request. Please try again.