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
AddInvariant adds an assumed invariant for the predicate pred. This is a Spacer-specific function.
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
GetGroundSatAnswer retrieves a bottom-up sequence of ground facts. The previous call to Query or QueryFromLvl must have returned Satisfiable. This is a Spacer-specific function.
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
GetReachable retrieves the reachable states of a predicate. This is a Spacer-specific function.
GetReasonUnknown retrieves explanation why fixedpoint engine returned status Unknown
GetRuleNamesAlongTrace returns the list of rule names along the counterexample trace. This is a Spacer-specific function.
GetRules retrieves the current rules as a string
GetRulesAlongTrace returns the list of rules along the counterexample trace. This is a Spacer-specific function.
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
QueryFromLvl poses a query against the asserted rules at the given level. This is a Spacer-specific function.
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