diff options
Diffstat (limited to 'src/util')
47 files changed, 559 insertions, 198 deletions
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index ea0b26248..54d95ced0 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): acsys ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/Assert.h b/src/util/Assert.h index e38a3f9cf..3334de4a0 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -235,9 +235,7 @@ public: #ifdef CVC4_DEBUG -#ifdef CVC4_DEBUG extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException; -#endif /* CVC4_DEBUG */ /** * Special assertion failure handling in debug mode; in non-debug @@ -259,9 +257,9 @@ void debugAssertionFailed(const AssertionException& thisException, do { \ if(EXPECT_FALSE( ! (cond) )) { \ /* save the last assertion failure */ \ - const char* lastException = s_debugLastException; \ - CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ - CVC4::debugAssertionFailed(exception, lastException); \ + const char* lastException = ::CVC4::s_debugLastException; \ + ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + ::CVC4::debugAssertionFailed(exception, lastException); \ } \ } while(0) @@ -271,27 +269,27 @@ void debugAssertionFailed(const AssertionException& thisException, # define AlwaysAssert(cond, msg...) \ do { \ if(EXPECT_FALSE( ! (cond) )) { \ - throw CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ } \ } while(0) #endif /* CVC4_DEBUG */ #define Unreachable(msg...) \ - throw CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw ::CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unhandled(msg...) \ - throw CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw ::CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unimplemented(msg...) \ - throw CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw ::CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define InternalError(msg...) \ - throw CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define IllegalArgument(arg, msg...) \ - throw CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw ::CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define CheckArgument(cond, arg, msg...) \ AlwaysAssertArgument(cond, arg, ## msg) #define AlwaysAssertArgument(cond, arg, msg...) \ do { \ if(EXPECT_FALSE( ! (cond) )) { \ - throw CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ } \ } while(0) diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 61ff27c08..f371a4d72 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -8,7 +8,7 @@ noinst_LTLIBRARIES = libutil.la libutilcudd.la # libutilcudd.la is a separate library so that we can pass separate # compiler flags libutilcudd_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) @CUDD_CPPFLAGS@ -libutilcudd_la_LIBADD = @CUDD_LDFLAGS@ +libutilcudd_la_LIBADD = @CUDD_LDFLAGS@ @CUDD_LIBS@ # Do not list built sources (like integer.h, rational.h, and tls.h) here! # Rather, list them under BUILT_SOURCES, and their .in versions under diff --git a/src/util/array.h b/src/util/array.h index c00cfdaa3..22605922b 100644 --- a/src/util/array.h +++ b/src/util/array.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/backtrackable.h b/src/util/backtrackable.h index 418172235..c5c6b1399 100644 --- a/src/util/backtrackable.h +++ b/src/util/backtrackable.h @@ -2,10 +2,10 @@ /*! \file backtrackable.h ** \verbatim ** Original author: lianah - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/bitvector.h b/src/util/bitvector.h index ade08164b..f05ebaf17 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -2,7 +2,7 @@ /*! \file bitvector.h ** \verbatim ** Original author: dejan - ** Major contributors: mdeters, cconway + ** Major contributors: cconway, mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/util/bool.h b/src/util/bool.h index d2a29c8d5..15d46b5d1 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp index 92534bfd4..862f1e5fc 100644 --- a/src/util/boolean_simplification.cpp +++ b/src/util/boolean_simplification.cpp @@ -1,7 +1,7 @@ /********************* */ /*! \file boolean_simplification.cpp ** \verbatim - ** Original author: taking + ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index c2da8af5b..b3dffa475 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -2,7 +2,7 @@ /*! \file boolean_simplification.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -198,6 +198,16 @@ public: } /** + * Negates an Expr, doing all the double-negation elimination that's + * possible. + * + * @param e the Expr to negate (cannot be the null Expr) + */ + static Expr negate(Expr e) throw(AssertionException) { + return negate(Node::fromExpr(e)).toExpr(); + } + + /** * Simplify an OR, AND, or IMPLIES. This function is the identity * for all other kinds. */ diff --git a/src/util/cardinality.h b/src/util/cardinality.h index e7f86c80e..6985ae38e 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -22,6 +22,11 @@ #ifndef __CVC4__CARDINALITY_H #define __CVC4__CARDINALITY_H +#if SWIG +%include "util/integer.h" +%include "util/Assert.h" +#endif /* SWIG */ + #include <iostream> #include <utility> @@ -140,6 +145,11 @@ public: return d_card > 0; } + /** Returns true iff this cardinality is infinite. */ + bool isInfinite() const throw() { + return d_card < 0; + } + /** * Returns true iff this cardinality is finite or countably * infinite. diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index aa3e6bf6b..c13b63e3f 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -49,6 +49,10 @@ bool Configuration::isTracingBuild() { return IS_TRACING_BUILD; } +bool Configuration::isDumpingBuild() { + return IS_DUMPING_BUILD; +} + bool Configuration::isMuzzledBuild() { return IS_MUZZLED_BUILD; } @@ -89,7 +93,11 @@ unsigned Configuration::getVersionRelease() { return CVC4_RELEASE; } -string Configuration::about() { +std::string Configuration::getVersionExtra() { + return CVC4_EXTRAVERSION; +} + +std::string Configuration::about() { return CVC4_ABOUT_STRING; } diff --git a/src/util/configuration.h b/src/util/configuration.h index 31a2ca3d4..cb207298c 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -53,6 +53,8 @@ public: static bool isTracingBuild(); + static bool isDumpingBuild(); + static bool isMuzzledBuild(); static bool isAssertionBuild(); @@ -73,6 +75,8 @@ public: static unsigned getVersionRelease(); + static std::string getVersionExtra(); + static std::string about(); static bool isBuiltWithGmp(); diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index 0421273ca..13347d970 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -49,6 +49,12 @@ namespace CVC4 { # define IS_TRACING_BUILD false #endif /* CVC4_TRACING */ +#ifdef CVC4_DUMPING +# define IS_DUMPING_BUILD true +#else /* CVC4_DUMPING */ +# define IS_DUMPING_BUILD false +#endif /* CVC4_DUMPING */ + #ifdef CVC4_MUZZLE # define IS_MUZZLED_BUILD true #else /* CVC4_MUZZLE */ diff --git a/src/util/congruence_closure.cpp b/src/util/congruence_closure.cpp index 9ce902b2a..14315ac5a 100644 --- a/src/util/congruence_closure.cpp +++ b/src/util/congruence_closure.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 83f6d15c0..4e690ec16 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -34,7 +34,7 @@ #include "context/cdset.h" #include "context/cdlist_context_memory.h" #include "util/exception.h" -#include "theory/uf/morgan/stacking_map.h" +#include "context/stacking_map.h" #include "util/stats.h" namespace CVC4 { @@ -66,11 +66,11 @@ struct CongruenceOperator { typedef Tail_ Tail; };/* class CongruenceOperator<> */ -#define CONGRUENCE_OPERATORS_1(kind1) CongruenceOperator<kind1, EndOfCongruenceOpList> -#define CONGRUENCE_OPERATORS_2(kind1, kind2) CongruenceOperator<kind1, CONGRUENCE_OPERATORS_1(kind2)> -#define CONGRUENCE_OPERATORS_3(kind1, kind2, kind3) CongruenceOperator<kind1, CONGRUENCE_OPERATORS_2(kind2, kind3)> -#define CONGRUENCE_OPERATORS_4(kind1, kind2, kind3, kind4) CongruenceOperator<kind1, CONGRUENCE_OPERATORS_3(kind2, kind3, kind4)> -#define CONGRUENCE_OPERATORS_5(kind1, kind2, kind3, kind4, kind5) CongruenceOperator<kind1, CONGRUENCE_OPERATORS_4(kind2, kind3, kind4, kind5)> +#define CONGRUENCE_OPERATORS_1(kind1) ::CVC4::CongruenceOperator<kind1, ::CVC4::EndOfCongruenceOpList> +#define CONGRUENCE_OPERATORS_2(kind1, kind2) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_1(kind2)> +#define CONGRUENCE_OPERATORS_3(kind1, kind2, kind3) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_2(kind2, kind3)> +#define CONGRUENCE_OPERATORS_4(kind1, kind2, kind3, kind4) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_3(kind2, kind3, kind4)> +#define CONGRUENCE_OPERATORS_5(kind1, kind2, kind3, kind4, kind5) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_4(kind2, kind3, kind4, kind5)> /** * Returns true if the kind k is registered as a congruence operator @@ -139,7 +139,7 @@ class CongruenceClosure { OutputChannel* d_out; // typedef all of these so that iterators are easy to define - typedef theory::uf::morgan::StackingMap<Node, NodeHashFunction> RepresentativeMap; + typedef context::StackingMap<Node, Node, NodeHashFunction> RepresentativeMap; typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList; typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists; typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList; @@ -270,6 +270,7 @@ private: if(i == d_eqMap.end()) { ++d_newSkolemVars; Node v = NodeManager::currentNM()->mkSkolem(t.getType()); + Debug("cc") << "CC made skolem " << v << std::endl; addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null()); d_added.insert(v); d_eqMap[t] = v; @@ -333,7 +334,7 @@ private: * Find the EC representative for a term t in the current context. */ inline TNode find(TNode t) const throw(AssertionException) { - TNode rep1 = d_representative.find(t); + TNode rep1 = d_representative[t]; return rep1.isNull() ? t : rep1; } @@ -1088,7 +1089,6 @@ std::ostream& operator<<(std::ostream& out, return out; } - }/* CVC4 namespace */ #endif /* __CVC4__UTIL__CONGRUENCE_CLOSURE_H */ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 926f31847..93651f1a9 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -2,7 +2,7 @@ /*! \file datatype.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: ajreynol ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/util/datatype.h b/src/util/datatype.h index 477b16f66..c64f420dd 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/debug.h b/src/util/debug.h index 402c5bed4..ad2dbc2dd 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp index 7641472f8..46807b1f9 100644 --- a/src/util/decision_engine.cpp +++ b/src/util/decision_engine.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index 3eee8aeb6..1c2bd3ef7 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/dynamic_array.h b/src/util/dynamic_array.h index c0a8cf260..2c8b842e4 100644 --- a/src/util/dynamic_array.h +++ b/src/util/dynamic_array.h @@ -2,10 +2,10 @@ /*! \file dynamic_array.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -17,11 +17,10 @@ ** \todo document this file **/ - #include "cvc4_private.h" -#ifndef __CVC4__UTIL__DYNAMICARRAY_H -#define __CVC4__UTIL__DYNAMICARRAY_H +#ifndef __CVC4__UTIL__DYNAMIC_ARRAY_H +#define __CVC4__UTIL__DYNAMIC_ARRAY_H #include "util/Assert.h" @@ -29,14 +28,14 @@ namespace CVC4 { template <class T> class DynamicArray { -private: +protected: T* d_arr; unsigned d_size; unsigned d_allocated; bool d_callDestructor; - void grow(){ + void grow() { bool empty = (d_arr == NULL); d_allocated = empty ? 15 : d_allocated * 2 + 1; unsigned allocSize = sizeof(T) * d_allocated; @@ -48,14 +47,14 @@ private: } public: - DynamicArray(bool deallocate = false): + DynamicArray(bool callDestructor = false) : d_arr(NULL), d_size(0), d_allocated(0), - d_callDestructor(deallocate){ + d_callDestructor(callDestructor) { } - ~DynamicArray(){ + virtual ~DynamicArray() { if(d_callDestructor) { for(unsigned i = 0; i < d_size; ++i) { d_arr[i].~T(); @@ -83,12 +82,17 @@ public: ++d_size; } + const T& operator[](unsigned i) const { + Assert(i < d_size, "index out of bounds in DynamicArray::operator[]"); + return d_arr[i]; + } + T& operator[](unsigned i) { Assert(i < d_size, "index out of bounds in DynamicArray::operator[]"); return d_arr[i]; } - const T& back() const{ + const T& back() const { Assert(d_size > 0, "DynamicArray::back() called on empty list"); return d_arr[d_size - 1]; } @@ -96,12 +100,53 @@ public: void pop_back() { Assert(d_size > 0, "DynamicArray::back() called on empty list"); --d_size; - if(d_callDestructor){ - d_arr[d_size].~T();; + if(d_callDestructor) { + d_arr[d_size].~T(); + } + } + + typedef T* iterator; + typedef const T* const_iterator; + + iterator begin() { return d_arr; } + iterator end() { return d_arr + d_size; } + const_iterator begin() const { return d_arr; } + const_iterator end() const { return d_arr + d_size; } + +};/* class DynamicArray<T> */ + +template <class T, class Ctor = T> +class DynamicGrowingArray : public DynamicArray<T> { + Ctor d_ctor; + +public: + DynamicGrowingArray(bool callDestructor, const Ctor& c) : + DynamicArray<T>(callDestructor), + d_ctor(c) { + } + + DynamicGrowingArray(bool callDestructor = false) : + DynamicArray<T>(callDestructor), + d_ctor() { + } + + T& operator[](unsigned i) { + while(this->d_allocated <= i) { + this->grow(); + } + while(this->d_size <= i) { + ::new((void*)(this->d_arr + this->d_size)) T(d_ctor); + ++this->d_size; } + return this->d_arr[i]; + } + + const T& operator[](unsigned i) const { + Assert(this->d_size > i); + return this->d_arr[i]; } -};/* CVC4::DynamicArray */ +};/* CVC4::DynamicGrowingArray */ }/* CVC4 namespace */ -#endif /* __CVC4__UTIL__DYNAMICARRAY_H */ +#endif /* __CVC4__UTIL__DYNAMIC_ARRAY_H */ diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index 87102e644..7d2badbfe 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/hash.h b/src/util/hash.h index cca60ce76..10211970f 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/integer.h.in b/src/util/integer.h.in index 7e1b9a1aa..b2973081d 100644 --- a/src/util/integer.h.in +++ b/src/util/integer.h.in @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief A multiprecision integer constant. + ** \brief A multiprecision integer constant ** ** A multiprecision integer constant. **/ @@ -26,8 +26,14 @@ #ifdef CVC4_CLN_IMP # include "util/integer_cln_imp.h" +# if SWIG + %include "util/integer_cln_imp.h" +# endif /* SWIG */ #endif /* CVC4_CLN_IMP */ #ifdef CVC4_GMP_IMP # include "util/integer_gmp_imp.h" +# if SWIG + %include "util/integer_gmp_imp.h" +# endif /* SWIG */ #endif /* CVC4_GMP_IMP */ diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 664027cdc..a7de8c75e 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -2,10 +2,10 @@ /*! \file integer_cln_imp.h ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): mdeters, dejan + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 60cee3937..237114d24 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -2,10 +2,10 @@ /*! \file integer_gmp_imp.h ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index e9c5122b3..bd5048040 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -2,7 +2,7 @@ /*! \file ite_removal.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -11,20 +11,22 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Representation of cardinality + ** \brief Removal of term ITEs ** - ** Simple class to represent a cardinality; used by the CVC4 type system - ** give the cardinality of sorts. + ** Removal of term ITEs. **/ #include <vector> #include "util/ite_removal.h" #include "theory/rewriter.h" +#include "expr/command.h" using namespace CVC4; using namespace std; +namespace CVC4 { + struct IteRewriteAttrTag {}; typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr; @@ -34,8 +36,7 @@ void RemoveITE::run(std::vector<Node>& output) { } } -Node RemoveITE::run(TNode node, std::vector<Node>& output) -{ +Node RemoveITE::run(TNode node, std::vector<Node>& output) { // Current node Debug("ite") << "removeITEs(" << node << ")" << endl; @@ -54,8 +55,18 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output) // Make the skolem to represent the ITE Node skolem = nodeManager->mkVar(nodeType); + if(Dump.isOn("declarations")) { + stringstream kss; + kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << skolem; + string ks = kss.str(); + Dump("declarations") << CommentCommand(ks + " is a variable introduced due to term-level ITE removal") << endl + << DeclareFunctionCommand(ks, nodeType.toType()) << endl; + } + // The new assertion - Node newAssertion = nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2])); + Node newAssertion = + nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), + skolem.eqNode(node[2])); Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; // Attach the skolem @@ -91,4 +102,6 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output) nodeManager->setAttribute(node, IteRewriteAttr(), Node::null()); return node; } -}; +} + +}/* CVC4 namespace */ diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index b286665cc..d68c6d933 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -1,9 +1,9 @@ /********************* */ /*! \file ite_removal.h ** \verbatim - ** Original author: mdeters + ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -11,10 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Representation of cardinality + ** \brief Removal of term ITEs ** - ** Simple class to represent a cardinality; used by the CVC4 type system - ** give the cardinality of sorts. + ** Removal of term ITEs. **/ #pragma once @@ -38,7 +37,6 @@ public: */ static Node run(TNode node, std::vector<Node>& additionalAssertions); -}; +};/* class RemoveTTE */ - -} +}/* CVC4 namespace */ diff --git a/src/util/language.h b/src/util/language.h index dbda6a315..d3405e35b 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -86,6 +86,9 @@ namespace output { enum CVC4_PUBLIC Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 + /** Match the output language to the input language */ + LANG_AUTO = -1, + // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE // diff --git a/src/util/matcher.h b/src/util/matcher.h index 5dc511bc2..6daceb8fd 100644 --- a/src/util/matcher.h +++ b/src/util/matcher.h @@ -1,8 +1,8 @@ /********************* */ /*! \file matcher.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none + ** Original author: mdeters + ** Major contributors: ajreynol ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/util/ntuple.h b/src/util/ntuple.h index 4c9a033a1..4f8b73945 100644 --- a/src/util/ntuple.h +++ b/src/util/ntuple.h @@ -30,6 +30,11 @@ public: T1 first; T2 second; T3 third; + triple(const T1& t1, const T2& t2, const T3& t3) : + first(t1), + second(t2), + third(t3) { + } };/* class triple<> */ template <class T1, class T2, class T3> @@ -45,9 +50,12 @@ public: T2 second; T3 third; T4 fourth; - quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) - : first(t1), second(t2), third(t3), fourth(t4) - { } + quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) : + first(t1), + second(t2), + third(t3), + fourth(t4) { + } };/* class quad<> */ template <class T1, class T2, class T3, class T4> diff --git a/src/util/options.cpp b/src/util/options.cpp index 9bceee931..7e6011352 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -2,7 +2,7 @@ /*! \file options.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: taking, cconway + ** Major contributors: cconway, taking ** Minor contributors (to current version): barrett, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -62,15 +62,16 @@ Options::Options() : err(&std::cerr), verbosity(0), inputLanguage(language::input::LANG_AUTO), - uf_implementation(MORGAN), + outputLanguage(language::output::LANG_AUTO), parseOnly(false), + preprocessOnly(false), semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT), theoryRegistration(true), memoryMap(false), strictParsing(false), lazyDefinitionExpansion(false), simplificationMode(SIMPLIFICATION_MODE_BATCH), - simplificationStyle(NO_SIMPLIFICATION_STYLE), + doStaticLearning(true), interactive(false), interactiveSetByUser(false), segvNoSpin(false), @@ -95,10 +96,13 @@ Options::Options() : static const string optionsDescription = "\ --lang | -L force input language (default is `auto'; see --lang help)\n\ + --output-lang force output language (default is `auto'; see --lang help)\n\ --version | -V identify this CVC4 binary\n\ --help | -h this command line reference\n\ --parse-only exit after parsing input\n\ - --preprocess-only exit after parsing preprocessing input (and dump preprocessed assertions, unless -q)\n\ + --preprocess-only exit after preprocessing (useful with --stats or --dump)\n\ + --dump=MODE dump preprocessed assertions, T-propagations, etc., see --dump=help\n\ + --dump-to=FILE all dumping goes to FILE (instead of stdout)\n\ --mmap memory map file input\n\ --show-config show CVC4 static configuration\n\ --segv-nospin don't spin on segfault waiting for gdb\n\ @@ -115,13 +119,13 @@ static const string optionsDescription = "\ --stats give statistics on exit\n\ --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ --print-expr-types print types with variables when printing exprs\n\ - --uf=morgan|tim select uninterpreted function theory implementation\n\ --interactive run interactively\n\ --no-interactive do not run interactively\n\ --produce-models support the get-value command\n\ --produce-assignments support the get-assignment command\n\ --lazy-definition-expansion expand define-fun lazily\n\ --simplification=MODE choose simplification mode, see --simplification=help\n\ + --no-static-learning turn off static learning (e.g. diamond-breaking)\n\ --replay=file replay decisions from file\n\ --replay-log=file log decisions and propagations to file\n\ --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\ @@ -140,6 +144,13 @@ Languages currently supported as arguments to the -L / --lang option:\n\ pl | cvc4 CVC4 presentation language\n\ smt | smtlib SMT-LIB format 1.2\n\ smt2 | smtlib2 SMT-LIB format 2.0\n\ +\n\ +Languages currently supported as arguments to the --output-lang option:\n\ + auto match the output language to the input language\n\ + pl | cvc4 CVC4 presentation language\n\ + smt | smtlib SMT-LIB format 1.2\n\ + smt2 | smtlib2 SMT-LIB format 2.0\n\ + ast internal format (simple syntax-tree language)\n\ "; static const string simplificationHelp = "\ @@ -154,18 +165,74 @@ incremental\n\ + run nonclausal simplification and clausal propagation at each ASSERT\n\ (and at CHECKSAT/QUERY/SUBTYPE)\n\ \n\ -You can also specify the level of aggressiveness for the simplification\n\ -(by repeating the --simplification option):\n\ +none\n\ ++ do not perform nonclausal simplification\n\ +"; + +static const string dumpHelp = "\ +Dump modes currently supported by the --dump option:\n\ \n\ -toplevel (default)\n\ -+ apply toplevel simplifications (things known true/false at outer level\n\ - only)\n\ +benchmark\n\ ++ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\ + does not include any declarations or assertions. Implied by all following\n\ + modes.\n\ \n\ -aggressive\n\ -+ do aggressive, local simplification across the entire formula\n\ +declarations\n\ ++ Dump declarations. Implied by all following modes.\n\ \n\ -none\n\ -+ do not perform nonclausal simplification\n\ +assertions\n\ ++ Output the assertions after non-clausal simplification and static\n\ + learning phases, but before presolve-time T-lemmas arrive. If\n\ + non-clausal simplification and static learning are off\n\ + (--simplification=none --no-static-learning), the output\n\ + will closely resemble the input (with term-level ITEs removed).\n\ +\n\ +learned\n\ ++ Output the assertions after non-clausal simplification, static\n\ + learning, and presolve-time T-lemmas. This should include all eager\n\ + T-lemmas (in the form provided by the theory, which my or may not be\n\ + clausal). Also includes level-0 BCP done by Minisat.\n\ +\n\ +clauses\n\ ++ Do all the preprocessing outlined above, and dump the CNF-converted\n\ + output\n\ +\n\ +state\n\ ++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\ + Implied by all \"stateful\" modes below and conflicts with all\n\ + non-stateful modes below.\n\ +\n\ +t-conflicts [non-stateful]\n\ ++ Output correctness queries for all theory conflicts\n\ +\n\ +missed-t-conflicts [stateful]\n\ ++ Output completeness queries for theory conflicts\n\ +\n\ +t-propagations [stateful]\n\ ++ Output correctness queries for all theory propagations\n\ +\n\ +missed-t-propagations [stateful]\n\ ++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\ +\n\ +t-lemmas [non-stateful]\n\ ++ Output correctness queries for all theory lemmas\n\ +\n\ +t-explanations [non-stateful]\n\ ++ Output correctness queries for all theory explanations\n\ +\n\ +Dump modes can be combined with multiple uses of --dump. Generally you want\n\ +one from the assertions category (either asertions, learned, or clauses), and\n\ +perhaps one or more stateful or non-stateful modes for checking correctness\n\ +and completeness of decision procedure implementations. Stateful modes dump\n\ +the contextual assertions made by the core solver (all decisions and propagations\n\ +as assertions; that affects the validity of the resulting correctness and\n\ +completeness queries, so of course stateful and non-stateful modes cannot\n\ +be mixed in the same run.\n\ +\n\ +The --output-language option controls the language used for dumping, and\n\ +this allows you to connect CVC4 to another solver implementation via a UNIX\n\ +pipe to perform on-line checking. The --dump-to option can be used to dump\n\ +to a file.\n\ "; string Options::getDescription() const { @@ -192,8 +259,11 @@ enum OptionValue { SMTCOMP = 256, /* avoid clashing with char options */ STATS, SEGV_NOSPIN, + OUTPUT_LANGUAGE, PARSE_ONLY, PREPROCESS_ONLY, + DUMP, + DUMP_TO, NO_CHECKING, NO_THEORY_REGISTRATION, USE_MMAP, @@ -204,6 +274,7 @@ enum OptionValue { UF_THEORY, LAZY_DEFINITION_EXPANSION, SIMPLIFICATION_MODE, + NO_STATIC_LEARNING, INTERACTIVE, NO_INTERACTIVE, PRODUCE_MODELS, @@ -263,8 +334,11 @@ static struct option cmdlineOptions[] = { { "version" , no_argument , NULL, 'V' }, { "about" , no_argument , NULL, 'V' }, { "lang" , required_argument, NULL, 'L' }, + { "output-lang", required_argument, NULL, OUTPUT_LANGUAGE }, { "parse-only" , no_argument , NULL, PARSE_ONLY }, - { "preprocess-only", no_argument , NULL, PREPROCESS_ONLY }, + { "preprocess-only", no_argument , NULL, PREPROCESS_ONLY }, + { "dump" , required_argument, NULL, DUMP }, + { "dump-to" , required_argument, NULL, DUMP_TO }, { "mmap" , no_argument , NULL, USE_MMAP }, { "strict-parsing", no_argument , NULL, STRICT_PARSING }, { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH }, @@ -272,6 +346,7 @@ static struct option cmdlineOptions[] = { { "uf" , required_argument, NULL, UF_THEORY }, { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION }, { "simplification", required_argument, NULL, SIMPLIFICATION_MODE }, + { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING }, { "interactive", no_argument , NULL, INTERACTIVE }, { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { "produce-models", no_argument , NULL, PRODUCE_MODELS }, @@ -371,6 +446,32 @@ throw(OptionException) { languageHelp = true; break; + case OUTPUT_LANGUAGE: + if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) { + outputLanguage = language::output::LANG_CVC4; + break; + } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) { + outputLanguage = language::output::LANG_SMTLIB; + break; + } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) { + outputLanguage = language::output::LANG_SMTLIB_V2; + break; + } else if(!strcmp(optarg, "ast")) { + outputLanguage = language::output::LANG_AST; + break; + } else if(!strcmp(optarg, "auto")) { + outputLanguage = language::output::LANG_AUTO; + break; + } + + if(strcmp(optarg, "help")) { + throw OptionException(string("unknown language for --output-lang: `") + + optarg + "'. Try --output-lang help."); + } + + languageHelp = true; + break; + case 't': Trace.on(optarg); break; @@ -396,6 +497,87 @@ throw(OptionException) { preprocessOnly = true; break; + case DUMP: { +#ifdef CVC4_DUMPING + char* tokstr = optarg; + char* toksave; + while((optarg = strtok_r(tokstr, ",", &toksave)) != NULL) { + tokstr = NULL; + if(!strcmp(optarg, "benchmark")) { + } else if(!strcmp(optarg, "declarations")) { + } else if(!strcmp(optarg, "assertions")) { + } else if(!strcmp(optarg, "learned")) { + } else if(!strcmp(optarg, "clauses")) { + } else if(!strcmp(optarg, "t-conflicts") || + !strcmp(optarg, "t-lemmas") || + !strcmp(optarg, "t-explanations")) { + // These are "non-state-dumping" modes. If state (SAT decisions, + // propagations, etc.) is dumped, it will interfere with the validity + // of these generated queries. + if(Dump.isOn("state")) { + throw OptionException(string("dump option `") + optarg + + "' conflicts with a previous, " + "state-dumping dump option. You cannot " + "mix stateful and non-stateful dumping modes; " + "see --dump help."); + } else { + Dump.on("no-permit-state"); + } + } else if(!strcmp(optarg, "state") || + !strcmp(optarg, "missed-t-conflicts") || + !strcmp(optarg, "t-propagations") || + !strcmp(optarg, "missed-t-propagations")) { + // These are "state-dumping" modes. If state (SAT decisions, + // propagations, etc.) is not dumped, it will interfere with the + // validity of these generated queries. + if(Dump.isOn("no-permit-state")) { + throw OptionException(string("dump option `") + optarg + + "' conflicts with a previous, " + "non-state-dumping dump option. You cannot " + "mix stateful and non-stateful dumping modes; " + "see --dump help."); + } else { + Dump.on("state"); + } + } else if(!strcmp(optarg, "help")) { + puts(dumpHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --dump: `") + + optarg + "'. Try --dump help."); + } + + Dump.on(optarg); + Dump.on("benchmark"); + if(strcmp(optarg, "benchmark")) { + Dump.on("declarations"); + } + } +#else /* CVC4_DUMPING */ + throw OptionException("The dumping feature was disabled in this build of CVC4."); +#endif /* CVC4_DUMPING */ + break; + } + + case DUMP_TO: { +#ifdef CVC4_DUMPING + if(optarg == NULL || *optarg == '\0') { + throw OptionException(string("Bad file name for --dump-to")); + } else if(!strcmp(optarg, "-")) { + Dump.setStream(DumpC::dump_cout); + } else { + ostream* dumpTo = new ofstream(optarg, ofstream::out | ofstream::trunc); + if(!*dumpTo) { + throw OptionException(string("Cannot open dump-to file (maybe it exists): `") + optarg + "'"); + } + Dump.setStream(*dumpTo); + } +#else /* CVC4_DUMPING */ + throw OptionException("The dumping feature was disabled in this build of CVC4."); +#endif /* CVC4_DUMPING */ + } + break; + case NO_THEORY_REGISTRATION: theoryRegistration = false; break; @@ -437,24 +619,6 @@ throw(OptionException) { } break; - case UF_THEORY: - { - if(!strcmp(optarg, "tim")) { - uf_implementation = Options::TIM; - } else if(!strcmp(optarg, "morgan")) { - uf_implementation = Options::MORGAN; - } else if(!strcmp(optarg, "help")) { - printf("UF implementations available:\n"); - printf(" tim\n"); - printf(" morgan\n"); - exit(1); - } else { - throw OptionException(string("unknown option for --uf: `") + - optarg + "'. Try --uf help."); - } - } - break; - case LAZY_DEFINITION_EXPANSION: lazyDefinitionExpansion = true; break; @@ -464,12 +628,8 @@ throw(OptionException) { simplificationMode = SIMPLIFICATION_MODE_BATCH; } else if(!strcmp(optarg, "incremental")) { simplificationMode = SIMPLIFICATION_MODE_INCREMENTAL; - } else if(!strcmp(optarg, "aggressive")) { - simplificationStyle = AGGRESSIVE_SIMPLIFICATION_STYLE; - } else if(!strcmp(optarg, "toplevel")) { - simplificationStyle = TOPLEVEL_SIMPLIFICATION_STYLE; } else if(!strcmp(optarg, "none")) { - simplificationStyle = NO_SIMPLIFICATION_STYLE; + simplificationMode = SIMPLIFICATION_MODE_NONE; } else if(!strcmp(optarg, "help")) { puts(simplificationHelp.c_str()); exit(1); @@ -479,6 +639,10 @@ throw(OptionException) { } break; + case NO_STATIC_LEARNING: + doStaticLearning = false; + break; + case INTERACTIVE: interactive = true; interactiveSetByUser = true; @@ -622,6 +786,7 @@ throw(OptionException) { printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no"); printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no"); printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); + printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no"); printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); diff --git a/src/util/options.h b/src/util/options.h index ce2bc71e7..c4e115b08 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -2,8 +2,8 @@ /*! \file options.h ** \verbatim ** Original author: mdeters - ** Major contributors: cconway - ** Minor contributors (to current version): dejan, taking + ** Major contributors: taking, cconway + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -71,11 +71,8 @@ struct CVC4_PUBLIC Options { /** The input language */ InputLanguage inputLanguage; - /** Enumeration of UF implementation choices */ - typedef enum { TIM, MORGAN } UfImplementation; - - /** Which implementation of uninterpreted function theory to use */ - UfImplementation uf_implementation; + /** The output language */ + OutputLanguage outputLanguage; /** Should we print the help message? */ bool help; @@ -112,21 +109,16 @@ struct CVC4_PUBLIC Options { /** Simplify the assertions as they come in */ SIMPLIFICATION_MODE_INCREMENTAL, /** Simplify the assertions all together once a check is requested */ - SIMPLIFICATION_MODE_BATCH + SIMPLIFICATION_MODE_BATCH, + /** Don't do simplification */ + SIMPLIFICATION_MODE_NONE } SimplificationMode; - /** When to perform nonclausal simplifications. */ + /** When/whether to perform nonclausal simplifications. */ SimplificationMode simplificationMode; - /** Enumeration of simplification styles (how much to simplify). */ - typedef enum { - AGGRESSIVE_SIMPLIFICATION_STYLE, - TOPLEVEL_SIMPLIFICATION_STYLE, - NO_SIMPLIFICATION_STYLE - } SimplificationStyle; - - /** Style of nonclausal simplifications to perform. */ - SimplificationStyle simplificationStyle; + /** Whether to perform the static learning pass. */ + bool doStaticLearning; /** Whether we're in interactive mode or not */ bool interactive; @@ -229,34 +221,18 @@ struct CVC4_PUBLIC Options { };/* struct Options */ inline std::ostream& operator<<(std::ostream& out, - Options::UfImplementation uf) CVC4_PUBLIC; - -inline std::ostream& operator<<(std::ostream& out, - Options::UfImplementation uf) { - switch(uf) { - case Options::TIM: - out << "TIM"; - break; - case Options::MORGAN: - out << "MORGAN"; - break; - default: - out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]"; - } - - return out; -} - -inline std::ostream& operator<<(std::ostream& out, Options::SimplificationMode mode) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, Options::SimplificationMode mode) { switch(mode) { + case Options::SIMPLIFICATION_MODE_INCREMENTAL: + out << "SIMPLIFICATION_MODE_INCREMENTAL"; + break; case Options::SIMPLIFICATION_MODE_BATCH: out << "SIMPLIFICATION_MODE_BATCH"; break; - case Options::SIMPLIFICATION_MODE_INCREMENTAL: - out << "SIMPLIFICATION_MODE_INCREMENTAL"; + case Options::SIMPLIFICATION_MODE_NONE: + out << "SIMPLIFICATION_MODE_NONE"; break; default: out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]"; diff --git a/src/util/output.cpp b/src/util/output.cpp index 29de4c360..3823f7be6 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -40,6 +40,8 @@ MessageC MessageChannel CVC4_PUBLIC (&cout); NoticeC NoticeChannel CVC4_PUBLIC (&cout); ChatC ChatChannel CVC4_PUBLIC (&cout); TraceC TraceChannel CVC4_PUBLIC (&cout); +std::ostream DumpC::dump_cout(cout.rdbuf());// copy cout stream buffer +DumpC DumpChannel CVC4_PUBLIC (&DumpC::dump_cout); #ifndef CVC4_MUZZLE @@ -155,6 +157,40 @@ int TraceC::printf(std::string tag, const char* fmt, ...) { # endif /* CVC4_TRACING */ +# ifdef CVC4_DUMPING + +int DumpC::printf(const char* tag, const char* fmt, ...) { + if(d_tags.find(string(tag)) == d_tags.end()) { + return 0; + } + + // chop off output after 1024 bytes + char buf[1024]; + va_list vl; + va_start(vl, fmt); + int retval = vsnprintf(buf, sizeof(buf), fmt, vl); + va_end(vl); + *d_os << buf; + return retval; +} + +int DumpC::printf(std::string tag, const char* fmt, ...) { + if(d_tags.find(tag) == d_tags.end()) { + return 0; + } + + // chop off output after 1024 bytes + char buf[1024]; + va_list vl; + va_start(vl, fmt); + int retval = vsnprintf(buf, sizeof(buf), fmt, vl); + va_end(vl); + *d_os << buf; + return retval; +} + +# endif /* CVC4_DUMPING */ + #endif /* ! CVC4_MUZZLE */ }/* CVC4 namespace */ diff --git a/src/util/output.h b/src/util/output.h index 6d0f27f2a..e096ff028 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): cconway, taking, dejan + ** Minor contributors (to current version): taking, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -190,6 +190,7 @@ public: bool on (std::string tag) { d_tags.insert(tag); return true; } bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } bool off(std::string tag) { d_tags.erase (tag); return false; } + bool off() { d_tags.clear(); return false; } bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } @@ -297,6 +298,7 @@ public: bool on (std::string tag) { d_tags.insert(tag); return true; } bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } bool off(std::string tag) { d_tags.erase (tag); return false; } + bool off() { d_tags.clear(); return false; } bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } @@ -305,6 +307,51 @@ public: std::ostream& getStream() { return *d_os; } };/* class TraceC */ +/** The dump output class */ +class CVC4_PUBLIC DumpC { + std::set<std::string> d_tags; + std::ostream* d_os; + +public: + /** + * A copy of cout for use by the dumper. This is important because + * it has different settings (e.g., the expr printing depth is always + * unlimited). */ + static std::ostream dump_cout; + + explicit DumpC(std::ostream* os) : d_os(os) {} + + int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); + int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); + + CVC4ostream operator()(const char* tag) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { + return CVC4ostream(d_os); + } else { + return CVC4ostream(); + } + } + CVC4ostream operator()(std::string tag) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + return CVC4ostream(d_os); + } else { + return CVC4ostream(); + } + } + + bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } + bool on (std::string tag) { d_tags.insert(tag); return true; } + bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } + bool off(std::string tag) { d_tags.erase (tag); return false; } + bool off() { d_tags.clear(); return false; } + + bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } + bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } + + std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& getStream() { return *d_os; } +};/* class DumpC */ + /** The debug output singleton */ extern DebugC DebugChannel CVC4_PUBLIC; /** The warning output singleton */ @@ -317,6 +364,8 @@ extern NoticeC NoticeChannel CVC4_PUBLIC; extern ChatC ChatChannel CVC4_PUBLIC; /** The trace output singleton */ extern TraceC TraceChannel CVC4_PUBLIC; +/** The dump output singleton */ +extern DumpC DumpChannel CVC4_PUBLIC; #ifdef CVC4_MUZZLE @@ -326,6 +375,7 @@ extern TraceC TraceChannel CVC4_PUBLIC; # define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel # define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel # define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel +# define Dump ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpChannel inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; } inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; } @@ -335,6 +385,8 @@ inline int NoticeC::printf(const char* fmt, ...) { return 0; } inline int ChatC::printf(const char* fmt, ...) { return 0; } inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; } inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; } +inline int DumpC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int DumpC::printf(std::string tag, const char* fmt, ...) { return 0; } #else /* CVC4_MUZZLE */ @@ -356,6 +408,13 @@ inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; } inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; } inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; } # endif /* CVC4_TRACING */ +# ifdef CVC4_DUMPING +# define Dump ::CVC4::DumpChannel +# else /* CVC4_DUMPING */ +# define Dump ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpChannel +inline int DumpC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int DumpC::printf(std::string tag, const char* fmt, ...) { return 0; } +# endif /* CVC4_DUMPING */ #endif /* CVC4_MUZZLE */ diff --git a/src/util/rational.h.in b/src/util/rational.h.in index 88c488290..17c1e31fc 100644 --- a/src/util/rational.h.in +++ b/src/util/rational.h.in @@ -11,9 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Multi-precision rational constants. + ** \brief A multi-precision rational constant ** - ** Multi-precision rational constants. + ** A multi-precision rational constant. **/ // this is used to avoid a public header dependence on cvc4autoconfig.h @@ -26,8 +26,14 @@ #ifdef CVC4_CLN_IMP # include "util/rational_cln_imp.h" +# if SWIG + %include "util/rational_cln_imp.h" +# endif /* SWIG */ #endif /* CVC4_CLN_IMP */ #ifdef CVC4_GMP_IMP # include "util/rational_gmp_imp.h" +# if SWIG + %include "util/rational_gmp_imp.h" +# endif /* SWIG */ #endif /* CVC4_GMP_IMP */ diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 057100d10..22e3a7ad1 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index b97484ff1..a883500f9 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index 5921b8fd3..b26172d66 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 167e0fc22..b97965169 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/result.cpp b/src/util/result.cpp index 8e1db27c4..8a2bcf3b2 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file result.h +/*! \file result.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/result.h b/src/util/result.h index 7da1dc0b7..c4733eab9 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 376a8a224..63ce23874 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -2,10 +2,10 @@ /*! \file sexpr.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 70d486ff6..474d8fa7a 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -2,10 +2,10 @@ /*! \file stats.cpp ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -20,6 +20,13 @@ #include "util/stats.h" #include "expr/node_manager.h" #include "expr/expr_manager_scope.h" +#include "lib/clock_gettime.h" + +#ifdef CVC4_STATISTICS_ON +# define __CVC4_USE_STATISTICS true +#else +# define __CVC4_USE_STATISTICS false +#endif using namespace CVC4; @@ -67,6 +74,24 @@ StatisticsRegistry::const_iterator StatisticsRegistry::end() { return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end(); }/* StatisticsRegistry::end() */ +void TimerStat::start() { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(!d_running); + clock_gettime(CLOCK_MONOTONIC, &d_start); + d_running = true; + } +}/* TimerStat::start() */ + +void TimerStat::stop() { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(d_running); + ::timespec end; + clock_gettime(CLOCK_MONOTONIC, &end); + d_data += end - d_start; + d_running = false; + } +}/* TimerStat::stop() */ + RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : d_em(&em), d_stat(stat) { ExprManagerScope ems(*d_em); diff --git a/src/util/stats.h b/src/util/stats.h index a94733595..7d3e33a6f 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -32,7 +32,6 @@ #include <vector> #include "util/Assert.h" -#include "lib/clock_gettime.h" namespace CVC4 { @@ -702,27 +701,13 @@ public: } /** Start the timer. */ - void start() { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(!d_running); - clock_gettime(CLOCK_MONOTONIC, &d_start); - d_running = true; - } - } + void start(); /** * Stop the timer and update the statistic value with the * accumulated time. */ - void stop() { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_running); - ::timespec end; - clock_gettime(CLOCK_MONOTONIC, &end); - d_data += end - d_start; - d_running = false; - } - } + void stop(); };/* class TimerStat */ diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp index 61c48fa8d..5d772b576 100644 --- a/src/util/trans_closure.cpp +++ b/src/util/trans_closure.cpp @@ -2,10 +2,10 @@ /*! \file trans_closure.cpp ** \verbatim ** Original author: barrett - ** Major contributors: none + ** Major contributors: ajreynol ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h index 951a32a63..ef04d7af5 100644 --- a/src/util/trans_closure.h +++ b/src/util/trans_closure.h @@ -2,8 +2,8 @@ /*! \file trans_closure.h ** \verbatim ** Original author: barrett - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: ajreynol + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences |