diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 13 | ||||
-rw-r--r-- | src/util/bitvector.h | 14 | ||||
-rw-r--r-- | src/util/boolean_simplification.h | 2 | ||||
-rw-r--r-- | src/util/chain.h | 50 | ||||
-rw-r--r-- | src/util/chain.i | 12 | ||||
-rw-r--r-- | src/util/cvc4_assert.cpp | 2 | ||||
-rw-r--r-- | src/util/cvc4_assert.h | 14 | ||||
-rw-r--r-- | src/util/datatype.h | 1 | ||||
-rw-r--r-- | src/util/debug.h | 4 | ||||
-rw-r--r-- | src/util/divisible.cpp | 29 | ||||
-rw-r--r-- | src/util/divisible.h | 62 | ||||
-rw-r--r-- | src/util/divisible.i | 10 | ||||
-rw-r--r-- | src/util/dump.h | 1 | ||||
-rw-r--r-- | src/util/exception.h | 8 | ||||
-rw-r--r-- | src/util/ite_removal.cpp | 6 | ||||
-rw-r--r-- | src/util/output.h | 2 | ||||
-rw-r--r-- | src/util/output.i | 70 | ||||
-rw-r--r-- | src/util/rational_cln_imp.h | 4 | ||||
-rw-r--r-- | src/util/record.h | 1 | ||||
-rw-r--r-- | src/util/recursion_breaker.h | 2 | ||||
-rw-r--r-- | src/util/regexp.h | 353 | ||||
-rw-r--r-- | src/util/result.cpp | 21 | ||||
-rw-r--r-- | src/util/result.h | 33 | ||||
-rw-r--r-- | src/util/result.i | 3 | ||||
-rw-r--r-- | src/util/sort_inference.cpp | 308 | ||||
-rw-r--r-- | src/util/sort_inference.h | 46 | ||||
-rw-r--r-- | src/util/statistics_registry.h | 2 | ||||
-rw-r--r-- | src/util/util_model.cpp | 2 | ||||
-rw-r--r-- | src/util/util_model.h | 12 |
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 */ |