Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt_util/boolean_simplification.h	Lines:	60	68	88.2 %
Date:	2021-11-05	Branches:	77	188	41.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Tim King, Andres Noetzli
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Simple, commonly-used routines for Boolean simplification.
 */

#include "cvc5_private.h"

#ifndef CVC5__BOOLEAN_SIMPLIFICATION_H
#define CVC5__BOOLEAN_SIMPLIFICATION_H

#include <vector>
#include <algorithm>

#include "base/check.h"
#include "expr/node.h"

namespace cvc5 {

/**
 * 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<Node>& 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<Node>& buffer)
  {
    if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) {
      std::sort(buffer.begin(), buffer.end());
      std::vector<Node>::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<Node> 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<Node> 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<Node>& 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<bool>());
    }
    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

#endif /* CVC5__BOOLEAN_SIMPLIFICATION_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Tim King, Andres Noetzli
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Simple, commonly-used routines for Boolean simplification.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__BOOLEAN_SIMPLIFICATION_H
19		#define CVC5__BOOLEAN_SIMPLIFICATION_H
20
21		#include <vector>
22		#include <algorithm>
23
24		#include "base/check.h"
25		#include "expr/node.h"
26
27		namespace cvc5 {
28
29		/**
30		* A class to contain a number of useful functions for simple
31		* simplification of nodes. One never uses it as an object (and
32		* it cannot be constructed). It is used as a namespace.
33		*/
34		class BooleanSimplification {
35		// cannot construct one of these
36		BooleanSimplification() = delete;
37		BooleanSimplification(const BooleanSimplification&) = delete;
38
39		CVC5_WARN_UNUSED_RESULT static bool push_back_associative_commute_recursive(
40		Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode);
41
42		public:
43		/**
44		* The threshold for removing duplicates. (See removeDuplicates().)
45		*/
46		static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10;
47
48		/**
49		* Remove duplicate nodes from a vector, modifying it in-place.
50		* If the vector has size >= DUPLICATE_REMOVAL_THRESHOLD, this
51		* function is a no-op.
52		*/
53	15772	static void removeDuplicates(std::vector<Node>& buffer)
54		{
55	15772	if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) {
56	15772	std::sort(buffer.begin(), buffer.end());
57		std::vector<Node>::iterator new_end =
58	15772	std::unique(buffer.begin(), buffer.end());
59	15772	buffer.erase(new_end, buffer.end());
60		}
61	15772	}
62
63		/**
64		* Takes a node with kind AND, collapses all AND and (NOT OR)-kinded
65		* children of it (as far as possible---see
66		* push_back_associative_commute()), removes duplicates, and returns
67		* the resulting Node.
68		*/
69	15756	static Node simplifyConflict(Node andNode)
70		{
71	15756	AssertArgument(!andNode.isNull(), andNode);
72	15756	AssertArgument(andNode.getKind() == kind::AND, andNode);
73
74	31508	std::vector<Node> buffer;
75	15754	push_back_associative_commute(andNode, buffer, kind::AND, kind::OR);
76
77	15754	removeDuplicates(buffer);
78
79	15754	if(buffer.size() == 1) {
80		return buffer[0];
81		}
82
83	31508	NodeBuilder nb(kind::AND);
84	15754	nb.append(buffer);
85	15754	return nb;
86		}
87
88		/**
89		* Takes a node with kind OR, collapses all OR and (NOT AND)-kinded
90		* children of it (as far as possible---see
91		* push_back_associative_commute()), removes duplicates, and returns
92		* the resulting Node.
93		*/
94	20	static Node simplifyClause(Node orNode)
95		{
96	20	AssertArgument(!orNode.isNull(), orNode);
97	20	AssertArgument(orNode.getKind() == kind::OR, orNode);
98
99	36	std::vector<Node> buffer;
100	18	push_back_associative_commute(orNode, buffer, kind::OR, kind::AND);
101
102	18	removeDuplicates(buffer);
103
104	18	Assert(buffer.size() > 0);
105	18	if(buffer.size() == 1) {
106		return buffer[0];
107		}
108
109	36	NodeBuilder nb(kind::OR);
110	18	nb.append(buffer);
111	18	return nb;
112		}
113
114		/**
115		* Takes a node with kind IMPLIES, converts it to an OR, then
116		* simplifies the result with simplifyClause().
117		*
118		* The input doesn't actually have to be Horn, it seems, but that's
119		* the common case(?), hence the name.
120		*/
121	10	static Node simplifyHornClause(Node implication)
122		{
123	10	AssertArgument(implication.getKind() == kind::IMPLIES, implication);
124
125	16	TNode left = implication[0];
126	16	TNode right = implication[1];
127
128	16	Node notLeft = negate(left);
129	16	Node clause = NodeBuilder(kind::OR) << notLeft << right;
130
131	16	return simplifyClause(clause);
132		}
133
134		/**
135		* Aids in reforming a node. Takes a node of (N-ary) kind k and
136		* copies its children into an output vector, collapsing its k-kinded
137		* children into it. Also collapses negations of notK. For example:
138		*
139		* push_back_associative_commute( [OR [OR a b] [OR b c d] [NOT [AND e f]]],
140		* buffer, kind::OR, kind::AND )
141		* yields a "buffer" vector of [a b b c d e f]
142		*
143		* @param n the node to operate upon
144		* @param buffer the output vector (must be empty on entry)
145		* @param k the kind to collapse (should equal the kind of node n)
146		* @param notK the "negation" of kind k (e.g. OR's negation is AND),
147		* or kind::UNDEFINED_KIND if none.
148		* @param negateChildren true if the children of the resulting node
149		* (that is, the elements in buffer) should all be negated; you want
150		* this if e.g. you're simplifying the (OR...) in (NOT (OR...)),
151		* intending to make the result an AND.
152		*/
153	15772	static inline void push_back_associative_commute(Node n,
154		std::vector<Node>& buffer,
155		Kind k,
156		Kind notK,
157		bool negateChildren = false)
158		{
159	15772	AssertArgument(buffer.empty(), buffer);
160	15772	AssertArgument(!n.isNull(), n);
161	15772	AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k);
162	15772	AssertArgument(notK != kind::NULL_EXPR, notK);
163	15772	AssertArgument(n.getKind() == k, n,
164		"expected node to have kind %s", kindToString(k).c_str());
165
166		bool b CVC5_UNUSED =
167	15772	push_back_associative_commute_recursive(n, buffer, k, notK, false);
168
169	15772	if(buffer.size() == 0) {
170		// all the TRUEs for an AND (resp FALSEs for an OR) were simplified away
171		buffer.push_back(NodeManager::currentNM()->mkConst(k == kind::AND ? true : false));
172		}
173	15772	}/* push_back_associative_commute() */
174
175		/**
176		* Negates a node, doing all the double-negation elimination
177		* that's possible.
178		*
179		* @param n the node to negate (cannot be the null node)
180		*/
181	36	static Node negate(TNode n)
182		{
183	36	AssertArgument(!n.isNull(), n);
184
185	34	bool polarity = true;
186	68	TNode base = n;
187	58	while(base.getKind() == kind::NOT){
188	12	base = base[0];
189	12	polarity = !polarity;
190		}
191	34	if(n.isConst()) {
192		return NodeManager::currentNM()->mkConst(!n.getConst<bool>());
193		}
194	34	if(polarity){
195	30	return base.notNode();
196		}else{
197	4	return base;
198		}
199		}
200
201		/**
202		* Simplify an OR, AND, or IMPLIES. This function is the identity
203		* for all other kinds.
204		*/
205	16260	inline static Node simplify(TNode n)
206		{
207	16260	switch(n.getKind()) {
208	15748	case kind::AND:
209	15748	return simplifyConflict(n);
210
211		case kind::OR:
212		return simplifyClause(n);
213
214		case kind::IMPLIES:
215		return simplifyHornClause(n);
216
217	512	default:
218	512	return n;
219		}
220		}
221
222		};/* class BooleanSimplification */
223
224		} // namespace cvc5
225
226		#endif /* CVC5__BOOLEAN_SIMPLIFICATION_H */