@@ -25,126 +25,90 @@ public void init() {
25
25
}
26
26
27
27
@ Test
28
- public void validLogicTest () throws SolverException , InterruptedException {
28
+ public void logicTest () throws SolverException , InterruptedException {
29
+ // Valid input string that sets the logic to QF_ALL
29
30
BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
30
- BooleanFormula broken =
31
+ BooleanFormula validLogic =
31
32
mgr .parse ("(set-logic QF_ALL)" + "(declare-const v Int)" + "(assert (= v 3))" );
32
- assertThatFormula (expected ).isEquivalentTo (broken );
33
- }
33
+ assertThatFormula (expected ).isEquivalentTo (validLogic );
34
34
35
- @ Test
36
- public void wrongLogicTest () {
37
- // When we change the code to not use sanitize() solver seem to just ignore set-logic
38
- // Except for OpenSMT, which always crashes
39
- assertThrows (
40
- IllegalArgumentException .class ,
41
- () -> mgr .parse ("(set-logic QF_UF)" + "(declare-const v Int)" + "(assert (= v 3))" ));
42
- }
35
+ // Invalid string that sets QF_UF, even though integers are needed
36
+ // Most solvers seem to just ignore the logic that was chosen
37
+ String wrongLogic = "(set-logic QF_UF)" + "(declare-const v Int)" + "(assert (= v 3))" ;
38
+ assertThrows (IllegalArgumentException .class , () -> mgr .parse (wrongLogic ));
43
39
44
- @ Test
45
- public void logicAfterOptionTest () {
46
- BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
47
- assertThrows (
48
- IllegalArgumentException .class ,
49
- () ->
50
- mgr .parse (
51
- "(set-option :produce-models true)"
52
- + "(set-logic ALL)"
53
- + "(declare-const v Int)"
54
- + "(assert (= v 3))" ));
55
- }
40
+ // Try setting logic after another command was already used
41
+ String logicAfterOption =
42
+ "(set-option :produce-models true)"
43
+ + "(set-logic ALL)"
44
+ + "(declare-const v Int)"
45
+ + "(assert (= v 3))" ;
46
+ assertThrows (IllegalArgumentException .class , () -> mgr .parse (logicAfterOption ));
56
47
57
- @ Test
58
- public void logicUsedTwiceTest () {
59
- BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
60
- assertThrows (
61
- IllegalArgumentException .class ,
62
- () ->
63
- mgr .parse (
64
- "(set-logic ALL)"
65
- + "(declare-const v Int)"
66
- + "(set-logic QF_UF)"
67
- + "(assert (= v 3))" ));
48
+ // Try setting the logic again after it has already been set
49
+ String logicTwice =
50
+ "(set-logic ALL)" + "(declare-const v Int)" + "(set-logic QF_UF)" + " (assert (= v 3))" ;
51
+ assertThrows (IllegalArgumentException .class , () -> mgr .parse (logicTwice ));
52
+
53
+ // Call (reset) and *then* set the logic again
54
+ String logicReset =
55
+ "(set-logic QF_UF)"
56
+ + "(reset)"
57
+ + "(set-logic ALL)"
58
+ + "(declare-const v Int)"
59
+ + "(assert (= v 3))" ;
60
+ assertThatFormula (mgr .parse (logicReset )).isEquivalentTo (expected );
68
61
}
69
62
70
63
@ Test
71
64
public void exitAtTheEnd () throws SolverException , InterruptedException {
72
- BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
73
- BooleanFormula broken = mgr .parse ("(declare-const v Int)" + "(assert (= v 3))" + "(exit)" );
74
- assertThatFormula (expected ).isEquivalentTo (broken );
75
- }
65
+ BooleanFormula expected = mgr .parse ("(declare-const v Int)" + "(assert (= v 3))" );
76
66
77
- @ Test
78
- public void exitNotTheEnd () {
79
- assertThrows (
80
- IllegalArgumentException .class ,
81
- () ->
82
- mgr .parse (
83
- "(declare-const v Int)" + "(assert (= v 3))" + "(exit)" + "(assert (= v 0))" ));
84
- }
67
+ // A valid input string with (exit) at the end
68
+ BooleanFormula exitAtTheEnd =
69
+ mgr .parse ("(declare-const v Int)" + "(assert (= v 3))" + "(exit)" );
70
+ assertThatFormula (expected ).isEquivalentTo (exitAtTheEnd );
85
71
86
- @ Test
87
- public void logicResetTest () throws SolverException , InterruptedException {
88
- BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
89
- BooleanFormula broken =
90
- mgr .parse (
91
- "(set-logic QF_UF)"
92
- + "(reset)"
93
- + "(set-logic ALL)"
94
- + "(declare-const v Int)"
95
- + "(assert (= v 3))" );
96
- assertThatFormula (expected ).isEquivalentTo (broken );
72
+ // An invalid input string where (exit) is used before the end of the file
73
+ String exitNotAtTheEnd =
74
+ "(declare-const v Int)" + "(assert (= v 3))" + "(exit)" + "(assert (= v 0))" ;
75
+ assertThrows (IllegalArgumentException .class , () -> mgr .parse (exitNotAtTheEnd ));
97
76
}
98
77
99
78
@ Test
100
79
public void stackPushTest () throws SolverException , InterruptedException {
101
80
BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
102
- BooleanFormula broken =
103
- mgr .parse (
104
- "(declare-const v Int)"
105
- + "(push 1)"
106
- + "(assert (= v 0))"
107
- + "(pop 1)"
108
- + "(assert (= v 3))" );
109
- assertThatFormula (expected ).isEquivalentTo (broken );
110
- }
111
81
112
- @ Test
113
- public void stackResetAssertionsTest () throws SolverException , InterruptedException {
114
- BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
115
- BooleanFormula broken =
116
- mgr .parse (
117
- "(declare-const v Int)"
118
- + "(assert (= v 3))"
119
- + "(reset-assertions)"
120
- + "(declare-const v Int)"
121
- + "(assert (= v 0))" );
122
- assertThatFormula (expected ).isEquivalentTo (broken );
123
- }
82
+ // Push assertions and then pop the stack to remove them
83
+ String stackPush =
84
+ "(declare-const v Int)" + "(push 1)" + "(assert (= v 0))" + "(pop 1)" + "(assert (= v 3))" ;
85
+ assertThatFormula (mgr .parse (stackPush )).isEquivalentTo (expected );
124
86
125
- @ Test
126
- public void globalStackResetAssertionsTest () throws SolverException , InterruptedException {
127
- BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
128
- BooleanFormula broken =
129
- mgr .parse (
130
- "(set-option :global-declarations true)"
131
- + "(declare-const v Int)"
132
- + "(assert (= v 3))"
133
- + "(reset-assertions)"
134
- + "(assert (= v 0))" );
135
- assertThatFormula (expected ).isEquivalentTo (broken );
136
- }
87
+ // Use (reset-assertions) to remove all assertions from the stack
88
+ String stackResetAssertions =
89
+ "(declare-const v Int)"
90
+ + "(assert (= v 3))"
91
+ + "(reset-assertions)"
92
+ + "(declare-const v Int)"
93
+ + "(assert (= v 0))" ;
94
+ assertThatFormula ((mgr .parse (stackResetAssertions ))).isEquivalentTo (expected );
137
95
138
- @ Test
139
- public void stackResetTest () throws SolverException , InterruptedException {
140
- BooleanFormula expected = mgr .parse ("(declare-const v Int)(assert (= v 3))" );
141
- BooleanFormula broken =
142
- mgr .parse (
143
- "(declare-const v Int)"
144
- + "(assert (= v 0))"
145
- + "(reset)"
146
- + "(declare-const v Int)"
147
- + "(assert (= v 3))" );
148
- assertThatFormula (expected ).isEquivalentTo (broken );
96
+ // With :global-declarations the reset will also remove all declarations
97
+ String globalStackResetAssertions =
98
+ "(set-option :global-declarations true)"
99
+ + "(declare-const v Int)"
100
+ + "(assert (= v 3))"
101
+ + "(reset-assertions)"
102
+ + "(assert (= v 0))" ;
103
+ assertThatFormula (mgr .parse (globalStackResetAssertions )).isEquivalentTo (expected );
104
+
105
+ // Just calling (reset) will also clear the stack
106
+ String stackReset =
107
+ "(declare-const v Int)"
108
+ + "(assert (= v 0))"
109
+ + "(reset)"
110
+ + "(declare-const v Int)"
111
+ + "(assert (= v 3))" ;
112
+ assertThatFormula (mgr .parse (stackReset )).isEquivalentTo (expected );
149
113
}
150
114
}
0 commit comments