From 4114f4faaab9ade220cbebed0b8be4d4282d5280 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Sun, 19 Oct 2014 20:06:47 -0400 Subject: [PATCH] Finish sets type enumerator implementation. --- src/Makefile.am | 1 + src/theory/sets/normal_form.h | 52 +++++++++++++++++++ src/theory/sets/theory_sets_rewriter.cpp | 22 +------- src/theory/sets/theory_sets_type_enumerator.h | 21 ++++---- 4 files changed, 64 insertions(+), 32 deletions(-) create mode 100644 src/theory/sets/normal_form.h diff --git a/src/Makefile.am b/src/Makefile.am index 3e0831467..d82c0945d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -239,6 +239,7 @@ libcvc4_la_SOURCES = \ theory/datatypes/datatypes_rewriter.h \ theory/datatypes/theory_datatypes.cpp \ theory/sets/expr_patterns.h \ + theory/sets/normal_form.h \ theory/sets/options_handlers.h \ theory/sets/scrutinize.h \ theory/sets/term_info.h \ diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h new file mode 100644 index 000000000..bc34ea6f1 --- /dev/null +++ b/src/theory/sets/normal_form.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file normal_form.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) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Normal form for set constants. + ** + ** Normal form for set constants. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__SETS__NORMAL_FORM_H +#define __CVC4__THEORY__SETS__NORMAL_FORM_H + +namespace CVC4 { +namespace theory { +namespace sets { + +class NormalForm { +public: + + static Node elementsToSet(std::set elements, TypeNode setType) + { + NodeManager* nm = NodeManager::currentNM(); + + if(elements.size() == 0) { + return nm->mkConst(EmptySet(nm->toType(setType))); + } else { + typeof(elements.begin()) it = elements.begin(); + Node cur = nm->mkNode(kind::SINGLETON, *it); + while( ++it != elements.end() ) { + cur = nm->mkNode(kind::UNION, cur, + nm->mkNode(kind::SINGLETON, *it)); + } + return cur; + } + } + +}; + +} +} +} + +#endif diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 01ad51733..226eca62b 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -15,6 +15,7 @@ **/ #include "theory/sets/theory_sets_rewriter.h" +#include "theory/sets/normal_form.h" namespace CVC4 { namespace theory { @@ -210,25 +211,6 @@ const Elements& collectConstantElements(TNode setterm, SettermElementsMap& sette return it->second; } -Node elementsToNormalConstant(Elements elements, - TypeNode setType) -{ - NodeManager* nm = NodeManager::currentNM(); - - if(elements.size() == 0) { - return nm->mkConst(EmptySet(nm->toType(setType))); - } else { - - Elements::iterator it = elements.begin(); - Node cur = nm->mkNode(kind::SINGLETON, *it); - while( ++it != elements.end() ) { - cur = nm->mkNode(kind::UNION, cur, - nm->mkNode(kind::SINGLETON, *it)); - } - return cur; - } -} - // static RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { @@ -252,7 +234,7 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { //rewrite set to normal form SettermElementsMap setTermElementsMap; // cache const Elements& elements = collectConstantElements(node, setTermElementsMap); - RewriteResponse response(REWRITE_DONE, elementsToNormalConstant(elements, node.getType())); + RewriteResponse response(REWRITE_DONE, NormalForm::elementsToSet(elements, node.getType())); Debug("sets-rewrite-constant") << "[sets-rewrite-constant] Rewriting " << node << std::endl << "[sets-rewrite-constant] to " << response.node << std::endl; return response; diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 5d14006bb..718c329fd 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -25,6 +25,7 @@ #include "expr/type_node.h" #include "expr/kind.h" #include "theory/rewriter.h" +#include "theory/sets/normal_form.h" namespace CVC4 { namespace theory { @@ -87,21 +88,17 @@ public: if (d_finished) { throw NoMoreValuesException(getType()); } - Node n = d_setConst; - // For now only support only sets of size 1 - Assert(d_index == 0 || d_index == 1); - - if(d_index == 1) { - n = d_nm->mkNode(kind::SINGLETON, *(*(d_constituentVec[0]))); + std::vector elements; + for(unsigned i = 0; i < d_constituentVec.size(); ++i) { + elements.push_back(*(*(d_constituentVec[i]))); } - // for (unsigned i = 0; i < d_indexVec.size(); ++i) { - // n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i]))); - // } - Trace("set-type-enum") << "operator * prerewrite: " << n << std::endl; - n = Rewriter::rewrite(n); - Trace("set-type-enum") << "operator * returning: " << n << std::endl; + Node n = NormalForm::elementsToSet(std::set(elements.begin(), elements.end()), + getType()); + + Assert(n == Rewriter::rewrite(n)); + return n; } -- 2.30.2