diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-02-26 22:19:47 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-02-26 22:19:47 +0000 |
commit | 3548c7e5f6afed4e07bf9a70f0403952c9262519 (patch) | |
tree | 18f5ae49fe1ecdc9f3254074df0990dc1930fbf2 /src/theory | |
parent | edf6aaa87da179948e6b233d16fa37d2aea58bbb (diff) |
Commit to fix bug 241 (improper "using namespace std" in a header). This caused a number of latent errors in sources and headers to come up. Those are now fixed (by adding "using" or "std::" depending on the context). Took the opportunity to bring many rewriter sources in line with coding conventions.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 23 | ||||
-rw-r--r-- | src/theory/arith/row_vector.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/row_vector.h | 4 | ||||
-rw-r--r-- | src/theory/arith/tableau.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 41 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 26 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.h | 41 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 27 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.h | 39 | ||||
-rw-r--r-- | src/theory/bv/cd_set_collection.h | 2 | ||||
-rw-r--r-- | src/theory/bv/slice_manager.h | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_core.h | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 24 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 41 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 26 | ||||
-rw-r--r-- | src/theory/uf/morgan/union_find.h | 16 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 39 |
19 files changed, 264 insertions, 110 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 75216dac6..cc80e2dd8 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -2,10 +2,10 @@ /*! \file arith_rewriter.cpp ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: dejan ** 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 @@ -17,7 +17,6 @@ ** \todo document this file **/ - #include "theory/theory.h" #include "theory/arith/normal_form.h" #include "theory/arith/arith_rewriter.h" diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index e161bd8d6..3a8fc191a 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -2,10 +2,10 @@ /*! \file arith_rewriter.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters + ** Major contributors: mdeters, dejan ** 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,6 +17,11 @@ ** \todo document this file **/ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__ARITH_REWRITER_H +#define __CVC4__THEORY__ARITH__ARITH_REWRITER_H + #include "theory/theory.h" #include "theory/arith/arith_constants.h" #include "theory/arith/arith_utilities.h" @@ -24,9 +29,6 @@ #include "theory/rewriter.h" -#ifndef __CVC4__THEORY__ARITH__REWRITER_H -#define __CVC4__THEORY__ARITH__REWRITER_H - namespace CVC4 { namespace theory { namespace arith { @@ -88,11 +90,10 @@ private: return !isAtom(n); } -}; - +};/* class ArithRewriter */ -}; /* namesapce rewrite */ -}; /* namespace theory */ -}; /* namespace CVC4 */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__REWRITER_H */ +#endif /* __CVC4__THEORY__ARITH__ARITH_REWRITER_H */ diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp index 2463adf47..0dc483126 100644 --- a/src/theory/arith/row_vector.cpp +++ b/src/theory/arith/row_vector.cpp @@ -3,7 +3,9 @@ using namespace CVC4; using namespace CVC4::theory; -using namespace CVC4::theory::arith ; +using namespace CVC4::theory::arith; + +using namespace std; bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) { if(arr.size() >= 2){ diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h index 29b79ddd5..bed33349d 100644 --- a/src/theory/arith/row_vector.h +++ b/src/theory/arith/row_vector.h @@ -85,7 +85,7 @@ protected: std::vector<ArithVarSet>& d_columnMatrix; NonZeroIterator lower_bound(ArithVar x_j) const{ - return std::lower_bound(d_entries.begin(), d_entries.end(), make_pair(x_j,0), cmp); + return std::lower_bound(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp); } typedef VarCoeffArray::iterator iterator; @@ -120,7 +120,7 @@ public: private: /** Debugging code. */ bool hasInEntries(ArithVar x_j) const { - return std::binary_search(d_entries.begin(), d_entries.end(), make_pair(x_j,0), cmp); + return std::binary_search(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp); } public: diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index ebf7dbee8..a85765303 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -24,6 +24,8 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; +using namespace std; + Tableau::~Tableau(){ while(!d_basicVariables.empty()){ ArithVar curr = *(d_basicVariables.begin()); diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 103707601..33a6233bc 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -1,12 +1,26 @@ -/* - * theory_arrays_rewriter.h - * - * Created on: Dec 21, 2010 - * Author: dejan - */ - -#pragma once - +/********************* */ +/*! \file theory_arrays_rewriter.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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_private.h" + +#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H +#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H #include "theory/rewriter.h" @@ -29,9 +43,10 @@ public: static inline void init() {} static inline void shutdown() {} -}; +};/* class TheoryArraysRewriter */ -} -} -} +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ +#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */ diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index a62bc6fa0..c1be3b906 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_bool_rewriter.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 <algorithm> #include "theory/booleans/theory_bool_rewriter.h" @@ -66,7 +85,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { return RewriteResponse(REWRITE_DONE, n); } -} -} -} - +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index 62eed9e2b..4a23249d4 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -1,11 +1,26 @@ -/* - * theory_bool_rewriter.h - * - * Created on: Dec 21, 2010 - * Author: dejan - */ - -#pragma once +/********************* */ +/*! \file theory_bool_rewriter.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H +#define __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H #include "theory/rewriter.h" @@ -25,8 +40,10 @@ public: static void init() {} static void shutdown() {} -}; +};/* class TheoryBoolRewriter */ + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -} -} -} +#endif /* __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */ diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 05f7891d6..b71d66c03 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -1,5 +1,26 @@ +/********************* */ +/*! \file theory_builtin_rewriter.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "theory/builtin/theory_builtin_rewriter.h" +using namespace std; + namespace CVC4 { namespace theory { namespace builtin { @@ -30,6 +51,6 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) { return out; } -} -} -} +}/* CVC4::theory::builtin namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 7da4289b1..d50397598 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -1,11 +1,26 @@ -/* - * theory_builtin_rewriter.h - * - * Created on: Dec 21, 2010 - * Author: dejan - */ +/********************* */ +/*! \file theory_builtin_rewriter.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 + **/ -#pragma once +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H +#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H #include "theory/rewriter.h" #include "theory/theory.h" @@ -41,8 +56,10 @@ public: static inline void init() {} static inline void shutdown() {} -}; +};/* class TheoryBuiltinRewriter */ + +}/* CVC4::theory::builtin namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -} -} -} +#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */ diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h index bd26a3595..33648660b 100644 --- a/src/theory/bv/cd_set_collection.h +++ b/src/theory/bv/cd_set_collection.h @@ -306,7 +306,7 @@ public: * String representation of a set. */ std::string toString(reference_type set) { - stringstream out; + std::stringstream out; print(out, set); return out.str(); } diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h index 436ebaec0..8fc1e0b9d 100644 --- a/src/theory/bv/slice_manager.h +++ b/src/theory/bv/slice_manager.h @@ -328,7 +328,7 @@ bool SliceManager<TheoryBitvector>::isSliced(TNode node) const { template <class TheoryBitvector> inline void SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>& sliced) { - Debug("slicing") << "SliceManager::slice(" << node << ")" << endl; + Debug("slicing") << "SliceManager::slice(" << node << ")" << std::endl; Assert(!isSliced(node)); @@ -343,7 +343,7 @@ inline void SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>& // Get the base term slice set set_collection::reference_type nodeSliceSet = d_nodeSlicing[nodeBase]; - Debug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << endl; + Debug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << std::endl; std::vector<size_t> slicePoints; d_setCollection.getElements(nodeSliceSet, low + 1, high - 1, slicePoints); diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index b600bc8f1..e183a592c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -27,6 +27,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::bv; using namespace CVC4::theory::bv::utils; +using namespace std; + void TheoryBV::preRegisterTerm(TNode node) { Debug("bitvector") << "TheoryBV::preRegister(" << node << ")" << std::endl; diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index e75f53711..7cfb46835 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -34,7 +34,7 @@ bool RewriteRule<ConcatFlatten>::applies(Node node) { template<> Node RewriteRule<ConcatFlatten>::apply(Node node) { NodeBuilder<> result(kind::BITVECTOR_CONCAT); - vector<Node> processing_stack; + std::vector<Node> processing_stack; processing_stack.push_back(node); while (!processing_stack.empty()) { Node current = processing_stack.back(); @@ -57,7 +57,7 @@ bool RewriteRule<ConcatExtractMerge>::applies(Node node) { template<> Node RewriteRule<ConcatExtractMerge>::apply(Node node) { - vector<Node> mergedExtracts; + std::vector<Node> mergedExtracts; Node current = node[0]; bool mergeStarted = false; @@ -115,7 +115,7 @@ bool RewriteRule<ConcatConstantMerge>::applies(Node node) { template<> Node RewriteRule<ConcatConstantMerge>::apply(Node node) { - vector<Node> mergedConstants; + std::vector<Node> mergedConstants; for (unsigned i = 0, end = node.getNumChildren(); i < end;) { if (node[i].getKind() != kind::CONST_BITVECTOR) { // If not a constant, just add it @@ -187,7 +187,7 @@ Node RewriteRule<ExtractConcat>::apply(Node node) { int extract_high = utils::getExtractHigh(node); int extract_low = utils::getExtractLow(node); - vector<Node> resultChildren; + std::vector<Node> resultChildren; Node concat = node[0]; for (int i = concat.getNumChildren() - 1; i >= 0 && extract_high >= 0; i--) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 08245afcb..9b545d25a 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -1,9 +1,21 @@ -/* - * theory_bv_rewriter.cpp - * - * Created on: Dec 21, 2010 - * Author: dejan - */ +/********************* */ +/*! \file theory_bv_rewriter.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "theory/theory.h" #include "theory/bv/theory_bv_rewriter.h" diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 437ac49d3..bdf1c8d51 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -1,11 +1,26 @@ -/* - * theory_bv_rewriter.h - * - * Created on: Dec 21, 2010 - * Author: dejan - */ - -#pragma once +/********************* */ +/*! \file theory_bv_rewriter.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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_private.h" + +#ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H +#define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H #include "theory/rewriter.h" @@ -29,8 +44,10 @@ public: static void init(); static void shutdown(); -}; +};/* class TheoryBVRewriter */ + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -} -} -} +#endif /* __CVC4__THEORY__BV__THEORY_BV_REWRITER_H */ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index fe7ad7a9a..e896f9058 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -1,14 +1,28 @@ -/* - * rewriter.cpp - * - * Created on: Dec 13, 2010 - * Author: dejan - */ +/********************* */ +/*! \file rewriter.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "theory/theory.h" #include "theory/rewriter.h" #include "theory/rewriter_tables.h" +using namespace std; + namespace CVC4 { namespace theory { diff --git a/src/theory/uf/morgan/union_find.h b/src/theory/uf/morgan/union_find.h index c378e5a8b..794d7452c 100644 --- a/src/theory/uf/morgan/union_find.h +++ b/src/theory/uf/morgan/union_find.h @@ -105,23 +105,23 @@ inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const { template <class NodeType, class NodeHash> inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) { - Trace("ufuf") << "UFUF find of " << n << endl; + Trace("ufuf") << "UFUF find of " << n << std::endl; typename MapType::iterator i = d_map.find(n); if(i == d_map.end()) { - Trace("ufuf") << "UFUF it is rep" << endl; + Trace("ufuf") << "UFUF it is rep" << std::endl; return n; } else { - Trace("ufuf") << "UFUF not rep: par is " << (*i).second << endl; - pair<TNode, TNode> pr = *i; + Trace("ufuf") << "UFUF not rep: par is " << (*i).second << std::endl; + std::pair<TNode, TNode> pr = *i; // our iterator is invalidated by the recursive call to find(), // since it mutates the map TNode p = find(pr.second); if(p == pr.second) { return p; } - d_trace.push_back(make_pair(n, pr.second)); + d_trace.push_back(std::make_pair(n, pr.second)); d_offset = d_trace.size(); - Trace("ufuf") << "UFUF setting canon of " << n << " : " << p << " @ " << d_trace.size() << endl; + Trace("ufuf") << "UFUF setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl; pr.second = p; d_map.insert(pr); return p; @@ -133,9 +133,9 @@ inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) { Assert(d_map.find(n) == d_map.end()); Assert(d_map.find(newParent) == d_map.end()); if(n != newParent) { - Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << endl; + Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl; d_map[n] = newParent; - d_trace.push_back(make_pair(n, TNode::null())); + d_trace.push_back(std::make_pair(n, TNode::null())); d_offset = d_trace.size(); } } diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index e71f74fea..744a3d966 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -1,11 +1,26 @@ -/* - * theory_uf_rewriter.h - * - * Created on: Dec 21, 2010 - * Author: dejan - */ +/********************* */ +/*! \file theory_uf_rewriter.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 + **/ -#pragma once +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__THEORY_UF_REWRITER_H +#define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H #include "theory/rewriter.h" @@ -42,8 +57,10 @@ public: static inline void init() {} static inline void shutdown() {} -}; +};/* class TheoryUfRewriter */ + +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -} -} -} +#endif /* __CVC4__THEORY__UF__THEORY_UF_REWRITER_H */ |