From dd458fe71d6ae2fc435751127ab8dcddf066ddbe Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 21 May 2022 18:43:30 -0500 Subject: [PATCH] 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. --- src/CMakeLists.txt | 4 +- src/preprocessing/passes/miplib_trick.cpp | 2 +- .../util}/boolean_simplification.cpp | 59 ++++++++++++------ .../util}/boolean_simplification.h | 62 +++++++++++-------- src/printer/smt2/smt2_printer.cpp | 1 - .../arith/linear/theory_arith_private.cpp | 1 - src/theory/booleans/theory_bool.cpp | 1 - .../util/boolean_simplification_black.cpp | 4 +- 8 files changed, 84 insertions(+), 50 deletions(-) rename src/{smt_util => preprocessing/util}/boolean_simplification.cpp (55%) rename src/{smt_util => preprocessing/util}/boolean_simplification.h (86%) 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/smt_util/boolean_simplification.cpp b/src/preprocessing/util/boolean_simplification.cpp similarity index 55% rename from src/smt_util/boolean_simplification.cpp rename to src/preprocessing/util/boolean_simplification.cpp index 2e1ee7b42..aa5a3a583 100644 --- a/src/smt_util/boolean_simplification.cpp +++ b/src/preprocessing/util/boolean_simplification.cpp @@ -13,51 +13,74 @@ * Simple, commonly-used routines for Boolean simplification. */ -#include "smt_util/boolean_simplification.h" +#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){ + for (; i != end; ++i) + { Node child = *i; - if(child.getKind() == k){ - if(! push_back_associative_commute_recursive(child, buffer, k, notK, negateNode)) { + 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)) { + } + 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())) { + } + 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 { + } + else + { buffer.push_back(negate(child)); } - }else{ - if(child.isConst()) { - if((k == kind::OR && child.getConst()) || - (k == kind::AND && !child.getConst())) { + } + else + { + if (child.isConst()) + { + if ((k == kind::OR && child.getConst()) + || (k == kind::AND && !child.getConst())) + { buffer.clear(); buffer.push_back(child); return false; } - } else { + } + else + { buffer.push_back(child); } } } } return true; -}/* BooleanSimplification::push_back_associative_commute_recursive() */ +} /* BooleanSimplification::push_back_associative_commute_recursive() */ +} // namespace preprocessing } // namespace cvc5::internal diff --git a/src/smt_util/boolean_simplification.h b/src/preprocessing/util/boolean_simplification.h similarity index 86% rename from src/smt_util/boolean_simplification.h rename to src/preprocessing/util/boolean_simplification.h index c4e14daad..d0a29d4c6 100644 --- a/src/smt_util/boolean_simplification.h +++ b/src/preprocessing/util/boolean_simplification.h @@ -18,20 +18,22 @@ #ifndef CVC5__BOOLEAN_SIMPLIFICATION_H #define CVC5__BOOLEAN_SIMPLIFICATION_H -#include #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 { +class BooleanSimplification +{ // cannot construct one of these BooleanSimplification() = delete; BooleanSimplification(const BooleanSimplification&) = delete; @@ -52,10 +54,11 @@ class BooleanSimplification { */ static void removeDuplicates(std::vector& buffer) { - if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) { + if (buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) + { std::sort(buffer.begin(), buffer.end()); std::vector::iterator new_end = - std::unique(buffer.begin(), buffer.end()); + std::unique(buffer.begin(), buffer.end()); buffer.erase(new_end, buffer.end()); } } @@ -76,7 +79,8 @@ class BooleanSimplification { removeDuplicates(buffer); - if(buffer.size() == 1) { + if (buffer.size() == 1) + { return buffer[0]; } @@ -102,7 +106,8 @@ class BooleanSimplification { removeDuplicates(buffer); Assert(buffer.size() > 0); - if(buffer.size() == 1) { + if (buffer.size() == 1) + { return buffer[0]; } @@ -160,17 +165,21 @@ class BooleanSimplification { 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()); + 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) { + 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)); + buffer.push_back( + NodeManager::currentNM()->mkConst(k == kind::AND ? true : false)); } - }/* push_back_associative_commute() */ + } /* push_back_associative_commute() */ /** * Negates a node, doing all the double-negation elimination @@ -184,16 +193,21 @@ class BooleanSimplification { bool polarity = true; TNode base = n; - while(base.getKind() == kind::NOT){ + while (base.getKind() == kind::NOT) + { base = base[0]; polarity = !polarity; } - if(n.isConst()) { + if (n.isConst()) + { return NodeManager::currentNM()->mkConst(!n.getConst()); } - if(polarity){ + if (polarity) + { return base.notNode(); - }else{ + } + else + { return base; } } @@ -204,23 +218,21 @@ class BooleanSimplification { */ inline static Node simplify(TNode n) { - switch(n.getKind()) { - case kind::AND: - return simplifyConflict(n); + switch (n.getKind()) + { + case kind::AND: return simplifyConflict(n); - case kind::OR: - return simplifyClause(n); + case kind::OR: return simplifyClause(n); - case kind::IMPLIES: - return simplifyHornClause(n); + case kind::IMPLIES: return simplifyHornClause(n); - default: - return n; + default: return n; } } -};/* class BooleanSimplification */ +}; /* 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/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 { -- 2.30.2