theory/sets: cleanup

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 0ff5f231d36d434fb27f9f08a4762357d7a1c816..940e8f2d2e5caec3e1866eefd97eea4bdabe4de2 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -89,8 +89,8 @@ void TheorySetsPrivate::check(Theory::Effort level) {
 void TheorySetsPrivate::assertEquality(TNode fact, TNode reason, bool learnt)
 {
   Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
-                    << ", " << reason
-                    << ", " << learnt << std::endl;
+                       << ", " << reason
+                       << ", " << learnt << std::endl;
 
   bool polarity = fact.getKind() != kind::NOT;
   TNode atom = polarity ? fact : fact[0];
@@ -605,7 +605,7 @@ Node TheorySetsPrivate::explain(TNode literal)
   std::vector<TNode> assumptions;
 
   if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
-     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
   } else if(atom.getKind() == kind::MEMBER) {
     if( !d_equalityEngine.hasTerm(atom)) {
       d_equalityEngine.addTerm(atom);

diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 76e60f5355d2c507848515017d99fdd8456ed787..db67576d84658b36540bf33fb357af1fadd2de6e 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -1,3 +1,19 @@
+/*********************                                                        */
+/*! \file theory_sets_rewriter.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory rewriter.
+ **
+ ** Sets theory rewriter.
+ **/
+
 #include "theory/sets/theory_sets_rewriter.h"
 
 namespace CVC4 {

diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index f01d198cf77a84fbd34ed8db231eaca8b32dfe17..715817508b4b861c0f60032199ab060752278d69 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -1,3 +1,19 @@
+/*********************                                                        */
+/*! \file theory_sets_rewriter.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory rewriter.
+ **
+ ** Sets theory rewriter.
+ **/
+
 #include "cvc4_private.h"
 
 #ifndef __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 35534de3009a911942078db357f2b21132fa83e4..aee2c92b58b7f44dc90b12bf43e7e6c604e6f3a8 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -1,3 +1,19 @@
+/*********************                                                        */
+/*! \file theory_sets_type_rules.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory type rules.
+ **
+ ** Sets theory type rules.
+ **/
+
 #include "cvc4_private.h"
 
 #ifndef __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H