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

Small fix for tautologies in cc for smt

Browse source
This commit is contained in:
Guillaume Bury 2014-11-14 17:53:16 +01:00
parent 566c30bdcc
commit fcbcf5a9d4
1 changed files with 11 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
smt/smt.ml
View file

@ -70,38 +70,37 @@ module Tsmt = struct
get : int -> formula;
push : formula -> formula list -> proof -> unit;
}
type level = U.t
type level = {
uf : U.t;
seen : formula list
}
type res =
| Sat of level
| Unsat of formula list * proof
let dummy = U.empty
let dummy = { uf = U.empty; seen = [] }
let env = ref U.empty
let env = ref dummy
let current_level () = !env
let temp = ref []
let assume s =
try
for i = s.start to s.start + s.length - 1 do
match s.get i with
| Fsmt.Fresh _ -> ()
| Fsmt.Equal (i, j) as f ->
temp := f :: !temp;
env := U.union !env i j
env := { !env with seen = f :: !env.seen };
env := { !env with uf = U.union !env.uf i j }
| Fsmt.Distinct (i, j) as f ->
temp := f :: !temp;
env := U.forbid !env i j
env := { !env with seen = f :: !env.seen };
env := { !env with uf = U.forbid !env.uf i j }
| _ -> assert false
done;
Sat (current_level ())
with U.Unsat ->
match !temp with
| _ :: _ -> Unsat (List.rev_map Fsmt.neg !temp, ())
| _ -> assert false
Unsat (List.rev_map Fsmt.neg !env.seen, ())
let backtrack l = env := l