Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/HarvardPL/AbcDatalog/llms.txt

Use this file to discover all available pages before exploring further.

DatalogValidator converts a raw Set<Clause> into a validated program object before evaluation. It checks each clause independently for safety (every variable in a rule head must be bound in the body), rejects unsupported language features unless explicitly enabled via builder methods, and produces an UnstratifiedProgram that separates EDB facts from IDB rules. For programs that use negation, StratifiedNegationValidator can further verify that the negation dependencies are stratifiable and return a StratifiedProgram.
Engines like SemiNaiveEngine and ConcurrentStratifiedNegationBottomUpEngine call DatalogValidator internally inside init. You only need to call the validator directly when constructing programs from code and wanting to inspect the validated structure before handing it to an engine, or when stratifying a program for use with engines that require a StratifiedProgram.

​
DatalogValidator

​
Builder methods

DatalogValidator uses a builder-style API to opt in to extended language features. Each method sets a flag and returns this. 
public DatalogValidator withBinaryUnificationInRuleBody()
Enables X = Y (or X = a) unification premises in rule bodies. Without this flag, any BinaryUnifier in a clause body causes DatalogValidationException. 
public DatalogValidator withBinaryDisunificationInRuleBody()
Enables X != Y disunification premises in rule bodies. Without this flag, any BinaryDisunifier causes DatalogValidationException. 
public DatalogValidator withAtomNegationInRuleBody()
Enables not atom (negated body atom) premises. Without this flag, any NegatedAtom in a rule body causes DatalogValidationException.

​
validate

public UnstratifiedProgram validate(Set<Clause> program) throws DatalogValidationException
Validates every clause in program and separates it into initial EDB facts and IDB rules.
​
program
Set<Clause>
required
The raw set of clauses from the parser or programmatic construction.
​
result
UnstratifiedProgram
A validated program with four accessor methods: getRules(), getInitialFacts(), getEdbPredicateSyms(), and getIdbPredicateSyms().
An overloaded form accepts a second boolean parameter treatIdbFactsAsClauses: 
public UnstratifiedProgram validate(Set<Clause> program, boolean treatIdbFactsAsClauses)
    throws DatalogValidationException
When true, body-less clauses whose predicate also appears as the head of a rule are kept as rules rather than placed into the initial EDB facts set.

​
UnstratifiedProgram

The result of DatalogValidator.validate. It provides:
MethodReturn typeDescription
getRules()Set<ValidClause>All validated IDB rules.
getInitialFacts()Set<PositiveAtom>All ground EDB facts.
getEdbPredicateSyms()Set<PredicateSym>EDB predicate symbols (appear in facts but not as rule heads).
getIdbPredicateSyms()Set<PredicateSym>IDB predicate symbols (appear as rule heads).
ValidClause is a package-private subtype of Clause that carries the guarantee of having passed validation.

​
StratifiedNegationValidator

For programs that use negation, call StratifiedNegationValidator.validate after DatalogValidator.validate to verify that negation dependencies are stratifiable: 
public static StratifiedProgram validate(UnstratifiedProgram prog)
    throws DatalogValidationException
​
prog
UnstratifiedProgram
required
The validated but not yet stratified program.
​
result
StratifiedProgram
A StratifiedProgram extending UnstratifiedProgram with two additional methods: getStrata() returns List<Set<PredicateSym>> (ordered strata from lowest to highest) and getPredToStratumMap() returns Map<PredicateSym, Integer> mapping each predicate to its stratum index.
Throws DatalogValidationException if the negation dependencies form a cycle (i.e., the program cannot be stratified).

​
DatalogValidationException

DatalogValidationException is a checked exception thrown by both DatalogValidator.validate and StratifiedNegationValidator.validate. Common causes include:
  • A variable in the head of a rule that does not appear in any positive body atom and is not explicitly bound via unification.
  • Use of a BinaryUnifier, BinaryDisunifier, or NegatedAtom without enabling the corresponding flag on the validator.
  • Unstratifiable negation (cycles through negation in the dependency graph).

​
Code example

import edu.harvard.seas.pl.abcdatalog.ast.Clause;
import edu.harvard.seas.pl.abcdatalog.ast.validation.*;
import edu.harvard.seas.pl.abcdatalog.parser.DatalogParser;
import edu.harvard.seas.pl.abcdatalog.parser.DatalogTokenizer;
import java.io.StringReader;
import java.util.Set;

// Program with negation and disunification
String src =
    "edge(a,b). edge(b,c)."
    + "reachable(X,Y) :- edge(X,Y)."
    + "reachable(X,Y) :- edge(X,Z), reachable(Z,Y)."
    + "unreachable(X,Y) :- node(X), node(Y), not reachable(X,Y), X != Y.";

DatalogTokenizer t = new DatalogTokenizer(new StringReader(src));
Set<Clause> clauses = DatalogParser.parseProgram(t);

// Validate with negation and disunification enabled
DatalogValidator validator = new DatalogValidator()
    .withAtomNegationInRuleBody()
    .withBinaryDisunificationInRuleBody();

UnstratifiedProgram unstrat = validator.validate(clauses);

// Stratify for use with a negation-aware engine
StratifiedProgram strat = StratifiedNegationValidator.validate(unstrat);

System.out.println("Strata count: " + strat.getStrata().size());

Build docs developers (and LLMs) love

Get started for freeTalk to us