From 2a3353431251ef0ef6e141033597f9c251da7f67 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 14 Sep 2016 19:55:57 +0200 Subject: [PATCH] Added (dummy) mcsat module for test binary --- Makefile | 3 +- _tags | 2 +- src/main.ml | 3 -- src/mcsat/mcsat.ml | 11 +++++ src/mcsat/mcsat.mli | 8 ++++ src/smt/mcsat.ml | 114 -------------------------------------------- src/smt/smt.ml | 47 +----------------- 7 files changed, 23 insertions(+), 165 deletions(-) create mode 100644 src/mcsat/mcsat.ml create mode 100644 src/mcsat/mcsat.mli delete mode 100644 src/smt/mcsat.ml diff --git a/Makefile b/Makefile index 328cc6dc..498c8e7d 100644 --- a/Makefile +++ b/Makefile @@ -53,8 +53,9 @@ log: clean: $(COMP) -clean + rm -rf $(NAME_BIN) -ALL_NAMES = $(NAME_CORE) $(NAME_SAT) $(NAME_SMT) +ALL_NAMES = $(NAME_CORE) # $(NAME_SAT) $(NAME_SMT) $(NAME_MCAT) TO_INSTALL_LIB=$(addsuffix .a, $(ALL_NAMES)) \ $(addsuffix .cmi, $(ALL_NAMES)) TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(TO_INSTALL_LIB)) diff --git a/_tags b/_tags index f350c48a..e737cd45 100644 --- a/_tags +++ b/_tags @@ -9,10 +9,10 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20) : include : include : include +: include : include : include : include -: include # Pack options : for-pack(Msat) diff --git a/src/main.ml b/src/main.ml index 521f5c6c..3ce4dd3f 100644 --- a/src/main.ml +++ b/src/main.ml @@ -5,11 +5,8 @@ Copyright 2014 Simon Cruanes *) module Sat = Sat.Make(struct end) -module Dummy = Sat module Smt = Smt.Make(struct end) - (* module Mcsat = Mcsat.Make(struct end) - *) module P = Dolmen.Logic.Make(Dolmen.ParseLocation) diff --git a/src/mcsat/mcsat.ml b/src/mcsat/mcsat.ml new file mode 100644 index 00000000..5acf092d --- /dev/null +++ b/src/mcsat/mcsat.ml @@ -0,0 +1,11 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Th = Solver.DummyTheory(Expr_smt.Atom) + +module Make(Dummy:sig end) = + Solver.Make(Expr_smt.Atom)(Th)(struct end) + diff --git a/src/mcsat/mcsat.mli b/src/mcsat/mcsat.mli new file mode 100644 index 00000000..edb13401 --- /dev/null +++ b/src/mcsat/mcsat.mli @@ -0,0 +1,8 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Make(Dummy: sig end) : Solver.S with type St.formula = Expr_smt.atom + diff --git a/src/smt/mcsat.ml b/src/smt/mcsat.ml deleted file mode 100644 index 9be8e7bc..00000000 --- a/src/smt/mcsat.ml +++ /dev/null @@ -1,114 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Fsmt = Expr - -module Tsmt = struct - - module M = Map.Make(Fsmt.Term) - module CC = Cc.Make(String) - - (* Type definitions *) - type term = Fsmt.Term.t - type formula = Fsmt.t - type proof = unit - - type level = { - cc : CC.t; - assign : (term * int) M.t; - } - - (* Functions *) - let dummy = { cc = CC.empty; assign = M.empty; } - - let env = ref dummy - - let current_level () = !env - - let to_clause (a, b, l) = - Log.debugf 10 "@[<2>Expl : %s; %s@ %a@]" - (fun k->k a b - (fun out () -> List.iter (Format.fprintf out " |- %s@ ") l) ()); - let rec aux acc = function - | [] | [_] -> acc - | x :: ((y :: _) as r) -> - aux (Fsmt.mk_eq x y :: acc) r - in - (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) - - let assume s = - let open Plugin_intf in - try - for i = s.start to s.start + s.length - 1 do - match s.get i with - | Assign (x, v, lvl) -> - env := { !env with assign = M.add x (v, lvl) !env.assign } - | Lit f -> - Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print f); - match f with - | Fsmt.Prop _ -> () - | Fsmt.Equal (i, j) -> - env := { !env with cc = CC.add_eq !env.cc i j } - | Fsmt.Distinct (i, j) -> - env := { !env with cc = CC.add_neq !env.cc i j } - done; - Sat - with CC.Unsat x -> - Log.debug 8 "Making explanation clause..."; - Unsat (to_clause x, ()) - - let backtrack l = env := l - - let assign t = CC.repr !env.cc t - - let iter_assignable f = function - | Fsmt.Prop _ -> () - | Fsmt.Equal(a, b) - | Fsmt.Distinct (a, b) -> f a; f b - - let max (a: int) (b: int) = if a < b then b else a - - let eval = function - | Fsmt.Prop _ -> Plugin_intf.Unknown - | Fsmt.Equal (a, b) -> - begin try - let a', lvl_a = M.find a !env.assign in - let b', lvl_b = M.find b !env.assign in - Plugin_intf.Valued (Fsmt.Term.equal a' b', max lvl_a lvl_b) - with Not_found -> - Plugin_intf.Unknown - end - | Fsmt.Distinct (a, b) -> - begin try - let a', lvl_a = M.find a !env.assign in - let b', lvl_b = M.find b !env.assign in - Plugin_intf.Valued (not (Fsmt.Term.equal a' b'), max lvl_a lvl_b) - with Not_found -> - Plugin_intf.Unknown - end - - let if_sat _ = () - -end - -module Make(Dummy:sig end) = struct - - include Mcsolver.Make(Fsmt)(Tsmt)(struct end) - module Dot = Dot.Make(Proof)(struct - let print_atom = St.print_atom - let lemma_info () = "Proof", Some "PURPLE", [] - end) - module Dedukti = Dedukti.Make(Proof)(struct - let print _ _ = () - let prove _ _ = () - let context _ _ = () - end) - - let print_clause = St.print_clause - let print_dot = Dot.print - let print_dedukti = Dedukti.print - -end diff --git a/src/smt/smt.ml b/src/smt/smt.ml index f80984fb..5acf092d 100644 --- a/src/smt/smt.ml +++ b/src/smt/smt.ml @@ -6,51 +6,6 @@ Copyright 2014 Simon Cruanes module Th = Solver.DummyTheory(Expr_smt.Atom) - (* struct - module CC = Cc.Make(String) - - type formula = Fsmt.t - type proof = unit - type level = CC.t - - let dummy = CC.empty - - let env = ref dummy - - let current_level () = !env - - let to_clause (a, b, l) = - Log.debugf 10 "@[Expl : %s; %s@ %a@]" - (fun k->k a b - (fun out () -> List.iter (Format.fprintf out "|- %s@ ") l) ()); - let rec aux acc = function - | [] | [_] -> acc - | x :: ((y :: _) as r) -> - aux (Fsmt.mk_eq x y :: acc) r - in - (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) - - let assume s = - let open Theory_intf in - try - for i = s.start to s.start + s.length - 1 do - Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print (s.get i)); - match s.get i with - | Fsmt.Prop _ -> () - | Fsmt.Equal (i, j) -> env := CC.add_eq !env i j - | Fsmt.Distinct (i, j) -> env := CC.add_neq !env i j - done; - Sat - with CC.Unsat x -> - Log.debug 8 "Making explanation clause..."; - Unsat (to_clause x, ()) - - let backtrack l = env := l - - let if_sat _ = () - -end - *) - module Make(Dummy:sig end) = Solver.Make(Expr_smt.Atom)(Th)(struct end) +