Partially finished formula to cfg function implemented

cabal.project

@@ -6,8 +6,8 @@
 
 packages:
   what4/
-  what4-abc/
-  what4-blt/
+--  what4-abc/
+--  what4-blt/
   what4-transition-system/
 
 optional-packages:

what4/src/What4/Protocol/Online.hs

@@ -63,10 +63,14 @@ import           Data.IORef
 import qualified Data.List as L
 #endif
 import           Data.List (intercalate)
+import qualified Data.Map as Map
+import qualified Data.Set as Set
 import           Data.Parameterized.Some
 import           Data.Proxy
 import           Data.Text (Text)
 import qualified Data.Text.Lazy as LazyText
+import           Data.Parameterized.NatRepr as NatRepr
+import           GHC.TypeNats as TypeNats
 import           Prettyprinter
 import           System.Exit
 import           System.IO
@@ -74,6 +78,7 @@ import qualified System.IO.Error as IOE
 import qualified System.IO.Streams as Streams
 import           System.Process (ProcessHandle, terminateProcess, waitForProcess)
 
+import           What4.BaseTypes
 import           What4.Expr
 import           What4.Interface {-(SolverEvent(..)
                                  , SolverStartSATQuery(..)
@@ -248,10 +253,11 @@ checkSatisfiable proc rsn p =
 data SMTType = 
     Bool
   | Intgr
-  | BV Int
+  | BV Integer
   | Str
   | Real
   | Float
+  deriving (Eq, Ord)
 instance Show SMTType where
   show Bool = "Bool"
   show Intgr = "Int"
@@ -260,6 +266,44 @@ instance Show SMTType where
   show Real = "Real"
   show Float = "Float"
 
+{- Attempt at the FIXME above
+   BaseTypeRepr tp replaces SMTType
+   The only problem: I'm currently replacing
+   [(SMTType, [(String, [SMTType])])] by [(BaseTypeRepr x, [(String, [BaseTypeRepr y])])] in getAbduct
+   This is incorrect, since this assumes for each BaseTypeRepr x, all the 
+   operators have only BaseTypeRepr y in their signature. I want something like 
+   BaseTypeRepr 'y where 'y is variable, and I don't know how to do this
+-- This replaces show
+btToStr :: BaseTypeRepr tp -> String
+btToStr BaseBoolRepr = "Bool"
+btToStr (BaseBVRepr n) = "(_ BitVec " <> (show n) <> ")"
+btToStr BaseIntegerRepr = "Int"
+btToStr BaseRealRepr = "Real"
+btToStr (BaseFloatRepr (FloatingPointPrecisionRepr eb sb)) = "(_ FloatingPoint " <> (show eb) <> " " <> (show sb) <> ")" 
+btToStr _ = "unsupported"
+
+-- This replaces the cfgToString
+cfgToString :: [(BaseTypeRepr x, [(String, [BaseTypeRepr y])])] -> String
+cfgToString [] = ""
+cfgToString g =
+  let nonTerminals = paren . unwords $ map (\(t,_) -> paren $ typNT t) g in
+  let rules = paren . intercalate "\n" $ map (\(t, acts) -> paren $ (lhs t) <> " " <> (rhs acts)) g in
+  (nonTerminals <> "\n" <> rules)
+  where
+    typNT' (BaseBVRepr n) = "GBV" <> (show n)
+    typNT' (BaseFloatRepr (FloatingPointPrecisionRepr eb sb)) = "GFP" <> (show eb) <> (show sb)
+    typNT' t = "G" <> (btToStr t)
+    typNT t = unwords [typNT' t, btToStr t]
+    
+    paren s = "("<>s<>")"
+    
+    lhs b = typNT b
+    rhs' (s, bs) = 
+      case bs of 
+          [] -> s
+          _ -> paren . unwords $ s : map typNT' bs
+    rhs sbs = paren . unwords $ map rhs' sbs -}
+
 -- A grammar for getting abducts is specified in terms of SMT sorts, 
 -- and sorted functions/constants. Convert it to a string to call with
 -- get-abduct
@@ -284,17 +328,63 @@ cfgToString g =
     rhs sbs = paren . unwords $ map rhs' sbs
 
 {- Can we pattern match on the BoolExpr, and automatically generate the grammar for abduction
-   using all the operators in it?
+   using all the operators in it? -}
 defaultCfg ::
   SMTReadWriter solver =>
   SolverProcess scope solver ->
-  BoolExpr scope ->
-  [(SMTType, [(String, [SMTType])])]
-defaultCfg proc t =
+  Expr scope tp ->
+  Map.Map SMTType (Set.Set (String, [SMTType])) ->
+  Map.Map SMTType (Set.Set (String, [SMTType]))
+defaultCfg proc t m =
   case t of
-  intLe _ _ _ -> []
-   _ -> []
--}
+    SemiRingLiteral repr coeff loc -> Map.empty
+    BoolExpr b loc -> Map.empty
+    AppExpr ae ->
+      case appExprApp ae of
+        BaseIte ty _ c e1 e2 -> Map.empty
+        BaseEq (BaseBVRepr n) e1 e2 ->
+          let n' = NatRepr.intValue n in
+          let m1 = defaultCfg proc e1 m in
+          let m2 = defaultCfg proc e2 m1 in
+          -- Do we have a rule for Bool already?
+          case (Map.lookup Bool m2) of
+            Just l ->
+              Map.adjust (Set.insert ("=", [BV n', BV n'])) Bool m2
+            Nothing ->
+              Map.insert Bool (Set.singleton ("=", [BV n', BV n'])) m2
+        NotPred e -> Map.empty
+        ConjPred cs -> Map.empty
+        BVSlt e1 e2 -> Map.empty
+        BVUlt e1 e2 -> Map.empty
+        _ -> Map.empty
+    _ -> Map.empty
+
+{-defaultCfg ::
+  SMTReadWriter solver =>
+  SolverProcess scope solver ->
+  BoolExpr scope ->
+  Map.Map SMTType (Set.Set (String, [SMTType])) ->
+  Map.Map SMTType (Set.Set (String, [SMTType]))
+defaultCfg proc t m =
+  case t of
+    AppExpr ae ->
+      case appExprApp ae of
+        BaseIte ty _ c e1 e2 -> Map.empty
+        BaseEq (BaseBVRepr n) e1 e2 ->
+          let m1 = defaultCfg proc e1 m in
+          let m2 = defaultCfg proc e2 m1 in
+          -- Do we have a rule for Bool already?
+          case Map.lookup Bool m2 of
+            Just l ->
+              Map.adjust (Set.insert l ("=", BV (toInteger n), BV (toInteger n))) Bool m2
+            Nothing ->
+              Map.insert Bool Set.singleton ("=", BV (toInteger n), BV (toInteger n))
+        NotPred e -> Map.empty
+        ConjPred cs -> Map.empty
+        BVSlt e1 e2 -> Map.empty
+        BVUlt e1 e2 -> Map.empty
+        _ -> Map.empty
+    _ -> Map.empty-}
 
 -- | Get `n` abducts from the SMT solver, the disjunction of which entail `t`, and bind them to `nm`
 getAbducts ::

what4/src/What4/Solver/CVC5.hs

@@ -228,8 +228,8 @@ setInteractiveLogicAndOptions writer = do
     -- Tell cvc5 to make declarations global, so they are not removed by 'pop' commands
     SMT2.setOption writer "global-declarations" "true"
     -- Tell cvc5 to compute UNSAT cores, if that feature is enabled
-    when (supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do
-      SMT2.setOption writer "produce-unsat-cores" "true"
+    -- when (supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do
+    --  SMT2.setOption writer "produce-unsat-cores" "true"
     -- Tell cvc5 to produce abducts, if that feature is enabled
     when (supportedFeatures writer `hasProblemFeature` useProduceAbducts) $ do
       SMT2.setOption writer "produce-abducts" "true"