From c1cdecfd689abec13ec8546b265695f707e89434 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Fri, 28 Feb 2014 08:21:21 -0500 Subject: [PATCH] theory/sets: cleanup --- src/theory/sets/theory_sets_private.cpp | 6 +++--- src/theory/sets/theory_sets_rewriter.cpp | 16 ++++++++++++++++ src/theory/sets/theory_sets_rewriter.h | 16 ++++++++++++++++ src/theory/sets/theory_sets_type_rules.h | 16 ++++++++++++++++ 4 files changed, 51 insertions(+), 3 deletions(-) diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 0ff5f231d..940e8f2d2 100644 --- 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 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 76e60f535..db67576d8 100644 --- 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 f01d198cf..715817508 100644 --- 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 35534de30..aee2c92b5 100644 --- 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 -- 2.30.2