Struct debug_sat::Graph

pub struct Graph {
    pub exprs: Vec<Expression>,
    pub havox: HashMap<(usize, usize), bool>,
    pub map: HashMap<Expression, usize>,
    pub history: Vec<(usize, usize)>,
    pub cache: RefCell<Vec<Option<usize>>>,
}

Binds expressions together with constraints and acceleration data structures.

Exposes members to allow advanced introspection.

Fields

exprs: Vec<Expression>

Expression nodes.

havox: HashMap<(usize, usize), bool>

Equality and inequality constraints.

map: HashMap<Expression, usize>

Contains a map to look up index of expressions.

history: Vec<(usize, usize)>

Used to keep track of assumptions. Changes to the havox diagram are recorded to roll back to moment right before assumption being made.

cache: RefCell<Vec<Option<usize>>>

Caches minimum id for equivalence classes.

Methods

impl Graph

fn new() -> Graph

Creates a new graph.

fn false_(&self) -> usize

Logical FALSE has a fixed location 0.

fn true_(&self) -> usize

Logical TRUE has a fixed location 1.

fn contains(&self, expr: &Expression) -> Option<usize>

Returns id of existing expression.

fn var(&mut self, name: usize) -> usize

Add variable.

name - index of variable referenced externally.

fn not(&mut self, a: usize) -> usize

Add logical NOT.

fn eq(&mut self, a: usize, b: usize) -> usize

Add logical EQ.

fn and(&mut self, a: usize, b: usize) -> usize

Add logical AND.

fn or(&mut self, a: usize, b: usize) -> usize

Add logical OR.

fn imply(&mut self, a: usize, b: usize) -> usize

Add logical material implication.

fn havox(&self, id: (usize, usize)) -> Option<bool>

Returns Some(true) if it is known that two things are equal. Returns Some(false) if it is known that two things are unequal. Returns None if it is unknown whether two things are equal.

The id is an edge of the format (min, max).

fn are_eq(&self, a: usize, b: usize) -> Option<bool>

Returns whether it is known that two expressions are equivalent.

fn true_and(&mut self, ind: usize) -> Proof

Checks whether it can be proven that one of the arguments are true. This means the return value depends on the other argument.

fn false_and(&mut self, ind: usize) -> Proof

Checks whether it can be proven that and expression is false, by knowing that one of the arguments are false.

fn false_or(&mut self, ind: usize) -> Proof

Checks whether it can be proven that one of the arguments are false. This means that the or expression is equal to the other argument.

fn true_or(&mut self, ind: usize) -> Proof

Checks whether it can be proven that or expression is true, by knowing that one of the arguments are true.

fn true_not(&mut self, ind: usize) -> Proof

Checks whether it can be proven that input to not expression is true. This means that the output is false.

fn false_not(&mut self, ind: usize) -> Proof

Checks whether it can be proven that input to not expression is false. This means that the output is true.

fn false_imply(&mut self, ind: usize) -> Proof

Checks whether assumption is proven to be false.

fn true_imply(&mut self, ind: usize) -> Proof

Checks whether assumption is proven to be true. True assumption makes the imply expression is equal to the conclusion.

fn false_eq(&mut self, ind: usize) -> Proof

Checks whether arguments to eq expression are inequal.

This means that the eq expression must be equal to false.

fn true_eq(&mut self, ind: usize) -> Proof

Checks whether arguments to eq expression are equal.

This means that the eq expression must be equal to true.

fn eq_true(&mut self, ind: usize) -> Proof

Checks whether one side is proven to be equal to other side.

The equation must be equal to true. When the equation is true, one side is equal to another.

fn eq_false(&mut self, ind: usize) -> Proof

Checks whether one side is proven to be inequal to the other side.

The equation must be equal to false. When the equation is false, one side is inequal to another.

fn paradox(&mut self, ind: usize) -> Proof

Checks that provably a ∧ ¬a results in a paradox.

fn tautology(&mut self, ind: usize) -> Proof

Checks that provably a ∨ ¬a results in a tautology.

fn or_false(&mut self, ind: usize) -> Proof

Checks whether it can be proven that the or expression is false. This means that both arguments must be false.

fn and_true(&mut self, ind: usize) -> Proof

Checks whether it can be proven that the and expression is true. This means that both arguments must be true.

fn not_true(&mut self, ind: usize) -> Proof

Check if it can be proven that output of not expression is true.

fn not_false(&mut self, ind: usize) -> Proof

Check if it can be proven that output of not expression is false.

fn excluded_middle(&mut self, ind: usize) -> Proof

Check that it can be proven that an expression is either true or false.

fn eq_and(&mut self, ind: usize) -> Proof

Checks whether it can be proven that and expression has equal arguments, which means that the and expression is the same as the argument.

fn neq_and(&mut self, ind: usize) -> Proof

Checks whether it can be proven that and expression has inequal arguments. This means that the and expression is always false.

fn eq_or(&mut self, ind: usize) -> Proof

Checks whether it can be proven that or expression has equal arguments. This means that the or expression is always equal to its argument.

fn neq_or(&mut self, ind: usize) -> Proof

Checks whether it can be proven that or expression has inequal arguments. This means the or expression is always true.

fn eq_imply(&mut self, ind: usize) -> Proof

Checks whether it can be proven that imply expression has equal arguments. This means the imply expression is always true.

fn neq_imply(&mut self, ind: usize) -> Proof

Checks whether it can be proven that imply expression has inequal arguments. This means the imply expression is always equal to the second argument.

fn path_and_not(&mut self, ind: usize) -> Proof

Checks that and[not] <=> or.

This is equivalent to not(and(a, b)) = or(not(a), not(b)).

fn path_not_and(&mut self, ind: usize) -> Proof

Checks that or <=> and[not].

This is equivalent to or(not(a), not(b)) = not(and(a, b)).

fn path_or_not(&mut self, ind: usize) -> Proof

Checks that or[not] <=> and.

This is equivalent to not(or(a, b)) = and(not(a), not(b)).

fn path_not_or(&mut self, ind: usize) -> Proof

Checks that and <=> or[not].

This is equivalent to or(not(a), not(b)) = not(and(a, b)).

fn not_not(&mut self, ind: usize) -> Proof

Checks that not . not <=> id.

fn assume_eq(&mut self, a: usize, b: usize) -> Assumption

Assume that two expressions are equivalent.

Returns an assumption that can be used to roll back change.

fn assume_neq(&mut self, a: usize, b: usize) -> Assumption

Assume that two expressions are inequivalent.

Returns an assumption that can be used to roll back change.

fn solve(&mut self) -> Proof

Solves as much as possible using all tactics.

Trait Implementations

impl Clone for Graph

fn clone(&self) -> Graph

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.