From: Morgan Deters Date: Tue, 24 Nov 2009 22:51:35 +0000 (+0000) Subject: various fixes and updates to use and support parser X-Git-Tag: cvc5-1.0.0~9410 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=61937ea05bff33070cc8252bc3b6c7d6fed7c9c3;p=cvc5.git various fixes and updates to use and support parser --- diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index a270e7362..5c1f605c9 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -27,6 +27,24 @@ my $excluded_directories = '^(minisat|CVS)$'; # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever. my $years = '2009'; +my $standard_template = <) { last if $line =~ /^ \*\*\s*$/; @@ -111,12 +124,7 @@ sub recurse { print $OUT "/********************* -*- C++ -*- */\n"; } print $OUT "/** $file\n"; - print $OUT " ** This file is part of the CVC4 prototype.\n"; - print $OUT " ** Copyright (c) $years The Analysis of Computer Systems Group (ACSys)\n"; - print $OUT " ** Courant Institute of Mathematical Sciences\n"; - print $OUT " ** New York University\n"; - print $OUT " ** See the file COPYING in the top-level source directory for licensing\n"; - print $OUT " ** information.\n"; + print $OUT $standard_template; print $OUT " **\n"; print $OUT " ** [[ Add file-specific comments here ]]\n"; print $OUT " **/\n\n"; diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index e25cf8595..f94a3c438 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -86,13 +86,4 @@ Expr Expr::xorExpr(const Expr& right) const { return ExprBuilder(*this).xorExpr(right); } -Expr Expr::skolemExpr(int i) const { - return ExprBuilder(*this).skolemExpr(i); -} - -Expr Expr::substExpr(const std::vector& oldTerms, - const std::vector& newTerms) const { - return ExprBuilder(*this).substExpr(oldTerms, newTerms); -} - }/* CVC4 namespace */ diff --git a/src/expr/expr.h b/src/expr/expr.h index d99708991..19f02650e 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -10,8 +10,8 @@ ** Reference-counted encapsulation of a pointer to an expression. **/ -#ifndef __CVC4_EXPR_H -#define __CVC4_EXPR_H +#ifndef __CVC4__EXPR_H +#define __CVC4__EXPR_H #include #include @@ -74,9 +74,6 @@ public: Expr iffExpr(const Expr& right) const; Expr impExpr(const Expr& right) const; Expr xorExpr(const Expr& right) const; - Expr skolemExpr(int i) const; - Expr substExpr(const std::vector& oldTerms, - const std::vector& newTerms) const; Expr plusExpr(const Expr& right) const; Expr uMinusExpr() const; @@ -100,4 +97,4 @@ inline Kind Expr::getKind() const { }/* CVC4 namespace */ -#endif /* __CVC4_EXPR_H */ +#endif /* __CVC4__EXPR_H */ diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index bf572cfbc..be9c60199 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -157,14 +157,6 @@ ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::skolemExpr(int i) { - Assert( d_kind != UNDEFINED_KIND ); - collapse(); - d_kind = SKOLEM; - //addChild(i);//FIXME: int constant - return *this; -} - // "Stream" expression constructor syntax ExprBuilder& ExprBuilder::operator<<(const Kind& op) { return *this; @@ -217,37 +209,13 @@ void ExprBuilder::addChild(ExprValue* ev) { } } -void ExprBuilder::collapse() { +ExprBuilder& ExprBuilder::collapse() { if(d_nchildren == nchild_thresh) { vector* v = new vector(); v->reserve(nchild_thresh + 5); - + // } -} - -// not const -ExprBuilder::operator Expr() { - // FIXME -} - -AndExprBuilder ExprBuilder::operator&&(Expr e) { - return AndExprBuilder(*this) && e; -} - -OrExprBuilder ExprBuilder::operator||(Expr e) { - return OrExprBuilder(*this) || e; -} - -PlusExprBuilder ExprBuilder::operator+ (Expr e) { - return PlusExprBuilder(*this) + e; -} - -PlusExprBuilder ExprBuilder::operator- (Expr e) { - return PlusExprBuilder(*this) - e; -} - -MultExprBuilder ExprBuilder::operator* (Expr e) { - return MultExprBuilder(*this) * e; + return *this; } }/* CVC4 namespace */ diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index 97f18ca6d..13f196dd0 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -43,7 +43,7 @@ class ExprBuilder { void addChild(const Expr&); void addChild(ExprValue*); - void collapse(); + ExprBuilder& collapse(); typedef ExprValue** ev_iterator; typedef ExprValue const** const_ev_iterator; @@ -74,12 +74,6 @@ public: ExprBuilder& iffExpr(const Expr& right); ExprBuilder& impExpr(const Expr& right); ExprBuilder& xorExpr(const Expr& right); - ExprBuilder& skolemExpr(int i); - ExprBuilder& substExpr(const std::vector& oldTerms, - const std::vector& newTerms); - /* - ExprBuilder& substExpr(const ExprHashMap& oldToNew); - */ /* TODO design: these modify ExprBuilder */ ExprBuilder& operator!() { return notExpr(); } @@ -92,6 +86,7 @@ public: // For pushing sequences of children ExprBuilder& append(const std::vector& children) { return append(children.begin(), children.end()); } + ExprBuilder& append(Expr child) { return append(&child, &(child)+1); } template ExprBuilder& append(const Iterator& begin, const Iterator& end); operator Expr();// not const @@ -102,71 +97,167 @@ public: PlusExprBuilder operator- (Expr); MultExprBuilder operator* (Expr); + friend class AndExprBuilder; + friend class OrExprBuilder; + friend class PlusExprBuilder; + friend class MultExprBuilder; };/* class ExprBuilder */ class AndExprBuilder { - ExprManager* d_em; + ExprBuilder d_eb; public: - AndExprBuilder(const ExprBuilder&); + AndExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != AND) { + d_eb.collapse(); + d_eb.d_kind = AND; + } + } AndExprBuilder& operator&&(Expr); OrExprBuilder operator||(Expr); - operator ExprBuilder(); + operator ExprBuilder() { return d_eb; } };/* class AndExprBuilder */ class OrExprBuilder { - ExprManager* d_em; + ExprBuilder d_eb; public: - OrExprBuilder(const ExprBuilder&); + OrExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != OR) { + d_eb.collapse(); + d_eb.d_kind = OR; + } + } AndExprBuilder operator&&(Expr); OrExprBuilder& operator||(Expr); - operator ExprBuilder(); + operator ExprBuilder() { return d_eb; } };/* class OrExprBuilder */ class PlusExprBuilder { - ExprManager* d_em; + ExprBuilder d_eb; public: - PlusExprBuilder(const ExprBuilder&); + PlusExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != PLUS) { + d_eb.collapse(); + d_eb.d_kind = PLUS; + } + } PlusExprBuilder& operator+(Expr); PlusExprBuilder& operator-(Expr); MultExprBuilder operator*(Expr); - operator ExprBuilder(); + operator ExprBuilder() { return d_eb; } };/* class PlusExprBuilder */ class MultExprBuilder { - ExprManager* d_em; + ExprBuilder d_eb; public: - MultExprBuilder(const ExprBuilder&); + MultExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != MULT) { + d_eb.collapse(); + d_eb.d_kind = MULT; + } + } PlusExprBuilder operator+(Expr); PlusExprBuilder operator-(Expr); MultExprBuilder& operator*(Expr); - operator ExprBuilder(); + operator ExprBuilder() { return d_eb; } };/* class MultExprBuilder */ template -ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) { +inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) { + return *this; +} + +// not const +inline ExprBuilder::operator Expr() { + // FIXME + return Expr::s_null; +} + +inline AndExprBuilder ExprBuilder::operator&&(Expr e) { + return AndExprBuilder(*this) && e; +} + +inline OrExprBuilder ExprBuilder::operator||(Expr e) { + return OrExprBuilder(*this) || e; +} + +inline PlusExprBuilder ExprBuilder::operator+ (Expr e) { + return PlusExprBuilder(*this) + e; +} + +inline PlusExprBuilder ExprBuilder::operator- (Expr e) { + return PlusExprBuilder(*this) - e; +} + +inline MultExprBuilder ExprBuilder::operator* (Expr e) { + return MultExprBuilder(*this) * e; +} + +inline AndExprBuilder& AndExprBuilder::operator&&(Expr e) { + d_eb.append(e); + return *this; +} + +inline OrExprBuilder AndExprBuilder::operator||(Expr e) { + return OrExprBuilder(d_eb.collapse()) || e; +} + +inline AndExprBuilder OrExprBuilder::operator&&(Expr e) { + return AndExprBuilder(d_eb.collapse()) && e; +} + +inline OrExprBuilder& OrExprBuilder::operator||(Expr e) { + d_eb.append(e); + return *this; +} + +inline PlusExprBuilder& PlusExprBuilder::operator+(Expr e) { + d_eb.append(e); + return *this; +} + +inline PlusExprBuilder& PlusExprBuilder::operator-(Expr e) { + d_eb.append(e.negate()); return *this; } +inline MultExprBuilder PlusExprBuilder::operator*(Expr e) { + return MultExprBuilder(d_eb.collapse()) * e; +} + +inline PlusExprBuilder MultExprBuilder::operator+(Expr e) { + return MultExprBuilder(d_eb.collapse()) + e; +} + +inline PlusExprBuilder MultExprBuilder::operator-(Expr e) { + return MultExprBuilder(d_eb.collapse()) - e; +} + +inline MultExprBuilder& MultExprBuilder::operator*(Expr e) { + d_eb.append(e); + return *this; +} + + }/* CVC4 namespace */ #endif /* __CVC4__EXPR_BUILDER_H */ diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index a65a2f3cd..3aeab8049 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -12,7 +12,7 @@ #include "expr_builder.h" #include "expr_manager.h" -#include "cvc4_expr.h" +#include "expr/expr.h" namespace CVC4 { diff --git a/src/include/cvc4.h b/src/include/cvc4.h index 7b068228f..5d33fa838 100644 --- a/src/include/cvc4.h +++ b/src/include/cvc4.h @@ -18,29 +18,19 @@ #include "util/result.h" #include "util/model.h" -// In terms of abstraction, this is below (and provides services to) -// ValidityChecker and above (and requires the services of) -// PropEngine. - namespace CVC4 { -// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the -// hood): use a type parameter and have check() delegate, or subclass -// SmtEngine and override check()? -// -// Probably better than that is to have a configuration object that -// indicates which passes are desired. The configuration occurs -// elsewhere (and can even occur at runtime). A simple "pass manager" -// of sorts determines check()'s behavior. -// -// The CNF conversion can go on in PropEngine. - class SmtEngine { /** Current set of assertions. */ // TODO: make context-aware to handle user-level push/pop. std::vector d_assertList; -private: + /** Our expression manager */ + ExprManager *d_em; + + /** User-level options */ + Options *opts; + /** * Pre-process an Expr. This is expected to be highly-variable, * with a lot of "source-level configurability" to add multiple @@ -74,10 +64,15 @@ private: void processAssertionList(); public: + /* + * Construct an SmtEngine with the given expression manager and user options. + */ + SmtEngine(ExprManager*, Options*); + /** - * Execute a command + * Execute a command. */ - void doCommand(Command c); + void doCommand(Command*); /** * Add a formula to the current context: preprocess, do per-theory diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h index d99708991..863097123 100644 --- a/src/include/cvc4_expr.h +++ b/src/include/cvc4_expr.h @@ -74,9 +74,6 @@ public: Expr iffExpr(const Expr& right) const; Expr impExpr(const Expr& right) const; Expr xorExpr(const Expr& right) const; - Expr skolemExpr(int i) const; - Expr substExpr(const std::vector& oldTerms, - const std::vector& newTerms) const; Expr plusExpr(const Expr& right) const; Expr uMinusExpr() const; diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index dcb23c303..5af3b5d21 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -25,9 +25,11 @@ #include "util/exception.h" #include "usage.h" #include "about.h" +#include "parser/language.h" using namespace std; using namespace CVC4; +using namespace CVC4::parser; namespace CVC4 { namespace main { @@ -39,12 +41,6 @@ Languages currently supported to the -L / --lang option:\n\ smt | smtlib SMT-LIB format\n\ "; -enum Language { - AUTO = 0, - PL, - SMTLIB, -};/* enum Language */ - enum OptionValue { SMTCOMP = 256, /* no clash with char options */ STATS diff --git a/src/main/main.cpp b/src/main/main.cpp index 8529f2ca2..1fc616fe6 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -10,6 +10,8 @@ ** [[ Add file-specific comments here ]] **/ +#include +#include #include #include #include @@ -23,9 +25,14 @@ #include "config.h" #include "main.h" #include "usage.h" +#include "parser/parser.h" +#include "expr/expr_manager.h" +#include "smt/smt_engine.h" +#include "parser/language.h" using namespace std; using namespace CVC4; +using namespace CVC4::parser; using namespace CVC4::main; int main(int argc, char *argv[]) { @@ -36,28 +43,37 @@ int main(int argc, char *argv[]) { int firstArgIndex = parseOptions(argc, argv, &opts); - FILE *infile; + istream *in; + ifstream infile; + Language lang = PL; if(firstArgIndex >= argc) { - infile = stdin; + in = &cin; } else if(argc > firstArgIndex + 1) { throw new Exception("Too many input files specified."); } else { - infile = fopen(argv[firstArgIndex], "r"); + in = &infile; + if(strlen(argv[firstArgIndex]) >= 4 && !strcmp(argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4, ".smt")) + lang = SMTLIB; + infile.open(argv[firstArgIndex], ifstream::in); + if(!infile) { throw new Exception(string("Could not open input file `") + argv[firstArgIndex] + "' for reading: " + strerror(errno)); exit(1); } + } - // ExprManager *exprMgr = ...; - // SmtEngine smt(exprMgr, &opts); - // Parser parser(infile, exprMgr, &opts); - // while(!parser.done) { - // Command *cmd = parser.get(); - // cmd->invoke(smt); - // delete cmd; - // } + ExprManager *exprMgr = new ExprManager(); + SmtEngine smt(exprMgr, &opts); + Parser parser(&smt, lang, *in, &opts); + while(!parser.done()) { + Command *cmd = parser.next(); + cmd->invoke(); + delete cmd; } + + if(infile) + infile.close(); } catch(CVC4::main::OptionException* e) { if(opts.smtcomp_mode) { printf("unknown"); diff --git a/src/parser/language.h b/src/parser/language.h new file mode 100644 index 000000000..7ea6547cd --- /dev/null +++ b/src/parser/language.h @@ -0,0 +1,31 @@ +/********************* -*- C++ -*- */ +/** language.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. + ** + ** Input languages. + **/ + +#ifndef __CVC4__PARSER__LANGUAGE_H +#define __CVC4__PARSER__LANGUAGE_H + +#include "util/exception.h" +#include "parser/language.h" + +namespace CVC4 { +namespace parser { + +enum Language { + AUTO = 0, + PL, + SMTLIB, +};/* enum Language */ + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__LANGUAGE_H */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 36b8c34eb..73565b8c4 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -13,13 +13,13 @@ #ifndef __CVC4__PARSER__PARSER_H #define __CVC4__PARSER__PARSER_H -#include "core/exception.h" -#include "core/lang.h" +#include "util/exception.h" +#include "parser/language.h" +#include "util/command.h" namespace CVC4 { namespace parser { - class ValidityChecker; class Expr; // Internal parser state and other data @@ -33,16 +33,11 @@ namespace parser { void deleteParser(); public: // Constructors - Parser(ValidityChecker* vc, InputLanguage lang, - // The 'interactive' flag is ignored when fileName != "" - bool interactive = true, - const std::string& fileName = ""); - Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is, - bool interactive = false); + Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, Options* opts, bool interactive = false); // Destructor ~Parser(); // Read the next command. - Expr next(); + CVC4::Command* next(); // Check if we are done (end of input has been reached) bool done() const; // The same check can be done by using the class Parser's value as diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 4eda5eb38..1d013a0b4 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -19,7 +19,7 @@ #include #include -#include "cvc4_expr.h" +#include "expr/expr.h" #include "expr/expr_manager.h" #include "util/exception.h" diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index e7d752419..b59c7c69e 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -13,10 +13,10 @@ %{ -#include "cvc4.h" -#include "cvc4_expr.h" +#include "smt/smt_engine.h" #include "parser/parser_exception.h" #include "parser/parser_state.h" +#include "expr/expr.h" #include "expr/expr_builder.h" #include "expr/expr_manager.h" #include "util/command.h" diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index 692a9cda5..e616b3a65 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -11,10 +11,12 @@ ** commands in SMT-LIB language. **/ -#include "cvc4.h" +#include "smt/smt_engine.h" #include "parser/parser_exception.h" #include "parser/parser_state.h" +#include + // Exported shared data namespace CVC4 { extern ParserState* parserState; diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 08d485882..5969e82d1 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -12,7 +12,7 @@ #ifndef __CVC4__PROP__PROP_ENGINE_H #define __CVC4__PROP__PROP_ENGINE_H -#include "cvc4_expr.h" +#include "expr/expr.h" #include "util/decision_engine.h" #include "theory/theory_engine.h" diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 325999db2..b8fc81961 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -4,4 +4,5 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libsmt.la -libsmt_la_SOURCES = +libsmt_la_SOURCES = \ + smt_engine.cpp diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 078bf9cde..149de058e 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** prover.h +/** cvc4.h ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -9,20 +9,22 @@ ** **/ -#ifndef __CVC4__SMT__SMT_ENGINE_H -#define __CVC4__SMT__SMT_ENGINE_H +#ifndef __CVC4__SMT_ENGINE_H +#define __CVC4__SMT_ENGINE_H #include -#include "core/cvc4_expr.h" -#include "core/result.h" -#include "core/model.h" +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "util/command.h" +#include "util/result.h" +#include "util/model.h" +#include "util/options.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) // PropEngine. namespace CVC4 { -namespace smt { // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass @@ -40,7 +42,12 @@ class SmtEngine { // TODO: make context-aware to handle user-level push/pop. std::vector d_assertList; -private: + /** Our expression manager */ + ExprManager *d_em; + + /** User-level options */ + Options *d_opts; + /** * Pre-process an Expr. This is expected to be highly-variable, * with a lot of "source-level configurability" to add multiple @@ -74,6 +81,16 @@ private: void processAssertionList(); public: + /* + * Construct an SmtEngine with the given expression manager and user options. + */ + SmtEngine(ExprManager* em, Options* opts) : d_em(em), d_opts(opts) {} + + /** + * Execute a command. + */ + void doCommand(Command*); + /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for @@ -110,7 +127,6 @@ public: void pop(); };/* class SmtEngine */ -}/* CVC4::smt namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__SMT__SMT_ENGINE_H */ +#endif /* __CVC4__SMT_ENGINE_H */ diff --git a/src/util/command.h b/src/util/command.h index 804d37717..976e2b3d7 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -12,26 +12,37 @@ #ifndef __CVC4__COMMAND_H #define __CVC4__COMMAND_H +#include "expr/expr.h" + namespace CVC4 { -class Command { - // distinct from Exprs +class SmtEngine; + +class Command { + SmtEngine* d_smt; + +public: + Command(CVC4::SmtEngine* smt) : d_smt(smt) {} + virtual void invoke() = 0; }; class AssertCommand : public Command { public: AssertCommand(const Expr&); + void invoke() { } }; class CheckSatCommand : public Command { public: CheckSatCommand(void); CheckSatCommand(const Expr&); + void invoke() { } }; class QueryCommand : public Command { public: QueryCommand(const Expr&); + void invoke() { } };