From 27dac5e91eee563d62795e43d5e7ac5f6c878730 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 17 Oct 2017 13:17:20 -0700 Subject: [PATCH] Fixing 2 instances of an unused variable. (#1253) --- src/theory/datatypes/datatypes_sygus.cpp | 16 +++++++++++----- src/theory/datatypes/datatypes_sygus.h | 1 - src/theory/sets/theory_sets_rewriter.cpp | 7 ++++--- 3 files changed, 15 insertions(+), 9 deletions(-) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index c543c16e2..5d48c1ce2 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -65,11 +65,17 @@ void SygusSplitNew::getSygusSplits( Node n, const Datatype& dt, std::vector< Nod splits.insert( splits.end(), d_splits[n].begin(), d_splits[n].end() ); } - -SygusSymBreakNew::SygusSymBreakNew( TheoryDatatypes * td, quantifiers::TermDbSygus * tds, context::Context* c ) : -d_td( td ), d_tds( tds ), d_context( c ), -d_testers( c ), d_is_const( c ), d_testers_exp( c ), d_active_terms( c ), d_currTermSize( c ) { - d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); +SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td, + quantifiers::TermDbSygus* tds, + context::Context* c) + : d_td(td), + d_tds(tds), + d_testers(c), + d_is_const(c), + d_testers_exp(c), + d_active_terms(c), + d_currTermSize(c) { + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); } SygusSymBreakNew::~SygusSymBreakNew() { diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 3e37fe728..bb83b4850 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -56,7 +56,6 @@ class SygusSymBreakNew private: TheoryDatatypes * d_td; quantifiers::TermDbSygus * d_tds; - context::Context* d_context; typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 8c3fe67d3..084ca6c96 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -15,10 +15,11 @@ **/ #include "theory/sets/theory_sets_rewriter.h" -#include "theory/sets/normal_form.h" -#include "theory/sets/rels_utils.h" + #include "expr/attribute.h" #include "options/sets_options.h" +#include "theory/sets/normal_form.h" +#include "theory/sets/rels_utils.h" namespace CVC4 { namespace theory { @@ -92,7 +93,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) static const unsigned MAX_CHILDREN = (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1; AlwaysAssert(childList.size() < MAX_CHILDREN, "do not support formulas this big"); - ChildList::iterator cur = childList.begin(), next, en = childList.end(); + ChildList::iterator cur = childList.begin(), en = childList.end(); Node ret = (*cur); ++cur; while( cur != en ) { -- 2.30.2