Interpreter only on LHS

liquid-fixpoint.cabal

@@ -69,8 +69,10 @@ library
                     Language.Fixpoint.Solver.EnvironmentReduction
                     Language.Fixpoint.Solver.GradualSolution
                     Language.Fixpoint.Solver.Instantiate
+                    Language.Fixpoint.Solver.Interpreter
                     Language.Fixpoint.Solver.PLE
                     Language.Fixpoint.Solver.Monad
+                    Language.Fixpoint.Solver.Normalize
                     Language.Fixpoint.Solver.Rewrite
                     Language.Fixpoint.Solver.Prettify
                     Language.Fixpoint.Solver.Sanitize

src/Language/Fixpoint/Solver.hs

@@ -96,7 +96,7 @@ ignoreQualifiers cfg fi
 --------------------------------------------------------------------------------
 -- | Solve FInfo system of horn-clause constraints -----------------------------
 --------------------------------------------------------------------------------
-solve :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a
+solve :: (NFData a, Fixpoint a, Show a, Loc a, PPrint a) => Solver a
 --------------------------------------------------------------------------------
 solve cfg q
   | parts cfg      = partition  cfg        $!! q
@@ -106,7 +106,7 @@ solve cfg q
   | minimizeKs cfg = minKvars cfg solve'   $!! q
   | otherwise      = solve'     cfg        $!! q
 
-solve' :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a
+solve' :: (NFData a, Fixpoint a, Show a, Loc a, PPrint a) => Solver a
 solve' cfg q = do
   when (save cfg) $ saveQuery   cfg q
   configSW  cfg     solveNative cfg q
@@ -179,7 +179,7 @@ inParallelUsing f xs = do
 --------------------------------------------------------------------------------
 -- | Native Haskell Solver -----------------------------------------------------
 --------------------------------------------------------------------------------
-solveNative, solveNative' :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a
+solveNative, solveNative' :: (NFData a, Fixpoint a, Show a, Loc a, PPrint a) => Solver a
 --------------------------------------------------------------------------------
 solveNative !cfg !fi0 = (solveNative' cfg fi0)
                           `catch`

src/Language/Fixpoint/Solver/EnvironmentReduction.hs

@@ -55,6 +55,7 @@ import           Language.Fixpoint.Types.Names
   , isPrefixOfSym
   , prefixOfSym
   , symbolText
+  , vvName
   )
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Refinements
@@ -618,13 +619,13 @@ inlineInExpr :: HashMap Symbol (m, SortedReft) -> Expr -> Expr
 inlineInExpr env = simplify . mapExprOnExpr inlineExpr
   where
     inlineExpr (EVar sym)
-      | anfPrefix `isPrefixOfSym` sym
+      | (anfPrefix `isPrefixOfSym` sym) || (vvName `isPrefixOfSym` sym)
       , Just (_, sr) <- HashMap.lookup sym env
       , let r = sr_reft sr
       , Just e <- isSingletonE (reftBind r) (reftPred r)
       = wrapWithCoercion Eq (sr_sort sr) e
     inlineExpr (PAtom br e0 e1@(dropECst -> EVar sym))
-      | anfPrefix `isPrefixOfSym` sym
+      | (anfPrefix `isPrefixOfSym` sym) || (vvName `isPrefixOfSym` sym)
       , isEq br
       , Just (_, sr) <- HashMap.lookup sym env
       , let r = sr_reft sr

src/Language/Fixpoint/Solver/Normalize.hs

