Prover: adds unit benchmark for symbolic expressions (#3885)

* bench(expr): Creates a unit-benchmark to help optimizing the expressions
* adds the cbor attribute
* commit zip file instead of the plain cbor object

.gitattributes

@@ -17,7 +17,9 @@
 *.ssz binary
 *.ssz_snappy binary
 *.png binary
+*.cbor binary
 
+prover/symbolic/testdata/**/*.cbor binary
 prover/prover-assets/**/**/**/*.bin binary
 prover/prover-assets/**/**/**/**/*.bin binary
 prover/prover-assets/kzgsrs/* binary

prover/go.mod

@@ -11,6 +11,7 @@ require (
 	github.com/consensys/gnark-crypto v0.13.1-0.20240802214859-ff4c0ddbe1ef
 	github.com/crate-crypto/go-kzg-4844 v1.1.0
 	github.com/dlclark/regexp2 v1.11.2
+	github.com/fxamacker/cbor/v2 v2.7.0
 	github.com/go-playground/validator/v10 v10.22.0
 	github.com/iancoleman/strcase v0.3.0
 	github.com/icza/bitio v1.1.0
@@ -48,7 +49,6 @@ require (
 	github.com/ethereum/go-verkle v0.1.1-0.20240306133620-7d920df305f0 // indirect
 	github.com/felixge/fgprof v0.9.4 // indirect
 	github.com/fsnotify/fsnotify v1.7.0 // indirect
-	github.com/fxamacker/cbor/v2 v2.7.0 // indirect
 	github.com/gabriel-vasile/mimetype v1.4.4 // indirect
 	github.com/getsentry/sentry-go v0.28.1 // indirect
 	github.com/go-ole/go-ole v1.3.0 // indirect

prover/protocol/serialization/implementation_registry.go

@@ -61,6 +61,7 @@ func init() {
 	RegisterImplementation(accessors.FromUnivXAccessor{})
 	RegisterImplementation(variables.X{})
 	RegisterImplementation(variables.PeriodicSample{})
+	RegisterImplementation(symbolic.StringVar(""))
 }
 
 // In order to save some space, we trim the prefix of the package path as this

prover/protocol/serialization/pure_expression.go

@@ -0,0 +1,55 @@
+package serialization
+
+import (
+	"fmt"
+	"io"
+	"reflect"
+
+	"github.com/consensys/zkevm-monorepo/prover/symbolic"
+	"github.com/consensys/zkevm-monorepo/prover/utils"
+)
+
+// UnmarshalExprCBOR reads a [symbolic.Expression] from a CBOR-encoded reader.
+// It panics on failure as this function is meant to read test-files for
+// the symbolic package.
+func UnmarshalExprCBOR(r io.Reader) *symbolic.Expression {
+
+	buf, err := io.ReadAll(r)
+	if err != nil {
+		utils.Panic("error while [io.ReadAll]: %v", err)
+	}
+
+	exprVal, err := DeserializeValue(
+		buf,
+		pureExprMode,
+		reflect.TypeOf(&symbolic.Expression{}),
+		nil,
+	)
+
+	if err != nil {
+		utils.Panic("DeserializeValue returned an error for expression: %v", err)
+	}
+
+	return exprVal.Interface().(*symbolic.Expression)
+}
+
+// MarshalExprCBOR marshals a [symbolic.Expression] using CBOR encoding and
+// writes the encoded result into `w`.
+func MarshalExprCBOR(w io.Writer, expr *symbolic.Expression) (int64, error) {
+
+	blob, err := SerializeValue(
+		reflect.ValueOf(expr),
+		pureExprMode,
+	)
+
+	if err != nil {
+		return 0, fmt.Errorf("could not serialize the expression with SerializeValue: %w", err)
+	}
+
+	n, err := w.Write(blob)
+	if err != nil {
+		return 0, fmt.Errorf("could not write the blob: %w", err)
+	}
+
+	return int64(n), nil
+}

prover/protocol/serialization/pure_expression_test.go

@@ -0,0 +1,79 @@
+package serialization
+
+import (
+	"bytes"
+	"fmt"
+	"testing"
+
+	"github.com/consensys/zkevm-monorepo/prover/protocol/column"
+	sym "github.com/consensys/zkevm-monorepo/prover/symbolic"
+)
+
+func TestPureExpr(t *testing.T) {
+
+	var (
+		stringA      = sym.NewDummyVar("a")
+		stringB      = sym.NewDummyVar("b")
+		comp         = newEmptyCompiledIOP()
+		colA         = comp.InsertColumn(0, "a", 16, column.Committed)
+		colB         = comp.InsertColumn(0, "b", 16, column.Committed)
+		exprBuilders = []func(a, b any) *sym.Expression{
+			func(a, b any) *sym.Expression {
+				return sym.Mul(a, b)
+			},
+			func(a, b any) *sym.Expression {
+				return sym.Mul(a, b, 1)
+			},
+			func(a, b any) *sym.Expression {
+				return sym.Add(a, b)
+			},
+			func(a, b any) *sym.Expression {
+				return sym.Add(a, b, 1)
+			},
+			func(a, b any) *sym.Expression {
+				return sym.Sub(a, b)
+			},
+			func(a, b any) *sym.Expression {
+				return sym.Sub(a, b, 1)
+			},
+		}
+	)
+
+	t.Run("without-comp", func(t *testing.T) {
+		for i := range exprBuilders {
+			t.Run(fmt.Sprintf("expression-%v", i), func(t *testing.T) {
+
+				var (
+					e       = exprBuilders[i](stringA, stringB)
+					buf     = &bytes.Buffer{}
+					_, errW = MarshalExprCBOR(buf, e)
+				)
+
+				if errW != nil {
+					t.Fatalf("failed writing the expression: %v", errW.Error())
+				}
+
+				_ = UnmarshalExprCBOR(buf)
+			})
+		}
+	})
+
+	t.Run("with-comp", func(t *testing.T) {
+		for i := range exprBuilders {
+			t.Run(fmt.Sprintf("expression-%v", i), func(t *testing.T) {
+
+				var (
+					e       = exprBuilders[i](colA, colB)
+					buf     = &bytes.Buffer{}
+					_, errW = MarshalExprCBOR(buf, e)
+				)
+
+				if errW != nil {
+					t.Fatalf("failed writing the expression: %v", errW.Error())
+				}
+
+				_ = UnmarshalExprCBOR(buf)
+			})
+		}
+	})
+}

prover/protocol/serialization/serialization.go

@@ -10,6 +10,7 @@ import (
 	"github.com/consensys/zkevm-monorepo/prover/protocol/column"
 	"github.com/consensys/zkevm-monorepo/prover/protocol/ifaces"
 	"github.com/consensys/zkevm-monorepo/prover/protocol/wizard"
+	"github.com/consensys/zkevm-monorepo/prover/symbolic"
 	"github.com/consensys/zkevm-monorepo/prover/utils"
 	"github.com/iancoleman/strcase"
 )
@@ -26,13 +27,19 @@ const (
 const (
 	DeclarationMode mode = iota
 	ReferenceMode
+	// pureExprMode is meant to serialize symbolic expression. All references to
+	// a compiled IOP are stripped out from the serialized expression. It allows
+	// deserializing without the complexity of the underlying CompiledIOP if
+	// there is one. It is used for generating/reading test-case expressions.
+	pureExprMode
 )
 
 // Types that necessitate special handling by the de/serializer
 var (
-	columnType  = reflect.TypeOf((*ifaces.Column)(nil)).Elem()
-	queryType   = reflect.TypeOf((*ifaces.Query)(nil)).Elem()
-	naturalType = reflect.TypeOf(column.Natural{})
+	columnType   = reflect.TypeOf((*ifaces.Column)(nil)).Elem()
+	queryType    = reflect.TypeOf((*ifaces.Query)(nil)).Elem()
+	naturalType  = reflect.TypeOf(column.Natural{})
+	metadataType = reflect.TypeOf((*symbolic.Metadata)(nil)).Elem()
 )
 
 // SerializeValue recursively serializes `v` into JSON. This function is
@@ -73,6 +80,18 @@ func SerializeValue(v reflect.Value, mode mode) (json.RawMessage, error) {
 
 	case reflect.Interface:
 
+		if mode == pureExprMode && v.Type() == metadataType {
+
+			var (
+				m              = v.Interface().(symbolic.Metadata)
+				mString        = m.String()
+				stringVar      = symbolic.StringVar(mString)
+				stringVarValue = reflect.ValueOf(stringVar)
+			)
+
+			return SerializeValue(stringVarValue, mode)
+		}
+
 		if mode == DeclarationMode && v.Type() == columnType {
 			// Only natural columns can be expected in this case.
 			col := v.Interface().(column.Natural)
@@ -299,6 +318,11 @@ func DeserializeValue(data json.RawMessage, mode mode, t reflect.Type, comp *wiz
 		// concrete type.
 		ifaceValue := reflect.New(t).Elem()
 
+		if mode == pureExprMode && t == metadataType {
+			var stringVar symbolic.StringVar
+			return DeserializeValue(data, mode, reflect.TypeOf(stringVar), comp)
+		}
+
 		if mode == DeclarationMode && t == columnType {
 			// Only natural columns can be expected in this case.
 			rawType := reflect.TypeOf(&serializableColumnDecl{})

prover/symbolic/csv.go

@@ -0,0 +1,141 @@
+package symbolic
+
+import (
+	"encoding/csv"
+	"fmt"
+	"io"
+	"strings"
+
+	"github.com/consensys/zkevm-monorepo/prover/maths/common/smartvectors"
+	"github.com/consensys/zkevm-monorepo/prover/maths/field"
+	"github.com/consensys/zkevm-monorepo/prover/utils"
+)
+
+const (
+	isConstantStr = "isConstant"
+	isZeroStr     = "isZero"
+	isOneStr      = "isOne"
+)
+
+func WriteConstantHoodAsCsv(w io.Writer, inputs []smartvectors.SmartVector) {
+
+	fmt.Fprintf(w, "cnt, %v, %v, %v\n", isConstantStr, isZeroStr, isOneStr)
+
+	for i := range inputs {
+
+		var (
+			c, isC = inputs[i].(*smartvectors.Constant)
+			isZero = isC && c.Val() == field.Zero()
+			isOne  = isC && c.Val() == field.One()
+		)
+
+		fmt.Fprintf(w, "%v, %v, %v, %v\n", i, isC, isZero, isOne)
+	}
+}
+
+func ReadConstanthoodFromCsv(r io.ReadCloser) [][3]bool {
+
+	res := make([][3]bool, 0, 1<<15)
+	rr := csv.NewReader(r)
+	rr.FieldsPerRecord = 0
+
+	header, err := rr.Read()
+	if err != nil {
+		utils.Panic("read header row: %v", err)
+	}
+
+	header[1] = strings.TrimSpace(header[1])
+	if header[1] != isConstantStr {
+		utils.Panic("unexpected field name: %v", header[1])
+	}
+
+	for row, err := rr.Read(); err != io.EOF; row, err = rr.Read() {
+
+		if err != nil {
+			utils.Panic("read row: %v", err)
+		}
+
+		g := [3]bool{}
+
+		for k := 1; k < 4; k++ {
+			var (
+				x       = strings.TrimSpace(row[k])
+				boolVar bool
+			)
+
+			switch {
+			case x == "true":
+				boolVar = true
+			case x == "false":
+				boolVar = false
+			default:
+				utils.Panic("invalid isConstant value = %v", x)
+			}
+
+			g[k-1] = boolVar
+		}
+
+		res = append(res, g)
+	}
+
+	return res
+}
+
+func (b *ExpressionBoard) WriteStatsToCSV(w io.Writer) {
+
+	fmt.Fprintf(w, "nodeCount, level, numInLevel, numChildren, numParent, operation, numCoeff1, numCoeff-1, numCoeff0, numCoeff2, numCoeff-2\n")
+
+	var (
+		nodeCnt = 0
+	)
+
+	for lvl := 0; lvl < len(b.Nodes); lvl++ {
+		for posInLvl := 0; posInLvl < len(b.Nodes[lvl]); posInLvl++ {
+
+			var (
+				node                    = b.Nodes[lvl][posInLvl]
+				cntCoeff1, cntCoeffMin1 int
+				cntCoeff0               int
+				cntCoeff2, cntCoeffMin2 int
+				operation               string
+				coeffs                  = []int{}
+			)
+
+			switch op := node.Operator.(type) {
+			case LinComb:
+				operation = "lin-comb"
+				coeffs = op.Coeffs
+			case Product:
+				operation = "product"
+				coeffs = op.Exponents
+			case PolyEval:
+				operation = "polyeval"
+			}
+
+			for _, c := range coeffs {
+				switch {
+				case c == 0:
+					cntCoeff0++
+				case c == 1:
+					cntCoeff1++
+				case c == -1:
+					cntCoeffMin1++
+				case c == 2:
+					cntCoeff2++
+				case c == -2:
+					cntCoeffMin2++
+				}
+			}
+
+			fmt.Fprintf(
+				w, "%v, %v, %v, %v, %v, %v, %v, %v, %v, %v, %v\n",
+				nodeCnt, lvl, posInLvl, len(node.Children), len(node.Parents),
+				operation, cntCoeff1, cntCoeffMin1, cntCoeff0, cntCoeff2,
+				cntCoeffMin2,
+			)
+
+			nodeCnt++
+		}
+	}
+
+}

prover/symbolic/evaluation_bench_test.go

@@ -0,0 +1,76 @@
+package symbolic_test
+
+import (
+	"fmt"
+	"path"
+	"testing"
+
+	"github.com/consensys/zkevm-monorepo/prover/backend/files"
+	"github.com/consensys/zkevm-monorepo/prover/maths/common/mempool"
+	"github.com/consensys/zkevm-monorepo/prover/maths/common/smartvectors"
+	"github.com/consensys/zkevm-monorepo/prover/maths/field"
+	"github.com/consensys/zkevm-monorepo/prover/protocol/serialization"
+	"github.com/consensys/zkevm-monorepo/prover/symbolic"
+)
+
+func BenchmarkEvaluationSingleThreaded(b *testing.B) {
+
+	makeRegular := func() smartvectors.SmartVector {
+		return smartvectors.Rand(symbolic.MaxChunkSize)
+	}
+
+	makeConst := func() smartvectors.SmartVector {
+		var x field.Element
+		x.SetRandom()
+		return smartvectors.NewConstant(x, symbolic.MaxChunkSize)
+	}
+
+	makeFullZero := func() smartvectors.SmartVector {
+		return smartvectors.NewConstant(field.Zero(), symbolic.MaxChunkSize)
+	}
+
+	makeFullOnes := func() smartvectors.SmartVector {
+		return smartvectors.NewConstant(field.One(), symbolic.MaxChunkSize)
+	}
+
+	for ratio := 1; ratio <= 32; ratio *= 2 {
+
+		b.Run(fmt.Sprintf("ratio-%v", ratio), func(b *testing.B) {
+
+			var (
+				testDir           = "testdata/evaluation-benchmark"
+				constanthoodFName = fmt.Sprintf("global-variable-constanthood-%v.csv", ratio)
+				exprFName         = fmt.Sprintf("global-cs-ratio-%v.cbor.gz", ratio)
+				constanthoodFPath = path.Join(testDir, constanthoodFName)
+				exprFPath         = path.Join(testDir, exprFName)
+				constantHoodFile  = files.MustRead(constanthoodFPath)
+				exprFile          = files.MustReadCompressed(exprFPath)
+				constantHood      = symbolic.ReadConstanthoodFromCsv(constantHoodFile)
+				expr              = serialization.UnmarshalExprCBOR(exprFile)
+				inputs            = make([]smartvectors.SmartVector, len(constantHood))
+				board             = expr.Board()
+				pool              = mempool.Create(symbolic.MaxChunkSize)
+			)
+
+			for i := range inputs {
+				switch {
+				case !constantHood[i][0]:
+					inputs[i] = makeRegular()
+				case constantHood[i][1]:
+					inputs[i] = makeFullZero()
+				case constantHood[i][2]:
+					inputs[i] = makeFullOnes()
+				default:
+					inputs[i] = makeConst()
+				}
+			}
+
+			b.ResetTimer()
+
+			for c := 0; c < b.N; c++ {
+				_ = board.Evaluate(inputs, pool)
+			}
+		})
+
+	}
+}

prover/symbolic/testdata/.gitignore

@@ -0,0 +1,3 @@
+!**/*.csv
+*.cbor
+!**/*.tar.gz

prover/symbolic/testdata/evaluation-benchmark/global-variable-constanthood-16.csv

@@ -0,0 +1,689 @@
+cnt, isConstant, isZero, isOne
+0, false, false, false
+1, false, false, false
+2, false, false, false
+3, true, false, false
+4, false, false, false
+5, false, false, false
+6, false, false, false
+7, false, false, false
+8, false, false, false
+9, false, false, false
+10, false, false, false
+11, false, false, false
+12, false, false, false
+13, false, false, false
+14, false, false, false
+15, false, false, false
+16, false, false, false
+17, false, false, false
+18, false, false, false
+19, false, false, false
+20, false, false, false
+21, false, false, false
+22, false, false, false
+23, false, false, false
+24, false, false, false
+25, false, false, false
+26, false, false, false
+27, false, false, false
+28, false, false, false
+29, false, false, false
+30, false, false, false
+31, false, false, false
+32, false, false, false
+33, false, false, false
+34, false, false, false
+35, false, false, false
+36, false, false, false
+37, false, false, false
+38, false, false, false
+39, false, false, false
+40, false, false, false
+41, false, false, false
+42, false, false, false
+43, false, false, false
+44, false, false, false
+45, false, false, false
+46, false, false, false
+47, false, false, false
+48, false, false, false
+49, false, false, false
+50, false, false, false
+51, false, false, false
+52, false, false, false
+53, false, false, false
+54, false, false, false
+55, false, false, false
+56, false, false, false
+57, false, false, false
+58, false, false, false
+59, false, false, false
+60, false, false, false
+61, false, false, false
+62, false, false, false
+63, false, false, false
+64, false, false, false
+65, false, false, false
+66, false, false, false
+67, false, false, false
+68, false, false, false
+69, false, false, false
+70, false, false, false
+71, false, false, false
+72, false, false, false
+73, false, false, false
+74, false, false, false
+75, false, false, false
+76, false, false, false
+77, false, false, false
+78, false, false, false
+79, false, false, false
+80, false, false, false
+81, false, false, false
+82, false, false, false
+83, false, false, false
+84, false, false, false
+85, false, false, false
+86, false, false, false
+87, false, false, false
+88, false, false, false
+89, false, false, false
+90, false, false, false
+91, false, false, false
+92, false, false, false
+93, false, false, false
+94, false, false, false
+95, false, false, false
+96, false, false, false
+97, false, false, false
+98, false, false, false
+99, false, false, false
+100, false, false, false
+101, false, false, false
+102, false, false, false
+103, false, false, false
+104, false, false, false
+105, false, false, false
+106, false, false, false
+107, false, false, false
+108, false, false, false
+109, false, false, false
+110, false, false, false
+111, false, false, false
+112, false, false, false
+113, false, false, false
+114, false, false, false
+115, false, false, false
+116, false, false, false
+117, false, false, false
+118, false, false, false
+119, false, false, false
+120, false, false, false
+121, false, false, false
+122, false, false, false
+123, false, false, false
+124, false, false, false
+125, false, false, false
+126, false, false, false
+127, false, false, false
+128, false, false, false
+129, false, false, false
+130, false, false, false
+131, false, false, false
+132, false, false, false
+133, false, false, false
+134, false, false, false
+135, false, false, false
+136, false, false, false
+137, false, false, false
+138, false, false, false
+139, false, false, false
+140, false, false, false
+141, false, false, false
+142, false, false, false
+143, false, false, false
+144, false, false, false
+145, false, false, false
+146, false, false, false
+147, false, false, false
+148, false, false, false
+149, false, false, false
+150, false, false, false
+151, false, false, false
+152, false, false, false
+153, false, false, false
+154, false, false, false
+155, false, false, false
+156, false, false, false
+157, false, false, false
+158, false, false, false
+159, false, false, false
+160, false, false, false
+161, false, false, false
+162, false, false, false
+163, false, false, false
+164, false, false, false
+165, false, false, false
+166, false, false, false
+167, false, false, false
+168, false, false, false
+169, false, false, false
+170, false, false, false
+171, false, false, false
+172, false, false, false
+173, false, false, false
+174, false, false, false
+175, false, false, false
+176, false, false, false
+177, false, false, false
+178, false, false, false
+179, false, false, false
+180, false, false, false
+181, false, false, false
+182, false, false, false
+183, false, false, false
+184, false, false, false
+185, false, false, false
+186, false, false, false
+187, false, false, false
+188, false, false, false
+189, false, false, false
+190, false, false, false
+191, false, false, false
+192, false, false, false
+193, false, false, false
+194, false, false, false
+195, false, false, false
+196, false, false, false
+197, false, false, false
+198, false, false, false
+199, false, false, false
+200, false, false, false
+201, false, false, false
+202, false, false, false
+203, false, false, false
+204, false, false, false
+205, false, false, false
+206, false, false, false
+207, false, false, false
+208, false, false, false
+209, false, false, false
+210, false, false, false
+211, false, false, false
+212, false, false, false
+213, false, false, false
+214, false, false, false
+215, false, false, false
+216, false, false, false
+217, false, false, false
+218, false, false, false
+219, false, false, false
+220, false, false, false
+221, false, false, false
+222, false, false, false
+223, false, false, false
+224, false, false, false
+225, false, false, false
+226, false, false, false
+227, false, false, false
+228, false, false, false
+229, false, false, false
+230, false, false, false
+231, false, false, false
+232, false, false, false
+233, false, false, false
+234, true, true, false
+235, true, true, false
+236, true, true, false
+237, true, false, false
+238, true, true, false
+239, true, false, false
+240, true, true, false
+241, true, false, true
+242, true, true, false
+243, true, true, false
+244, true, true, false
+245, true, true, false
+246, true, false, false
+247, true, true, false
+248, true, false, false
+249, true, true, false
+250, true, false, true
+251, true, true, false
+252, true, true, false
+253, true, true, false
+254, true, true, false
+255, true, false, false
+256, true, true, false
+257, true, false, false
+258, true, true, false
+259, true, false, true
+260, true, true, false
+261, true, true, false
+262, true, true, false
+263, true, true, false
+264, true, false, false
+265, true, true, false
+266, true, false, false
+267, true, true, false
+268, true, false, true
+269, true, true, false
+270, true, true, false
+271, true, true, false
+272, true, true, false
+273, true, false, false
+274, true, true, false
+275, true, false, false
+276, true, true, false
+277, true, false, true
+278, true, true, false
+279, true, true, false
+280, true, true, false
+281, true, true, false
+282, true, false, false
+283, true, true, false
+284, true, false, false
+285, true, true, false
+286, true, false, true
+287, true, true, false
+288, true, true, false
+289, true, true, false
+290, true, true, false
+291, true, false, false
+292, true, true, false
+293, true, false, false
+294, true, true, false
+295, true, false, true
+296, true, true, false
+297, true, true, false
+298, true, true, false
+299, true, true, false
+300, true, false, false
+301, true, true, false
+302, true, false, false
+303, true, true, false
+304, true, false, true
+305, true, true, false
+306, true, true, false
+307, true, true, false
+308, true, true, false
+309, true, false, false
+310, true, true, false
+311, true, false, false
+312, true, true, false
+313, true, false, true
+314, true, true, false
+315, true, true, false
+316, true, true, false
+317, true, true, false
+318, true, false, false
+319, true, true, false
+320, true, false, false
+321, true, true, false
+322, true, false, true
+323, true, true, false
+324, true, true, false
+325, true, true, false
+326, true, true, false
+327, true, false, false
+328, true, true, false
+329, true, false, false
+330, true, true, false
+331, true, false, true
+332, true, true, false
+333, true, true, false
+334, true, true, false
+335, true, true, false
+336, true, false, false
+337, true, true, false
+338, true, false, false
+339, true, true, false
+340, true, false, true
+341, true, true, false
+342, true, true, false
+343, true, true, false
+344, true, true, false
+345, true, false, false
+346, true, true, false
+347, true, false, false
+348, true, true, false
+349, true, false, true
+350, true, true, false
+351, true, true, false
+352, true, true, false
+353, true, true, false
+354, true, false, false
+355, true, true, false
+356, true, false, false
+357, true, true, false
+358, true, false, true
+359, true, true, false
+360, true, true, false
+361, true, true, false
+362, true, true, false
+363, true, false, false
+364, true, true, false
+365, true, false, false
+366, true, true, false
+367, true, false, true
+368, true, true, false
+369, true, true, false
+370, true, true, false
+371, true, true, false
+372, true, false, false
+373, true, true, false
+374, true, false, false
+375, true, true, false
+376, true, false, true
+377, true, true, false
+378, true, true, false
+379, true, true, false
+380, true, true, false
+381, true, false, false
+382, true, true, false
+383, true, false, false
+384, true, true, false
+385, true, false, true
+386, true, true, false
+387, true, true, false
+388, true, true, false
+389, true, true, false
+390, true, false, false
+391, true, true, false
+392, true, false, false
+393, true, true, false
+394, true, false, true
+395, true, true, false
+396, true, true, false
+397, true, true, false
+398, true, true, false
+399, true, false, false
+400, true, true, false
+401, true, false, false
+402, true, true, false
+403, true, false, true
+404, true, true, false
+405, true, true, false
+406, true, true, false
+407, true, true, false
+408, true, false, false
+409, true, true, false
+410, true, false, false
+411, true, true, false
+412, true, false, true
+413, true, true, false
+414, true, true, false
+415, true, true, false
+416, true, true, false
+417, true, false, false
+418, true, true, false
+419, true, false, false
+420, true, true, false
+421, true, false, true
+422, true, true, false
+423, true, true, false
+424, true, true, false
+425, true, true, false
+426, true, false, false
+427, true, true, false
+428, true, false, false
+429, true, true, false
+430, true, false, true
+431, true, true, false
+432, true, true, false
+433, true, true, false
+434, true, true, false
+435, true, false, false
+436, true, true, false
+437, true, false, false
+438, true, true, false
+439, true, false, true
+440, true, true, false
+441, true, true, false
+442, true, true, false
+443, true, true, false
+444, true, false, false
+445, true, true, false
+446, true, false, false
+447, true, true, false
+448, true, false, true
+449, true, true, false
+450, true, true, false
+451, true, true, false
+452, true, true, false
+453, true, false, false
+454, true, true, false
+455, true, false, false
+456, true, true, false
+457, true, false, true
+458, true, true, false
+459, true, true, false
+460, true, true, false
+461, true, true, false
+462, true, false, false
+463, true, true, false
+464, true, false, false
+465, true, true, false
+466, true, false, true
+467, true, true, false
+468, true, true, false
+469, true, true, false
+470, true, true, false
+471, true, false, false
+472, true, true, false
+473, true, false, false
+474, true, true, false
+475, true, false, true
+476, true, true, false
+477, true, true, false
+478, true, true, false
+479, false, false, false
+480, true, false, false
+481, true, true, false
+482, true, false, false
+483, false, false, false
+484, true, false, true
+485, false, false, false
+486, true, true, false
+487, true, true, false
+488, false, false, false
+489, true, false, false
+490, true, true, false
+491, true, false, false
+492, false, false, false
+493, true, false, true
+494, false, false, false
+495, true, true, false
+496, true, true, false
+497, false, false, false
+498, true, false, false
+499, true, true, false
+500, true, false, false
+501, false, false, false
+502, true, false, true
+503, true, true, false
+504, true, true, false
+505, true, true, false
+506, false, false, false
+507, true, false, false
+508, true, true, false
+509, true, false, false
+510, false, false, false
+511, true, false, true
+512, true, true, false
+513, true, true, false
+514, true, true, false
+515, true, true, false
+516, true, false, false
+517, true, true, false
+518, true, false, false
+519, false, false, false
+520, true, false, true
+521, true, true, false
+522, true, true, false
+523, true, true, false
+524, true, true, false
+525, true, false, false
+526, true, true, false
+527, true, false, false
+528, false, false, false
+529, true, false, true
+530, true, true, false
+531, true, true, false
+532, true, true, false
+533, true, true, false
+534, true, false, false
+535, true, true, false
+536, true, false, false
+537, false, false, false
+538, true, false, true
+539, true, true, false
+540, true, true, false
+541, true, true, false
+542, true, true, false
+543, true, false, false
+544, true, true, false
+545, true, false, false
+546, true, true, false
+547, true, false, true
+548, true, true, false
+549, true, true, false
+550, true, true, false
+551, true, true, false
+552, true, false, false
+553, true, true, false
+554, true, false, false
+555, true, true, false
+556, true, false, true
+557, true, true, false
+558, true, true, false
+559, true, true, false
+560, true, true, false
+561, true, false, false
+562, true, true, false
+563, true, false, false
+564, true, true, false
+565, true, false, true
+566, true, true, false
+567, true, true, false
+568, true, true, false
+569, true, true, false
+570, true, false, false
+571, true, true, false
+572, true, false, false
+573, true, true, false
+574, true, false, true
+575, true, true, false
+576, true, true, false
+577, true, true, false
+578, true, true, false
+579, true, false, false
+580, true, true, false
+581, true, false, false
+582, true, true, false
+583, true, false, true
+584, true, true, false
+585, true, true, false
+586, true, true, false
+587, true, true, false
+588, true, false, false
+589, true, true, false
+590, true, false, false
+591, true, true, false
+592, true, false, true
+593, true, true, false
+594, true, true, false
+595, true, true, false
+596, true, true, false
+597, true, false, false
+598, true, true, false
+599, true, false, false
+600, true, true, false
+601, true, false, true
+602, true, true, false
+603, true, true, false
+604, true, true, false
+605, true, true, false
+606, true, false, false
+607, true, true, false
+608, true, false, false
+609, true, true, false
+610, true, false, true
+611, true, true, false
+612, true, true, false
+613, true, true, false
+614, true, true, false
+615, true, false, false
+616, true, true, false
+617, true, false, false
+618, true, true, false
+619, true, false, true
+620, true, true, false
+621, true, true, false
+622, true, true, false
+623, true, true, false
+624, true, false, false
+625, true, true, false
+626, true, false, false
+627, true, true, false
+628, true, false, true
+629, true, true, false
+630, true, true, false
+631, true, true, false
+632, true, true, false
+633, true, false, false
+634, true, true, false
+635, true, false, false
+636, true, true, false
+637, true, false, true
+638, true, true, false
+639, true, true, false
+640, true, true, false
+641, true, true, false
+642, true, false, false
+643, true, true, false
+644, true, false, false
+645, true, true, false
+646, true, false, true
+647, true, true, false
+648, true, true, false
+649, true, true, false
+650, true, true, false
+651, true, false, false
+652, true, true, false
+653, true, false, false
+654, true, true, false
+655, true, false, true
+656, true, true, false
+657, true, true, false
+658, true, true, false
+659, true, true, false
+660, true, false, false
+661, true, true, false
+662, true, false, false
+663, true, true, false
+664, true, false, true
+665, true, true, false
+666, true, true, false
+667, true, true, false
+668, true, true, false
+669, true, false, false
+670, true, true, false
+671, true, false, false
+672, true, true, false
+673, true, false, true
+674, true, true, false
+675, false, false, false
+676, false, false, false
+677, false, false, false
+678, false, false, false
+679, false, false, false
+680, false, false, false
+681, false, false, false
+682, false, false, false
+683, false, false, false
+684, false, false, false
+685, false, false, false
+686, false, false, false
+687, false, false, false

prover/symbolic/testdata/evaluation-benchmark/global-variable-constanthood-32.csv

@@ -0,0 +1,199 @@
+cnt, isConstant, isZero, isOne
+0, false, false, false
+1, false, false, false
+2, false, false, false
+3, false, false, false
+4, false, false, false
+5, false, false, false
+6, false, false, false
+7, false, false, false
+8, false, false, false
+9, false, false, false
+10, false, false, false
+11, false, false, false
+12, false, false, false
+13, false, false, false
+14, false, false, false
+15, false, false, false
+16, false, false, false
+17, false, false, false
+18, false, false, false
+19, false, false, false
+20, false, false, false
+21, false, false, false
+22, false, false, false
+23, false, false, false
+24, false, false, false
+25, false, false, false
+26, false, false, false
+27, false, false, false
+28, false, false, false
+29, false, false, false
+30, false, false, false
+31, false, false, false
+32, false, false, false
+33, false, false, false
+34, false, false, false
+35, false, false, false
+36, false, false, false
+37, false, false, false
+38, false, false, false
+39, false, false, false
+40, false, false, false
+41, false, false, false
+42, false, false, false
+43, false, false, false
+44, false, false, false
+45, false, false, false
+46, false, false, false
+47, false, false, false
+48, true, false, false
+49, false, false, false
+50, false, false, false
+51, false, false, false
+52, false, false, false
+53, false, false, false
+54, false, false, false
+55, false, false, false
+56, false, false, false
+57, false, false, false
+58, false, false, false
+59, false, false, false
+60, false, false, false
+61, false, false, false
+62, false, false, false
+63, false, false, false
+64, false, false, false
+65, false, false, false
+66, false, false, false
+67, false, false, false
+68, false, false, false
+69, false, false, false
+70, false, false, false
+71, false, false, false
+72, false, false, false
+73, false, false, false
+74, false, false, false
+75, false, false, false
+76, false, false, false
+77, false, false, false
+78, false, false, false
+79, false, false, false
+80, false, false, false
+81, false, false, false
+82, false, false, false
+83, false, false, false
+84, false, false, false
+85, false, false, false
+86, false, false, false
+87, false, false, false
+88, false, false, false
+89, false, false, false
+90, false, false, false
+91, false, false, false
+92, false, false, false
+93, false, false, false
+94, false, false, false
+95, false, false, false
+96, false, false, false
+97, false, false, false
+98, false, false, false
+99, false, false, false
+100, false, false, false
+101, false, false, false
+102, false, false, false
+103, false, false, false
+104, false, false, false
+105, false, false, false
+106, false, false, false
+107, false, false, false
+108, false, false, false
+109, false, false, false
+110, false, false, false
+111, false, false, false
+112, false, false, false
+113, false, false, false
+114, false, false, false
+115, false, false, false
+116, false, false, false
+117, false, false, false
+118, false, false, false
+119, false, false, false
+120, false, false, false
+121, false, false, false
+122, false, false, false
+123, false, false, false
+124, false, false, false
+125, false, false, false
+126, false, false, false
+127, false, false, false
+128, false, false, false
+129, false, false, false
+130, false, false, false
+131, false, false, false
+132, false, false, false
+133, false, false, false
+134, false, false, false
+135, false, false, false
+136, false, false, false
+137, false, false, false
+138, false, false, false
+139, false, false, false
+140, false, false, false
+141, false, false, false
+142, false, false, false
+143, false, false, false
+144, false, false, false
+145, false, false, false
+146, false, false, false
+147, false, false, false
+148, false, false, false
+149, false, false, false
+150, false, false, false
+151, false, false, false
+152, false, false, false
+153, false, false, false
+154, false, false, false
+155, false, false, false
+156, false, false, false
+157, false, false, false
+158, false, false, false
+159, false, false, false
+160, false, false, false
+161, false, false, false
+162, false, false, false
+163, false, false, false
+164, false, false, false
+165, false, false, false
+166, false, false, false
+167, false, false, false
+168, false, false, false
+169, false, false, false
+170, false, false, false
+171, false, false, false
+172, false, false, false
+173, false, false, false
+174, false, false, false
+175, false, false, false
+176, false, false, false
+177, false, false, false
+178, false, false, false
+179, false, false, false
+180, false, false, false
+181, false, false, false
+182, false, false, false
+183, false, false, false
+184, false, false, false
+185, false, false, false
+186, false, false, false
+187, false, false, false
+188, false, false, false
+189, false, false, false
+190, false, false, false
+191, false, false, false
+192, false, false, false
+193, false, false, false
+194, false, false, false
+195, false, false, false
+196, false, false, false
+197, false, false, false