From 8e8a59247548437b3285fb083131ba06a663a078 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 11 Dec 2014 15:31:25 +0100 Subject: [PATCH] Some reorganization of files/folders --- .merlin | 6 + Makefile | 2 +- _tags | 2 + mcsolver/expr_intf.ml | 54 ++ mcsolver/mcsolver.ml | 776 ++++++++++++++++++ mcsolver/mcsolver.mli | 69 ++ mcsolver/mcsolver_types.ml | 213 +++++ .../mcsolver_types.mli | 10 +- .../mcsolver_types_intf.ml | 0 sat/theory_intf.ml => mcsolver/plugin_intf.ml | 0 msat.mlpack | 34 +- sat/explanation.ml | 72 -- sat/explanation_intf.ml | 36 - {sat => solver}/.merlin | 0 {sat => solver}/formula_intf.ml | 0 {sat => solver}/res.ml | 0 {sat => solver}/res.mli | 0 {sat => solver}/res_intf.ml | 0 {sat => solver}/solver.ml | 0 {sat => solver}/solver.mli | 0 {sat => solver}/solver_types.ml | 0 {sat => solver}/solver_types.mli | 0 solver/solver_types_intf.ml | 95 +++ solver/theory_intf.ml | 61 ++ {sat => solver}/tseitin.ml | 0 {sat => solver}/tseitin.mli | 0 {sat => solver}/tseitin_intf.ml | 0 27 files changed, 1295 insertions(+), 135 deletions(-) create mode 100644 mcsolver/expr_intf.ml create mode 100644 mcsolver/mcsolver.ml create mode 100644 mcsolver/mcsolver.mli create mode 100644 mcsolver/mcsolver_types.ml rename sat/explanation.mli => mcsolver/mcsolver_types.mli (72%) rename sat/solver_types_intf.ml => mcsolver/mcsolver_types_intf.ml (100%) rename sat/theory_intf.ml => mcsolver/plugin_intf.ml (100%) delete mode 100644 sat/explanation.ml delete mode 100644 sat/explanation_intf.ml rename {sat => solver}/.merlin (100%) rename {sat => solver}/formula_intf.ml (100%) rename {sat => solver}/res.ml (100%) rename {sat => solver}/res.mli (100%) rename {sat => solver}/res_intf.ml (100%) rename {sat => solver}/solver.ml (100%) rename {sat => solver}/solver.mli (100%) rename {sat => solver}/solver_types.ml (100%) rename {sat => solver}/solver_types.mli (100%) create mode 100644 solver/solver_types_intf.ml create mode 100644 solver/theory_intf.ml rename {sat => solver}/tseitin.ml (100%) rename {sat => solver}/tseitin.mli (100%) rename {sat => solver}/tseitin_intf.ml (100%) diff --git a/.merlin b/.merlin index cc724db2..d9bc3db3 100644 --- a/.merlin +++ b/.merlin @@ -1,6 +1,12 @@ S sat S smt +S solver +S mcsolver S util + +B _build/ B _build/sat B _build/smt +B _build/solver +B _build/mcsolver B _build/util diff --git a/Makefile b/Makefile index e47b80ea..fb58f8a1 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ LOG=build.log COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display FLAGS= -DIRS=-Is sat,smt,util,util/smtlib +DIRS=-Is mcsolver,solver,sat,smt,util,util/smtlib DOC=msat.docdir/index.html TEST=sat_solve.native bench_stats.native diff --git a/_tags b/_tags index de6046b2..589352bd 100644 --- a/_tags +++ b/_tags @@ -2,6 +2,8 @@ : package(unix) : for-pack(Msat), package(zarith) : for-pack(Msat) +: for-pack(Msat) +: for-pack(Msat) # enable stronger inlining everywhere : inline(15) diff --git a/mcsolver/expr_intf.ml b/mcsolver/expr_intf.ml new file mode 100644 index 00000000..b18dfc13 --- /dev/null +++ b/mcsolver/expr_intf.ml @@ -0,0 +1,54 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Guillaume Bury *) +(* INRIA *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module type S = sig + (** Signature of formulas that parametrises the SMT Solver Module. *) + + module Term : sig + (** The type of terms *) + type t + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val print : Format.formatter -> t -> unit + end + + module Formula : sig + (** The type of atomic formulas over terms. *) + type t + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val print : Format.formatter -> t -> unit + end + + val dummy : Formula.t + (** Formula constants. A valid formula should never be physically equal to [dummy] *) + + val fresh : unit -> Formula.t + (** Returns a fresh litteral, distinct from any other literal (used in cnf conversion) *) + + val neg : Formula.t -> Formula.t + (** Formula negation *) + + val norm : Formula.t -> Formula.t * bool + (** Returns a 'normalized' form of the formula, possibly negated (in which case return true). + [norm] must be so that [a] and [neg a] normalises to the same formula. *) + + val iter_pure : (Term.t -> unit) -> Formula.t -> bool + (** An iterator over the pure subterms of a formula *) + +end + diff --git a/mcsolver/mcsolver.ml b/mcsolver/mcsolver.ml new file mode 100644 index 00000000..34db799d --- /dev/null +++ b/mcsolver/mcsolver.ml @@ -0,0 +1,776 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo Zero *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module Make (E : Expr_intf.S) + (Th : Plugin_intf.S with type formula = E.Formula.t) = struct + + module St = Mcsolver_types.Make(E)(Th) + module Proof = Res.Make(St) + + open St + + exception Sat + exception Unsat + exception Restart + exception Conflict of clause + + (* a push/pop state *) + type user_level = { + ul_trail : int; (* height of the decision trail *) + ul_clauses : int; (* number of clauses *) + ul_learnt : int; (* number of learnt clauses *) + } + + (* Singleton type containing the current state *) + type env = { + + mutable is_unsat : bool; + (* if [true], constraints are already false *) + + mutable unsat_conflict : clause option; + (* conflict clause at decision level 0, if any *) + + clauses : clause Vec.t; + (* all currently active clauses *) + + learnts : clause Vec.t; + (* learnt clauses *) + + mutable clause_inc : float; + (* increment for clauses' activity *) + + mutable var_inc : float; + (* increment for variables' activity *) + + trail : atom Vec.t; + (* decision stack + propagated atoms *) + + trail_lim : int Vec.t; + (* decision levels in [trail] *) + + user_levels : user_level Vec.t; + (* user-defined levels, for {!push} and {!pop} *) + + mutable qhead : int; + (* Start offset in the queue of unit facts to propagate, within the trail *) + + mutable simpDB_assigns : int; + (* number of toplevel assignments since last call to [simplify ()] *) + + mutable simpDB_props : int; + (* remaining number of propagations before the next call to [simplify ()] *) + + order : Iheap.t; + (* Heap ordered by variable activity *) + + mutable progress_estimate : float; + (* progression estimate, updated by [search ()] *) + + remove_satisfied : bool; + + var_decay : float; + (* inverse of the activity factor for variables. Default 1/0.999 *) + + clause_decay : float; + (* inverse of the activity factor for clauses. Default 1/0.95 *) + + mutable restart_first : int; + (* intial restart limit, default 100 *) + + restart_inc : float; + (* multiplicative factor for restart limit, default 1.5 *) + + mutable learntsize_factor : float; + (* initial limit for the number of learnt clauses, 1/3 of initial + number of clauses by default *) + + learntsize_inc : float; + (* multiplicative factor for [learntsize_factor] at each restart, default 1.1 *) + + expensive_ccmin : bool; + (* control minimization of conflict clause, default true *) + + polarity_mode : bool; + (* default polarity for decision *) + + mutable starts : int; + mutable decisions : int; + mutable propagations : int; + mutable conflicts : int; + mutable clauses_literals : int; + mutable learnts_literals : int; + mutable max_literals : int; + mutable tot_literals : int; + mutable nb_init_clauses : int; + mutable model : var Vec.t; + mutable tenv_queue : Th.level Vec.t; + mutable tatoms_qhead : int; + } + + let env = { + is_unsat = false; + unsat_conflict = None; + clauses = Vec.make 0 dummy_clause; (*updated during parsing*) + learnts = Vec.make 0 dummy_clause; (*updated during parsing*) + clause_inc = 1.; + var_inc = 1.; + trail = Vec.make 601 dummy_atom; + trail_lim = Vec.make 601 (-1); + user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0}; + qhead = 0; + simpDB_assigns = -1; + simpDB_props = 0; + order = Iheap.init 0; (* updated in solve *) + progress_estimate = 0.; + remove_satisfied = true; + var_decay = 1. /. 0.95; + clause_decay = 1. /. 0.999; + restart_first = 100; + restart_inc = 1.5; + learntsize_factor = 1. /. 3. ; + learntsize_inc = 1.1; + expensive_ccmin = true; + polarity_mode = false; + starts = 0; + decisions = 0; + propagations = 0; + conflicts = 0; + clauses_literals = 0; + learnts_literals = 0; + max_literals = 0; + tot_literals = 0; + nb_init_clauses = 0; + model = Vec.make 0 dummy_var; + tenv_queue = Vec.make 100 Th.dummy; + tatoms_qhead = 0; + } + + (* Misc functions *) + let to_float i = float_of_int i + let to_int f = int_of_float f + + let f_weight i j = + (St.get_var j).weight < (St.get_var i).weight + + let f_filter i = + (St.get_var i).level < 0 + + + (* Var/clause activity *) + let insert_var_order v = + Iheap.insert f_weight env.order v.vid + + let var_decay_activity () = + env.var_inc <- env.var_inc *. env.var_decay + + let clause_decay_activity () = + env.clause_inc <- env.clause_inc *. env.clause_decay + + let var_bump_activity v = + v.weight <- v.weight +. env.var_inc; + if v.weight > 1e100 then begin + for i = 0 to (St.nb_vars ()) - 1 do + (St.get_var i).weight <- (St.get_var i).weight *. 1e-100 + done; + env.var_inc <- env.var_inc *. 1e-100; + end; + if Iheap.in_heap env.order v.vid then + Iheap.decrease f_weight env.order v.vid + + let clause_bump_activity c = + c.activity <- c.activity +. env.clause_inc; + if c.activity > 1e20 then begin + for i = 0 to (Vec.size env.learnts) - 1 do + (Vec.get env.learnts i).activity <- + (Vec.get env.learnts i).activity *. 1e-20; + done; + env.clause_inc <- env.clause_inc *. 1e-20 + end + + (* Convenient access *) + let decision_level () = Vec.size env.trail_lim + + let nb_assigns () = Vec.size env.trail + let nb_clauses () = Vec.size env.clauses + let nb_learnts () = Vec.size env.learnts + let nb_vars () = St.nb_vars () + + let new_decision_level() = + Vec.push env.trail_lim (Vec.size env.trail); + Vec.push env.tenv_queue (Th.current_level ()); (* save the current tenv *) + Log.debug 5 "New decision level : %d (%d in env queue)(%d in trail)" + (Vec.size env.trail_lim) (Vec.size env.tenv_queue) (Vec.size env.trail); + () + + let attach_clause c = + Vec.push (Vec.get c.atoms 0).neg.watched c; + Vec.push (Vec.get c.atoms 1).neg.watched c; + Log.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 0).neg St.pp_clause c; + Log.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 1).neg St.pp_clause c; + if c.learnt then + env.learnts_literals <- env.learnts_literals + Vec.size c.atoms + else + env.clauses_literals <- env.clauses_literals + Vec.size c.atoms + + let detach_clause c = + c.removed <- true; + (* + Vec.remove (Vec.get c.atoms 0).neg.watched c; + Vec.remove (Vec.get c.atoms 1).neg.watched c; + *) + if c.learnt then + env.learnts_literals <- env.learnts_literals - Vec.size c.atoms + else + env.clauses_literals <- env.clauses_literals - Vec.size c.atoms + + let remove_clause c = detach_clause c + + let satisfied c = + Vec.exists (fun atom -> atom.is_true) c.atoms + + (* cancel down to [lvl] excluded *) + let cancel_until lvl = + Log.debug 5 "Bactracking to decision level %d (excluded)" lvl; + if decision_level () > lvl then begin + env.qhead <- Vec.get env.trail_lim lvl; + env.tatoms_qhead <- env.qhead; + for c = Vec.size env.trail - 1 downto env.qhead do + let a = Vec.get env.trail c in + a.is_true <- false; + a.neg.is_true <- false; + a.var.level <- -1; + a.var.reason <- None; + a.var.vpremise <- History []; + insert_var_order a.var + done; + Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) + Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); + Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl); + Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl) + end; + assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) + + let report_unsat ({atoms=atoms} as confl) = + Log.debug 5 "Unsat conflict : %a" St.pp_clause confl; + env.unsat_conflict <- Some confl; + env.is_unsat <- true; + raise Unsat + + let enqueue a lvl reason = + assert (not a.is_true && not a.neg.is_true && + a.var.level < 0 && a.var.reason = None && lvl >= 0); + assert (lvl = decision_level ()); + (* keep the reason for proof/unsat-core *) + (*let reason = if lvl = 0 then None else reason in*) + a.is_true <- true; + a.var.level <- lvl; + a.var.reason <- reason; + Log.debug 8 "Enqueue: %a" pp_atom a; + Vec.push env.trail a + + (* conflict analysis *) + let analyze c_clause = + let pathC = ref 0 in + let learnt = ref [] in + let cond = ref true in + let blevel = ref 0 in + let seen = ref [] in + let c = ref c_clause in + let tr_ind = ref (Vec.size env.trail - 1) in + let size = ref 1 in + let history = ref [] in + while !cond do + if !c.learnt then clause_bump_activity !c; + history := !c :: !history; + (* visit the current predecessors *) + for j = 0 to Vec.size !c.atoms - 1 do + let q = Vec.get !c.atoms j in + (*printf "I visit %a@." D1.atom q;*) + assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) + if not q.var.seen && q.var.level > 0 then begin + var_bump_activity q.var; + q.var.seen <- true; + seen := q :: !seen; + if q.var.level >= decision_level () then begin + incr pathC + end else begin + learnt := q :: !learnt; + incr size; + blevel := max !blevel q.var.level + end + end + done; + + (* look for the next node to expand *) + while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; + decr pathC; + let p = Vec.get env.trail !tr_ind in + decr tr_ind; + match !pathC, p.var.reason with + | 0, _ -> + cond := false; + learnt := p.neg :: (List.rev !learnt) + | n, None -> assert false + | n, Some cl -> c := cl + done; + List.iter (fun q -> q.var.seen <- false) !seen; + !blevel, !learnt, !history, !size + + let record_learnt_clause blevel learnt history size = + begin match learnt with + | [] -> assert false + | [fuip] -> + assert (blevel = 0); + fuip.var.vpremise <- history; + let name = fresh_lname () in + let uclause = make_clause name learnt size true history in + Log.debug 2 "Unit clause learnt : %a" St.pp_clause uclause; + Vec.push env.learnts uclause; + enqueue fuip 0 (Some uclause) + | fuip :: _ -> + let name = fresh_lname () in + let lclause = make_clause name learnt size true history in + Log.debug 2 "New clause learnt : %a" St.pp_clause lclause; + Vec.push env.learnts lclause; + attach_clause lclause; + clause_bump_activity lclause; + enqueue fuip blevel (Some lclause) + end; + var_decay_activity (); + clause_decay_activity () + + let add_boolean_conflict confl = + env.conflicts <- env.conflicts + 1; + if decision_level() = 0 then report_unsat confl; (* Top-level conflict *) + let blevel, learnt, history, size = analyze confl in + cancel_until blevel; + record_learnt_clause blevel learnt (History history) size + + (* Add a new clause *) + exception Trivial + + let simplify_zero atoms init0 = + (* TODO: could be more efficient than [@] everywhere? *) + assert (decision_level () = 0); + let aux (atoms, init) a = + if a.is_true then raise Trivial; + if a.neg.is_true then + match a.var.vpremise with + | History v -> atoms, [init0] + | Lemma p -> assert false + else + a::atoms, init + in + let atoms, init = List.fold_left aux ([], []) atoms in + List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init + + let partition atoms init0 = + let rec partition_aux trues unassigned falses init = function + | [] -> trues @ unassigned @ falses, init + | a::r -> + if a.is_true then + if a.var.level = 0 then raise Trivial + else (a::trues) @ unassigned @ falses @ r, init + else if a.neg.is_true then + if a.var.level = 0 then match a.var.vpremise with + | History v -> + partition_aux trues unassigned falses [init0] r + | Lemma _ -> assert false + else + partition_aux trues unassigned (a::falses) init r + else partition_aux trues (a::unassigned) falses init r + in + if decision_level () = 0 then + simplify_zero atoms init0 + else + partition_aux [] [] [] [] atoms + + let add_clause ~cnumber atoms history = + if env.is_unsat then raise Unsat; + let init_name = string_of_int cnumber in + let init0 = make_clause init_name atoms (List.length atoms) (history <> History []) history in + Log.debug 10 "Adding clause : %a" St.pp_clause init0; + try + let atoms, init = partition atoms init0 in + let history = match init with + | [] -> history + | l -> History l + in + let size = List.length atoms in + match atoms with + | [] -> + report_unsat init0; + | a::b::_ -> + let name = fresh_name () in + let clause = make_clause name atoms size (history <> History []) history in + Log.debug 10 "New clause : %a" St.pp_clause init0; + attach_clause clause; + Vec.push env.clauses clause; + if a.neg.is_true then begin + let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in + cancel_until lvl; + add_boolean_conflict clause + end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin + let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in + cancel_until lvl; + enqueue a lvl (Some clause) + end + | [a] -> + cancel_until 0; + a.var.vpremise <- history; + enqueue a 0 (match init with [init0] -> Some init0 | _ -> None) + with Trivial -> () + + + (* Decide on a new litteral *) + let rec pick_branch_lit () = + let max = Iheap.remove_min f_weight env.order in + let v = St.get_var max in + if v.level>= 0 then begin + assert (v.pa.is_true || v.na.is_true); + pick_branch_lit () + end else + v + + let progress_estimate () = + let prg = ref 0. in + let nbv = to_float (nb_vars()) in + let lvl = decision_level () in + let _F = 1. /. nbv in + for i = 0 to lvl do + let _beg = if i = 0 then 0 else Vec.get env.trail_lim (i-1) in + let _end = if i=lvl then Vec.size env.trail else Vec.get env.trail_lim i in + prg := !prg +. _F**(to_float i) *. (to_float (_end - _beg)) + done; + !prg /. nbv + + let propagate_in_clause a c i watched new_sz = + let atoms = c.atoms in + let first = Vec.get atoms 0 in + if first == a.neg then begin (* false lit must be at index 1 *) + Vec.set atoms 0 (Vec.get atoms 1); + Vec.set atoms 1 first + end; + let first = Vec.get atoms 0 in + if first.is_true then begin + (* true clause, keep it in watched *) + Vec.set watched !new_sz c; + incr new_sz; + end + else + try (* look for another watch lit *) + for k = 2 to Vec.size atoms - 1 do + let ak = Vec.get atoms k in + if not (ak.neg.is_true) then begin + (* watch lit found: update and exit *) + Vec.set atoms 1 ak; + Vec.set atoms k a.neg; + Vec.push ak.neg.watched c; + Log.debug 8 "New watcher (%a) for clause : %a" St.pp_atom ak.neg St.pp_clause c; + raise Exit + end + done; + (* no watch lit found *) + if first.neg.is_true then begin + (* clause is false *) + env.qhead <- Vec.size env.trail; + for k = i to Vec.size watched - 1 do + Vec.set watched !new_sz (Vec.get watched k); + incr new_sz; + done; + Log.debug 3 "Conflict found : %a" St.pp_clause c; + raise (Conflict c) + end + else begin + (* clause is unit *) + Vec.set watched !new_sz c; + incr new_sz; + Log.debug 5 "Unit clause : %a" St.pp_clause c; + enqueue first (decision_level ()) (Some c) + end + with Exit -> () + + let propagate_atom a res = + Log.debug 8 "Propagating %a" St.pp_atom a; + let watched = a.watched in + Log.debug 10 "Watching %a :" St.pp_atom a; + Vec.iter (fun c -> Log.debug 10 " %a" St.pp_clause c) watched; + let new_sz_w = ref 0 in + begin + try + for i = 0 to Vec.size watched - 1 do + let c = Vec.get watched i in + if not c.removed then propagate_in_clause a c i watched new_sz_w + done; + with Conflict c -> + assert (!res = None); + res := Some c + end; + let dead_part = Vec.size watched - !new_sz_w in + Vec.shrink watched dead_part + + (* Propagation (boolean and theory *) + let _th_cnumber = ref 0 + let slice_get i = (Vec.get env.trail i).lit + let slice_push l lemma = + decr _th_cnumber; + let atoms = List.rev_map (fun x -> add_atom x) l in + Iheap.grow_to_by_double env.order (St.nb_vars ()); + List.iter (fun a -> insert_var_order a.var) atoms; + add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma) + + let current_slice () = Th.({ + start = env.tatoms_qhead; + length = (Vec.size env.trail) - env.tatoms_qhead; + get = slice_get; + push = slice_push; + }) + + let rec theory_propagate () = + let head = Vec.size env.trail in + match Th.assume (current_slice ()) with + | Th.Sat _ -> + env.tatoms_qhead <- head; + propagate () + | Th.Unsat (l, p) -> + let l = List.rev_map St.add_atom l in + let c = St.make_clause (St.fresh_name ()) l (List.length l) true (Lemma p) in + Some c + + and propagate () = + if env.qhead = Vec.size env.trail then + None + else begin + let num_props = ref 0 in + let res = ref None in + while env.qhead < Vec.size env.trail do + let a = Vec.get env.trail env.qhead in + env.qhead <- env.qhead + 1; + incr num_props; + propagate_atom a res; + done; + env.propagations <- env.propagations + !num_props; + env.simpDB_props <- env.simpDB_props - !num_props; + match !res with + | None -> theory_propagate () + | _ -> !res + end + + (* heuristic comparison between clauses, by their size (unary/binary or not) + and activity *) + let f_sort_db c1 c2 = + let sz1 = Vec.size c1.atoms in + let sz2 = Vec.size c2.atoms in + let c = compare c1.activity c2.activity in + if sz1 = sz2 && c = 0 then 0 + else + if sz1 > 2 && (sz2 = 2 || c < 0) then -1 + else 1 + + (* returns true if the clause is used as a reason for a propagation, + and therefore can be needed in case of conflict. In this case + the clause can't be forgotten *) + let locked c = false (* + Vec.exists + (fun v -> match v.reason with + | Some c' -> c ==c' + | _ -> false + ) env.vars + *) + + (* remove some learnt clauses *) + let reduce_db () = () (* + let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in + Vec.sort env.learnts f_sort_db; + let lim2 = Vec.size env.learnts in + let lim1 = lim2 / 2 in + let j = ref 0 in + for i = 0 to lim1 - 1 do + let c = Vec.get env.learnts i in + if Vec.size c.atoms > 2 && not (locked c) then + remove_clause c + else + begin Vec.set env.learnts !j c; incr j end + done; + for i = lim1 to lim2 - 1 do + let c = Vec.get env.learnts i in + if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then + remove_clause c + else + begin Vec.set env.learnts !j c; incr j end + done; + Vec.shrink env.learnts (lim2 - !j) + *) + + (* remove from [vec] the clauses that are satisfied in the current trail *) + let remove_satisfied vec = + for i = 0 to Vec.size vec - 1 do + let c = Vec.get vec i in + if satisfied c then remove_clause c + done + + module HUC = Hashtbl.Make + (struct type t = clause let equal = (==) let hash = Hashtbl.hash end) + + let simplify () = + assert (decision_level () = 0); + if env.is_unsat then raise Unsat; + begin + match propagate () with + | Some confl -> report_unsat confl + | None -> () + end; + if nb_assigns() <> env.simpDB_assigns && env.simpDB_props <= 0 then begin + if Vec.size env.learnts > 0 then remove_satisfied env.learnts; + if env.remove_satisfied then remove_satisfied env.clauses; + (*Iheap.filter env.order f_filter f_weight;*) + env.simpDB_assigns <- nb_assigns (); + env.simpDB_props <- env.clauses_literals + env.learnts_literals; + end + + let search n_of_conflicts n_of_learnts = + let conflictC = ref 0 in + env.starts <- env.starts + 1; + while (true) do + match propagate () with + | Some confl -> (* Conflict *) + incr conflictC; + add_boolean_conflict confl + + | None -> (* No Conflict *) + if nb_assigns() = St.nb_vars () (* env.nb_init_vars *) then raise Sat; + if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then + begin + env.progress_estimate <- progress_estimate(); + cancel_until 0; + raise Restart + end; + if decision_level() = 0 then simplify (); + + if n_of_learnts >= 0 && + Vec.size env.learnts - nb_assigns() >= n_of_learnts then + reduce_db(); + + env.decisions <- env.decisions + 1; + + new_decision_level(); + let next = pick_branch_lit () in + let current_level = decision_level () in + assert (next.level < 0); + Log.debug 5 "Deciding on %a" St.pp_atom next.pa; + enqueue next.pa current_level None + done + + let check_clause c = + let b = ref false in + let atoms = c.atoms in + for i = 0 to Vec.size atoms - 1 do + let a = Vec.get atoms i in + b := !b || a.is_true + done; + assert (!b) + + let check_vec vec = + for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done + + (* + let check_model () = + check_vec env.clauses; + check_vec env.learnts + *) + + (* fixpoint of propagation and decisions until a model is found, or a + conflict is reached *) + let solve () = + if env.is_unsat then raise Unsat; + let n_of_conflicts = ref (to_float env.restart_first) in + let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in + try + while true do + begin try + search (to_int !n_of_conflicts) (to_int !n_of_learnts); + with Restart -> () + end; + n_of_conflicts := !n_of_conflicts *. env.restart_inc; + n_of_learnts := !n_of_learnts *. env.learntsize_inc; + done; + with + | Sat -> () + + let add_clauses cnf ~cnumber = + let aux cl = + add_clause ~cnumber cl (History []); + match propagate () with + | None -> () | Some confl -> report_unsat confl + in + List.iter aux cnf + + let init_solver cnf ~cnumber = + let nbv = St.nb_vars () in + let nbc = env.nb_init_clauses + List.length cnf in + Iheap.grow_to_by_double env.order nbv; + (* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *) + St.iter_vars insert_var_order; + Vec.grow_to_by_double env.model nbv; + Vec.grow_to_by_double env.clauses nbc; + Vec.grow_to_by_double env.learnts nbc; + env.nb_init_clauses <- nbc; + add_clauses cnf ~cnumber + + + let assume cnf ~cnumber = + let cnf = List.rev_map (List.rev_map St.add_atom) cnf in + init_solver cnf ~cnumber + + let eval lit = + let var, negated = make_var lit in + assert (var.pa.is_true || var.na.is_true); + let truth = var.pa.is_true in + if negated then not truth else truth + + let history () = env.learnts + + let unsat_conflict () = env.unsat_conflict + + type level = int + + let base_level = 0 + + let current_level () = Vec.size env.user_levels + + let push () = + let ul_trail = if Vec.is_empty env.trail_lim + then base_level + else Vec.last env.trail_lim + and ul_clauses = Vec.size env.clauses + and ul_learnt = Vec.size env.learnts in + Vec.push env.user_levels {ul_trail; ul_clauses;ul_learnt}; + Vec.size env.user_levels + + let pop l = + if l > current_level() + then invalid_arg "cannot pop() to level, it is too high"; + let ul = Vec.get env.user_levels l in + (* see whether we can reset [env.is_unsat] *) + if env.is_unsat && not (Vec.is_empty env.trail_lim) then ( + (* level at which the decision that lead to unsat was made *) + let last = Vec.last env.trail_lim in + if ul.ul_trail < last then env.is_unsat <- false + ); + cancel_until ul.ul_trail; + Vec.shrink env.clauses ul.ul_clauses; + Vec.shrink env.learnts ul.ul_learnt; + () + + let clear () = pop base_level +end + diff --git a/mcsolver/mcsolver.mli b/mcsolver/mcsolver.mli new file mode 100644 index 00000000..4d841daf --- /dev/null +++ b/mcsolver/mcsolver.mli @@ -0,0 +1,69 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Mohamed Iguernelala *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module Make (E : Expr_intf.S) + (Th : Theory_intf.S with type formula = E.Formula.t) : sig + (** Functor to create a SMT Solver parametrised by the atomic + formulas and a theory. *) + + exception Unsat + + module St : Mcsolver_types.S + with type formula = E.Formula.t + + module Proof : Res.S + with type atom = St.atom + and type clause = St.clause + and type lemma = Th.proof + + val solve : unit -> unit + (** Try and solves the current set of assumptions. + @return () if the current set of clauses is satisfiable + @raise Unsat if a toplevel conflict is found *) + + val assume : E.Formula.t list list -> cnumber:int -> unit + (** Add the list of clauses to the current set of assumptions. + Modifies the sat solver state in place. + @raise Unsat if a conflict is detect when adding the clauses *) + + val eval : E.Formula.t -> bool + (** Returns the valuation of a formula in the current state + of the sat solver. *) + + val history : unit -> St.clause Vec.t + (** Returns the history of learnt clauses, in the right order. *) + + val unsat_conflict : unit -> St.clause option + (** Returns the unsat clause found at the toplevel, if it exists (i.e if + [solve] has raised [Unsat]) *) + + type level + (** Abstract notion of assumption level. *) + + val base_level : level + (** Level with no assumption at all, corresponding to the empty solver *) + + val current_level : unit -> level + (** The current level *) + + val push : unit -> level + (** Create a new level that extends the previous one. *) + + val pop : level -> unit + (** Go back to the given level, forgetting every assumption added since. + @raise Invalid_argument if the current level is below the argument *) + + val clear : unit -> unit + (** Return to level {!base_level} *) +end + diff --git a/mcsolver/mcsolver_types.ml b/mcsolver/mcsolver_types.ml new file mode 100644 index 00000000..9fede52c --- /dev/null +++ b/mcsolver/mcsolver_types.ml @@ -0,0 +1,213 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +open Printf + +module type S = Mcsolver_types_intf.S + +module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct + + type formula = E.Formula.t + type proof = Th.proof + + type var = + { vid : int; + pa : atom; + na : atom; + mutable weight : float; + mutable seen : bool; + mutable level : int; + mutable reason: reason; + mutable vpremise : premise} + + and atom = + { var : var; + lit : formula; + neg : atom; + mutable watched : clause Vec.t; + mutable is_true : bool; + aid : int } + + and clause = + { name : string; + atoms : atom Vec.t ; + mutable activity : float; + mutable removed : bool; + learnt : bool; + cpremise : premise } + + and reason = clause option + + and premise = + | History of clause list + | Lemma of proof + + let dummy_lit = E.dummy + + let rec dummy_var = + { vid = -101; + pa = dummy_atom; + na = dummy_atom; + level = -1; + reason = None; + weight = -1.; + seen = false; + vpremise = History [] } + and dummy_atom = + { var = dummy_var; + lit = dummy_lit; + watched = Obj.magic 0; + (* should be [Vec.make_empty dummy_clause] + but we have to break the cycle *) + neg = dummy_atom; + is_true = false; + aid = -102 } + + let dummy_clause = + { name = ""; + atoms = Vec.make_empty dummy_atom; + activity = -1.; + removed = false; + learnt = false; + cpremise = History [] } + + let () = + dummy_atom.watched <- Vec.make_empty dummy_clause + + module MA = Map.Make(E.Formula) + + let normal_form = E.norm + + let ma = ref MA.empty + let vars = Vec.make 107 dummy_var + + let nb_vars () = Vec.size vars + let get_var i = Vec.get vars i + let iter_vars f = Vec.iter f vars + + let cpt_mk_var = ref 0 + let make_var = + fun lit -> + let lit, negated = normal_form lit in + try MA.find lit !ma, negated + with Not_found -> + let cpt_fois_2 = !cpt_mk_var lsl 1 in + let rec var = + { vid = !cpt_mk_var; + pa = pa; + na = na; + level = -1; + reason = None; + weight = 0.; + seen = false; + vpremise = History []; + } + and pa = + { var = var; + lit = lit; + watched = Vec.make 10 dummy_clause; + neg = na; + is_true = false; + aid = cpt_fois_2 (* aid = vid*2 *) } + and na = + { var = var; + lit = E.neg lit; + watched = Vec.make 10 dummy_clause; + neg = pa; + is_true = false; + aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in + ma := MA.add lit var !ma; + incr cpt_mk_var; + Vec.push vars var; + assert (Vec.get vars var.vid == var && !cpt_mk_var = Vec.size vars); + var, negated + + let add_atom lit = + let var, negated = make_var lit in + if negated then var.na else var.pa + + let make_clause name ali sz_ali is_learnt premise = + let atoms = Vec.from_list ali sz_ali dummy_atom in + { name = name; + atoms = atoms; + removed = false; + learnt = is_learnt; + activity = 0.; + cpremise = premise} + + let empty_clause = make_clause "Empty" [] 0 false (History []) + + let fresh_lname = + let cpt = ref 0 in + fun () -> incr cpt; "L" ^ (string_of_int !cpt) + + let fresh_dname = + let cpt = ref 0 in + fun () -> incr cpt; "D" ^ (string_of_int !cpt) + + let fresh_name = + let cpt = ref 0 in + fun () -> incr cpt; "C" ^ (string_of_int !cpt) + + let clear () = + cpt_mk_var := 0; + ma := MA.empty + + (* Pretty printing for atoms and clauses *) + let print_atom fmt a = E.Formula.print fmt a.lit + + let print_atoms fmt v = + print_atom fmt (Vec.get v 0); + if (Vec.size v) > 1 then begin + for i = 1 to (Vec.size v) - 1 do + Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i) + done + end + + let print_clause fmt c = + Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms + + (* Complete debug printing *) + let sign a = if a==a.var.pa then "" else "-" + + let level a = + match a.var.level, a.var.reason with + | n, _ when n < 0 -> assert false + | 0, Some c -> sprintf "->0/%s" c.name + | 0, None -> "@0" + | n, Some c -> sprintf "->%d/%s" n c.name + | n, None -> sprintf "@@%d" n + + let value a = + if a.is_true then sprintf "[T%s]" (level a) + else if a.neg.is_true then sprintf "[F%s]" (level a) + else "" + + let pp_premise b = function + | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v + | Lemma _ -> bprintf b "th_lemma" + + let pp_atom b a = + bprintf b "%s%d%s [lit:%s] vpremise={{%a}}" + (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit) + pp_premise a.var.vpremise + + let pp_atoms_vec b vec = + for i = 0 to Vec.size vec - 1 do + bprintf b "%a ; " pp_atom (Vec.get vec i) + done + + let pp_clause b {name=name; atoms=arr; cpremise=cp; learnt=learnt} = + bprintf b "%s%s{ %a} cpremise={{%a}}" name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp + +end diff --git a/sat/explanation.mli b/mcsolver/mcsolver_types.mli similarity index 72% rename from sat/explanation.mli rename to mcsolver/mcsolver_types.mli index e39650a6..02170f85 100644 --- a/sat/explanation.mli +++ b/mcsolver/mcsolver_types.mli @@ -4,15 +4,15 @@ (* Combining model checking algorithms and SMT solvers *) (* *) (* Sylvain Conchon and Alain Mebsout *) -(* Stephane Lescuyer *) -(* INRIA, Universite Paris-Sud 11 *) +(* Universite Paris-Sud 11 *) (* *) (* Copyright 2011. This file is distributed under the terms of the *) (* Apache Software License version 2.0 *) (* *) (**************************************************************************) -module type S = Explanation_intf.S +module type S = Solver_types_intf.S -module Make : functor (St : Solver_types.S) -> S with type atom = St.atom -(** Functor to create the types of explanations used in the Solver Module. *) +module Make : functor (E : Expr_intf.S)(Th : Theory_intf.S) + -> S with type formula = E.Formula.t and type proof = Th.proof +(** Functor to instantiate the types of clauses for the Solver. *) diff --git a/sat/solver_types_intf.ml b/mcsolver/mcsolver_types_intf.ml similarity index 100% rename from sat/solver_types_intf.ml rename to mcsolver/mcsolver_types_intf.ml diff --git a/sat/theory_intf.ml b/mcsolver/plugin_intf.ml similarity index 100% rename from sat/theory_intf.ml rename to mcsolver/plugin_intf.ml diff --git a/msat.mlpack b/msat.mlpack index 06c0082b..b23032f6 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -1,34 +1,26 @@ -# Sat Modules -Explanation +# Solver Modules Formula_intf -Res -Sat Solver Solver_types Theory_intf + +# Mcsat Solver modules +Expr_intf +Mcsolver +Mcsolver_types +Plugin_intf + +# Auxiliary modules +Res Tseitin Tseitin_intf +# Sat modules +Sat + # Smt Modules Cc Sig Smt Unionfind -# Old modules -#Arith -#Cc -#Combine -#Exception -#Fm -#Intervals -#Literal -#Polynome -#Smt -#Sum -#Symbols -#Term -#Ty -#Uf -#Use - diff --git a/sat/explanation.ml b/sat/explanation.ml deleted file mode 100644 index 08171473..00000000 --- a/sat/explanation.ml +++ /dev/null @@ -1,72 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Stephane Lescuyer *) -(* INRIA, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Format - -module type S = Explanation_intf.S - -module Make(Stypes : Solver_types.S) = struct - - type atom = Stypes.atom - - type exp = Atom of atom | Fresh of int - - module S = Set.Make(struct - type t = exp - let compare a b = match a,b with - | Atom _, Fresh _ -> -1 - | Fresh _, Atom _ -> 1 - | Fresh i1, Fresh i2 -> i1 - i2 - | Atom a, Atom b -> Stypes.(a.aid - b.aid) - end) - - type t = S.t - - let singleton e = S.singleton (Atom e) - - let empty = S.empty - - let union s1 s2 = S.union s1 s2 - - let iter_atoms f s = - S.iter (fun e -> match e with - | Fresh _ -> () - | Atom a -> f a) s - - let fold_atoms f s acc = - S.fold (fun e acc -> match e with - | Fresh _ -> acc - | Atom a -> f a acc) s acc - - let merge e1 e2 = e1 - - let fresh_exp = - let r = ref (-1) in - fun () -> incr r; !r - - let remove_fresh i s = - let fi = Fresh i in - if S.mem fi s then Some (S.remove fi s) - else None - - let add_fresh i = S.add (Fresh i) - - let print fmt ex = - fprintf fmt "{"; - S.iter (function - | Atom a -> fprintf fmt "%s, " (Log.on_buffer Stypes.pp_atom a) - | Fresh i -> fprintf fmt "Fresh%d " i) ex; - fprintf fmt "}" - -end diff --git a/sat/explanation_intf.ml b/sat/explanation_intf.ml deleted file mode 100644 index 4e8f52af..00000000 --- a/sat/explanation_intf.ml +++ /dev/null @@ -1,36 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Stephane Lescuyer *) -(* INRIA, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -module type S = sig - (** Signature for explanations. To be modified to allow passing bulks of assumptions to the theories. *) - - type t - type exp - type atom - - val empty : t - val singleton : atom -> t - - val union : t -> t -> t - val merge : t -> t -> t - - val iter_atoms : (atom -> unit) -> t -> unit - val fold_atoms : (atom -> 'a -> 'a ) -> t -> 'a -> 'a - - val fresh_exp : unit -> int - val add_fresh : int -> t -> t - val remove_fresh : int -> t -> t option - - val print : Format.formatter -> t -> unit -end diff --git a/sat/.merlin b/solver/.merlin similarity index 100% rename from sat/.merlin rename to solver/.merlin diff --git a/sat/formula_intf.ml b/solver/formula_intf.ml similarity index 100% rename from sat/formula_intf.ml rename to solver/formula_intf.ml diff --git a/sat/res.ml b/solver/res.ml similarity index 100% rename from sat/res.ml rename to solver/res.ml diff --git a/sat/res.mli b/solver/res.mli similarity index 100% rename from sat/res.mli rename to solver/res.mli diff --git a/sat/res_intf.ml b/solver/res_intf.ml similarity index 100% rename from sat/res_intf.ml rename to solver/res_intf.ml diff --git a/sat/solver.ml b/solver/solver.ml similarity index 100% rename from sat/solver.ml rename to solver/solver.ml diff --git a/sat/solver.mli b/solver/solver.mli similarity index 100% rename from sat/solver.mli rename to solver/solver.mli diff --git a/sat/solver_types.ml b/solver/solver_types.ml similarity index 100% rename from sat/solver_types.ml rename to solver/solver_types.ml diff --git a/sat/solver_types.mli b/solver/solver_types.mli similarity index 100% rename from sat/solver_types.mli rename to solver/solver_types.mli diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml new file mode 100644 index 00000000..724bc3f3 --- /dev/null +++ b/solver/solver_types_intf.ml @@ -0,0 +1,95 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module type S = sig + (** The signatures of clauses used in the Solver. *) + + type formula + type proof + + type var = { + vid : int; + pa : atom; + na : atom; + mutable weight : float; + mutable seen : bool; + mutable level : int; + mutable reason : reason; + mutable vpremise : premise + } + + and atom = { + var : var; + lit : formula; + neg : atom; + mutable watched : clause Vec.t; + mutable is_true : bool; + aid : int + } + + and clause = { + name : string; + atoms : atom Vec.t; + mutable activity : float; + mutable removed : bool; + learnt : bool; + cpremise : premise + } + + and reason = clause option + and premise = + | History of clause list + | Lemma of proof + (** Recursive types for literals (atoms) and clauses *) + + val dummy_var : var + val dummy_atom : atom + val dummy_clause : clause + (** Dummy values for use in vector dummys *) + + val empty_clause : clause + (** The empty clause *) + + val add_atom : formula -> atom + (** Returns the atom associated with the given formula *) + + val make_var : formula -> var * bool + (** Returns the variable linked with the given formula, and wether the atom associated with the formula + is [var.pa] or [var.na] *) + + val make_clause : string -> atom list -> int -> bool -> premise -> clause + (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *) + + val nb_vars : unit -> int + val get_var : int -> var + val iter_vars : (var -> unit) -> unit + (** Read access to the vector of variables created *) + + val fresh_name : unit -> string + val fresh_lname : unit -> string + val fresh_dname : unit -> string + (** Fresh names for clauses *) + + val clear : unit -> unit + (** Forget all variables cretaed *) + + val print_atom : Format.formatter -> atom -> unit + val print_clause : Format.formatter -> clause -> unit + (** Pretty printing functions for atoms and clauses *) + + val pp_atom : Buffer.t -> atom -> unit + val pp_clause : Buffer.t -> clause -> unit + (** Debug function for atoms and clauses (very verbose) *) + +end + diff --git a/solver/theory_intf.ml b/solver/theory_intf.ml new file mode 100644 index 00000000..8358f3e7 --- /dev/null +++ b/solver/theory_intf.ml @@ -0,0 +1,61 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon, Evelyne Contejean *) +(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) +(* CNRS, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module type S = sig + (** Singature for theories to be given to the Solver. *) + + type formula + (** The type of formulas. Should be compatble with Formula_intf.S *) + + type proof + (** A custom type for the proofs of lemmas produced by the theory. *) + + type slice = { + start : int; + length : int; + get : int -> formula; + push : formula list -> proof -> unit; + } + (** The type for a slice of litterals to assume/propagate in the theory. + [get] operations should only be used for integers [ start <= i < start + length]. + [push clause proof] allows to add a tautological clause to the sat solver. *) + + type level + (** The type for levels to allow backtracking. *) + + (** Type returned by the theory, either the current set of assumptions is satisfiable, + or it is not, in which case a tautological clause (hopefully minimal) is returned. + Formulas in the unsat clause must come from the current set of assumptions, i.e + must have been encountered in a slice. *) + type res = + | Sat of level + | Unsat of formula list * proof + + val dummy : level + (** A dummy level. *) + + val current_level : unit -> level + (** Return the current level of the theory (either the empty/beginning state, or the + last level returned by the [assume] function). *) + + val assume : slice -> res + (** Assume the formulas in the slice, possibly pushing new formulas to be propagated, + and returns the result of the new assumptions. *) + + val backtrack : level -> unit + (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the + same state as when it returned the value [l], *) + +end + diff --git a/sat/tseitin.ml b/solver/tseitin.ml similarity index 100% rename from sat/tseitin.ml rename to solver/tseitin.ml diff --git a/sat/tseitin.mli b/solver/tseitin.mli similarity index 100% rename from sat/tseitin.mli rename to solver/tseitin.mli diff --git a/sat/tseitin_intf.ml b/solver/tseitin_intf.ml similarity index 100% rename from sat/tseitin_intf.ml rename to solver/tseitin_intf.ml