mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2014-10-13 18:59:37 -07:00
parent e46114819b 5e36d3a6a2
commit bae201b37d
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); Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
} }
/// <summary> /// <summary>
/// Adds a parameter setting. /// Adds a parameter setting.
/// </summary> /// </summary>
@ -103,6 +104,17 @@ namespace Microsoft.Z3
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject); 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> /// <summary>
/// A string representation of the parameter set. /// A string representation of the parameter set.
/// </summary> /// </summary>

12
src/shell/opt_frontend.cpp
View file

@ -168,6 +168,7 @@ class opb {
int id = in.parse_int(); int id = in.parse_int();
p = m.mk_const(symbol(id), m.mk_bool_sort()); p = m.mk_const(symbol(id), m.mk_bool_sort());
if (negated) p = m.mk_not(p); if (negated) p = m.mk_not(p);
in.skip_whitespace();
return p; return p;
} }
@ -179,7 +180,7 @@ class opb {
return result; return result;
} }
app_ref parse_coeff() { rational parse_coeff_r() {
in.skip_whitespace(); in.skip_whitespace();
svector<char> num; svector<char> num;
bool pos = true; bool pos = true;
@ -187,9 +188,13 @@ class opb {
if (*in == '+') ++in; if (*in == '+') ++in;
if (!pos) num.push_back('-'); if (!pos) num.push_back('-');
in.skip_whitespace(); 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); 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() { app_ref parse_term() {
@ -229,7 +234,6 @@ public:
in(in), arith(m) {} in(in), arith(m) {}
void parse() { void parse() {
while (true) { while (true) {
in.skip_whitespace(); in.skip_whitespace();
if (in.eof()) { if (in.eof()) {