[WIP] Add more contradiction detections on eq/in conjunctions.

lib/predicate.rb

@@ -88,6 +88,7 @@ def constants
   def &(other)
     return self  if other.tautology? or other==self
     return other if tautology?
+
     Predicate.new(expr & other.expr)
   end
 

lib/predicate/nodes/and.rb

@@ -7,6 +7,8 @@ def operator_symbol
     end
 
     def &(other)
+      return contradiction if in_contradiction?(self, other)
+
       case other
       when Tautology     then self
       when Contradiction then other

lib/predicate/nodes/eq.rb

@@ -7,12 +7,9 @@ def operator_symbol
     end
 
     def &(other)
-      return super unless free_variables == other.free_variables
       case other
-      when Eq
-        return self if constants == other.constants
-        return contradiction
       when In
+        return super unless free_variables == other.free_variables
         return super unless var_against_literal_value? && other.var_against_literal_value?
         mine, hers = self.right.value, other.right.value
         return self if hers.include?(mine)

lib/predicate/nodes/expr.rb

@@ -31,6 +31,12 @@ def identifier?
       sexpr_type == :identifier
     end
 
+    def in_contradiction?(me, other)
+      mine = me.constants
+      yours = other.constants
+      (mine.keys & yours.keys).any?{|k| mine[k] != yours[k] }
+    end
+
     def !
       sexpr([:not, self])
     end
@@ -41,6 +47,8 @@ def &(other)
       return other if other.contradiction?
       return self  if other.tautology?
       return other & self if other.dyadic_priority > self.dyadic_priority
+      return contradiction if in_contradiction?(self, other)
+
       sexpr([:and, self, other])
     end
 

spec/nodes/and/test_and.rb

@@ -30,5 +30,15 @@ class Predicate
       end
     end
 
+    context 'with an eq yielding a contradiction' do
+      let(:right) {
+        Factory.eq(:x, 5)
+      }
+
+      it 'returns a contradiction' do
+        expect(subject).to be_a(Contradiction)
+      end
+    end
+
   end
-end
+end

spec/nodes/eq/test_and.rb

@@ -14,6 +14,12 @@ class Predicate
       it{ should be_a(Contradiction) }
     end
 
+    context 'with an and leading to a contradiction' do
+      let(:right){ Factory.eq(:y, 4) & Factory.eq(:x, 3) }
+
+      it{ should be_a(Contradiction) }
+    end
+
     context 'with an IN on same variable and literal' do
       let(:right){ Factory.in(:x, [2,4]) }