Commit 1192d014 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

toFrac recurse in frac

parent 19796374
......@@ -251,19 +251,18 @@ assertConstraintSmt :: Int -> Constraint SmtPoly -> SmtM ()
assertConstraintSmt i (GEQ g l r) = assertEntailSmt i g (l `geqLit` r)
entailsSmtK :: PP.Pretty a => Int -> DNF SmtLit -> DNF SmtLit -> (Bool -> SmtM a) -> SmtM a
entailsSmtK i p c k = k False
-- anySatM (conjs c) where
-- anySatM [] = k False
-- anySatM (cs:css) = do
-- SMT.push
-- s <- allSatM (lits cs)
-- if s then k True <* SMT.pop else SMT.pop >> anySatM css
-- allSatM [] = return True
-- allSatM ls = forM ls (ent p) *> SMT.checkSat
entailsSmtK i p c k =
anySatM (conjs c) where
anySatM [] = k False
anySatM (cs:css) = do
SMT.push
s <- allSatM (lits cs)
if s then k True <* SMT.pop else SMT.pop >> anySatM css
allSatM [] = return True
allSatM ls = forM ls (ent p) *> SMT.checkSat
-- TODO: add syntactic checks and possibly assert
-- ent = assertEntailSmt i
ent = assertEntailSmt i
applyTemplate :: (Num c, Eq c) => [c] -> [C.CExp c] -> C.CExp c
......@@ -276,7 +275,8 @@ applyTemplate qs = C.sum . zipWith C.scale (E.constant `map` qs)
-- toFrac :: AExp -> (AExp, Exp)
toFrac :: (Eq c, Num c) => C.CExp c -> (C.CExp c, E.Expression c)
toFrac c@C.E{} = (c,1)
toFrac (C.Div c e) = (c,e)
toFrac (C.Div c e) = (d,e*f) where
(d,f) = toFrac c
toFrac (C.Sup c1 c2) = (C.scale f2 d1 `C.sup` C.scale f1 d2, f1 * f2 * f) where
(d1,e1) = toFrac c1
(d2,e2) = toFrac c2
......
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