diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-13 10:08:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-13 10:08:27 -0500 |
commit | 2267c5050fafde26b34dc1e84de015617efa7cc7 (patch) | |
tree | 0f2fa596850760667205e6b45ec6f09b471aacaa /src/parser/smt2/smt2.h | |
parent | eba03c5af0112aea04d83977333ae37e8a13137d (diff) |
Introduce smt2 parsing utility ParseOp and refactor (#3165)
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 65 |
1 files changed, 64 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 669104954..7c7f290a5 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -28,6 +28,7 @@ #include "api/cvc4cpp.h" #include "parser/parser.h" #include "parser/smt1/smt1.h" +#include "parser/smt2/parse_op.h" #include "smt/command.h" #include "theory/logic_info.h" #include "util/abstract_value.h" @@ -444,7 +445,69 @@ class Smt2 : public Parser parseError(withLogic); } -private: + //------------------------- processing parse operators + /** + * Given a parse operator p, apply a type ascription to it. This method is run + * when we encounter "(as t type)" and information regarding t has been stored + * in p. + * + * This updates p to take into account the ascription. This may include: + * - Converting an (pre-ascribed) array constant specification "const" to + * an ascribed array constant specification (as const type) where type is + * (Array T1 T2) for some T1, T2. + * - Converting a (nullary or non-nullary) parametric datatype constructor to + * the specialized constructor for the given type. + * - Converting an empty set, universe set, or separation nil reference to + * the respective term of the given type. + * - If p's expression field is set, then we leave p unchanged, check if + * that expression has the given type and throw a parse error otherwise. + */ + void applyTypeAscription(ParseOp& p, Type type); + /** + * This converts a ParseOp to expression, assuming it is a standalone term. + * + * In particular: + * - If p's expression field is set, then that expression is returned. + * - If p's name field is set, then we look up that name in the symbol table + * of this class. + * In other cases, a parse error is thrown. + */ + Expr parseOpToExpr(ParseOp& p); + /** + * Apply parse operator to list of arguments, and return the resulting + * expression. + * + * This method involves two phases. + * (1) Processing the operator represented by p, + * (2) Applying that operator to the set of arguments. + * + * For (1), this involves determining the kind of the overall expression. We + * may be in one the following cases: + * - If p's expression field is set, we may choose to prepend it to args, or + * otherwise determine the appropriate kind of the overall expression based on + * this expression. + * - If p's name field is set, then we get the appropriate symbol for that + * name, which may involve disambiguating that name if it is overloaded based + * on the types of args. We then determine the overall kind of the return + * expression based on that symbol. + * - p's kind field may be already set. + * + * For (2), we construct the overall expression, which may involve the + * following: + * - If p is an array constant specification (as const (Array T1 T2)), then + * we return the appropriate array constant based on args[0]. + * - If p represents a tuple selector, then we infer the appropriate tuple + * selector expression based on the type of args[0]. + * - If the overall kind of the expression is chainable, we may convert it + * to a left- or right-associative chain. + * - If the overall kind is MINUS and args has size 1, then we return an + * application of UMINUS. + * - If the overall expression is a partial application, then we process this + * as a chain of HO_APPLY terms. + */ + Expr applyParseOp(ParseOp& p, std::vector<Expr>& args); + //------------------------- end processing parse operators + private: std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type; std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars; std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body; |