Merge pull request #18 from timothy-king/master

Merging in the glpk changes

1 files changed, 19 insertions, 0 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 11626c1de..98aa43e71 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -238,6 +238,25 @@ inline Node flattenAnd(Node n){
   return NodeManager::currentNM()->mkNode(kind::AND, out);
 }
 
+inline Node getIdentity(Kind k){
+  switch(k){
+  case kind::AND:
+    return NodeManager::currentNM()->mkConst<bool>(true);
+  case kind::PLUS:
+    return NodeManager::currentNM()->mkConst(Rational(1));
+  default:
+    Unreachable();
+  }
+}
+
+inline Node safeConstructNary(NodeBuilder<>& nb){
+  switch(nb.getNumChildren()){
+  case 0:  return getIdentity(nb.getKind());
+  case 1:  return nb[0];
+  default: return (Node)nb;
+  }
+}
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */