Add dependent resource inference

bin/Synquid.hs

@@ -7,7 +7,7 @@ import Synquid.Program
 import Synquid.Error
 import Synquid.Pretty
 import Synquid.Parser
-import Synquid.Logic (Formula(..), QSpace)
+import Synquid.Logic (Formula(..))
 import Synquid.Resolver (resolveDecls)
 import Synquid.Solver.Monad hiding (name)
 import Synquid.Solver.HornClause
@@ -16,24 +16,20 @@ import Synquid.Synthesis.Util
 import Synquid.HtmlOutput
 import Synquid.Solver.Types
 import Synquid.Solver.CEGIS (initCEGISState)
+import Synquid.Z3 (z3LitToInt)
 
-import           Control.Applicative ((<|>))
 import           Control.Monad
 import           Control.Monad.State hiding (fix)
 import           System.Exit
 import           System.Console.CmdArgs
 import           Data.Time.Calendar
 import qualified Data.Map as Map
-import           Data.Map.Ordered (OMap)
 import qualified Data.Map.Ordered as OMap
-import           Data.Set (Set)
-import qualified Data.Set as Set
-import           Control.Lens ((.~), (^.), (%~), (&), (%=), _last, _Just)
+import           Data.Maybe (isJust)
+import           Control.Lens ((.~), (^.), (%~), (%=), _last, _Just)
 
 import Data.List.Split
 
-import Debug.Pretty.Simple
-
 programName = "resyn"
 versionName = "0.1"
 releaseDate = fromGregorian 2020 7 15
@@ -55,8 +51,9 @@ main = do
                     _constantTime = constTime,
                     _cegisBound = cegis_max,
                     _enumerate = ec,
-                    _inferResources = infer,
+                    _inferResources = isJust infer,
                     _rsolver = res_solver,
+                    _rSolverDomain = maybe Constant id infer,
                     _sygusLog = logfile,
                     _cvc4 = cvc4cmd
                   }
@@ -146,7 +143,7 @@ data CommandLineArgs
         ct :: Bool,
         cegis_max :: Int,
         eac :: Bool,
-        infer :: Bool,
+        infer :: Maybe RDomain,
         res_solver :: ResourceSolver,
         logfile :: Maybe String,
         solve_sygus :: String
@@ -186,7 +183,7 @@ synt = Synthesis {
   ct                  = False           &= help ("Require that all branching expressions consume a constant amount of resources (default: False)"),
   cegis_max           = 100             &= help ("Maximum number of iterations through the CEGIS loop (default: 100)"),
   eac                 = False           &= help ("Enumerate-and-check instead of round-trip resource analysis (default: False)"),
-  infer               = False           &= help ("Infer all resource bounds (default: False)"),
+  infer               = Nothing         &= help ("Infer all resource bounds (default: False)"),
   res_solver          = CEGIS           &= help (unwords ["Which solver should be used for resource constraints?", show SYGUS, show CEGIS, show Incremental, "(default: ", show CEGIS, ")"]),
   logfile             = Nothing         &= help ("File for logging SYGUS constraints (default: no logging)"),
   solve_sygus         = "cvc4"          &= help ("Command to run SYGUS solver (default: \"cvc4\")")
@@ -310,7 +307,7 @@ runOnFile synquidParams explorerParams solverParams file libs = do
       -- potentials and their values
       when ((not (null results)) && infer) $ do
         -- We first replace all our Z3 lits where we can to avoid derefencing freed ptrs
-        let potls = fmap (fmap z3litToInt) $ (finalTState (last results)) ^. persistentState . inferredRVars
+        let potls = fmap (fmap z3LitToInt) $ (finalTState (last results)) ^. persistentState . inferredRVars
 
         liftIO $ mapM_ (\g -> pdoc ((prettyWithInferred potls g) <+> text "(inferred)"))
                $ fmap goal results
@@ -344,12 +341,9 @@ runOnFile synquidParams explorerParams solverParams file libs = do
       -- we collect all res constraints into our state and solve these constraints
       -- at the very end.
 
-      -- TODO: This is awful for performance. Right now we check all created resource constraints
-      -- for each function as type-check it. This is good for errors, bad for performance.
-      -- We should try to not do resource checking until the very end
-
       -- We first modify our persistent typing state to add the inferred potl vars of this goal
-      _Just . inferredRVars %= \x -> OMap.unionWithL (\_ -> const) x (OMap.fromList [(p, Nothing) | p <- gInferredPotlVars goal])
+      _Just . inferredRVars %= \x -> OMap.unionWithL (\_ -> const) x (OMap.fromList [(p, Nothing) | (p, _, _) <- gInferredPotlVars goal])
+      _Just . resourceVars %= (flip Map.union) (Map.fromList $ [(a, b) | (a, b, _) <- gInferredPotlVars goal])
 
       -- We first get our persistent typing state and pass it through
       mpts <- get
@@ -366,9 +360,6 @@ runOnFile synquidParams explorerParams solverParams file libs = do
 
           return result
 
-    z3litToInt (Z3Lit _ _ s) = IntLit (read s :: Int)
-    z3litToInt x = x
-
     assembleResult goal ps = SynthesisResult (fst (head ps)) (snd (head ps)) (tail ps) goal
     updateLogLevel goal orig = if gSynthesize goal then orig else 0 -- prevent logging while type checking measures
 

src/Synquid/Logic.hs

@@ -235,16 +235,6 @@ unknownsOf (Cons _ _ es) = Set.unions $ map unknownsOf es
 unknownsOf (All _ e) = unknownsOf e
 unknownsOf _ = Set.empty
 
--- collect guards of ITE expressions
---   careful, this should only be used on resource formulas!
-itesOf :: Formula -> [Formula]
-itesOf (Ite g t f) = [Ite g t f] -- Assumes no nested ITEs!
-itesOf (WithSubst _ f) = itesOf f
-itesOf (Unary _ f) = itesOf f
-itesOf (Binary _ f g) = itesOf f ++ itesOf g
-itesOf _ = [] 
-
-
 
 -- | 'posNegUnknowns' @fml@: sets of positive and negative predicate unknowns in @fml@
 posNegUnknowns :: Formula -> (Set Id, Set Id)

src/Synquid/Pretty.hs

@@ -74,9 +74,7 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<+>), (<$>), hsep, vsep)
 import qualified Text.PrettyPrint.ANSI.Leijen as L
 import qualified Data.Set as Set
 import qualified Data.Map as Map
