137 lines
5.0 KiB
Diff
137 lines
5.0 KiB
Diff
From bfc7216250e666a59e304f3b7518f8b0bccccbae Mon Sep 17 00:00:00 2001
|
|
From: Shea Levy <shea@shealevy.com>
|
|
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 <shea@shealevy.com>
|
|
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 <shea@shealevy.com>
|
|
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)><formula>(x) = let
|
|
+ implement list_vt_map$fopr<@(s2exp,s2exp)><formula>(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)><formula> (pairs)
|
|
+ list_vt_map<(s2exp,s2exp)><formula> (pairs)
|
|
+ val () = list_vt_free(pairs)
|
|
//
|
|
implement
|
|
list_vt_fold$init<formula><formula> (x) = x
|
|
|
|
From 50de956561e6bf43190d7efb385bb6da658f1637 Mon Sep 17 00:00:00 2001
|
|
From: Shea Levy <shea@shealevy.com>
|
|
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<commarg><string> (x) =
|
|
+ list_vt_map$fopr<commarg><string> (x) =
|
|
case- x of
|
|
| Script (s) => s
|
|
//
|
|
val scriptargs = filter (list_vt_copy (args))
|
|
- val scripts = mapfree<commarg><string> (scriptargs)
|
|
+ val scripts = map<commarg><string> (scriptargs)
|
|
+ val () = list_vt_free (scriptargs)
|
|
//
|
|
implement
|
|
list_find$pred<commarg> (x) =
|