- Modifies expr/emptyset.h to use SetType only as an incomplete type within expr/emptyset.h. This breaks the include cycle between expr/emptyset.h, expr/expr.h and expr/type.h.
- Refactors SExpr to avoid a potentially infinite cycle. This is likely overkill, but it works.
- Moving Expr::setlanguage and related utilities out of the Expr class and into their own file. This allows files in util/ to know the output language set on an ostream.
Expr onePlusTwo = em.mkExpr(kind::PLUS,
em.mkConst(Rational(1)),
em.mkConst(Rational(2)));
- std::cout << Expr::setlanguage(language::output::LANG_CVC4)
+ std::cout << language::SetLanguage(language::output::LANG_CVC4)
<< smt.getInfo("name")
<< " says that 1 + 2 = "
<< smt.simplify(onePlusTwo)
//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
#include "smt/smt_engine.h"
+#include "options/set_language.h"
using namespace std;
using namespace CVC4;
smt.setOption("produce-models", true);
// Set output language to SMTLIB2
- cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
-
+ cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
+
Type integer = em.integerType();
Type set = em.mkSetType(integer);
//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
#include "smt/smt_engine.h"
+#include "options/set_language.h"
using namespace CVC4;
smt.setOption("strings-exp", true);
// Set output language to SMTLIB2
- std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
-
+ std::cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
+
// String type
Type string = em.stringType();
* Author: dejan
*/
-#include <string>
+#include <boost/uuid/sha1.hpp>
#include <fstream>
#include <iostream>
#include <sstream>
+#include <string>
-#include "word.h"
+#include "options/language.h"
+#include "options/set_language.h"
#include "sha1.hpp"
#include "smt_util/command.h"
-
-#include <boost/uuid/sha1.hpp>
+#include "word.h"
using namespace std;
using namespace CVC4;
// The output
ofstream output(argv[3]);
- output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2);
+ output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2);
output << SetBenchmarkLogicCommand("QF_BV") << endl;
output << SetBenchmarkStatusCommand(SMT_UNSATISFIABLE) << endl;
cerr << e << endl;
}
}
-
-
-
* Author: dejan
*/
-#include <string>
+#include <boost/uuid/sha1.hpp>
#include <fstream>
#include <iostream>
#include <sstream>
+#include <string>
-#include "word.h"
+#include "options/language.h"
+#include "options/set_language.h"
#include "sha1.hpp"
#include "smt_util/command.h"
-
-#include <boost/uuid/sha1.hpp>
+#include "word.h"
using namespace std;
using namespace CVC4;
string msg = argv[1];
unsigned msgSize = msg.size();
ofstream output(argv[2]);
- output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2);
+ output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2);
output << SetBenchmarkLogicCommand("QF_BV") << endl;
output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl;
hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[msgSize];
for (unsigned i = 0; i < msgSize; ++ i) {
stringstream ss;
- ss << "x" << i;
+ ss << "x" << i;
cvc4input[i] = hashsmt::cvc4_uchar8(ss.str());
output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl;
cerr << e << endl;
}
}
-
-
-
#include <vector>
#include "expr/expr.h"
+#include "options/language.h"
#include "options/options.h"
+#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/smt_engine.h"
using namespace CVC4::options;
using namespace CVC4::theory;
-int main(int argc, char* argv[])
+int main(int argc, char* argv[])
{
- // Get the filename
+ // Get the filename
string input(argv[1]);
// Create the expression manager
Options options;
options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
ExprManager exprManager(options);
-
- cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << Expr::setdepth(-1);
+
+ cout << language::SetLanguage(language::output::LANG_SMTLIB_V2)
+ << Expr::setdepth(-1);
// Create the parser
ParserBuilder parserBuilder(&exprManager, input, options);
}
cout << *cmd << endl;
- delete cmd;
+ delete cmd;
}
cout << "(check-sat)" << endl;
-
+
// Get rid of the parser
delete parser;
}
-
#include <vector>
#include "expr/expr.h"
+#include "options/language.h"
#include "options/options.h"
+#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt_util/command.h"
using namespace CVC4::parser;
using namespace CVC4::options;
-bool nonsense(char c) { return !isalnum(c); }
+bool nonsense(char c) { return !isalnum(c); }
#ifdef ENABLE_AXIOMS
const bool enableAxioms = true;
Type elementType = t.getElementType();
ostringstream oss_type;
- oss_type << Expr::setlanguage(language::output::LANG_SMTLIB_V2)
+ oss_type << language::SetLanguage(language::output::LANG_SMTLIB_V2)
<< elementType;
string elementTypeAsString = oss_type.str();
elementTypeAsString.erase(
// define-sort
ostringstream oss_name;
- oss_name << Expr::setlanguage(language::output::LANG_SMTLIB_V2)
+ oss_name << language::SetLanguage(language::output::LANG_SMTLIB_V2)
<< "(Set " << elementType << ")";
string name = oss_name.str();
Type newt = em->mkArrayType(t.getElementType(), em->booleanType());
int N = sizeof(setaxioms) / sizeof(setaxioms[0]);
for(int i = 0; i < N; ++i) {
string s = setaxioms[i];
- ostringstream oss; oss << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << elementType;
+ ostringstream oss;
+ oss << language::SetLanguage(language::output::LANG_SMTLIB_V2) << elementType;
boost::replace_all(s, "HOLDA", elementTypeAsString);
boost::replace_all(s, "HOLDB", oss.str());
if( s == "" ) continue;
public:
Mapper(ExprManager* e) : em(e),depth(0) {
- sout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+ sout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
}
void defineSetSort() {
// Create the expression manager
Options options;
options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
- cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+ cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
// cout << Expr::dag(0);
ExprManager exprManager(options);
Mapper m(&exprManager);
-
+
// Create the parser
ParserBuilder parserBuilder(&exprManager, input, options);
if(input == "<stdin>") parserBuilder.withStreamInput(cin);
Parser* parser = parserBuilder.build();
-
+
// Variables and assertions
vector<string> variables;
vector<string> info_tags;
#include "expr/expr.h"
#include "options/language.h"
+#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/smt_engine.h"
toLang = toOutputLanguage(fromLang);
}
- *out << Expr::setlanguage(toLang);
+ *out << language::SetLanguage(toLang);
Options opts;
opts.set(options::inputLanguage, fromLang);
#include "expr/sexpr.h"
#include "options/expr_options.h"
#include "options/parser_options.h"
+#include "options/set_language.h"
#include "options/smt_options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
void ValidityChecker::printExpr(const Expr& e, std::ostream& os) {
Expr::setdepth::Scope sd(os, -1);
Expr::printtypes::Scope pt(os, false);
- Expr::setlanguage::Scope sl(os, d_em->getOptions()[CVC4::options::outputLanguage]);
+ CVC4::language::SetLanguage::Scope sl(os, d_em->getOptions()[CVC4::options::outputLanguage]);
os << e;
}
#include "expr/node.h"
#include "expr/node_manager.h"
#include "expr/type.h"
+#include "options/set_language.h"
using namespace std;
// Unfortunately, in the case of complex selector types, we can
// enter nontrivial recursion here. Make sure that doesn't happen.
stringstream ss;
- ss << Expr::setlanguage(language::output::LANG_CVC4);
+ ss << language::SetLanguage(language::output::LANG_CVC4);
ss.iword(s_printDatatypeNamesOnly) = 1;
t.toStream(ss);
return ss.str();
Debug("datatypes-output") << "printNameOnly is now " << printNameOnly << std::endl;
// can only output datatypes in the CVC4 native language
- Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
+ language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
os << "DATATYPE " << dt.getName();
if(dt.isParametric()) {
std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) {
// can only output datatypes in the CVC4 native language
- Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
+ language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
os << ctor.getName();
std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
// can only output datatypes in the CVC4 native language
- Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
+ language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
os << arg.getName() << ": " << arg.getTypeName();
#include "expr/emptyset.h"
-#include <iostream>
+#include <iosfwd>
+
+#include "expr/expr.h"
+#include "expr/type.h"
namespace CVC4 {
return out << "emptyset(" << asa.getType() << ')';
}
+size_t EmptySetHashFunction::operator()(const EmptySet& es) const {
+ return TypeHashFunction()(es.getType());
+}
+
+/**
+ * Constructs an emptyset of the specified type. Note that the argument
+ * is the type of the set itself, NOT the type of the elements.
+ */
+EmptySet::EmptySet(const SetType& setType)
+ : d_type(new SetType(setType))
+{ }
+
+EmptySet::EmptySet(const EmptySet& es)
+ : d_type(new SetType(es.getType()))
+{ }
+
+EmptySet& EmptySet::operator=(const EmptySet& es) {
+ (*d_type) = es.getType();
+ return *this;
+}
+
+
+EmptySet::~EmptySet() throw() {
+ delete d_type;
+}
+
+const SetType& EmptySet::getType() const {
+ return *d_type;
+}
+
+bool EmptySet::operator==(const EmptySet& es) const throw() {
+ return getType() == es.getType();
+}
+
+bool EmptySet::operator!=(const EmptySet& es) const throw() {
+ return !(*this == es);
+}
+
+bool EmptySet::operator<(const EmptySet& es) const throw() {
+ return getType() < es.getType();
+}
+
+bool EmptySet::operator<=(const EmptySet& es) const throw() {
+ return getType() <= es.getType();
+}
+
+bool EmptySet::operator>(const EmptySet& es) const throw() {
+ return !(*this <= es);
+}
+
+bool EmptySet::operator>=(const EmptySet& es) const throw() {
+ return !(*this < es);
+}
+
+
}/* CVC4 namespace */
#pragma once
+#include <iosfwd>
+
namespace CVC4 {
// messy; Expr needs EmptySet (because it's the payload of a
- // CONSTANT-kinded expression), and EmptySet needs Expr.
- class CVC4_PUBLIC EmptySet;
+ // CONSTANT-kinded expression), EmptySet needs SetType, and
+ // SetType needs Expr. Using a forward declaration here in
+ // order to break the build cycle.
+ // Uses of SetType need to be as an incomplete type throughout
+ // this header.
+ class CVC4_PUBLIC SetType;
}/* CVC4 namespace */
-#include "expr/expr.h"
-#include "expr/type.h"
-#include <iostream>
-
namespace CVC4 {
-
class CVC4_PUBLIC EmptySet {
-
- const SetType d_type;
-
- EmptySet() { }
public:
-
/**
* Constructs an emptyset of the specified type. Note that the argument
* is the type of the set itself, NOT the type of the elements.
*/
- EmptySet(SetType setType):d_type(setType) { }
-
-
- ~EmptySet() throw() {
- }
+ EmptySet(const SetType& setType);
+ ~EmptySet() throw();
+ EmptySet(const EmptySet& other);
+ EmptySet& operator=(const EmptySet& other);
- SetType getType() const { return d_type; }
+ const SetType& getType() const;
+ bool operator==(const EmptySet& es) const throw();
+ bool operator!=(const EmptySet& es) const throw();
+ bool operator<(const EmptySet& es) const throw();
+ bool operator<=(const EmptySet& es) const throw();
+ bool operator>(const EmptySet& es) const throw() ;
+ bool operator>=(const EmptySet& es) const throw();
- bool operator==(const EmptySet& es) const throw() {
- return d_type == es.d_type;
- }
- bool operator!=(const EmptySet& es) const throw() {
- return !(*this == es);
- }
+private:
+ /** Pointer to the SetType node. This is never NULL. */
+ SetType* d_type;
- bool operator<(const EmptySet& es) const throw() {
- return d_type < es.d_type;
- }
- bool operator<=(const EmptySet& es) const throw() {
- return d_type <= es.d_type;
- }
- bool operator>(const EmptySet& es) const throw() {
- return !(*this <= es);
- }
- bool operator>=(const EmptySet& es) const throw() {
- return !(*this < es);
- }
+ EmptySet();
};/* class EmptySet */
std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC;
struct CVC4_PUBLIC EmptySetHashFunction {
- inline size_t operator()(const EmptySet& es) const {
- return TypeHashFunction()(es.getType());
- }
+ size_t operator()(const EmptySet& es) const;
};/* struct EmptySetHashFunction */
}/* CVC4 namespace */
const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
const int ExprDag::s_iosIndex = std::ios_base::xalloc();
-const int ExprSetLanguage::s_iosIndex = std::ios_base::xalloc();
}/* CVC4::expr namespace */
class CVC4_PUBLIC ExprSetDepth;
class CVC4_PUBLIC ExprPrintTypes;
class CVC4_PUBLIC ExprDag;
- class CVC4_PUBLIC ExprSetLanguage;
class ExportPrivate;
}/* CVC4::expr namespace */
*/
typedef expr::ExprDag dag;
- /**
- * IOStream manipulator to set the output language for Exprs.
- */
- typedef expr::ExprSetLanguage setlanguage;
-
/**
* Very basic pretty printer for Expr.
* This is equivalent to calling e.getNode().printAst(...)
};/* class ExprDag::Scope */
};/* class ExprDag */
-
-/**
- * IOStream manipulator to set the output language for Exprs.
- */
-class CVC4_PUBLIC ExprSetLanguage {
- /**
- * The allocated index in ios_base for our depth setting.
- */
- static const int s_iosIndex;
-
- /**
- * The default language to use, for ostreams that haven't yet had a
- * setlanguage() applied to them and where the current Options
- * information isn't available.
- */
- static const int s_defaultOutputLanguage = language::output::LANG_AUTO;
-
- /**
- * When this manipulator is used, the setting is stored here.
- */
- OutputLanguage d_language;
-
-public:
- /**
- * Construct a ExprSetLanguage with the given setting.
- */
- ExprSetLanguage(OutputLanguage l) : d_language(l) {}
-
- inline void applyLanguage(std::ostream& out) {
- // (offset by one to detect whether default has been set yet)
- out.iword(s_iosIndex) = int(d_language) + 1;
- }
-
- static inline OutputLanguage getLanguage(std::ostream& out) {
- long& l = out.iword(s_iosIndex);
- if(l == 0) {
- // set the default language on this ostream
- // (offset by one to detect whether default has been set yet)
- if(not Options::isCurrentNull()) {
- l = options::outputLanguage() + 1;
- }
- if(l <= 0 || l > language::output::LANG_MAX) {
- // if called from outside the library, we may not have options
- // available to us at this point (or perhaps the output language
- // is not set in Options). Default to something reasonable, but
- // don't set "l" since that would make it "sticky" for this
- // stream.
- return OutputLanguage(s_defaultOutputLanguage);
- }
- }
- return OutputLanguage(l - 1);
- }
-
- static inline void setLanguage(std::ostream& out, OutputLanguage l) {
- // (offset by one to detect whether default has been set yet)
- out.iword(s_iosIndex) = int(l) + 1;
- }
-
- /**
- * Set a language on the output stream for the current stack scope.
- * This makes sure the old language is reset on the stream after
- * normal OR exceptional exit from the scope, using the RAII C++
- * idiom.
- */
- class Scope {
- std::ostream& d_out;
- OutputLanguage d_oldLanguage;
-
- public:
-
- inline Scope(std::ostream& out, OutputLanguage language) :
- d_out(out),
- d_oldLanguage(ExprSetLanguage::getLanguage(out)) {
- ExprSetLanguage::setLanguage(out, language);
- }
-
- inline ~Scope() {
- ExprSetLanguage::setLanguage(d_out, d_oldLanguage);
- }
-
- };/* class ExprSetLanguage::Scope */
-
-};/* class ExprSetLanguage */
-
}/* CVC4::expr namespace */
${getConst_instantiations}
return out;
}
-/**
- * Sets the output language when pretty-printing a Expr to an ostream.
- * Use like this:
- *
- * // let out be an ostream, e an Expr
- * out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) {
- l.applyLanguage(out);
- return out;
-}
-
}/* CVC4::expr namespace */
inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
#include "expr/metakind.h"
#include "expr/expr.h"
#include "options/language.h"
+#include "options/set_language.h"
#include "util/configuration.h"
#include "util/utility.h"
#include "util/hash.h"
/**
* IOStream manipulator to set the output language for Exprs.
*/
- typedef expr::ExprSetLanguage setlanguage;
+ typedef language::SetLanguage setlanguage;
/**
* Very basic pretty printer for Node.
#include "base/cvc4_assert.h"
#include "expr/expr.h"
+#include "options/set_language.h"
#include "util/smt2_quote_string.h"
return out;
}
+
+SExpr::~SExpr() {
+ if(d_children != NULL){
+ delete d_children;
+ d_children = NULL;
+ }
+ Assert(d_children == NULL);
+}
+
+SExpr& SExpr::operator=(const SExpr& other) {
+ d_sexprType = other.d_sexprType;
+ d_integerValue = other.d_integerValue;
+ d_rationalValue = other.d_rationalValue;
+ d_stringValue = other.d_stringValue;
+
+ if(d_children == NULL && other.d_children == NULL){
+ // Do nothing.
+ } else if(d_children == NULL){
+ d_children = new SExprVector(*other.d_children);
+ } else if(other.d_children == NULL){
+ delete d_children;
+ d_children = NULL;
+ } else {
+ (*d_children) = other.getChildren();
+ }
+ Assert( isAtom() == other.isAtom() );
+ Assert( (d_children == NULL) == isAtom() );
+ return *this;
+}
+
+SExpr::SExpr() :
+ d_sexprType(SEXPR_STRING),
+ d_integerValue(0),
+ d_rationalValue(0),
+ d_stringValue(""),
+ d_children(NULL) {
+}
+
+
+SExpr::SExpr(const SExpr& other) :
+ d_sexprType(other.d_sexprType),
+ d_integerValue(other.d_integerValue),
+ d_rationalValue(other.d_rationalValue),
+ d_stringValue(other.d_stringValue),
+ d_children(NULL)
+{
+ d_children = (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children);
+ // d_children being NULL is equivalent to the node being an atom.
+ Assert( (d_children == NULL) == isAtom() );
+}
+
+
+SExpr::SExpr(const CVC4::Integer& value) :
+ d_sexprType(SEXPR_INTEGER),
+ d_integerValue(value),
+ d_rationalValue(0),
+ d_stringValue(""),
+ d_children(NULL) {
+ }
+
+SExpr::SExpr(int value) :
+ d_sexprType(SEXPR_INTEGER),
+ d_integerValue(value),
+ d_rationalValue(0),
+ d_stringValue(""),
+ d_children(NULL) {
+}
+
+SExpr::SExpr(long int value) :
+ d_sexprType(SEXPR_INTEGER),
+ d_integerValue(value),
+ d_rationalValue(0),
+ d_stringValue(""),
+ d_children(NULL) {
+}
+
+SExpr::SExpr(unsigned int value) :
+ d_sexprType(SEXPR_INTEGER),
+ d_integerValue(value),
+ d_rationalValue(0),
+ d_stringValue(""),
+ d_children(NULL) {
+}
+
+SExpr::SExpr(unsigned long int value) :
+ d_sexprType(SEXPR_INTEGER),
+ d_integerValue(value),
+ d_rationalValue(0),
+ d_stringValue(""),
+ d_children(NULL) {
+}
+
+SExpr::SExpr(const CVC4::Rational& value) :
+ d_sexprType(SEXPR_RATIONAL),
+ d_integerValue(0),
+ d_rationalValue(value),
+ d_stringValue(""),
+ d_children(NULL) {
+}
+
+SExpr::SExpr(const std::string& value) :
+ d_sexprType(SEXPR_STRING),
+ d_integerValue(0),
+ d_rationalValue(0),
+ d_stringValue(value),
+ d_children(NULL) {
+}
+
+ /**
+ * This constructs a string expression from a const char* value.
+ * This cannot be removed in order to support SExpr("foo").
+ * Given the other constructors this SExpr("foo") converts to bool.
+ * instead of SExpr(string("foo")).
+ */
+SExpr::SExpr(const char* value) :
+ d_sexprType(SEXPR_STRING),
+ d_integerValue(0),
+ d_rationalValue(0),
+ d_stringValue(value),
+ d_children(NULL) {
+}
+
#warning "TODO: Discuss this change with Clark."
SExpr::SExpr(bool value) :
d_sexprType(SEXPR_KEYWORD),
d_integerValue(0),
d_rationalValue(0),
d_stringValue(value ? "true" : "false"),
- d_children() {
+ d_children(NULL) {
+}
+
+SExpr::SExpr(const Keyword& value) :
+ d_sexprType(SEXPR_KEYWORD),
+ d_integerValue(0),
+ d_rationalValue(0),
+ d_stringValue(value.getString()),
+ d_children(NULL) {
+}
+
+SExpr::SExpr(const std::vector<SExpr>& children) :
+ d_sexprType(SEXPR_NOT_ATOM),
+ d_integerValue(0),
+ d_rationalValue(0),
+ d_stringValue(""),
+ d_children(new SExprVector(children)) {
}
std::string SExpr::toString() const {
return ss.str();
}
+/** Is this S-expression an atom? */
+bool SExpr::isAtom() const {
+ return d_sexprType != SEXPR_NOT_ATOM;
+}
+
+/** Is this S-expression an integer? */
+bool SExpr::isInteger() const {
+ return d_sexprType == SEXPR_INTEGER;
+}
+
+/** Is this S-expression a rational? */
+bool SExpr::isRational() const {
+ return d_sexprType == SEXPR_RATIONAL;
+}
+
+/** Is this S-expression a string? */
+bool SExpr::isString() const {
+ return d_sexprType == SEXPR_STRING;
+}
+
+/** Is this S-expression a keyword? */
+bool SExpr::isKeyword() const {
+ return d_sexprType == SEXPR_KEYWORD;
+}
+
+
std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
SExpr::toStream(out, sexpr);
return out;
}
void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() {
- toStream(out, sexpr, Expr::setlanguage::getLanguage(out));
+ toStream(out, sexpr, language::SetLanguage::getLanguage(out));
}
void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() {
const std::vector<SExpr>& SExpr::getChildren() const {
CheckArgument( !isAtom(), this );
- return d_children;
+ Assert( d_children != NULL );
+ return *d_children;
}
bool SExpr::operator==(const SExpr& s) const {
- return d_sexprType == s.d_sexprType &&
- d_integerValue == s.d_integerValue &&
- d_rationalValue == s.d_rationalValue &&
- d_stringValue == s.d_stringValue &&
- d_children == s.d_children;
+ if (d_sexprType == s.d_sexprType &&
+ d_integerValue == s.d_integerValue &&
+ d_rationalValue == s.d_rationalValue &&
+ d_stringValue == s.d_stringValue) {
+ if(d_children == NULL && s.d_children == NULL){
+ return true;
+ } else if(d_children != NULL && s.d_children != NULL){
+ return getChildren() == s.getChildren();
+ }
+ }
+ return false;
}
bool SExpr::operator!=(const SExpr& s) const {
#define __CVC4__SEXPR_H
#include <iomanip>
-#include <sstream>
+#include <iosfwd>
#include <string>
#include <vector>
* string value, or a list of other S-expressions.
*/
class CVC4_PUBLIC SExpr {
-
- enum SExprTypes {
- SEXPR_STRING,
- SEXPR_KEYWORD,
- SEXPR_INTEGER,
- SEXPR_RATIONAL,
- SEXPR_NOT_ATOM
- } d_sexprType;
-
- /** The value of an atomic integer-valued S-expression. */
- CVC4::Integer d_integerValue;
-
- /** The value of an atomic rational-valued S-expression. */
- CVC4::Rational d_rationalValue;
-
- /** The value of an atomic S-expression. */
- std::string d_stringValue;
-
- /** The children of a list S-expression. */
- std::vector<SExpr> d_children;
-
public:
typedef SExprKeyword Keyword;
- SExpr() :
- d_sexprType(SEXPR_STRING),
- d_integerValue(0),
- d_rationalValue(0),
- d_stringValue(""),
- d_children() {
- }
+ SExpr();
+ SExpr(const SExpr&);
+ SExpr& operator=(const SExpr& other);
+ ~SExpr();
- SExpr(const CVC4::Integer& value) :
- d_sexprType(SEXPR_INTEGER),
- d_integerValue(value),
- d_rationalValue(0),
- d_stringValue(""),
- d_children() {
- }
+ SExpr(const CVC4::Integer& value);
- SExpr(int value) :
- d_sexprType(SEXPR_INTEGER),
- d_integerValue(value),
- d_rationalValue(0),
- d_stringValue(""),
- d_children() {
- }
+ SExpr(int value);
+ SExpr(long int value);
+ SExpr(unsigned int value);
+ SExpr(unsigned long int value);
- SExpr(long int value) :
- d_sexprType(SEXPR_INTEGER),
- d_integerValue(value),
- d_rationalValue(0),
- d_stringValue(""),
- d_children() {
- }
+ SExpr(const CVC4::Rational& value);
- SExpr(unsigned int value) :
- d_sexprType(SEXPR_INTEGER),
- d_integerValue(value),
- d_rationalValue(0),
- d_stringValue(""),
- d_children() {
- }
-
- SExpr(unsigned long int value) :
- d_sexprType(SEXPR_INTEGER),
- d_integerValue(value),
- d_rationalValue(0),
- d_stringValue(""),
- d_children() {
- }
-
- SExpr(const CVC4::Rational& value) :
- d_sexprType(SEXPR_RATIONAL),
- d_integerValue(0),
- d_rationalValue(value),
- d_stringValue(""),
- d_children() {
- }
-
- SExpr(const std::string& value) :
- d_sexprType(SEXPR_STRING),
- d_integerValue(0),
- d_rationalValue(0),
- d_stringValue(value),
- d_children() {
- }
+ SExpr(const std::string& value);
/**
* This constructs a string expression from a const char* value.
* Given the other constructors this SExpr("foo") converts to bool.
* instead of SExpr(string("foo")).
*/
- SExpr(const char* value) :
- d_sexprType(SEXPR_STRING),
- d_integerValue(0),
- d_rationalValue(0),
- d_stringValue(value),
- d_children() {
- }
+ SExpr(const char* value);
/**
* This adds a convenience wrapper to SExpr to cast from bools.
* This is internally handled as the strings "true" and "false"
*/
SExpr(bool value);
-
- SExpr(const Keyword& value) :
- d_sexprType(SEXPR_KEYWORD),
- d_integerValue(0),
- d_rationalValue(0),
- d_stringValue(value.getString()),
- d_children() {
- }
-
- SExpr(const std::vector<SExpr>& children) :
- d_sexprType(SEXPR_NOT_ATOM),
- d_integerValue(0),
- d_rationalValue(0),
- d_stringValue(""),
- d_children(children) {
- }
+ SExpr(const Keyword& value);
+ SExpr(const std::vector<SExpr>& children);
/** Is this S-expression an atom? */
- bool isAtom() const {
- return d_sexprType != SEXPR_NOT_ATOM;
- }
+ bool isAtom() const;
/** Is this S-expression an integer? */
- bool isInteger() const {
- return d_sexprType == SEXPR_INTEGER;
- }
+ bool isInteger() const;
/** Is this S-expression a rational? */
- bool isRational() const {
- return d_sexprType == SEXPR_RATIONAL;
- }
+ bool isRational() const;
/** Is this S-expression a string? */
- bool isString() const {
- return d_sexprType == SEXPR_STRING;
- }
+ bool isString() const;
/** Is this S-expression a keyword? */
- bool isKeyword() const {
- return d_sexprType == SEXPR_KEYWORD;
- }
+ bool isKeyword() const;
/**
* This wraps the toStream() printer.
/**
* Outputs the SExpr onto the ostream out. This version reads defaults to the
- * OutputLanguage, Expr::setlanguage::getLanguage(out). The indent level is
+ * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level is
* set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise.
*/
static void toStream(std::ostream& out, const SExpr& sexpr) throw();
/** Returns true if this language quotes Keywords when printing. */
static bool languageQuotesKeywords(OutputLanguage language);
+ enum SExprTypes {
+ SEXPR_STRING,
+ SEXPR_KEYWORD,
+ SEXPR_INTEGER,
+ SEXPR_RATIONAL,
+ SEXPR_NOT_ATOM
+ } d_sexprType;
+
+ /** The value of an atomic integer-valued S-expression. */
+ CVC4::Integer d_integerValue;
+
+ /** The value of an atomic rational-valued S-expression. */
+ CVC4::Rational d_rationalValue;
+
+ /** The value of an atomic S-expression. */
+ std::string d_stringValue;
+
+ typedef std::vector<SExpr> SExprVector;
+
+ /**
+ * The children of a list S-expression.
+ * Whenever the SExpr isAtom() holds, this points at NULL.
+ *
+ * This should be a pointer in case the implementation of vector<SExpr> ever
+ * directly contained or allocated an SExpr. If this happened this would trigger,
+ * either the size being infinite or SExpr() being an infinite loop.
+ */
+ SExprVector* d_children;
};/* class SExpr */
/** Prints an SExpr. */
#include "options/main_options.h"
#include "options/options.h"
#include "options/printer_options.h"
+#include "options/set_language.h"
#include "options/smt_options.h"
#include "smt_util/command.h"
// important even for muzzled builds (to get result output right)
*d_threadOptions[i][options::out]
- << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]);
+ << language::SetLanguage(d_threadOptions[i][options::outputLanguage]);
}
}
}/* CommandExecutorPortfolio::lemmaSharingInit() */
#include "options/main_options.h"
#include "options/options.h"
#include "options/quantifiers_options.h"
+#include "options/set_language.h"
#include "options/smt_options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
}
// important even for muzzled builds (to get result output right)
- *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
+ *opts[options::out] << language::SetLanguage(opts[options::outputLanguage]);
// Create the expression manager using appropriate options
ExprManager* exprMgr;
opts.set(options::replayStream, new Parser::ExprStream(replayParser));
}
if( opts[options::replayLog] != NULL ) {
- *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
+ *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
}
int returnValue = 0;
printer_modes.h \
quantifiers_modes.cpp \
quantifiers_modes.h \
+ set_language.cpp \
+ set_language.h \
simplification_mode.cpp \
simplification_mode.h \
theoryof_mode.cpp \
LANG_Z3STR,
/** The SyGuS input language */
LANG_SYGUS,
-
+
// START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
// THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
--- /dev/null
+/********************* */
+/*! \file language.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Definition of input and output languages
+ **
+ ** Definition of input and output languages.
+ **/
+#include "options/set_language.h"
+
+#include <iosfwd>
+#include <iomanip>
+
+#include "options/language.h"
+#include "options/options.h"
+
+namespace CVC4 {
+namespace language {
+
+const int SetLanguage::s_iosIndex = std::ios_base::xalloc();
+
+SetLanguage::Scope::Scope(std::ostream& out, OutputLanguage language)
+ : d_out(out)
+ , d_oldLanguage(SetLanguage::getLanguage(out))
+{
+ SetLanguage::setLanguage(out, language);
+}
+
+SetLanguage::Scope::~Scope(){
+ SetLanguage::setLanguage(d_out, d_oldLanguage);
+}
+
+
+SetLanguage::SetLanguage(OutputLanguage l)
+ : d_language(l)
+{}
+
+void SetLanguage::applyLanguage(std::ostream& out) {
+ // (offset by one to detect whether default has been set yet)
+ out.iword(s_iosIndex) = int(d_language) + 1;
+}
+
+OutputLanguage SetLanguage::getLanguage(std::ostream& out) {
+ long& l = out.iword(s_iosIndex);
+ if(l == 0) {
+ // set the default language on this ostream
+ // (offset by one to detect whether default has been set yet)
+ if(not Options::isCurrentNull()) {
+ l = options::outputLanguage() + 1;
+ }
+ if(l <= 0 || l > language::output::LANG_MAX) {
+ // if called from outside the library, we may not have options
+ // available to us at this point (or perhaps the output language
+ // is not set in Options). Default to something reasonable, but
+ // don't set "l" since that would make it "sticky" for this
+ // stream.
+ return OutputLanguage(s_defaultOutputLanguage);
+ }
+ }
+ return OutputLanguage(l - 1);
+}
+
+void SetLanguage::setLanguage(std::ostream& out, OutputLanguage l) {
+ // (offset by one to detect whether default has been set yet)
+ out.iword(s_iosIndex) = int(l) + 1;
+}
+
+std::ostream& operator<<(std::ostream& out, SetLanguage l) {
+ l.applyLanguage(out);
+ return out;
+}
+
+}/* CVC4::language namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file language.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Definition of input and output languages
+ **
+ ** Definition of input and output languages.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__OPTIONS__SET_LANGUAGE_H
+#define __CVC4__OPTIONS__SET_LANGUAGE_H
+
+#include <iostream>
+#include "options/language.h"
+
+namespace CVC4 {
+namespace language {
+
+/**
+ * IOStream manipulator to set the output language for Exprs.
+ */
+class CVC4_PUBLIC SetLanguage {
+public:
+ /**
+ * Set a language on the output stream for the current stack scope.
+ * This makes sure the old language is reset on the stream after
+ * normal OR exceptional exit from the scope, using the RAII C++
+ * idiom.
+ */
+ class Scope {
+ public:
+ Scope(std::ostream& out, OutputLanguage language);
+ ~Scope();
+ private:
+ std::ostream& d_out;
+ OutputLanguage d_oldLanguage;
+ };/* class SetLanguage::Scope */
+
+ /**
+ * Construct a ExprSetLanguage with the given setting.
+ */
+ SetLanguage(OutputLanguage l);
+
+ void applyLanguage(std::ostream& out);
+
+ static OutputLanguage getLanguage(std::ostream& out);
+
+ static void setLanguage(std::ostream& out, OutputLanguage l);
+
+private:
+
+ /**
+ * The allocated index in ios_base for our depth setting.
+ */
+ static const int s_iosIndex;
+
+ /**
+ * The default language to use, for ostreams that haven't yet had a
+ * setlanguage() applied to them and where the current Options
+ * information isn't available.
+ */
+ static const int s_defaultOutputLanguage = language::output::LANG_AUTO;
+
+ /**
+ * When this manipulator is used, the setting is stored here.
+ */
+ OutputLanguage d_language;
+};/* class SetLanguage */
+
+
+/**
+ * Sets the output language when pretty-printing a Expr to an ostream.
+ * This is used liek this:
+ *
+ * // let out be an ostream, e an Expr
+ * out << language::SetLanguage(LANG_SMTLIB_V2_5) << e << endl;
+ *
+ * This used to be used like this:
+ *
+ * // let out be an ostream, e an Expr
+ * out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_PUBLIC;
+
+}/* CVC4::language namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OPTIONS__SET_LANGUAGE_H */
Expr e = createPrecedenceTree(parser, em, expressions, operators, 0, expressions.size() - 1);
if(Debug.isOn("prec") && operators.size() > 1) {
- Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
+ language::SetLanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
Debug("prec") << "=> " << e << std::endl;
}
return e;
#include <stdint.h>
#include <cassert>
+#include "options/set_language.h"
#include "parser/antlr_tracing.h"
#include "parser/parser.h"
#include "smt_util/command.h"
<< "with type " << oldType << std::endl;
if(oldType != t) {
std::stringstream ss;
- ss << Expr::setlanguage(language::output::LANG_CVC4)
+ ss << language::SetLanguage(language::output::LANG_CVC4)
<< "incompatible type for `" << *i << "':" << std::endl
<< " old type: " << oldType << std::endl
<< " new type: " << t << std::endl;
std::string name;
}
: identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e]
- { Debug("parser") << Expr::setlanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
+ { Debug("parser") << language::SetLanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
PARSER_STATE->defineVar(name, e);
Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: "
<< name << std::endl
#include "expr/expr.h"
#include "expr/kind.h"
#include "expr/type.h"
+#include "options/set_language.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
#include "parser/smt2/smt2.h"
{ sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
| builtinOp[k]
{ std::stringstream ss;
- ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k);
+ ss << language::SetLanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k);
sexpr = SExpr(ss.str());
}
;
static std::string quoteSymbol(TNode n) {
#warning "check the old implementation. It seems off."
std::stringstream ss;
- ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
+ ss << language::SetLanguage(language::output::LANG_SMTLIB_V2_5);
return CVC4::quoteSymbol(ss.str());
}
#include "options/printer_options.h"
#include "options/prop_options.h"
#include "options/quantifiers_options.h"
+#include "options/set_language.h"
#include "options/smt_options.h"
#include "options/strings_options.h"
#include "options/theory_options.h"
if(!options::outputLanguage.wasSetByUser() &&
options::outputLanguage() == language::output::LANG_SMTLIB_V2_5) {
options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0);
- *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_0);
+ *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0);
}
return;
} else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
if(!options::outputLanguage.wasSetByUser() &&
options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5);
- *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
+ *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5);
}
return;
}
}
stringstream ss;
- ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream()))
+ ss << language::SetLanguage(language::SetLanguage::getLanguage(Dump.getStream()))
<< func;
DefineFunctionCommand c(ss.str(), func, formals, formula);
addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
#include "options/parser_options.h"
#include "options/printer_modes.h"
#include "options/quantifiers_modes.h"
+#include "options/set_language.h"
#include "options/simplification_mode.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
int dagSetting = expr::ExprDag::getDag(__channel_get); \
size_t exprDepthSetting = expr::ExprSetDepth::getDepth(__channel_get); \
bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \
- OutputLanguage languageSetting = expr::ExprSetLanguage::getLanguage(__channel_get); \
+ OutputLanguage languageSetting = language::SetLanguage::getLanguage(__channel_get); \
__channel_set; \
__channel_get << Expr::dag(dagSetting); \
__channel_get << Expr::setdepth(exprDepthSetting); \
__channel_get << Expr::printtypes(printtypesSetting); \
- __channel_get << Expr::setlanguage(languageSetting); \
+ __channel_get << language::SetLanguage(languageSetting); \
}
void SmtOptionsHandler::dumpToFile(std::string option, std::string optarg) {
}else{
if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
std::stringstream ss;
- ss << Expr::setlanguage(options::outputLanguage());
+ ss << language::SetLanguage(options::outputLanguage());
ss << "e_" << tn;
mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
#include <string>
#include "expr/expr.h"
+#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt_util/command.h"
psr->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
Expr e = psr->nextExpression();
stringstream ss;
- ss << Expr::setlanguage(outlang) << Expr::setdepth(-1) << e;
+ ss << language::SetLanguage(outlang) << Expr::setdepth(-1) << e;
assert(psr->nextExpression().isNull());// next expr should be null
assert(psr->done());// parser should be done
string s = ss.str();
#include <sstream>
#include "expr/expr_manager.h"
+#include "options/set_language.h"
#include "options/smt_options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2);
- cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+ cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
ExprManager em(opts);
SmtEngine smt(&em);
#include "expr/node.h"
#include "expr/node_manager.h"
#include "options/language.h"
+#include "options/set_language.h"
#include "smt_util/boolean_simplification.h"
using namespace CVC4;
BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD);
cout << Expr::setdepth(-1)
- << Expr::setlanguage(language::output::LANG_CVC4);
+ << language::SetLanguage(language::output::LANG_CVC4);
}
void tearDown() {
projects / cvc5.git / commitdiff