Language.Fixpoint.Horn.Transformations

Documentation

uniq :: Cstr a -> Cstr a

flatten :: Flatten a => a -> a

elim :: Cstr a -> Cstr a

elim solves all of the KVars in a Cstr (assuming no cycles...) >>> elim . qCstr . fst $ parseFromFile hornP "testshornpos/test00.smt2" (and (forall ((x int) (x > 0)) (forall ((y int) (y > x)) (forall ((v int) (v == x + y)) ((v > 0)))))) >>> elim . qCstr . fst $ parseFromFile hornP "testshornpos/test01.smt2" (and (forall ((x int) (x > 0)) (and (forall ((y int) (y > x)) (forall ((v int) (v == x + y)) ((v > 0)))) (forall ((z int) (z > 100)) (forall ((v int) (v == x + z)) ((v > 100))))))) >>> elim . qCstr . fst $ parseFromFile hornP "testshornpos/test02.smt2" (and (forall ((x int) (x > 0)) (and (forall ((y int) (y > x + 100)) (forall ((v int) (v == x + y)) ((true)))) (forall ((y int) (y > x + 100)) (forall ((v int) (v == x + y)) (forall ((z int) (z == v)) (forall ((v int) (v == x + z)) ((v > 100)))))))))

elimPis :: [Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)

>>> (q, opts) <- parseFromFile hornP "tests/horn/pos/ebind01.smt2"
>>> let (Just noside, Just side) = split $ pokec $ qCstr q
>>> F.pprint $ elimPis ["x1"] (noside, side )
(forall ((m int) (true))
 (forall ((x1 int) (forall [v : int]
  . v == m + 1 => v == x1
&& forall [v : int]
     . v == x1 + 1 => v == 2 + m))
  (and
   (forall ((v int) (v == m + 1))
    (((v == x1))))
   (forall ((v int) (v == x1 + 1))
    (((v == 2 + m))))))) : (forall ((m int) (true))
                            (exists ((x1 int) (true))
                             ((forall [v : int]
                                 . v == m + 1 => v == x1
                               && forall [v : int]
                                    . v == x1 + 1 => v == 2 + m))))

>>> (q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2"
>>> let (Just noside, Just side) = split $ pokec $ qCstr q
>>> F.pprint $ elimPis ["x1"] (noside, side )
(forall ((m int) (true))
 (forall ((z int) (z == m - 1))
  (and
   (forall ((v1 int) (v1 == z + 2))
    ((k v1)))
   (forall ((x1 int) (forall [v2 : int]
  . $k[fix$36$$954$arg$36$k$35$1:=v2] => v2 == x1
&& forall [v3 : int]
     . v3 == x1 + 1 => v3 == m + 2))
    (and
     (forall ((v2 int) (k v2))
      (((v2 == x1))))
     (forall ((v3 int) (v3 == x1 + 1))
      (((v3 == m + 2))))))))) : (forall ((m int) (true))
                                 (forall ((z int) (z == m - 1))
                                  (exists ((x1 int) (true))
                                   ((forall [v2 : int]
                                       . $k[fix$36$$954$arg$36$k$35$1:=v2] => v2 == x1
                                     && forall [v3 : int]
                                          . v3 == x1 + 1 => v3 == m + 2)))))

solveEbs :: PPrint a => Config -> Query a -> IO (Query a)

solveEbs takes a query and returns a query with the ebinds solved out

it has some preconditions - pi -> k -> pi structure. That is, there are no cycles, and while ks can depend on other ks, pis cannot directly depend on other pis - predicate for exists binder is true. (TODO: is this pre stale?)

cstrToExpr :: Cstr a -> Expr

Orphan instances

Visitable Pred

Methods

visit :: Monoid a => Visitor a c -> c -> Pred -> VisitM a Pred

Visitable (Cstr a)

Methods

visit :: Monoid a0 => Visitor a0 c -> c -> Cstr a -> VisitM a0 (Cstr a)