Permalink
Browse files

allow LET bindings (ansatzweise)

  • Loading branch information...
1 parent 752082e commit 8f456110798b186427f8e4c4b4825e433088c4ad @jwaldmann committed Apr 15, 2012
Showing with 10 additions and 3 deletions.
  1. +0 −3 Main.hs
  2. +10 −0 Satchmo/SMT/Solve.hs
View
@@ -10,9 +10,6 @@
-- Assumption: input contains exactly one (check-sat)
-- followed by (get-value) for all global names.
--- Assumption: input does not contain local bindings (LET)
-
-
import Satchmo.SMT.Config
import Satchmo.SMT.Solve
View
@@ -201,6 +201,16 @@ term dict f = case f of
return $ case M.lookup fun m of
Just v -> v
Nothing -> error $ "Satchmo.SMT.Solve: " ++ show fun
+ Term_let bindings body -> do
+ svs <- forM bindings $ \ (Var_binding s t) -> do
+ v <- term dict t
+ return ( s, v )
+ m <- get
+ put $ M.union (M.fromList svs) m
+ v <- term dict body
+ put m -- restore original environment
+ return v
+
Term_qual_identifier_ ( Qual_identifier ( Identifier fun )) args ->
case fun of
"not" -> do [Code_Bool x] <- forM args $ term dict

0 comments on commit 8f45611

Please sign in to comment.