From 86f3526110de9ca8c4d92696744c07d9dbad4e72 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Apr 2017 11:48:06 -0700 Subject: [PATCH] update get-value to also respect parameter model_index, #955 Signed-off-by: Nikolaj Bjorner --- src/parsers/smt2/smt2parser.cpp | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index d2b55af1d..b7f33d333 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2218,11 +2218,27 @@ namespace smt2 { if (m_cached_strings.empty()) throw cmd_exception("invalid get-value command, empty list of terms"); next(); + unsigned index = 0; + if (curr_is_keyword() && curr_id() == ":model_index") { + next(); + check_int("integer index expected to indexed model evaluation"); + if (!curr_numeral().is_unsigned()) + throw parser_exception("expected unsigned integer index to model evaluation"); + index = curr_numeral().get_unsigned(); + next(); + } + check_rparen("invalid get-value command, ')' expected"); if (!m_ctx.is_model_available() || m_ctx.get_check_sat_result() == 0) throw cmd_exception("model is not available"); model_ref md; - m_ctx.get_check_sat_result()->get_model(md); + if (index == 0) { + m_ctx.get_check_sat_result()->get_model(md); + } + else { + m_ctx.get_opt()->get_box_model(md, index); + + } m_ctx.regular_stream() << "("; expr ** expr_it = expr_stack().c_ptr() + spos; expr ** expr_end = expr_it + m_cached_strings.size();