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

Better clause names

Browse source
This commit is contained in:
Guillaume Bury 2015-03-13 14:31:46 +01:00
parent cddf914ce6
commit 0050fdae3c
5 changed files with 18 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
smt/mcsat.ml
View file

@ -123,7 +123,6 @@ module Make(Dummy:sig end) = struct
| Sat | Sat
| Unsat | Unsat
let _i = ref 0
let solve () = let solve () =
try try
SmtSolver.solve (); SmtSolver.solve ();
@ -131,9 +130,8 @@ module Make(Dummy:sig end) = struct
with SmtSolver.Unsat -> Unsat with SmtSolver.Unsat -> Unsat
let assume l = let assume l =
incr _i;
try try
SmtSolver.assume l !_i SmtSolver.assume l
with SmtSolver.Unsat -> () with SmtSolver.Unsat -> ()
let get_proof () = let get_proof () =

16
solver/mcsolver.ml
View file

@ -622,7 +622,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
let atoms = List.rev_map (fun x -> new_atom x) l in let atoms = List.rev_map (fun x -> new_atom x) l in
Iheap.grow_to_by_double env.order (St.nb_vars ()); Iheap.grow_to_by_double env.order (St.nb_vars ());
List.iter (fun a -> insert_var_order (Either.mk_right a.var)) atoms; List.iter (fun a -> insert_var_order (Either.mk_right a.var)) atoms;
add_clause "lemma" atoms (Lemma lemma) add_clause (fresh_tname ()) atoms (Lemma lemma)
let slice_propagate f lvl = let slice_propagate f lvl =
let a = add_atom f in let a = add_atom f in
@ -655,7 +655,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
let l = List.rev_map new_atom l in let l = List.rev_map new_atom l in
Iheap.grow_to_by_double env.order (St.nb_vars ()); Iheap.grow_to_by_double env.order (St.nb_vars ());
List.iter (fun a -> insert_var_order (Either.mk_right a.var)) l; List.iter (fun a -> insert_var_order (Either.mk_right a.var)) l;
let c = St.make_clause (St.fresh_name ()) l (List.length l) true (Lemma p) in let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) in
Some c Some c
and propagate () = and propagate () =
@ -819,9 +819,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
let check_vec vec = let check_vec vec =
for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done
let add_clauses cnf ~cnumber = let add_clauses cnf =
let aux cl = let aux cl =
add_clause "hyp" cl (History []); add_clause (fresh_hname ()) cl (History []);
match propagate () with match propagate () with
| None -> () | Some confl -> report_unsat confl | None -> () | Some confl -> report_unsat confl
in in
@ -850,7 +850,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
with with
| Sat -> () | Sat -> ()
let init_solver cnf ~cnumber = let init_solver cnf =
let nbv = St.nb_vars () in let nbv = St.nb_vars () in
let nbc = env.nb_init_clauses + List.length cnf in let nbc = env.nb_init_clauses + List.length cnf in
Iheap.grow_to_by_double env.order nbv; Iheap.grow_to_by_double env.order nbv;
@ -863,11 +863,11 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
(fun v -> L.debug 50 " -- %a" St.pp_semantic_var v) (fun v -> L.debug 50 " -- %a" St.pp_semantic_var v)
(fun a -> L.debug 50 " -- %a" St.pp_atom a.tag.pa) (fun a -> L.debug 50 " -- %a" St.pp_atom a.tag.pa)
); );
add_clauses cnf ~cnumber add_clauses cnf
let assume cnf ~cnumber = let assume cnf =
let cnf = List.rev_map (List.rev_map St.add_atom) cnf in let cnf = List.rev_map (List.rev_map St.add_atom) cnf in
init_solver cnf ~cnumber init_solver cnf
let eval lit = let eval lit =
let var, negated = make_boolean_var lit in let var, negated = make_boolean_var lit in

2
solver/mcsolver.mli
View file

@ -24,7 +24,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
@return () if the current set of clauses is satisfiable @return () if the current set of clauses is satisfiable
@raise Unsat if a toplevel conflict is found *) @raise Unsat if a toplevel conflict is found *)
val assume : E.Formula.t list list -> cnumber:int -> unit val assume : E.Formula.t list list -> unit
(** Add the list of clauses to the current set of assumptions. (** Add the list of clauses to the current set of assumptions.
Modifies the sat solver state in place. Modifies the sat solver state in place.
@raise Unsat if a conflict is detect when adding the clauses *) @raise Unsat if a conflict is detect when adding the clauses *)

8
solver/mcsolver_types.ml
View file

@ -185,9 +185,13 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
let cpt = ref 0 in let cpt = ref 0 in
fun () -> incr cpt; "L" ^ (string_of_int !cpt) fun () -> incr cpt; "L" ^ (string_of_int !cpt)
let fresh_dname = let fresh_hname =
let cpt = ref 0 in let cpt = ref 0 in
fun () -> incr cpt; "D" ^ (string_of_int !cpt) fun () -> incr cpt; "H" ^ (string_of_int !cpt)
let fresh_tname =
let cpt = ref 0 in
fun () -> incr cpt; "T" ^ (string_of_int !cpt)
let fresh_name = let fresh_name =
let cpt = ref 0 in let cpt = ref 0 in

3
solver/mcsolver_types_intf.ml
View file

@ -91,7 +91,8 @@ module type S = sig
val fresh_name : unit -> string val fresh_name : unit -> string
val fresh_lname : unit -> string val fresh_lname : unit -> string
val fresh_dname : unit -> string val fresh_tname : unit -> string
val fresh_hname : unit -> string
(** Fresh names for clauses *) (** Fresh names for clauses *)
val proof_debug : proof -> string * (atom list) * (semantic var list) * (string option) val proof_debug : proof -> string * (atom list) * (semantic var list) * (string option)