From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Thu, 28 Oct 2021 11:26:49 +0000 (-0500)
Subject: Fix `(set-info <sexpr>)` parsing and printing bugs. (#7427)
X-Git-Tag: cvc5-1.0.0~945
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=661ed996725b1e4d6dbd7b58b583bcf4da20f530;p=cvc5.git

Fix `(set-info <sexpr>)` parsing and printing bugs. (#7427)

Given
```smt2
(set-info :source (0 1 True False x ""))
```
`cvc5` currently prints the command below with `-o raw-benchmark`
```smt2
(set-info : |(0 1 True False x )|)
```
This PR ensures that `cvc5` correctly prints the command by
- Parsing and storing keywords eagerly before parsing their values.
- Removing pre-processing steps done to symbols and string literals.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e3aee250e..696eb6ad4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -735,10 +735,8 @@ setInfoInternal[std::unique_ptr<cvc5::Command>* cmd]
   std::string name;
   api::Term sexpr;
 }
-  : KEYWORD symbolicExpr[sexpr]
-    { name = AntlrInput::tokenText($KEYWORD);
-      cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr)));
-    }
+  : keyword[name] symbolicExpr[sexpr]
+    { cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr))); }
   ;
 
 setOptionInternal[std::unique_ptr<cvc5::Command>* cmd]
@@ -1247,8 +1245,12 @@ simpleSymbolicExprNoKeyword[std::string& s]
     { s = AntlrInput::tokenText($HEX_LITERAL); }
   | BINARY_LITERAL
     { s = AntlrInput::tokenText($BINARY_LITERAL); }
-  | str[s,false]
-  | symbol[s,CHECK_NONE,SYM_SORT]
+  | SIMPLE_SYMBOL
+    { s = AntlrInput::tokenText($SIMPLE_SYMBOL); }
+  | QUOTED_SYMBOL
+    { s = AntlrInput::tokenText($QUOTED_SYMBOL); }
+  | STRING_LITERAL
+    { s = AntlrInput::tokenText($STRING_LITERAL); }
   | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
         | DECLARE_SORT_TOK
         | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK
@@ -1839,16 +1841,16 @@ attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr]
       api::Term n = SOLVER->mkInteger(sIntLit.str());
       retExpr = MK_TERM(api::INST_ATTRIBUTE, keyword, n);
     }
-  | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr]
+  | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbol[s,CHECK_UNDECLARED,SYM_VARIABLE]
     {
       api::Term keyword = SOLVER->mkString("qid");
-      api::Term name = SOLVER->mkString(sexprToString(sexpr));
+      api::Term name = SOLVER->mkString(s);
       retExpr = MK_TERM(api::INST_ATTRIBUTE, keyword, name);
     }
-  | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
+  | ATTRIBUTE_NAMED_TOK symbol[s,CHECK_UNDECLARED,SYM_VARIABLE]
     {
       // notify that expression was given a name
-      PARSER_STATE->notifyNamedExpression(expr, sexprToString(sexpr));
+      PARSER_STATE->notifyNamedExpression(expr, s);
     }
   ;
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index ccb2ed2c6..171f8e524 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1617,8 +1617,7 @@ void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
                                      const std::string& flag,
                                      const std::string& value) const
 {
-  out << "(set-info :" << flag << " " << cvc5::quoteSymbol(value) << ")"
-      << std::endl;
+  out << "(set-info :" << flag << " " << value << ")" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
diff --git a/test/regress/regress0/bug522.smt2 b/test/regress/regress0/bug522.smt2
index 3a9ea0eaa..ad6e526a8 100644
--- a/test/regress/regress0/bug522.smt2
+++ b/test/regress/regress0/bug522.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: sat
 ; EXPECT: sat
-(set-option :incremental "true")
+(set-option :incremental true)
 (set-logic QF_UF)
 
 (push 1)
diff --git a/test/regress/regress0/options/ast-and-sexpr.smt2 b/test/regress/regress0/options/ast-and-sexpr.smt2
index 2a464571c..41012f888 100644
--- a/test/regress/regress0/options/ast-and-sexpr.smt2
+++ b/test/regress/regress0/options/ast-and-sexpr.smt2
@@ -13,5 +13,6 @@
 (get-option :command-verbosity)
 ; There is no SMT option to get the verbosity of a specific command
 
-(set-info :source (0 1 True False x ""))
+(set-info :source (true false (- 15) 15 15.0 #b00001111 #x0f x |x 
+"| "" """"))
 (get-info :status)
diff --git a/test/regress/regress1/quantifiers/bi-artm-s.smt2 b/test/regress/regress1/quantifiers/bi-artm-s.smt2
index af8ee945d..9c6b821b5 100644
--- a/test/regress/regress1/quantifiers/bi-artm-s.smt2
+++ b/test/regress/regress1/quantifiers/bi-artm-s.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --fmf-bound-lazy
 ; EXPECT: unsat
-(set-option :incremental "false")
+(set-option :incremental false)
 (set-info :status unsat)
 (set-logic ALL)
 (declare-fun Y () String)
diff --git a/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2
index c0b3aac7c..4a132a39b 100644
--- a/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2
+++ b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed
-; COMMAND-LINE: --full-saturate-quant --ee-mode=central
+; COMMAND-LINE: -q --full-saturate-quant --ee-mode=distributed
+; COMMAND-LINE: -q --full-saturate-quant --ee-mode=central
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
@@ -23,7 +23,7 @@
 (declare-fun $Event_EventHandleGenerator_type_value () T@$TypeValue)
 (assert (= 0 (|l#R| $EmptyValueArray)))
 (assert (forall ((v1 T@$Value) (v2 T@$Value)) (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (forall ((i Int)) (or (> 0 i) (>= i (|l#R| (|v#V| v1))) ($IsEqual_stratified (sel (|v#R| (|v#V| v1)) i) (sel (|v#R| (|v#V| v2)) i))))))))
-(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid :skolemid)))
+(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid || :skolemid ||)))
 (declare-fun |Select_[$Location]$bool| (b T@$Location) Bool)
 (declare-fun $m@@0 () T@M)
 (declare-fun $abort_flag@2 () Bool)