GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt_util/boolean_simplification.cpp Lines: 15 27 55.6 %
Date: 2021-03-23 Branches: 38 102 37.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file boolean_simplification.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Simple routines for Boolean simplification
13
 **
14
 ** Simple, commonly-used routines for Boolean simplification.
15
 **/
16
17
#include "smt_util/boolean_simplification.h"
18
19
namespace CVC4 {
20
21
44
bool BooleanSimplification::push_back_associative_commute_recursive(
22
    Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
23
{
24
44
  Node::iterator i = n.begin(), end = n.end();
25
264
  for(; i != end; ++i){
26
220
    Node child = *i;
27
110
    if(child.getKind() == k){
28
10
      if(! push_back_associative_commute_recursive(child, buffer, k, notK, negateNode)) {
29
        return false;
30
      }
31
100
    }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){
32
10
      if(! push_back_associative_commute_recursive(child[0], buffer, notK, k, !negateNode)) {
33
        return false;
34
      }
35
    }else{
36
90
      if(negateNode){
37
20
        if(child.isConst()) {
38
          if((k == kind::AND && child.getConst<bool>()) ||
39
             (k == kind::OR && !child.getConst<bool>())) {
40
            buffer.clear();
41
            buffer.push_back(negate(child));
42
            return false;
43
          }
44
        } else {
45
20
          buffer.push_back(negate(child));
46
        }
47
      }else{
48
70
        if(child.isConst()) {
49
          if((k == kind::OR && child.getConst<bool>()) ||
50
             (k == kind::AND && !child.getConst<bool>())) {
51
            buffer.clear();
52
            buffer.push_back(child);
53
            return false;
54
          }
55
        } else {
56
70
          buffer.push_back(child);
57
        }
58
      }
59
    }
60
  }
61
44
  return true;
62
}/* BooleanSimplification::push_back_associative_commute_recursive() */
63
64
26685
}/* CVC4 namespace */