@@ -0,0 +1,47 @@
+module Language.Fixpoint.Solver.Normalize (normalize) where 
+
+import  Language.Fixpoint.Types 
+
+-------------------------------------------------------------------------------
+-- | Normalization of Equation: make their arguments unique -------------------
+-------------------------------------------------------------------------------
+
+class Normalizable a where 
+  normalize :: a -> a 
+
+instance Normalizable (GInfo c a) where 
+  normalize si = si {ae = normalize $ ae si}
+
+instance Normalizable AxiomEnv where 
+  normalize aenv = aenv { aenvEqs   = (normalize <$> aenvEqs   aenv)
+                        , aenvSimpl = (normalize <$> aenvSimpl aenv) }
+
+instance Normalizable Rewrite where 
+  normalize rw = rw { smArgs = xs', smBody = normalizeBody (smName rw) $ subst su $ smBody rw }
+    where 
+      su  = mkSubst $ zipWith (\x y -> (x,EVar y)) xs xs'
+      xs  = smArgs rw 
+      xs' = zipWith mkSymbol xs [0..]
+      mkSymbol x i = x `suffixSymbol` intSymbol (smName rw) i 
+
+instance Normalizable Equation where 
+  normalize eq = eq {eqArgs = zip xs' ss, 
+                     eqBody = normalizeBody (eqName eq) $ subst su $ eqBody eq }
+    where 
+      su           = mkSubst $ zipWith (\x y -> (x,EVar y)) xs xs'
+      (xs,ss)      = unzip (eqArgs eq) 
+      xs'          = zipWith mkSymbol xs [0..]
+      mkSymbol x i = x `suffixSymbol` intSymbol (eqName eq) i 
+
+normalizeBody :: Symbol -> Expr -> Expr
+normalizeBody f = go   
+  where 
+    go e 
+      | any (== f) (syms e) 
+      = go' e 
+    go e 
+      = e 
+
+    go' (PAnd [PImp c e1,PImp (PNot c') e2])
+      | c == c' = EIte c e1 (go' e2)
+    go' e = e 

src/Language/Fixpoint/Solver/PLE.hs

@@ -78,7 +78,7 @@ traceE (e,e')
 --------------------------------------------------------------------------------
 {-# SCC instantiate #-}
 instantiate :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
-instantiate cfg fi' subcIds = do
+instantiate cfg fi subcIds = do
     let cs = M.filterWithKey
                (\i c -> isPleCstr aEnv i c && maybe True (i `L.elem`) subcIds)
                (cm fi)
@@ -95,7 +95,6 @@ instantiate cfg fi' subcIds = do
     file   = srcFile cfg ++ ".evals"
     sEnv   = symbolEnv cfg fi
     aEnv   = ae fi
-    fi     = normalize fi'
 
 savePLEEqualities :: Config -> SInfo a -> InstRes -> IO ()
 savePLEEqualities cfg fi res = when (save cfg) $ do
@@ -429,6 +428,8 @@ isGoodApp γ e
 
 
 
+
+
 getCstr :: M.HashMap SubcId (SimpC a) -> SubcId -> SimpC a
 getCstr env cid = Misc.safeLookup "Instantiate.getCstr" cid env
 
@@ -1127,62 +1128,6 @@ applyConstantFolding bop e1 e2 =
         getOp' op  = getOp op
 
 
--------------------------------------------------------------------------------
--- | Normalization of Equation: make their arguments unique -------------------
--------------------------------------------------------------------------------
-
-class Normalizable a where
-  normalize :: a -> a
-
-instance Normalizable (GInfo c a) where
-  normalize si = si {ae = normalize $ ae si}
-
-instance Normalizable AxiomEnv where
-  normalize aenv = aenv { aenvEqs   = mytracepp "aenvEqs"  (normalize <$> aenvEqs   aenv)
-                        , aenvSimpl = mytracepp "aenvSimpl" (normalize <$> aenvSimpl aenv) }
-
-instance Normalizable Rewrite where
-  normalize rw = rw { smArgs = xs', smBody = normalizeBody (smName rw) $ subst su $ smBody rw }
-    where
-      su  = mkSubst $ zipWith (\x y -> (x,EVar y)) xs xs'
-      xs  = smArgs rw
-      xs' = zipWith mkSymbol xs [0..]
-      mkSymbol x i = x `suffixSymbol` intSymbol (smName rw) i
-
-
-instance Normalizable Equation where
-  normalize eq = eq {eqArgs = zip xs' ss, eqBody = normalizeBody (eqName eq) $ subst su $ eqBody eq }
-    where
-      su      = mkSubst $ zipWith (\x y -> (x,EVar y)) xs xs'
-      (xs,ss) = unzip (eqArgs eq)
-      xs'     = zipWith mkSymbol xs [0..]
-      mkSymbol x i = x `suffixSymbol` intSymbol (eqName eq) i
-
-
-normalizeBody :: Symbol -> Expr -> Expr
-normalizeBody f = go
-  where
-    go e
-      | any (== f) (syms e)
-      = go' e
-    go e
-      = e
-
-    go' (PAnd [PImp c e1,PImp (PNot c') e2])
-      | c == c' = EIte c e1 (go' e2)
-    go' e = e
-
-_splitBranches :: Symbol -> Expr -> [(Expr, Expr)]
-_splitBranches f = go
-  where
-    go (PAnd es)
-      | any (== f) (syms es)
-      = go' <$> es
-    go e
-      = [(PTrue, e)]
-
-    go' (PImp c e) = (c, e)
-    go' e          = (PTrue, e)
 
 -- -- TODO:FUEL Config
 -- maxFuel :: Int
