Add one smallest FQTest

src/Refinements-Tests/FQNegTest.class.st

@@ -0,0 +1,17 @@
+Class {
+	#name : #FQNegTest,
+	#superclass : #FQTest,
+	#category : #'Refinements-Tests'
+}
+
+{ #category : #tests }
+FQNegTest >> testConjRhs [
+	self proveNeg: '
+constraint:
+  env []
+  lhs {v:int | Bool true }
+  rhs {v:int | ((0 toInt < 1) & (1 toInt < 0)) }
+  id 1
+  tag [1]
+'
+]

src/Refinements-Tests/FQPosTest.class.st

@@ -0,0 +1,17 @@
+Class {
+	#name : #FQPosTest,
+	#superclass : #FQTest,
+	#category : #'Refinements-Tests'
+}
+
+{ #category : #tests }
+FQPosTest >> testConjRhs [
+	self provePos: '
+constraint:
+  env []
+  lhs {v:int | Bool true }
+  rhs {v:int | ((0 toInt < 1) & (1 toInt > 0)) }
+  id 1
+  tag [1]
+'
+]

src/Refinements-Tests/FQTest.class.st

@@ -0,0 +1,21 @@
+Class {
+	#name : #FQTest,
+	#superclass : #TestCase,
+	#category : #'Refinements-Tests'
+}
+
+{ #category : #proving }
+FQTest >> proveNeg: txt [
+	| q |
+	q := FQParser parse: txt.
+	self deny: q isPetitFailure.
+	self deny: q solve isSafe
+]
+
+{ #category : #proving }
+FQTest >> provePos: txt [
+	| q |
+	q := FQParser parse: txt.
+	self deny: q isPetitFailure.
+	self assert: q solve isSafe
+]