Correctly parse uninterpreted constant values in get-value (#7393)

SMT-LIB indicates that abstract values can appear in terms as arguments to `get-value`.  This is not currently the case, as pointed out by #6908.

This updates our parser so that bindings are added to the symbol table for all uninterpreted constants in the model whenever we parse a `get-value` term.

Fixes #6908.

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 84c0bd17c632721ca7c486ada55cad04aa05c389..9f34b56479c688344f67b2e2cc2fa845d7580d36 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -737,6 +737,36 @@ void Parser::pushScope(bool isUserContext)
   d_symman->pushScope(isUserContext);
 }
 
+void Parser::pushGetValueScope()
+{
+  pushScope();
+  // we must bind all relevant uninterpreted constants, which coincide with
+  // the set of uninterpreted constants that are printed in the definition
+  // of a model.
+  std::vector<api::Sort> declareSorts = d_symman->getModelDeclareSorts();
+  Trace("parser") << "Push get value scope, with " << declareSorts.size()
+                  << " declared sorts" << std::endl;
+  for (const api::Sort& s : declareSorts)
+  {
+    std::vector<api::Term> elements = d_solver->getModelDomainElements(s);
+    for (const api::Term& e : elements)
+    {
+      // Uninterpreted constants are abstract values, which by SMT-LIB are
+      // required to be annotated with their type, e.g. (as @uc_Foo_0 Foo).
+      // Thus, the element is not printed simply as its name.
+      std::string en = e.toString();
+      size_t index = en.find("(as ");
+      if (index == 0)
+      {
+        index = en.find(" ", 4);
+        en = en.substr(4, index - 4);
+      }
+      Trace("parser") << "Get value scope : " << en << " -> " << e << std::endl;
+      defineVar(en, e);
+    }
+  }
+}
+
 void Parser::popScope()
 {
   d_symman->popScope();

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 4b04c77b77fa9e62355d7006f5bac119b0603d65..19e5b85311c1a003a176bc569362239a12982436 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -716,6 +716,14 @@ public:
    */
   void pushScope(bool isUserContext = false);
 
+  /** Push scope for get-value
+   *
+   * This pushes a scope by a call to pushScope that binds all relevant bindings
+   * required for parsing the SMT-LIB command `get-value`. This includes
+   * all uninterpreted constant values in user-defined uninterpreted sorts.
+   */
+  void pushGetValueScope();
+
   void popScope();
 
   virtual void reset();

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a75aa36da08c5e44cdae0fe9e3fc97a49e32a0f6..e3aee250ec6dac2e3164e4e4007896ade8564844 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -343,7 +343,13 @@ command [std::unique_ptr<cvc5::Command>* cmd]
   | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
   | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
   | /* value query */
-    GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    GET_VALUE_TOK 
+    {
+      PARSER_STATE->checkThatLogicIsSet();
+      // bind all symbols specific to the model, e.g. uninterpreted constant
+      // values
+      PARSER_STATE->pushGetValueScope();
+    }
     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
       { cmd->reset(new GetValueCommand(terms)); }
     | ~LPAREN_TOK
@@ -352,6 +358,7 @@ command [std::unique_ptr<cvc5::Command>* cmd]
                                  "parentheses?");
       }
     )
+    { PARSER_STATE->popScope(); }
   | /* get-assignment */
     GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd->reset(new GetAssignmentCommand()); }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 81b2bd0c98b74480cc951da30a453c982732a4fc..da6f4c3c9728f0e3467f9a0bd088996271afd78b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -782,6 +782,7 @@ set(regress_0_tests
   regress0/parser/force_logic_set_logic.smt2
   regress0/parser/force_logic_success.smt2
   regress0/parser/issue5163.smt2
+  regress0/parser/issue6908-get-value-uc.smt2
   regress0/parser/issue7274.smt2
   regress0/parser/linear_arithmetic_err1.smt2
   regress0/parser/linear_arithmetic_err2.smt2

diff --git a/test/regress/regress0/parser/issue6908-get-value-uc.smt2 b/test/regress/regress0/parser/issue6908-get-value-uc.smt2
new file mode 100644 (file)
index 0000000..b6825fe
--- /dev/null
+++ b/test/regress/regress0/parser/issue6908-get-value-uc.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --produce-models
+; EXPECT: sat
+; EXPECT: (((f (as @uc_Foo_0 Foo)) 3))
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-sort Foo 0)
+(declare-fun f (Foo) Int)
+(assert (exists ((x Foo)) (= (f x) 3)))
+(check-sat)
+(get-value ((f @uc_Foo_0)))