Tractables/Dice.jl

uncomment

Closed this issue · 1 comments

github-actions commented

println_flush(rs.io, "Saving samples...")

time_sample = @Elapsed with_concrete_ad_flips(rs.var_vals, g.e) do

save_samples(rs, joinpath(rs.out_dir, "terms_$(s).txt"), g.e)

end

println(rs.io, " $(time_sample) seconds")

println(rs.io)

Dice.jl/examples/qc/benchmarks/benchmarks.jl

Line 376 in a5fe094

# TODO: uncomment 

##################################

abstract type STLC <: Benchmark end
function sandwich(::Type{STLC})
    (
        "From QuickChick Require Import QuickChick. Import QcNotation.
From Coq Require Import Bool ZArith List. Import ListNotations.
From ExtLib Require Import Monad.
From ExtLib.Data.Monads Require Import OptionMonad.
Import MonadNotation.

From STLC Require Import Impl Spec.",
"Definition test_prop_SinglePreserve :=
forAll gSized (fun (e: Expr) =>
  prop_SinglePreserve e).

(*! QuickChick test_prop_SinglePreserve. *)

Definition test_prop_MultiPreserve :=
forAll gSized (fun (e: Expr) =>
  prop_MultiPreserve e).

(*! QuickChick test_prop_MultiPreserve. *)
          "
    )
end


struct STLCGeneration <: Generation{STLC}
    e::Opt.T{Expr.T}
    constructors_overapproximation::Vector{Opt.T{Expr.T}}
end
function generation_emit_stats(rs::RunState, g::STLCGeneration, s::String)
    # TODO: uncomment
    # println_flush(rs.io, "Saving samples...")
    # time_sample = @elapsed with_concrete_ad_flips(rs.var_vals, g.e) do
    #     save_samples(rs, joinpath(rs.out_dir, "terms_$(s).txt"), g.e)
    # end
    # println(rs.io, "  $(time_sample) seconds")
    # println(rs.io)
end
value(g::STLCGeneration) = g.e