simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Still in extreme debug mode

Browse source
This commit is contained in:
Guillaume Bury 2015-03-15 22:00:48 +01:00
parent c5fd429821
commit 5a61a6c852
3 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
solver/mcsolver.ml
View file

@ -7,7 +7,7 @@ Copyright 2014 Simon Cruanes
module Make (L : Log_intf.S)(E : Expr_intf.S) module Make (L : Log_intf.S)(E : Expr_intf.S)
(Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct
module St = Mcsolver_types.Make(E)(Th) module St = Mcsolver_types.Make(L)(E)(Th)
module Proof = Mcproof.Make(L)(St) module Proof = Mcproof.Make(L)(St)
open St open St

10
solver/mcsolver_types.ml
View file

@ -15,7 +15,7 @@ open Printf
module type S = Mcsolver_types_intf.S module type S = Mcsolver_types_intf.S
module Make (E : Expr_intf.S)(Th : Plugin_intf.S with module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
type formula = E.Formula.t and type term = E.Term.t) = struct type formula = E.Formula.t and type term = E.Term.t) = struct
(* Types declarations *) (* Types declarations *)
@ -130,9 +130,11 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
let make_boolean_var = let make_boolean_var =
fun lit -> fun lit ->
L.debug 100 "normalizing lit";
let lit, negated = E.norm lit in let lit, negated = E.norm lit in
try MF.find f_map lit, negated try MF.find f_map lit, negated
with Not_found -> with Not_found ->
L.debug 100 "Lit not in table";
let cpt_fois_2 = !cpt_mk_var lsl 1 in let cpt_fois_2 = !cpt_mk_var lsl 1 in
let rec var = let rec var =
{ vid = !cpt_mk_var; { vid = !cpt_mk_var;
@ -157,16 +159,22 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
neg = pa; neg = pa;
is_true = false; is_true = false;
aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
L.debug 100 "adding lit to table...";
MF.add f_map lit var; MF.add f_map lit var;
L.debug 100 "done";
incr cpt_mk_var; incr cpt_mk_var;
Vec.push vars (Either.mk_right var); Vec.push vars (Either.mk_right var);
L.debug 100 "iterating on new lit...";
Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit; Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit;
L.debug 100 "done";
var, negated var, negated
let add_term t = make_semantic_var t let add_term t = make_semantic_var t
let add_atom lit = let add_atom lit =
Log.debug 100 "entering add_atom";
let var, negated = make_boolean_var lit in let var, negated = make_boolean_var lit in
Log.debug 100 "found atom";
if negated then var.tag.na else var.tag.pa if negated then var.tag.na else var.tag.pa
let make_clause name ali sz_ali is_learnt premise = let make_clause name ali sz_ali is_learnt premise =

2
solver/mcsolver_types.mli
View file

@ -13,7 +13,7 @@
module type S = Mcsolver_types_intf.S module type S = Mcsolver_types_intf.S
module Make : functor (E : Expr_intf.S)(Th : Plugin_intf.S with module Make : functor (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
type term = E.Term.t and type formula = E.Formula.t) type term = E.Term.t and type formula = E.Formula.t)
-> S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof -> S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof
(** Functor to instantiate the types of clauses for the Solver. *) (** Functor to instantiate the types of clauses for the Solver. *)