diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-17 08:39:27 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-17 08:39:27 +0000 |
commit | 7293554b109742697d4d928ed7b58acadc6de947 (patch) | |
tree | 73e057306fac266b5c9ca9cf12ae050f73c43bdf /src | |
parent | acd68152ff9600bdff208376f2cd43f09d45cdc8 (diff) |
another pass
Diffstat (limited to 'src')
35 files changed, 174 insertions, 114 deletions
diff --git a/src/core/expr.cpp b/src/core/expr.cpp index 1af197f27..cdc7e6775 100644 --- a/src/core/expr.cpp +++ b/src/core/expr.cpp @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** expr.cpp ** This file is part of the CVC4 prototype. - ** - ** Reference-counted encapsulation of a pointer to an expression. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Reference-counted encapsulation of a pointer to an expression. **/ #include "expr.h" diff --git a/src/core/expr_manager.cpp b/src/core/expr_manager.cpp index 93903c3aa..c18fd9652 100644 --- a/src/core/expr_manager.cpp +++ b/src/core/expr_manager.cpp @@ -1,10 +1,13 @@ /********************* -*- C++ -*- */ /** expr_manager.cpp ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Expression manager implementation. **/ #include <vector> diff --git a/src/core/expr_value.cpp b/src/core/expr_value.cpp index b7c65023e..b42773482 100644 --- a/src/core/expr_value.cpp +++ b/src/core/expr_value.cpp @@ -1,16 +1,17 @@ -/********************* +/********************* -*- C++ -*- */ /** expr_value.cpp ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. ** ** An expression node. ** ** Instances of this class are generally referenced through ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the ** reference count on ExprValue instances and - ** - ** The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University **/ #include "expr_value.h" diff --git a/src/include/assert.h b/src/include/assert.h index 473cd21f1..a66503641 100644 --- a/src/include/assert.h +++ b/src/include/assert.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** assert.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_ASSERT_H diff --git a/src/include/attr_type.h b/src/include/attr_type.h index e5eb222fe..d24385f8e 100644 --- a/src/include/attr_type.h +++ b/src/include/attr_type.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** attr_type.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_ATTR_TYPE_H diff --git a/src/include/command.h b/src/include/command.h index 45b59a95b..944b9c621 100644 --- a/src/include/command.h +++ b/src/include/command.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** command.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_COMMAND_H diff --git a/src/include/context.h b/src/include/context.h index 1997e63d6..fce2f0b8d 100644 --- a/src/include/context.h +++ b/src/include/context.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** context.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_CONTEXT_H diff --git a/src/include/debug.h b/src/include/debug.h index 95e705bcb..36942d1ae 100644 --- a/src/include/debug.h +++ b/src/include/debug.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** debug.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_DEBUG_H diff --git a/src/include/decision_engine.h b/src/include/decision_engine.h index 8745adad5..ec0172535 100644 --- a/src/include/decision_engine.h +++ b/src/include/decision_engine.h @@ -1,17 +1,19 @@ /********************* -*- C++ -*- */ /** decision_engine.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ -#include "literal.h" - #ifndef __CVC4_DECISION_ENGINE_H #define __CVC4_DECISION_ENGINE_H +#include "literal.h" + namespace CVC4 { // In terms of abstraction, this is below (and provides services to) diff --git a/src/include/exception.h b/src/include/exception.h index ce19b0d68..792a98701 100644 --- a/src/include/exception.h +++ b/src/include/exception.h @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** exception.h ** This file is part of the CVC4 prototype. - ** - ** Exception class. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Exception class. **/ #ifndef __CVC4_EXCEPTION_H diff --git a/src/include/expr.h b/src/include/expr.h index 9ca449ce7..e92ece93d 100644 --- a/src/include/expr.h +++ b/src/include/expr.h @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** expr.h ** This file is part of the CVC4 prototype. - ** - ** Reference-counted encapsulation of a pointer to an expression. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Reference-counted encapsulation of a pointer to an expression. **/ #ifndef __CVC4_EXPR_H diff --git a/src/include/expr_attribute.h b/src/include/expr_attribute.h index 1c10a6663..77700096e 100644 --- a/src/include/expr_attribute.h +++ b/src/include/expr_attribute.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** expr_attribute.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_EXPR_ATTRIBUTE_H diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h index 342834e37..a95ecb2e3 100644 --- a/src/include/expr_builder.h +++ b/src/include/expr_builder.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** expr_builder.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_EXPR_BUILDER_H diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h index 5dae5b854..59a3eb7a3 100644 --- a/src/include/expr_manager.h +++ b/src/include/expr_manager.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** expr_manager.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_EXPR_MANAGER_H diff --git a/src/include/expr_value.h b/src/include/expr_value.h index c15241ebf..ea14c3fa7 100644 --- a/src/include/expr_value.h +++ b/src/include/expr_value.h @@ -1,16 +1,17 @@ -/********************* +/********************* -*- C++ -*- */ /** expr_value.h ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. ** ** An expression node. ** ** Instances of this class are generally referenced through ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the ** reference count on ExprValue instances and - ** - ** The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University **/ #ifndef __CVC4_EXPR_VALUE_H diff --git a/src/include/kind.h b/src/include/kind.h index a015a6b71..5d99330ca 100644 --- a/src/include/kind.h +++ b/src/include/kind.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** kind.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_KIND_H diff --git a/src/include/literal.h b/src/include/literal.h index 93855edb8..8b147c640 100644 --- a/src/include/literal.h +++ b/src/include/literal.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** literal.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_LITERAL_H diff --git a/src/include/model.h b/src/include/model.h index 205dcf18f..c07b75dfa 100644 --- a/src/include/model.h +++ b/src/include/model.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** model.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_MODEL_H diff --git a/src/include/parser.h b/src/include/parser.h index 63a448b28..e30b31b1c 100644 --- a/src/include/parser.h +++ b/src/include/parser.h @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** parser.h ** This file is part of the CVC4 prototype. - ** - ** Parser abstraction. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Parser abstraction. **/ #ifndef __CVC4_PARSER_H diff --git a/src/include/parser_exception.h b/src/include/parser_exception.h index 8bad801f4..debb75e70 100644 --- a/src/include/parser_exception.h +++ b/src/include/parser_exception.h @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ -/** exception.h +/** parser_exception.h ** This file is part of the CVC4 prototype. - ** - ** Exception class. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Exception class. **/ #ifndef __CVC4_PARSER_EXCEPTION_H diff --git a/src/include/prop_engine.h b/src/include/prop_engine.h index 90d07a47b..de25c5594 100644 --- a/src/include/prop_engine.h +++ b/src/include/prop_engine.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** prop_engine.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_PROP_ENGINE_H diff --git a/src/include/prover.h b/src/include/prover.h index e48d6336c..de29f48c0 100644 --- a/src/include/prover.h +++ b/src/include/prover.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** prover.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_PROVER_H diff --git a/src/include/result.h b/src/include/result.h index cfabd3be2..50f488682 100644 --- a/src/include/result.h +++ b/src/include/result.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** result.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_RESULT_H diff --git a/src/include/sat.h b/src/include/sat.h index 13578ec8d..00a94c142 100644 --- a/src/include/sat.h +++ b/src/include/sat.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** sat.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_SAT_H diff --git a/src/include/theory.h b/src/include/theory.h index 5c50c7a37..935c23b08 100644 --- a/src/include/theory.h +++ b/src/include/theory.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** theory.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_THEORY_H diff --git a/src/include/theory_engine.h b/src/include/theory_engine.h index f4e36f604..2a0841d8d 100644 --- a/src/include/theory_engine.h +++ b/src/include/theory_engine.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** theory_engine.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_THEORY_ENGINE_H diff --git a/src/include/unique_id.h b/src/include/unique_id.h index 55fa24e51..1a6f3427a 100644 --- a/src/include/unique_id.h +++ b/src/include/unique_id.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** unique_id.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_UNIQUE_ID_H diff --git a/src/include/vc.h b/src/include/vc.h index 57d8a957e..845d1eb6d 100644 --- a/src/include/vc.h +++ b/src/include/vc.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** vc.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** **/ #ifndef __CVC4_VC_H diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 8cf9f4a6d..a9560ab93 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -12,10 +12,10 @@ libparser_a_SOURCES = \ BUILT_SOURCES = \ pl_scanner.cpp \ pl.cpp \ - pl.h \ + pl.hpp \ smtlib_scanner.cpp \ smtlib.cpp \ - smtlib.h + smtlib.hpp # produce headers too AM_YFLAGS = -d @@ -25,11 +25,11 @@ pl_scanner.cpp: pl_scanner.lpp smtlib_scanner.cpp: smtlib_scanner.lpp $(LEX) $(AM_LFLAGS) $(LFLAGS) -P smtlib -o $@ $< -pl_scanner.o: pl.h +pl_scanner.o: pl.hpp pl.cpp: pl.ypp $(YACC) $(AM_YFLAGS) $(YFLAGS) -p PL -o $@ $< -smtlib_scanner.o: smtlib.h +smtlib_scanner.o: smtlib.hpp smtlib.cpp: smtlib.ypp $(YACC) $(AM_YFLAGS) $(YFLAGS) -p smtlib -o $@ $< diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 35ca74ecd..89170beeb 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -1,6 +1,11 @@ /********************* -*- C++ -*- */ /** parser.cpp ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. ** ** Parser implementation. ** diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 4444925e2..6ab0ada49 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -1,6 +1,11 @@ /********************* -*- C++ -*- */ /** parser_state.h ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. ** ** Extra state of the parser shared by the lexer and parser. ** diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index e9aeab78e..d8fd57c8c 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -1,12 +1,11 @@ /********************* -*- C++ -*- */ -/** smtlib.ypp +/** pl.ypp ** This file is part of the CVC4 prototype. - ** - ** Reference-counted encapsulation of a pointer to an expression. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. ** ** This file contains the bison code for the parser that reads in CVC ** commands in the presentation language (hence "PL"). diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp index d70937e34..ba8a8e85d 100644 --- a/src/parser/pl_scanner.lpp +++ b/src/parser/pl_scanner.lpp @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** pl_scanner.lpp ** This file is part of the CVC4 prototype. - ** - ** Reference-counted encapsulation of a pointer to an expression. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** CVC4 presentation language lexer. **/ %option interactive @@ -22,7 +23,7 @@ #include <iostream> #include "expr_manager.h" /* for the benefit of parsePL_defs.h */ #include "parser_state.h" -#include "pl.h" +#include "pl.hpp" #include "debug.h" namespace CVC4 { diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index 97f61e715..0f3aa8cf4 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -1,12 +1,11 @@ -%{/******************* -*- C++ -*- */ +%{/********************* -*- C++ -*- */ /** smtlib.ypp ** This file is part of the CVC4 prototype. - ** - ** Reference-counted encapsulation of a pointer to an expression. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. ** ** This file contains the bison code for the parser that reads in CVC ** commands in SMT-LIB language. @@ -17,18 +16,18 @@ #include "parser_state.h" // Exported shared data -namespace CVC3 { - extern ParserTemp* parserTemp; +namespace CVC4 { + extern ParserState* parserState; } // Define shortcuts for various things -#define TMP CVC3::parserTemp -#define EXPR CVC3::parserTemp->expr -#define VC (CVC3::parserTemp->vc) -#define ARRAYSENABLED (CVC3::parserTemp->arrFlag) -#define BVENABLED (CVC3::parserTemp->bvFlag) -#define BVSIZE (CVC3::parserTemp->bvSize) -#define RAT(args) CVC3::newRational args -#define QUERYPARSED CVC3::parserTemp->queryParsed +#define TMP CVC4::parserState +#define EXPR CVC4::parserState->expr +#define VC (CVC4::parserState->vc) +#define ARRAYSENABLED (CVC4::parserState->arrFlag) +#define BVENABLED (CVC4::parserState->bvFlag) +#define BVSIZE (CVC4::parserState->bvSize) +#define RAT(args) CVC4::newRational args +#define QUERYPARSED CVC4::parserState->queryParsed // Suppress the bogus warning suppression in bison (it generates // compile error) @@ -40,9 +39,9 @@ extern int smtliblex(void); int smtliberror(const char *s) { std::ostringstream ss; - ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum + ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum << ": " << s; - return CVC3::parserTemp->error(ss.str()); + return CVC4::parserState->error(ss.str()); } @@ -55,9 +54,9 @@ int smtliberror(const char *s) %union { std::string *str; std::vector<std::string> *strvec; - CVC3::Expr *node; - std::vector<CVC3::Expr> *vec; - std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann; + CVC4::Expr *node; + std::vector<CVC4::Expr> *vec; + std::pair<std::vector<CVC4::Expr>, std::vector<std::string> > *pat_ann; }; diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp index b78b27a0d..bb5802aed 100644 --- a/src/parser/smtlib_scanner.lpp +++ b/src/parser/smtlib_scanner.lpp @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** smtlib_scanner.lpp ** This file is part of the CVC4 prototype. - ** - ** Reference-counted encapsulation of a pointer to an expression. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Lexer for smtlib format. **/ %option interactive @@ -19,7 +20,7 @@ %{ #include <iostream> -#include "smtlib.h" +#include "smtlib.hpp" #include "debug.h" namespace CVC4 { |