mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-11 21:48:50 -05:00
e1717f3afe
the idea is that most changes should be undone upon backtracking, using the global `on_backtrack` command and `at_level_0` to know when something is going to be permanent. In particular, should be (possibly optionally) undone on backtracking: - addition of clauses (clauses being attached) - propagations of atoms - addition of literals to the heap - internalization of literals (tbd) clauses should also be added immediately, not pushed into a queue
30 lines
636 B
OCaml
30 lines
636 B
OCaml
|
||
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)
|