Fix. If >2 arity multiplication nodes are requested. Apply associativity to give...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1445 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 88c60b370012380d3bbab7be38e93feb1c4c8594..8c03115d35133c25c6aeadcd2adc281703e164ee 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -913,8 +913,29 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
                                     result = NodeFactory::CreateTerm(BEEV::BVMULT, width, children[1][0], children[0]);
                                     result = NodeFactory::CreateTerm(BEEV::BVUMINUS, width, result);
                                   }
-
                                  }
+                         else if (children.size() > 2)
+                             {
+                                 //Never create multiplications with arity > 2.
+
+                                 deque<ASTNode> names;
+
+                                 for (unsigned i = 0; i < children.size(); i++)
+                                   names.push_back(children[i]);
+
+                                 while (names.size() > 1)
+                                   {
+                                     ASTNode a = names.front();
+                                     names.pop_front();
+
+                                     ASTNode b = names.front();
+                                     names.pop_front();
+
+                                     ASTNode n = NodeFactory::CreateTerm(BVMULT, a.GetValueWidth(), a, b);
+                                     names.push_back(n);
+                                   }
+                                 result = names.front();
+                             }
                  }
                  break;