diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-27 14:12:17 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-27 14:12:17 -0500 |
commit | d6c7967cfc7a9f8530f0de50f12f99bfc5f93da7 (patch) | |
tree | 2741c23c2cc42c065dc2aa573e0983e8f10823c1 /src/preprocessing/passes/synth_rew_rules.h | |
parent | a236ade3242599d4916fd9ee676c2c68c7c004b1 (diff) |
Synthesize candidate-rewrites from standard inputs (#1918)
Diffstat (limited to 'src/preprocessing/passes/synth_rew_rules.h')
-rw-r--r-- | src/preprocessing/passes/synth_rew_rules.h | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h new file mode 100644 index 000000000..cf0b491fb --- /dev/null +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -0,0 +1,48 @@ +/********************* */ +/*! \file synth_rew_rules.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A technique for synthesizing candidate rewrites of the form t1 = t2, + ** where t1 and t2 are subterms of the input. + **/ + +#ifndef __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H +#define __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** + * This class computes candidate rewrite rules of the form t1 = t2, where + * t1 and t2 are subterms of assertionsToPreprocess. It prints + * "candidate-rewrite" messages on the output stream of options. + * + * In contrast to other preprocessing passes, this pass does not modify + * the set of assertions. + */ +class SynthRewRulesPass : public PreprocessingPass +{ + public: + SynthRewRulesPass(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */ |