From be634c3e74b4294f11556e8617b2b9c841847d97 Mon Sep 17 00:00:00 2001 From: K9-guardian Date: Mon, 15 Jan 2024 21:09:51 -0800 Subject: [PATCH 1/3] Use calculateCuts in elim to ignore cyclic constraints instead of crashing --- src/Language/Fixpoint/Horn/Solve.hs | 2 +- src/Language/Fixpoint/Horn/Transformations.hs | 19 ++++++++++++------- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/src/Language/Fixpoint/Horn/Solve.hs b/src/Language/Fixpoint/Horn/Solve.hs index e5c213634..13b6f459e 100644 --- a/src/Language/Fixpoint/Horn/Solve.hs +++ b/src/Language/Fixpoint/Horn/Solve.hs @@ -88,7 +88,7 @@ eliminate cfg q | F.eliminate cfg == F.Existentials = do Tx.solveEbs cfg q | F.eliminate cfg == F.Horn = do - let c = Tx.elim $ H.qCstr q + let c = Tx.elim cfg q whenLoud $ putStrLn "Horn Elim:" whenLoud $ putStrLn $ F.showpp c pure $ q { H.qCstr = c } diff --git a/src/Language/Fixpoint/Horn/Transformations.hs b/src/Language/Fixpoint/Horn/Transformations.hs index 40fe3d758..09453e423 100644 --- a/src/Language/Fixpoint/Horn/Transformations.hs +++ b/src/Language/Fixpoint/Horn/Transformations.hs @@ -773,19 +773,24 @@ substPred su (Var k xs) = Var k $ upd <$> xs where upd x = M.lookupDefault x x su ------------------------------------------------------------------------------ --- | elim solves all of the KVars in a Cstr (assuming no cycles...) --- >>> elim . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test00.smt2" +-- | elim solves all of the KVars in a Cstr +-- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/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 "tests/horn/pos/test01.smt2" +-- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/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 "tests/horn/pos/test02.smt2" +-- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/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))))))))) +-- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/test03.smt2" +-- (and (and (forall ((x int) (x > 0)) (forall ((v int) (v == x)) (($k0 v)))) (forall ((y int) ($k0 y)) (forall ((v int) (v == y + 1)) (($k0 v)))) (forall ((z int) ($k0 z)) ((z > 0))))) ------------------------------------------------------------------------------ -elim :: Cstr a -> Cstr a +elim :: (F.PPrint a) => F.Config -> Query a -> Cstr a ------------------------------------------------------------------------------ -elim c = if S.null $ boundKvars res then res else error "called elim on cyclic constraint" +elim cfg query = S.foldl' elim1 c acyclicKs where - res = S.foldl' elim1 c (boundKvars c) + c = qCstr query + kvars = boundKvars c + cuts = calculateCuts cfg query c + acyclicKs = kvars `S.difference` cuts elim1 :: Cstr a -> F.Symbol -> Cstr a -- Find a `sol1` solution to a kvar `k`, and then subsitute in the solution for From bc9edd4d7cc3c0936a907188aa2e43d0009d4846 Mon Sep 17 00:00:00 2001 From: K9-guardian Date: Mon, 29 Jan 2024 17:13:29 -0800 Subject: [PATCH 2/3] add testcase with both cyclic and acyclic constraint --- src/Language/Fixpoint/Horn/Transformations.hs | 2 ++ tests/horn/pos/test04.smt2 | 20 +++++++++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 tests/horn/pos/test04.smt2 diff --git a/src/Language/Fixpoint/Horn/Transformations.hs b/src/Language/Fixpoint/Horn/Transformations.hs index 09453e423..88d5d449f 100644 --- a/src/Language/Fixpoint/Horn/Transformations.hs +++ b/src/Language/Fixpoint/Horn/Transformations.hs @@ -782,6 +782,8 @@ substPred su (Var k xs) = Var k $ upd <$> xs -- (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))))))))) -- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/test03.smt2" -- (and (and (forall ((x int) (x > 0)) (forall ((v int) (v == x)) (($k0 v)))) (forall ((y int) ($k0 y)) (forall ((v int) (v == y + 1)) (($k0 v)))) (forall ((z int) ($k0 z)) ((z > 0))))) +-- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/test04.smt2" +-- (and (forall ((x int) (x > 0)) (forall ((v int) (v == x)) (($k0 v)))) (forall ((y int) ($k0 y)) (forall ((yyy int) (true)) (forall ((vvv int) (vvv == yyy + 1)) (forall ((v int) (and (v == vvv) (y == yyy))) (($k0 v)))))) (forall ((z int) ($k0 z)) ((z > 0)))) ------------------------------------------------------------------------------ elim :: (F.PPrint a) => F.Config -> Query a -> Cstr a ------------------------------------------------------------------------------ diff --git a/tests/horn/pos/test04.smt2 b/tests/horn/pos/test04.smt2 new file mode 100644 index 000000000..979f5a36f --- /dev/null +++ b/tests/horn/pos/test04.smt2 @@ -0,0 +1,20 @@ +// TODO move to actual SMTLIB format + +(var $k0 ((Int))) +(var $k1 ((int) (int))) + +(qualif Foo ((v Int)) ((v > 0))) + +(constraint + (and + (forall ((yyy Int) (true)) + (forall ((vvv Int) (vvv = yyy + 1)) + (($k1 vvv yyy)))) + (forall ((x Int) (x > 0)) + (forall ((v Int) (v = x)) + (($k0 v)))) + (forall ((y Int) ($k0 y)) + (forall ((v Int) ($k1 v y)) + (($k0 v)))) + (forall ((z Int) ($k0 z)) + ((z > 0))))) From 704bad1afeca6c337e7e3e1e848acb1e00998e6e Mon Sep 17 00:00:00 2001 From: K9-guardian Date: Mon, 25 Mar 2024 12:30:06 -0700 Subject: [PATCH 3/3] Fix acyclicEliminate to support new smt format --- src/Language/Fixpoint/Horn/Transformations.hs | 12 ++++---- tests/horn/pos/test04.smt2 | 28 +++++++++---------- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/Language/Fixpoint/Horn/Transformations.hs b/src/Language/Fixpoint/Horn/Transformations.hs index 88d5d449f..f430eb4fd 100644 --- a/src/Language/Fixpoint/Horn/Transformations.hs +++ b/src/Language/Fixpoint/Horn/Transformations.hs @@ -774,18 +774,18 @@ substPred su (Var k xs) = Var k $ upd <$> xs ------------------------------------------------------------------------------ -- | elim solves all of the KVars in a Cstr --- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/test00.smt2" +-- >>> elim defConfig <$> Language.Fixpoint.Horn.SMTParse.parseFromFile hornP "tests/horn/pos/test00.smt2" -- (and (forall ((x int) (x > 0)) (forall ((y int) (y > x)) (forall ((v int) (v == x + y)) ((v > 0)))))) --- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/test01.smt2" +-- >>> elim defConfig <$> parseFromFile Language.Fixpoint.Horn.SMTParse.hornP "tests/horn/pos/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 defConfig . fst <$> parseFromFile hornP "tests/horn/pos/test02.smt2" +-- >>> elim defConfig <$> parseFromFile Language.Fixpoint.Horn.SMTParse.hornP "tests/horn/pos/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))))))))) --- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/test03.smt2" +-- >>> elim defConfig <$> parseFromFile Language.Fixpoint.Horn.SMTParse.hornP "tests/horn/pos/test03.smt2" -- (and (and (forall ((x int) (x > 0)) (forall ((v int) (v == x)) (($k0 v)))) (forall ((y int) ($k0 y)) (forall ((v int) (v == y + 1)) (($k0 v)))) (forall ((z int) ($k0 z)) ((z > 0))))) --- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/test04.smt2" +-- >>> elim defConfig <$> parseFromFile Language.Fixpoint.Horn.SMTParse.hornP "tests/horn/pos/test04.smt2" -- (and (forall ((x int) (x > 0)) (forall ((v int) (v == x)) (($k0 v)))) (forall ((y int) ($k0 y)) (forall ((yyy int) (true)) (forall ((vvv int) (vvv == yyy + 1)) (forall ((v int) (and (v == vvv) (y == yyy))) (($k0 v)))))) (forall ((z int) ($k0 z)) ((z > 0)))) ------------------------------------------------------------------------------ -elim :: (F.PPrint a) => F.Config -> Query a -> Cstr a +elim :: (F.Fixpoint a, F.PPrint a) => F.Config -> Query a -> Cstr a ------------------------------------------------------------------------------ elim cfg query = S.foldl' elim1 c acyclicKs where diff --git a/tests/horn/pos/test04.smt2 b/tests/horn/pos/test04.smt2 index 979f5a36f..454e54280 100644 --- a/tests/horn/pos/test04.smt2 +++ b/tests/horn/pos/test04.smt2 @@ -1,20 +1,20 @@ -// TODO move to actual SMTLIB format +(fixpoint "--eliminate=horn") -(var $k0 ((Int))) -(var $k1 ((int) (int))) +(qualif Foo ((v Int)) (> v 0)) -(qualif Foo ((v Int)) ((v > 0))) +(var $k0 ((Int))) +(var $k1 ((Int) (Int))) -(constraint - (and +(constraint + (and (forall ((yyy Int) (true)) - (forall ((vvv Int) (vvv = yyy + 1)) - (($k1 vvv yyy)))) - (forall ((x Int) (x > 0)) - (forall ((v Int) (v = x)) - (($k0 v)))) + (forall ((vvv Int) ((= vvv (+ yyy 1)))) + ($k1 vvv yyy))) + (forall ((x Int) ((> x 0))) + (forall ((v Int) ((= v x))) + ($k0 v))) (forall ((y Int) ($k0 y)) - (forall ((v Int) ($k1 v y)) - (($k0 v)))) + (forall ((v Int) ($k1 v y)) + ($k0 v))) (forall ((z Int) ($k0 z)) - ((z > 0))))) + ((> z 0)))))