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

Added (dummy) mcsat module for test binary

Browse source
This commit is contained in:
Guillaume Bury 2016-09-14 19:55:57 +02:00
parent 4522aa3ddc
commit 2a33534312
7 changed files with 23 additions and 165 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
Makefile
View file

@ -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))

2
_tags
View file

@ -9,10 +9,10 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
<src/core>: include
<src/solver>: include
<src/backend>: include
<src/util>: include
<src/sat>: include
<src/smt>: include
<src/mcsat>: include
<src/util>: include
# Pack options
<src/core/*.cmx>: for-pack(Msat)

3
src/main.ml
View file

@ -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)

11
src/mcsat/mcsat.ml Normal file
View file

@ -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)

8
src/mcsat/mcsat.mli Normal file
View file

@ -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

114
src/smt/mcsat.ml
View file

@ -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

47
src/smt/smt.ml
View file

@ -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)