Solver

Functions for solving Datalog programs and querying their models.

Definitions

def facts0(p: PredSym, d: Datalog): Vector[t] with Order[t]§ Source

Returns all facts in d associated with the predicate symbol p.

def facts1(p: PredSym, d: Datalog): Vector[t] with Order[t]§ Source

Returns all facts in d associated with the predicate symbol p.

def facts10(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10]

§ Source

Returns all facts in d associated with the predicate symbol p.

def facts11(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Order[t11]

§ Source

Returns all facts in d associated with the predicate symbol p.

def facts12(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Order[t11], Order[t12]

§ Source

Returns all facts in d associated with the predicate symbol p.

def facts13(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Order[t11], Order[t12], Order[t13]

§ Source

Returns all facts in d associated with the predicate symbol p.

def facts14(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Order[t11], Order[t12], Order[t13], Order[t14]

§ Source

Returns all facts in d associated with the predicate symbol p.

def facts15(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Order[t11], Order[t12], Order[t13], Order[t14], Order[t15]

§ Source

Returns all facts in d associated with the predicate symbol p.

def facts2(p: PredSym, d: Datalog): Vector[(t1, t2)] with Order[t1], Order[t2]§ Source

Returns all facts in d associated with the predicate symbol p.

def facts3(p: PredSym, d: Datalog): Vector[(t1, t2, t3)] with Order[t1], Order[t2], Order[t3]§ Source

Returns all facts in d associated with the predicate symbol p.

def facts4(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4)] with Order[t1], Order[t2], Order[t3], Order[t4]§ Source

Returns all facts in d associated with the predicate symbol p.

def facts5(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5]

§ Source

Returns all facts in d associated with the predicate symbol p.

def facts6(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5, t6)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6]

§ Source

Returns all facts in d associated with the predicate symbol p.

def facts7(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5, t6, t7)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7]

§ Source

Returns all facts in d associated with the predicate symbol p.

def facts8(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5, t6, t7, t8)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8]

§ Source

Returns all facts in d associated with the predicate symbol p.

def facts9(p: PredSym, d: Datalog): Vector[(t1, t2, t3, t4, t5, t6, t7, t8, t9)] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9]

§ Source

Returns all facts in d associated with the predicate symbol p.

def injectInto1(p: PredSym, ts: f[t1]): Datalog \ Aef[f] with Order[t1], Foldable[f]§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1). p(t1').} given the sequence (t1), (t1').

def injectInto10(p: PredSym, ts: f[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10). p(t1', t2', t3', t4', t5', t6', t7', t8', t9', t10').} given the sequence (t1, t2, t3, t4, t5, t6, t7, t8, t9, t10), (t1', t2', t3', t4', t5', t6', t7', t8', t9', t10').

