From bfc7216250e666a59e304f3b7518f8b0bccccbae Mon Sep 17 00:00:00 2001 From: Shea Levy Date: Thu, 30 Apr 2015 16:50:47 -0400 Subject: [PATCH] Add missing case in fprint_s2rt --- projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats | 1 + 1 file changed, 1 insertion(+) diff --git a/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats b/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats index a841b5f..5bc28d7 100644 --- a/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats +++ b/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats @@ -113,6 +113,7 @@ case+ s2t0 of | S2RTfun (args, ret) => fprint (out, "S2RTfun()") | S2RTtup () => fprint (out, "S2RTtup()") | S2RTerr () => fprint (out, "S2RTerr()") +| S2RTuninterp (str) => fprint! (out, "S2RTuninterp(", str, ")") // | S2RTignored () => fprint (out, "S2RTignored()") // From 9d4c7669d0d3bc8725648684391a2962ed5a922e Mon Sep 17 00:00:00 2001 From: Shea Levy Date: Thu, 30 Apr 2015 17:13:35 -0400 Subject: [PATCH] ATS-extsolve: Get rid of verbose . overload --- projects/MEDIUM/ATS-extsolve/solving/solver.dats | 2 +- projects/MEDIUM/ATS-extsolve/solving/solver.sats | 6 ------ 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/projects/MEDIUM/ATS-extsolve/solving/solver.dats b/projects/MEDIUM/ATS-extsolve/solving/solver.dats index 8446cd5..f2f77b4 100644 --- a/projects/MEDIUM/ATS-extsolve/solving/solver.dats +++ b/projects/MEDIUM/ATS-extsolve/solving/solver.dats @@ -250,7 +250,7 @@ end // end of [c3nstr_solve_main] implement c3nstr_solve (c3t, scripts, verbose) = let var env : smtenv val _ = smtenv_nil (env) - val () = env.verbose (verbose) + val () = smtenv_set_verbose(env, verbose) val () = case+ scripts of | list_nil () => () diff --git a/projects/MEDIUM/ATS-extsolve/solving/solver.sats b/projects/MEDIUM/ATS-extsolve/solving/solver.sats index e43a028..dae452c 100644 --- a/projects/MEDIUM/ATS-extsolve/solving/solver.sats +++ b/projects/MEDIUM/ATS-extsolve/solving/solver.sats @@ -39,14 +39,8 @@ fun smtenv_load_scripts (env: &smtenv, scripts: List0(string)): void fun smtenv_get_solver (env: &smtenv): solver -fun smtenv_get_verbose (env: &smtenv): bool - -overload .verbose with smtenv_get_verbose - fun smtenv_set_verbose (env: &smtenv, verbose: bool): void -overload .verbose with smtenv_set_verbose - fun formula_cst (s2c: s2cst): formula (* ****** ****** *) From e3473a8d9dc7c56cda1111a439db7123254d00b4 Mon Sep 17 00:00:00 2001 From: Shea Levy Date: Thu, 30 Apr 2015 18:09:33 -0400 Subject: [PATCH 1/2] solver_smt.dats: Don't use mapfree on linear list of non-linear values --- projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats b/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats index 04055b9..b49602d 100644 --- a/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats +++ b/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats @@ -348,7 +348,7 @@ in // val () = assertloc (length(pairs) > 0) // - implement list_vt_mapfree$fopr<@(s2exp,s2exp)>(x) = let + implement list_vt_map$fopr<@(s2exp,s2exp)>(x) = let val (pf, fpf | Env) = $UN.ptr1_vtake{smtenv}(addr@ env) val met = formula_make (!Env, x.0) val bound = formula_make (!Env, x.1) @@ -362,7 +362,8 @@ in end // val assertions = - list_vt_mapfree<(s2exp,s2exp)> (pairs) + list_vt_map<(s2exp,s2exp)> (pairs) + val () = list_vt_free(pairs) // implement list_vt_fold$init (x) = x From 50de956561e6bf43190d7efb385bb6da658f1637 Mon Sep 17 00:00:00 2001 From: Shea Levy Date: Thu, 30 Apr 2015 18:18:56 -0400 Subject: [PATCH 2/2] ats-extsolve/main.dats: Don't use mapfree on linear list of non-linear values --- projects/MEDIUM/ATS-extsolve/main.dats | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/projects/MEDIUM/ATS-extsolve/main.dats b/projects/MEDIUM/ATS-extsolve/main.dats index ac30ca0..930697d 100644 --- a/projects/MEDIUM/ATS-extsolve/main.dats +++ b/projects/MEDIUM/ATS-extsolve/main.dats @@ -34,7 +34,7 @@ dynload "commarg.dats" (* ****** ****** *) -overload mapfree with list_vt_mapfree +overload map with list_vt_map overload filter with list_vt_filter (* ****** ****** *) @@ -56,12 +56,13 @@ implement main0 (argc, argv) = let | Script (s) => true | _ =>> false implement - list_vt_mapfree$fopr (x) = + list_vt_map$fopr (x) = case- x of | Script (s) => s // val scriptargs = filter (list_vt_copy (args)) - val scripts = mapfree (scriptargs) + val scripts = map (scriptargs) + val () = list_vt_free (scriptargs) // implement list_find$pred (x) =