diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-07 18:16:40 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-07 18:16:40 -0700 |
commit | 97c7e81a68b31328e5bf40dd6939826e3cc1cf93 (patch) | |
tree | 9daa06998b858d27675bb3a716728e2ede3cb385 /src/parser/smt2/smt2.h | |
parent | 3fac8f369bd29f9856e2b61fbb5029d780fde64b (diff) |
[SMT2 Parser] Move code of `rewriterulesCommand` (#3334)
This commit moves the code in `rewriterulesCommand` in the SMT2 parser
to the `Smt2` class. Additionally, it creates a `boundVarList` rule to
reduce code duplication.
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 5caedb934..ec7e2071a 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -198,6 +198,24 @@ class Smt2 : public Parser void resetAssertions(); /** + * Creates a command that asserts a rule. + * + * @param kind The kind of rule (RR_REWRITE, RR_REDUCTION, RR_DEDUCTION) + * @param bvl Bound variable list + * @param triggers List of triggers + * @param guards List of guards + * @param heads List of heads + * @param body The body of the rule + * @return The command that asserts the rewrite rule + */ + std::unique_ptr<Command> assertRewriteRule(Kind kind, + Expr bvl, + const std::vector<Expr>& triggers, + const std::vector<Expr>& guards, + const std::vector<Expr>& heads, + Expr body); + + /** * Class for creating instances of `SynthFunCommand`s. Creating an instance * of this class pushes the scope, destroying it pops the scope. */ @@ -624,6 +642,15 @@ class Smt2 : public Parser void addSepOperators(); InputLanguage getLanguage() const; + + /** + * Utility function to create a conjunction of expressions. + * + * @param es Expressions in the conjunction + * @return True if `es` is empty, `e` if `es` consists of a single element + * `e`, the conjunction of expressions otherwise. + */ + Expr mkAnd(const std::vector<Expr>& es); }; /* class Smt2 */ }/* CVC4::parser namespace */ |