def injectInto11(p: PredSym, ts: f[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Order[t11], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11). p(t1', t2', t3', t4', t5', t6', t7', t8', t9', t10', t11').} given the sequence (t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11), (t1', t2', t3', t4', t5', t6', t7', t8', t9', t10', t11').

def injectInto12(p: PredSym, ts: f[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Order[t11], Order[t12], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12). p(t1', t2', t3', t4', t5', t6', t7', t8', t9', t10', t11', t12').} given the sequence (t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12), (t1', t2', t3', t4', t5', t6', t7', t8', t9', t10', t11', t12').

def injectInto13(p: PredSym, ts: f[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Order[t11], Order[t12], Order[t13], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13). p(t1', t2', t3', t4', t5', t6', t7', t8', t9', t10', t11', t12', t13').} given the sequence (t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13), (t1', t2', t3', t4', t5', t6', t7', t8', t9', t10', t11', t12', t13').

def injectInto14(p: PredSym, ts: f[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Order[t11], Order[t12], Order[t13], Order[t14], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14). p(t1', t2', t3', t4', t5', t6', t7', t8', t9', t10', t11', t12', t13', t14').} given the sequence (t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14), (t1', t2', t3', t4', t5', t6', t7', t8', t9', t10', t11', t12', t13', t14').

def injectInto15(p: PredSym, ts: f[(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Order[t10], Order[t11], Order[t12], Order[t13], Order[t14], Order[t15], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15). p(t1', t2', t3', t4', t5', t6', t7', t8', t9', t10', t11', t12', t13', t14', t15').} given the sequence (t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15), (t1', t2', t3', t4', t5', t6', t7', t8', t9', t10', t11', t12', t13', t14', t15').

def injectInto2(p: PredSym, ts: f[(t1, t2)]): Datalog \ Aef[f] with Order[t1], Order[t2], Foldable[f]§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2). p(t1', t2').} given the sequence (t1, t2), (t1', t2').

def injectInto3(p: PredSym, ts: f[(t1, t2, t3)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Foldable[f]§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3). p(t1', t2', t3').} given the sequence (t1, t2, t3), (t1', t2', t3').

def injectInto4(p: PredSym, ts: f[(t1, t2, t3, t4)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4). p(t1', t2', t3', t4').} given the sequence (t1, t2, t3, t4), (t1', t2', t3', t4').

def injectInto5(p: PredSym, ts: f[(t1, t2, t3, t4, t5)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5). p(t1', t2', t3', t4', t5').} given the sequence (t1, t2, t3, t4, t5), (t1', t2', t3', t4', t5').

def injectInto6(p: PredSym, ts: f[(t1, t2, t3, t4, t5, t6)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5, t6). p(t1', t2', t3', t4', t5', t6').} given the sequence (t1, t2, t3, t4, t5, t6), (t1', t2', t3', t4', t5', t6').

def injectInto7(p: PredSym, ts: f[(t1, t2, t3, t4, t5, t6, t7)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5, t6, t7). p(t1', t2', t3', t4', t5', t6', t7').} given the sequence (t1, t2, t3, t4, t5, t6, t7), (t1', t2', t3', t4', t5', t6', t7').

def injectInto8(p: PredSym, ts: f[(t1, t2, t3, t4, t5, t6, t7, t8)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5, t6, t7, t8). p(t1', t2', t3', t4', t5', t6', t7', t8').} given the sequence (t1, t2, t3, t4, t5, t6, t7, t8), (t1', t2', t3', t4', t5', t6', t7', t8').

def injectInto9(p: PredSym, ts: f[(t1, t2, t3, t4, t5, t6, t7, t8, t9)]): Datalog \ Aef[f] with Order[t1], Order[t2], Order[t3], Order[t4], Order[t5], Order[t6], Order[t7], Order[t8], Order[t9], Foldable[f]

§ Source

Insert all facts in the given sequence f into the given relation p.

I.e. returns a Datalog program corresponding to #{p(t1, t2, t3, t4, t5, t6, t7, t8, t9). p(t1', t2', t3', t4', t5', t6', t7', t8', t9').} given the sequence (t1, t2, t3, t4, t5, t6, t7, t8, t9), (t1', t2', t3', t4', t5', t6', t7', t8', t9').

def projectSym(p: PredSym, d: Datalog): Datalog§ Source

Project all facts in the given Datalog program d that has p in its head.

def provenanceOf(p: PredSym, f: Vector[Boxed], withh: Vector[PredSym], mkExtVar: PredSym -> (Vector[Boxed] -> t), d: Datalog): Vector[t]

§ Source

Returns the provenance of fact f of relation p given Datalog program d.

def rename(preds: List[PredSym], d: Datalog): Datalog§ Source

Renames every predicate symbol in d with a fresh name, except for those in preds.

def runSolver(d: Datalog): Datalog§ Source

Returns the minimal model of the given Datalog program d. The minimal model is given by the model semantics for Datalog programs with stratified negation. The stratification is computed automatically by the solver.

def runSolverWithProvenance(d: Datalog): Datalog§ Source

Returns a provenance model of the given Datalog program d. The provenance model can later be used for provenance queries.

def union(d1: Datalog, d2: Datalog): Datalog§ Source

Returns the pairwise union of d1 and d2. I.e. the facts of the union is the union of the facts and likewise for rules. A fact or rule may occur twice in the Datalog program. This has no effect on its semantics.