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

lower overhead for adding clauses to the SAT solver

Browse source 
- directly build clauses from arrays
- use IArrays rather than lists, when possible
- pushing local/persistent clauses is now direct, no more queues
This commit is contained in:
Simon Cruanes 2018-02-19 19:47:03 -06:00
parent 582f1aad18
commit d53bd8671a
21 changed files with 178 additions and 149 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/backend/Dimacs.ml
View file

@ -103,7 +103,7 @@ module Make(St : Solver_types_intf.S) = struct
| _ -> assert false)
(Vec.to_list local)
in
let local = St.Clause.make l St.Local in
let local = St.Clause.make_l l St.Local in
(* Number of atoms and clauses *)
Format.fprintf fmt
"@[<v>%s@,%a%a%a@]@."

4
src/sat/Dagon_sat.ml
View file

@ -40,8 +40,8 @@ type 'clause export = 'clause Solver_intf.export = {
}
type ('form, 'proof) actions = ('form,'proof) Theory_intf.actions = Actions of {
push : 'form list -> 'proof -> unit;
push_local : 'form list -> 'proof -> unit;
push_persistent : 'form IArray.t -> 'proof -> unit;
push_local : 'form IArray.t -> 'proof -> unit;
on_backtrack: (unit -> unit) -> unit;
at_level_0 : unit -> bool;
propagate : 'form -> 'form list -> 'proof -> unit;

28
src/sat/Internal.ml
View file

@ -284,7 +284,7 @@ module Make
) else if !duplicates = [] then (
clause
) else (
Clause.make !res (History [clause])
Clause.make_l !res (History [clause])
)
(* Partition literals for new clauses, into:
@ -456,7 +456,7 @@ module Make
with only one formula (which is [a]). So we explicitly create that clause
and set it as the cause for the propagation of [a], that way we can
rebuild the whole resolution tree when we want to prove [a]. *)
let c' = Clause.make l (History (cl :: history)) in
let c' = Clause.make_l l (History (cl :: history)) in
Log.debugf 5
(fun k -> k "Simplified reason: @[<v>%a@,%a@]" Clause.debug cl Clause.debug c');
Bcp c'
@ -658,13 +658,13 @@ module Make
if fuip.neg.is_true then (
report_unsat st confl
) else (
let uclause = Clause.make cr.cr_learnt (History cr.cr_history) in
let uclause = Clause.make_l cr.cr_learnt (History cr.cr_history) in
Vec.push st.clauses_learnt uclause;
(* no need to attach [uclause], it is true at level 0 *)
enqueue_bool st fuip (Bcp uclause)
)
| fuip :: _ ->
let lclause = Clause.make cr.cr_learnt (History cr.cr_history) in
let lclause = Clause.make_l cr.cr_learnt (History cr.cr_history) in
Vec.push st.clauses_learnt lclause;
attach_clause st lclause;
clause_bump_activity st lclause;
@ -778,7 +778,7 @@ module Make
List.iteri (fun i a -> c.atoms.(i) <- a) atoms;
c
) else (
Clause.make atoms (History (c :: history))
Clause.make_l atoms (History (c :: history))
)
in
Log.debugf 3 (fun k->k "(@[sat.add_clause.new_clause@ %a@])" Clause.debug clause);
@ -912,22 +912,22 @@ module Make
f a.lit
done
let act_push_ ~permanent st (l:formula list) (lemma:proof): unit =
let atoms = List.rev_map (mk_atom st) l in
let act_push_ ~permanent st (l:formula IArray.t) (lemma:proof): unit =
let atoms = IArray.to_array_map (mk_atom st) l in
let c = Clause.make atoms (Lemma lemma) in
Log.debugf 3 (fun k->k "(@[sat.push_clause@ %a@])" Clause.debug c);
add_clause ~permanent st c
(* TODO: ensure that the clause is removed upon backtracking *)
let act_push_local = act_push_ ~permanent:false
let act_push = act_push_ ~permanent:true
let act_push_persistent = act_push_ ~permanent:true
(* TODO: ensure that the clause is removed upon backtracking *)
let act_propagate (st:t) f causes proof : unit =
let l = List.rev_map (mk_atom st) causes in
if List.for_all (fun a -> a.is_true) l then (
let p = mk_atom st f in
let c = Clause.make (p :: List.map Atom.neg l) (Lemma proof) in
let c = Clause.make_l (p :: List.map Atom.neg l) (Lemma proof) in
if p.is_true then (
) else if p.neg.is_true then (
add_clause ~permanent:false st c
@ -953,7 +953,7 @@ module Make
let act_at_level_0 st () = at_level_0 st
let actions st = Theory_intf.Actions {
push = act_push st;
push_persistent = act_push_persistent st;
push_local = act_push_local st;
on_backtrack = on_backtrack st;
at_level_0 = act_at_level_0 st;
@ -996,7 +996,7 @@ module Make
(* conflict *)
let l = List.rev_map (mk_atom st) l in
List.iter (fun a -> insert_var_order st a.var) l;
let c = St.Clause.make l (Lemma p) in
let c = St.Clause.make_l l (Lemma p) in
Some c
)
@ -1120,7 +1120,7 @@ module Make
)
| Theory_intf.Unsat (l, p) ->
let atoms = List.rev_map (mk_atom st) l in
let c = Clause.make atoms (Lemma p) in
let c = Clause.make_l atoms (Lemma p) in
Log.debugf 3
(fun k -> k "(@[@{<Yellow>sat.theory_conflict_clause@}@ %a@])" Clause.debug c);
(* must backtrack *)
@ -1136,7 +1136,7 @@ module Make
let cs = List.rev_map
(fun atoms ->
let atoms = List.rev_map (mk_atom st) atoms in
Clause.make ?tag atoms Hyp)
Clause.make_l ?tag atoms Hyp)
cnf
in
let add_clauses () =
@ -1194,7 +1194,7 @@ module Make
Log.debugf 3 (fun k-> k "(@[sat.local_assumption@ %a@])" Atom.debug a);
assert (decision_level st = base_level st);
if not a.is_true then (
let c = Clause.make [a] Local in
let c = Clause.make [|a|] Local in
Log.debugf 5 (fun k -> k "(@[sat.add_temp_clause@ %a@])" Clause.debug c);
Vec.push st.clauses_temp c;
if a.neg.is_true then (

6
src/sat/Res.ml
View file

@ -126,7 +126,7 @@ module Make(St : Solver_types.S) = struct
) else (
assert (a.St.neg.St.is_true);
let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in
let c' = St.Clause.make [a.St.neg] r in
let c' = St.Clause.make [| a.St.neg |] r in
a.St.var.St.reason <- Some St.(Bcp c');
Log.debugf debug
(fun k -> k "New reason: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c');
@ -141,7 +141,7 @@ module Make(St : Solver_types.S) = struct
else (
Log.debugf info (fun k -> k "Proving unsat from: @[%a@]" St.Clause.debug conflict);
let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in
let res = St.Clause.make [] (St.History (conflict :: l)) in
let res = St.Clause.make [| |] (St.History (conflict :: l)) in
Log.debugf info (fun k -> k "Proof found: @[%a@]" St.Clause.debug res);
res
)
@ -175,7 +175,7 @@ module Make(St : Solver_types.S) = struct
begin match r with
| [] -> (l, c, d, a)
| _ ->
let new_clause = St.Clause.make l (St.History [c; d]) in
let new_clause = St.Clause.make_l l (St.History [c; d]) in
chain_res (new_clause, l) r
end
| _ ->

17
src/sat/Solver.ml
View file

@ -24,6 +24,7 @@ module Make
type formula = St.formula
type atom = St.formula
type lit = St.atom
type clause = St.clause
type theory = Th.t
@ -130,15 +131,25 @@ module Make
let local = S.temp st in
{hyps; history; local}
module Lit = struct
type t = lit
let pp = St.Atom.pp
let make = S.mk_atom
end
module Clause = struct
include St.Clause
let atoms c = St.Clause.atoms c |> Array.map (fun a -> a.St.lit)
let atoms c = St.Clause.atoms c |> IArray.of_array_map (fun a -> a.St.lit)
let atoms_l c = St.Clause.atoms_l c |> List.map (fun a -> a.St.lit)
let make st ?tag l =
let[@inline] make ?tag (a:lit array) : t = St.Clause.make ?tag a St.Hyp
let[@inline] make_l ?tag l : t = St.Clause.make_l ?tag l St.Hyp
let of_atoms st ?tag l =
let l = List.map (S.mk_atom st) l in
St.Clause.make ?tag l St.Hyp
make_l ?tag l
end
module Formula = St.Formula

21
src/sat/Solver_intf.ml
View file

@ -48,7 +48,9 @@ module type S = sig
type formula (** user formulas *)
type clause
type lit (** SAT solver literals *)
type clause (** SAT solver clauses *)
type theory (** user theory *)
@ -133,15 +135,28 @@ module type S = sig
type solver = t
module Lit : sig
type t = lit
val make : solver -> atom -> t
val pp : t CCFormat.printer
end
module Clause : sig
type t = clause
val atoms : t -> atom array
val atoms : t -> atom IArray.t
val atoms_l : t -> atom list
val tag : t -> int option
val equal : t -> t -> bool
val make : solver -> ?tag:int -> atom list -> t
val make : ?tag:int -> lit array -> t
(** Make a clause from this array of SAT literals.
The array's ownership is transferred to the clause, do not mutate it *)
val make_l : ?tag:int -> lit list -> t
val of_atoms : solver -> ?tag:int -> atom list -> t
val pp : t printer
end

9
src/sat/Solver_types.ml
View file

@ -269,7 +269,7 @@ module Make (E : Theory_intf.S) = struct
(sign a) (a.var.vid+1) debug_value a E.Form.print a.lit
let debug_a out vec =
Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec
Array.iteri (fun i a -> if i>0 then Format.fprintf out "@ "; debug out a) vec
end
module Clause = struct
@ -278,8 +278,7 @@ module Make (E : Theory_intf.S) = struct
let make =
let n = ref 0 in
fun ?tag ali premise ->
let atoms = Array.of_list ali in
fun ?tag atoms premise ->
let name = !n in
incr n;
{ name;
@ -290,7 +289,9 @@ module Make (E : Theory_intf.S) = struct
cpremise = premise;
}
let empty = make [] (History [])
let make_l ?tag l pr = make ?tag (Array.of_list l) pr
let empty = make [| |] (History [])
let name = name_of_clause
let[@inline] equal c1 c2 = c1==c2
let[@inline] atoms c = c.atoms

9
src/sat/Solver_types_intf.ml
View file

@ -184,8 +184,13 @@ module type S = sig
val empty : t
(** The empty clause *)
val make : ?tag:int -> Atom.t list -> premise -> clause
(** [make_clause name atoms size premise] creates a clause with the given attributes. *)
val make : ?tag:int -> Atom.t array -> premise -> t
(** [make_clause name atoms size premise] creates a clause with
the given attributes.
The array's ownership is transferred to the clause, do not
mutate it after that. *)
val make_l : ?tag:int -> Atom.t list -> premise -> t
val pp : t printer
val pp_dimacs : t printer

4
src/sat/Theory_intf.ml
View file

@ -42,10 +42,10 @@ type ('formula, 'proof) res =
(** Actions given to the theory during initialization, to be used
at any time *)
type ('form, 'proof) actions = Actions of {
push : 'form list -> 'proof -> unit;
push_persistent : 'form IArray.t -> 'proof -> unit;
(** Allows to add a persistent clause to the solver. *)
push_local : 'form list -> 'proof -> unit;
push_local : 'form IArray.t -> 'proof -> unit;
(** Allows to add a local clause to the solver. The clause
will be removed after backtracking. *)

30
src/smt/Clause.ml
View file

@ -1,30 +0,0 @@
open Solver_types
type t = Lit.t list
let lits c = c
let pp out c = match lits c with
| [] -> Fmt.string out "false"
| [lit] -> Lit.pp out lit
| l ->
Format.fprintf out "[@[<hv>%a@]]"
(Util.pp_list ~sep:" ∨ " Lit.pp) l
(* canonical form: sorted list *)
let make =
fun l -> CCList.sort_uniq ~cmp:Lit.compare l
let equal_ c1 c2 = CCList.equal Lit.equal (lits c1) (lits c2)
let hash_ c = Hash.list Lit.hash (lits c)
module Tbl = CCHashtbl.Make(struct
type t_ = t
type t = t_
let equal = equal_
let hash = hash_
end)
let iter f c = List.iter f (lits c)
let to_seq c = Sequence.of_list (lits c)

12
src/smt/Clause.mli
View file

@ -1,12 +0,0 @@
open Solver_types
type t = Lit.t list
val make : Lit.t list -> t
val lits : t -> Lit.t list
val iter : (Lit.t -> unit) -> t -> unit
val to_seq : t -> Lit.t Sequence.t
val pp : t Fmt.printer
module Tbl : CCHashtbl.S with type key = t

11
src/smt/Congruence_closure.ml
View file

@ -411,6 +411,17 @@ let assert_lit cc lit : unit = match Lit.view lit with
push_combine cc n rhs (E_lit lit);
()
let assert_eq cc (t:term) (u:term) expl : unit =
let n1 = add cc t in
let n2 = add cc u in
if not (same_class cc n1 n2) then (
union cc n1 n2 expl
)
let assert_distinct _cc (l:term list) _expl : unit =
assert (match l with[] | [_] -> false | _ -> true);
Util.errorf "unimplemented: CC.distinct"
let create ?(size=2048) ~actions (tst:Term.state) : t =
assert (actions.at_lvl_0 ());
let nd = Equiv_class.dummy in

12
src/smt/Congruence_closure.mli
View file

@ -46,10 +46,6 @@ val same_class : t -> node -> node -> bool
val union : t -> node -> node -> explanation -> unit
(** Merge the two equivalence classes. Will be undone on backtracking. *)
val assert_lit : t -> Lit.t -> unit
(** Given a literal, assume it in the congruence closure and propagate
its consequences. Will be backtracked. *)
val mem : t -> term -> bool
(** Is the term properly added to the congruence closure? *)
@ -63,6 +59,14 @@ val add_seq : t -> term Sequence.t -> unit
val all_classes : t -> repr Sequence.t
(** All current classes *)
val assert_lit : t -> Lit.t -> unit
(** Given a literal, assume it in the congruence closure and propagate
its consequences. Will be backtracked. *)
val assert_eq : t -> term -> term -> explanation -> unit
val assert_distinct : t -> term list -> explanation -> unit
val check : t -> unit
val final_check : t -> unit

13
src/smt/Explanation.ml
View file

@ -1,13 +1,24 @@
open Solver_types
type t = explanation
type t = explanation =
| E_reduction
| E_lit of lit
| E_congruence of cc_node * cc_node
| E_injectivity of cc_node * cc_node
| E_reduce_eq of cc_node * cc_node
| E_custom of {
name : ID.t; args : explanation list;
pp : (ID.t * explanation list) Fmt.printer;
}
let compare = cmp_exp
let equal a b = cmp_exp a b = 0
let pp = pp_explanation
let[@inline] lit l : t = E_lit l
module Set = CCSet.Make(struct
type t = explanation
let compare = compare

10
src/smt/Lit.ml
View file

@ -1,7 +1,15 @@
open Solver_types
type t = lit
type t = lit = {
lit_view : lit_view;
lit_sign : bool
}
and view = lit_view =
| Lit_fresh of ID.t
| Lit_atom of term
| Lit_expanded of term
let neg l = {l with lit_sign=not l.lit_sign}

11
src/smt/Lit.mli
View file

@ -2,7 +2,16 @@
open Solver_types
type t = lit
type t = lit = {
lit_view : lit_view;
lit_sign : bool
}
and view = lit_view =
| Lit_fresh of ID.t
| Lit_atom of term
| Lit_expanded of term
val neg : t -> t
val abs : t -> t
val sign : t -> bool

32
src/smt/Solver.ml
View file

@ -13,8 +13,8 @@ type level = int
module Sat_solver = Dagon_sat.Make(Theory_combine)
let[@inline] clause_of_mclause (c:Sat_solver.clause): Clause.t =
Sat_solver.Clause.atoms_l c |> Clause.make
let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
Sat_solver.Clause.atoms c
module Proof = struct
type t = Sat_solver.Proof.proof
@ -22,8 +22,7 @@ module Proof = struct
let pp out (p:t) : unit =
let pp_step_res out p =
let {Sat_solver.Proof.conclusion; _ } = Sat_solver.Proof.expand p in
let conclusion = clause_of_mclause conclusion in
Clause.pp out conclusion
Sat_solver.Clause.pp out conclusion
in
let pp_step out = function
| Sat_solver.Proof.Lemma _ -> Format.fprintf out "(@[<1>lemma@ ()@])"
@ -35,9 +34,8 @@ module Proof = struct
Format.fprintf out "(@[<v>";
Sat_solver.Proof.fold
(fun () {Sat_solver.Proof.conclusion; step } ->
let conclusion = clause_of_mclause conclusion in
Format.fprintf out "(@[<hv1>step@ %a@ @[<1>from:@ %a@]@])@,"
Clause.pp conclusion pp_step step)
Sat_solver.Clause.pp conclusion pp_step step)
() p;
Format.fprintf out "@])";
()
@ -51,11 +49,12 @@ type t = {
config: Config.t
}
let solver self = self.solver
let th_combine (self:t) : Theory_combine.t = Sat_solver.theory self.solver
let add_theory self th = Theory_combine.add_theory (th_combine self) th
let[@inline] solver self = self.solver
let[@inline] th_combine (self:t) : Theory_combine.t = Sat_solver.theory self.solver
let[@inline] add_theory self th = Theory_combine.add_theory (th_combine self) th
let[@inline] cc self = Theory_combine.cc (th_combine self)
let stats self = self.stat
let tst self = Theory_combine.tst (th_combine self)
let[@inline] tst self = Theory_combine.tst (th_combine self)
let create ?size ?(config=Config.empty) ~theories () : t =
let self = {
@ -359,7 +358,7 @@ end
(** {2 Main} *)
(* convert unsat-core *)
let clauses_of_unsat_core (core:Sat_solver.clause list): Clause.t Sequence.t =
let clauses_of_unsat_core (core:Sat_solver.clause list): Lit.t IArray.t Sequence.t =
Sequence.of_list core
|> Sequence.map clause_of_mclause
@ -388,11 +387,18 @@ let do_on_exit ~on_exit =
List.iter (fun f->f()) on_exit;
()
let assume (self:t) (c:Clause.t) : unit =
let assume (self:t) (c:Lit.t IArray.t) : unit =
let sat = solver self in
let c = Sat_solver.Clause.make sat (Clause.lits c) in
let c = Sat_solver.Clause.make (IArray.to_array_map (Sat_solver.Lit.make sat) c) in
Sat_solver.add_clause ~permanent:false sat c
let[@inline] assume_eq self t u expl : unit =
Congruence_closure.assert_eq (cc self) t u (E_lit expl)
let[@inline] assume_distinct self l expl : unit =
(* FIXME: custom evaluation instead (register to subterms) *)
Congruence_closure.assert_distinct (cc self) l (E_lit expl)
(*
type unsat_core = Sat.clause list
*)

6
src/smt/Solver.mli
View file

@ -44,10 +44,14 @@ val create :
val solver : t -> Sat_solver.t
val th_combine : t -> Theory_combine.t
val add_theory : t -> Theory.t -> unit
val cc : t -> Congruence_closure.t
val stats : t -> Stat.t
val tst : t -> Term.state
val assume : t -> Clause.t -> unit
val assume : t -> Lit.t IArray.t -> unit
val assume_eq : t -> Term.t -> Term.t -> Lit.t -> unit
val assume_distinct : t -> Term.t list -> Lit.t -> unit
val solve :
?on_exit:(unit -> unit) list ->

27
src/smt/Theory.ml
View file

@ -1,4 +1,19 @@
module Clause : sig
type t = Lit.t IArray.t
val pp : t CCFormat.printer
end = struct
type t = Lit.t IArray.t
let pp out c =
if IArray.length c = 0 then CCFormat.string out "false"
else if IArray.length c = 1 then Lit.pp out (IArray.get c 0)
else (
Format.fprintf out "[@[<hv>%a@]]"
(Util.pp_iarray ~sep:" ∨ " Lit.pp) c
)
end
(** Runtime state of a theory, with all the operations it provides.
['a] is the internal state *)
type state = State : {
@ -37,13 +52,13 @@ type actions = {
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
case_split: Clause.t -> unit;
(** Force the solver to case split on this clause.
The clause will be removed upon backtracking. *)
add_local_axiom: Lit.t IArray.t -> unit;
(** Add local clause to the SAT solver. This clause will be
removed when the solver backtracks. *)
add_axiom: Clause.t -> unit;
(** Add a persistent axiom to the SAT solver. This will not
be backtracked *)
add_persistent_axiom: Lit.t IArray.t -> unit;
(** Add toplevel clause to the SAT solver. This clause will
not be backtracked. *)
find: Term.t -> Equiv_class.t;
(** Find representative of this term *)

61
src/smt/Theory_combine.ml
View file

@ -30,13 +30,6 @@ type t = {
(** congruence closure *)
mutable theories : Theory.state list;
(** Set of theories *)
lemma_q : Clause.t Queue.t;
(** list of clauses that have been newly generated, waiting
to be propagated to the core solver.
invariant: those clauses must be tautologies *)
split_q : Clause.t Queue.t;
(** Local clauses to be added to the core solver, that will
be removed on backtrack *)
mutable conflict: conflict option;
(** current conflict, if any *)
}
@ -64,27 +57,10 @@ let assume_lit (self:t) (lit:Lit.t) : unit =
theories self (fun (Theory.State th) -> th.on_assert th.st lit);
end
(* push clauses from {!lemma_queue} into the slice *)
let push_new_clauses_into_cdcl (self:t) : unit =
let Sat_solver.Actions r = self.cdcl_acts in
(* persistent lemmas *)
while not (Queue.is_empty self.lemma_q) do
let c = Queue.pop self.lemma_q in
Sat_solver.Log.debugf 5 (fun k->k "(@[<2>push_lemma@ %a@])" Clause.pp c);
r.push c Proof.default
done;
(* local splits *)
while not (Queue.is_empty self.split_q) do
let c = Queue.pop self.split_q in
Sat_solver.Log.debugf 5 (fun k->k "(@[<2>split_on@ %a@])" Clause.pp c);
r.push_local c Proof.default
done
(* return result to the SAT solver *)
let cdcl_return_res (self:t) : _ Sat_solver.res =
begin match self.conflict with
| None ->
push_new_clauses_into_cdcl self;
Sat_solver.Sat
| Some c ->
let lit_set =
@ -93,13 +69,12 @@ let cdcl_return_res (self:t) : _ Sat_solver.res =
in
let conflict_clause =
Lit.Set.to_list lit_set
|> List.map Lit.neg
|> Clause.make
|> IArray.of_list_map Lit.neg
in
Sat_solver.Log.debugf 3
(fun k->k "(@[<1>conflict@ clause: %a@])"
Clause.pp conflict_clause);
Sat_solver.Unsat (Clause.lits conflict_clause, Proof.default)
Theory.Clause.pp conflict_clause);
Sat_solver.Unsat (IArray.to_list conflict_clause, Proof.default)
end
let[@inline] check (self:t) : unit =
@ -153,7 +128,7 @@ let act_propagate (self:t) f guard : unit =
in
Sat_solver.Log.debugf 2
(fun k->k "(@[@{<green>propagate@}@ %a@ :guard %a@])"
Lit.pp f Clause.pp guard);
Lit.pp f (Util.pp_list Lit.pp) guard);
r.propagate f guard Proof.default
(** {2 Interface to Congruence Closure} *)
@ -190,8 +165,6 @@ let create (cdcl_acts:_ Sat_solver.actions) : t =
Congruence_closure.create ~size:1024 ~actions self.tst;
);
theories = [];
lemma_q = Queue.create();
split_q = Queue.create();
conflict = None;
} in
ignore @@ Lazy.force @@ self.cc;
@ -202,37 +175,35 @@ let create (cdcl_acts:_ Sat_solver.actions) : t =
let act_all_classes self = Congruence_closure.all_classes (cc self)
let act_propagate_eq self t u guard =
let r_t = Congruence_closure.add (cc self) t in
let r_u = Congruence_closure.add (cc self) u in
Congruence_closure.union (cc self) r_t r_u guard
Congruence_closure.assert_eq (cc self) t u guard
let act_find self t =
Congruence_closure.add (cc self) t
|> Congruence_closure.find (cc self)
let act_case_split self (c:Clause.t) =
Sat_solver.Log.debugf 2 (fun k->k "(@[<1>add_split@ @[%a@]@])" Clause.pp c);
Queue.push c self.split_q
let act_add_local_axiom self c : unit =
Sat_solver.Log.debugf 5 (fun k->k "(@[<2>th_combine.push_local_lemma@ %a@])" Theory.Clause.pp c);
let Sat_solver.Actions r = self.cdcl_acts in
r.push_local c Proof.default
(* push one clause into [M], in the current level (not a lemma but
an axiom) *)
let act_add_axiom self (c:Clause.t): unit =
Sat_solver.Log.debugf 2 (fun k->k "(@[<1>add_axiom@ @[%a@]@])" Clause.pp c);
(* TODO incr stat_num_clause_push; *)
Queue.push c self.lemma_q
let act_add_persistent_axiom self c : unit =
Sat_solver.Log.debugf 5 (fun k->k "(@[<2>th_combine.push_persistent_lemma@ %a@])" Theory.Clause.pp c);
let Sat_solver.Actions r = self.cdcl_acts in
r.push_persistent c Proof.default
let mk_theory_actions (self:t) : Theory.actions =
let Sat_solver.Actions r = self.cdcl_acts in
{
Theory.
{ Theory.
on_backtrack = r.on_backtrack;
at_lvl_0 = r.at_level_0;
raise_conflict = act_raise_conflict;
propagate = act_propagate self;
all_classes = act_all_classes self;
propagate_eq = act_propagate_eq self;
case_split = act_case_split self;
add_axiom = act_add_axiom self;
add_local_axiom = act_add_local_axiom self;
add_persistent_axiom = act_add_persistent_axiom self;
find = act_find self;
}

2
src/smtlib/Process.ml
View file

@ -310,7 +310,7 @@ let process_stmt
(* TODO
hyps := clauses @ !hyps;
*)
Solver.assume solver (Clause.make [Lit.atom t]);
Solver.assume solver (IArray.singleton (Lit.atom t));
E.return()
| A.Goal (_, _) ->
Util.errorf "cannot deal with goals yet"