@@ -1203,4 +1148,4 @@ checkFuel f = do
   fc <- gets evFuel
   case (M.lookup f (fcMap fc), fcMax fc) of
     (Just fk, Just n) -> pure (fk <= n)
-    _                 -> pure True
+    _                 -> pure True

src/Language/Fixpoint/Solver/Solve.hs

@@ -34,10 +34,16 @@ import qualified Data.HashSet        as S
 import qualified Data.List           as L
 import Language.Fixpoint.Types (resStatus, FixResult(Unsafe))
 import qualified Language.Fixpoint.Types.Config as C
+import Language.Fixpoint.Solver.Interpreter (instInterpreter)
 import Language.Fixpoint.Solver.Instantiate (instantiate)
+-- import Debug.Trace                      (trace)
+import Language.Fixpoint.Solver.Normalize 
+
+-- mytrace :: String -> a -> a
+-- mytrace =  {- trace -} flip const
 
 --------------------------------------------------------------------------------
-solve :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> F.SInfo a -> IO (F.Result (Integer, a))
+solve :: (NFData a, F.Fixpoint a, Show a, F.Loc a, PPrint a) => Config -> F.SInfo a -> IO (F.Result (Integer, a))
 --------------------------------------------------------------------------------
 
 solve cfg fi = do
@@ -79,6 +85,16 @@ solverInfo cfg fI
 siKvars :: F.SInfo a -> S.HashSet F.KVar
 siKvars = S.fromList . M.keys . F.ws
 
