Merge pull request #3503 from diffblue/smt2-get-assignment

SMT2: get-assignment

Author: Daniel Kroening

regression/smt2_solver/get-assignment/get-assignment1.desc

@@ -0,0 +1,8 @@
+CORE
+get-assignment1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+^\(\(y_equality true\)\)$
+--

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)

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

src/solvers/smt2/smt2_parser.h

@@ -42,6 +42,15 @@ class smt2_parsert:public smt2_tokenizert
   using id_mapt=std::map<irep_idt, idt>;
   id_mapt id_map;
 
+  struct named_termt
+  {
+    exprt term;
+    symbol_exprt name;
+  };
+
+  using named_termst = std::map<irep_idt, named_termt>;
+  named_termst named_terms;
+
   bool exit;
 
   /// This skips tokens until all bracketed expressions are closed

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 )

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))

src/solvers/smt2/smt2_tokenizer.h

@@ -60,6 +60,7 @@ class smt2_tokenizert:public parsert
     STRING_LITERAL,
     NUMERAL,
     SYMBOL,
+    KEYWORD,
     OPEN,
     CLOSE
   };