<commit_before>/// The part of the Z3 backend that translates terms to Z3.
module Starling.Backends.Z3

open Microsoft
open Chessie.ErrorHandling
open Starling
open Starling.Collections
open Starling.Core.Expr
open Starling.Core.Var
open Starling.Core.Model
open Starling.Core.GuardedView
open Starling.Core.Instantiate
open Starling.Core.Sub
open Starling.Core.Z3
open Starling.Reifier
open Starling.Optimiser


/// <summary>
///     Types for the Z3 backend, including errors.
/// </summary>
[<AutoOpen>]
module Types =
    // A Z3-reified term.
    type ZTerm = Term<Z3.BoolExpr, Z3.BoolExpr, Z3.BoolExpr>

    /// Type of requests to the Z3 backend.
    type Request =
        /// Only translate the term views; return `Response.Translate`.
        | Translate
        /// Translate and combine term Z3 expressions; return `Response.Combine`.
        | Combine
        /// Translate, combine, and run term Z3 expressions; return `Response.Sat`.
        | Sat
        /// Produce a MuZ3 model; return `Response.MuTranslate`.
        | MuTranslate
        /// Produce a MuZ3 fixedpoint; return `Response.MuFix`.
        | MuFix
        /// Produce a MuZ3 sat list; return `Response.MuSat`.
        | MuSat

    /// <summary>
    ///     Type of MuZ3 results.
    /// </summary>
    type MuSat =
        /// <summary>
        ///     The proof succeeded with the <c>FuncDecl</c> being assigned
        ///     with the given <c>Expr</c>.
        /// </summary>
        | Sat of Z3.Expr
        /// <summary>
        ///     The proof failed with the assignments of the <c>FuncDecl</c>s
        ///     given by the <c>Expr</c>.
        /// </summary>
        | Unsat of Z3.Expr
        /// <summary>
        ///     The proof gave an odd result.
        /// </summary>
        | Unknown of reason: string

    /// <summary>
    ///     A MuZ3 model.
    /// </summary>
    type MuModel =
        { /// <summary>
          ///     List of definite viewdefs, as (view, def) pairs, to check.
          /// </summary>
          Definites : (VFunc * BoolExpr) list
          /// <summary>
          ///     Map of (view name, FuncDecl) bindings.
          /// </summary>
          FuncDecls : Map<string, Z3.FuncDecl>
          /// <summary>
          ///     List of fixedpoint rules.
          /// </summary>
          Rules : Map<string, Z3.BoolExpr> }

    /// Type of responses from the Z3 backend.
    [<NoComparison>]
    type Response =
        /// Output of the term translation step only.
        | Translate of Model<ZTerm, DFunc>
        /// Output of the final Z3 terms only.
        | Combine of Model<Z3.BoolExpr, DFunc>
        /// Output of satisfiability reports for the Z3 terms.
        | Sat of Map<string, Z3.Status>
        /// Output of the MuZ3 translation step only.
        | MuTranslate of MuModel
        /// Output of the MuZ3 fixedpoint generation step only.
        | MuFix of fixedpoint : Z3.Fixedpoint * unsafe : Z3.FuncDecl
        /// Output of the MuZ3 proof.
        | MuSat of MuSat

    /// A Z3 translation error.
    type Error =
        /// The translator was given an indefinite constraint.
        /// The Z3 backend cannot handle indefinite constraints.
        | IndefiniteConstraint of viewdef: DFunc
        /// Instantiation of a view failed.
        | InstantiationError of view: VFunc
                              * details: Starling.Core.Instantiate.Types.Error


/// <summary>
///     Pretty printers for the Z3 types.
/// </summary>
module Pretty =            
    open Starling.Core.Pretty
    open Starling.Core.Expr.Pretty
    open Starling.Core.Model.Pretty
    open Starling.Core.Instantiate.Pretty
    open Starling.Core.Z3.Pretty

    /// Pretty-prints a MuSat.
    let printMuSat =
        function
        | MuSat.Sat ex -> colonSep [ String "sat" ; printZ3Exp ex ]
        | MuSat.Unsat ex -> colonSep [ String "unsat" ; printZ3Exp ex ]
        | MuSat.Unknown reason -> colonSep [ String "unknown" ; String reason ]
    
    /// Pretty-prints a MuModel.
    let printMuModel { Definites = ds ; Rules = rs ; FuncDecls = fdm } =
        printAssoc
            Indented
            [ (String "Definites",
               ds |>
               List.map (fun (f, d) -> equality (printVFunc f)
                                                (printBoolExpr d))
               |> vsep)
              (String "Rules",
               rs
               |> Map.toSeq
               |> Seq.map (fun (g, sym) ->
                               commaSep [ String (sym.ToString())
                                          String (g.ToString()) ] )
               |> vsep)
              (String "Goals",
               printMap Inline String (fun s -> String (s.ToString())) fdm) ]

    /// Pretty-prints a response.
    let printResponse mview =
        function
        | Response.Translate m ->
            printModelView
                mview
                (printTerm printZ3Exp printZ3Exp printZ3Exp)
                printDFunc
                m<commit_msg>Make muZ3 output easier to read.<commit_after>/// The part of the Z3 backend that translates terms to Z3.
module Starling.Backends.Z3