-import qualified Data.Map.Ordered as OMap
 import Data.Map (Map)
-import Data.Map.Ordered (OMap)
 import Data.Set (Set)
 import Data.List
 import Data.Maybe (fromMaybe)
@@ -198,7 +196,7 @@ fmlDocAt n fml = condHlParens (n' <= n) (
     SetLit s elems -> hlBrackets $ commaSep $ map fmlDoc elems
     Var s name -> if name == valueVarName then special name else text name
     Unknown s name -> if Map.null s then text name else hMapDoc pretty pretty s <> text name
-    WithSubst _ e -> fmlDocAt n' e
+    WithSubst s e -> if Map.null s then fmlDocAt n' e else hMapDoc pretty pretty s <> fmlDocAt n' e
     Unary op e -> pretty op <> fmlDocAt n' e
     Binary op e1 e2 -> fmlDocAt n' e1 <+> pretty op <+> fmlDocAt n' e2
     Ite e0 e1 e2 -> keyword "if" <+> fmlDoc e0 <+> keyword "then" <+> fmlDoc e1 <+> keyword "else" <+> fmlDoc e2

src/Synquid/Program.hs

@@ -658,7 +658,7 @@ data Goal = Goal {
   gImpl :: UProgram,            -- ^ Implementation template
   gDepth :: Int,                -- ^ Maximum level of auxiliary goal nesting allowed inside this goal
   gSourcePos :: SourcePos,      -- ^ Source Position,
-  gInferredPotlVars :: [Id],    -- ^ Set of potential vars to infer for this fn
+  gInferredPotlVars :: [(Id, [Formula], Environment)],    -- ^ Set of potential vars to infer for this fn
   gInferSolve :: Bool,          -- ^ If gInferredPotlVars isn't empty, indicates if we should actually solve inference constraints or just collect them without solving
   gSynthesize :: Bool           -- ^ Synthesis flag (false implies typechecking only)
 } deriving (Show, Eq, Ord)
@@ -793,3 +793,4 @@ defaultSetType = DataDecl name typeVars preds cons
     insert = ConstructorSig insertSetCtor (FunctionT "x" (ScalarT (TypeVarT Map.empty "a" defMultiplicity) (BoolLit True) defPotential) (FunctionT "xs" (ScalarT (DatatypeT setTypeName [ScalarT (TypeVarT Map.empty "a" defMultiplicity) (BoolLit True) defPotential] []) (BoolLit True) defPotential) (ScalarT (DatatypeT setTypeName [ScalarT (TypeVarT Map.empty "a" defMultiplicity) (BoolLit True) defPotential] []) (BoolLit True) defPotential) defCost) defCost)
 
 setConstructors = [emptySetCtor, singletonCtor, insertSetCtor]
+