Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Sat example.

  • Loading branch information...
commit 222f2451a11af3703dc8e2520833c8905e4b236f 1 parent f9f8a28
@leepike authored
Showing with 10 additions and 2 deletions.
  1. +10 −2 Examples/Sat.hs
View
12 Examples/Sat.hs
@@ -1,6 +1,8 @@
-- | Example of a simple SAT solver (simply constructs the truth table) in
-- Copilot.
+-- {-# LANGUAGE RebindableSyntax #-}
+
module Languages where
import Language.Copilot
@@ -24,7 +26,6 @@ sat (i,f) = (xs, res)
xs' 0 = []
xs' n = clk (period $ 2 P.^ n) (phase (0 :: Int)) : xs' (n P.- 1)
-
satSpec :: SatFunc -> Spec
satSpec f = do
observer "sat" (snd $ sat f)
@@ -40,9 +41,16 @@ satSpec f = do
mkObs idx strm = do observer ("obs" P.++ show idx) strm
return (idx P.+ 1)
-
-- Example SAT function.
f0 :: SatFunc
f0 = (3, \[a,b,c] -> a && (b || (not c)))
+f1 :: SatFunc
+f1 = (9, \[a,b,c,d,e,f,g,h,i] -> a && b && c && d && e &&
+ f && g && h && i && i && not i)
+
+-- | Run the interpreter long enough to get an answer.
+runFunc :: SatFunc -> IO ()
+runFunc f = interpret (2 P.^ fst f) (satSpec f)
+
---------------------------------------------------------------------------------
Please sign in to comment.
Something went wrong with that request. Please try again.