Fix errors and reduce warnings on clang (merge from mdeters/clang)

diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
index 6c8e5de46d2799ac02d70e50bac87414ff04221d..49b0b54a7e840fff6d75c239885a397e97f82e7e 100755 (executable)
--- a/contrib/get-antlr-3.4
+++ b/contrib/get-antlr-3.4
@@ -49,10 +49,10 @@ cd libantlr3c-3.4
 
 if [ ${MACHINE_TYPE} == 'x86_64' ]; then
   # 64-bit stuff here
-  ./configure --enable-64bit --disable-antlrdebug --prefix=`pwd`/../.. $ANTLR_CONFIGURE_ARGS
+  ./configure --enable-64bit --disable-shared --disable-antlrdebug --prefix=`pwd`/../.. $ANTLR_CONFIGURE_ARGS
 else
   # 32-bit stuff here
-  ./configure --disable-antlrdebug --prefix=`pwd`/../.. $ANTLR_CONFIGURE_ARGS
+  ./configure --disable-shared --disable-antlrdebug --prefix=`pwd`/../.. $ANTLR_CONFIGURE_ARGS
 fi
 
 cp Makefile Makefile.orig

diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index a085161bcf9f400649d7aca0672bb497c9091cb7..9a14caec5f586dc07b9e80248f014994b9150b2d 100644 (file)
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -752,7 +752,7 @@ public:
                      table_value_type table_value_type;
     typedef attr::AttributeTraits<table_value_type, context_dep> traits;
     uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
-    Assert(traits::cleanup.size() == id);// sanity check
+    //Assert(traits::cleanup.size() == id);// sanity check
     traits::cleanup.push_back(attr::getCleanupStrategy<value_t,
                                                        CleanupStrategy>::fn);
     return id;

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index b9cae94316606267a59dcecb32139c6c5c018177..09018cbfd73fdeb1a9c1cbb981ce15bc7234f38f 100644 (file)
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -43,7 +43,7 @@ class SmtEngine;
 class NodeManager;
 class Options;
 class IntStat;
-class ExprManagerMapCollection;
+struct ExprManagerMapCollection;
 class StatisticsRegistry;
 
 namespace expr {

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 442d29ac9781203206da2d328a519990ddf2efaf..b353ec5dc59570a56e6c383e788603a27a256899 100644 (file)
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -67,7 +67,7 @@ namespace prop {
   class TheoryProxy;
 }/* CVC4::prop namespace */
 
-class ExprManagerMapCollection;
+struct ExprManagerMapCollection;
 
 struct ExprHashFunction;
 

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 47504b0e4a5ee6aac7faf517d9fdf7a177afc59c..0cab4e628cc3894ed31ee4fafdddc4a2b0f7f231 100644 (file)
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -27,7 +27,7 @@
 namespace CVC4 {
 namespace kind {
 
-enum Kind_t {
+enum CVC4_PUBLIC Kind_t {
   UNDEFINED_KIND = -1, /**< undefined */
   NULL_EXPR, /**< Null kind */
 ${kind_decls}

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index cc52b11b99d3bbbce0b6014391134fb9e3900dfd..4e95c0fe20b17ac5ec149d69f98c604fa4165ae7 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -204,111 +204,48 @@ bool Type::isBoolean() const {
   return d_typeNode->isBoolean();
 }
 
-/** Cast to a Boolean type */
-Type::operator BooleanType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isBoolean(), this);
-  return BooleanType(*this);
-}
-
 /** Is this the integer type? */
 bool Type::isInteger() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isInteger();
 }
 
-/** Cast to a integer type */
-Type::operator IntegerType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isInteger(), this);
-  return IntegerType(*this);
-}
-
 /** Is this the real type? */
 bool Type::isReal() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isReal();
 }
 
-/** Cast to a real type */
-Type::operator RealType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isReal(), this);
-  return RealType(*this);
-}
-
 /** Is this the string type? */
 bool Type::isString() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isString();
 }
 
-/** Cast to a string type */
-Type::operator StringType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isString(), this);
-  return StringType(*this);
-}
-
 /** Is this the bit-vector type? */
 bool Type::isBitVector() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isBitVector();
 }
 
-/** Cast to a bit-vector type */
-Type::operator BitVectorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isBitVector(), this);
-  return BitVectorType(*this);
-}
-
-/** Cast to a Constructor type */
-Type::operator DatatypeType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isDatatype(), this);
-  return DatatypeType(*this);
-}
-
 /** Is this a datatype type? */
 bool Type::isDatatype() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype();
 }
 
