From 90cc5b0eccafd2f571b3bc388095bf8976cb8d18 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 19 Nov 2021 13:57:46 -0600 Subject: [PATCH] Remove n-ary builder (#7671) Adds the only usage of this file into ite_simp.cpp, where it is specialized for AND. This is work towards eliminating arithmetic subtyping (that utility had an unused and ambiguous use of mkConst(CONST_RATIONAL, ...)). --- src/CMakeLists.txt | 2 - src/preprocessing/passes/ite_simp.cpp | 84 ++++++++++- src/smt_util/nary_builder.cpp | 205 -------------------------- src/smt_util/nary_builder.h | 57 ------- 4 files changed, 82 insertions(+), 266 deletions(-) delete mode 100644 src/smt_util/nary_builder.cpp delete mode 100644 src/smt_util/nary_builder.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 58ccd288c..a04ea799d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -344,8 +344,6 @@ libcvc5_add_sources( smt/witness_form.h smt_util/boolean_simplification.cpp smt_util/boolean_simplification.h - smt_util/nary_builder.cpp - smt_util/nary_builder.h theory/arith/approx_simplex.cpp theory/arith/approx_simplex.h theory/arith/arith_ite_utils.cpp diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 433bca568..14ed9df07 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -22,7 +22,6 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_statistics_registry.h" -#include "smt_util/nary_builder.h" #include "theory/arith/arith_ite_utils.h" #include "theory/theory_engine.h" @@ -34,6 +33,87 @@ namespace cvc5 { namespace preprocessing { namespace passes { +Node mkAssocAnd(const std::vector& children) +{ + NodeManager* nm = NodeManager::currentNM(); + if (children.size() == 0) + { + return nm->mkConst(true); + } + else if (children.size() == 1) + { + return children[0]; + } + else + { + const uint32_t max = kind::metakind::getMaxArityForKind(kind::AND); + const uint32_t min = kind::metakind::getMinArityForKind(kind::AND); + + Assert(min <= children.size()); + + unsigned int numChildren = children.size(); + if (numChildren <= max) + { + return nm->mkNode(kind::AND, children); + } + + typedef std::vector::const_iterator const_iterator; + const_iterator it = children.begin(); + const_iterator end = children.end(); + + /* The new top-level children and the children of each sub node */ + std::vector newChildren; + std::vector subChildren; + + while (it != end && numChildren > max) + { + /* Grab the next max children and make a node for them. */ + for (const_iterator next = it + max; it != next; ++it, --numChildren) + { + subChildren.push_back(*it); + } + Node subNode = nm->mkNode(kind::AND, subChildren); + newChildren.push_back(subNode); + subChildren.clear(); + } + + /* If there's children left, "top off" the Expr. */ + if (numChildren > 0) + { + /* If the leftovers are too few, just copy them into newChildren; + * otherwise make a new sub-node */ + if (numChildren < min) + { + for (; it != end; ++it) + { + newChildren.push_back(*it); + } + } + else + { + for (; it != end; ++it) + { + subChildren.push_back(*it); + } + Node subNode = nm->mkNode(kind::AND, subChildren); + newChildren.push_back(subNode); + } + } + + /* It's inconceivable we could have enough children for this to fail + * (more than 2^32, in most cases?). */ + AlwaysAssert(newChildren.size() <= max) + << "Too many new children in mkAssociative"; + + /* It would be really weird if this happened (it would require + * min > 2, for one thing), but let's make sure. */ + AlwaysAssert(newChildren.size() >= min) + << "Too few new children in mkAssociative"; + + return nm->mkNode(kind::AND, newChildren); + } +} + /* -------------------------------------------------------------------------- */ namespace { @@ -71,7 +151,7 @@ void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess, assertionsToPreprocess->resize(before); size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1; intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]); - Node newLast = cvc5::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); + Node newLast = mkAssocAnd(intoConjunction); assertionsToPreprocess->replace(lastBeforeItes, newLast); Assert(assertionsToPreprocess->size() == before); } diff --git a/src/smt_util/nary_builder.cpp b/src/smt_util/nary_builder.cpp deleted file mode 100644 index 6d6259d73..000000000 --- a/src/smt_util/nary_builder.cpp +++ /dev/null @@ -1,205 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King, Aina Niemetz, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ -#include "smt_util/nary_builder.h" - -#include "expr/metakind.h" -#include "util/rational.h" - -using namespace std; - -namespace cvc5 { -namespace util { - -Node NaryBuilder::mkAssoc(Kind kind, const std::vector& children) -{ - if (children.size() == 0) - { - return zeroArity(kind); - } - else if (children.size() == 1) - { - return children[0]; - } - else - { - const uint32_t max = kind::metakind::getMaxArityForKind(kind); - const uint32_t min = kind::metakind::getMinArityForKind(kind); - - Assert(min <= children.size()); - - unsigned int numChildren = children.size(); - NodeManager* nm = NodeManager::currentNM(); - if( numChildren <= max ) { - return nm->mkNode(kind,children); - } - - typedef std::vector::const_iterator const_iterator; - const_iterator it = children.begin() ; - const_iterator end = children.end() ; - - /* The new top-level children and the children of each sub node */ - std::vector newChildren; - std::vector subChildren; - - while( it != end && numChildren > max ) { - /* Grab the next max children and make a node for them. */ - for(const_iterator next = it + max; it != next; ++it, --numChildren ) { - subChildren.push_back(*it); - } - Node subNode = nm->mkNode(kind,subChildren); - newChildren.push_back(subNode); - subChildren.clear(); - } - - /* If there's children left, "top off" the Expr. */ - if(numChildren > 0) { - /* If the leftovers are too few, just copy them into newChildren; - * otherwise make a new sub-node */ - if(numChildren < min) { - for(; it != end; ++it) { - newChildren.push_back(*it); - } - } else { - for(; it != end; ++it) { - subChildren.push_back(*it); - } - Node subNode = nm->mkNode(kind, subChildren); - newChildren.push_back(subNode); - } - } - - /* It's inconceivable we could have enough children for this to fail - * (more than 2^32, in most cases?). */ - AlwaysAssert(newChildren.size() <= max) - << "Too many new children in mkAssociative"; - - /* It would be really weird if this happened (it would require - * min > 2, for one thing), but let's make sure. */ - AlwaysAssert(newChildren.size() >= min) - << "Too few new children in mkAssociative"; - - return nm->mkNode(kind,newChildren); - } -} - -Node NaryBuilder::zeroArity(Kind k){ - using namespace kind; - NodeManager* nm = NodeManager::currentNM(); - switch(k){ - case AND: - return nm->mkConst(true); - case OR: - return nm->mkConst(false); - case PLUS: return nm->mkConst(CONST_RATIONAL, Rational(0)); - case MULT: return nm->mkConst(CONST_RATIONAL, Rational(1)); - default: - return Node::null(); - } -} - - -RePairAssocCommutativeOperators::RePairAssocCommutativeOperators() - : d_cache() -{} -RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){} -size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); } -void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); } - -bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){ - using namespace kind; - switch(k){ - case BITVECTOR_CONCAT: - case BITVECTOR_AND: - case BITVECTOR_OR: - case BITVECTOR_XOR: - case BITVECTOR_MULT: - case BITVECTOR_ADD: - case DISTINCT: - case PLUS: - case MULT: - case AND: - case OR: - return true; - default: - return false; - } -} - -Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){ - if(d_cache.find(n) != d_cache.end()){ - return d_cache[n]; - } - Node result = - isAssociateCommutative(n.getKind()) ? - case_assoccomm(n) : case_other(n); - - d_cache[n] = result; - return result; -} - -Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){ - Kind k = n.getKind(); - Assert(isAssociateCommutative(k)); - Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED); - unsigned N = n.getNumChildren(); - Assert(N >= 2); - - Node last = rePairAssocCommutativeOperators( n[N-1]); - Node nextToLast = rePairAssocCommutativeOperators(n[N-2]); - - NodeManager* nm = NodeManager::currentNM(); - Node last2 = nm->mkNode(k, nextToLast, last); - - if(N <= 2){ - return last2; - } else{ - Assert(N > 2); - Node prevRound = last2; - for(unsigned prevPos = N-2; prevPos > 0; --prevPos){ - unsigned currPos = prevPos-1; - Node curr = rePairAssocCommutativeOperators(n[currPos]); - Node round = nm->mkNode(k, curr, prevRound); - prevRound = round; - } - return prevRound; - } -} - -Node RePairAssocCommutativeOperators::case_other(TNode n){ - if(n.isConst() || n.isVar()){ - return n; - } - - NodeBuilder nb(n.getKind()); - - if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { - nb << n.getOperator(); - } - - // Remove the ITEs from the children - for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) { - Node newChild = rePairAssocCommutativeOperators(*i); - nb << newChild; - } - - Node result = (Node)nb; - return result; -} - -}/* util namespace */ -} // namespace cvc5 diff --git a/src/smt_util/nary_builder.h b/src/smt_util/nary_builder.h deleted file mode 100644 index 7af0f95a0..000000000 --- a/src/smt_util/nary_builder.h +++ /dev/null @@ -1,57 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include "cvc5_private.h" - -#pragma once - -#include -#include - -#include "expr/node.h" - -namespace cvc5 { -namespace util { - -class NaryBuilder { -public: - static Node mkAssoc(Kind k, const std::vector& children); - static Node zeroArity(Kind k); -};/* class NaryBuilder */ - -class RePairAssocCommutativeOperators { -public: - RePairAssocCommutativeOperators(); - ~RePairAssocCommutativeOperators(); - - Node rePairAssocCommutativeOperators(TNode n); - - static bool isAssociateCommutative(Kind k); - - size_t size() const; - void clear(); -private: - Node case_assoccomm(TNode n); - Node case_other(TNode n); - - typedef std::unordered_map NodeMap; - NodeMap d_cache; -};/* class RePairAssocCommutativeOperators */ - -}/* util namespace */ -} // namespace cvc5 -- 2.30.2