Commit f5132895 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

heuristics for entailment without SMT

parent 0bc972dc
def qn ():
var l1, l2, n, i, tick_z
var l1, l2, n, i
l1 = 0
l2 = 0
i = 0
......@@ -21,6 +21,6 @@ def qn ():
l2 = l2 + 1
if l1 >= l2:
tick_z = l1 + tick_z
tick l1
else:
tick_z = l2 + tick_z
tick l2
def qn ():
var l1, l2, n
l1 = 0
l2 = 0
while [l1 >= 0 and l2 >= 0] n>0:
n = n - 1
if l1 > 0:
l1 = l1 - 1
if l2 > 0:
l2 = l2 - 1
prob (49,1):
skip
else:
prob(1,4):
l1 = l1 + 3
else:
prob(1,1):
l2 = l2 + 2
else:
l1 = l1 + 2
l2 = l2 + 1
nondet:
tick l1
else:
tick l2
def seq ():
var n, x
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
......@@ -403,7 +403,7 @@ et t (While _ i b c) f =
g <- case t of {Evt -> return C.zero; Ect -> ect c C.zero}
ns <- extractRanking c i b g f
logMsg2 "Norms" ns
hs <- traverse (evt c . C.fromNorm) ns
hs <- traverse (et Evt c . C.fromNorm) ns
let ui = UpperInvariant { inv = i
, cnd = b
, cost = g
......
......@@ -197,14 +197,6 @@ decode = C.traverseCoeff decodeCoeff where
encode :: CExp -> AExp
encode = C.mapCoeff acoeff
-- implication elimination
----------------------------------------------------------------------
handelman :: Int -> Conj SmtLit -> SmtLit -> SmtM SmtFormula
handelman deg = eqCoefficientsWith $
\premise -> SMT.sumA <$> mapM withWeight [SMT.prod ms | ms <- replicateM deg (SMT.one : premise)]
-- invariant solver
----------------------------------------------------------------------
......@@ -241,27 +233,35 @@ type Context = DNF SmtLit
data Constraint e = GEQ Context e e
deriving (Functor)
handelman :: Int -> Conj SmtLit -> SmtLit -> SmtM SmtFormula
handelman deg = eqCoefficientsWith $
\premise -> SMT.sumA <$> mapM withWeight [SMT.prod ms | ms <- replicateM deg (SMT.one : premise)]
assertEntailSmt :: Int -> DNF SmtLit -> SmtLit -> SmtM ()
assertEntailSmt i (Disj cs) p = forM_ cs $ \c -> SMT.assert =<< handelman i c p
-- assertEntailSmt i ctx@(Disj cs) p = forM_ (conjs (d ctx)) $ \c -> SMT.assert =<< handelman i c p
-- where d cs = debug (show (PP.pretty cs PP.<> PP.text "|-" PP.<> PP.pretty p)) cs
-- assertEntailSmt i (Disj cs) p = forM_ cs $ \c -> SMT.assert =<< handelman i c p
assertEntailSmt i ctx@(Disj cs) p = forM_ cs entailConj
where
entailConj c
| p `S.member` litsSet c = return ()
| otherwise = SMT.assert =<< handelman i c p
-- d p = debug (show (PP.pretty ctx PP.<> PP.text " |- " PP.<> PP.pretty p)) p
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 =
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
-- elimination of cost expression
----------------------------------------------------------------------
......
......@@ -2,9 +2,9 @@ flags: {}
packages:
- '.'
extra-deps:
# - '../../../../dev/gubs'
# - /home/mavanzin/sources/gubs
- git: https://github.com/ComputationWithBoundedResources/gubs
commit: a2072f60ed7b8f0d3c05c8d4c90e5f1d661318f8
commit: bf9283d51c754df487ddf7d8a7fbc6b34664a259
- git: https://github.com/mzini/monad-trace
commit: 64ac8dc558e62b82711148f0570b6f12c3b14f0a
- megaparsec-8.0.0
......
Markdown is supported
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