summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am13
-rw-r--r--src/util/bitvector.h14
-rw-r--r--src/util/boolean_simplification.h2
-rw-r--r--src/util/chain.h50
-rw-r--r--src/util/chain.i12
-rw-r--r--src/util/cvc4_assert.cpp2
-rw-r--r--src/util/cvc4_assert.h14
-rw-r--r--src/util/datatype.h1
-rw-r--r--src/util/debug.h4
-rw-r--r--src/util/divisible.cpp29
-rw-r--r--src/util/divisible.h62
-rw-r--r--src/util/divisible.i10
-rw-r--r--src/util/dump.h1
-rw-r--r--src/util/exception.h8
-rw-r--r--src/util/ite_removal.cpp6
-rw-r--r--src/util/output.h2
-rw-r--r--src/util/output.i70
-rw-r--r--src/util/rational_cln_imp.h4
-rw-r--r--src/util/record.h1
-rw-r--r--src/util/recursion_breaker.h2
-rw-r--r--src/util/regexp.h353
-rw-r--r--src/util/result.cpp21
-rw-r--r--src/util/result.h33
-rw-r--r--src/util/result.i3
-rw-r--r--src/util/sort_inference.cpp308
-rw-r--r--src/util/sort_inference.h46
-rw-r--r--src/util/statistics_registry.h2
-rw-r--r--src/util/util_model.cpp2
-rw-r--r--src/util/util_model.h12
29 files changed, 895 insertions, 192 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 4f93f5a61..156288600 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -39,9 +39,11 @@ libutil_la_SOURCES = \
datatype.h \
datatype.cpp \
tuple.h \
- maybe.h \
record.h \
record.cpp \
+ divisible.h \
+ divisible.cpp \
+ maybe.h \
matcher.h \
gmp_util.h \
sexpr.h \
@@ -75,6 +77,7 @@ libutil_la_SOURCES = \
ite_removal.h \
ite_removal.cpp \
node_visitor.h \
+ chain.h \
index.h \
uninterpreted_constant.h \
uninterpreted_constant.cpp \
@@ -85,7 +88,8 @@ libutil_la_SOURCES = \
util_model.h \
util_model.cpp \
sort_inference.h \
- sort_inference.cpp
+ sort_inference.cpp \
+ regexp.h
libstatistics_la_SOURCES = \
statistics_registry.h \
@@ -122,7 +126,7 @@ EXTRA_DIST = \
datatype.i \
tuple.i \
record.i \
- output.i \
+ divisible.i \
cardinality.i \
result.i \
configuration.i \
@@ -136,7 +140,8 @@ EXTRA_DIST = \
rational.i \
hash.i \
predicate.i \
- uninterpreted_constant.i
+ uninterpreted_constant.i \
+ chain.i
DISTCLEANFILES = \
integer.h.tmp \
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 2d5d29339..04e23217b 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -396,7 +396,7 @@ struct CVC4_PUBLIC BitVectorHashFunction {
/**
* The structure representing the extraction operation for bit-vectors. The
- * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
+ * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
* by taking the bits at indices <code>high ... low</code>
*/
struct CVC4_PUBLIC BitVectorExtract {
@@ -492,6 +492,13 @@ struct CVC4_PUBLIC BitVectorRotateRight {
operator unsigned () const { return rotateRightAmount; }
};/* struct BitVectorRotateRight */
+struct CVC4_PUBLIC IntToBitVector {
+ unsigned size;
+ IntToBitVector(unsigned size)
+ : size(size) {}
+ operator unsigned () const { return size; }
+};/* struct IntToBitVector */
+
template <typename T>
struct CVC4_PUBLIC UnsignedHashFunction {
inline size_t operator()(const T& x) const {
@@ -514,6 +521,11 @@ inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
return os << "[" << bv.bitIndex << "]";
}
+inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) CVC4_PUBLIC;
+inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) {
+ return os << "[" << bv.size << "]";
+}
+
}/* CVC4 namespace */
#endif /* __CVC4__BITVECTOR_H */
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
index e5c4ead6c..be39f69c1 100644
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -22,6 +22,7 @@
#include <vector>
#include <algorithm>
+#include "expr/expr_manager_scope.h"
#include "expr/node.h"
#include "util/cvc4_assert.h"
@@ -202,6 +203,7 @@ public:
* @param e the Expr to negate (cannot be the null Expr)
*/
static Expr negate(Expr e) throw(AssertionException) {
+ ExprManagerScope ems(e);
return negate(Node::fromExpr(e)).toExpr();
}
diff --git a/src/util/chain.h b/src/util/chain.h
new file mode 100644
index 000000000..2e9cf7bf6
--- /dev/null
+++ b/src/util/chain.h
@@ -0,0 +1,50 @@
+/********************* */
+/*! \file chain.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CHAIN_H
+#define __CVC4__CHAIN_H
+
+#include "expr/kind.h"
+#include <iostream>
+
+namespace CVC4 {
+
+/** A class to represent a chained, built-in operator. */
+class Chain {
+ Kind d_kind;
+public:
+ explicit Chain(Kind k) : d_kind(k) { }
+ bool operator==(const Chain& ch) const { return d_kind == ch.d_kind; }
+ bool operator!=(const Chain& ch) const { return d_kind != ch.d_kind; }
+ Kind getOperator() const { return d_kind; }
+};/* class Chain */
+
+inline std::ostream& operator<<(std::ostream& out, const Chain& ch) {
+ return out << ch.getOperator();
+}
+
+struct ChainHashFunction {
+ size_t operator()(const Chain& ch) const {
+ return kind::KindHashFunction()(ch.getOperator());
+ }
+};/* struct ChainHashFunction */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CHAIN_H */
diff --git a/src/util/chain.i b/src/util/chain.i
new file mode 100644
index 000000000..1c97a527f
--- /dev/null
+++ b/src/util/chain.i
@@ -0,0 +1,12 @@
+%{
+#include "util/chain.h"
+%}
+
+%rename(equals) CVC4::Chain::operator==(const Chain&) const;
+%ignore CVC4::Chain::operator!=(const Chain&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Chain&);
+
+%rename(apply) CVC4::ChainHashFunction::operator()(const CVC4::Chain&) const;
+
+%include "util/chain.h"
diff --git a/src/util/cvc4_assert.cpp b/src/util/cvc4_assert.cpp
index eb7b81a39..08e2867f6 100644
--- a/src/util/cvc4_assert.cpp
+++ b/src/util/cvc4_assert.cpp
@@ -136,7 +136,7 @@ void debugAssertionFailed(const AssertionException& thisException,
const char* propagatingException) {
static CVC4_THREADLOCAL(bool) alreadyFired = false;
- if(EXPECT_TRUE( !std::uncaught_exception() ) || alreadyFired) {
+ if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) {
throw thisException;
}
diff --git a/src/util/cvc4_assert.h b/src/util/cvc4_assert.h
index c070fc389..7d359a56b 100644
--- a/src/util/cvc4_assert.h
+++ b/src/util/cvc4_assert.h
@@ -252,7 +252,7 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
// details of the exception
# define AlwaysAssert(cond, msg...) \
do { \
- if(EXPECT_FALSE( ! (cond) )) { \
+ if(__builtin_expect( ( ! (cond) ), false )) { \
/* save the last assertion failure */ \
const char* lastException = ::CVC4::s_debugLastException; \
::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
@@ -265,7 +265,7 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
// will terminate() if thrown during stack unwinding.
# define AlwaysAssert(cond, msg...) \
do { \
- if(EXPECT_FALSE( ! (cond) )) { \
+ if(__builtin_expect( ( ! (cond) ), false )) { \
throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
} \
} while(0)
@@ -283,13 +283,13 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg)
#define CheckArgument(cond, arg, msg...) \
do { \
- if(EXPECT_FALSE( ! (cond) )) { \
+ if(__builtin_expect( ( ! (cond) ), false )) { \
throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \
} \
} while(0)
#define AlwaysAssertArgument(cond, arg, msg...) \
do { \
- if(EXPECT_FALSE( ! (cond) )) { \
+ if(__builtin_expect( ( ! (cond) ), false )) { \
throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
} \
} while(0)
@@ -299,9 +299,9 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
# define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
# define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg)
#else /* ! CVC4_ASSERTIONS */
-# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
-# define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
-# define DebugCheckArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
+# define Assert(cond, msg...) /*__builtin_expect( ( cond ), true )*/
+# define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/
+# define DebugCheckArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/
#endif /* CVC4_ASSERTIONS */
}/* CVC4 namespace */
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 3da441f1f..c46c10c97 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -33,7 +33,6 @@ namespace CVC4 {
#include "expr/expr.h"
#include "expr/type.h"
-#include "util/output.h"
#include "util/hash.h"
#include "util/exception.h"
diff --git a/src/util/debug.h b/src/util/debug.h
index 3e7c4d8be..97c176f02 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -27,11 +27,11 @@
#ifdef CVC4_ASSERTIONS
// the __builtin_expect() helps us if assert is built-in or a macro
-# define cvc4assert(x) assert(EXPECT_TRUE( x ))
+# define cvc4assert(x) assert(__builtin_expect( ( x ), true ))
#else
// TODO: use a compiler annotation when assertions are off ?
// (to improve optimization)
-# define cvc4assert(x) /*EXPECT_TRUE( x )*/
+# define cvc4assert(x) /*__builtin_expect( ( x ), true )*/
#endif /* CVC4_ASSERTIONS */
#endif /* __CVC4__DEBUG_H */
diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp
new file mode 100644
index 000000000..4e20d6b5f
--- /dev/null
+++ b/src/util/divisible.cpp
@@ -0,0 +1,29 @@
+/********************* */
+/*! \file divisible.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "util/divisible.h"
+#include "util/exception.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+Divisible::Divisible(const Integer& n) : k(n) {
+ CheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N");
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/divisible.h b/src/util/divisible.h
new file mode 100644
index 000000000..0c0c7bc5b
--- /dev/null
+++ b/src/util/divisible.h
@@ -0,0 +1,62 @@
+/********************* */
+/*! \file divisible.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__DIVISIBLE_H
+#define __CVC4__DIVISIBLE_H
+
+#include <iostream>
+#include "util/integer.h"
+#include "util/exception.h"
+
+namespace CVC4 {
+
+/**
+ * The structure representing the divisibility-by-k predicate.
+ */
+struct CVC4_PUBLIC Divisible {
+ const Integer k;
+
+ Divisible(const Integer& n);
+
+ bool operator==(const Divisible& d) const {
+ return k == d.k;
+ }
+
+ bool operator!=(const Divisible& d) const {
+ return !(*this == d);
+ }
+};/* struct Divisible */
+
+/**
+ * Hash function for the Divisible objects.
+ */
+struct CVC4_PUBLIC DivisibleHashFunction {
+ size_t operator()(const Divisible& d) const {
+ return d.k.hash();
+ }
+};/* struct DivisibleHashFunction */
+
+inline std::ostream& operator <<(std::ostream& os, const Divisible& d) CVC4_PUBLIC;
+inline std::ostream& operator <<(std::ostream& os, const Divisible& d) {
+ return os << "divisible-by-" << d.k;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DIVISIBLE_H */
diff --git a/src/util/divisible.i b/src/util/divisible.i
new file mode 100644
index 000000000..7599360ca
--- /dev/null
+++ b/src/util/divisible.i
@@ -0,0 +1,10 @@
+%{
+#include "util/divisible.h"
+%}
+
+%rename(equals) CVC4::Divisible::operator==(const Divisible&) const;
+%ignore CVC4::Divisible::operator!=(const Divisible&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Divisible&);
+
+%include "util/divisible.h"
diff --git a/src/util/dump.h b/src/util/dump.h
index 2ef6010e3..0bde68d76 100644
--- a/src/util/dump.h
+++ b/src/util/dump.h
@@ -19,7 +19,6 @@
#ifndef __CVC4__DUMP_H
#define __CVC4__DUMP_H
-#include "util/output.h"
#include "expr/command.h"
namespace CVC4 {
diff --git a/src/util/exception.h b/src/util/exception.h
index 082a50ef2..cd4b763ef 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -138,13 +138,13 @@ namespace CVC4 {
#ifndef CheckArgument
template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) {
- if(EXPECT_FALSE( !cond )) { \
+ if(__builtin_expect( ( !cond ), false )) { \
throw ::CVC4::IllegalArgumentException("", "", ""); \
} \
}
template <class T> inline void CheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
template <class T> inline void CheckArgument(bool cond, const T& arg) {
- if(EXPECT_FALSE( !cond )) { \
+ if(__builtin_expect( ( !cond ), false )) { \
throw ::CVC4::IllegalArgumentException("", "", ""); \
} \
}
@@ -153,13 +153,13 @@ template <class T> inline void CheckArgument(bool cond, const T& arg) {
#ifndef DebugCheckArgument
template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) {
- if(EXPECT_FALSE( !cond )) { \
+ if(__builtin_expect( ( !cond ), false )) { \
throw ::CVC4::IllegalArgumentException("", "", ""); \
} \
}
template <class T> inline void DebugCheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
template <class T> inline void DebugCheckArgument(bool cond, const T& arg) {
- if(EXPECT_FALSE( !cond )) { \
+ if(__builtin_expect( ( !cond ), false )) { \
throw ::CVC4::IllegalArgumentException("", "", ""); \
} \
}
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index f26bbe0aa..7d4948251 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -30,7 +30,11 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
{
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
std::vector<Node> quantVar;
- output[i] = run(output[i], output, iteSkolemMap, quantVar);
+ // Do this in two steps to avoid Node problems(?)
+ // Appears related to bug 512, splitting this into two lines
+ // fixes the bug on clang on Mac OS
+ Node itesRemoved = run(output[i], output, iteSkolemMap, quantVar);
+ output[i] = itesRemoved;
}
}
diff --git a/src/util/output.h b/src/util/output.h
index 263d5a144..7394f24ab 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -14,7 +14,7 @@
** Output utility classes and functions.
**/
-#include "cvc4_public.h"
+#include "cvc4_private_library.h"
#ifndef __CVC4__OUTPUT_H
#define __CVC4__OUTPUT_H
diff --git a/src/util/output.i b/src/util/output.i
deleted file mode 100644
index 74953ba53..000000000
--- a/src/util/output.i
+++ /dev/null
@@ -1,70 +0,0 @@
-%{
-#include "util/output.h"
-%}
-
-%ignore CVC4::null_streambuf;
-%ignore std::streambuf;
-%feature("valuewrapper") std::ostream;
-
-// There are issues with SWIG's attempted wrapping of these variables when
-// it tries to generate the getters and setters. For now, just ignore them.
-%ignore CVC4::null_sb;
-%ignore CVC4::null_os;
-%ignore CVC4::DumpOutC::dump_cout;
-%ignore CVC4::CVC4ostream;
-
-%ignore operator<<;
-%ignore on(std::string);
-%ignore isOn(std::string);
-%ignore off(std::string);
-%ignore printf(std::string, const char*, ...);
-
-%ignore CVC4::IndentedScope;
-%ignore CVC4::push(CVC4ostream&);
-%ignore CVC4::pop(CVC4ostream&);
-
-%ignore CVC4::ScopedDebug::ScopedDebug(std::string);
-%ignore CVC4::ScopedDebug::ScopedDebug(std::string, bool);
-
-%ignore CVC4::ScopedTrace::ScopedTrace(std::string);
-%ignore CVC4::ScopedTrace::ScopedTrace(std::string, bool);
-
-%ignore CVC4::WarningC::WarningC(std::ostream*);
-%ignore CVC4::MessageC::MessageC(std::ostream*);
-%ignore CVC4::NoticeC::NoticeC(std::ostream*);
-%ignore CVC4::ChatC::ChatC(std::ostream*);
-%ignore CVC4::TraceC::TraceC(std::ostream*);
-%ignore CVC4::DebugC::DebugC(std::ostream*);
-%ignore CVC4::DumpOutC::DumpOutC(std::ostream*);
-
-%ignore CVC4::WarningC::operator();
-%ignore CVC4::MessageC::operator();
-%ignore CVC4::NoticeC::operator();
-%ignore CVC4::ChatC::operator();
-%ignore CVC4::TraceC::operator();
-%ignore CVC4::DebugC::operator();
-%ignore CVC4::DumpOutC::operator();
-
-%ignore CVC4::WarningC::getStream();
-%ignore CVC4::MessageC::getStream();
-%ignore CVC4::NoticeC::getStream();
-%ignore CVC4::ChatC::getStream();
-%ignore CVC4::TraceC::getStream();
-%ignore CVC4::DebugC::getStream();
-%ignore CVC4::DumpOutC::getStream();
-
-%ignore CVC4::WarningC::setStream(std::ostream&);
-%ignore CVC4::MessageC::setStream(std::ostream&);
-%ignore CVC4::NoticeC::setStream(std::ostream&);
-%ignore CVC4::ChatC::setStream(std::ostream&);
-%ignore CVC4::TraceC::setStream(std::ostream&);
-%ignore CVC4::DebugC::setStream(std::ostream&);
-%ignore CVC4::DumpOutC::setStream(std::ostream&);
-
-%ignore operator std::ostream&;
-%ignore operator CVC4ostream;
-
-%rename(get) operator ();
-%rename(ok) operator bool;
-
-%include "util/output.h"
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 1e27fa859..da2af6c1f 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -155,10 +155,10 @@ public:
#ifdef CVC4_NEED_INT64_T_OVERLOADS
Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) {
- d_value /= static_cast<long>(d);
+ d_value /= cln::cl_I(d);
}
Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) {
- d_value /= static_cast<unsigned long>(d);
+ d_value /= cln::cl_I(d);
}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
diff --git a/src/util/record.h b/src/util/record.h
index 3d6481320..63c54930e 100644
--- a/src/util/record.h
+++ b/src/util/record.h
@@ -91,7 +91,6 @@ public:
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 {
diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h
index 07bf10984..a4177f600 100644
--- a/src/util/recursion_breaker.h
+++ b/src/util/recursion_breaker.h
@@ -86,7 +86,7 @@ class RecursionBreaker {
static CVC4_THREADLOCAL(Map*) s_maps;
std::string d_tag;
- const T& d_item;
+ const T d_item;
bool d_firstToTag;
bool d_recursion;
diff --git a/src/util/regexp.h b/src/util/regexp.h
new file mode 100644
index 000000000..58f58a40f
--- /dev/null
+++ b/src/util/regexp.h
@@ -0,0 +1,353 @@
+/********************* */
+/*! \file regexp.h
+ ** \verbatim
+ ** Original author: Tianyi Liang
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__REGEXP_H
+#define __CVC4__REGEXP_H
+
+#include <iostream>
+#include <string>
+//#include "util/exception.h"
+//#include "util/integer.h"
+#include "util/hash.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC Char {
+
+private:
+ unsigned int d_char;
+
+public:
+ Char() {}
+
+ Char(const unsigned int c)
+ : d_char(c) {}
+
+ ~Char() {}
+
+ Char& operator =(const Char& y) {
+ if(this != &y) d_char = y.d_char;
+ return *this;
+ }
+
+ bool operator ==(const Char& y) const {
+ return d_char == y.d_char ;
+ }
+
+ bool operator !=(const Char& y) const {
+ return d_char != y.d_char ;
+ }
+
+ bool operator <(const Char& y) const {
+ return d_char < y.d_char;
+ }
+
+ bool operator >(const Char& y) const {
+ return d_char > y.d_char ;
+ }
+
+ bool operator <=(const Char& y) const {
+ return d_char <= y.d_char;
+ }
+
+ bool operator >=(const Char& y) const {
+ return d_char >= y.d_char ;
+ }
+
+ /*
+ * Convenience functions
+ */
+ std::string toString() const {
+ std::string str = "1";
+ str[0] = (char) d_char;
+ return str;
+ }
+
+ unsigned size() const {
+ return 1;
+ }
+
+ const char* c_str() const {
+ return toString().c_str();
+ }
+};/* class Char */
+
+namespace strings {
+
+struct CharHashFunction {
+ size_t operator()(const ::CVC4::Char& c) const {
+ return __gnu_cxx::hash<const char*>()(c.toString().c_str());
+ }
+};/* struct CharHashFunction */
+
+}
+
+inline std::ostream& operator <<(std::ostream& os, const Char& c) CVC4_PUBLIC;
+inline std::ostream& operator <<(std::ostream& os, const Char& c) {
+ return os << "\"" << c.toString() << "\"";
+}
+
+class CVC4_PUBLIC String {
+
+private:
+ std::vector<unsigned int> d_str;
+
+ bool isVecSame(const std::vector<unsigned int> &a, const std::vector<unsigned int> &b) const {
+ if(a.size() != b.size()) return false;
+ else {
+ for(unsigned int i=0; i<a.size(); ++i)
+ if(a[i] != b[i]) return false;
+ return true;
+ }
+ }
+
+public:
+ String() {}
+
+ String(const std::string &s) {
+ for(unsigned int i=0; i<s.size(); ++i) {
+ d_str.push_back( convertCharToUnsignedInt(s[i]) );
+ }
+ }
+
+ String(const char* s) {
+ for(unsigned int i=0,len=strlen(s); i<len; ++i) {
+ d_str.push_back( convertCharToUnsignedInt(s[i]) );
+ }
+ }
+
+ String(const std::vector<unsigned int> &s) : d_str(s) { }
+
+ ~String() {}
+
+ String& operator =(const String& y) {
+ if(this != &y) d_str = y.d_str;
+ return *this;
+ }
+
+ bool operator ==(const String& y) const {
+ return isVecSame(d_str, y.d_str);
+ }
+
+ bool operator !=(const String& y) const {
+ return ! ( isVecSame(d_str, y.d_str) );
+ }
+
+ String concat (const String& other) const {
+ std::vector<unsigned int> ret_vec(d_str);
+ ret_vec.insert( ret_vec.end(), other.d_str.begin(), other.d_str.end() );
+ return String(ret_vec);
+ }
+
+ bool operator <(const String& y) const {
+ if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
+ else {
+ for(unsigned int i=0; i<d_str.size(); ++i)
+ if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
+
+ return false;
+ }
+ }
+
+ bool operator >(const String& y) const {
+ if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
+ else {
+ for(unsigned int i=0; i<d_str.size(); ++i)
+ if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
+
+ return false;
+ }
+ }
+
+ bool operator <=(const String& y) const {
+ if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
+ else {
+ for(unsigned int i=0; i<d_str.size(); ++i)
+ if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
+
+ return true;
+ }
+ }
+
+ bool operator >=(const String& y) const {
+ if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
+ else {
+ for(unsigned int i=0; i<d_str.size(); ++i)
+ if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
+
+ return true;
+ }
+ }
+
+ bool strncmp(const String &y, unsigned int n) const {
+ for(unsigned int i=0; i<n; ++i)
+ if(d_str[i] != y.d_str[i]) return false;
+ return true;
+ }
+
+ /*
+ * Convenience functions
+ */
+ std::string toString() const {
+ std::string str;
+ for(unsigned int i=0; i<d_str.size(); ++i) {
+ str += convertUnsignedIntToChar( d_str[i] );
+ //TODO isPrintable: ( "\\" + (convertUnsignedIntToChar( d_str[i] ) );
+ }
+ return str;
+ }
+
+ unsigned size() const {
+ return d_str.size();
+ }
+
+ String substr(unsigned i) const {
+ std::vector<unsigned int> ret_vec;
+ std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
+ //for(unsigned k=0; k<i; k++) ++itr;
+ ret_vec.insert(ret_vec.end(), itr, d_str.end());
+ return String(ret_vec);
+ }
+ String substr(unsigned i, unsigned j) const {
+ std::vector<unsigned int> ret_vec;
+ std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
+ //for(unsigned k=0; k<i; k++) ++itr;
+ //std::vector<unsigned int>::const_iterator itr2 = itr;
+ //for(unsigned k=0; k<j; k++) ++itr2;
+ ret_vec.insert( ret_vec.end(), itr, itr + j );
+ return String(ret_vec);
+ }
+
+public:
+ static unsigned int convertCharToUnsignedInt( char c ) {
+ int i = (int)c;
+ i = i-65;
+ return (unsigned int)(i<0 ? i+256 : i);
+ }
+ static char convertUnsignedIntToChar( unsigned int i ){
+ int ii = i+65;
+ return (char)(ii>=256 ? ii-256 : ii);
+ }
+ static bool isPrintable( unsigned int i ){
+ char c = convertUnsignedIntToChar( i );
+ return isprint( (int)c );
+ }
+
+};/* class String */
+
+namespace strings {
+
+struct StringHashFunction {
+ size_t operator()(const ::CVC4::String& s) const {
+ return __gnu_cxx::hash<const char*>()(s.toString().c_str());
+ }
+};/* struct StringHashFunction */
+
+}
+
+inline std::ostream& operator <<(std::ostream& os, const String& s) CVC4_PUBLIC;
+inline std::ostream& operator <<(std::ostream& os, const String& s) {
+ return os << "\"" << s.toString() << "\"";
+}
+
+class CVC4_PUBLIC RegExp {
+
+private:
+ std::string d_str;
+
+public:
+ RegExp() {}
+
+ RegExp(const std::string s)
+ : d_str(s) {}
+
+ ~RegExp() {}
+
+ RegExp& operator =(const RegExp& y) {
+ if(this != &y) d_str = y.d_str;
+ return *this;
+ }
+
+ bool operator ==(const RegExp& y) const {
+ return d_str == y.d_str ;
+ }
+
+ bool operator !=(const RegExp& y) const {
+ return d_str != y.d_str ;
+ }
+
+ String concat (const RegExp& other) const {
+ return String(d_str + other.d_str);
+ }
+
+ bool operator <(const RegExp& y) const {
+ return d_str < y.d_str;
+ }
+
+ bool operator >(const RegExp& y) const {
+ return d_str > y.d_str ;
+ }
+
+ bool operator <=(const RegExp& y) const {
+ return d_str <= y.d_str;
+ }
+
+ bool operator >=(const RegExp& y) const {
+ return d_str >= y.d_str ;
+ }
+
+ /*
+ * Convenience functions
+ */
+
+ size_t hash() const {
+ unsigned int h = 1;
+
+ for (size_t i = 0; i < d_str.length(); ++i) {
+ h = (h << 5) + d_str[i];
+ }
+
+ return h;
+ }
+
+ std::string toString() const {
+ return d_str;
+ }
+
+ unsigned size() const {
+ return d_str.size();
+ }
+};/* class String */
+
+/**
+ * Hash function for the RegExp constants.
+ */
+struct CVC4_PUBLIC RegExpHashFunction {
+ inline size_t operator()(const RegExp& s) const {
+ return s.hash();
+ }
+};/* struct RegExpHashFunction */
+
+inline std::ostream& operator <<(std::ostream& os, const RegExp& s) CVC4_PUBLIC;
+inline std::ostream& operator <<(std::ostream& os, const RegExp& s) {
+ return os << s.toString();
+}
+}/* CVC4 namespace */
+
+#endif /* __CVC4__STRING_H */
diff --git a/src/util/result.cpp b/src/util/result.cpp
index e0e34f07d..909a7d8c6 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -27,11 +27,12 @@ using namespace std;
namespace CVC4 {
-Result::Result(const std::string& instr) :
+Result::Result(const std::string& instr, std::string inputName) :
d_sat(SAT_UNKNOWN),
d_validity(VALIDITY_UNKNOWN),
d_which(TYPE_NONE),
- d_unknownExplanation(UNKNOWN_REASON) {
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
string s = instr;
transform(s.begin(), s.end(), s.begin(), ::tolower);
if(s == "sat" || s == "satisfiable") {
@@ -115,13 +116,13 @@ Result Result::asSatisfiabilityResult() const throw() {
switch(d_validity) {
case INVALID:
- return Result(SAT);
+ return Result(SAT, d_inputName);
case VALID:
- return Result(UNSAT);
+ return Result(UNSAT, d_inputName);
case VALIDITY_UNKNOWN:
- return Result(SAT_UNKNOWN, d_unknownExplanation);
+ return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
default:
Unhandled(d_validity);
@@ -129,7 +130,7 @@ Result Result::asSatisfiabilityResult() const throw() {
}
// TYPE_NONE
- return Result(SAT_UNKNOWN, NO_STATUS);
+ return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
}
Result Result::asValidityResult() const throw() {
@@ -141,13 +142,13 @@ Result Result::asValidityResult() const throw() {
switch(d_sat) {
case SAT:
- return Result(INVALID);
+ return Result(INVALID, d_inputName);
case UNSAT:
- return Result(VALID);
+ return Result(VALID, d_inputName);
case SAT_UNKNOWN:
- return Result(VALIDITY_UNKNOWN, d_unknownExplanation);
+ return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
default:
Unhandled(d_sat);
@@ -155,7 +156,7 @@ Result Result::asValidityResult() const throw() {
}
// TYPE_NONE
- return Result(VALIDITY_UNKNOWN, NO_STATUS);
+ return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName);
}
string Result::toString() const {
diff --git a/src/util/result.h b/src/util/result.h
index cb1bd50fa..21bf563bd 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -71,47 +71,58 @@ private:
enum Validity d_validity;
enum Type d_which;
enum UnknownExplanation d_unknownExplanation;
+ std::string d_inputName;
public:
Result() :
d_sat(SAT_UNKNOWN),
d_validity(VALIDITY_UNKNOWN),
d_which(TYPE_NONE),
- d_unknownExplanation(UNKNOWN_REASON) {
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName("") {
}
- Result(enum Sat s) :
+ Result(enum Sat s, std::string inputName = "") :
d_sat(s),
d_validity(VALIDITY_UNKNOWN),
d_which(TYPE_SAT),
- d_unknownExplanation(UNKNOWN_REASON) {
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
CheckArgument(s != SAT_UNKNOWN,
"Must provide a reason for satisfiability being unknown");
}
- Result(enum Validity v) :
+ Result(enum Validity v, std::string inputName = "") :
d_sat(SAT_UNKNOWN),
d_validity(v),
d_which(TYPE_VALIDITY),
- d_unknownExplanation(UNKNOWN_REASON) {
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
CheckArgument(v != VALIDITY_UNKNOWN,
"Must provide a reason for validity being unknown");
}
- Result(enum Sat s, enum UnknownExplanation unknownExplanation) :
+ Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
d_sat(s),
d_validity(VALIDITY_UNKNOWN),
d_which(TYPE_SAT),
- d_unknownExplanation(unknownExplanation) {
+ d_unknownExplanation(unknownExplanation),
+ d_inputName(inputName) {
CheckArgument(s == SAT_UNKNOWN,
"improper use of unknown-result constructor");
}
- Result(enum Validity v, enum UnknownExplanation unknownExplanation) :
+ Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
d_sat(SAT_UNKNOWN),
d_validity(v),
d_which(TYPE_VALIDITY),
- d_unknownExplanation(unknownExplanation) {
+ d_unknownExplanation(unknownExplanation),
+ d_inputName(inputName) {
CheckArgument(v == VALIDITY_UNKNOWN,
"improper use of unknown-result constructor");
}
- Result(const std::string& s);
+ Result(const std::string& s, std::string inputName = "");
+
+ Result(const Result& r, std::string inputName) {
+ *this = r;
+ d_inputName = inputName;
+ }
enum Sat isSat() const {
return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
@@ -142,6 +153,8 @@ public:
std::string toString() const;
+ std::string getInputName() const { return d_inputName; }
+
};/* class Result */
inline bool Result::operator!=(const Result& r) const throw() {
diff --git a/src/util/result.i b/src/util/result.i
index 029a3618a..b77bfd881 100644
--- a/src/util/result.i
+++ b/src/util/result.i
@@ -12,8 +12,9 @@
%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation);
%ignore CVC4::operator==(enum Result::Sat, const Result&);
-%ignore CVC4::operator==(enum Result::Validity, const Result&);
%ignore CVC4::operator!=(enum Result::Sat, const Result&);
+
+%ignore CVC4::operator==(enum Result::Validity, const Result&);
%ignore CVC4::operator!=(enum Result::Validity, const Result&);
%include "util/result.h"
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index d44499fa8..b66d1cbe4 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -20,15 +20,70 @@
#include <vector>
#include "util/sort_inference.h"
+#include "theory/uf/options.h"
+//#include "theory/rewriter.h"
using namespace CVC4;
using namespace std;
namespace CVC4 {
+void SortInference::UnionFind::print(const char * c){
+ for( std::map< int, int >::iterator it = d_eqc.begin(); it != d_eqc.end(); ++it ){
+ Trace(c) << "s_" << it->first << " = s_" << it->second << ", ";
+ }
+ for( unsigned i=0; i<d_deq.size(); i++ ){
+ Trace(c) << "s_" << d_deq[i].first << " != s_" << d_deq[i].second << ", ";
+ }
+ Trace(c) << std::endl;
+}
+void SortInference::UnionFind::set( UnionFind& c ) {
+ clear();
+ for( std::map< int, int >::iterator it = c.d_eqc.begin(); it != c.d_eqc.end(); ++it ){
+ d_eqc[ it->first ] = it->second;
+ }
+ d_deq.insert( d_deq.end(), c.d_deq.begin(), c.d_deq.end() );
+}
+int SortInference::UnionFind::getRepresentative( int t ){
+ std::map< int, int >::iterator it = d_eqc.find( t );
+ if( it==d_eqc.end() || it->second==t ){
+ return t;
+ }else{
+ int rt = getRepresentative( it->second );
+ d_eqc[t] = rt;
+ return rt;
+ }
+}
+void SortInference::UnionFind::setEqual( int t1, int t2 ){
+ if( t1!=t2 ){
+ int rt1 = getRepresentative( t1 );
+ int rt2 = getRepresentative( t2 );
+ if( rt1>rt2 ){
+ d_eqc[rt1] = rt2;
+ }else{
+ d_eqc[rt2] = rt1;
+ }
+ }
+}
+bool SortInference::UnionFind::isValid() {
+ for( unsigned i=0; i<d_deq.size(); i++ ){
+ if( areEqual( d_deq[i].first, d_deq[i].second ) ){
+ return false;
+ }
+ }
+ return true;
+}
+
+
+void SortInference::recordSubsort( int s ){
+ s = d_type_union_find.getRepresentative( s );
+ if( std::find( d_sub_sorts.begin(), d_sub_sorts.end(), s )==d_sub_sorts.end() ){
+ d_sub_sorts.push_back( s );
+ }
+}
void SortInference::printSort( const char* c, int t ){
- int rt = getRepresentative( t );
+ int rt = d_type_union_find.getRepresentative( t );
if( d_type_types.find( rt )!=d_type_types.end() ){
Trace(c) << d_type_types[rt];
}else{
@@ -43,30 +98,49 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
std::map< Node, Node > var_bound;
process( assertions[i], var_bound );
}
- //print debug
- if( Trace.isOn("sort-inference") ){
- for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
- Trace("sort-inference") << it->first << " : ";
- if( !d_op_arg_types[ it->first ].empty() ){
- Trace("sort-inference") << "( ";
- for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
- printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
- Trace("sort-inference") << " ";
- }
- Trace("sort-inference") << ") -> ";
+ for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
+ Trace("sort-inference") << it->first << " : ";
+ if( !d_op_arg_types[ it->first ].empty() ){
+ Trace("sort-inference") << "( ";
+ for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
+ recordSubsort( d_op_arg_types[ it->first ][i] );
+ printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
+ Trace("sort-inference") << " ";
}
- printSort( "sort-inference", it->second );
- Trace("sort-inference") << std::endl;
+ Trace("sort-inference") << ") -> ";
}
- for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
- Trace("sort-inference") << "Quantified formula " << it->first << " : " << std::endl;
- for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- printSort( "sort-inference", it2->second );
- Trace("sort-inference") << std::endl;
- }
+ recordSubsort( it->second );
+ printSort( "sort-inference", it->second );
+ Trace("sort-inference") << std::endl;
+ }
+ for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
+ Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl;
+ for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+ printSort( "sort-inference", it2->second );
Trace("sort-inference") << std::endl;
}
+ Trace("sort-inference") << std::endl;
}
+
+ //determine monotonicity of sorts
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
+ std::map< Node, Node > var_bound;
+ processMonotonic( assertions[i], true, true, var_bound );
+ }
+
+ Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl;
+ for( unsigned i=0; i<d_sub_sorts.size(); i++ ){
+ printSort( "sort-inference", d_sub_sorts[i] );
+ if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
+ Trace("sort-inference") << " is interpreted." << std::endl;
+ }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
+ Trace("sort-inference") << " is monotonic." << std::endl;
+ }else{
+ Trace("sort-inference") << " is not monotonic." << std::endl;
+ }
+ }
+
if( doRewrite ){
//simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)
for( unsigned i=0; i<assertions.size(); i++ ){
@@ -82,47 +156,43 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
}
//add lemma enforcing introduced constants to be distinct?
}
- }
-}
-
-int SortInference::getRepresentative( int t ){
- std::map< int, int >::iterator it = d_type_union_find.find( t );
- if( it!=d_type_union_find.end() ){
- if( it->second==t ){
- return t;
- }else{
- int rt = getRepresentative( it->second );
- d_type_union_find[t] = rt;
- return rt;
+ }else if( !options::ufssSymBreak() ){
+ std::map< int, Node > constants;
+ //just add a bunch of unit lemmas
+ for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
+ int rt = d_type_union_find.getRepresentative( it->second );
+ if( d_op_arg_types[ it->first ].empty() && constants.find( rt )==constants.end() ){
+ constants[ rt ] = it->first;
+ }
}
- }else{
- return t;
+ //add unit lemmas for each constant
+ Node first_const;
+ for( std::map< int, Node >::iterator it = constants.begin(); it != constants.end(); ++it ){
+ if( first_const.isNull() ){
+ first_const = it->second;
+ }else{
+ Node eq = first_const.eqNode( it->second );
+ //eq = Rewriter::rewrite( eq );
+ Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl;
+ assertions.push_back( eq );
+ }
+ }
+
+
}
+ initialSortCount = sortCount;
}
void SortInference::setEqual( int t1, int t2 ){
if( t1!=t2 ){
- int rt1 = getRepresentative( t1 );
- int rt2 = getRepresentative( t2 );
+ int rt1 = d_type_union_find.getRepresentative( t1 );
+ int rt2 = d_type_union_find.getRepresentative( t2 );
if( rt1!=rt2 ){
Trace("sort-inference-debug") << "Set equal : ";
printSort( "sort-inference-debug", rt1 );
Trace("sort-inference-debug") << " ";
printSort( "sort-inference-debug", rt2 );
Trace("sort-inference-debug") << std::endl;
- //check if they must be a type
- std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 );
- std::map< int, TypeNode >::iterator it2 = d_type_types.find( rt2 );
- if( it2!=d_type_types.end() ){
- if( it1==d_type_types.end() ){
- //swap sides
- int swap = rt1;
- rt1 = rt2;
- rt2 = swap;
- }else{
- Assert( rt1==rt2 );
- }
- }
/*
d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() );
d_type_eq_class[rt2].clear();
@@ -132,7 +202,19 @@ void SortInference::setEqual( int t1, int t2 ){
}
Trace("sort-inference-debug") << "}" << std::endl;
*/
- d_type_union_find[rt2] = rt1;
+ if( rt2>rt1 ){
+ //swap
+ int swap = rt1;
+ rt1 = rt2;
+ rt2 = swap;
+ }
+ d_type_union_find.d_eqc[rt1] = rt2;
+ std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 );
+ if( it1!=d_type_types.end() ){
+ Assert( d_type_types.find( rt2 )==d_type_types.end() );
+ d_type_types[rt2] = it1->second;
+ d_type_types.erase( rt1 );
+ }
}
}
}
@@ -155,14 +237,17 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
Trace("sort-inference-debug") << "Process " << n << std::endl;
//add to variable bindings
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
- for( size_t i=0; i<n[0].getNumChildren(); i++ ){
- //TODO: try applying sort inference to quantified variables
- d_var_types[n][ n[0][i] ] = sortCount;
- sortCount++;
+ if( d_var_types.find( n )!=d_var_types.end() ){
+ return getIdForType( n.getType() );
+ }else{
+ for( size_t i=0; i<n[0].getNumChildren(); i++ ){
+ //apply sort inference to quantified variables
+ d_var_types[n][ n[0][i] ] = sortCount;
+ sortCount++;
- //type of the quantified variable must be the same
- //d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );
- var_bound[ n[0][i] ] = n;
+ //type of the quantified variable must be the same
+ var_bound[ n[0][i] ] = n;
+ }
}
}
@@ -192,6 +277,9 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
if( n.getKind()==kind::EQUAL ){
//we only require that the left and right hand side must be equal
setEqual( child_types[0], child_types[1] );
+ //int eqType = getIdForType( n[0].getType() );
+ //setEqual( child_types[0], eqType );
+ //setEqual( child_types[1], eqType );
retType = getIdForType( n.getType() );
}else if( n.getKind()==kind::APPLY_UF ){
Node op = n.getOperator();
@@ -227,11 +315,11 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
//d_type_eq_class[sortCount].push_back( n );
}
retType = d_op_return_types[n];
- }else if( n.isConst() ){
- Trace("sort-inference-debug") << n << " is a constant." << std::endl;
+ //}else if( n.isConst() ){
+ // Trace("sort-inference-debug") << n << " is a constant." << std::endl;
//can be any type we want
- retType = sortCount;
- sortCount++;
+ // retType = sortCount;
+ // sortCount++;
}else{
Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl;
//it is an interpretted term
@@ -251,9 +339,43 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
return retType;
}
+void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ) {
+ if( n.getKind()==kind::FORALL ){
+ for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+ var_bound[n[0][i]] = n;
+ }
+ processMonotonic( n[1], pol, hasPol, var_bound );
+ for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+ var_bound.erase( n[0][i] );
+ }
+ }else if( n.getKind()==kind::EQUAL ){
+ if( !hasPol || pol ){
+ for( unsigned i=0; i<2; i++ ){
+ if( var_bound.find( n[i] )==var_bound.end() ){
+ int sid = getSortId( var_bound[n[i]], n[i] );
+ d_non_monotonic_sorts[sid] = true;
+ break;
+ }
+ }
+ }
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ bool npol = pol;
+ bool nhasPol = hasPol;
+ if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){
+ npol = !npol;
+ }
+ if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){
+ nhasPol = false;
+ }
+ processMonotonic( n[i], npol, nhasPol, var_bound );
+ }
+ }
+}
+
TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){
- int rt = getRepresentative( t );
+ int rt = d_type_union_find.getRepresentative( t );
if( d_type_types.find( rt )!=d_type_types.end() ){
return d_type_types[rt];
}else{
@@ -278,7 +400,7 @@ TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){
}
TypeNode SortInference::getTypeForId( int t ){
- int rt = getRepresentative( t );
+ int rt = d_type_union_find.getRepresentative( t );
if( d_type_types.find( rt )!=d_type_types.end() ){
return d_type_types[rt];
}else{
@@ -414,15 +536,71 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
}
int SortInference::getSortId( Node n ) {
Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n;
- return getRepresentative( d_op_return_types[op] );
+ if( d_op_return_types.find( op )!=d_op_return_types.end() ){
+ return d_type_union_find.getRepresentative( d_op_return_types[op] );
+ }else{
+ return 0;
+ }
}
int SortInference::getSortId( Node f, Node v ) {
- return getRepresentative( d_var_types[f][v] );
+ if( d_var_types.find( f )!=d_var_types.end() ){
+ return d_type_union_find.getRepresentative( d_var_types[f][v] );
+ }else{
+ return 0;
+ }
}
void SortInference::setSkolemVar( Node f, Node v, Node sk ){
+ Trace("sort-inference-temp") << "Set skolem var for " << f << ", variable " << v << std::endl;
+ if( isWellSortedFormula( f ) && d_var_types.find( f )==d_var_types.end() ){
+ std::map< Node, Node > var_bound;
+ process( f, var_bound );
+ }
d_op_return_types[sk] = getSortId( f, v );
+ Trace("sort-inference-temp") << "Set skolem sort id for " << sk << " to " << d_op_return_types[sk] << std::endl;
+}
+
+bool SortInference::isWellSortedFormula( Node n ) {
+ if( n.getType().isBoolean() && n.getKind()!=kind::APPLY_UF ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !isWellSortedFormula( n[i] ) ){
+ return false;
+ }
+ }
+ return true;
+ }else{
+ return isWellSorted( n );
+ }
+}
+
+bool SortInference::isWellSorted( Node n ) {
+ if( getSortId( n )==0 ){
+ return false;
+ }else{
+ if( n.getKind()==kind::APPLY_UF ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ int s1 = getSortId( n[i] );
+ int s2 = d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] );
+ if( s1!=s2 ){
+ return false;
+ }
+ if( !isWellSorted( n[i] ) ){
+ return false;
+ }
+ }
+ }
+ return true;
+ }
+}
+
+void SortInference::getSortConstraints( Node n, UnionFind& uf ) {
+ if( n.getKind()==kind::APPLY_UF ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ getSortConstraints( n[i], uf );
+ uf.setEqual( getSortId( n[i] ), d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] ) );
+ }
+ }
}
}/* CVC4 namespace */
diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h
index 1bcb8a208..8f0fc5e9f 100644
--- a/src/util/sort_inference.h
+++ b/src/util/sort_inference.h
@@ -28,11 +28,33 @@ namespace CVC4 {
class SortInference{
private:
- //for debugging
- //std::map< int, std::vector< Node > > d_type_eq_class;
+ //all subsorts
+ std::vector< int > d_sub_sorts;
+ std::map< int, bool > d_non_monotonic_sorts;
+ void recordSubsort( int s );
+public:
+ class UnionFind {
+ public:
+ UnionFind(){}
+ UnionFind( UnionFind& c ){
+ set( c );
+ }
+ std::map< int, int > d_eqc;
+ //pairs that must be disequal
+ std::vector< std::pair< int, int > > d_deq;
+ void print(const char * c);
+ void clear() { d_eqc.clear(); d_deq.clear(); }
+ void set( UnionFind& c );
+ int getRepresentative( int t );
+ void setEqual( int t1, int t2 );
+ void setDisequal( int t1, int t2 ){ d_deq.push_back( std::pair< int, int >( t1, t2 ) ); }
+ bool areEqual( int t1, int t2 ) { return getRepresentative( t1 )==getRepresentative( t2 ); }
+ bool isValid();
+ };
private:
int sortCount;
- std::map< int, int > d_type_union_find;
+ int initialSortCount;
+ UnionFind d_type_union_find;
std::map< int, TypeNode > d_type_types;
std::map< TypeNode, int > d_id_for_types;
//for apply uf operators
@@ -41,12 +63,17 @@ private:
//for bound variables
std::map< Node, std::map< Node, int > > d_var_types;
//get representative
- int getRepresentative( int t );
void setEqual( int t1, int t2 );
int getIdForType( TypeNode tn );
void printSort( const char* c, int t );
//process
int process( Node n, std::map< Node, Node >& var_bound );
+
+//for monotonicity inference
+private:
+ void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound );
+
+//for rewriting
private:
//mapping from old symbols to new symbols
std::map< Node, Node > d_symbol_map;
@@ -60,15 +87,24 @@ private:
Node getNewSymbol( Node old, TypeNode tn );
//simplify
Node simplify( Node n, std::map< Node, Node >& var_bound );
+
public:
- SortInference() : sortCount( 0 ){}
+ SortInference() : sortCount( 1 ){}
~SortInference(){}
void simplify( std::vector< Node >& assertions, bool doRewrite = false );
+ //get sort id for term n
int getSortId( Node n );
+ //get sort id for variable of quantified formula f
int getSortId( Node f, Node v );
//set that sk is the skolem variable of v for quantifier f
void setSkolemVar( Node f, Node v, Node sk );
+public:
+ //is well sorted
+ bool isWellSortedFormula( Node n );
+ bool isWellSorted( Node n );
+ //get constraints for being well-typed according to computed sub-types
+ void getSortConstraints( Node n, SortInference::UnionFind& uf );
};
}
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 3bec559d5..8ffc60d17 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -847,7 +847,7 @@ public:
* like in this example, which takes the place of the declaration of a
* statistics field "d_checkTimer":
*
- * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::morgan::checkTime");
+ * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime");
*
* If any args need to be passed to the constructor, you can specify
* them after the string.
diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp
index ab4c95ea5..1c2dc2edf 100644
--- a/src/util/util_model.cpp
+++ b/src/util/util_model.cpp
@@ -24,7 +24,7 @@ using namespace std;
namespace CVC4 {
-std::ostream& operator<<(std::ostream& out, Model& m) {
+std::ostream& operator<<(std::ostream& out, const Model& m) {
smt::SmtScope smts(&m.d_smt);
Expr::dag::Scope scope(out, false);
Printer::getPrinter(options::outputLanguage())->toStream(out, m);
diff --git a/src/util/util_model.h b/src/util/util_model.h
index 535493a2d..e5bd1f955 100644
--- a/src/util/util_model.h
+++ b/src/util/util_model.h
@@ -29,10 +29,14 @@ class Command;
class SmtEngine;
class Model;
-std::ostream& operator<<(std::ostream&, Model&);
+std::ostream& operator<<(std::ostream&, const Model&);
class Model {
- friend std::ostream& operator<<(std::ostream&, Model&);
+ friend std::ostream& operator<<(std::ostream&, const Model&);
+ friend class SmtEngine;
+
+ /** the input name (file name, etc.) this model is associated to */
+ std::string d_inputName;
protected:
/** The SmtEngine we're associated with */
@@ -50,6 +54,10 @@ public:
const Command* getCommand(size_t i) const;
/** get the smt engine that this model is hooked up to */
SmtEngine* getSmtEngine() { return &d_smt; }
+ /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
+ const SmtEngine* getSmtEngine() const { return &d_smt; }
+ /** get the input name (file name, etc.) this model is associated to */
+ std::string getInputName() const { return d_inputName; }
public:
/** get value for expression */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback