kdrag.solvers.datalog

Classes

Datalog()

A simple datalog solver using sqlite

class kdrag.solvers.datalog.Datalog

Bases: object

A simple datalog solver using sqlite

>>> import kdrag as kd
>>> s = Datalog()
>>> edge = smt.Function('edge', smt.IntSort(), smt.IntSort(), smt.BoolSort())
>>> path = smt.Function('path', smt.IntSort(), smt.IntSort(), smt.BoolSort())
>>> s.declare_sig([edge, path])
>>> x, y, z = smt.Ints('x y z')
>>> s.run(edge(1,2))
>>> s.run(edge(2,3))
>>> s.run(kd.QForAll([x,y], edge(x,y), path(x,y)))
>>> s.run(kd.QForAll([x,y,z], edge(x,y), path(y,z), path(x,z)))
>>> s.run(kd.QForAll([x,y,z], edge(x,y), path(y,z), path(x,z)))
>>> s.db.execute("SELECT * FROM path").fetchall()
[(1, 2), (2, 3), (1, 3)]

declare_sig(sig: list[FuncDeclRef])

Parameters:: sig (list[FuncDeclRef])

run(rule: Rule | BoolRef)

Parameters:: rule (Rule | BoolRef)