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;
*/
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();
${getConst_instantiations}
-#line 762 "${template}"
+#line 754 "${template}"
namespace expr {
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) {
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();
throw ParserException("Interactive input broken.");
}
- char* lineBuf;
+ char* lineBuf = NULL;
string input;
stringbuf sb;
string line;
/* 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;
@parser::includes {
+#include <stdint.h>
#include "expr/command.h"
#include "parser/parser.h"
#include "util/subrange_bound.h"
namespace CVC4 {
class Expr;
-}/* CVC4 namespace */
-namespace CVC4 {
namespace parser {
namespace cvc {
/**
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 */
* Parses an expression.
* @return the parsed expression
*/
-parseExpr returns [CVC4::Expr expr]
+parseExpr returns [CVC4::parser::cvc::myExpr expr]
: formula[expr]
| EOF
;
// 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 {
/**
** 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
#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"
#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
;
: identifier[name,check,SYM_SORT]
;
-sortSymbol returns [CVC4::Type t]
+sortSymbol returns [CVC4::parser::smt::myType t]
@declarations {
std::string name;
}
// 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 {
/**
** See the file COPYING in the top-level source directory for licensing
** information.
**/
-}
+}/* @header */
@lexer::includes {
#define ANTLR3_INLINE_INPUT_ASCII
#include "parser/antlr_tracing.h"
-}
+
+}/* @lexer::includes */
@lexer::postinclude {
#include <stdint.h>
#undef PARSER_STATE
#define PARSER_STATE ((Smt2*)LEXER->super)
-}
+}/* @lexer::postinclude */
@parser::includes {
#include "expr/command.h"
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"
#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
;
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);
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);
// 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);
#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)
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:
/**
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) {
projects / cvc5.git / commitdiff