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

more hooks in CC (to add clauses)

Browse source
This commit is contained in:
Simon Cruanes 2021-09-13 06:34:45 -04:00
parent 3ea7064de4
commit 677cc0c116
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
2 changed files with 23 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/cc/Sidekick_cc.ml
View file

@ -26,6 +26,7 @@ module Make (A: CC_ARG)
type term_store = T.Term.store type term_store = T.Term.store
type lit = Lit.t type lit = Lit.t
type fun_ = T.Fun.t type fun_ = T.Fun.t
type clause_pool_id = Clause_pool_id.t
type proof = A.proof type proof = A.proof
type dproof = proof -> unit type dproof = proof -> unit
type actions = Actions.t type actions = Actions.t
@ -264,6 +265,7 @@ module Make (A: CC_ARG)
field_marked_explain: Bits.field; (* used to mark traversed nodes when looking for a common ancestor *) field_marked_explain: Bits.field; (* used to mark traversed nodes when looking for a common ancestor *)
true_ : node lazy_t; true_ : node lazy_t;
false_ : node lazy_t; false_ : node lazy_t;
clauses_to_add: (Lit.t list * clause_pool_id option * dproof) Vec.t;
stat: Stat.t; stat: Stat.t;
count_conflict: int Stat.counter; count_conflict: int Stat.counter;
count_props: int Stat.counter; count_props: int Stat.counter;
@ -894,6 +896,7 @@ module Make (A: CC_ARG)
pending=Vec.create(); pending=Vec.create();
combine=Vec.create(); combine=Vec.create();
undo=Backtrack_stack.create(); undo=Backtrack_stack.create();
clauses_to_add=Vec.create();
true_; true_;
false_; false_;
stat; stat;
@ -916,10 +919,25 @@ module Make (A: CC_ARG)
let n = T_tbl.find cc.tbl t in let n = T_tbl.find cc.tbl t in
find_ n find_ n
let add_clauses self acts : unit =
if not (Vec.is_empty self.clauses_to_add) then (
Vec.iter
(fun (lits,pool,dp) ->
A.Actions.add_clause acts ?pool lits dp)
self.clauses_to_add;
Vec.clear self.clauses_to_add;
)
let[@inline] check cc acts : unit = let[@inline] check cc acts : unit =
Log.debug 5 "(cc.check)"; Log.debug 5 "(cc.check)";
cc.new_merges <- false; cc.new_merges <- false;
update_tasks cc acts add_clauses cc acts;
update_tasks cc acts;
add_clauses cc acts;
()
let[@inline] add_clause ?pool self lits dp : unit =
Vec.push self.clauses_to_add (lits,pool,dp)
let new_merges cc = cc.new_merges let new_merges cc = cc.new_merges

4
src/core/Sidekick_core.ml
View file

@ -368,6 +368,7 @@ module type CC_S = sig
and type proof = proof and type proof = proof
type term_store = T.Term.store type term_store = T.Term.store
type term = T.Term.t type term = T.Term.t
type clause_pool_id = Clause_pool_id.t
type fun_ = T.Fun.t type fun_ = T.Fun.t
type lit = Lit.t type lit = Lit.t
type actions = Actions.t type actions = Actions.t
@ -622,6 +623,9 @@ module type CC_S = sig
val merge_t : t -> term -> term -> Expl.t -> unit val merge_t : t -> term -> term -> Expl.t -> unit
(** Shortcut for adding + merging *) (** Shortcut for adding + merging *)
val add_clause : ?pool:clause_pool_id -> t -> Lit.t list -> dproof -> unit
(** Learn a lemma *)
val check : t -> actions -> unit val check : t -> actions -> unit
(** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc. (** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc.
Will use the {!actions} to propagate literals, declare conflicts, etc. *) Will use the {!actions} to propagate literals, declare conflicts, etc. *)