Struct egg::Explanation
source · pub struct Explanation<L: Language> {
pub explanation_trees: TreeExplanation<L>,
/* private fields */
}
Expand description
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§
source§impl<L: Language + Display + FromOp> Explanation<L>
impl<L: Language + Display + FromOp> Explanation<L>
sourcepub fn get_flat_string(&mut self) -> String
pub fn get_flat_string(&mut self) -> String
Get each flattened term in the explanation as an s-expression string.
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)
sourcepub fn get_string(&self) -> String
pub fn get_string(&self) -> String
Get each the tree-style explanation as an s-expression string.
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)
sourcepub fn get_string_with_let(&self) -> String
pub fn get_string_with_let(&self) -> String
Get the tree-style explanation as an s-expression string 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))))))
sourcepub fn get_flat_strings(&mut self) -> Vec<String>
pub fn get_flat_strings(&mut self) -> Vec<String>
Get each term in the explanation as a string.
See get_string
for the format of these strings.
sourcepub fn get_tree_size(&self) -> usize
pub fn get_tree_size(&self) -> usize
Get the size of this explanation tree in terms of the number of rewrites in the let-bound version of the tree.
source§impl<L: Language> Explanation<L>
impl<L: Language> Explanation<L>
sourcepub fn new(explanation_trees: TreeExplanation<L>) -> Explanation<L>
pub fn new(explanation_trees: TreeExplanation<L>) -> Explanation<L>
Construct a new explanation given its tree representation.
sourcepub fn make_flat_explanation(&mut self) -> &FlatExplanation<L>
pub fn make_flat_explanation(&mut self) -> &FlatExplanation<L>
Construct the flat representation of the explanation and return it.
sourcepub fn check_proof<'a, R, N>(&mut self, rules: R)where
R: IntoIterator<Item = &'a Rewrite<L, N>>,
L: 'a,
N: 'a + Analysis<L>,
pub fn check_proof<'a, R, N>(&mut self, rules: R)where R: IntoIterator<Item = &'a Rewrite<L, N>>, L: 'a, N: 'a + Analysis<L>,
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
.