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

Aliased def of negated in Expr_intf

Browse source
This commit is contained in:
Guillaume Bury 2016-07-08 17:34:46 +02:00
parent b56e4e3355
commit eba84fba42
2 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/core/expr_intf.ml
View file

@ -4,6 +4,10 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
type negated = Formula_intf.negated =
| Negated (* changed sign *)
| Same_sign (* kept sign *)
module type S = sig
(** Signature of formulas that parametrises the Mcsat Solver Module. *)
@ -37,7 +41,7 @@ module type S = sig
val neg : Formula.t -> Formula.t
(** Formula negation *)
val norm : Formula.t -> Formula.t * Formula_intf.negated
val norm : Formula.t -> Formula.t * negated
(** Returns a 'normalized' form of the formula, possibly negated
(in which case return [Negated]).
[norm] must be so that [a] and [neg a] normalise to the same formula,

8
src/example/expr.ml
View file

@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module FI = Formula_intf
module I = Formula_intf
exception Invalid_var
@ -40,9 +40,9 @@ let neg = function
| Distinct (a, b) -> Equal (a, b)
let norm = function
| Prop i -> Prop (abs i), if i < 0 then FI.Negated else FI.Same_sign
| Equal (a, b) -> Equal (a, b), FI.Same_sign
| Distinct (a, b) -> Equal (a, b), FI.Negated
| Prop i -> Prop (abs i), if i < 0 then I.Negated else I.Same_sign
| Equal (a, b) -> Equal (a, b), I.Same_sign
| Distinct (a, b) -> Equal (a, b), I.Negated
(* Only used after normalisation, so usual functions should work *)
let hash = Hashtbl.hash