+doInterpret :: (F.Loc a, Fixpoint a, PPrint a) => Config -> F.SInfo a -> [F.SubcId] -> SolveM (F.SInfo a, [Integer])
+doInterpret cfg fi0 subcIds = do
+  (fi, solved) <- liftIO $ instInterpreter cfg fi0 subcIds
+  modify $ update' fi
+  return (fi, solved)  
+  where
+    update' fi ss = ss{ssBinds = F.bs fi'}
+      where
+        fi' = (siQuery sI) {F.hoInfo = F.HOI (C.allowHO cfg) (C.allowHOqs cfg)}
+        sI  = solverInfo cfg fi
 
 {-# SCC doPLE #-}
 doPLE :: (F.Loc a) =>  Config -> F.SInfo a -> [F.SubcId] -> SolveM ()
@@ -93,7 +109,7 @@ doPLE cfg fi0 subcIds = do
 
 --------------------------------------------------------------------------------
 {-# SCC solve_ #-}
-solve_ :: (NFData a, F.Fixpoint a, F.Loc a)
+solve_ :: (NFData a, F.Fixpoint a, F.Loc a, Show a, PPrint a)
        => Config
        -> F.SInfo a
        -> Sol.Solution
@@ -109,17 +125,35 @@ solve_ cfg fi s0 ks wkl = do
     s3       <- {- SCC "sol-refine" #-} refine bindingsInSmt s2 wkl
     res0     <- {- SCC "sol-result" #-} result bindingsInSmt cfg wkl s3
     return (s3, res0)
+  let finormalized = normalize fi
+  liftIO $ printUnsafe "ORG" (resStatus res0) 
   res <- case resStatus res0 of
     Unsafe _ bads | not (noLazyPLE cfg) && rewriteAxioms cfg -> do
-      doPLE cfg fi (map fst bads)
+      goods <- if (useInterpreter cfg) 
+                 then snd <$> doInterpret cfg finormalized (fst <$> bads)
+                 else return [] 
+      liftIO $ printUnsafe "INT" (markSafe goods $ resStatus res0) 
+      doPLE cfg finormalized (map fst bads L.\\ goods)
       sendConcreteBindingsToSMT F.emptyIBindEnv $ \bindingsInSmt -> do
         s4 <- {- SCC "sol-refine" #-} refine bindingsInSmt s3 wkl
-        result bindingsInSmt cfg wkl s4
+        r4 <- result bindingsInSmt cfg wkl s4
+        liftIO $ printUnsafe "PLE" (markSafe goods $ resStatus r4) 
+        return r4{resStatus = markSafe goods $ resStatus r4}
     _ -> return res0
   st      <- stats
   let res' = {- SCC "sol-tidy"   #-} tidyResult res
   return $!! (res', st)
 
+printUnsafe :: String -> FixResult (SubcId, a) -> IO ()
+printUnsafe s (Unsafe _ ids) = putStrLn (s ++ " " ++ show (L.sort (fst <$> ids)))
+printUnsafe s _ = putStrLn ( s ++  " All SAFE") 
+
+markSafe :: [SubcId] -> FixResult (SubcId, a) -> FixResult (SubcId, a)
+markSafe sids (Unsafe s ids) = case filter (\(i,_) -> i `notElem` sids) ids of 
+                                 []    -> F.Safe s
+                                 rest  -> Unsafe s rest
+markSafe _ r = r 
+
 --------------------------------------------------------------------------------
 -- | tidyResult ensures we replace the temporary kVarArg names introduced to
 --   ensure uniqueness with the original names in the given WF constraints.

src/Language/Fixpoint/Types/Config.hs

@@ -87,6 +87,7 @@ data Config = Config
   , nonLinCuts       :: Bool           -- ^ Treat non-linear vars as cuts
   , noslice          :: Bool           -- ^ Disable non-concrete KVar slicing
   , rewriteAxioms    :: Bool           -- ^ Allow axiom instantiation via rewriting
+  , useInterpreter   :: Bool           -- ^ Use the interpreter to assist PLE
   , oldPLE           :: Bool           -- ^ Use old version of PLE
   , noIncrPle        :: Bool           -- ^ Use incremental PLE
   , noEnvironmentReduction :: Bool     -- ^ Don't use environment reduction
@@ -183,6 +184,7 @@ defConfig = Config {
   , nonLinCuts               = False &= help "Treat non-linear kvars as cuts"
   , noslice                  = False &= help "Disable non-concrete KVar slicing"
   , rewriteAxioms            = False &= help "allow axiom instantiation via rewriting"
+  , useInterpreter           = False &= help "Use the interpreter to assist PLE"
   , oldPLE                   = False &= help "Use old version of PLE"
   , noIncrPle                = False &= help "Don't use incremental PLE"
   , noEnvironmentReduction   =

src/Language/Fixpoint/Types/Names.hs

@@ -40,6 +40,8 @@ module Language.Fixpoint.Types.Names (
   , isNonSymbol
   , isLitSymbol
   , isTestSymbol
+  , isANFSymbol
+  , isDataconSymbol
   -- , isCtorSymbol
   , isNontrivialVV
   , isDummy
@@ -73,6 +75,7 @@ module Language.Fixpoint.Types.Names (
   , tempSymbol
   , gradIntSymbol
   , appendSymbolText
+  , dataconSymbol
 
   -- * Wrapping Symbols
   , litSymbol
@@ -489,14 +492,25 @@ gradIntSymbol = intSymbol gradPrefix
 bindSymbol :: Integer -> Symbol
 bindSymbol = intSymbol bindPrefix
 
-tempPrefix, anfPrefix, renamePrefix, litPrefix, gradPrefix, bindPrefix :: Symbol
+tempPrefix, anfPrefix, renamePrefix, litPrefix, gradPrefix, bindPrefix, dataconPrefix :: Symbol
 tempPrefix   = "lq_tmp$"
 anfPrefix    = "lq_anf$"
 renamePrefix = "lq_rnm$"
+dataconPrefix = "lq_dc$"
 litPrefix    = "lit$"
 gradPrefix   = "grad$"
 bindPrefix   = "b$"
 
+dataconSymbol :: Integer -> Symbol 
+dataconSymbol = intSymbol dataconPrefix
+isDataconSymbol :: Symbol -> Bool
+isDataconSymbol = isPrefixOfSym dataconPrefix
+
+
+isANFSymbol :: Symbol -> Bool
+isANFSymbol = isPrefixOfSym anfPrefix
+
+
 testPrefix  :: Symbol
 testPrefix   = "is$"