File tree Expand file tree Collapse file tree 30 files changed +52
-52
lines changed
src/org/sosy_lab/java_smt Expand file tree Collapse file tree 30 files changed +52
-52
lines changed Original file line number Diff line number Diff line change 21
21
22
22
import com .google .errorprone .annotations .CanIgnoreReturnValue ;
23
23
24
- import org .sosy_lab .java_smt .visitors .BooleanFormulaTransformationVisitor ;
25
- import org .sosy_lab .java_smt .visitors .BooleanFormulaVisitor ;
26
- import org .sosy_lab .java_smt .visitors .TraversalProcess ;
24
+ import org .sosy_lab .java_smt .api . visitors .BooleanFormulaTransformationVisitor ;
25
+ import org .sosy_lab .java_smt .api . visitors .BooleanFormulaVisitor ;
26
+ import org .sosy_lab .java_smt .api . visitors .TraversalProcess ;
27
27
28
28
import java .util .Collection ;
29
29
import java .util .Set ;
Original file line number Diff line number Diff line change 22
22
import com .google .errorprone .annotations .CanIgnoreReturnValue ;
23
23
24
24
import org .sosy_lab .common .Appender ;
25
- import org .sosy_lab .java_smt .visitors .FormulaTransformationVisitor ;
26
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
27
- import org .sosy_lab .java_smt .visitors .TraversalProcess ;
25
+ import org .sosy_lab .java_smt .api . visitors .FormulaTransformationVisitor ;
26
+ import org .sosy_lab .java_smt .api . visitors .FormulaVisitor ;
27
+ import org .sosy_lab .java_smt .api . visitors .TraversalProcess ;
28
28
29
29
import java .util .List ;
30
30
import java .util .Map ;
Original file line number Diff line number Diff line change 17
17
* See the License for the specific language governing permissions and
18
18
* limitations under the License.
19
19
*/
20
- package org .sosy_lab .java_smt .visitors ;
20
+ package org .sosy_lab .java_smt .api . visitors ;
21
21
22
22
import com .google .common .collect .Collections2 ;
23
23
Original file line number Diff line number Diff line change 17
17
* See the License for the specific language governing permissions and
18
18
* limitations under the License.
19
19
*/
20
- package org .sosy_lab .java_smt .visitors ;
20
+ package org .sosy_lab .java_smt .api . visitors ;
21
21
22
22
import org .sosy_lab .java_smt .api .BooleanFormula ;
23
23
import org .sosy_lab .java_smt .api .BooleanFormulaManager ;
Original file line number Diff line number Diff line change 17
17
* See the License for the specific language governing permissions and
18
18
* limitations under the License.
19
19
*/
20
- package org .sosy_lab .java_smt .visitors ;
20
+ package org .sosy_lab .java_smt .api . visitors ;
21
21
22
22
import org .sosy_lab .java_smt .api .BooleanFormula ;
23
23
import org .sosy_lab .java_smt .api .Formula ;
Original file line number Diff line number Diff line change 17
17
* See the License for the specific language governing permissions and
18
18
* limitations under the License.
19
19
*/
20
- package org .sosy_lab .java_smt .visitors ;
20
+ package org .sosy_lab .java_smt .api . visitors ;
21
21
22
22
import org .sosy_lab .java_smt .api .BooleanFormula ;
23
23
import org .sosy_lab .java_smt .api .Formula ;
Original file line number Diff line number Diff line change 17
17
* See the License for the specific language governing permissions and
18
18
* limitations under the License.
19
19
*/
20
- package org .sosy_lab .java_smt .visitors ;
20
+ package org .sosy_lab .java_smt .api . visitors ;
21
21
22
22
import org .sosy_lab .java_smt .api .Formula ;
23
23
Original file line number Diff line number Diff line change 17
17
* See the License for the specific language governing permissions and
18
18
* limitations under the License.
19
19
*/
20
- package org .sosy_lab .java_smt .visitors ;
20
+ package org .sosy_lab .java_smt .api . visitors ;
21
21
22
22
import org .sosy_lab .java_smt .api .BooleanFormula ;
23
23
import org .sosy_lab .java_smt .api .Formula ;
Original file line number Diff line number Diff line change 17
17
* See the License for the specific language governing permissions and
18
18
* limitations under the License.
19
19
*/
20
- package org .sosy_lab .java_smt .visitors ;
20
+ package org .sosy_lab .java_smt .api . visitors ;
21
21
22
22
import org .sosy_lab .common .rationals .Rational ;
23
23
import org .sosy_lab .java_smt .api .BooleanFormula ;
Original file line number Diff line number Diff line change 17
17
* See the License for the specific language governing permissions and
18
18
* limitations under the License.
19
19
*/
20
- package org .sosy_lab .java_smt .visitors ;
20
+ package org .sosy_lab .java_smt .api . visitors ;
21
21
22
22
import com .google .common .collect .ImmutableSet ;
23
23
Original file line number Diff line number Diff line change 22
22
* The visitors of this package allow for efficient traversal, manipulation
23
23
* and transformation of formulas.
24
24
*/
25
- package org .sosy_lab .java_smt .visitors ;
25
+ package org .sosy_lab .java_smt .api . visitors ;
Original file line number Diff line number Diff line change 35
35
import org .sosy_lab .java_smt .api .FunctionDeclaration ;
36
36
import org .sosy_lab .java_smt .api .FunctionDeclarationKind ;
37
37
import org .sosy_lab .java_smt .api .QuantifiedFormulaManager .Quantifier ;
38
- import org .sosy_lab .java_smt .visitors .BooleanFormulaTransformationVisitor ;
39
- import org .sosy_lab .java_smt .visitors .BooleanFormulaVisitor ;
40
- import org .sosy_lab .java_smt .visitors .DefaultFormulaVisitor ;
41
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
42
- import org .sosy_lab .java_smt .visitors .TraversalProcess ;
38
+ import org .sosy_lab .java_smt .api . visitors .BooleanFormulaTransformationVisitor ;
39
+ import org .sosy_lab .java_smt .api . visitors .BooleanFormulaVisitor ;
40
+ import org .sosy_lab .java_smt .api . visitors .DefaultFormulaVisitor ;
41
+ import org .sosy_lab .java_smt .api . visitors .FormulaVisitor ;
42
+ import org .sosy_lab .java_smt .api . visitors .TraversalProcess ;
43
43
44
44
import java .util .ArrayDeque ;
45
45
import java .util .Arrays ;
Original file line number Diff line number Diff line change 35
35
import org .sosy_lab .java_smt .api .IntegerFormulaManager ;
36
36
import org .sosy_lab .java_smt .api .RationalFormulaManager ;
37
37
import org .sosy_lab .java_smt .api .Tactic ;
38
+ import org .sosy_lab .java_smt .api .visitors .FormulaTransformationVisitor ;
39
+ import org .sosy_lab .java_smt .api .visitors .FormulaVisitor ;
40
+ import org .sosy_lab .java_smt .api .visitors .TraversalProcess ;
38
41
import org .sosy_lab .java_smt .basicimpl .tactics .NNFVisitor ;
39
42
import org .sosy_lab .java_smt .basicimpl .tactics .UfElimination ;
40
- import org .sosy_lab .java_smt .visitors .FormulaTransformationVisitor ;
41
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
42
- import org .sosy_lab .java_smt .visitors .TraversalProcess ;
43
43
44
44
import java .util .Arrays ;
45
45
import java .util .List ;
Original file line number Diff line number Diff line change 37
37
import org .sosy_lab .java_smt .api .FunctionDeclarationKind ;
38
38
import org .sosy_lab .java_smt .api .NumeralFormula .IntegerFormula ;
39
39
import org .sosy_lab .java_smt .api .NumeralFormula .RationalFormula ;
40
+ import org .sosy_lab .java_smt .api .visitors .DefaultFormulaVisitor ;
41
+ import org .sosy_lab .java_smt .api .visitors .FormulaVisitor ;
42
+ import org .sosy_lab .java_smt .api .visitors .TraversalProcess ;
40
43
import org .sosy_lab .java_smt .basicimpl .AbstractFormula .ArrayFormulaImpl ;
41
44
import org .sosy_lab .java_smt .basicimpl .AbstractFormula .BitvectorFormulaImpl ;
42
45
import org .sosy_lab .java_smt .basicimpl .AbstractFormula .BooleanFormulaImpl ;
43
46
import org .sosy_lab .java_smt .basicimpl .AbstractFormula .FloatingPointFormulaImpl ;
44
47
import org .sosy_lab .java_smt .basicimpl .AbstractFormula .FloatingPointRoundingModeFormulaImpl ;
45
48
import org .sosy_lab .java_smt .basicimpl .AbstractFormula .IntegerFormulaImpl ;
46
49
import org .sosy_lab .java_smt .basicimpl .AbstractFormula .RationalFormulaImpl ;
47
- import org .sosy_lab .java_smt .visitors .DefaultFormulaVisitor ;
48
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
49
- import org .sosy_lab .java_smt .visitors .TraversalProcess ;
50
50
51
51
import java .util .ArrayDeque ;
52
52
import java .util .Deque ;
Original file line number Diff line number Diff line change 25
25
import org .sosy_lab .java_smt .api .Formula ;
26
26
import org .sosy_lab .java_smt .api .FunctionDeclaration ;
27
27
import org .sosy_lab .java_smt .api .QuantifiedFormulaManager .Quantifier ;
28
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
28
+ import org .sosy_lab .java_smt .api . visitors .FormulaVisitor ;
29
29
30
30
import java .util .ArrayList ;
31
31
import java .util .Deque ;
Original file line number Diff line number Diff line change 27
27
import org .sosy_lab .java_smt .api .Formula ;
28
28
import org .sosy_lab .java_smt .api .FunctionDeclaration ;
29
29
import org .sosy_lab .java_smt .api .QuantifiedFormulaManager .Quantifier ;
30
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
31
- import org .sosy_lab .java_smt .visitors .TraversalProcess ;
32
- import org .sosy_lab .java_smt .visitors .TraversalProcess .TraversalType ;
30
+ import org .sosy_lab .java_smt .api . visitors .FormulaVisitor ;
31
+ import org .sosy_lab .java_smt .api . visitors .TraversalProcess ;
32
+ import org .sosy_lab .java_smt .api . visitors .TraversalProcess .TraversalType ;
33
33
34
34
import java .util .ArrayDeque ;
35
35
import java .util .Deque ;
Original file line number Diff line number Diff line change 24
24
import org .sosy_lab .java_smt .api .BooleanFormulaManager ;
25
25
import org .sosy_lab .java_smt .api .FormulaManager ;
26
26
import org .sosy_lab .java_smt .api .FunctionDeclaration ;
27
- import org .sosy_lab .java_smt .visitors .BooleanFormulaTransformationVisitor ;
27
+ import org .sosy_lab .java_smt .api . visitors .BooleanFormulaTransformationVisitor ;
28
28
29
29
import java .util .ArrayList ;
30
30
import java .util .List ;
Original file line number Diff line number Diff line change 47
47
import org .sosy_lab .java_smt .api .NumeralFormula .IntegerFormula ;
48
48
import org .sosy_lab .java_smt .api .QuantifiedFormulaManager ;
49
49
import org .sosy_lab .java_smt .api .QuantifiedFormulaManager .Quantifier ;
50
- import org .sosy_lab .java_smt .visitors .DefaultFormulaVisitor ;
51
- import org .sosy_lab .java_smt .visitors .TraversalProcess ;
50
+ import org .sosy_lab .java_smt .api . visitors .DefaultFormulaVisitor ;
51
+ import org .sosy_lab .java_smt .api . visitors .TraversalProcess ;
52
52
53
53
import java .util .ArrayList ;
54
54
import java .util .Collection ;
Original file line number Diff line number Diff line change 30
30
import org .sosy_lab .java_smt .api .FunctionDeclarationKind ;
31
31
import org .sosy_lab .java_smt .api .InterpolatingProverEnvironment ;
32
32
import org .sosy_lab .java_smt .api .SolverException ;
33
- import org .sosy_lab .java_smt .visitors .BooleanFormulaTransformationVisitor ;
33
+ import org .sosy_lab .java_smt .api . visitors .BooleanFormulaTransformationVisitor ;
34
34
35
35
import java .util .ArrayList ;
36
36
import java .util .Collection ;
Original file line number Diff line number Diff line change 19
19
import org .sosy_lab .java_smt .api .ProverEnvironment ;
20
20
import org .sosy_lab .java_smt .api .SolverContext ;
21
21
import org .sosy_lab .java_smt .api .SolverContext .ProverOptions ;
22
- import org .sosy_lab .java_smt .visitors .FormulaTransformationVisitor ;
22
+ import org .sosy_lab .java_smt .api . visitors .FormulaTransformationVisitor ;
23
23
24
24
import java .util .ArrayList ;
25
25
import java .util .HashMap ;
Original file line number Diff line number Diff line change 80
80
import org .sosy_lab .java_smt .api .FormulaType .ArrayFormulaType ;
81
81
import org .sosy_lab .java_smt .api .FormulaType .FloatingPointType ;
82
82
import org .sosy_lab .java_smt .api .FunctionDeclarationKind ;
83
+ import org .sosy_lab .java_smt .api .visitors .FormulaVisitor ;
83
84
import org .sosy_lab .java_smt .basicimpl .FormulaCreator ;
84
85
import org .sosy_lab .java_smt .basicimpl .FunctionDeclarationImpl ;
85
86
import org .sosy_lab .java_smt .solvers .mathsat5 .Mathsat5Formula .Mathsat5ArrayFormula ;
89
90
import org .sosy_lab .java_smt .solvers .mathsat5 .Mathsat5Formula .Mathsat5FloatingPointRoundingModeFormula ;
90
91
import org .sosy_lab .java_smt .solvers .mathsat5 .Mathsat5Formula .Mathsat5IntegerFormula ;
91
92
import org .sosy_lab .java_smt .solvers .mathsat5 .Mathsat5Formula .Mathsat5RationalFormula ;
92
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
93
93
94
94
import java .math .BigInteger ;
95
95
import java .util .List ;
Original file line number Diff line number Diff line change 53
53
import org .sosy_lab .java_smt .api .FormulaType ;
54
54
import org .sosy_lab .java_smt .api .FormulaType .ArrayFormulaType ;
55
55
import org .sosy_lab .java_smt .api .FunctionDeclarationKind ;
56
+ import org .sosy_lab .java_smt .api .visitors .FormulaVisitor ;
56
57
import org .sosy_lab .java_smt .basicimpl .FormulaCreator ;
57
58
import org .sosy_lab .java_smt .basicimpl .FunctionDeclarationImpl ;
58
59
import org .sosy_lab .java_smt .solvers .princess .PrincessFunctionDeclaration .PrincessByExampleDeclaration ;
59
60
import org .sosy_lab .java_smt .solvers .princess .PrincessFunctionDeclaration .PrincessIFunctionDeclaration ;
60
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
61
61
62
62
import scala .Enumeration ;
63
63
Original file line number Diff line number Diff line change 36
36
import org .sosy_lab .java_smt .api .FormulaType ;
37
37
import org .sosy_lab .java_smt .api .FormulaType .ArrayFormulaType ;
38
38
import org .sosy_lab .java_smt .api .FunctionDeclarationKind ;
39
+ import org .sosy_lab .java_smt .api .visitors .FormulaVisitor ;
39
40
import org .sosy_lab .java_smt .basicimpl .FormulaCreator ;
40
41
import org .sosy_lab .java_smt .basicimpl .FunctionDeclarationImpl ;
41
42
import org .sosy_lab .java_smt .basicimpl .ObjectArrayBackedList ;
42
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
43
43
44
44
import java .util .List ;
45
45
Original file line number Diff line number Diff line change 35
35
import org .sosy_lab .java_smt .api .BooleanFormula ;
36
36
import org .sosy_lab .java_smt .api .Formula ;
37
37
import org .sosy_lab .java_smt .api .FormulaType ;
38
+ import org .sosy_lab .java_smt .api .visitors .FormulaVisitor ;
38
39
import org .sosy_lab .java_smt .basicimpl .AbstractFormulaManager ;
39
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
40
40
41
41
import java .io .IOException ;
42
42
import java .util .ArrayDeque ;
Original file line number Diff line number Diff line change 53
53
import org .sosy_lab .java_smt .api .FunctionDeclarationKind ;
54
54
import org .sosy_lab .java_smt .api .QuantifiedFormulaManager .Quantifier ;
55
55
import org .sosy_lab .java_smt .api .SolverException ;
56
+ import org .sosy_lab .java_smt .api .visitors .FormulaVisitor ;
56
57
import org .sosy_lab .java_smt .basicimpl .FormulaCreator ;
57
58
import org .sosy_lab .java_smt .basicimpl .FunctionDeclarationImpl ;
58
59
import org .sosy_lab .java_smt .solvers .z3 .Z3Formula .Z3ArrayFormula ;
62
63
import org .sosy_lab .java_smt .solvers .z3 .Z3Formula .Z3FloatingPointRoundingModeFormula ;
63
64
import org .sosy_lab .java_smt .solvers .z3 .Z3Formula .Z3IntegerFormula ;
64
65
import org .sosy_lab .java_smt .solvers .z3 .Z3Formula .Z3RationalFormula ;
65
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
66
66
67
67
import java .lang .ref .PhantomReference ;
68
68
import java .lang .ref .Reference ;
Original file line number Diff line number Diff line change 35
35
import org .sosy_lab .java_smt .api .InterpolatingProverEnvironment ;
36
36
import org .sosy_lab .java_smt .api .QuantifiedFormulaManager .Quantifier ;
37
37
import org .sosy_lab .java_smt .api .SolverException ;
38
- import org .sosy_lab .java_smt .visitors .DefaultFormulaVisitor ;
39
- import org .sosy_lab .java_smt .visitors .TraversalProcess ;
38
+ import org .sosy_lab .java_smt .api . visitors .DefaultFormulaVisitor ;
39
+ import org .sosy_lab .java_smt .api . visitors .TraversalProcess ;
40
40
41
41
import java .io .IOException ;
42
42
import java .io .Writer ;
Original file line number Diff line number Diff line change 42
42
import org .sosy_lab .java_smt .api .QuantifiedFormulaManager .Quantifier ;
43
43
import org .sosy_lab .java_smt .api .SolverException ;
44
44
import org .sosy_lab .java_smt .api .Tactic ;
45
- import org .sosy_lab .java_smt .visitors .DefaultFormulaVisitor ;
45
+ import org .sosy_lab .java_smt .api . visitors .DefaultFormulaVisitor ;
46
46
47
47
import java .util .ArrayList ;
48
48
import java .util .List ;
Original file line number Diff line number Diff line change 43
43
import org .sosy_lab .java_smt .api .QuantifiedFormulaManager .Quantifier ;
44
44
import org .sosy_lab .java_smt .api .SolverException ;
45
45
import org .sosy_lab .java_smt .api .Tactic ;
46
- import org .sosy_lab .java_smt .visitors .BooleanFormulaVisitor ;
46
+ import org .sosy_lab .java_smt .api . visitors .BooleanFormulaVisitor ;
47
47
48
48
import java .util .ArrayList ;
49
49
import java .util .List ;
Original file line number Diff line number Diff line change 36
36
import org .sosy_lab .java_smt .api .FunctionDeclaration ;
37
37
import org .sosy_lab .java_smt .api .FunctionDeclarationKind ;
38
38
import org .sosy_lab .java_smt .api .NumeralFormula .IntegerFormula ;
39
- import org .sosy_lab .java_smt .visitors .BooleanFormulaTransformationVisitor ;
40
- import org .sosy_lab .java_smt .visitors .BooleanFormulaVisitor ;
41
- import org .sosy_lab .java_smt .visitors .DefaultBooleanFormulaVisitor ;
42
- import org .sosy_lab .java_smt .visitors .DefaultFormulaVisitor ;
43
- import org .sosy_lab .java_smt .visitors .FormulaTransformationVisitor ;
44
- import org .sosy_lab .java_smt .visitors .FormulaVisitor ;
45
- import org .sosy_lab .java_smt .visitors .TraversalProcess ;
39
+ import org .sosy_lab .java_smt .api . visitors .BooleanFormulaTransformationVisitor ;
40
+ import org .sosy_lab .java_smt .api . visitors .BooleanFormulaVisitor ;
41
+ import org .sosy_lab .java_smt .api . visitors .DefaultBooleanFormulaVisitor ;
42
+ import org .sosy_lab .java_smt .api . visitors .DefaultFormulaVisitor ;
43
+ import org .sosy_lab .java_smt .api . visitors .FormulaTransformationVisitor ;
44
+ import org .sosy_lab .java_smt .api . visitors .FormulaVisitor ;
45
+ import org .sosy_lab .java_smt .api . visitors .TraversalProcess ;
46
46
47
47
import java .util .ArrayList ;
48
48
import java .util .HashSet ;
Original file line number Diff line number Diff line change 32
32
import org .sosy_lab .java_smt .api .Formula ;
33
33
import org .sosy_lab .java_smt .api .FormulaType ;
34
34
import org .sosy_lab .java_smt .api .FunctionDeclaration ;
35
- import org .sosy_lab .java_smt .visitors .ExpectedFormulaVisitor ;
35
+ import org .sosy_lab .java_smt .api . visitors .ExpectedFormulaVisitor ;
36
36
37
37
import java .util .List ;
38
38
You can’t perform that action at this time.
0 commit comments