From 6801acdafddecd8a1244d1175c9b7d29630f20b8 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 15 Nov 2014 12:20:34 +0100 Subject: [PATCH] Normalisation is now done in constructors for smt --- smt/smt.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/smt/smt.ml b/smt/smt.ml index 8a886c83..45e084f2 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -29,8 +29,8 @@ module Fsmt = struct if i <> "" then i else raise Invalid_var - let mk_eq i j = Equal (mk_var i, mk_var j) - let mk_neq i j = Distinct (mk_var i, mk_var j) + let mk_eq i j = Equal (mk_var (min i j), mk_var (max i j)) + let mk_neq i j = Distinct (mk_var (min i j), mk_var (max i j)) let neg = function | Prop i -> Prop (-i) @@ -39,8 +39,8 @@ module Fsmt = struct let norm = function | Prop i -> Prop (abs i), i < 0 - | Equal (a, b) -> Equal (min a b, max a b), false - | Distinct (a, b) -> Equal (min a b, max a b), true + | Equal (a, b) -> Equal (a, b), false + | Distinct (a, b) -> Equal (a, b), true (* Only used after normalisation, so usual functions should work *) let hash = Hashtbl.hash