-/** Cast to a Constructor type */
-Type::operator ConstructorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isConstructor(), this);
-  return ConstructorType(*this);
-}
-
 /** Is this the Constructor type? */
 bool Type::isConstructor() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isConstructor();
 }
 
-/** Cast to a Selector type */
-Type::operator SelectorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSelector(), this);
-  return SelectorType(*this);
-}
-
 /** Is this the Selector type? */
 bool Type::isSelector() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSelector();
 }
 
-/** Cast to a Tester type */
-Type::operator TesterType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isTester(), this);
-  return TesterType(*this);
-}
-
 /** Is this the Tester type? */
 bool Type::isTester() const {
   NodeManagerScope nms(d_nodeManager);
@@ -330,64 +267,30 @@ bool Type::isPredicate() const {
   return d_typeNode->isPredicate();
 }
 
-/** Cast to a function type */
-Type::operator FunctionType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isFunction(), this);
-  return FunctionType(*this);
-}
-
 /** Is this a tuple type? */
 bool Type::isTuple() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isTuple();
 }
 
-/** Cast to a tuple type */
-Type::operator TupleType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isTuple(), this);
-  return TupleType(*this);
-}
-
 /** Is this a record type? */
 bool Type::isRecord() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isRecord();
 }
 
-/** Cast to a record type */
-Type::operator RecordType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isRecord(), this);
-  return RecordType(*this);
-}
-
 /** Is this a symbolic expression type? */
 bool Type::isSExpr() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSExpr();
 }
 
-/** Cast to a symbolic expression type */
-Type::operator SExprType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSExpr(), this);
-  return SExprType(*this);
-}
-
 /** Is this an array type? */
 bool Type::isArray() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isArray();
 }
 
-/** Cast to an array type */
-Type::operator ArrayType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  return ArrayType(*this);
-}
-
 /** Is this a sort kind */
 bool Type::isSort() const {
   NodeManagerScope nms(d_nodeManager);
@@ -395,25 +298,11 @@ bool Type::isSort() const {
 }
 
 /** Cast to a sort type */
-Type::operator SortType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSort(), this);
-  return SortType(*this);
-}
-
-/** Is this a sort constructor kind */
 bool Type::isSortConstructor() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSortConstructor();
 }
 
-/** Cast to a sort constructor type */
-Type::operator SortConstructorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSortConstructor(), this);
-  return SortConstructorType(*this);
-}
-
 /** Is this a predicate subtype */
 /* - not in release 1.0
 bool Type::isPredicateSubtype() const {
@@ -422,28 +311,12 @@ bool Type::isPredicateSubtype() const {
 }
 */
 
-/** Cast to a predicate subtype */
-/* - not in release 1.0
-Type::operator PredicateSubtype() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isPredicateSubtype(), this);
-  return PredicateSubtype(*this);
-}
-*/
-
 /** Is this an integer subrange */
 bool Type::isSubrange() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSubrange();
 }
 
