Skip to content

Commit

Permalink
[Z3] Add test for solver parameter description API
Browse files Browse the repository at this point in the history
This test merely tests that we get back something sensible.
  • Loading branch information
janvrany authored and shingarov committed Jun 25, 2024
1 parent e55127e commit c21b97c
Showing 1 changed file with 17 additions and 1 deletion.
18 changes: 17 additions & 1 deletion src/Z3-Tests/SimpleZ3Test.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -437,7 +437,7 @@ SimpleZ3Test >> testParameterSet [
pset := ('DoReMi' -> 42) toZ3ParameterSet.
self assert: (pset toString asLowercase includesSubstring: 'doremi').

pset := (Dictionary withKeysAndValues:#('foo' 1.0 'bar' 'baz')) toZ3ParameterSet.
pset := (Dictionary newFromPairs: #('foo' 1.0 'bar' 'baz')) toZ3ParameterSet.
self assert: (pset toString asLowercase includesSubstring: 'foo').
self assert: (pset toString asLowercase includesSubstring: 'bar').

Expand Down Expand Up @@ -659,6 +659,22 @@ SimpleZ3Test >> testSolverForLogic [
self assert: solver assertions contents isEmpty
]

{ #category : #tests }
SimpleZ3Test >> testSolverParameterDescriptions [
| solver paramDescrs |

solver := Z3Solver new.
paramDescrs := solver parameterDescriptions.
self assert: paramDescrs size > 0.

"Just test that `Z3ParameterDescriptionSet >> #at:` returns
something sensible."
self assert: (paramDescrs at: 1) name isString.

paramDescrs release.
solver release.
]

{ #category : #tests }
SimpleZ3Test >> testSplitNoOverlap [
| x y solver m |
Expand Down

0 comments on commit c21b97c

Please sign in to comment.