Struct egg::Explanation

pub struct Explanation<L: Language> {
    pub explanation_trees: TreeExplanation<L>,
    /* private fields */
}

A data structure representing an explanation that two terms are equivalent.

There are two representations of explanations, each of which can be represented as s-expressions in strings. See Explanation for more details.

Fields

explanation_trees: TreeExplanation<L>

The tree representation of the explanation.

Implementations

impl<L: Language + Display> Explanation<L>

pub fn get_flat_string(&mut self) -> String

Get the flattened explanation as a string.

pub fn get_string(&self) -> String

Get the tree-style explanation as a string.

pub fn get_string_with_let(&self) -> String

Get the tree-style explanation with let binding as a string. See get_sexp_with_let for the format of these strings.

pub fn get_flat_strings(&mut self) -> Vec<String>

Get each term in the explanation as a string.

pub fn get_sexp(&self) -> Sexp

Get each the tree-style explanation as an s-expression.

The s-expression format mirrors the format of each TreeTerm. When a child contains an explanation, the explanation is wrapped with “(Explanation …)”. When a term is being re-written it is wrapped with “(Rewrite=> rule-name expression)” or “(Rewrite<= rule-name expression)”. “Rewrite=>” indicates that the previous term is rewritten to the current term and “Rewrite<=” indicates that the current term is rewritten to the previous term. The name of the rule or the reason provided to union_instantiations.

The following example shows that (+ 1 (- a (* (- 2 1) a))) = 1 Example explanation:

(+ 1 (- a (* (- 2 1) a)))
(+
   1
   (Explanation
     (- a (* (- 2 1) a))
     (-
       a
       (Explanation
         (* (- 2 1) a)
         (* (Explanation (- 2 1) (Rewrite=> constant_fold 1)) a)
         (Rewrite=> comm-mul (* a 1))
         (Rewrite<= mul-one a)))
     (Rewrite=> cancel-sub 0)))
(Rewrite=> constant_fold 1)

pub fn get_sexp_with_let(&self) -> Sexp

Get the tree-style explanation as an s-expression with let binding to enable sharing of subproofs.

The following explanation shows that (+ x (+ x (+ x x))) = (* 4 x). Steps such as factoring are shared via the let bindings. Example explanation:

(let
    (v_0 (Rewrite=> mul-one (* x 1)))
    (let
      (v_1 (+ (Explanation x v_0) (Explanation x v_0)))
      (let
        (v_2 (+ 1 1))
        (let
          (v_3 (Rewrite=> factor (* x v_2)))
          (Explanation
            (+ x (+ x (+ x x)))
            (Rewrite=> assoc-add (+ (+ x x) (+ x x)))
            (+ (Explanation (+ x x) v_1 v_3) (Explanation (+ x x) v_1 v_3))
            (Rewrite=> factor (* x (+ (+ 1 1) (+ 1 1))))
            (Rewrite=> comm-mul (* (+ (+ 1 1) (+ 1 1)) x))
            (*
              (Explanation
                (+ (+ 1 1) (+ 1 1))
                (+
                  (Explanation (+ 1 1) (Rewrite=> constant_fold 2))
                  (Explanation (+ 1 1) (Rewrite=> constant_fold 2)))
                (Rewrite=> constant_fold 4))
              x))))))

pub fn get_flat_sexps(&mut self) -> Vec<Sexp>

Get each flattened term in the explanation as an s-expression.

The s-expression format mirrors the format of each FlatTerm. Each expression after the first will be annotated in one location with a rewrite. When a term is being re-written it is wrapped with “(Rewrite=> rule-name expression)” or “(Rewrite<= rule-name expression)”. “Rewrite=>” indicates that the previous term is rewritten to the current term and “Rewrite<=” indicates that the current term is rewritten to the previous term. The name of the rule or the reason provided to union_instantiations.

Example explanation:

(+ 1 (- a (* (- 2 1) a)))
(+ 1 (- a (* (Rewrite=> constant_fold 1) a)))
(+ 1 (- a (Rewrite=> comm-mul (* a 1))))
(+ 1 (- a (Rewrite<= mul-one a)))
(+ 1 (Rewrite=> cancel-sub 0))
(Rewrite=> constant_fold 1)

impl<L: Language> Explanation<L>

pub fn new(explanation_trees: TreeExplanation<L>) -> Explanation<L>

Construct a new explanation given its tree representation.

pub fn make_flat_explanation(&mut self) -> &FlatExplanation<L>

Construct the flat representation of the explanation and return it.

pub fn check_proof<'a, R, N: Analysis<L>>(&mut self, rules: R) where
    R: IntoIterator<Item = &'a Rewrite<L, N>>,
    L: 'a,
    N: 'a, 

Check the validity of the explanation with respect to the given rules. This only is able to check rule applications when the rules are implement get_pattern_ast.

Trait Implementations

impl<L: Language + Display> Display for Explanation<L>

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

Formats the value using the given formatter.