From: Andrew Reynolds Date: Sat, 21 May 2022 23:43:30 +0000 (-0500) Subject: Move smt_util to preprocessing/util (#8799) X-Git-Tag: cvc5-1.0.1~108 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd458fe71d6ae2fc435751127ab8dcddf066ddbe;p=cvc5.git Move smt_util to preprocessing/util (#8799) src/smt_util contains a single file that is only used by the miplib trick preprocessing pass. This moves it to preprocessing/util. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 52e3669c2..c045f77c8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -134,6 +134,8 @@ libcvc5_add_sources( preprocessing/preprocessing_pass_context.h preprocessing/preprocessing_pass_registry.cpp preprocessing/preprocessing_pass_registry.h + preprocessing/util/boolean_simplification.cpp + preprocessing/util/boolean_simplification.h preprocessing/util/ite_utilities.cpp preprocessing/util/ite_utilities.h printer/ast/ast_printer.cpp @@ -347,8 +349,6 @@ libcvc5_add_sources( smt/unsat_core_manager.h smt/witness_form.cpp smt/witness_form.h - smt_util/boolean_simplification.cpp - smt_util/boolean_simplification.h theory/arith/arith_evaluator.cpp theory/arith/arith_evaluator.h theory/arith/arith_ite_utils.cpp diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index e891eb22e..372f70a21 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -25,8 +25,8 @@ #include "options/base_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" +#include "preprocessing/util/boolean_simplification.h" #include "smt/smt_statistics_registry.h" -#include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" diff --git a/src/preprocessing/util/boolean_simplification.cpp b/src/preprocessing/util/boolean_simplification.cpp new file mode 100644 index 000000000..aa5a3a583 --- /dev/null +++ b/src/preprocessing/util/boolean_simplification.cpp @@ -0,0 +1,86 @@ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 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. + * **************************************************************************** + * + * Simple, commonly-used routines for Boolean simplification. + */ + +#include "preprocessing/util/boolean_simplification.h" + +namespace cvc5::internal { +namespace preprocessing { + +bool BooleanSimplification::push_back_associative_commute_recursive( + Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode) +{ + Node::iterator i = n.begin(), end = n.end(); + for (; i != end; ++i) + { + Node child = *i; + if (child.getKind() == k) + { + if (!push_back_associative_commute_recursive( + child, buffer, k, notK, negateNode)) + { + return false; + } + } + else if (child.getKind() == kind::NOT && child[0].getKind() == notK) + { + if (!push_back_associative_commute_recursive( + child[0], buffer, notK, k, !negateNode)) + { + return false; + } + } + else + { + if (negateNode) + { + if (child.isConst()) + { + if ((k == kind::AND && child.getConst()) + || (k == kind::OR && !child.getConst())) + { + buffer.clear(); + buffer.push_back(negate(child)); + return false; + } + } + else + { + buffer.push_back(negate(child)); + } + } + else + { + if (child.isConst()) + { + if ((k == kind::OR && child.getConst()) + || (k == kind::AND && !child.getConst())) + { + buffer.clear(); + buffer.push_back(child); + return false; + } + } + else + { + buffer.push_back(child); + } + } + } + } + return true; +} /* BooleanSimplification::push_back_associative_commute_recursive() */ + +} // namespace preprocessing +} // namespace cvc5::internal diff --git a/src/preprocessing/util/boolean_simplification.h b/src/preprocessing/util/boolean_simplification.h new file mode 100644 index 000000000..d0a29d4c6 --- /dev/null +++ b/src/preprocessing/util/boolean_simplification.h @@ -0,0 +1,238 @@ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 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. + * **************************************************************************** + * + * Simple, commonly-used routines for Boolean simplification. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__BOOLEAN_SIMPLIFICATION_H +#define CVC5__BOOLEAN_SIMPLIFICATION_H + +#include +#include + +#include "base/check.h" +#include "expr/node.h" + +namespace cvc5::internal { +namespace preprocessing { + +/** + * A class to contain a number of useful functions for simple + * simplification of nodes. One never uses it as an object (and + * it cannot be constructed). It is used as a namespace. + */ +class BooleanSimplification +{ + // cannot construct one of these + BooleanSimplification() = delete; + BooleanSimplification(const BooleanSimplification&) = delete; + + CVC5_WARN_UNUSED_RESULT static bool push_back_associative_commute_recursive( + Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode); + + public: + /** + * The threshold for removing duplicates. (See removeDuplicates().) + */ + static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10; + + /** + * Remove duplicate nodes from a vector, modifying it in-place. + * If the vector has size >= DUPLICATE_REMOVAL_THRESHOLD, this + * function is a no-op. + */ + static void removeDuplicates(std::vector& buffer) + { + if (buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) + { + std::sort(buffer.begin(), buffer.end()); + std::vector::iterator new_end = + std::unique(buffer.begin(), buffer.end()); + buffer.erase(new_end, buffer.end()); + } + } + + /** + * Takes a node with kind AND, collapses all AND and (NOT OR)-kinded + * children of it (as far as possible---see + * push_back_associative_commute()), removes duplicates, and returns + * the resulting Node. + */ + static Node simplifyConflict(Node andNode) + { + AssertArgument(!andNode.isNull(), andNode); + AssertArgument(andNode.getKind() == kind::AND, andNode); + + std::vector buffer; + push_back_associative_commute(andNode, buffer, kind::AND, kind::OR); + + removeDuplicates(buffer); + + if (buffer.size() == 1) + { + return buffer[0]; + } + + NodeBuilder nb(kind::AND); + nb.append(buffer); + return nb; + } + + /** + * Takes a node with kind OR, collapses all OR and (NOT AND)-kinded + * children of it (as far as possible---see + * push_back_associative_commute()), removes duplicates, and returns + * the resulting Node. + */ + static Node simplifyClause(Node orNode) + { + AssertArgument(!orNode.isNull(), orNode); + AssertArgument(orNode.getKind() == kind::OR, orNode); + + std::vector buffer; + push_back_associative_commute(orNode, buffer, kind::OR, kind::AND); + + removeDuplicates(buffer); + + Assert(buffer.size() > 0); + if (buffer.size() == 1) + { + return buffer[0]; + } + + NodeBuilder nb(kind::OR); + nb.append(buffer); + return nb; + } + + /** + * Takes a node with kind IMPLIES, converts it to an OR, then + * simplifies the result with simplifyClause(). + * + * The input doesn't actually have to be Horn, it seems, but that's + * the common case(?), hence the name. + */ + static Node simplifyHornClause(Node implication) + { + AssertArgument(implication.getKind() == kind::IMPLIES, implication); + + TNode left = implication[0]; + TNode right = implication[1]; + + Node notLeft = negate(left); + Node clause = NodeBuilder(kind::OR) << notLeft << right; + + return simplifyClause(clause); + } + + /** + * Aids in reforming a node. Takes a node of (N-ary) kind k and + * copies its children into an output vector, collapsing its k-kinded + * children into it. Also collapses negations of notK. For example: + * + * push_back_associative_commute( [OR [OR a b] [OR b c d] [NOT [AND e f]]], + * buffer, kind::OR, kind::AND ) + * yields a "buffer" vector of [a b b c d e f] + * + * @param n the node to operate upon + * @param buffer the output vector (must be empty on entry) + * @param k the kind to collapse (should equal the kind of node n) + * @param notK the "negation" of kind k (e.g. OR's negation is AND), + * or kind::UNDEFINED_KIND if none. + * @param negateChildren true if the children of the resulting node + * (that is, the elements in buffer) should all be negated; you want + * this if e.g. you're simplifying the (OR...) in (NOT (OR...)), + * intending to make the result an AND. + */ + static inline void push_back_associative_commute(Node n, + std::vector& buffer, + Kind k, + Kind notK, + bool negateChildren = false) + { + AssertArgument(buffer.empty(), buffer); + AssertArgument(!n.isNull(), n); + AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k); + AssertArgument(notK != kind::NULL_EXPR, notK); + AssertArgument(n.getKind() == k, + n, + "expected node to have kind %s", + kindToString(k).c_str()); + + bool b CVC5_UNUSED = + push_back_associative_commute_recursive(n, buffer, k, notK, false); + + if (buffer.size() == 0) + { + // all the TRUEs for an AND (resp FALSEs for an OR) were simplified away + buffer.push_back( + NodeManager::currentNM()->mkConst(k == kind::AND ? true : false)); + } + } /* push_back_associative_commute() */ + + /** + * Negates a node, doing all the double-negation elimination + * that's possible. + * + * @param n the node to negate (cannot be the null node) + */ + static Node negate(TNode n) + { + AssertArgument(!n.isNull(), n); + + bool polarity = true; + TNode base = n; + while (base.getKind() == kind::NOT) + { + base = base[0]; + polarity = !polarity; + } + if (n.isConst()) + { + return NodeManager::currentNM()->mkConst(!n.getConst()); + } + if (polarity) + { + return base.notNode(); + } + else + { + return base; + } + } + + /** + * Simplify an OR, AND, or IMPLIES. This function is the identity + * for all other kinds. + */ + inline static Node simplify(TNode n) + { + switch (n.getKind()) + { + case kind::AND: return simplifyConflict(n); + + case kind::OR: return simplifyClause(n); + + case kind::IMPLIES: return simplifyHornClause(n); + + default: return n; + } + } + +}; /* class BooleanSimplification */ + +} // namespace preprocessing +} // namespace cvc5::internal + +#endif /* CVC5__BOOLEAN_SIMPLIFICATION_H */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 62d6f3bb4..519d67fc1 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -40,7 +40,6 @@ #include "printer/let_binding.h" #include "proof/unsat_core.h" #include "smt/command.h" -#include "smt_util/boolean_simplification.h" #include "theory/bags/table_project_op.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/datatypes/sygus_datatype_utils.h" diff --git a/src/smt_util/boolean_simplification.cpp b/src/smt_util/boolean_simplification.cpp deleted file mode 100644 index 2e1ee7b42..000000000 --- a/src/smt_util/boolean_simplification.cpp +++ /dev/null @@ -1,63 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 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. - * **************************************************************************** - * - * Simple, commonly-used routines for Boolean simplification. - */ - -#include "smt_util/boolean_simplification.h" - -namespace cvc5::internal { - -bool BooleanSimplification::push_back_associative_commute_recursive( - Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode) -{ - Node::iterator i = n.begin(), end = n.end(); - for(; i != end; ++i){ - Node child = *i; - if(child.getKind() == k){ - if(! push_back_associative_commute_recursive(child, buffer, k, notK, negateNode)) { - return false; - } - }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){ - if(! push_back_associative_commute_recursive(child[0], buffer, notK, k, !negateNode)) { - return false; - } - }else{ - if(negateNode){ - if(child.isConst()) { - if((k == kind::AND && child.getConst()) || - (k == kind::OR && !child.getConst())) { - buffer.clear(); - buffer.push_back(negate(child)); - return false; - } - } else { - buffer.push_back(negate(child)); - } - }else{ - if(child.isConst()) { - if((k == kind::OR && child.getConst()) || - (k == kind::AND && !child.getConst())) { - buffer.clear(); - buffer.push_back(child); - return false; - } - } else { - buffer.push_back(child); - } - } - } - } - return true; -}/* BooleanSimplification::push_back_associative_commute_recursive() */ - -} // namespace cvc5::internal diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h deleted file mode 100644 index c4e14daad..000000000 --- a/src/smt_util/boolean_simplification.h +++ /dev/null @@ -1,226 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Tim King, Andres Noetzli - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 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. - * **************************************************************************** - * - * Simple, commonly-used routines for Boolean simplification. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__BOOLEAN_SIMPLIFICATION_H -#define CVC5__BOOLEAN_SIMPLIFICATION_H - -#include -#include - -#include "base/check.h" -#include "expr/node.h" - -namespace cvc5::internal { - -/** - * A class to contain a number of useful functions for simple - * simplification of nodes. One never uses it as an object (and - * it cannot be constructed). It is used as a namespace. - */ -class BooleanSimplification { - // cannot construct one of these - BooleanSimplification() = delete; - BooleanSimplification(const BooleanSimplification&) = delete; - - CVC5_WARN_UNUSED_RESULT static bool push_back_associative_commute_recursive( - Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode); - - public: - /** - * The threshold for removing duplicates. (See removeDuplicates().) - */ - static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10; - - /** - * Remove duplicate nodes from a vector, modifying it in-place. - * If the vector has size >= DUPLICATE_REMOVAL_THRESHOLD, this - * function is a no-op. - */ - static void removeDuplicates(std::vector& buffer) - { - if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) { - std::sort(buffer.begin(), buffer.end()); - std::vector::iterator new_end = - std::unique(buffer.begin(), buffer.end()); - buffer.erase(new_end, buffer.end()); - } - } - - /** - * Takes a node with kind AND, collapses all AND and (NOT OR)-kinded - * children of it (as far as possible---see - * push_back_associative_commute()), removes duplicates, and returns - * the resulting Node. - */ - static Node simplifyConflict(Node andNode) - { - AssertArgument(!andNode.isNull(), andNode); - AssertArgument(andNode.getKind() == kind::AND, andNode); - - std::vector buffer; - push_back_associative_commute(andNode, buffer, kind::AND, kind::OR); - - removeDuplicates(buffer); - - if(buffer.size() == 1) { - return buffer[0]; - } - - NodeBuilder nb(kind::AND); - nb.append(buffer); - return nb; - } - - /** - * Takes a node with kind OR, collapses all OR and (NOT AND)-kinded - * children of it (as far as possible---see - * push_back_associative_commute()), removes duplicates, and returns - * the resulting Node. - */ - static Node simplifyClause(Node orNode) - { - AssertArgument(!orNode.isNull(), orNode); - AssertArgument(orNode.getKind() == kind::OR, orNode); - - std::vector buffer; - push_back_associative_commute(orNode, buffer, kind::OR, kind::AND); - - removeDuplicates(buffer); - - Assert(buffer.size() > 0); - if(buffer.size() == 1) { - return buffer[0]; - } - - NodeBuilder nb(kind::OR); - nb.append(buffer); - return nb; - } - - /** - * Takes a node with kind IMPLIES, converts it to an OR, then - * simplifies the result with simplifyClause(). - * - * The input doesn't actually have to be Horn, it seems, but that's - * the common case(?), hence the name. - */ - static Node simplifyHornClause(Node implication) - { - AssertArgument(implication.getKind() == kind::IMPLIES, implication); - - TNode left = implication[0]; - TNode right = implication[1]; - - Node notLeft = negate(left); - Node clause = NodeBuilder(kind::OR) << notLeft << right; - - return simplifyClause(clause); - } - - /** - * Aids in reforming a node. Takes a node of (N-ary) kind k and - * copies its children into an output vector, collapsing its k-kinded - * children into it. Also collapses negations of notK. For example: - * - * push_back_associative_commute( [OR [OR a b] [OR b c d] [NOT [AND e f]]], - * buffer, kind::OR, kind::AND ) - * yields a "buffer" vector of [a b b c d e f] - * - * @param n the node to operate upon - * @param buffer the output vector (must be empty on entry) - * @param k the kind to collapse (should equal the kind of node n) - * @param notK the "negation" of kind k (e.g. OR's negation is AND), - * or kind::UNDEFINED_KIND if none. - * @param negateChildren true if the children of the resulting node - * (that is, the elements in buffer) should all be negated; you want - * this if e.g. you're simplifying the (OR...) in (NOT (OR...)), - * intending to make the result an AND. - */ - static inline void push_back_associative_commute(Node n, - std::vector& buffer, - Kind k, - Kind notK, - bool negateChildren = false) - { - AssertArgument(buffer.empty(), buffer); - AssertArgument(!n.isNull(), n); - AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k); - AssertArgument(notK != kind::NULL_EXPR, notK); - AssertArgument(n.getKind() == k, n, - "expected node to have kind %s", kindToString(k).c_str()); - - bool b CVC5_UNUSED = - push_back_associative_commute_recursive(n, buffer, k, notK, false); - - if(buffer.size() == 0) { - // all the TRUEs for an AND (resp FALSEs for an OR) were simplified away - buffer.push_back(NodeManager::currentNM()->mkConst(k == kind::AND ? true : false)); - } - }/* push_back_associative_commute() */ - - /** - * Negates a node, doing all the double-negation elimination - * that's possible. - * - * @param n the node to negate (cannot be the null node) - */ - static Node negate(TNode n) - { - AssertArgument(!n.isNull(), n); - - bool polarity = true; - TNode base = n; - while(base.getKind() == kind::NOT){ - base = base[0]; - polarity = !polarity; - } - if(n.isConst()) { - return NodeManager::currentNM()->mkConst(!n.getConst()); - } - if(polarity){ - return base.notNode(); - }else{ - return base; - } - } - - /** - * Simplify an OR, AND, or IMPLIES. This function is the identity - * for all other kinds. - */ - inline static Node simplify(TNode n) - { - switch(n.getKind()) { - case kind::AND: - return simplifyConflict(n); - - case kind::OR: - return simplifyClause(n); - - case kind::IMPLIES: - return simplifyHornClause(n); - - default: - return n; - } - } - -};/* class BooleanSimplification */ - -} // namespace cvc5::internal - -#endif /* CVC5__BOOLEAN_SIMPLIFICATION_H */ diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp index e58a7ce0a..697267f7a 100644 --- a/src/theory/arith/linear/theory_arith_private.cpp +++ b/src/theory/arith/linear/theory_arith_private.cpp @@ -44,7 +44,6 @@ #include "proof/proof_rule.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" -#include "smt_util/boolean_simplification.h" #include "theory/arith/linear/approx_simplex.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/linear/arith_static_learner.h" diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index f491e4003..9df6e08a6 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -19,7 +19,6 @@ #include #include "proof/proof_node_manager.h" -#include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" #include "theory/booleans/theory_bool_rewriter.h" #include "theory/substitutions.h" diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index f6d48b7d2..b6405c133 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -21,9 +21,11 @@ #include "expr/node.h" #include "options/io_utils.h" #include "options/language.h" -#include "smt_util/boolean_simplification.h" +#include "preprocessing/util/boolean_simplification.h" #include "test_node.h" +using namespace cvc5::internal::preprocessing; + namespace cvc5::internal { namespace test {