# "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever.
my $years = '2009';
+my $standard_template = <<EOF;
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) $years 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.
+EOF
+
+my $public_template = <<EOF;
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) $years 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.
+EOF
+
## end config ##
use strict;
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";
while(my $line = <$IN>) {
last if $line =~ /^ \*\*\s*$/;
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";
return ExprBuilder(*this).xorExpr(right);
}
-Expr Expr::skolemExpr(int i) const {
- return ExprBuilder(*this).skolemExpr(i);
-}
-
-Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
- const std::vector<Expr>& newTerms) const {
- return ExprBuilder(*this).substExpr(oldTerms, newTerms);
-}
-
}/* CVC4 namespace */
** 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 <vector>
#include <stdint.h>
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<Expr>& oldTerms,
- const std::vector<Expr>& newTerms) const;
Expr plusExpr(const Expr& right) const;
Expr uMinusExpr() const;
}/* CVC4 namespace */
-#endif /* __CVC4_EXPR_H */
+#endif /* __CVC4__EXPR_H */
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;
}
}
-void ExprBuilder::collapse() {
+ExprBuilder& ExprBuilder::collapse() {
if(d_nchildren == nchild_thresh) {
vector<Expr>* v = new vector<Expr>();
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 */
void addChild(const Expr&);
void addChild(ExprValue*);
- void collapse();
+ ExprBuilder& collapse();
typedef ExprValue** ev_iterator;
typedef ExprValue const** const_ev_iterator;
ExprBuilder& iffExpr(const Expr& right);
ExprBuilder& impExpr(const Expr& right);
ExprBuilder& xorExpr(const Expr& right);
- ExprBuilder& skolemExpr(int i);
- ExprBuilder& substExpr(const std::vector<Expr>& oldTerms,
- const std::vector<Expr>& newTerms);
- /*
- ExprBuilder& substExpr(const ExprHashMap<Expr>& oldToNew);
- */
/* TODO design: these modify ExprBuilder */
ExprBuilder& operator!() { return notExpr(); }
// For pushing sequences of children
ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); }
+ ExprBuilder& append(Expr child) { return append(&child, &(child)+1); }
template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end);
operator Expr();// not const
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 <class Iterator>
-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 */
#include "expr_builder.h"
#include "expr_manager.h"
-#include "cvc4_expr.h"
+#include "expr/expr.h"
namespace CVC4 {
#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<Expr> 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
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
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<Expr>& oldTerms,
- const std::vector<Expr>& newTerms) const;
Expr plusExpr(const Expr& right) const;
Expr uMinusExpr() const;
#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 {
smt | smtlib SMT-LIB format\n\
";
-enum Language {
- AUTO = 0,
- PL,
- SMTLIB,
-};/* enum Language */
-
enum OptionValue {
SMTCOMP = 256, /* no clash with char options */
STATS
** [[ Add file-specific comments here ]]
**/
+#include <iostream>
+#include <fstream>
#include <cstdio>
#include <cstdlib>
#include <cerrno>
#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[]) {
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");
--- /dev/null
+/********************* -*- 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 */
#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
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
#include <iostream>
#include <sstream>
-#include "cvc4_expr.h"
+#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "util/exception.h"
%{
-#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"
** commands in SMT-LIB language.
**/
-#include "cvc4.h"
+#include "smt/smt_engine.h"
#include "parser/parser_exception.h"
#include "parser/parser_state.h"
+#include <vector>
+
// Exported shared data
namespace CVC4 {
extern ParserState* parserState;
#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"
noinst_LTLIBRARIES = libsmt.la
-libsmt_la_SOURCES =
+libsmt_la_SOURCES = \
+ smt_engine.cpp
/********************* -*- 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
**
**/
-#ifndef __CVC4__SMT__SMT_ENGINE_H
-#define __CVC4__SMT__SMT_ENGINE_H
+#ifndef __CVC4__SMT_ENGINE_H
+#define __CVC4__SMT_ENGINE_H
#include <vector>
-#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
// TODO: make context-aware to handle user-level push/pop.
std::vector<Expr> 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
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
void pop();
};/* class SmtEngine */
-}/* CVC4::smt namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__SMT__SMT_ENGINE_H */
+#endif /* __CVC4__SMT_ENGINE_H */
#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() { }
};
projects / cvc5.git / commitdiff