1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Morgan Deters, Tim King |
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 "smt_util/boolean_simplification.h" |
17 |
|
|
18 |
|
namespace cvc5 { |
19 |
|
|
20 |
44 |
bool BooleanSimplification::push_back_associative_commute_recursive( |
21 |
|
Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) |
22 |
|
{ |
23 |
44 |
Node::iterator i = n.begin(), end = n.end(); |
24 |
264 |
for(; i != end; ++i){ |
25 |
220 |
Node child = *i; |
26 |
110 |
if(child.getKind() == k){ |
27 |
10 |
if(! push_back_associative_commute_recursive(child, buffer, k, notK, negateNode)) { |
28 |
|
return false; |
29 |
|
} |
30 |
100 |
}else if(child.getKind() == kind::NOT && child[0].getKind() == notK){ |
31 |
10 |
if(! push_back_associative_commute_recursive(child[0], buffer, notK, k, !negateNode)) { |
32 |
|
return false; |
33 |
|
} |
34 |
|
}else{ |
35 |
90 |
if(negateNode){ |
36 |
20 |
if(child.isConst()) { |
37 |
|
if((k == kind::AND && child.getConst<bool>()) || |
38 |
|
(k == kind::OR && !child.getConst<bool>())) { |
39 |
|
buffer.clear(); |
40 |
|
buffer.push_back(negate(child)); |
41 |
|
return false; |
42 |
|
} |
43 |
|
} else { |
44 |
20 |
buffer.push_back(negate(child)); |
45 |
|
} |
46 |
|
}else{ |
47 |
70 |
if(child.isConst()) { |
48 |
|
if((k == kind::OR && child.getConst<bool>()) || |
49 |
|
(k == kind::AND && !child.getConst<bool>())) { |
50 |
|
buffer.clear(); |
51 |
|
buffer.push_back(child); |
52 |
|
return false; |
53 |
|
} |
54 |
|
} else { |
55 |
70 |
buffer.push_back(child); |
56 |
|
} |
57 |
|
} |
58 |
|
} |
59 |
|
} |
60 |
44 |
return true; |
61 |
|
}/* BooleanSimplification::push_back_associative_commute_recursive() */ |
62 |
|
|
63 |
29322 |
} // namespace cvc5 |