diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/datatype.cpp | 1 | ||||
-rw-r--r-- | src/util/integer_cln_imp.h | 4 | ||||
-rw-r--r-- | src/util/record.cpp | 40 | ||||
-rw-r--r-- | src/util/record.h | 156 | ||||
-rw-r--r-- | src/util/record.i | 5 | ||||
-rw-r--r-- | src/util/tuple.h | 74 | ||||
-rw-r--r-- | src/util/tuple.i | 5 | ||||
-rw-r--r-- | src/util/util_model.cpp | 10 | ||||
-rw-r--r-- | src/util/util_model.h | 6 |
10 files changed, 299 insertions, 5 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index e72706ea3..804bcde11 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -43,6 +43,9 @@ libutil_la_SOURCES = \ array.h \ datatype.h \ datatype.cpp \ + tuple.h \ + record.h \ + record.cpp \ matcher.h \ gmp_util.h \ sexpr.h \ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index a225339cd..be98e40e1 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -558,6 +558,7 @@ Expr DatatypeConstructor::getConstructor() const { Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + ExprManagerScope ems(d_constructor); const Datatype& dt = Datatype::datatypeOf(d_constructor); CheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric"); DatatypeType dtt = dt.getDatatypeType(); diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index ad21be287..07e85c118 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -59,7 +59,9 @@ private: void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) { try { if(s.find_first_not_of('0') == std::string::npos) { - // string of all zeroes, CLN has a bug for these inputs + // String of all zeroes, CLN has a bug for these inputs up to and + // including CLN v1.3.2. + // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details. d_value = read_integer(flags, "0", NULL, NULL); } else { d_value = read_integer(flags, s.c_str(), NULL, NULL); diff --git a/src/util/record.cpp b/src/util/record.cpp new file mode 100644 index 000000000..f3dc29f81 --- /dev/null +++ b/src/util/record.cpp @@ -0,0 +1,40 @@ +/********************* */ +/*! \file record.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 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.\endverbatim + ** + ** \brief A class representing a record definition + ** + ** A class representing a record definition. + **/ + +#include "util/record.h" + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& os, const Record& r) { + os << "[# "; + bool first = true; + for(Record::iterator i = r.begin(); i != r.end(); ++i) { + if(!first) { + os << ", "; + } + os << (*i).first << ":" << (*i).second; + first = false; + } + os << " #]"; + + return os; +} + +}/* CVC4 namespace */ diff --git a/src/util/record.h b/src/util/record.h new file mode 100644 index 000000000..2c15d30e0 --- /dev/null +++ b/src/util/record.h @@ -0,0 +1,156 @@ +/********************* */ +/*! \file record.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 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.\endverbatim + ** + ** \brief A class representing a Record definition + ** + ** A class representing a Record definition. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__RECORD_H +#define __CVC4__RECORD_H + +#include <iostream> +#include <string> +#include <vector> +#include <utility> +#include "util/hash.h" + +namespace CVC4 { + +class Record; + +// operators for record select and update + +class CVC4_PUBLIC RecordSelect { + std::string d_field; +public: + RecordSelect(const std::string& field) throw() : d_field(field) { } + std::string getField() const throw() { return d_field; } + bool operator==(const RecordSelect& t) const throw() { return d_field == t.d_field; } + bool operator!=(const RecordSelect& t) const throw() { return d_field != t.d_field; } +};/* class RecordSelect */ + +class CVC4_PUBLIC RecordUpdate { + std::string d_field; +public: + RecordUpdate(const std::string& field) throw() : d_field(field) { } + std::string getField() const throw() { return d_field; } + bool operator==(const RecordUpdate& t) const throw() { return d_field == t.d_field; } + bool operator!=(const RecordUpdate& t) const throw() { return d_field != t.d_field; } +};/* class RecordUpdate */ + +struct CVC4_PUBLIC RecordSelectHashFunction { + inline size_t operator()(const RecordSelect& t) const { + return StringHashFunction()(t.getField()); + } +};/* struct RecordSelectHashFunction */ + +struct CVC4_PUBLIC RecordUpdateHashFunction { + inline size_t operator()(const RecordUpdate& t) const { + return StringHashFunction()(t.getField()); + } +};/* struct RecordUpdateHashFunction */ + +std::ostream& operator<<(std::ostream& out, const RecordSelect& t) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC; + +inline std::ostream& operator<<(std::ostream& out, const RecordSelect& t) { + return out << "[" << t.getField() << "]"; +} + +inline std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) { + return out << "[" << t.getField() << "]"; +} + +}/* CVC4 namespace */ + +#include "expr/expr.h" +#include "expr/type.h" + +namespace CVC4 { + +// now an actual record definition + +class CVC4_PUBLIC Record { + std::vector< std::pair<std::string, Type> > d_fields; + +public: + + typedef std::vector< std::pair<std::string, Type> >::const_iterator const_iterator; + typedef const_iterator iterator; + + Record(const std::vector< std::pair<std::string, Type> >& fields) : + d_fields(fields) { + CheckArgument(! fields.empty(), fields, "fields in record description cannot be empty"); + } + + const_iterator find(std::string name) const { + const_iterator i; + for(i = begin(); i != end(); ++i) { + if((*i).first == name) { + break; + } + } + return i; + } + + size_t getIndex(std::string name) const { + const_iterator i = find(name); + CheckArgument(i != end(), name, "requested field `%s' does not exist in record", name.c_str()); + return i - begin(); + } + + size_t getNumFields() const { + return d_fields.size(); + } + + const_iterator begin() const { + return d_fields.begin(); + } + + const_iterator end() const { + return d_fields.end(); + } + + std::pair<std::string, Type> operator[](size_t index) const { + CheckArgument(index < d_fields.size(), index, "index out of bounds for record type"); + return d_fields[index]; + } + + bool operator==(const Record& r) const { + return d_fields == r.d_fields; + } + + bool operator!=(const Record& r) const { + return !(*this == r); + } + +};/* class Record */ + +struct CVC4_PUBLIC RecordHashFunction { + inline size_t operator()(const Record& r) const { + size_t n = 0; + for(Record::iterator i = r.begin(); i != r.end(); ++i) { + n = (n << 3) ^ TypeHashFunction()((*i).second); + } + return n; + } +};/* struct RecordHashFunction */ + +std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__RECORD_H */ diff --git a/src/util/record.i b/src/util/record.i new file mode 100644 index 000000000..f662178c2 --- /dev/null +++ b/src/util/record.i @@ -0,0 +1,5 @@ +%{ +#include "util/record.h" +%} + +%include "util/record.h" diff --git a/src/util/tuple.h b/src/util/tuple.h new file mode 100644 index 000000000..6c1e981a4 --- /dev/null +++ b/src/util/tuple.h @@ -0,0 +1,74 @@ +/********************* */ +/*! \file tuple.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 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.\endverbatim + ** + ** \brief Tuple operators + ** + ** Tuple operators. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__TUPLE_H +#define __CVC4__TUPLE_H + +#include <iostream> +#include <string> +#include <vector> +#include <utility> + +namespace CVC4 { + +class CVC4_PUBLIC TupleSelect { + unsigned d_index; +public: + TupleSelect(unsigned index) throw() : d_index(index) { } + unsigned getIndex() const throw() { return d_index; } + bool operator==(const TupleSelect& t) const throw() { return d_index == t.d_index; } + bool operator!=(const TupleSelect& t) const throw() { return d_index != t.d_index; } +};/* class TupleSelect */ + +class CVC4_PUBLIC TupleUpdate { + unsigned d_index; +public: + TupleUpdate(unsigned index) throw() : d_index(index) { } + unsigned getIndex() const throw() { return d_index; } + bool operator==(const TupleUpdate& t) const throw() { return d_index == t.d_index; } + bool operator!=(const TupleUpdate& t) const throw() { return d_index != t.d_index; } +};/* class TupleUpdate */ + +struct CVC4_PUBLIC TupleSelectHashFunction { + inline size_t operator()(const TupleSelect& t) const { + return t.getIndex(); + } +};/* struct TupleSelectHashFunction */ + +struct CVC4_PUBLIC TupleUpdateHashFunction { + inline size_t operator()(const TupleUpdate& t) const { + return t.getIndex(); + } +};/* struct TupleUpdateHashFunction */ + +std::ostream& operator<<(std::ostream& out, const TupleSelect& t) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) CVC4_PUBLIC; + +inline std::ostream& operator<<(std::ostream& out, const TupleSelect& t) { + return out << "[" << t.getIndex() << "]"; +} + +inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) { + return out << "[" << t.getIndex() << "]"; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__TUPLE_H */ diff --git a/src/util/tuple.i b/src/util/tuple.i new file mode 100644 index 000000000..d7301d201 --- /dev/null +++ b/src/util/tuple.i @@ -0,0 +1,5 @@ +%{ +#include "util/tuple.h" +%} + +%include "util/tuple.h" diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp index bb2924b51..0c058fce9 100644 --- a/src/util/util_model.cpp +++ b/src/util/util_model.cpp @@ -36,11 +36,17 @@ Model::Model() : } size_t Model::getNumCommands() const { - return d_smt.d_modelCommands->size(); + return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); } const Command* Model::getCommand(size_t i) const { - return (*d_smt.d_modelCommands)[i]; + Assert(i < getNumCommands()); + // index the global commands first, then the locals + if(i < d_smt.d_modelGlobalCommands.size()) { + return d_smt.d_modelGlobalCommands[i]; + } else { + return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()]; + } } }/* CVC4 namespace */ diff --git a/src/util/util_model.h b/src/util/util_model.h index 72ff8af60..21c3fb400 100644 --- a/src/util/util_model.h +++ b/src/util/util_model.h @@ -35,8 +35,8 @@ class Model { friend std::ostream& operator<<(std::ostream&, Model&); protected: - /** The SmtEngine we're associated to */ - const SmtEngine& d_smt; + /** The SmtEngine we're associated with */ + SmtEngine& d_smt; /** construct the base class; users cannot do this, only CVC4 internals */ Model(); @@ -48,6 +48,8 @@ public: size_t getNumCommands() const; /** get command */ const Command* getCommand(size_t i) const; + /** get the smt engine that this model is hooked up to */ + SmtEngine* getSmtEngine() { return &d_smt; } public: /** get value for expression */ |