simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-05 19:00:33 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(cdsat): decide new variables

Browse source
This commit is contained in:
Simon Cruanes 2022-11-06 22:37:10 -05:00
parent 3412b272fb
commit f2a7489d39
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 15 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/cdsat/core.ml
View file

@ -187,8 +187,21 @@ let pop_levels (self : t) n : unit =
let[@inline] get_term_to_var self = self.term_to_var
let[@inline] term_to_var self t : TVar.t =
Term_to_var.convert self.term_to_var t
let term_to_var self t : TVar.t =
(* TODO: simplify [t] *)
let v = Term_to_var.convert self.term_to_var t in
(* add new variables to vars_to_decide *)
while
match TVar.pop_new_var self.vst with
| None -> false
| Some v ->
Vars_to_decide.add self.vars_to_decide v;
true
do
()
done;
v
let add_term_to_var_hook self h = Term_to_var.add_hook self.term_to_var h

7
src/cdsat/solver.ml
View file

@ -41,13 +41,6 @@ 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