From 7463bd66aa935d4fe9530cbce9a8353327a04501 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 19 Jul 2021 09:45:34 -0400
Subject: [PATCH] fix(sat): sign error

---
 src/sat/Solver.ml | 17 ++---------------
 1 file changed, 2 insertions(+), 15 deletions(-)

diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml
index 33781d60..9600b0a9 100644
--- a/src/sat/Solver.ml
+++ b/src/sat/Solver.ml
@@ -188,19 +188,6 @@ module Make(Plugin : PLUGIN)
       let[@inline] level self a = Var.level self (var a)
       let[@inline] seen_both self a = seen self a && seen self (neg a)
 
-      (*
-      let[@inline] var a = a.var
-      let[@inline] neg a = a.neg
-      let[@inline] abs a = a.var.pa
-      let[@inline] formula a = a.lit
-      let[@inline] equal a b = a == b
-      let[@inline] sign a = a == abs a
-      let[@inline] hash a = Hashtbl.hash a.aid
-      let[@inline] compare a b = compare a.aid b.aid
-      let[@inline] reason a = V.reason a.var
-      let[@inline] id a = a.aid
-         *)
-
       let pp self fmt a = Formula.pp fmt (lit self a)
 
       let pp_a self fmt v =
@@ -296,8 +283,8 @@ module Make(Plugin : PLUGIN)
     let alloc_atom (self:t) ?default_pol lit : atom =
       let var, negated = alloc_var self ?default_pol lit in
       match negated with
-      | Solver_intf.Negated -> Atom.pa var
-      | Solver_intf.Same_sign -> Atom.na var
+      | Solver_intf.Same_sign -> Atom.pa var
+      | Solver_intf.Negated -> Atom.na var
 
     (*
     let[@inline] is_true a = a.is_true