Skip to content
Browse files

rework (start to include exotic domains)

  • Loading branch information...
1 parent 1024395 commit 25d8425362741820288786c1616759f61296a3f5 @jwaldmann committed Apr 23, 2012
Showing with 62 additions and 107 deletions.
  1. +4 −19 Main.hs
  2. +58 −88 Satchmo/SMT/Solve.hs
View
23 Main.hs
@@ -6,13 +6,15 @@
-- 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.
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
146 Satchmo/SMT/Solve.hs
@@ -11,14 +11,8 @@ import Prelude hiding ( and, or, not )
import qualified Prelude
import Satchmo.SMT.Config
-
-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.SMT.Dictionary
+import Satchmo.SMT.ToTerm
import qualified Satchmo.Boolean as B
import qualified Satchmo.SAT.Mini
@@ -27,6 +21,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,70 +38,29 @@ 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 )
-- case out of { Just m -> C.execute m s ; Nothing -> return () }
-- 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
@@ -117,29 +75,41 @@ execute0 conf s = do
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 ))
+ Unary { bits = b } -> evalStateT (script (unary_fixed b) s) ( M.empty )
+ Binary { bits = b } -> evalStateT (script (binary_fixed b) s) ( M.empty )
-type Solver m n b = StateT (M.Map Symbol ( Code n b )) m
+type Solver m n = StateT (M.Map Symbol ( Code n )) m
-type SolverC m n b =
- ( Functor m, Monad m, Decode m n Integer, Decode m b Bool )
+type SolverC m n v =
+ ( Functor m, Monad m, Decode m n v, Decode m B.Boolean Bool, ToTerm v )
-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 +126,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 +135,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,12 +157,12 @@ 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_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
@@ -223,38 +193,38 @@ 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
_ -> error $ "Satchmo.SMT.Solve.term.2: " ++ show f
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

0 comments on commit 25d8425

Please sign in to comment.
Something went wrong with that request. Please try again.