Question about a fixpoint example

[meditans]

Hi, I'm trying to translate this example in z3's documentation using the api provided by this package. The closest thing I can get is:

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, DefaultSignatures          #-}
{-# LANGUAGE DeriveAnyClass, DeriveGeneric, FlexibleContexts            #-}
{-# LANGUAGE FlexibleInstances, FunctionalDependencies, GADTs           #-}
{-# LANGUAGE KindSignatures, MultiParamTypeClasses, ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications, TypeFamilies, TypeFamilyDependencies     #-}
{-# LANGUAGE TypeOperators, UndecidableInstances                        #-}

import Z3.Monad
import Control.Monad.Trans (liftIO)
import Control.Monad

run :: IO ()
run = evalZ3 fixpointComputation

fixpointComputation :: Z3 ()
fixpointComputation = do
  intSort <- mkIntSort
  edge <- join $ mkFuncDecl <$> (mkStringSymbol "edge") <*> pure [intSort, intSort] <*> mkBoolSort
  path <- join $ mkFuncDecl <$> (mkStringSymbol "path") <*> pure [intSort, intSort] <*> mkBoolSort
  a <- join $ mkVar <$> mkStringSymbol "a" <*> (pure intSort)
  b <- join $ mkVar <$> mkStringSymbol "b" <*> (pure intSort)
  c <- join $ mkVar <$> mkStringSymbol "c" <*> (pure intSort)
  fpAddRule (implies_ (mkApp edge [a,b]) (mkApp path [a,b])) (mkStringSymbol "ruleSymbol1")
  fpAddRule (implies_ (and_ [mkApp edge [a,b], mkApp edge [b,c]]) (mkApp path [a,c])) (mkStringSymbol "ruleSymbol2")
  fpAddRule (join $ mkApp <$> pure edge <*> sequence [ic 1, ic 2]) (mkStringSymbol "base1")
  fpAddRule (join $ mkApp <$> pure edge <*> sequence [ic 1, ic 3]) (mkStringSymbol "base2")
  fpAddRule (join $ mkApp <$> pure edge <*> sequence [ic 2, ic 4]) (mkStringSymbol "base3")
  q3 <- join $ mkFuncDecl <$> (mkStringSymbol "q3") <*> pure [intSort] <*> mkBoolSort
  one <- ic 1
  fpAddRule (implies_ (mkApp path [one,b]) (mkApp q3 [b])) (mkStringSymbol "q3rule")
  liftIO . putStrLn $ "AN ERROR IS ABOUT TO HAPPEN:"
  res <- fixedpointQueryRelations [q3]
  liftIO . putStrLn $ "The solution:"
  liftIO . print $ res
  astRes <- fixedpointGetAnswer
  astResString <- astToString astRes
  liftIO . print $ astResString

--------------------------------------------------------------------------------
-- Utilities
--------------------------------------------------------------------------------

(===) :: Z3 AST -> Z3 AST -> Z3 AST
(===) a b = join (mkEq <$> a <*> b)

not_ :: Z3 AST -> Z3 AST
not_ a = join (mkNot <$> a)

assert_ :: Z3 AST -> Z3 ()
assert_ a = join (assert <$> a)

implies_ :: Z3 AST -> Z3 AST -> Z3 AST
implies_ a b = join (mkImplies <$> a <*> b)

and_ :: [Z3 AST] -> Z3 AST
and_ a = sequence a >>= mkAnd

fpAddRule :: Z3 AST -> Z3 Symbol -> Z3 ()
fpAddRule a b = join $ fixedpointAddRule <$> a <*> b

fpRegisterRelation :: Z3 FuncDecl -> Z3 ()
fpRegisterRelation a = join $ fixedpointRegisterRelation <$> a

ic :: Int -> Z3 AST
ic n = join $ mkConst <$> mkIntSymbol n <*> mkIntSort

Unfortunately, if I try to run the run function, I get, after the warning I inserted:

AN ERROR IS ABOUT TO HAPPEN:
*** Exception: Z3 error: Illegal head. The head predicate needs to be uninterpreted and registered (as recursive) (path a b)

Could you show me how to get the output of the example problem?

NOTE for the reasons outlined in [#9] you shouldn't use the last z3 (z3-4.7.1 is ok)

[IagoAbal]

Hi,

I am no expert in the Fixedpoint API, but you may be using the API incorrectly. This error is raised by the Z3 library itself.

Could you try to reproduce this with the C or the Python API? If you can get it to work with one of the official APIs, then I would have strong evidence to believe that the problem may be somewhere in the Haskell bindings.

[meditans]

Hi, I think I am indeed using the haskell api incorrectly! The question was mainly along the lines of "what am I doing wrong?", because my translation seems to me a fairly close analogue of the smt2-lib version. In the meantime, I found your old bitbucket repo, and saw how the fixpoint API was added, and I'd like to ping @DAHeath, which should be more knowledgeable on this aspect.