From: Morgan Deters Date: Mon, 2 May 2011 05:04:36 +0000 (+0000) Subject: Minor fixes to various parts of CVC4, including the removal of the uintptr_t construc... X-Git-Tag: cvc5-1.0.0~8569 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=99c42d62491307279403059690fa31be1fb3af63;p=cvc5.git Minor fixes to various parts of CVC4, including the removal of the uintptr_t constructors for Type and Expr (which existed due to ANTLR limitations). These issues are now handled (as a hack, due to said limitations) in the parser rather than the CVC4 core. --- diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index b7000fea6..286ddf611 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -95,13 +95,6 @@ Expr::Expr(const Expr& e) : d_exprManager(e.d_exprManager) { } -Expr::Expr(uintptr_t n) : - d_node(new Node), - d_exprManager(NULL) { - - AlwaysAssert(n == 0); -} - Expr::~Expr() { ExprManagerScope ems(*this); delete d_node; diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 43d40105e..b0157adbf 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -153,14 +153,6 @@ 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(); @@ -758,7 +750,7 @@ public: ${getConst_instantiations} -#line 762 "${template}" +#line 754 "${template}" namespace expr { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 0df385a29..567bb2d40 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -53,12 +53,6 @@ Type::Type() : d_nodeManager(NULL) { } -Type::Type(uintptr_t n) : - d_typeNode(new TypeNode), - d_nodeManager(NULL) { - AlwaysAssert(n == 0); -} - Type::Type(const Type& t) : d_typeNode(new TypeNode(*t.d_typeNode)), d_nodeManager(t.d_nodeManager) { diff --git a/src/expr/type.h b/src/expr/type.h index 682e5fbcd..980a750d5 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -112,14 +112,6 @@ protected: public: - /** - * 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. - */ - Type(uintptr_t n); - /** Force a virtual destructor for safety. */ virtual ~Type(); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index cf04dacdf..707fc0ef3 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -130,7 +130,7 @@ Command* InteractiveShell::readCommand() { throw ParserException("Interactive input broken."); } - char* lineBuf; + char* lineBuf = NULL; string input; stringbuf sb; string line; @@ -138,12 +138,12 @@ Command* InteractiveShell::readCommand() { /* Prompt the user for input. */ if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline("CVC4> "); - if(lineBuf != NULL && lineBuf[0] != '\0') { - ::add_history(lineBuf); - } - line = lineBuf == NULL ? "" : lineBuf; - free(lineBuf); + lineBuf = ::readline("CVC4> "); + if(lineBuf != NULL && lineBuf[0] != '\0') { + ::add_history(lineBuf); + } + line = lineBuf == NULL ? "" : lineBuf; + free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { d_out << "CVC4> " << flush; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 8df9ea6a0..af0024156 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -433,6 +433,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { @parser::includes { +#include #include "expr/command.h" #include "parser/parser.h" #include "util/subrange_bound.h" @@ -440,9 +441,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { namespace CVC4 { class Expr; -}/* CVC4 namespace */ -namespace CVC4 { namespace parser { namespace cvc { /** @@ -469,6 +468,17 @@ namespace CVC4 { mySubrangeBound(const Integer& i) : CVC4::SubrangeBound(i) {} mySubrangeBound(const SubrangeBound& b) : CVC4::SubrangeBound(b) {} };/* class mySubrangeBound */ + + /** + * Just exists to give us the uintptr_t construction that + * ANTLR requires. + */ + struct myExpr : public CVC4::Expr { + myExpr() : CVC4::Expr() {} + myExpr(uintptr_t) : CVC4::Expr() {} + myExpr(const Expr& e) : CVC4::Expr(e) {} + myExpr(const myExpr& e) : CVC4::Expr(e) {} + };/* struct myExpr */ }/* CVC4::parser::cvc namespace */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ @@ -521,7 +531,7 @@ using namespace CVC4::parser; * Parses an expression. * @return the parsed expression */ -parseExpr returns [CVC4::Expr expr] +parseExpr returns [CVC4::parser::cvc::myExpr expr] : formula[expr] | EOF ; diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index e964c020a..0cceb53e4 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -29,7 +29,7 @@ options { // Note that CVC4's BoundedTokenBuffer requires a fixed k ! // If you change this k, change it also in smt_input.cpp ! k = 2; -} +}/* options */ @header { /** @@ -40,7 +40,7 @@ options { ** See the file COPYING in the top-level source directory for licensing ** information. **/ -} +}/* @header */ @lexer::includes { /** This suppresses warnings about the redefinition of token symbols between @@ -58,19 +58,50 @@ options { #define ANTLR3_INLINE_INPUT_ASCII #include "parser/antlr_tracing.h" -} +}/* @lexer::includes */ @parser::includes { + +#include + #include "expr/command.h" #include "parser/parser.h" #include "parser/antlr_tracing.h" namespace CVC4 { class Expr; + + namespace parser { + namespace smt { + /** + * Just exists to provide the uintptr_t constructor that ANTLR + * requires. + */ + struct myExpr : public CVC4::Expr { + myExpr() : CVC4::Expr() {} + myExpr(void*) : CVC4::Expr() {} + myExpr(const Expr& e) : CVC4::Expr(e) {} + myExpr(const myExpr& e) : CVC4::Expr(e) {} + };/* struct myExpr */ + + /** + * Just exists to provide the uintptr_t constructor that ANTLR + * requires. + */ + struct myType : public CVC4::Type { + myType() : CVC4::Type() {} + myType(void*) : CVC4::Type() {} + myType(const Type& t) : CVC4::Type(t) {} + myType(const myType& t) : CVC4::Type(t) {} + };/* struct myType */ + }/* CVC4::parser::smt namespace */ + }/* CVC4::parser namespace */ }/* CVC4 namespace */ -} + +}/* @parser::includes */ @parser::postinclude { + #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" @@ -96,14 +127,14 @@ using namespace CVC4::parser; #undef MK_CONST #define MK_CONST EXPR_MANAGER->mkConst -} +}/* @parser::postinclude */ /** * Parses an expression. * @return the parsed expression */ -parseExpr returns [CVC4::Expr expr] +parseExpr returns [CVC4::parser::smt::myExpr expr] : annotatedFormula[expr] | EOF ; @@ -445,7 +476,7 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check] : identifier[name,check,SYM_SORT] ; -sortSymbol returns [CVC4::Type t] +sortSymbol returns [CVC4::parser::smt::myType t] @declarations { std::string name; } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 17ea1611d..a8dfbfeab 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -29,7 +29,7 @@ options { // Note that CVC4's BoundedTokenBuffer requires a fixed k ! // If you change this k, change it also in smt2_input.cpp ! k = 2; -} +}/* options */ @header { /** @@ -40,7 +40,7 @@ options { ** See the file COPYING in the top-level source directory for licensing ** information. **/ -} +}/* @header */ @lexer::includes { @@ -59,7 +59,8 @@ options { #define ANTLR3_INLINE_INPUT_ASCII #include "parser/antlr_tracing.h" -} + +}/* @lexer::includes */ @lexer::postinclude { #include @@ -73,7 +74,7 @@ using namespace CVC4::parser; #undef PARSER_STATE #define PARSER_STATE ((Smt2*)LEXER->super) -} +}/* @lexer::postinclude */ @parser::includes { #include "expr/command.h" @@ -81,10 +82,27 @@ using namespace CVC4::parser; namespace CVC4 { class Expr; + + namespace parser { + namespace smt2 { + /** + * Just exists to provide the uintptr_t constructor that ANTLR + * requires. + */ + struct myExpr : public CVC4::Expr { + myExpr() : CVC4::Expr() {} + myExpr(void*) : CVC4::Expr() {} + myExpr(const Expr& e) : CVC4::Expr(e) {} + myExpr(const myExpr& e) : CVC4::Expr(e) {} + };/* struct myExpr */ + }/* CVC4::parser::smt2 namespace */ + }/* CVC4::parser namespace */ }/* CVC4 namespace */ -} + +}/* @parser::includes */ @parser::postinclude { + #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" @@ -110,13 +128,13 @@ using namespace CVC4::parser; #undef MK_CONST #define MK_CONST EXPR_MANAGER->mkConst -} +}/* parser::postinclude */ /** * Parses an expression. * @return the parsed expression, or the Null Expr if we've reached the end of the input */ -parseExpr returns [CVC4::Expr expr] +parseExpr returns [CVC4::parser::smt2::myExpr expr] : term[expr] | EOF ; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 45c697d0b..60346ab2e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -128,7 +128,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_context(em->getContext()), d_userContext(new Context()), d_exprManager(em), - d_nodeManager(d_exprManager->getNodeManager()) { + d_nodeManager(d_exprManager->getNodeManager()), + d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), + d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), + d_staticLearningTime("smt::SmtEngine::staticLearningTime") { NodeManagerScope nms(d_nodeManager); @@ -448,6 +451,8 @@ Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in) try { Node n; if(!Options::current()->lazyDefinitionExpansion) { + TimerStat::CodeTimer codeTimer(smt.d_definitionExpansionTime); + Chat() << "Expanding definitions: " << in << endl; Debug("expand") << "have: " << n << endl; hash_map cache; n = expandDefinitions(smt, in, cache); @@ -459,6 +464,8 @@ Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in) // For now, don't re-statically-learn from learned facts; this could // be useful though (e.g., theory T1 could learn something further // from something learned previously by T2). + Chat() << "Performing static learning: " << n << endl; + TimerStat::CodeTimer codeTimer(smt.d_staticLearningTime); NodeBuilder<> learned(kind::AND); learned << n; smt.d_theoryEngine->staticLearning(n, learned); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b872985fb..408db1a2f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -35,6 +35,7 @@ #include "util/options.h" #include "util/result.h" #include "util/sexpr.h" +#include "util/stats.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -179,6 +180,14 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::smt::SmtEnginePrivate; + // === STATISTICS === + /** time spent in definition-expansion */ + TimerStat d_definitionExpansionTime; + /** time spent in non-clausal simplification */ + TimerStat d_nonclausalSimplificationTime; + /** time spent in static learning */ + TimerStat d_staticLearningTime; + public: /** diff --git a/src/util/dynamic_array.h b/src/util/dynamic_array.h index c1298500e..c0a8cf260 100644 --- a/src/util/dynamic_array.h +++ b/src/util/dynamic_array.h @@ -38,7 +38,7 @@ private: void grow(){ bool empty = (d_arr == NULL); - d_allocated = empty ? d_allocated = 15 : d_allocated * 2 + 1; + d_allocated = empty ? 15 : d_allocated * 2 + 1; unsigned allocSize = sizeof(T) * d_allocated; T* tmpList = (T*) (empty ? malloc(allocSize) :realloc(d_arr, allocSize)); if(tmpList == NULL) {