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 | |
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')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 18 | ||||
-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 | ||||
-rw-r--r-- | src/util/configuration_private.h | 2 |
21 files changed, 273 insertions, 121 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 18ed9b5da..28a90d741 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -197,13 +197,13 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) } else { // Lemma vec<Lit> assigned_lits; - Debug("minisat::lemmas") << "Asserting lemma with " << ps.size() << " literals." << endl; + Debug("minisat::lemmas") << "Asserting lemma with " << ps.size() << " literals." << std::endl; bool lemmaSatisfied = false; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { if (ps[i] == ~p) { // We don't add clauses that represent splits directly, they are decision literals // so they will get decided upon and sent to the theory - Debug("minisat::lemmas") << "Lemma is a tautology." << endl; + Debug("minisat::lemmas") << "Lemma is a tautology." << std::endl; return true; } if (value(ps[i]) == l_Undef) { @@ -216,7 +216,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) p = ps[i]; if (value(p) == l_True) lemmaSatisfied = true; assigned_lits.push(p); - Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << endl; + Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << std::endl; } } Assert(j >= 1 || lemmaSatisfied, "You are asserting a falsified lemma, produce a conflict instead!"); @@ -232,7 +232,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) } } if (value(ps[1]) != l_Undef && max_level != -1) { - swap(ps[1], ps[max_level_j]); + std::swap(ps[1], ps[max_level_j]); } ps.shrink(i - j); } @@ -249,7 +249,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) clauses.push(cr); attachClause(cr); if (propagate_first_literal) { - Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << endl; + Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << std::endl; lemma_propagated_literals.push(ps[0]); lemma_propagated_reasons.push(cr); propagating_lemmas.push(cr); @@ -915,11 +915,11 @@ lbool Solver::search(int nof_conflicts) // If we have more assertions from lemmas, we continue if (problem_extended) { - Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << endl; + Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << std::endl; for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) { if (value(var(lemma_propagated_literals[i])) == l_Undef) { - Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl; + Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << std::endl; uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]); } } @@ -1080,7 +1080,7 @@ static double luby(double y, int x){ // NOTE: assumptions passed in member-variable 'assumptions'. lbool Solver::solve_() { - Debug("minisat") << "nvars = " << nVars() << endl; + Debug("minisat") << "nvars = " << nVars() << std::endl; in_solve = true; @@ -1123,7 +1123,7 @@ lbool Solver::solve_() model.growTo(nVars()); for (int i = 0; i < nVars(); i++) { model[i] = value(i); - Debug("minisat") << i << " = " << model[i] << endl; + Debug("minisat") << i << " = " << model[i] << std::endl; } }else if (status == l_False && conflict.size() == 0) ok = false; 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 */ diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index 27b019378..56423e7d5 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -20,8 +20,6 @@ #ifndef __CVC4__CONFIGURATION_PRIVATE_H #define __CVC4__CONFIGURATION_PRIVATE_H -using namespace std; - namespace CVC4 { #ifdef CVC4_DEBUG |