diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/expr/expr_template.h | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r-- | src/expr/expr_template.h | 52 |
1 files changed, 41 insertions, 11 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index bffb37ddb..e95e434fe 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -35,12 +35,13 @@ ${includes} #include "util/exception.h" #include "util/language.h" +#include "util/hash.h" // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 44 "${template}" +#line 45 "${template}" namespace CVC4 { @@ -121,6 +122,11 @@ std::ostream& operator<<(std::ostream& out, */ std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC; +// for hash_maps, hash_sets.. +struct ExprHashFunction { + size_t operator()(CVC4::Expr e) const; +};/* struct ExprHashFunction */ + /** * Class encapsulating CVC4 expressions and methods for constructing new * expressions. @@ -344,6 +350,22 @@ public: Type getType(bool check = false) const throw (TypeCheckingException); /** + * Substitute "replacement" in for "e". + */ + Expr substitute(Expr e, Expr replacement) const; + + /** + * Substitute "replacements" in for "exes". + */ + Expr substitute(const std::vector<Expr> exes, + const std::vector<Expr>& replacements) const; + + /** + * Substitute pairs of (ex,replacement) from the given map. + */ + Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const; + + /** * Returns the string representation of the expression. * @return a string representation of the expression */ @@ -365,18 +387,28 @@ public: /** * Check if this is a null expression. + * * @return true if a null expression */ bool isNull() const; /** * Check if this is a null expression. + * * @return true if NOT a null expression */ operator bool() const; /** + * Check if this is an expression representing a variable. + * + * @return true if a variable expression + */ + bool isVariable() const; + + /** * Check if this is an expression representing a constant. + * * @return true if a constant expression */ bool isConst() const; @@ -541,7 +573,7 @@ public: /** * Make a Boolean if-then-else expression using this expression as the - * condition, and given the then and else parts + * condition, and given the then and else parts. * @param then_e the then branch expression * @param else_e the else branch expression * @return the if-then-else expression @@ -550,13 +582,14 @@ public: /** * Make a term if-then-else expression using this expression as the - * condition, and given the then and else parts + * condition, and given the then and else parts. * @param then_e the then branch expression * @param else_e the else branch expression * @return the if-then-else expression */ Expr iteExpr(const Expr& then_e, const Expr& else_e) const; -}; + +};/* class BoolExpr */ namespace expr { @@ -791,7 +824,7 @@ public: ${getConst_instantiations} -#line 795 "${template}" +#line 828 "${template}" namespace expr { @@ -839,12 +872,9 @@ inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) { }/* CVC4::expr namespace */ -// for hash_maps, hash_sets.. -struct ExprHashFunction { - size_t operator()(CVC4::Expr e) const { - return (size_t) e.getId(); - } -};/* struct ExprHashFunction */ +inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { + return (size_t) e.getId(); +} }/* CVC4 namespace */ |