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

avoid duplicating the definition of slices in Theory_intf

Browse source
This commit is contained in:
Simon Cruanes 2016-07-01 15:25:10 +02:00
parent 66740e5de8
commit 403347ddaf
3 changed files with 14 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
smt/smt.ml
View file

@ -5,6 +5,7 @@ Copyright 2014 Simon Cruanes
*)
module Fsmt = Expr
module ThI = Theory_intf
module Tsmt = struct
@ -12,12 +13,6 @@ module Tsmt = struct
type formula = Fsmt.t
type proof = unit
type slice = {
start : int;
length : int;
get : int -> formula;
push : formula list -> proof -> unit;
}
type level = CC.t
type res =
@ -43,9 +38,9 @@ module Tsmt = struct
let assume s =
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
for i = s.ThI.start to s.ThI.start + s.ThI.length - 1 do
Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print (s.ThI.get i));
match s.ThI.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

10
solver/solver.ml
View file

@ -11,6 +11,7 @@
(**************************************************************************)
module type S = Solver_intf.S
module ThI = Theory_intf
module DummyTheory(F : Formula_intf.S) = struct
(* We don't have anything to do since the SAT Solver already
@ -75,10 +76,11 @@ module Plugin(E : Formula_intf.S)
let assume s =
match Th.assume {
Th.start = s.start;
Th.length = s.length;
Th.get = assume_get s;
Th.push = s.push;
ThI.
start = s.start;
length = s.length;
get = assume_get s;
push = s.push;
} with
| Th.Sat _ -> Sat
| Th.Unsat (l, p) -> Unsat (l, p)

15
solver/theory_intf.ml
View file

@ -18,6 +18,9 @@ type ('form, 'proof) slice = {
get : int -> 'form;
push : 'form list -> 'proof -> unit;
}
(** The type for a slice of literals to assume/propagate in the theory.
[get] operations should only be used for integers [ start <= i < start + length].
[push clause proof] allows to add a tautological clause to the sat solver. *)
module type S = sig
(** Signature for theories to be given to the Solver. *)
@ -28,16 +31,6 @@ module type S = sig
type proof
(** A custom type for the proofs of lemmas produced by the theory. *)
type slice = {
start : int;
length : int;
get : int -> formula;
push : formula list -> proof -> unit;
}
(** The type for a slice of literals to assume/propagate in the theory.
[get] operations should only be used for integers [ start <= i < start + length].
[push clause proof] allows to add a tautological clause to the sat solver. *)
type level
(** The type for levels to allow backtracking. *)
@ -56,7 +49,7 @@ module type S = sig
(** Return the current level of the theory (either the empty/beginning state, or the
last level returned by the [assume] function). *)
val assume : slice -> res
val assume : (formula, proof) slice -> res
(** Assume the formulas in the slice, possibly pushing new formulas to be propagated,
and returns the result of the new assumptions. *)