satsolver/parser_test.go at master · Harrison-Miller/satsolver · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
package satsolver

import (
	"github.com/stretchr/testify/require"
	"strings"
	"testing"
)

func TestParser(t *testing.T) {
	t.Run("a", func(t *testing.T) {
		f, err := Parse(strings.NewReader("a"))
		require.NoError(t, err)

		require.Len(t, f.C, 1)
		require.Len(t, f.C[0].L, 1)
		require.False(t, f.C[0].L[0].Negated)
		require.Equal(t, "a", f.C[0].L[0].V.Name)
	})

	t.Run("~a", func(t *testing.T) {
		f, err := Parse(strings.NewReader("~a"))
		require.NoError(t, err)

		require.Len(t, f.C, 1)
		require.Len(t, f.C[0].L, 1)
		require.True(t, f.C[0].L[0].Negated)
		require.Equal(t, "a", f.C[0].L[0].V.Name)
	})

	t.Run("a ^ b", func(t *testing.T) {
		f, err := Parse(strings.NewReader("a ^ ~b"))
		require.NoError(t, err)

		require.Len(t, f.C, 2)
		require.Len(t, f.C[0].L, 1)
		require.Len(t, f.C[1].L, 1)

		require.False(t, f.C[0].L[0].Negated)
		require.Equal(t, "a", f.C[0].L[0].V.Name)

		require.True(t, f.C[1].L[0].Negated)
		require.Equal(t, "b", f.C[1].L[0].V.Name)
	})

	t.Run("(a v b)", func(t *testing.T) {
		f, err := Parse(strings.NewReader("(a v b)"))
		require.NoError(t, err)

		require.Len(t, f.C, 1)
		require.Len(t, f.C[0].L, 2)

		require.False(t, f.C[0].L[0].Negated)
		require.Equal(t, "a", f.C[0].L[0].V.Name)

		require.False(t, f.C[0].L[1].Negated)
		require.Equal(t, "b", f.C[0].L[1].V.Name)
	})

	t.Run("a ^ (~b v c) ^ d", func(t *testing.T) {
		f, err := Parse(strings.NewReader("a ^ (~b v c) ^ d"))
		require.NoError(t, err)

		require.Len(t, f.C, 3)
		require.Len(t, f.C[0].L, 1)
		require.Len(t, f.C[1].L, 2)
		require.Len(t, f.C[2].L, 1)

		require.False(t, f.C[0].L[0].Negated)
		require.Equal(t, "a", f.C[0].L[0].V.Name)

		require.True(t, f.C[1].L[0].Negated)
		require.Equal(t, "b", f.C[1].L[0].V.Name)

		require.False(t, f.C[1].L[1].Negated)
		require.Equal(t, "c", f.C[1].L[1].V.Name)

		require.False(t, f.C[2].L[0].Negated)
		require.Equal(t, "d", f.C[2].L[0].V.Name)
	})

	t.Run("a ^ a", func(t *testing.T) {
		f, err := Parse(strings.NewReader("a ^ a"))
		require.NoError(t, err)

		require.Len(t, f.C, 2)
		require.Len(t, f.C[0].L, 1)
		require.Len(t, f.C[1].L, 1)

		require.False(t, f.C[0].L[0].Negated)
		require.Equal(t, "a", f.C[0].L[0].V.Name)

		require.False(t, f.C[1].L[0].Negated)
		require.Equal(t, "a", f.C[1].L[0].V.Name)

		require.Same(t, f.C[0].L[0].V, f.C[1].L[0].V)
	})

}