Improve precision of datetime

Strata/Languages/Boogie/Options.lean

@@ -4,6 +4,10 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
+structure Z3Options where
+  -- Will prepend `(set-option e.fst e.snd)` ... for each `e: String × String` in `options`
+  options : List (String × String)
+
 structure Options where
   verbose : Bool
   parseOnly : Bool
@@ -13,6 +17,8 @@ structure Options where
   removeIrrelevantAxioms : Bool
   /-- Solver time limit in seconds -/
   solverTimeout : Nat
+  z3Options: Option Z3Options
+
 
 def Options.default : Options := {
   verbose := true,
@@ -21,7 +27,8 @@ def Options.default : Options := {
   checkOnly := false,
   stopOnFirstError := false,
   removeIrrelevantAxioms := false,
-  solverTimeout := 10
+  solverTimeout := 10,
+  z3Options := none,
 }
 
 instance : Inhabited Options where

Strata/Languages/Boogie/Verifier.lean

@@ -179,15 +179,27 @@ instance : ToFormat VCResults where
 instance : ToString VCResults where
   toString rs := toString (VCResults.format rs)
 
-def getSolverPrelude : String → SolverM Unit
-| "z3" => do
-  -- These options are set by the standard Boogie implementation and are
-  -- generally good for the Boogie dialect, too, though we may want to
-  -- have more fine-grained criteria for when to use them.
-  Solver.setOption "smt.mbqi" "false"
-  Solver.setOption "auto_config" "false"
-| "cvc5" => return ()
-| _ => return ()
+def getSolverPrelude (z3Options : Option Z3Options) (solverName : String) : SolverM Unit :=
+  match z3Options with
+  | .some l => do
+      let rec go := (λ l =>
+        match l with
+        | [] => return ()
+        | h :: t => do
+          Solver.setOption h.fst h.snd
+          go t
+        )
+      go l.options
+  | _ =>
+    match solverName with
+    | "z3" => do
+      -- These options are set by the standard Boogie implementation and are
+      -- generally good for the Boogie dialect, too, though we may want to
+      -- have more fine-grained criteria for when to use them.
+      Solver.setOption "smt.mbqi" "false"
+      Solver.setOption "auto_config" "false"
+    | "cvc5" => return ()
+    | _ => return ()
 
 def getSolverFlags (options : Options) (solver : String) : Array String :=
   let produceModels :=
@@ -213,7 +225,7 @@ def dischargeObligation
   let filename := s!"{VC_folder_name}/{filename}"
   let handle ← IO.FS.Handle.mk filename IO.FS.Mode.write
   let solver ← Solver.fileWriter handle
-  let prelude := getSolverPrelude smtsolver
+  let prelude := getSolverPrelude options.z3Options smtsolver
   let (ids, estate) ← Strata.SMT.Encoder.encodeBoogie ctx prelude terms solver
   let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter
   if options.verbose then IO.println s!"Wrote problem to {filename}."

Strata/Languages/Python/BoogiePrelude.lean

@@ -393,18 +393,18 @@ function Timedelta_get_days(timedelta : int) : int;
 function Timedelta_get_seconds(timedelta : int) : int;
 function Timedelta_get_microseconds(timedelta : int) : int;
 
-axiom [Timedelta_deconstructors]:
-    (forall days0 : int, seconds0 : int, msecs0 : int,
-            days : int, seconds : int, msecs : int
-            :: {(Timedelta_mk(days0, seconds0, msecs0))}
-      Timedelta_mk(days0, seconds0, msecs0) ==
-          Timedelta_mk(days, seconds, msecs) &&
-      0 <= msecs && msecs < 1000000 &&
-      0 <= seconds && seconds < 3600 * 24 &&
-      -999999999 <= days && days <= 999999999
-      ==> Timedelta_get_days(Timedelta_mk(days0, seconds0, msecs0)) == days &&
-          Timedelta_get_seconds(Timedelta_mk(days0, seconds0, msecs0)) == seconds &&
-          Timedelta_get_microseconds(Timedelta_mk(days0, seconds0, msecs0)) == msecs);
+//axiom [Timedelta_deconstructors]:
+//    (forall days0 : int, seconds0 : int, msecs0 : int,
+//            days : int, seconds : int, msecs : int
+//            :: {(Timedelta_mk(days0, seconds0, msecs0))}
+//      Timedelta_mk(days0, seconds0, msecs0) ==
+//          Timedelta_mk(days, seconds, msecs) &&
+//      0 <= msecs && msecs < 1000000 &&
+//      0 <= seconds && seconds < 3600 * 24 &&
+//      -999999999 <= days && days <= 999999999
+//      ==> Timedelta_get_days(Timedelta_mk(days0, seconds0, msecs0)) == days &&
+//          Timedelta_get_seconds(Timedelta_mk(days0, seconds0, msecs0)) == seconds &&
+//          Timedelta_get_microseconds(Timedelta_mk(days0, seconds0, msecs0)) == msecs);
 
 
 ////// Datetime.

Strata/Languages/Python/PythonToBoogie.lean

@@ -194,6 +194,7 @@ partial def PyExprToString (e : Python.expr SourceRange) : String :=
       | .Name _ id _ => s!"List[{id.val}]"
       | _ => panic! s!"Unsupported slice: {repr slice}"
     | _ => panic! s!"Unsupported subscript to string: {repr e}"
+  | .Constant _ (.ConString _ s) _ => s.val
   | _ => panic! s!"Unhandled Expr: {repr e}"
 
 def PyExprToMonoTy (e : Python.expr SourceRange) : Lambda.LMonoTy :=
@@ -609,9 +610,13 @@ partial def PyStmtToBoogie (jmp_targets: List String) (translation_ctx : Transla
         ([.ite guard (assign_tgt ++ (ArrPyStmtToBoogie translation_ctx body.val).fst) []], none)
       | _ => panic! s!"tgt must be single name: {repr tgt}"
       -- TODO: missing havoc
-    | .Assert _ a _ =>
+    | .Assert _ a msg =>
       let res := PyExprToBoogie translation_ctx a
-      ([(.assert "py_assertion" res.expr)], none)
+      match msg.val with
+      | .some s =>
+        ([(.assert ("py_assertion_" ++ PyExprToString s) res.expr), (.assume ("py_assertion_assume_" ++ PyExprToString s) res.expr)], none)
+      | _ =>
+        ([(.assert "py_assertion" res.expr), (.assume "py_assertion_assume" res.expr)], none)
     | .AugAssign _ lhs op rhs =>
       match op with
       | .Add _ =>

StrataMain.lean

@@ -208,7 +208,8 @@ def pyAnalyzeCommand : Command where
     let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f))
                         (Boogie.verify "z3" newPgm { Options.default with stopOnFirstError := false,
                                                                           verbose,
-                                                                          removeIrrelevantAxioms := true }
+                                                                          removeIrrelevantAxioms := false,
+                                                                          z3Options := some {options := []} }
                                                    (moreFns := Strata.Python.ReFactory))
     let mut s := ""
     for vcResult in vcResults do

StrataTest/Languages/Python/expected/test_datetime.expected

@@ -13,10 +13,10 @@ assert_opt_name_none_or_bar: verified
 
 ensures_maybe_except_none: verified
 
-py_assertion: unknown
+py_assertion_start_leq_end: verified
 
-py_assertion: unknown
+py_assertion_start_dt_eq_start: verified
 
-py_assertion: unknown
+py_assertion_end_dt_eq_end: verified
 
-py_assertion: unknown
+py_assertion_start_dt_leq_end_dt: verified

StrataTest/Languages/Python/tests/test_datetime.py

@@ -18,13 +18,13 @@
 
 # my_f_str(str(start), str(end))
 
-assert start <= end
+assert start <= end, "start_leq_end"
 
 # These require mbqi / autoconfig
 start_dt : datetime = datetime.strptime(str(start), "%Y-%m-%d")
-assert start_dt == start
+assert start_dt == start, "start_dt_eq_start"
 end_dt : datetime = datetime.strptime(str(end), "%Y-%m-%d")
-assert end_dt == end
+assert end_dt == end, "end_dt_eq_end"
 
 # This is unknown
-assert start_dt <= end_dt
+assert start_dt <= end_dt, "start_dt_leq_end_dt"