From 8e3e62533d254a3848544584db6b6d51ddfca0ca Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 26 Nov 2018 12:34:21 +0000 Subject: [PATCH 1/3] smt2 tokenizer: keywords Keywords are simple symbols preceded by a colon, and used for a range of purposes in the SMT-LIB2 syntax. The tokenizer now recognizes keywords. --- src/solvers/smt2/smt2_tokenizer.cpp | 8 +++++++- src/solvers/smt2/smt2_tokenizer.h | 1 + 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/solvers/smt2/smt2_tokenizer.cpp b/src/solvers/smt2/smt2_tokenizer.cpp index c2fe95448d3..dec183a56ee 100644 --- a/src/solvers/smt2/smt2_tokenizer.cpp +++ b/src/solvers/smt2/smt2_tokenizer.cpp @@ -254,7 +254,13 @@ void smt2_tokenizert::get_token_from_stream() case ':': // keyword token = get_simple_symbol(); - return; + if(token == SYMBOL) + { + token = KEYWORD; + return; + } + else + throw error("expecting symbol after colon"); case '#': if(in->get(ch)) diff --git a/src/solvers/smt2/smt2_tokenizer.h b/src/solvers/smt2/smt2_tokenizer.h index 62016c24367..d1fd4a774cd 100644 --- a/src/solvers/smt2/smt2_tokenizer.h +++ b/src/solvers/smt2/smt2_tokenizer.h @@ -60,6 +60,7 @@ class smt2_tokenizert:public parsert STRING_LITERAL, NUMERAL, SYMBOL, + KEYWORD, OPEN, CLOSE }; From 439d38c794251790ef057fb9b9b474e497dd75b9 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 26 Nov 2018 12:35:31 +0000 Subject: [PATCH 2/3] smt2 parser: term attributes Term attributes are used for a) named terms, and b) patterns for quantifiers. --- src/solvers/smt2/smt2_parser.cpp | 33 ++++++++++++++++++++++++++++++++ src/solvers/smt2/smt2_parser.h | 9 +++++++++ 2 files changed, 42 insertions(+) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index c3524bd4905..5894054ffdb 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -427,6 +427,39 @@ exprt smt2_parsert::function_application() throw error(msg.str()); } } + else if(buffer == "!") + { + // these are "term attributes" + const auto term = expression(); + + while(peek() == KEYWORD) + { + next_token(); // eat the keyword + if(buffer == "named") + { + // 'named terms' must be Boolean + if(term.type().id() != ID_bool) + throw error("named terms must be Boolean"); + + if(next_token() == SYMBOL) + { + const symbol_exprt symbol_expr(buffer, bool_typet()); + auto &named_term = named_terms[symbol_expr.get_identifier()]; + named_term.term = term; + named_term.name = symbol_expr; + } + else + throw error("invalid name attribute, expected symbol"); + } + else + throw error("unknown term attribute"); + } + + if(next_token() != CLOSE) + throw error("expected ')' at end of term attribute"); + else + return term; + } else { // non-indexed symbol; hash it diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 8f5d1a2010f..88b271d7f26 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -42,6 +42,15 @@ class smt2_parsert:public smt2_tokenizert using id_mapt=std::map; id_mapt id_map; + struct named_termt + { + exprt term; + symbol_exprt name; + }; + + using named_termst = std::map; + named_termst named_terms; + bool exit; /// This skips tokens until all bracketed expressions are closed From 4c6a340447b9fa196746e23cd94c7bfbef454856 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 26 Nov 2018 11:13:16 +0000 Subject: [PATCH 3/3] smt2: implemented get-assignment get-assignment returns the satisfying assignment for a given set of named terms. --- .../get-assignment/get-assignment1.desc | 8 +++++ .../get-assignment/get-assignment1.smt2 | 13 ++++++++ src/solvers/smt2/smt2_solver.cpp | 31 ++++++++++++++++++- 3 files changed, 51 insertions(+), 1 deletion(-) create mode 100644 regression/smt2_solver/get-assignment/get-assignment1.desc create mode 100644 regression/smt2_solver/get-assignment/get-assignment1.smt2 diff --git a/regression/smt2_solver/get-assignment/get-assignment1.desc b/regression/smt2_solver/get-assignment/get-assignment1.desc new file mode 100644 index 00000000000..ccb13c7edbe --- /dev/null +++ b/regression/smt2_solver/get-assignment/get-assignment1.desc @@ -0,0 +1,8 @@ +CORE +get-assignment1.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +^\(\(y_equality true\)\)$ +-- diff --git a/regression/smt2_solver/get-assignment/get-assignment1.smt2 b/regression/smt2_solver/get-assignment/get-assignment1.smt2 new file mode 100644 index 00000000000..718768621c2 --- /dev/null +++ b/regression/smt2_solver/get-assignment/get-assignment1.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_BV) +(set-option :produce-assignments true) + +(declare-const var_x (_ BitVec 8)) ; nullary function +(declare-const var_y (_ BitVec 8)) ; nullary function +(declare-const var_z (_ BitVec 8)) ; nullary function + +(assert (= var_x #x01)) +(assert (! (= var_y #x02) :named y_equality)) +(assert (= var_z (bvadd var_x var_y))) + +(check-sat) +(get-assignment) diff --git a/src/solvers/smt2/smt2_solver.cpp b/src/solvers/smt2/smt2_solver.cpp index 8a751736788..f9d46a78b8f 100644 --- a/src/solvers/smt2/smt2_solver.cpp +++ b/src/solvers/smt2/smt2_solver.cpp @@ -232,6 +232,36 @@ void smt2_solvert::command(const std::string &c) std::cout << smt2_format(constant_exprt(buffer, string_typet())) << '\n'; } + else if(c == "get-assignment") + { + // print satisfying assignment for all named expressions + + if(status != SAT) + throw error("model is not available"); + + bool first = true; + + std::cout << '('; + for(const auto &named_term : named_terms) + { + const symbol_tablet symbol_table; + const namespacet ns(symbol_table); + const auto value = + simplify_expr(solver.get(named_term.second.term), ns); + + if(value.is_constant()) + { + if(first) + first = false; + else + std::cout << '\n' << ' '; + + std::cout << '(' << smt2_format(named_term.second.name) << ' ' + << smt2_format(value) << ')'; + } + } + std::cout << ')' << '\n'; + } else if(c == "simplify") { // this is a command that Z3 appears to implement @@ -256,7 +286,6 @@ void smt2_solvert::command(const std::string &c) | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) ) | ( define-sort hsymboli ( hsymboli ??? ) hsorti ) | ( get-assertions ) - | ( get-assignment ) | ( get-info hinfo_flag i ) | ( get-model ) | ( get-option hkeywordi )