Commit 9faed3ec authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

added ec function and simple examples

parent b2b6e982
......@@ -33,7 +33,7 @@ type SmtFormula = SMT.SMTFormula SMT.SMTLib2
type SmtExpression = SMT.SMTExpression SMT.SMTLib2
runSmtM :: SmtM a -> a
-- runSmtM = SMT.runSMTLib2 "z3" ["-smt2", "-in"]
-- runSmtM = unsafePerformIO . SMT.runSMTLib2 "z3" ["-smt2", "-in"]
runSmtM = unsafePerformIO . SMT.runSMTLib2Using "QF_LIRA" "yices-smt2" ["--incremental"]
-- runSmtM = unsafePerformIO . SMT.runSMTLib2 "yices-smt2" []
......
......@@ -4,12 +4,43 @@ module PWhile.Testbed.Examples where
import Prelude
import Data.String
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Data.PWhile.Program (C(..))
import qualified Data.PWhile.CostExpression as C
import PWhile.InferEt
import PWhile.Testbed.DSL
import PWhile.Util
prettyResult :: PP.Pretty a => a -> PP.Doc
prettyResult r = PP.text "***" PP.<$$> PP.pretty r PP.<$$> PP.text "<<<"
run_ :: FilterResult -> (C -> SolveM a) -> Program -> IO [Result a]
run_ t m = run t . m . fst . gen
ec :: FilterResult -> Program -> IO ()
ec t p = run_ t (flip ect C.zero) p >>= mapM_ (putPrettyLn . prettyResult)
ifThenElse :: BExp -> Program -> Program -> Program
ifThenElse = ite top
succ1 :: Program
succ1 = do
[x,n] <- vars ["x","N"]
while' (x .< n) $ do
tick
x .= x + 1
rdwalk :: Program
rdwalk = do
[x,n,z] <- vars ["x","N","z"]
while' (x .< n) $ do
-- while' (x + 2 .<= n) $ do
choice [ (1, x .= x + 2)
, (1, x .= x - 1) ]
tick
-- Absynth Examples
----------------------------------------------------------------------
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment