From c34e648148265a2cd358294b2dac82551e0519d7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 5 Nov 2022 22:40:22 -0400 Subject: [PATCH] feat(cdsat): use `Vars_to_decide` to decide in main outer loop --- src/cdsat/TVar.ml | 4 +++ src/cdsat/TVar.mli | 4 +++ src/cdsat/core.ml | 50 ++++++++++++++++++++++++++++++++--- src/cdsat/plugin_bool.ml | 3 +++ src/cdsat/solver.ml | 7 +++++ src/core-logic/t_builtins.ml | 2 +- src/core-logic/t_builtins.mli | 4 +-- 7 files changed, 67 insertions(+), 7 deletions(-) diff --git a/src/cdsat/TVar.ml b/src/cdsat/TVar.ml index 0d62b2e0..a67c08d2 100644 --- a/src/cdsat/TVar.ml +++ b/src/cdsat/TVar.ml @@ -129,6 +129,10 @@ let pp (self : store) out (v : t) : unit = (Term.pp_limit ~max_depth:5 ~max_nodes:30) t +module Tbl = Util.Int_tbl +module Set = Util.Int_set +module Map = Util.Int_map + module Internal = struct let create (self : store) (t : Term.t) ~theory_view : t = assert (not @@ Term.Weak_map.mem self.of_term t); diff --git a/src/cdsat/TVar.mli b/src/cdsat/TVar.mli index b1a8dc5b..b16235b3 100644 --- a/src/cdsat/TVar.mli +++ b/src/cdsat/TVar.mli @@ -65,6 +65,10 @@ val pop_new_var : store -> t option val pp : store -> t Fmt.printer +module Tbl : CCHashtbl.S with type key = t +module Set : CCSet.S with type elt = t +module Map : CCMap.S with type key = t + (**/**) module Internal : sig diff --git a/src/cdsat/core.ml b/src/cdsat/core.ml index e27c7e15..ae32acbd 100644 --- a/src/cdsat/core.ml +++ b/src/cdsat/core.ml @@ -27,6 +27,7 @@ type t = { trail: Trail.t; plugins: plugin Vec.t; term_to_var: Term_to_var.t; + vars_to_decide: Vars_to_decide.t; pending_assignments: pending_assignment Vec.t; mutable last_res: Check_res.t option; proof_tracer: Proof.Tracer.t; @@ -69,6 +70,7 @@ let create ?(stats = Stat.create ()) ~arg tst vst ~proof_tracer () : t = plugins = Vec.create (); pending_assignments = Vec.create (); term_to_var = Term_to_var.create vst; + vars_to_decide = Vars_to_decide.create (); last_res = None; proof_tracer; n_restarts = Stat.mk_int stats "cdsat.restarts"; @@ -116,6 +118,7 @@ let pop_levels (self : t) n : unit = trail; plugins; term_to_var = _; + vars_to_decide = _; pending_assignments; last_res = _; proof_tracer = _; @@ -183,7 +186,7 @@ let perform_pending_assignments (self : t) : unit = | Some _value' -> (* conflict should only occur on booleans since they're the only propagation-able variables *) - assert (Term.is_a_bool (TVar.term self.vst v)); + assert (Term.has_ty_bool (TVar.term self.vst v)); Log.debugf 0 (fun k -> k "TODO: conflict (incompatible values for %a)" (TVar.pp self.vst) v); raise_conflict @@ -222,6 +225,41 @@ let propagate (self : t) : Conflict.t option = None with E_conflict c -> Some c +(* TODO *) +let make_sat_res (_self : t) : Check_res.sat_result = + { + Check_res.get_value = (fun _ -> assert false); + iter_classes = (fun _ -> assert false); + eval_lit = (fun _ -> assert false); + iter_true_lits = (fun _ -> assert false); + } + +let rec decide (self : t) : [ `Decided | `Full_model ] = + match Vars_to_decide.pop_next self.vars_to_decide with + | None -> `Full_model + | Some v -> + if TVar.has_value self.vst v then + decide self + else ( + (* try to find a plugin that can decide [v] *) + Log.debugf 20 (fun k -> k "(@[cdsat.decide@ %a@])" (TVar.pp self.vst) v); + + let exception Decided of Value.t in + try + iter_plugins self ~f:(fun (P p) -> + match p.decide p.st v with + | Some value -> raise_notrace (Decided value) + | None -> ()); + + Error.errorf "no plugin can decide %a" (TVar.pp self.vst) v + with Decided value -> + Trail.push_level self.trail; + let level = Trail.n_levels self.trail in + Log.debugf 5 (fun k -> k "(@[cdsat.new-level %d@])" level); + assign self v ~value ~level ~reason:(Reason.decide level); + `Decided + ) + let solve ~on_exit ~on_progress ~should_stop ~assumptions (self : t) : Check_res.t = let@ () = Profile.with_ "cdsat.solve" in @@ -254,9 +292,13 @@ let solve ~on_exit ~on_progress ~should_stop ~assumptions (self : t) : (* TODO: see if we want to restart *) assert false | None -> - Log.debugf 0 (fun k -> k "TODO: decide"); - (* TODO: decide *) - ()); + (match decide self with + | `Decided -> () + | `Full_model -> + let sat = make_sat_res self in + + res := Check_res.Sat sat; + continue := false)); (* regularly check if it's time to stop *) if !n_conflicts mod 64 = 0 then diff --git a/src/cdsat/plugin_bool.ml b/src/cdsat/plugin_bool.ml index 2e735040..1eb531d4 100644 --- a/src/cdsat/plugin_bool.ml +++ b/src/cdsat/plugin_bool.ml @@ -27,6 +27,9 @@ let decide (self : t) (v : TVar.t) : Value.t option = | T_and _ | T_or _ -> (* TODO: phase saving? or is it done directly in the core? *) Some (Term.true_ self.tst) + | _ when Term.has_ty_bool (TVar.term self.vst v) -> + (* TODO: phase saving? or is it done directly in the core? *) + Some (Term.true_ self.tst) | _ -> None let propagate (self : t) (act : Core.Plugin_action.t) (v : TVar.t) diff --git a/src/cdsat/solver.ml b/src/cdsat/solver.ml index 9560cccc..99728b09 100644 --- a/src/cdsat/solver.ml +++ b/src/cdsat/solver.ml @@ -41,6 +41,13 @@ let[@inline] vst self = self.vst let add_ty (_self : t) ~ty:_ : unit = () +(* TODO: + when asserting [t], we convert it into [v]. + At that point we need to add [v] and its sub-variables (recursively) + to the [Core.t], so it can itself add them to [Vars_to_decide.t]. + + Sub-variables of asserted terms are what needs to be decided. *) + let assert_term_ (self : t) (t : Term.t) pr : unit = Log.debugf 50 (fun k -> k "(@[cdsat.core.assert@ %a@])" Term.pp t); let sign, t = Term.abs self.tst t in diff --git a/src/core-logic/t_builtins.ml b/src/core-logic/t_builtins.ml index 45e65451..d0e96736 100644 --- a/src/core-logic/t_builtins.ml +++ b/src/core-logic/t_builtins.ml @@ -126,7 +126,7 @@ let is_bool t = | E_const { c_view = C_bool; _ } -> true | _ -> false -let[@inline] is_a_bool t = is_bool (ty t) +let[@inline] has_ty_bool t = is_bool (ty t) let is_true t = match view t with diff --git a/src/core-logic/t_builtins.mli b/src/core-logic/t_builtins.mli index 4d865507..4cc2d3b5 100644 --- a/src/core-logic/t_builtins.mli +++ b/src/core-logic/t_builtins.mli @@ -29,8 +29,8 @@ val is_eq : t -> bool val is_bool : t -> bool (** [is_bool t] is true if [t] is the type bool itself *) -val is_a_bool : t -> bool -(** [is_a_bool t] is true if [t] has type [bool] *) +val has_ty_bool : t -> bool +(** [has_ty_bool t] is true if [t] has type [bool] *) val is_true : t -> bool val is_false : t -> bool