diff options
Diffstat (limited to 'src/preprocessing')
70 files changed, 232 insertions, 295 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 7408f4ba3..caad369b7 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andres Noetzli, Justin Xu, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index b133bc490..5d8f64594 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andres Noetzli, Justin Xu, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 888456174..31c92a09f 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -2,9 +2,9 @@ /*! \file ackermann.cpp ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar, Aina Niemetz, Clark Barrett, Ying Sheng + ** Ying Sheng, Yoni Zohar, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index 4aa26da85..1d2b6e9ce 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -2,9 +2,9 @@ /*! \file ackermann.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Yoni Zohar + ** Ying Sheng, Aina Niemetz, Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 98313efda..71aa028d4 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -2,9 +2,9 @@ /*! \file apply_substs.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Andres Noetzli + ** Aina Niemetz, Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h index f20ffa61e..4f2dd24e5 100644 --- a/src/preprocessing/passes/apply_substs.h +++ b/src/preprocessing/passes/apply_substs.h @@ -2,9 +2,9 @@ /*! \file apply_substs.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index e18e6f6c6..ad512bdfd 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Makai Mann, Yoni Zohar, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index 6e6d368eb..968672e86 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -2,9 +2,9 @@ /*! \file bool_to_bv.h ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar, Makai Mann, Liana Hadarean + ** Makai Mann, Yoni Zohar, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp index d62c8a97e..5d6ed9b4f 100644 --- a/src/preprocessing/passes/bv_abstraction.cpp +++ b/src/preprocessing/passes/bv_abstraction.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h index b5840b355..aa1134a9b 100644 --- a/src/preprocessing/passes/bv_abstraction.h +++ b/src/preprocessing/passes/bv_abstraction.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp index a16a8347d..d4dd2b9b9 100644 --- a/src/preprocessing/passes/bv_eager_atoms.cpp +++ b/src/preprocessing/passes/bv_eager_atoms.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h index 4ed685855..cd84f1aaa 100644 --- a/src/preprocessing/passes/bv_eager_atoms.h +++ b/src/preprocessing/passes/bv_eager_atoms.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index b08f69b50..68696015e 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -2,9 +2,9 @@ /*! \file bv_gauss.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Tim King + ** Aina Niemetz, Mathias Preiner, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index 7fb23814a..f09b2dbe4 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -2,9 +2,9 @@ /*! \file bv_gauss.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Mathias Preiner, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp index bfc02f332..a0f2ffdd5 100644 --- a/src/preprocessing/passes/bv_intro_pow2.cpp +++ b/src/preprocessing/passes/bv_intro_pow2.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index 86d5ebfef..fcfef6f39 100644 --- a/src/preprocessing/passes/bv_intro_pow2.h +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index 33b41210a..f4d4d5b8c 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Yoni Zohar, Liana Hadarean, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h index dc0494943..f0f4b3856 100644 --- a/src/preprocessing/passes/bv_to_bool.h +++ b/src/preprocessing/passes/bv_to_bool.h @@ -2,9 +2,9 @@ /*! \file bv_to_bool.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Yoni Zohar, Tim King + ** Liana Hadarean, Yoni Zohar, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 0e4bc41c0..5b125b4b6 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -2,9 +2,9 @@ /*! \file bv_to_int.cpp ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar and Ahmed Irfan + ** Yoni Zohar, Ahmed Irfan ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim @@ -184,43 +184,41 @@ Node BVToInt::eliminationPass(Node n) (d_eliminationCache.find(current) != d_eliminationCache.end()); bool inRebuildCache = (d_rebuildCache.find(current) != d_rebuildCache.end()); - if (!inRebuildCache) + if (!inEliminationCache) { - // current is not the elimination of any previously-visited node - if (!inEliminationCache) - { - // current hasn't been eliminated yet. - // eliminate operators from it - Node currentEliminated = - FixpointRewriteStrategy<RewriteRule<UdivZero>, - RewriteRule<SdivEliminate>, - RewriteRule<SremEliminate>, - RewriteRule<SmodEliminate>, - RewriteRule<RepeatEliminate>, - RewriteRule<ZeroExtendEliminate>, - RewriteRule<SignExtendEliminate>, - RewriteRule<RotateRightEliminate>, - RewriteRule<RotateLeftEliminate>, - RewriteRule<CompEliminate>, - RewriteRule<SleEliminate>, - RewriteRule<SltEliminate>, - RewriteRule<SgtEliminate>, - RewriteRule<SgeEliminate>, - RewriteRule<ShlByConst>, - RewriteRule<LshrByConst> >::apply(current); - // save in the cache - d_eliminationCache[current] = currentEliminated; - // put the eliminated node in the rebuild cache, but mark that it hasn't - // yet been rebuilt by assigning null. - d_rebuildCache[currentEliminated] = Node(); - // Push the eliminated node to the stack - toVisit.push_back(currentEliminated); - // Add the children to the stack for future processing. - toVisit.insert( - toVisit.end(), currentEliminated.begin(), currentEliminated.end()); - } + // current hasn't been eliminated yet. + // eliminate operators from it + Node currentEliminated = + FixpointRewriteStrategy<RewriteRule<UdivZero>, + RewriteRule<SdivEliminate>, + RewriteRule<SremEliminate>, + RewriteRule<SmodEliminate>, + RewriteRule<RepeatEliminate>, + RewriteRule<ZeroExtendEliminate>, + RewriteRule<SignExtendEliminate>, + RewriteRule<RotateRightEliminate>, + RewriteRule<RotateLeftEliminate>, + RewriteRule<CompEliminate>, + RewriteRule<SleEliminate>, + RewriteRule<SltEliminate>, + RewriteRule<SgtEliminate>, + RewriteRule<SgeEliminate>, + RewriteRule<ShlByConst>, + RewriteRule<LshrByConst> >::apply(current); + // save in the cache + d_eliminationCache[current] = currentEliminated; + // also assign the eliminated now to itself to avoid revisiting. + d_eliminationCache[currentEliminated] = currentEliminated; + // put the eliminated node in the rebuild cache, but mark that it hasn't + // yet been rebuilt by assigning null. + d_rebuildCache[currentEliminated] = Node(); + // Push the eliminated node to the stack + toVisit.push_back(currentEliminated); + // Add the children to the stack for future processing. + toVisit.insert( + toVisit.end(), currentEliminated.begin(), currentEliminated.end()); } - else + if (inRebuildCache) { // current was already added to the rebuild cache. if (d_rebuildCache[current].isNull()) diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index f0e0ea02e..5015d1e8e 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -2,9 +2,9 @@ /*! \file bv_to_int.h ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar and Ahmed Irfan + ** Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp index 8bf4cc816..39b3e1512 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.cpp +++ b/src/preprocessing/passes/extended_rewriter_pass.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h index dbaaa05ad..de6648d17 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.h +++ b/src/preprocessing/passes/extended_rewriter_pass.h @@ -2,9 +2,9 @@ /*! \file extended_rewriter_pass.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index 59b5ddf6e..25bb0e532 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index 89c3a3e3e..67cb0f770 100644 --- a/src/preprocessing/passes/global_negate.h +++ b/src/preprocessing/passes/global_negate.h @@ -2,9 +2,9 @@ /*! \file global_negate.h ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar + ** Yoni Zohar, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 65945f0d7..bb524315a 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index f0de321c4..be088c46b 100644 --- a/src/preprocessing/passes/ho_elim.h +++ b/src/preprocessing/passes/ho_elim.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 9fa9a0c05..e30c03f26 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -2,9 +2,9 @@ /*! \file int_to_bv.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Yoni Zohar, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim @@ -23,6 +23,7 @@ #include <vector> #include "expr/node.h" +#include "expr/node_traversal.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -36,107 +37,58 @@ using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>; namespace { -// TODO: clean this up -struct intToBV_stack_element -{ - TNode d_node; - bool d_children_added; - intToBV_stack_element(TNode node) : d_node(node), d_children_added(false) {} -}; /* struct intToBV_stack_element */ - bool childrenTypesChanged(Node n, NodeMap& cache) { - bool result = false; for (Node child : n) { TypeNode originalType = child.getType(); TypeNode newType = cache[child].getType(); if (! newType.isSubtypeOf(originalType)) { - result = true; - break; + return true; } } - return result; + return false; } Node intToBVMakeBinary(TNode n, NodeMap& cache) { - // Do a topological sort of the subexpressions and substitute them - vector<intToBV_stack_element> toVisit; - toVisit.push_back(n); - - while (!toVisit.empty()) + for (TNode current : NodeDfsIterable(n, VisitOrder::POSTORDER, + [&cache](TNode nn) { return cache.count(nn) > 0; })) { - // The current node we are processing - intToBV_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.d_node; - - NodeMap::iterator find = cache.find(current); - if (find != cache.end()) + Node result; + NodeManager* nm = NodeManager::currentNM(); + if (current.getNumChildren() == 0) { - toVisit.pop_back(); - continue; + result = current; } - if (stackHead.d_children_added) + else if (current.getNumChildren() > 2 + && (current.getKind() == kind::PLUS + || current.getKind() == kind::MULT)) { - // Children have been processed, so rebuild this node - Node result; - NodeManager* nm = NodeManager::currentNM(); - if (current.getNumChildren() > 2 - && (current.getKind() == kind::PLUS - || current.getKind() == kind::MULT)) - { - Assert(cache.find(current[0]) != cache.end()); - result = cache[current[0]]; - for (unsigned i = 1; i < current.getNumChildren(); ++i) - { - Assert(cache.find(current[i]) != cache.end()); - Node child = current[i]; - Node childRes = cache[current[i]]; - result = nm->mkNode(current.getKind(), result, childRes); - } - } - else + Assert(cache.find(current[0]) != cache.end()); + result = cache[current[0]]; + for (unsigned i = 1; i < current.getNumChildren(); ++i) { - NodeBuilder<> builder(current.getKind()); - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << current.getOperator(); - } - - for (unsigned i = 0; i < current.getNumChildren(); ++i) - { - Assert(cache.find(current[i]) != cache.end()); - builder << cache[current[i]]; - } - result = builder; + Assert(cache.find(current[i]) != cache.end()); + Node child = current[i]; + Node childRes = cache[current[i]]; + result = nm->mkNode(current.getKind(), result, childRes); } - cache[current] = result; - toVisit.pop_back(); } else { - // Mark that we have added the children if any - if (current.getNumChildren() > 0) - { - stackHead.d_children_added = true; - // We need to add the children - for (TNode::iterator child_it = current.begin(); - child_it != current.end(); - ++child_it) - { - TNode childNode = *child_it; - NodeMap::iterator childFind = cache.find(childNode); - if (childFind == cache.end()) - { - toVisit.push_back(childNode); - } - } + NodeBuilder<> builder(current.getKind()); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); } - else + + for (unsigned i = 0; i < current.getNumChildren(); ++i) { - cache[current] = current; - toVisit.pop_back(); + Assert(cache.find(current[i]) != cache.end()); + builder << cache[current[i]]; } + result = builder; } + cache[current] = result; } return cache[n]; } @@ -147,30 +99,16 @@ Node intToBV(TNode n, NodeMap& cache) AlwaysAssert(size > 0); AlwaysAssert(!options::incrementalSolving()); - vector<intToBV_stack_element> toVisit; NodeMap binaryCache; Node n_binary = intToBVMakeBinary(n, binaryCache); - toVisit.push_back(TNode(n_binary)); - while (!toVisit.empty()) + for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER, + [&cache](TNode nn) { return cache.count(nn) > 0; })) { - // The current node we are processing - intToBV_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.d_node; - - // If node is already in the cache we're done, pop from the stack - NodeMap::iterator find = cache.find(current); - if (find != cache.end()) - { - toVisit.pop_back(); - continue; - } - - // Not yet substituted, so process NodeManager* nm = NodeManager::currentNM(); - if (stackHead.d_children_added) + if (current.getNumChildren() > 0) { - // Children have been processed, so rebuild this node + // Not a leaf vector<Node> children; unsigned max = 0; for (unsigned i = 0; i < current.getNumChildren(); ++i) @@ -258,73 +196,51 @@ Node intToBV(TNode n, NodeMap& cache) result = Rewriter::rewrite(result); cache[current] = result; - toVisit.pop_back(); } else { - // Mark that we have added the children if any - if (current.getNumChildren() > 0) + // It's a leaf: could be a variable or a numeral + Node result = current; + if (current.isVar()) { - stackHead.d_children_added = true; - // We need to add the children - for (TNode::iterator child_it = current.begin(); - child_it != current.end(); - ++child_it) + if (current.getType() == nm->integerType()) { - TNode childNode = *child_it; - NodeMap::iterator childFind = cache.find(childNode); - if (childFind == cache.end()) - { - toVisit.push_back(childNode); - } + result = nm->mkSkolem("__intToBV_var", + nm->mkBitVectorType(size), + "Variable introduced in intToBV pass"); } } - else + else if (current.isConst()) { - // It's a leaf: could be a variable or a numeral - Node result = current; - if (current.isVar()) + switch (current.getKind()) { - if (current.getType() == nm->integerType()) + case kind::CONST_RATIONAL: { - result = nm->mkSkolem("__intToBV_var", - nm->mkBitVectorType(size), - "Variable introduced in intToBV pass"); - } - } - else if (current.isConst()) - { - switch (current.getKind()) - { - case kind::CONST_RATIONAL: - { - Rational constant = current.getConst<Rational>(); - if (constant.isIntegral()) { - AlwaysAssert(constant >= 0); - BitVector bv(size, constant.getNumerator()); - if (bv.toSignedInteger() != constant.getNumerator()) - { - throw TypeCheckingException( - current.toExpr(), - string("Not enough bits for constant in intToBV: ") - + current.toString()); - } - result = nm->mkConst(bv); + Rational constant = current.getConst<Rational>(); + if (constant.isIntegral()) { + AlwaysAssert(constant >= 0); + BitVector bv(size, constant.getNumerator()); + if (bv.toSignedInteger() != constant.getNumerator()) + { + throw TypeCheckingException( + current.toExpr(), + string("Not enough bits for constant in intToBV: ") + + current.toString()); } - break; + result = nm->mkConst(bv); } - default: break; + break; } + default: break; } - else - { - throw TypeCheckingException( - current.toExpr(), - string("Cannot translate to BV: ") + current.toString()); - } - cache[current] = result; - toVisit.pop_back(); } + else + { + throw TypeCheckingException( + current.toExpr(), + string("Cannot translate to BV: ") + current.toString()); + } + cache[current] = result; } } return cache[n_binary]; diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h index 95f31621a..284cf7256 100644 --- a/src/preprocessing/passes/int_to_bv.h +++ b/src/preprocessing/passes/int_to_bv.h @@ -2,9 +2,9 @@ /*! \file int_to_bv.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 6ad97f4a3..f021fff28 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -2,9 +2,9 @@ /*! \file ite_removal.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h index 5620b4afb..950d7342a 100644 --- a/src/preprocessing/passes/ite_removal.h +++ b/src/preprocessing/passes/ite_removal.h @@ -2,9 +2,9 @@ /*! \file ite_removal.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 7f7c4c95f..9a6a8ec61 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Aina Niemetz, Tim King, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index 44976bded..cf122c4c9 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -2,9 +2,9 @@ /*! \file ite_simp.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index debb4d2ac..f64fce118 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -2,9 +2,9 @@ /*! \file miplib_trick.cpp ** \verbatim ** Top contributors (to current version): - ** Mathias Preiner, Tim King, Andres Noetzli + ** Mathias Preiner, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index f1748d635..d57658d47 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index eb5728228..1f7e298ee 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -2,9 +2,9 @@ /*! \file nl_ext_purify.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h index 7744df824..a3004a7e8 100644 --- a/src/preprocessing/passes/nl_ext_purify.h +++ b/src/preprocessing/passes/nl_ext_purify.h @@ -2,9 +2,9 @@ /*! \file nl_ext_purify.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 03f38370b..6d2482a0e 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -2,9 +2,9 @@ /*! \file non_clausal_simp.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Andres Noetzli + ** Aina Niemetz, Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index cb4ece4a9..6e3645177 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -2,9 +2,9 @@ /*! \file non_clausal_simp.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index d852f2d86..1f9ca579c 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h index e73b721ff..fed566f78 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.h +++ b/src/preprocessing/passes/pseudo_boolean_processor.h @@ -2,9 +2,9 @@ /*! \file pseudo_boolean_processor.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Andres Noetzli + ** Tim King, Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index bc2c136e4..a4d8454a0 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -2,9 +2,9 @@ /*! \file quantifier_macros.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Yoni Zohar, Morgan Deters + ** Andrew Reynolds, Yoni Zohar, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index 6b62c4d31..30a83e54a 100644 --- a/src/preprocessing/passes/quantifier_macros.h +++ b/src/preprocessing/passes/quantifier_macros.h @@ -2,9 +2,9 @@ /*! \file quantifier_macros.h ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar, Andrew Reynolds + ** Yoni Zohar, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index eb6017402..3052e9629 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Caleb Donovick ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h index 991b3dd05..1e8b298f1 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.h +++ b/src/preprocessing/passes/quantifiers_preprocess.h @@ -2,9 +2,9 @@ /*! \file quantifiers_preprocess.h ** \verbatim ** Top contributors (to current version): - ** Caleb Donovick + ** Caleb Donovick, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 1c77f6f54..0e8ee3c4d 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -2,9 +2,9 @@ /*! \file real_to_int.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h index 7949fb051..d5c3be4e5 100644 --- a/src/preprocessing/passes/real_to_int.h +++ b/src/preprocessing/passes/real_to_int.h @@ -2,9 +2,9 @@ /*! \file real_to_int.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp index deb58ae9f..e12691cc0 100644 --- a/src/preprocessing/passes/rewrite.cpp +++ b/src/preprocessing/passes/rewrite.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Caleb Donovick ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h index e83cafb85..3bced24b1 100644 --- a/src/preprocessing/passes/rewrite.h +++ b/src/preprocessing/passes/rewrite.h @@ -2,9 +2,9 @@ /*! \file rewrite.h ** \verbatim ** Top contributors (to current version): - ** Caleb Donovick + ** Caleb Donovick, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index a81dbb4b5..b6f575789 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Yoni Zohar, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h index 1a5e36c40..8cbab3e29 100644 --- a/src/preprocessing/passes/sep_skolem_emp.h +++ b/src/preprocessing/passes/sep_skolem_emp.h @@ -2,9 +2,9 @@ /*! \file sep_skolem_emp.h ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar + ** Yoni Zohar, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index d0612086c..92c2e55b1 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h index ae722529d..3a8646109 100644 --- a/src/preprocessing/passes/sort_infer.h +++ b/src/preprocessing/passes/sort_infer.h @@ -2,9 +2,9 @@ /*! \file sort_infer.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli + ** Andrew Reynolds, Mathias Preiner, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index ec3982e03..314c34617 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -2,9 +2,9 @@ /*! \file static_learning.cpp ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar + ** Yoni Zohar, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h index f200755c5..16498f080 100644 --- a/src/preprocessing/passes/static_learning.h +++ b/src/preprocessing/passes/static_learning.h @@ -2,9 +2,9 @@ /*! \file static_learning.h ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar + ** Yoni Zohar, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 776e738d3..d8a587136 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -2,9 +2,9 @@ /*! \file sygus_inference.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h index 91deb445c..6b84ea3fe 100644 --- a/src/preprocessing/passes/sygus_inference.h +++ b/src/preprocessing/passes/sygus_inference.h @@ -2,9 +2,9 @@ /*! \file sygus_inference.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index f1e9e39c5..699899c1e 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -2,9 +2,9 @@ /*! \file synth_rew_rules.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h index 38ef98b35..80e09fd11 100644 --- a/src/preprocessing/passes/synth_rew_rules.h +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -2,9 +2,9 @@ /*! \file synth_rew_rules.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 1399363fa..5cc25b73f 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h index cfa9ab0b5..764685b85 100644 --- a/src/preprocessing/passes/theory_preprocess.h +++ b/src/preprocessing/passes/theory_preprocess.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 5d544ae57..7d1f66d65 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -2,9 +2,9 @@ /*! \file unconstrained_simplifier.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Andres Noetzli, Tim King + ** Clark Barrett, Andres Noetzli, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim @@ -75,6 +75,16 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) { d_unconstrained.erase(current); } + else + { + // Also erase the children from the visited-once set when we visit a + // node a second time, otherwise variables in this node are not + // erased from the set of unconstrained variables. + for (TNode childNode : current) + { + toVisit.push_back(unc_preprocess_stack_element(childNode, current)); + } + } } ++find->second; continue; @@ -91,6 +101,15 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) d_unconstrained.insert(current); } } + else if (current.isClosure()) + { + // Throw an exception. This should never happen in practice unless the + // user specifically enabled unconstrained simplification in an illegal + // logic. + throw LogicException( + "Cannot use unconstrained simplification in this logic, due to " + "(possibly internally introduced) quantified formula."); + } else { for (TNode childNode : current) diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index ac4fd0a03..c10730d60 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -2,9 +2,9 @@ /*! \file unconstrained_simplifier.h ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Andres Noetzli + ** Clark Barrett, Andres Noetzli, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim @@ -62,7 +62,11 @@ class UnconstrainedSimplifier : public PreprocessingPass theory::SubstitutionMap d_substitutions; const LogicInfo& d_logicInfo; - + /** + * Visit all subterms in assertion. This method throws a LogicException if + * there is a subterm that is unhandled by this preprocessing pass (e.g. a + * quantified formula). + */ void visitAll(TNode assertion); Node newUnconstrainedVar(TypeNode t, TNode var); void processUnconstrained(); diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 84c3ca79b..965edcd2f 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Justin Xu, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index 4a2e71488..e81f71666 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -2,9 +2,9 @@ /*! \file preprocessing_pass.h ** \verbatim ** Top contributors (to current version): - ** Justin Xu + ** Justin Xu, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 75085d7c4..c7e7ae82c 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Aina Niemetz, Mathias Preiner, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index f4317d786..deb600885 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -2,9 +2,9 @@ /*! \file preprocessing_pass_context.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, Justin Xu + ** Aina Niemetz, Mathias Preiner, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index e264c17e5..59c03479e 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -2,9 +2,9 @@ /*! \file preprocessing_pass_registry.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli, Justin Xu, Yoni Zohar + ** Andres Noetzli, Yoni Zohar, Justin Xu ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h index 9cc109897..cf10ab902 100644 --- a/src/preprocessing/preprocessing_pass_registry.h +++ b/src/preprocessing/preprocessing_pass_registry.h @@ -2,9 +2,9 @@ /*! \file preprocessing_pass_registry.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli, Justin Xu, Yoni Zohar + ** Andres Noetzli, Justin Xu, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index c609eebd7..45762341a 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Aina Niemetz, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h index ad195e62e..d26dee206 100644 --- a/src/preprocessing/util/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Aina Niemetz, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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.\endverbatim |