Fixedpoint solver for Datalog and constrained Horn clauses (CHC)
Context methods (receiver omitted for clarity)
NewFixedpoint creates a new fixedpoint solver
Fixedpoint represents a fixedpoint solver for Datalog/CHC queries
AddCover adds a cover constraint to a predicate at a given level
AddFact adds a table fact to the fixedpoint solver
AddRule adds a rule (Horn clause) to the fixedpoint solver The rule should be an implication of the form body => head where head is a relation and body is a conjunction of relations
Assert adds a constraint into the fixedpoint solver
FromFile parses a Datalog program from a file
FromString parses a Datalog program from a string
GetAnswer retrieves the satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability
GetAssertions retrieves the fixedpoint assertions as an AST vector
GetCoverDelta retrieves the cover delta for a given predicate and level
GetHelp returns a string describing all available fixedpoint solver parameters
GetNumLevels retrieves the number of levels explored for a given predicate
GetParamDescrs retrieves parameter descriptions for the fixedpoint solver
GetReasonUnknown retrieves explanation why fixedpoint engine returned status Unknown
GetRules retrieves the current rules as a string
GetStatistics retrieves statistics for the fixedpoint solver
Query queries the fixedpoint solver with a constraint Returns Satisfiable if there is a derivation, Unsatisfiable if not
QueryRelations queries the fixedpoint solver with an array of relations Returns Satisfiable if any relation is non-empty, Unsatisfiable otherwise
RegisterRelation registers a predicate as a recursive relation
SetParams sets the fixedpoint solver parameters
SetPredicateRepresentation sets the predicate representation for a given relation
String returns the string representation of the fixedpoint solver
UpdateRule updates a named rule in the fixedpoint solver
Statistics represents statistics for Z3 solvers
GetDoubleValue returns the double value at the given index
GetKey returns the key (name) of a statistical data entry at the given index
GetUintValue returns the unsigned integer value at the given index
IsDouble returns true if the statistical data at the given index is double
IsUint returns true if the statistical data at the given index is unsigned integer
Size returns the number of statistical data entries
String returns the string representation of statistics