Skip to content

Commit

Permalink
Fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@Halbaroth
Halbaroth committed Oct 13, 2023
1 parent f252ff7 commit 48079c6
Show file tree
Hide file tree
Showing 3 changed files with 52 additions and 31 deletions.
9 changes: 7 additions & 2 deletions src/lib/reasoners/intervalCalculus.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2045,11 +2045,13 @@ let case_split env uf ~for_model =
| _ -> res

let optimizing_split env uf opt_split =
Fmt.pr "DEBUG: %a@." Expr.print opt_split.Th_util.e;
if not @@ is_num_term opt_split.Th_util.e then
(* Some other theory should find an optimium value for e. *)
None
else
begin
(* TODO: move this comment. *)
(* soundness: if there are expressions to optmize, this should be
done without waiting for ~for_model flag to be true *)
let {Th_util.order; r = r; is_max = to_max; e; value } = opt_split in
Expand Down Expand Up @@ -2096,8 +2098,7 @@ let optimizing_split env uf opt_split =
in
Some { opt_split with value }

| Sim.Core.Max(mx,_sol) ->
let {Sim.Core.max_v; _} = Lazy.force mx in
| Sim.Core.Max (lazy Sim.Core.{ max_v; is_le = true }, _sol) ->
let max_p = Q.add max_v.bvalue.v c in
let optim = if to_max then max_p else Q.mult Q.m_one max_p in
Printer.print_dbg "%a has a %s: %a@."
Expand All @@ -2115,6 +2116,10 @@ let optimizing_split env uf opt_split =
LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one)
in
Some { opt_split with value = Value s; }

| Sim.Core.Max (lazy Sim.Core.{ is_le = false; _ }, _) ->
(* There is no upper bound as it's a large bound. *)
None
end
end
(*** part dedicated to FPA reasoning ************************************)
Expand Down
2 changes: 1 addition & 1 deletion src/lib/reasoners/satml_frontend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1063,7 +1063,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
| Value _ ->
assert false
| Unknown ->
assert false
seen_infinity := true; acc
) obj []
in
begin match acc with
Expand Down
72 changes: 44 additions & 28 deletions src/lib/reasoners/theory.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -428,42 +428,58 @@ module Main_Default : S = struct
| Th_util.Unknown -> acc (* not optimized yet *)
| Value _ -> Util.MI.add ord {v with value = Unknown} acc
| Pinfinity | Minfinity -> assert false (* may happen? *)
)objectives objectives
) objectives objectives

let look_for_sat ?(bad_last=None) ch env l ~for_model =
let rec aux ch bad_last dl env li =
let rec aux ~optimize ch bad_last dl env li =
Options.exec_thread_yield ();
match li, bad_last with
| [], _ ->
begin
Options.tool_req 3 "TR-CCX-CS-Case-Split";
match next_optimization ~for_model env with
| Some opt_split ->
begin
let opt_split =
if optimize then
match next_optimization ~for_model env with
| Some opt_split ->
begin
match CC_X.optimizing_split env.gamma_finite opt_split with
| Some x -> x
| Some x ->
let to_opt =
register_optimized_split env.objectives x
in
let env = {env with objectives = to_opt} in
begin
match opt_split.value with
| Value v ->
let splits = add_explanations_to_splits [v] in
aux ~optimize ch None dl env splits
| Pinfinity | Minfinity ->
if for_model then
aux ~optimize:false ch None dl env []
else
{ env with choices = List.rev dl }, ch
| Unknown -> assert false
end
| None ->
(* At least one theory should be able to optimize the
split. *)
assert false
in
let to_opt = register_optimized_split env.objectives opt_split in
let env = {env with objectives = to_opt} in
begin
match opt_split.value with
| Value v ->
let splits = add_explanations_to_splits [v] in
aux ch None dl env splits
| Pinfinity | Minfinity ->
if for_model then
aux ch None dl env []
aux ~optimize:false ch None dl env []
else
{ env with choices = List.rev dl }, ch
| Unknown -> assert false
end
end
| None ->
| None ->
begin
let l, base_env =
CC_X.case_split env.gamma_finite ~for_model
in
let env = {env with gamma_finite = base_env} in
match l with
| [] ->
{ env with choices = List.rev dl }, ch

| _ ->
let l = add_explanations_to_splits l in
aux ~optimize ch None dl env l
end
else
begin
let l, base_env =
CC_X.case_split env.gamma_finite ~for_model
Expand All @@ -475,15 +491,15 @@ module Main_Default : S = struct

| _ ->
let l = add_explanations_to_splits l in
aux ch None dl env l
aux ~optimize ch None dl env l
end
end
| ((c, lit_orig, CNeg, ex_c) as a)::l, _ ->
let facts = CC_X.empty_facts () in
CC_X.add_fact facts (LSem c,ex_c,lit_orig);
let base_env, ch = CC_X.assume_literals env.gamma_finite ch facts in
let env = { env with gamma_finite = base_env} in
aux ch bad_last (a::dl) env l
aux ~optimize ch bad_last (a::dl) env l

(* This optimisation is not correct with the current explanation *)
(* | [(c, lit_orig, CPos exp, ex_c)], Yes (dep,_) -> *)
Expand All @@ -500,7 +516,7 @@ module Main_Default : S = struct
let base_env, ch = CC_X.assume_literals env.gamma_finite ch facts in
let env = { env with gamma_finite = base_env} in
Options.tool_req 3 "TR-CCX-CS-Normal-Run";
aux ch bad_last (a::dl) env l
aux ~optimize ch bad_last (a::dl) env l
with Ex.Inconsistent (dep, classes) ->
match Ex.remove_fresh exp dep with
| None ->
Expand All @@ -524,9 +540,9 @@ module Main_Default : S = struct
let env =
{ env with objectives =
partial_objectives_reset env.objectives is_opt } in
aux ch None dl env [neg_c, lit_orig, CNeg, dep]
aux ~optimize ch None dl env [neg_c, lit_orig, CNeg, dep]
in
aux ch bad_last (List.rev env.choices) env l
aux ~optimize:true ch bad_last (List.rev env.choices) env l

(* remove old choices involving fresh variables that are no longer in UF *)
let filter_valid_choice uf (ra,_,_,_) =
Expand Down

0 comments on commit 48079c6

Please sign in to comment.