summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/preprocessing/passes/ite_simp.cpp84
-rw-r--r--src/smt_util/nary_builder.cpp205
-rw-r--r--src/smt_util/nary_builder.h57
4 files changed, 82 insertions, 266 deletions
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<Node>& 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<Node>::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<Node> newChildren;
+ std::vector<Node> 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<Node>& 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<Node>::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<Node> newChildren;
- std::vector<Node> 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 <unordered_map>
-#include <vector>
-
-#include "expr/node.h"
-
-namespace cvc5 {
-namespace util {
-
-class NaryBuilder {
-public:
- static Node mkAssoc(Kind k, const std::vector<Node>& 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<Node, Node> NodeMap;
- NodeMap d_cache;
-};/* class RePairAssocCommutativeOperators */
-
-}/* util namespace */
-} // namespace cvc5
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback