Models for relevant regular expression operations

Strata/Languages/Boogie/Boogie.lean

@@ -34,19 +34,28 @@ namespace Boogie
    types.
 -/
 
-def typeCheck (options : Options) (program : Program) : Except Std.Format Program := do
+def typeCheck (options : Options) (program : Program)
+    (moreFns : @Lambda.Factory BoogieLParams := Lambda.Factory.default) :
+    Except Std.Format Program := do
   let T := Lambda.TEnv.default
-  let C := { Lambda.LContext.default with functions := Boogie.Factory, knownTypes := Boogie.KnownTypes }
+  let factory ← Boogie.Factory.addFactory moreFns
+  let C := { Lambda.LContext.default with
+                functions := factory,
+                knownTypes := Boogie.KnownTypes }
   let (program, _T) ← Program.typeCheck C T program
   -- dbg_trace f!"[Strata.Boogie] Type variables:\n{T.state.substInfo.subst.length}"
   -- dbg_trace f!"[Strata.Boogie] Annotated program:\n{program}"
   if options.verbose then dbg_trace f!"[Strata.Boogie] Type checking succeeded.\n"
   return program
 
-def typeCheckAndPartialEval (options : Options) (program : Program) :
-  Except Std.Format (List (Program × Env)) := do
-  let program ← typeCheck options program
-  let E := { Env.init with program := program }
+def typeCheckAndPartialEval (options : Options) (program : Program)
+    (moreFns : @Lambda.Factory BoogieLParams := Lambda.Factory.default) :
+    Except Std.Format (List (Program × Env)) := do
+  let program ← typeCheck options program moreFns
+  let σ ← (Lambda.LState.init).addFactory Boogie.Factory
+  let σ ← σ.addFactory moreFns
+  let E := { Env.init with exprEnv := σ,
+                           program := program }
   let pEs := Program.eval E
   if options.verbose then do
     dbg_trace f!"{Std.Format.line}VCs:"

Strata/Languages/Boogie/Examples/FailingAssertion.lean

@@ -63,9 +63,10 @@ Proof Obligation:
 Wrote problem to vcs/assert_0.smt2.
 
 
-Obligation assert_0: solver error!
+Obligation assert_0: could not be proved!
 
-Error: Cannot find model for id: f1
+Result: failed
+CEx: ⏎
 
 Evaluated program:
 type MapII := (Map int int)
@@ -80,7 +81,8 @@ assert [assert_0] (((~select $__a0) #0) == #1)
 ---
 info:
 Obligation: assert_0
-Result: err Cannot find model for id: f1
+Result: failed
+CEx:
 -/
 #guard_msgs in
 #eval verify "cvc5" failing

Strata/Languages/Boogie/Verifier.lean

@@ -127,8 +127,13 @@ def solverResult (vars : List (IdentT LMonoTy Visibility)) (ans : String)
   match verdict with
   | "sat"     =>
     let rawModel ← getModel rest
-    let model ← processModel vars rawModel ctx E
-    .ok (.sat model)
+    -- We suppress any counterexample processing errors.
+    -- Likely, these would be because of the suboptimal implementation
+    -- of the counterexample parser, which shouldn't hold back useful
+    -- feedback (i.e., problem was `sat`) from the user.
+    match (processModel vars rawModel ctx E) with
+    | .ok model => .ok (.sat model)
+    | .error _model_err => (.ok (.sat []))
   | "unsat"   =>  .ok .unsat
   | "unknown" =>  .ok .unknown
   | _     =>  .error ans
@@ -297,8 +302,11 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
            if options.stopOnFirstError then break
     return results
 
-def verify (smtsolver : String) (program : Program) (options : Options := Options.default) : EIO Format VCResults := do
-  match Boogie.typeCheckAndPartialEval options program with
+def verify (smtsolver : String) (program : Program)
+    (options : Options := Options.default)
+    (moreFns : @Lambda.Factory BoogieLParams := Lambda.Factory.default) :
+    EIO Format VCResults := do
+  match Boogie.typeCheckAndPartialEval options program moreFns with
   | .error err =>
     .error f!"[Strata.Boogie] Type checking error: {format err}"
   | .ok pEs =>
@@ -316,12 +324,13 @@ namespace Strata
 
 open Lean.Parser
 
-def typeCheck (ictx : InputContext) (env : Program) (options : Options := Options.default) :
+def typeCheck (ictx : InputContext) (env : Program) (options : Options := Options.default)
+    (moreFns : @Lambda.Factory Boogie.BoogieLParams := Lambda.Factory.default) :
   Except Std.Format Boogie.Program := do
   let (program, errors) := TransM.run ictx (translateProgram env)
   if errors.isEmpty then
     -- dbg_trace f!"AST: {program}"
-    Boogie.typeCheck options program
+    Boogie.typeCheck options program moreFns
   else
     .error s!"DDM Transform Error: {repr errors}"
 
@@ -333,12 +342,14 @@ def Boogie.getProgram
 def verify
     (smtsolver : String) (env : Program)
     (ictx : InputContext := Inhabited.default)
-    (options : Options := Options.default) : IO Boogie.VCResults := do
+    (options : Options := Options.default)
+    (moreFns : @Lambda.Factory Boogie.BoogieLParams := Lambda.Factory.default)
+    : IO Boogie.VCResults := do
   let (program, errors) := Boogie.getProgram env ictx
   if errors.isEmpty then
     -- dbg_trace f!"AST: {program}"
     EIO.toIO (fun f => IO.Error.userError (toString f))
-                (Boogie.verify smtsolver program options)
+                (Boogie.verify smtsolver program options moreFns)
   else
     panic! s!"DDM Transform Error: {repr errors}"