From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 29 Dec 2011 00:07:52 +0000 (+0000)
Subject: Fix. If >2 arity multiplication nodes are requested. Apply associativity to give... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c58b26e3eb56e759e4dbb9727000355dec720ddb;p=francis%2Fstp.git

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



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 88c60b3..8c03115 100644
--- 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;