diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-10-28 06:26:49 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-28 11:26:49 +0000 |
commit | 661ed996725b1e4d6dbd7b58b583bcf4da20f530 (patch) | |
tree | cded2326cd1191e790ce387183a4aefbeaba15b8 /test | |
parent | 46f5a39730ebd42421963c23de81a75652fb6629 (diff) |
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.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/bug522.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/options/ast-and-sexpr.smt2 | 3 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/bi-artm-s.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 | 6 |
4 files changed, 7 insertions, 6 deletions
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) |