The SexpInliner API. More...
#include <SexpInliner.h>
Related Functions | |
(Note that these are not member functions.) | |
| void | SexpInliner_blacklist_name (SexpInliner_ptr self, node_ptr var) |
| Adds to the blacklist the given name. | |
| void | SexpInliner_clear_blacklist (SexpInliner_ptr self) |
| Clears the internal set of blacklisted names. | |
| void | SexpInliner_clear_equivalences (SexpInliner_ptr self) |
| Clears the internal cache of forced equivalences. | |
| void | SexpInliner_clear_invariants (SexpInliner_ptr self) |
| Clears the internal cache of forced invariants. | |
| SexpInliner_ptr | SexpInliner_copy (const SexpInliner_ptr self) |
| Copy costructor. | |
| SexpInliner_ptr | SexpInliner_create (SymbTable_ptr st, const size_t fixpoint_limit) |
| Sexp Inliner constructor. | |
| void | SexpInliner_destroy (SexpInliner_ptr self) |
| Destructor. | |
| boolean | SexpInliner_force_equivalence (SexpInliner_ptr self, node_ptr var, Expr_ptr expr) |
| Forces to learn that var (can be timed) and expr are equivalent. The expression is assumed to be already flattened, and defines expanded. | |
| boolean | SexpInliner_force_equivalences (SexpInliner_ptr self, Set_t equivs) |
| Forces to learn all equivalences in given set. | |
| boolean | SexpInliner_force_invariant (SexpInliner_ptr self, node_ptr var, Expr_ptr expr) |
| Forces to learn that var and expr are invariantly equivalent. | |
| boolean | SexpInliner_force_invariants (SexpInliner_ptr self, Set_t invars) |
| Forces to learn all invariants in given set. | |
| SymbTable_ptr | SexpInliner_get_symb_table (const SexpInliner_ptr self) |
| Returns the symbol table that is connected to the BoolEnc instance connected to self. | |
| hash_ptr | SexpInliner_get_var2expr_hash (SexpInliner_ptr self) |
| Get the internal var2expr hash. | |
| hash_ptr | SexpInliner_get_var2invar_hash (SexpInliner_ptr self) |
| Get the internal var2invar hash. | |
| InlineRes_ptr | SexpInliner_inline (SexpInliner_ptr self, Expr_ptr expr, boolean *changed) |
| Performs inlining of given expression. | |
| Expr_ptr | SexpInliner_inline_no_learning (SexpInliner_ptr self, Expr_ptr expr, boolean *changed) |
| Performs inlining of given expression. | |
The SexpInliner API.
The SexpInliner type The SexpInliner type
| void SexpInliner_blacklist_name | ( | SexpInliner_ptr | self, | |
| node_ptr | var | |||
| ) | [related] |
Adds to the blacklist the given name.
Any name occurring in the blacklist will be not substituted. Use to avoid inlining a set of variables.
| void SexpInliner_clear_blacklist | ( | SexpInliner_ptr | self | ) | [related] |
Clears the internal set of blacklisted names.
| void SexpInliner_clear_equivalences | ( | SexpInliner_ptr | self | ) | [related] |
Clears the internal cache of forced equivalences.
| void SexpInliner_clear_invariants | ( | SexpInliner_ptr | self | ) | [related] |
Clears the internal cache of forced invariants.
| SexpInliner_ptr SexpInliner_copy | ( | const SexpInliner_ptr | self | ) | [related] |
Copy costructor.
| SexpInliner_ptr SexpInliner_create | ( | SymbTable_ptr | st, | |
| const size_t | fixpoint_limit | |||
| ) | [related] |
Sexp Inliner constructor.
fixpoint_limit is a integer bound controlling the maximum number of iteration to be carried out when inlining an expression. Use 0 (zero) for no limit.
| void SexpInliner_destroy | ( | SexpInliner_ptr | self | ) | [related] |
Destructor.
| boolean SexpInliner_force_equivalence | ( | SexpInliner_ptr | self, | |
| node_ptr | var, | |||
| Expr_ptr | expr | |||
| ) | [related] |
Forces to learn that var (can be timed) and expr are equivalent. The expression is assumed to be already flattened, and defines expanded.
The equivalence is learnt even if given name is blacklisted. The equivalence substitutes any previously forced equivalence about the same variable. Returns true if the equivalence was accepted, or false otherwise.
| boolean SexpInliner_force_equivalences | ( | SexpInliner_ptr | self, | |
| Set_t | equivs | |||
| ) | [related] |
Forces to learn all equivalences in given set.
There is an implicit assumption about the format of each element in the set. It must be either a EQUAL, a EQDEF or a IFF node where left operand is a variable. This method may be useful to force equivalences previously returned by a InlineRes instance.
Returns true if any equivalence was accepted, false if all were rejected
| boolean SexpInliner_force_invariant | ( | SexpInliner_ptr | self, | |
| node_ptr | var, | |||
| Expr_ptr | expr | |||
| ) | [related] |
Forces to learn that var and expr are invariantly equivalent.
var must be a flat variable name (not nexted not timed). The expression is assumed to be already flattened. The invariant is learnt even if given name is blacklisted. The invariant substitutes any previously forced invariant about the same variable.
Returns true if the invariant was successfully forced, or false otherwise.
| boolean SexpInliner_force_invariants | ( | SexpInliner_ptr | self, | |
| Set_t | invars | |||
| ) | [related] |
Forces to learn all invariants in given set.
There is an implicit assumption about the format of each element in the set. It must be either a EQUAL, a EQDEF, or a IFF node where left operand is a variable. This method may be useful to force invariants previously returned by a InlineRes instance.
Returns true if any invariant was accepted, false if all were rejected
| SymbTable_ptr SexpInliner_get_symb_table | ( | const SexpInliner_ptr | self | ) | [related] |
Returns the symbol table that is connected to the BoolEnc instance connected to self.
| hash_ptr SexpInliner_get_var2expr_hash | ( | SexpInliner_ptr | self | ) | [related] |
Get the internal var2expr hash.
Get the internal var2expr hash. Do not perform any side-effects on this hash
| hash_ptr SexpInliner_get_var2invar_hash | ( | SexpInliner_ptr | self | ) | [related] |
Get the internal var2invar hash.
Get the internal var2invar hash. Do not perform any side-effects on this hash
| InlineRes_ptr SexpInliner_inline | ( | SexpInliner_ptr | self, | |
| Expr_ptr | expr, | |||
| boolean * | changed | |||
| ) | [related] |
Performs inlining of given expression.
Applies inlining to the given expression, with fixpoint.
Returned InlineRes object contains the result. Returned instance must be destroyed by the caller. If given variable changed is not NULL, it will be set to true if any inlining has been applied, or will be set to false if no inlining has been applied.
Before carrying out the actual inlining, this method learn automatically equivalences out of the given formula.
WARNING: The expression is assumed to be already flattened, and normalized (all nodes created with find_node)
| Expr_ptr SexpInliner_inline_no_learning | ( | SexpInliner_ptr | self, | |
| Expr_ptr | expr, | |||
| boolean * | changed | |||
| ) | [related] |
Performs inlining of given expression.
Applies inlining to the given expression, with fixpoint, and returns the result expression.
If given variable changed is not NULL, it will be set to true if any inlining has been applied, or will be set to false if no inlining has been applied.
Before carrying out the actual inlining, this method learn automatically equivalences out of the given formula. [MD] Is this comment wrong? Simply cut and paste from the method [MD] SexpInliner_inline?
WARNING: The expression is assumed to be already flattened, and normalized (all nodes created with find_node)
SexpInliner_inline
1.6.1
