diff options
Diffstat (limited to 'src/preprocessing/passes/quantifier_macros.h')
| -rw-r--r-- | src/preprocessing/passes/quantifier_macros.h | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index 59a4bee2d..c5e557a9e 100644 --- a/src/preprocessing/passes/quantifier_macros.h +++ b/src/preprocessing/passes/quantifier_macros.h @@ -64,7 +64,17 @@ class QuantifierMacros : public PreprocessingPass bool reqComplete); void addMacro(Node op, Node n, std::vector<Node>& opc); void debugMacroDefinition(Node oo, Node n); - bool simplify(std::vector<Node>& assertions, bool doRewrite = false); + /** + * This applies macro elimination to the given pipeline, which discovers + * whether there are any quantified formulas corresponding to macros. + * + * @param ap The pipeline to apply macros to. + * @param doRewrite Whether we also wish to rewrite the assertions based on + * the discovered macro definitions. + * @return Whether new definitions were inferred and we rewrote the assertions + * based on them. + */ + bool simplify(AssertionPipeline* ap, bool doRewrite = false); Node simplify(Node n); void finalizeDefinitions(); void clearMaps(); |