mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

add useful API for parameter setting

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-13 14:20:53 -07:00
parent 11fee1c8d0
commit a0cdeb2cfe
2 changed files with 20 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/api/dotnet/Params.cs
View file

@ -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>

12
src/shell/opt_frontend.cpp
View file

@ -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()) {