diff options
22 files changed, 380 insertions, 206 deletions
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 5cf543459..db3ac47da 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -2,7 +2,7 @@ # # update-copyright.pl # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2009, 2010 The CVC4 Project +# Copyright (c) 2009, 2010, 2011 The CVC4 Project # # usage: update-copyright [ files/directories... ] # @@ -34,7 +34,7 @@ my $excluded_paths = '^src/parser/antlr_input_imports.cpp$'; # Years of copyright for the template. E.g., the string # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever. -my $years = '2009, 2010'; +my $years = '2009, 2010, 2011'; my $standard_template = <<EOF; ** This file is part of the CVC4 prototype. @@ -91,7 +91,110 @@ EOF print "Updating sources...\n"; -recurse(shift @searchdirs) while $#searchdirs >= 0; +while($#searchdirs >= 0) { + my $dir = shift @searchdirs; + my $mode = (stat($dir))[2] || warn "file or directory \`$dir' does not exist!"; + my $is_directory = S_ISDIR($mode); + if($is_directory) { + recurse($dir); + } else { + if($dir =~ m,^(.*)\/([^/]*)$,) { + my($dir, $file) = ($1, $2); + if($dir eq "") { + $dir = "/"; + } + handleFile($dir, $file); + } else { + handleFile(".", $dir); + } + } +} + +sub handleFile { + my ($srcdir, $file) = @_; + next if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g)$/); + next if ($srcdir.'/'.$file) =~ /$excluded_paths/; + print "$srcdir/$file..."; + my $infile = $srcdir.'/'.$file; + my $outfile = $srcdir.'/#'.$file.'.tmp'; + open(my $IN, $infile) || die "error opening $infile for reading"; + open(my $OUT, '>', $outfile) || die "error opening $outfile for writing"; + open(my $AUTHOR, "$dir/get-authors " . $infile . '|'); + my $author = <$AUTHOR>; chomp $author; + my $major_contributors = <$AUTHOR>; chomp $major_contributors; + my $minor_contributors = <$AUTHOR>; chomp $minor_contributors; + close $AUTHOR; + $_ = <$IN>; + if(m,^(%{)?/\*(\*| )\*\*\*,) { + print "updating\n"; + if($file =~ /\.(y|yy|ypp|Y)$/) { + print $OUT "%{/******************* */\n"; + print $OUT "/** $file\n"; + } elsif($file =~ /\.g$/) { + # avoid javadoc-style comment here; antlr complains + print $OUT "/* ******************* */\n"; + print $OUT "/*! \\file $file\n"; + } else { + print $OUT "/********************* */\n"; + print $OUT "/*! \\file $file\n"; + } + print $OUT " ** \\verbatim\n"; + print $OUT " ** Original author: $author\n"; + print $OUT " ** Major contributors: $major_contributors\n"; + print $OUT " ** Minor contributors (to current version): $minor_contributors\n"; + print $OUT $standard_template; + print $OUT " **\n"; + while(my $line = <$IN>) { + last if $line =~ /^ \*\*\s*$/; + } + } else { + my $line = $_; + print "adding\n"; + if($file =~ /\.(y|yy|ypp|Y)$/) { + print $OUT "%{/******************* */\n"; + print $OUT "/*! \\file $file\n"; + } elsif($file =~ /\.g$/) { + # avoid javadoc-style comment here; antlr complains + print $OUT "/* ******************* */\n"; + print $OUT "/*! \\file $file\n"; + } else { + print $OUT "/********************* */\n"; + print $OUT "/*! \\file $file\n"; + } + print $OUT " ** \\verbatim\n"; + print $OUT " ** Original author: $author\n"; + print $OUT " ** Major contributors: $major_contributors\n"; + print $OUT " ** Minor contributors (to current version): $minor_contributors\n"; + print $OUT $standard_template; + print $OUT " **\n"; + print $OUT " ** \\brief [[ Add one-line brief description here ]]\n"; + print $OUT " **\n"; + print $OUT " ** [[ Add lengthier description here ]]\n"; + print $OUT " ** \\todo document this file\n"; + print $OUT " **/\n\n"; + print $OUT $line; + if($file =~ /\.(y|yy|ypp|Y)$/) { + while(my $line = <$IN>) { + chomp $line; + if($line =~ '\s*%{(.*)') { + print $OUT "$1\n"; + last; + } + # just in case something's weird with the file ? + if(!($line =~ '\s*')) { + print $OUT "$line\n"; + last; + } + } + } + } + while(my $line = <$IN>) { + print $OUT $line; + } + close $IN; + close $OUT; + rename($outfile, $infile) || die "can't rename working file \`$outfile' to \`$infile'"; +} sub recurse { my ($srcdir) = @_; @@ -106,88 +209,7 @@ sub recurse { next if $file =~ /$excluded_directories/; recurse($srcdir.'/'.$file); } else { - next if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g)$/); - next if ($srcdir.'/'.$file) =~ /$excluded_paths/; - print "$srcdir/$file..."; - my $infile = $srcdir.'/'.$file; - my $outfile = $srcdir.'/#'.$file.'.tmp'; - open(my $IN, $infile) || die "error opening $infile for reading"; - open(my $OUT, '>', $outfile) || die "error opening $outfile for writing"; - open(my $AUTHOR, "$dir/get-authors " . $infile . '|'); - my $author = <$AUTHOR>; chomp $author; - my $major_contributors = <$AUTHOR>; chomp $major_contributors; - my $minor_contributors = <$AUTHOR>; chomp $minor_contributors; - close $AUTHOR; - $_ = <$IN>; - if(m,^(%{)?/\*(\*| )\*\*\*,) { - print "updating\n"; - if($file =~ /\.(y|yy|ypp|Y)$/) { - print $OUT "%{/******************* */\n"; - print $OUT "/** $file\n"; - } elsif($file =~ /\.g$/) { - # avoid javadoc-style comment here; antlr complains - print $OUT "/* ******************* */\n"; - print $OUT "/*! \\file $file\n"; - } else { - print $OUT "/********************* */\n"; - print $OUT "/*! \\file $file\n"; - } - print $OUT " ** \\verbatim\n"; - print $OUT " ** Original author: $author\n"; - print $OUT " ** Major contributors: $major_contributors\n"; - print $OUT " ** Minor contributors (to current version): $minor_contributors\n"; - print $OUT $standard_template; - print $OUT " **\n"; - while(my $line = <$IN>) { - last if $line =~ /^ \*\*\s*$/; - } - } else { - my $line = $_; - print "adding\n"; - if($file =~ /\.(y|yy|ypp|Y)$/) { - print $OUT "%{/******************* */\n"; - print $OUT "/*! \\file $file\n"; - } elsif($file =~ /\.g$/) { - # avoid javadoc-style comment here; antlr complains - print $OUT "/* ******************* */\n"; - print $OUT "/*! \\file $file\n"; - } else { - print $OUT "/********************* */\n"; - print $OUT "/*! \\file $file\n"; - } - print $OUT " ** \\verbatim\n"; - print $OUT " ** Original author: $author\n"; - print $OUT " ** Major contributors: $major_contributors\n"; - print $OUT " ** Minor contributors (to current version): $minor_contributors\n"; - print $OUT $standard_template; - print $OUT " **\n"; - print $OUT " ** \\brief [[ Add one-line brief description here ]]\n"; - print $OUT " **\n"; - print $OUT " ** [[ Add lengthier description here ]]\n"; - print $OUT " ** \\todo document this file\n"; - print $OUT " **/\n\n"; - print $OUT $line; - if($file =~ /\.(y|yy|ypp|Y)$/) { - while(my $line = <$IN>) { - chomp $line; - if($line =~ '\s*%{(.*)') { - print $OUT "$1\n"; - last; - } - # just in case something's weird with the file ? - if(!($line =~ '\s*')) { - print $OUT "$line\n"; - last; - } - } - } - } - while(my $line = <$IN>) { - print $OUT $line; - } - close $IN; - close $OUT; - rename($outfile, $infile) || die "can't rename working file \`$outfile' to \`$infile'"; + handleFile($srcdir, $file); } } closedir $DIR; 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 |