open Microsoft
open Chessie.ErrorHandling
open Starling
open Starling.Collections
open Starling.Core.Expr
open Starling.Core.Var
open Starling.Core.Model
open Starling.Core.GuardedView
open Starling.Core.Instantiate
open Starling.Core.Sub
open Starling.Core.Z3
open Starling.Reifier
open Starling.Optimiser


/// <summary>
///     Types for the Z3 backend, including errors.
/// </summary>
[<AutoOpen>]
module Types =
    // A Z3-reified term.
    type ZTerm = Term<Z3.BoolExpr, Z3.BoolExpr, Z3.BoolExpr>

    /// Type of requests to the Z3 backend.
    type Request =
        /// Only translate the term views; return `Response.Translate`.
        | Translate
        /// Translate and combine term Z3 expressions; return `Response.Combine`.
        | Combine
        /// Translate, combine, and run term Z3 expressions; return `Response.Sat`.
        | Sat
        /// Produce a MuZ3 model; return `Response.MuTranslate`.
        | MuTranslate
        /// Produce a MuZ3 fixedpoint; return `Response.MuFix`.
        | MuFix
        /// Produce a MuZ3 sat list; return `Response.MuSat`.
        | MuSat

    /// <summary>
    ///     Type of MuZ3 results.
    /// </summary>
    type MuSat =
        /// <summary>
        ///     The proof succeeded with the <c>FuncDecl</c> being assigned
        ///     with the given <c>Expr</c>.
        /// </summary>
        | Sat of Z3.Expr
        /// <summary>
        ///     The proof failed with the assignments of the <c>FuncDecl</c>s
        ///     given by the <c>Expr</c>.
        /// </summary>
        | Unsat of Z3.Expr
        /// <summary>
        ///     The proof gave an odd result.
        /// </summary>
        | Unknown of reason: string

    /// <summary>
    ///     A MuZ3 model.
    /// </summary>
    type MuModel =
        { /// <summary>
          ///     List of definite viewdefs, as (view, def) pairs, to check.
          /// </summary>
          Definites : (VFunc * BoolExpr) list
          /// <summary>
          ///     Map of (view name, FuncDecl) bindings.
          /// </summary>
          FuncDecls : Map<string, Z3.FuncDecl>
          /// <summary>
          ///     List of fixedpoint rules.
          /// </summary>
          Rules : Map<string, Z3.BoolExpr> }

    /// Type of responses from the Z3 backend.
    [<NoComparison>]
    type Response =
        /// Output of the term translation step only.
        | Translate of Model<ZTerm, DFunc>
        /// Output of the final Z3 terms only.
        | Combine of Model<Z3.BoolExpr, DFunc>
        /// Output of satisfiability reports for the Z3 terms.
        | Sat of Map<string, Z3.Status>
        /// Output of the MuZ3 translation step only.
        | MuTranslate of MuModel
        /// Output of the MuZ3 fixedpoint generation step only.
        | MuFix of fixedpoint : Z3.Fixedpoint * unsafe : Z3.FuncDecl
        /// Output of the MuZ3 proof.
        | MuSat of MuSat

    /// A Z3 translation error.
    type Error =
        /// The translator was given an indefinite constraint.
        /// The Z3 backend cannot handle indefinite constraints.
        | IndefiniteConstraint of viewdef: DFunc
        /// Instantiation of a view failed.
        | InstantiationError of view: VFunc
                              * details: Starling.Core.Instantiate.Types.Error


/// <summary>
///     Pretty printers for the Z3 types.
/// </summary>
module Pretty =            
    open Starling.Core.Pretty
    open Starling.Core.Expr.Pretty
    open Starling.Core.Model.Pretty
    open Starling.Core.Instantiate.Pretty
    open Starling.Core.Z3.Pretty

    /// Pretty-prints a MuSat.
    let printMuSat =
        function
        | MuSat.Sat ex -> vsep [ String "Proof FAILED."
                                 headed "Counter-example" [ printZ3Exp ex ] ]
        | MuSat.Unsat ex -> vsep [ String "Proof SUCCEEDED."
                                   headed "View assignments" [ printZ3Exp ex ] ]
        | MuSat.Unknown reason -> colonSep [ String "Proof status unknown"
                                             String reason ]
    
    /// Pretty-prints a MuModel.
    let printMuModel { Definites = ds ; Rules = rs ; FuncDecls = fdm } =
        printAssoc
            Indented
            [ (String "Definites",
               ds |>
               List.map (fun (f, d) -> equality (printVFunc f)
                                                (printBoolExpr d))
               |> vsep)
              (String "Rules",
               rs
               |> Map.toSeq
               |> Seq.map (fun (g, sym) ->
                               commaSep [ String (sym.ToString())
                                          String (g.ToString()) ] )
               |> vsep)
              (String "Goals",
               printMap Inline String (fun s -> String (s.ToString())) fdm) ]

    /// Pretty-prints a response.
    let printResponse mview =
        function
        | Response.Translate m ->
            printModelView
                mview
                (printTerm printZ3Exp printZ3Exp printZ3Exp)
                printDFunc
                m
{'fraction_non_alphanumeric': 0.10607097467983186, 'fraction_numerical': 0.007918662625867632, 'mean_word_length': 1.5215676608331279, 'pattern_counts': {'":': 0, '<': 75, '<?xml version=': 0, '>': 99, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5578015', 'n_tokens_mistral': 2910, 'n_tokens_neox': 2800, 'n_words': 897}