summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_template.cpp7
-rw-r--r--src/expr/expr_template.h10
-rw-r--r--src/expr/type.cpp6
-rw-r--r--src/expr/type.h8
-rw-r--r--src/main/interactive_shell.cpp14
-rw-r--r--src/parser/cvc/Cvc.g16
-rw-r--r--src/parser/smt/Smt.g45
-rw-r--r--src/parser/smt2/Smt2.g32
-rw-r--r--src/smt/smt_engine.cpp9
-rw-r--r--src/smt/smt_engine.h9
-rw-r--r--src/util/dynamic_array.h2
11 files changed, 102 insertions, 56 deletions
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 <stdint.h>
#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 <stdint.h>
+
#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 <stdint.h>
@@ -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<TNode, Node, TNodeHashFunction> 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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback