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

use params for arguments to Fixedpoint methods

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-13 18:09:30 -07:00
parent 88f4ce68fd
commit bdd8685146
2 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/dotnet/Fixedpoint.cs
View file

@ -146,7 +146,7 @@ namespace Microsoft.Z3
/// The query is satisfiable if there is an instance of some relation that is non-empty.
/// The query is unsatisfiable if there are no derivations satisfying any of the relations.
/// </summary>
public Status Query(FuncDecl[] relations)
public Status Query(params FuncDecl[] relations)
{
Contract.Requires(relations != null);
Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null));
@ -262,7 +262,7 @@ namespace Microsoft.Z3
/// <summary>
/// Convert benchmark given as set of axioms, rules and queries to a string.
/// </summary>
public string ToString(BoolExpr[] queries)
public string ToString(params BoolExpr[] queries)
{
return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,

8
src/smt/theory_lra.cpp
View file

@ -1163,10 +1163,12 @@ public:
}
rational get_value(theory_var v) const {
if (v == null_theory_var ||
v >= static_cast<theory_var>(m_theory_var2var_index.size()))
v >= static_cast<theory_var>(m_theory_var2var_index.size())) {
TRACE("arith", tout << "Variable v" << v << " not internalized\n";);
return rational::zero();
}
lp::var_index vi = m_theory_var2var_index[v];
if (m_variable_values.count(vi) > 0)
@ -1207,6 +1209,7 @@ public:
if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
reset_variable_values();
m_solver->get_model(m_variable_values);
TRACE("arith", display(tout););
}
}
@ -2642,6 +2645,7 @@ public:
}
else {
rational r = get_value(v);
TRACE("arith", tout << "v" << v << " := " << r << "\n";);
if (a.is_int(o) && !r.is_int()) r = floor(r);
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
}