Skip to content

Commit

Permalink
solver: Move OpamBuiltinZ3.Syntax to a new OpamCudfCriteria module
Browse files Browse the repository at this point in the history
  • Loading branch information
kit-ty-kate authored and rjbou committed Aug 20, 2024
1 parent 6a212c3 commit d8683ec
Show file tree
Hide file tree
Showing 5 changed files with 142 additions and 86 deletions.
2 changes: 2 additions & 0 deletions doc/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -198,6 +198,8 @@ <h1>opam %{OPAMVERSION}% API and libraries documentation</h1>
<td>Configuration options for this lib (record, global reference, setter, initialisation)</td></tr>
<tr><th><a href="opam-solver/OpamActionGraph">opamActionGraph.ml</a></th>
<td>Handles graphs of actions (package changes), based on ocamlgraph</td></tr>
<tr><th><a href="opam-solver/OpamCudfCriteria">opamCudfCriteria.ml</a></th>
<td>Cudf criteria helper functions (string conversion, etc.)</td></tr>
<tr><th><a href="opam-solver/OpamCudfSolver">opamCudfSolver.ml</a></th>
<td>Bindings to implementation of CUDF solvers, either built-in or external</td></tr>
<tr><th><a href="opam-solver/OpamCudf">opamCudf.ml</a></th>
Expand Down
1 change: 1 addition & 0 deletions master_changes.md
Original file line number Diff line number Diff line change
Expand Up @@ -211,6 +211,7 @@ users)
* `OpamStateConfig.opamroot_with_provenance`: restore previous behaviour to `OpamStateConfig.opamroot` for compatibility with third party code [#6047 @dra27]

## opam-solver
* `OpamCudfCriteria`, `OpamBuiltinZ3.Syntax`: Move `OpamBuiltinZ3.Syntax` into a dedicated module `OpamCudfCriteria` [#6130 @kit-ty-kate]

## opam-format
* Add `OpamTypesBase.switch_selections_{compare,equal}`: proper comparison functions for `OpamTypes.switch_selections` [#6102 @kit-ty-kate]
Expand Down
89 changes: 3 additions & 86 deletions src/solver/opamBuiltinZ3.real.ml
Original file line number Diff line number Diff line change
Expand Up @@ -273,17 +273,10 @@ let sum ctx (_, universe, _) filter value =
[]
universe

type filter = Installed | Changed | Removed | New |
Upgraded | Downgraded | Requested
type property = string option
type sign = Plus | Minus

type criterion = sign * filter * property

let def_criterion ctx opt (preamble, universe, request as cudf)
(sign, filter, property : criterion) =
(sign, filter, property : OpamCudfCriteria.criterion) =
let filter_f = match filter with
| Installed -> fun p -> psym ctx p
| Installed | Solution -> fun p -> psym ctx p
| Changed ->
fun p ->
if p.Cudf.installed then
Expand Down Expand Up @@ -367,82 +360,6 @@ let def_criterion ctx opt (preamble, universe, request as cudf)
let def_criteria ctx opt cudf crits =
List.iter (def_criterion ctx opt cudf) crits

module Syntax = struct

let criterion_of_string (s,params) =
let sign = match s.[0] with
| '+' -> Plus
| '-' -> Minus
| c -> failwith (Printf.sprintf "criteria_of_string sign=%c" c)
| exception Invalid_argument _ ->
failwith "criteria_of_string sign=EOF"
in
let s = String.sub s 1 (String.length s - 1) in
let subset_of_string = function
| "new" -> New
| "removed" -> Removed
| "changed" -> Changed
| "up" -> Upgraded
| "down" -> Downgraded
| "installed" | "solution" -> Installed
| "request" -> Requested
| s -> failwith ("criteria_of_string subset="^s)
in
match s, params with
| "count", [field; subset] ->
sign, subset_of_string subset, Some field
| s, [] -> sign, subset_of_string s, None
| s, _ -> failwith ("criteria_of_string s="^s)
(*
let string_of_criterion (sign, filter, property: criterion) =
Printf.sprintf "%c%s%s"
(match sign with Plus -> '+' | Minus -> '-')
(match filter with
| Installed -> "installed"
| Changed -> "changed"
| Removed -> "removed"
| New -> "new"
| Upgraded -> "up"
| Downgraded -> "down"
| Requested -> "request")
(match property with None -> "" | Some p -> "["^p^"]")
*)
let criteria_of_string s =
let start = ref 0 in
let crits = ref [] in
let params = ref None in
for i = 0 to String.length s - 1 do
match s.[i] with
| ',' ->
let sub = String.sub s !start (i - !start) in
start := i + 1;
if sub <> "" then
(match !params with
| None -> crits := (sub, []) :: !crits
| Some (name, ps) -> params := Some (name, sub :: ps))
| '[' ->
let sub = String.sub s !start (i - !start) in
start := i + 1;
if !params <> None then failwith "criteria_of_string";
params := Some (sub, [])
| ']' ->
let sub = String.sub s !start (i - !start) in
start := i + 1;
(match !params with
| None -> failwith "criteria_of_string"
| Some (name, ps) ->
params := None;
crits := (name, List.rev (sub::ps)) :: !crits)
| _ -> ()
done;
if !start < String.length s then
crits := (String.sub s !start (String.length s - !start), []) :: !crits;
if !params <> None then failwith "criteria_of_string";
let r = List.rev_map criterion_of_string !crits in
r

end

let extract_solution_packages universe opt =
match Z3.Optimize.get_model opt with
| Some model ->
Expand Down Expand Up @@ -485,7 +402,7 @@ let call ~criteria ?timeout (preamble, universe, _ as cudf) =
log "Generating optimization criteria";
let opt = Z3.Optimize.mk_opt ctx.z3 in
let _criteria_def_handles =
def_criteria ctx opt cudf (Syntax.criteria_of_string criteria)
def_criteria ctx opt cudf (OpamCudfCriteria.of_string criteria)
in
log "Sending the problem to Z3";
let params =
Expand Down
99 changes: 99 additions & 0 deletions src/solver/opamCudfCriteria.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
(**************************************************************************)
(* *)
(* Copyright 2017-2019 OCamlPro *)
(* *)
(* All rights reserved. This file is distributed under the terms of the *)
(* GNU Lesser General Public License version 2.1, with the special *)
(* exception on linking described in the file LICENSE. *)
(* *)
(**************************************************************************)

type filter =
| Installed
| Solution
| Changed
| Removed
| New
| Upgraded
| Downgraded
| Requested

type property = string option

type sign = Plus | Minus

type criterion = sign * filter * property

let criterion_of_string (s,params) =
let sign = match s.[0] with
| '+' -> Plus
| '-' -> Minus
| c -> failwith (Printf.sprintf "criteria_of_string sign=%c" c)
| exception Invalid_argument _ ->
failwith "criteria_of_string sign=EOF"
in
let s = String.sub s 1 (String.length s - 1) in
let subset_of_string = function
| "new" -> New
| "removed" -> Removed
| "changed" -> Changed
| "up" -> Upgraded
| "down" -> Downgraded
| "installed" -> Installed
| "solution" -> Solution
| "request" -> Requested
| s -> failwith ("criteria_of_string subset="^s)
in
match s, params with
| "count", [field; subset] ->
sign, subset_of_string subset, Some field
| s, [] -> sign, subset_of_string s, None
| s, _ -> failwith ("criteria_of_string s="^s)

let criterion_to_string (sign, filter, property: criterion) =
Printf.sprintf "%c%s%s"
(match sign with Plus -> '+' | Minus -> '-')
(match filter with
| Installed -> "installed"
| Solution -> "solution"
| Changed -> "changed"
| Removed -> "removed"
| New -> "new"
| Upgraded -> "up"
| Downgraded -> "down"
| Requested -> "request")
(match property with None -> "" | Some p -> "["^p^"]")

let of_string s =
let start = ref 0 in
let crits = ref [] in
let params = ref None in
for i = 0 to String.length s - 1 do
match s.[i] with
| ',' ->
let sub = String.sub s !start (i - !start) in
start := i + 1;
if sub <> "" then
(match !params with
| None -> crits := (sub, []) :: !crits
| Some (name, ps) -> params := Some (name, sub :: ps))
| '[' ->
let sub = String.sub s !start (i - !start) in
start := i + 1;
if !params <> None then failwith "criteria_of_string";
params := Some (sub, [])
| ']' ->
let sub = String.sub s !start (i - !start) in
start := i + 1;
(match !params with
| None -> failwith "criteria_of_string"
| Some (name, ps) ->
params := None;
crits := (name, List.rev (sub::ps)) :: !crits)
| _ -> ()
done;
if !start < String.length s then
crits := (String.sub s !start (String.length s - !start), []) :: !crits;
if !params <> None then failwith "criteria_of_string";
let r = List.rev_map criterion_of_string !crits in
r
37 changes: 37 additions & 0 deletions src/solver/opamCudfCriteria.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
(**************************************************************************)
(* *)
(* Copyright 2017-2019 OCamlPro *)
(* *)
(* All rights reserved. This file is distributed under the terms of the *)
(* GNU Lesser General Public License version 2.1, with the special *)
(* exception on linking described in the file LICENSE. *)
(* *)
(**************************************************************************)

(** Cudf criteria helpers *)

(* {2 Criterion types} *)
type filter =
| Installed
| Solution
| Changed
| Removed
| New
| Upgraded
| Downgraded
| Requested

type property = string option

type sign = Plus | Minus

type criterion = sign * filter * property

(* {2 String conversion} *)

val criterion_to_string : criterion -> string

(** [of_string s] Parses the string [s] as a CUDF optimization criteria.
@raise {!Stdlib.Failure} if the string is invalid *)
val of_string : string -> criterion list

0 comments on commit d8683ec

Please sign in to comment.