From a0cdeb2cfeb88580ac971cd8b2bbeb51f48e0b60 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Oct 2014 14:20:53 -0700
Subject: [PATCH] add useful API for parameter setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/Params.cs   | 12 ++++++++++++
 src/shell/opt_frontend.cpp | 12 ++++++++----
 2 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs
index 56a7a891f..a1334e612 100644
--- a/src/api/dotnet/Params.cs
+++ b/src/api/dotnet/Params.cs
@@ -69,6 +69,7 @@ namespace Microsoft.Z3
             Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
         }
 
+
         /// <summary>
         /// Adds a parameter setting.
         /// </summary>
@@ -103,6 +104,17 @@ namespace Microsoft.Z3
             Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
         }
 
+        /// <summary>
+        /// Adds a parameter setting.
+        /// </summary>
+        public void Add(string name, string value)
+        {
+            Contract.Requires(name != null);
+            Contract.Requires(value != null);
+
+            Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject);
+        }
+
         /// <summary>
         /// A string representation of the parameter set.
         /// </summary>
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 566a2c911..cb1f75561 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -168,6 +168,7 @@ class opb {
         int id = in.parse_int();
         p = m.mk_const(symbol(id), m.mk_bool_sort());
         if (negated) p = m.mk_not(p);
+        in.skip_whitespace();
         return p;
     }
 
@@ -179,7 +180,7 @@ class opb {
         return result;
     }
 
-    app_ref parse_coeff() {
+    rational parse_coeff_r() {
         in.skip_whitespace();
         svector<char> num;
         bool pos = true;
@@ -187,9 +188,13 @@ class opb {
         if (*in == '+') ++in;
         if (!pos) num.push_back('-');
         in.skip_whitespace();
-        while (*in >= '0' && *in <='9') num.push_back(*in), ++in;
+        while ('0' <= *in && *in <='9') num.push_back(*in), ++in;
         num.push_back(0);
-        return app_ref(arith.mk_numeral(rational(num.c_ptr()), true), m);
+        return rational(num.c_ptr());
+    }
+
+    app_ref parse_coeff() {
+        return app_ref(arith.mk_numeral(parse_coeff_r(), true), m);
     }
     
     app_ref parse_term() {        
@@ -229,7 +234,6 @@ public:
         in(in), arith(m) {}
 
     void parse() {
-
         while (true) {
             in.skip_whitespace();
             if (in.eof()) {