diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/.gitignore | 4 | ||||
-rw-r--r-- | src/expr/command.h | 34 | ||||
-rw-r--r-- | src/expr/expr.cpp | 29 | ||||
-rw-r--r-- | src/expr/expr.h | 17 |
4 files changed, 63 insertions, 21 deletions
diff --git a/src/expr/.gitignore b/src/expr/.gitignore new file mode 100644 index 000000000..4618e07b0 --- /dev/null +++ b/src/expr/.gitignore @@ -0,0 +1,4 @@ +/.deps +/Makefile.in +/kind.h +/metakind.h diff --git a/src/expr/command.h b/src/expr/command.h index 3c42c153c..e5994b3c7 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -36,6 +36,20 @@ class Command; inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; +/** The status an SMT benchmark can have */ +enum BenchmarkStatus { + /** Benchmark is satisfiable */ + SMT_SATISFIABLE, + /** Benchmark is unsatisfiable */ + SMT_UNSATISFIABLE, + /** The status of the benchmark is unknown */ + SMT_UNKNOWN +}; + +inline std::ostream& operator<<(std::ostream& out, + BenchmarkStatus status) + CVC4_PUBLIC; + class CVC4_PUBLIC Command { public: virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; @@ -107,15 +121,6 @@ protected: class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { public: - /** The status an SMT benchmark can have */ - enum BenchmarkStatus { - /** Benchmark is satisfiable */ - SMT_SATISFIABLE, - /** Benchmark is unsatisfiable */ - SMT_UNSATISFIABLE, - /** The status of the benchmark is unknown */ - SMT_UNKNOWN - }; SetBenchmarkStatusCommand(BenchmarkStatus status); void invoke(SmtEngine* smt); void toStream(std::ostream& out) const; @@ -123,9 +128,6 @@ protected: BenchmarkStatus d_status; };/* class SetBenchmarkStatusCommand */ -inline std::ostream& operator<<(std::ostream& out, - SetBenchmarkStatusCommand::BenchmarkStatus status) - CVC4_PUBLIC; class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { public: @@ -288,16 +290,16 @@ inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { /* output stream insertion operator for benchmark statuses */ inline std::ostream& operator<<(std::ostream& out, - SetBenchmarkStatusCommand::BenchmarkStatus status) { + BenchmarkStatus status) { switch(status) { - case SetBenchmarkStatusCommand::SMT_SATISFIABLE: + case SMT_SATISFIABLE: return out << "sat"; - case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE: + case SMT_UNSATISFIABLE: return out << "unsat"; - case SetBenchmarkStatusCommand::SMT_UNKNOWN: + case SMT_UNKNOWN: return out << "unknown"; default: diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 5acd0736a..2bcd28422 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -40,6 +40,12 @@ Expr::Expr(const Expr& e) : d_node(new Node(*e.d_node)), d_exprManager(e.d_exprManager) { } +Expr::Expr(uintptr_t n) : + d_node(new Node()), + d_exprManager(NULL) { + AlwaysAssert(n==0); +} + ExprManager* Expr::getExprManager() const { return d_exprManager; } @@ -50,13 +56,26 @@ Expr::~Expr() { } Expr& Expr::operator=(const Expr& e) { - if(this != &e) { - ExprManagerScope ems(*this); - delete d_node; - d_node = new Node(*e.d_node); - d_exprManager = e.d_exprManager; + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); + ExprManagerScope ems(*this); + *d_node = *e.d_node; + d_exprManager = e.d_exprManager; + return *this; +} + +/* This should only ever be assigning NULL to a null Expr! */ +Expr& Expr::operator=(uintptr_t n) { + AlwaysAssert(n==0); + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + if( EXPECT_FALSE(!isNull()) ) { + *d_node = Node::null(); } return *this; +/* + Assert(isNull()); + return *this; +*/ } bool Expr::operator==(const Expr& e) const { diff --git a/src/expr/expr.h b/src/expr/expr.h index c5478b1da..48b64fd17 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -48,6 +48,14 @@ public: */ Expr(const Expr& e); + /** + * Initialize from an integer. Fails if the integer is not 0. + * NOTE: This is here purely to support the auto-initialization + * behavior of the ANTLR3 C backend. Should be removed if future + * versions of ANTLR fix the problem. + */ + Expr(uintptr_t n); + /** Destructor */ ~Expr(); @@ -61,6 +69,15 @@ public: Expr& operator=(const Expr& e); /** + * Assignment from an integer. Fails if the integer is not 0. + * NOTE: This is here purely to support the auto-initialization + * behavior of the ANTLR3 C backend (i.e., a rule attribute + * <code>Expr e</code> gets initialized with <code>e = NULL;</code>. + * Should be removed if future versions of ANTLR fix the problem. + */ + Expr& operator=(uintptr_t n); + + /** * Syntactic comparison operator. Returns true if expressions belong to the * same expression manager and are syntactically identical. * @param e the expression to compare to |