Skip to content

Commit

Permalink
fix(smt2/parser.yy): Fix name_sort_list
Browse files Browse the repository at this point in the history
Close #245
  • Loading branch information
soonho-tri committed May 26, 2021
1 parent 0d34d44 commit 6d1da9f
Show file tree
Hide file tree
Showing 5 changed files with 26 additions and 7 deletions.
8 changes: 4 additions & 4 deletions dreal/smt2/parser.yy
Original file line number Diff line number Diff line change
Expand Up @@ -522,10 +522,10 @@ name_sort: '(' SYMBOL sort ')' {
;

name_sort_list: /* empty list */ { $$ = std::vector<Variable>{}; }
| name_sort name_sort_list {
const Variable& v = $1;
$2.push_back(v);
$$ = $2;
| name_sort_list name_sort {
const Variable& v = $2;
$1.push_back(v);
$$ = $1;
}
;

Expand Down
4 changes: 2 additions & 2 deletions dreal/test/smt2/define_fun_02.smt2.expected
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
delta-sat with delta = 0.001
z : [-1, -1]
z : [1, 1]
(model
(define-fun z () Real -1)
(define-fun z () Real 1)
)
13 changes: 13 additions & 0 deletions dreal/test/smt2/github_245.smt2
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
(set-logic QF_NRA)
(declare-fun a () Real)
(declare-fun b () Real)
(define-fun get_R ((x Real) (y Real)) Real
(* x (cos y)))
(assert (= a 12))
(assert (= b -0.7853981633974483))
(declare-fun R () Real)
;(assert (= R (* a (cos b))))
(assert (= R (get_R a b)))
(check-sat)
(get-model)

6 changes: 6 additions & 0 deletions dreal/test/smt2/github_245.smt2.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
delta-sat with delta = 0.001
(model
(define-fun a () Real 12)
(define-fun b () Real [-0.78539816339744839, -0.78539816339744828])
(define-fun R () Real [8.4852813742385571, 8.4852813742385855])
)
2 changes: 1 addition & 1 deletion dreal/test/smt2/option_smtlib2_compliant_01.smt2.expected
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
delta-sat
0.001
(
(z (- 1))
(z 1)
)

0 comments on commit 6d1da9f

Please sign in to comment.