-/** Cast to a predicate subtype */
-Type::operator SubrangeType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSubrange(), this);
-  return SubrangeType(*this);
-}
-
 vector<Type> FunctionType::getArgTypes() const {
   NodeManagerScope nms(d_nodeManager);
   vector<Type> args;

diff --git a/src/expr/type.h b/src/expr/type.h
index 4223d71ab5c513b87c2e7a2544dcbff941dfaa88..ce6291cd82b77430094cab7fa4c88ddd85f87ed2 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -30,15 +30,15 @@
 namespace CVC4 {
 
 class NodeManager;
-class ExprManager;
-class Expr;
+class CVC4_PUBLIC ExprManager;
+class CVC4_PUBLIC Expr;
 class TypeNode;
-class ExprManagerMapCollection;
+struct CVC4_PUBLIC ExprManagerMapCollection;
 
-class SmtEngine;
+class CVC4_PUBLIC SmtEngine;
 
-class Datatype;
-class Record;
+class CVC4_PUBLIC Datatype;
+class CVC4_PUBLIC Record;
 
 template <bool ref_count>
 class NodeTemplate;
@@ -239,60 +239,30 @@ public:
    */
   bool isBoolean() const;
 
-  /**
-   * Cast this type to a Boolean type
-   * @return the BooleanType
-   */
-  operator BooleanType() const throw(IllegalArgumentException);
-
   /**
    * Is this the integer type?
    * @return true if the type is a integer type
    */
   bool isInteger() const;
 
-  /**
-   * Cast this type to a integer type
-   * @return the IntegerType
-   */
-  operator IntegerType() const throw(IllegalArgumentException);
-
   /**
    * Is this the real type?
    * @return true if the type is a real type
    */
   bool isReal() const;
 
-  /**
-   * Cast this type to a real type
-   * @return the RealType
-   */
-  operator RealType() const throw(IllegalArgumentException);
-
   /**
    * Is this the string type?
    * @return true if the type is the string type
    */
   bool isString() const;
 
-  /**
-   * Cast this type to a string type
-   * @return the StringType
-   */
-  operator StringType() const throw(IllegalArgumentException);
-
   /**
    * Is this the bit-vector type?
    * @return true if the type is a bit-vector type
    */
   bool isBitVector() const;
 
-  /**
-   * Cast this type to a bit-vector type
-   * @return the BitVectorType
-   */
-  operator BitVectorType() const throw(IllegalArgumentException);
-
   /**
    * Is this a function type?
    * @return true if the type is a function type
@@ -306,132 +276,66 @@ public:
    */
   bool isPredicate() const;
 
-  /**
-   * Cast this type to a function type
-   * @return the FunctionType
-   */
-  operator FunctionType() const throw(IllegalArgumentException);
-
   /**
    * Is this a tuple type?
    * @return true if the type is a tuple type
    */
   bool isTuple() const;
 
-  /**
-   * Cast this type to a tuple type
-   * @return the TupleType
-   */
-  operator TupleType() const throw(IllegalArgumentException);
-
   /**
    * Is this a record type?
    * @return true if the type is a record type
    */
   bool isRecord() const;
 
-  /**
-   * Cast this type to a record type
-   * @return the RecordType
-   */
-  operator RecordType() const throw(IllegalArgumentException);
-
   /**
    * Is this a symbolic expression type?
    * @return true if the type is a symbolic expression type
    */
   bool isSExpr() const;
 
-  /**
-   * Cast this type to a symbolic expression type
-   * @return the SExprType
-   */
-  operator SExprType() const throw(IllegalArgumentException);
-
   /**
    * Is this an array type?
    * @return true if the type is a array type
    */
   bool isArray() const;
 
-  /**
-   * Cast this type to an array type
-   * @return the ArrayType
-   */
-  operator ArrayType() const throw(IllegalArgumentException);
-
   /**
    * Is this a datatype type?
    * @return true if the type is a datatype type
    */
   bool isDatatype() const;
 
-  /**
-   * Cast this type to a datatype type
-   * @return the DatatypeType
-   */
-  operator DatatypeType() const throw(IllegalArgumentException);
-
   /**
    * Is this a constructor type?
    * @return true if the type is a constructor type
    */
   bool isConstructor() const;
 
-  /**
-   * Cast this type to a constructor type
-   * @return the ConstructorType
-   */
-  operator ConstructorType() const throw(IllegalArgumentException);
-
   /**
    * Is this a selector type?
    * @return true if the type is a selector type
    */
   bool isSelector() const;
 
-  /**
-   * Cast this type to a selector type
-   * @return the SelectorType
-   */
-  operator SelectorType() const throw(IllegalArgumentException);
-
   /**
    * Is this a tester type?
    * @return true if the type is a tester type
    */
   bool isTester() const;
 
-  /**
-   * Cast this type to a tester type
-   * @return the TesterType
-   */
-  operator TesterType() const throw(IllegalArgumentException);
-
   /**
    * Is this a sort kind?
    * @return true if this is a sort kind
    */
   bool isSort() const;
 
-  /**
-   * Cast this type to a sort type
-   * @return the sort type
-   */
-  operator SortType() const throw(IllegalArgumentException);
-
   /**
    * Is this a sort constructor kind?
    * @return true if this is a sort constructor kind
    */
   bool isSortConstructor() const;
 
-  /**
-   * Cast this type to a sort constructor type
-   * @return the sort constructor type
-   */
-  operator SortConstructorType() const throw(IllegalArgumentException);
-
   /**
    * Is this a predicate subtype?
    * @return true if this is a predicate subtype
@@ -439,25 +343,12 @@ public:
   // not in release 1.0
   //bool isPredicateSubtype() const;
 
-  /**
-   * Cast this type to a predicate subtype
-   * @return the predicate subtype
-   */
-  // not in release 1.0
-  //operator PredicateSubtype() const throw(IllegalArgumentException);
-
   /**
    * Is this an integer subrange type?
    * @return true if this is an integer subrange type
    */
   bool isSubrange() const;
 
-  /**
-   * Cast this type to an integer subrange type
-   * @return the integer subrange type
-   */
-  operator SubrangeType() const throw(IllegalArgumentException);
-
   /**
    * Outputs a string representation of this type to the stream.
    * @param out the stream to output to

diff --git a/src/options/options.h b/src/options/options.h
index 2d49765f30fe126e2bd2a7693334f112c960cf09..5f17f5a5cfb009aa817668c411b78570664b48bb 100644 (file)
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -31,7 +31,7 @@
 namespace CVC4 {
 
 namespace options {
-  class OptionsHolder;
+  struct OptionsHolder;
 }/* CVC4::options namespace */
 
 class ExprStream;

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index d05fe24a7b5988ffdd5ef07234e9579a7d3e4526..c1351c6a2fa264cda7509c5ea028a3765928e9f2 100644 (file)
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -26,7 +26,7 @@ namespace CVC4 {
 bool          ProofManager::isInitialized = false;
 ProofManager* ProofManager::proofManager = NULL;
 
-ProofManager::ProofManager(ProofFormat format = LFSC):
+ProofManager::ProofManager(ProofFormat format):
   d_satProof(NULL),
   d_cnfProof(NULL),
   d_format(format)

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 3bfff14567965a9b228f70c68cc07cecf321305d..91eb2ed994cab776a9ee70329f604bca4ed814ae 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -52,7 +52,7 @@ class ProofManager {
   
   static ProofManager* proofManager; 
   static bool isInitialized; 
-  ProofManager(ProofFormat format);
+  ProofManager(ProofFormat format = LFSC);
 public:
   static ProofManager* currentPM();
 

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 978ac8d7b85d20c9ea9b392469088af94068473a..68969c78b7d6560ced50217435b38b5eab0f9e72 100644 (file)
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "theory/interrupted.h"
 using namespace BVMinisat;
 
-namespace CVC4 {
+namespace BVMinisat {
 
 #define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] "
 

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index e5d876b487f27ef24b00c44e80462584a1ee10ae..b4807b021d3013c4c4c681b34e6b399b80e9085e 100644 (file)
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -130,8 +130,6 @@ public:
 
 };/* class DPLLSatSolverInterface */
 
-}/* CVC4::prop namespace */
-
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
   out << lit.toString();
   return out;
@@ -167,6 +165,7 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
   return out;
 }
 
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROP__SAT_MODULE_H */

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3edcd687205a3789b4d6c81e431bcf84df40ff11..cdae68d96c57162fc8f3123a7043e1f1bc8b42d7 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -47,7 +47,7 @@ namespace CVC4 {
 template <bool ref_count> class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
-class NodeHashFunction;
+struct NodeHashFunction;
 
 class Command;
 class GetModelCommand;
@@ -77,7 +77,7 @@ namespace smt {
    */
   class DefinedFunction;
 
-  class SmtEngineStatistics;
+  struct SmtEngineStatistics;
   class SmtEnginePrivate;
   class SmtScope;
   class BooleanTermConverter;

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 9a41d8d2395d391871c779fceaae57c2422257b9..fdb4a8ffac3fa6eeab6b802c07e3824c0fccd919 100644 (file)
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -225,7 +225,7 @@ private:
   bool equalSizes();
 
   bool inMaps(ArithVar x) const{
-    return 0 <= x && x < d_mapSize;
+    return x < d_mapSize;
   }
 
 };/* class ArithPartialModel */

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 23cd8381dd2d5a237816f241083d5cf9f499166e..8bcc644146cbbc9c022d187f708a2c8e1d382709 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -430,10 +430,6 @@ Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
 template<> inline
 bool RewriteRule<XorNot>::applies(TNode node) {
   Unreachable();
-  if (node.getKind() == kind::BITVECTOR_XOR &&
-      node.getNumChildren() == 2 &&
-          node[0].getKind() == kind::BITVECTOR_NOT &&
-          node[1].getKind() == kind::BITVECTOR_NOT); 
 }
 
 template<> inline

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 3d98674a883c7612270b305e26012ad633f7b248..8272ce168a340fcb3f23dc74bed80393c434d882 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -42,10 +42,6 @@ void FirstOrderModel::reset(){
   TheoryModel::reset();
 }
 
-void FirstOrderModel::addTerm( Node n ){
-  TheoryModel::addTerm( n );
-}
-
 void FirstOrderModel::initialize( bool considerAxioms ){
   //rebuild models
   d_uf_model_tree.clear();

diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 3779579fdbdfbddd964a8ab136e453bf04270079..50a94196857beb7ec19a9eaa8e911909e0bcfc6a 100644 (file)
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -33,8 +33,6 @@ class TermDb;
 class FirstOrderModel : public TheoryModel
 {
 private:
-  //add term function
-  void addTerm( Node n );
   //for initialize model
   void initializeModelForTerm( Node n );
   /** whether an axiom is asserted */

diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index c6fd9611c0e0e3d8224379738d4f3291750398d6..a82b94f7347bcddeb311cc4fb9f7cc80a2982091 100644 (file)
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -276,7 +276,7 @@ void TheoryRewriteRules::check(Effort level) {
       if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE)
         continue;
       // If it has a value it should already has been notified
-      bool value; value = value; // avoiding the warning in non debug mode
+      bool value CVC4_UNUSED;
       Assert(!getValuation().hasSatValue(g,value));
       Debug("rewriterules::check") << "RewriteRules::Check Narrowing on:" << g << std::endl;
       /** Can split on already rewritten instrule... but... */

diff --git a/src/theory/theory.h b/src/theory/theory.h
index e76441f6b3cef0919db8720eab76c88177819aa0..5b20324303938ff0bf9d1fc62df6ca022c0302c7 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -50,13 +50,13 @@ namespace theory {
 class QuantifiersEngine;
 class TheoryModel;
 
-namespace rrinst{
-class CandidateGenerator;
-}
+namespace rrinst {
+  class CandidateGenerator;
+}/* CVC4::theory::rrinst namespace */
 
 namespace eq {
-class EqualityEngine;
-}
+  class EqualityEngine;
+}/* CVC4::theory::eq namespace */
 
 /**
  * Information about an assertion for the theories.
@@ -787,14 +787,10 @@ public:
   std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
 };/* class Theory */
 
-std::ostream& operator<<(std::ostream& os, Theory::Effort level);
-
-namespace eq{
-  class EqualityEngine;
-}
-
+std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
+inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a);
 
-inline Assertion Theory::get() {
+inline theory::Assertion Theory::get() {
   Assert( !done(), "Theory::get() called with assertion queue empty!" );
 
   // Get the assertion
@@ -810,7 +806,9 @@ inline Assertion Theory::get() {
   return fact;
 }
 
-}/* CVC4::theory namespace */
+inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a) {
+  return out << a.assertion;
+}
 
 inline std::ostream& operator<<(std::ostream& out,
                                 const CVC4::theory::Theory& theory) {
@@ -831,6 +829,7 @@ inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertSta
   return out;
 }
 
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__THEORY_H */

diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h
index e444ba6e27093f5e633650b267afc1ef983361ec..4c8e646bd71e7b86f08135cd0a8df12060d1f4b2 100644 (file)
--- a/src/util/node_visitor.h
+++ b/src/util/node_visitor.h
@@ -36,10 +36,11 @@ class NodeVisitor {
   /**
    * Guard against NodeVisitor<> being re-entrant.
    */
+  template <class T>
   class GuardReentry {
-    bool& d_guard;
+    T& d_guard;
   public:
-    GuardReentry(bool& guard)
+    GuardReentry(T& guard)
     : d_guard(guard) {
       Assert(!d_guard);
       d_guard = true;
@@ -71,7 +72,7 @@ public:
    */
   static typename Visitor::return_type run(Visitor& visitor, TNode node) {
 
-    GuardReentry guard(bool(s_inRun));
+    GuardReentry<CVC4_THREADLOCAL_TYPE(bool)> guard(s_inRun);
 
     // Notify of a start
     visitor.start(node);

diff --git a/src/util/record.h b/src/util/record.h
index 2c15d30e013a2fe000f8170bb92f657ad0e22b34..27b090e1dce3163864424575f04209107769e2d3 100644 (file)
--- a/src/util/record.h
+++ b/src/util/record.h
@@ -29,7 +29,7 @@
 
 namespace CVC4 {
 
-class Record;
+class CVC4_PUBLIC Record;
 
 // operators for record select and update
 

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 0a5450b8ae09397e235983f4e9545ec81bdbfba7..9aca3cb5abcc2f895bea93ac79f0ba4f56cebc9f 100644 (file)
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -42,6 +42,8 @@ namespace CVC4 {
 class ExprManager;
 class SmtEngine;
 
+inline std::ostream& operator<<(std::ostream& os, const timespec& t);
+
 /**
  * The base class for all statistics.
  *