Struct Fixedpoint 

pub struct Fixedpoint { /* private fields */ }

Context for Horn clause / Datalog solving.

See also

• Fixedpoint::add_rule
• Fixedpoint::query

Implementations

impl Fixedpoint

pub fn new() -> Fixedpoint

Create a new fixedpoint context.

pub fn add_rule(&self, rule: &impl Ast, name: Option<&str>)

Add a Horn clause rule to the fixedpoint context.

Example

let fp = Fixedpoint::new();
let p = Bool::new_const("p");
let q = Bool::new_const("q");

// Add rule: p => q
fp.add_rule(&p.implies(&q), None);

pub fn add_fact(&self, pred: &FuncDecl, args: &[u32])

Add a fact (ground assertion) to the fixedpoint context.

pub fn assert(&self, axiom: &impl Ast)

Assert a formula in the fixedpoint context.

pub fn query(&self, query: &impl Ast) -> SatResult

Query the fixedpoint context for satisfiability.

Returns the result of the query (satisfiable, unsatisfiable, or unknown).

pub fn query_relations(&self, relations: &[&FuncDecl]) -> SatResult

Query the fixedpoint context with multiple relations.

pub fn get_answer(&self) -> Option<Bool>

Get the answer substitution after a successful query. This provides the concrete values that make the query satisfiable.

pub fn get_reason_unknown(&self) -> String

Get the reason (core) for unsatisfiability after an unsuccessful query.

pub fn update_rule(&self, rule: &impl Ast, name: &str)

Update a named rule.

pub fn get_num_levels(&self, pred: &FuncDecl) -> u32

Get the number of levels explored during the last query.

pub fn get_cover_delta(&self, level: i32, predicate: &FuncDecl) -> Option<Bool>

Get the cover (approximation) at a given level.

pub fn add_cover(&self, level: i32, predicate: &FuncDecl, property: &impl Ast)

Add a cover for a predicate at a given level.

pub fn get_statistics(&self) -> Statistics

Get statistics about the last query.

pub fn register_relation(&self, pred: &FuncDecl)

Register a relation as fixedpoint-defined (least-fixedpoint semantics).

pub fn set_params(&self, params: &Params)

Set parameters for the fixedpoint context.

pub fn get_help(&self) -> String

Get the help string for fixedpoint parameters.

pub fn from_string(&self, s: &str) -> Result<(), String>

Parse a fixedpoint problem from a string in SMT-LIB format.

pub fn from_file(&self, filename: &str) -> Result<(), String>

Parse a file containing a fixedpoint problem.

Trait Implementations

impl Debug for Fixedpoint

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Default for Fixedpoint

fn default() -> Self

Returns the “default value” for a type.

impl Display for Fixedpoint

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Drop for Fixedpoint

fn drop(&mut self)

Executes the destructor for this type.