From bdd8685146c91a159c5cb336d8dc439787eb49b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Jul 2018 18:09:30 -0700 Subject: [PATCH] use params for arguments to Fixedpoint methods Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Fixedpoint.cs | 4 ++-- src/smt/theory_lra.cpp | 8 ++++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index e2fb7fe5a..102a96ac5 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -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. /// - 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 /// /// Convert benchmark given as set of axioms, rules and queries to a string. /// - public string ToString(BoolExpr[] queries) + public string ToString(params BoolExpr[] queries) { return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject, diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 9c054830c..ef1cd5f0a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1163,10 +1163,12 @@ public: } rational get_value(theory_var v) const { - + if (v == null_theory_var || - v >= static_cast(m_theory_var2var_index.size())) + v >= static_cast(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))); }