Commits

Pierre Carbonnelle  committed e0760c5

Negated literal can now have unbound variables : ~p(X). These variables are left in an undefined state and should not be used further in a clause.
Support negation of conjunctions : ~(p(X) & q(X))
Support negation of function comparison : ~(f[a]<'d')

  • Participants
  • Parent commits aaee562

Comments (0)

Files changed (3)

File pyDatalog/pyEngine.py

     if class0 and terms[0].is_const() and terms[0].id is None: return
     if hasattr(literal0.pred, 'base_pred'): # this is a negated literal
         if Debug : print("pyDatalog will search negation of %s" % literal0)
+        """ 
         for term in terms:
             if not term.is_const(): # all terms of a negated predicate must be bound
                 raise RuntimeError('Terms of a negated literal must be bound : %s' % str(literal0))
+        """
         base_literal = Literal(literal0.pred.base_pred, terms)
         """ the rest of the processing essentially performs the following, 
         but in its own environment, and with precautions to avoid stack overflow :
 
             complete(lambda base_subgoal=base_subgoal: merge(base_subgoal) or search(base_subgoal),
                      lambda base_subgoal=base_subgoal, subgoal=subgoal, literal=literal:
+                        # TODO deal with variable terms in result 
                         fact(subgoal, literal) if 0 == len(list(base_subgoal.facts.values())) else None)
                 
         schedule(Thunk(lambda base_literal=base_literal, subgoal=subgoal, literal=literal0: 

File pyDatalog/pyParser.py

     created by p(a,b) & q(c,d)
     operator '&' means 'and', and returns a Body
     """
+    Counter = 0
     def __init__(self, *args):
         LazyListOfList.__init__(self)
         self.literals = []
             return LazyListOfList.__str__(self)
         return ' & '.join(list(map (str, self.literals)))
 
-    def literal(self):
+    def literal(self, permanent=False):
         # return a literal that can be queried to resolve the body
         env, args = OrderedDict(), []
         for literal in self.literals:
                 if isinstance(arg, pyDatalog.Variable):
                     args.append(arg)
         # TODO cleanup : use args instead of env.values() ?
-        literal = Literal('_pyD_query', list(env.values()))
-        literal.lua.pred.reset_clauses()
+        if permanent:
+            literal = Literal('_pyD_query' + str(Body.Counter), list(env.values()))
+            Body.Counter = Body.Counter + 1
+        else:
+            literal = Literal('_pyD_query', list(env.values()))
+            literal.lua.pred.reset_clauses()
         literal <= self
         literal.args = args
         return literal 
         
+    def __invert__(self):
+        """unary ~ means negation """
+        return ~(self.literal(permanent=True))
+
     def ask(self):
         literal = self.literal()
         literal.ask()

File pyDatalog/test.py

 
     """ negation                                                     """    
     
+    @pyDatalog.program()
+    def _negation():
+        +p(a, b)
+        assert ask(~p(X, b)) == None
+        assert ask(~p(X, c)) == set([('X', 'c')])
+
     pyDatalog.load("""
         + even(0)
         even(N) <= (N > 0) & (N1==N-1) & odd(N1)
 
     @pyDatalog.program()
     def function_negation(): 
-        assert ask((f[a]==X) & (~(X<'d'))) == None # TODO support direct negation of comparison
-        assert ask((f[a]==X) & (~(X in('d',)))) == set([('c',)]) # TODO support direct negation of comparison
+        assert not(ask(~(f[a]<'d'))) 
+        assert not(ask(~(f[X]<'d'))) 
+        assert ask(~(f[a] in('d',)))
         
     """ aggregates                                                         """
     
     assert (Z.b[X]==Y) == [(z, 'za')]
     assert (Z.c[X]==Y) == [(z, 'za')]
     assert ((Z.c[X]==Y) & (Z.c[X]>'a')) == [(z, 'za')]
+    assert (Z.c[X]>'a') == [(z,)]
     assert (z.b) == 'za'
     assert (z.c) == 'za'
     
     assert ~Z.x(w)
     assert ~ (Z.z[w]=='z')
     assert(Z.pred(X)) == [(w,)]
-    assert(Z.pred(X) & ~ (Z.z[X]=='z')) == [(w,)]
+    assert(Z.pred(X) & ~ (Z.z[X]>='z')) == [(w,)]
     assert(Z.x(X) & ~(Z.pred(X))) == [(z,)]
 
     assert (Z.len[X]==Y) == [(w, 1), (z, 1)]
     assert_error("ask( (A.c[X]==Y) & (Z.c[X]==Y))", "TypeError: First argument of Z.c\[1\]==\('.','.'\) must be a Z, not a A ")
     assert_ask("A.u[X]==Y", "Predicate without definition \(or error in resolver\): A.u\[1\]==/2")
     assert_ask("A.u[X,Y]==Z", "Predicate without definition \(or error in resolver\): A.u\[2\]==/3")
-    assert_ask("~z(X)", "Terms of a negated literal must be bound : ~z\(X\)")
     assert_error('(a_sum[X] == sum(Y, key=Y)) <= p(X, Z, Y)', "Error: Duplicate definition of aggregate function.")
     assert_error('(two(X)==Z) <= (Z==X+(lambda X: X))', 'Syntax error near equality: consider using brackets. two\(X\)')
     assert_error('p(X) <= sum(X, key=X)', 'Invalid body for clause')