#
# 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... ]
#
# 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.
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) = @_;
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;
} 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) {
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!");
}
}
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);
}
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);
// 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]);
}
}
// NOTE: assumptions passed in member-variable 'assumptions'.
lbool Solver::solve_()
{
- Debug("minisat") << "nvars = " << nVars() << endl;
+ Debug("minisat") << "nvars = " << nVars() << std::endl;
in_solve = true;
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;
/*! \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
** \todo document this file
**/
-
#include "theory/theory.h"
#include "theory/arith/normal_form.h"
#include "theory/arith/arith_rewriter.h"
/*! \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
** \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"
#include "theory/rewriter.h"
-#ifndef __CVC4__THEORY__ARITH__REWRITER_H
-#define __CVC4__THEORY__ARITH__REWRITER_H
-
namespace CVC4 {
namespace theory {
namespace arith {
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 */
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){
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;
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:
using namespace CVC4::theory;
using namespace CVC4::theory::arith;
+using namespace std;
+
Tableau::~Tableau(){
while(!d_basicVariables.empty()){
ArithVar curr = *(d_basicVariables.begin());
-/*
- * 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"
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 */
+/********************* */
+/*! \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"
return RewriteResponse(REWRITE_DONE, n);
}
-}
-}
-}
-
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
-/*
- * 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"
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 */
+/********************* */
+/*! \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 {
return out;
}
-}
-}
-}
+}/* CVC4::theory::builtin namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
-/*
- * 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"
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 */
* String representation of a set.
*/
std::string toString(reference_type set) {
- stringstream out;
+ std::stringstream out;
print(out, set);
return out.str();
}
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));
// 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);
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;
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();
template<>
Node RewriteRule<ConcatExtractMerge>::apply(Node node) {
- vector<Node> mergedExtracts;
+ std::vector<Node> mergedExtracts;
Node current = node[0];
bool mergeStarted = false;
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
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--) {
-/*
- * 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"
-/*
- * 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"
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 */
-/*
- * 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 {
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;
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();
}
}
-/*
- * 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"
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 */
#ifndef __CVC4__CONFIGURATION_PRIVATE_H
#define __CVC4__CONFIGURATION_PRIVATE_H
-using namespace std;
-
namespace CVC4 {
#ifdef CVC4_DEBUG
projects / cvc5.git / commitdiff