From acd68152ff9600bdff208376f2cd43f09d45cdc8 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 17 Nov 2009 07:19:39 +0000 Subject: fixes and additions --- src/include/debug.h | 24 +++++++++++++++ src/include/exception.h | 2 +- src/include/expr.h | 27 ++++++++++++++-- src/include/expr_builder.h | 4 +++ src/include/expr_manager.h | 56 ++++++++++++---------------------- src/include/expr_value.h | 9 +++--- src/include/kind.h | 6 +++- src/include/parser_temp.h | 76 ---------------------------------------------- 8 files changed, 82 insertions(+), 122 deletions(-) create mode 100644 src/include/debug.h delete mode 100644 src/include/parser_temp.h (limited to 'src/include') diff --git a/src/include/debug.h b/src/include/debug.h new file mode 100644 index 000000000..95e705bcb --- /dev/null +++ b/src/include/debug.h @@ -0,0 +1,24 @@ +/********************* -*- C++ -*- */ +/** debug.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_DEBUG_H +#define __CVC4_DEBUG_H + +#include + +#ifdef DEBUG +// the __builtin_expect() helps us if assert is built-in or a macro +# define cvc4assert(x) assert(__builtin_expect((x), 1)) +#else +// TODO: use a compiler annotation when assertions are off ? +// (to improve optimization) +# define cvc4assert(x) +#endif /* DEBUG */ + +#endif /* __CVC4_DEBUG_H */ diff --git a/src/include/exception.h b/src/include/exception.h index 3502fdf0c..ce19b0d68 100644 --- a/src/include/exception.h +++ b/src/include/exception.h @@ -10,7 +10,7 @@ **/ #ifndef __CVC4_EXCEPTION_H -#ifndef __CVC4_EXCEPTION_H +#define __CVC4_EXCEPTION_H #include #include diff --git a/src/include/expr.h b/src/include/expr.h index 5e3559fd7..9ca449ce7 100644 --- a/src/include/expr.h +++ b/src/include/expr.h @@ -12,6 +12,9 @@ #ifndef __CVC4_EXPR_H #define __CVC4_EXPR_H +#include +#include + namespace CVC4 { class ExprValue; @@ -34,19 +37,39 @@ class Expr { * Increments the reference count. */ explicit Expr(ExprValue*); +public: + Expr(const Expr&); + /** Destructor. Decrements the reference count and, if zero, * collects the ExprValue. */ ~Expr(); -public: + Expr& operator=(const Expr&); + /** Access to the encapsulated expression. * @return the encapsulated expression. */ ExprValue* operator->(); - /** Const access to the encapsulated expressoin. + /** Const access to the encapsulated expression. * @return the encapsulated expression [const]. */ const ExprValue* operator->() const; + uint64_t hash() const; + + Expr eqExpr(const Expr& right) const; + Expr notExpr() const; + Expr negate() const; // avoid double-negatives + Expr andExpr(const Expr& right) const; + Expr orExpr(const Expr& right) const; + Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const; + Expr iffExpr(const Expr& right) const; + Expr impExpr(const Expr& right) const; + Expr xorExpr(const Expr& right) const; + Expr skolemExpr(int i) const; + Expr substExpr(const std::vector& oldTerms, + const std::vector& newTerms) const; + + static Expr null() { return s_null; } };/* class Expr */ } /* CVC4 namespace */ diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h index 59503aa4f..342834e37 100644 --- a/src/include/expr_builder.h +++ b/src/include/expr_builder.h @@ -43,6 +43,10 @@ class ExprBuilder { public: + ExprBuilder(); + ExprBuilder(const Expr&); + ExprBuilder(const ExprBuilder&); + // Compound expression constructors ExprBuilder& eqExpr(const Expr& right); ExprBuilder& notExpr(); diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h index 0c265f57f..5dae5b854 100644 --- a/src/include/expr_manager.h +++ b/src/include/expr_manager.h @@ -23,47 +23,29 @@ public: static ExprManager* currentEM() { return s_current; } // general expression-builders - Expr build(Kind kind); - Expr build(Kind kind, Expr child1); - Expr build(Kind kind, Expr child1, Expr child2); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10); + Expr mkExpr(Kind kind); + Expr mkExpr(Kind kind, Expr child1); + Expr mkExpr(Kind kind, Expr child1, Expr child2); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); // N-ary version - Expr build(Kind kind, std::vector children); + Expr mkExpr(Kind kind, std::vector children); // TODO: these use the current EM (but must be renamed) /* - static Expr build(Kind kind) - { currentEM()->build(kind); } - static Expr build(Kind kind, Expr child1); - { currentEM()->build(kind, child1); } - static Expr build(Kind kind, Expr child1, Expr child2); - { currentEM()->build(kind, child1, child2); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3); - { currentEM()->build(kind, child1, child2, child3); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); - { currentEM()->build(kind, child1, child2, child3, child4); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); - { currentEM()->build(kind, child1, child2, child3, child4, child5); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6); - { currentEM()->build(kind, child1, child2, child3, child4, child5, child6); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7); - { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8); - { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9); - { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10); - { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9, child10); } - // N-ary version - static Expr build(Kind kind, vector children) - { currentEM()->build(kind, children); } + static Expr mkExpr(Kind kind) + { currentEM()->mkExpr(kind); } + static Expr mkExpr(Kind kind, Expr child1); + { currentEM()->mkExpr(kind, child1); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2); + { currentEM()->mkExpr(kind, child1, child2); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + { currentEM()->mkExpr(kind, child1, child2, child3); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + { currentEM()->mkExpr(kind, child1, child2, child3, child4); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } */ // do we want a varargs one? perhaps not.. diff --git a/src/include/expr_value.h b/src/include/expr_value.h index ca12b8e03..c15241ebf 100644 --- a/src/include/expr_value.h +++ b/src/include/expr_value.h @@ -16,6 +16,7 @@ #ifndef __CVC4_EXPR_VALUE_H #define __CVC4_EXPR_VALUE_H +#include #include "expr.h" namespace CVC4 { @@ -41,14 +42,12 @@ class ExprValue { /** Variable number of child nodes */ Expr d_children[0]; + friend class Expr; + public: /** Hash this expression. * @return the hash value of this expression. */ - unsigned hash() const; - - /** Convert to (wrap in) an Expr. - * @return an Expr pointing to this expression. */ - operator Expr(); + uint64_t hash() const; // Iterator support diff --git a/src/include/kind.h b/src/include/kind.h index 9307cc677..a015a6b71 100644 --- a/src/include/kind.h +++ b/src/include/kind.h @@ -22,7 +22,11 @@ enum Kind { XOR, NOT, PLUS, - MINUS + MINUS, + ITE, + IFF, + SKOLEM, + SUBST };/* enum Kind */ }/* CVC4 namespace */ diff --git a/src/include/parser_temp.h b/src/include/parser_temp.h deleted file mode 100644 index d64a770e4..000000000 --- a/src/include/parser_temp.h +++ /dev/null @@ -1,76 +0,0 @@ -/********************* -*- C++ -*- */ -/** parser_temp.h - ** This file is part of the CVC4 prototype. - ** - ** A temporary holder for data used with the parser. - ** - ** The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - **/ - -#ifndef __CVC4_PARSER_TEMP_H -#define __CVC4_PARSER_TEMP_H - -#include - -#include "expr.h" -#include "exception.h" - -namespace CVC4 { - - class ValidityChecker; - - class ParserTemp { - private: - // Counter for uniqueID of bound variables - int d_uid; - // The main prompt when running interactive - std::string prompt1; - // The interactive prompt in the middle of a multi-line command - std::string prompt2; - // The currently used prompt - std::string prompt; - public: - ValidityChecker* vc; - std::istream* is; - // The current input line - int lineNum; - // File name - std::string fileName; - // The last parsed Expr - Expr expr; - // Whether we are done or not - bool done; - // Whether we are running interactive - bool interactive; - // Whether arrays are enabled for smt-lib format - bool arrFlag; - // Whether bit-vectors are enabled for smt-lib format - bool bvFlag; - // Size of bit-vectors for smt-lib format - int bvSize; - // Did we encounter a formula query (smtlib) - bool queryParsed; - // Default constructor - ParserTemp() : d_uid(0), prompt1("CVC> "), prompt2("- "), - prompt("CVC> "), lineNum(1), done(false), arrFlag(false), queryParsed(false) { } - // Parser error handling (implemented in parser.cpp) - int error(const std::string& s); - // Get the next uniqueID as a string - std::string uniqueID() { - std::ostringstream ss; - ss << d_uid++; - return ss.str(); - } - // Get the current prompt - std::string getPrompt() { return prompt; } - // Set the prompt to the main one - void setPrompt1() { prompt = prompt1; } - // Set the prompt to the secondary one - void setPrompt2() { prompt = prompt2; } - }; - -}/* CVC4 namespace */ - -#endif /* __CVC4_PARSER_TEMP_H */ -- cgit v1.2.3