Equivalence checking as a component

[mario-bucev]

Equivalence checking is now a component, activated with --equivchk. As before, it requires --models and --comparefuns to be fed with a list of model function(s) and candidate function(s) respectively, and optionally accept a --norm=<fn name> for normalization function. Note that @traceInduct functions need not to run with the --equivchk option.
New options:

• --equivchk-n=<int> (default: 3): specify the N hyperparameter
• --equivchk-init-score=<int> (default: 200): specify the initial score for models
• --equivchk-max-perm=<int> (default: 16): maximum number of matching for auxiliary functions
• --silent-verification=<bool> (default: false): do not print any message when a VC fails to verify (whether due to invalidity or timeout).

This PR:

• ⚠️ factors unificationConstraint from oo.TypeOps to ast.TypeOps. oo.TypeOps overrides ast.TypeOps for oo constructs.
• splits Trace into EquivalenceChecker and TraceInductElimination.
• adds a test suite for equivalence checking, so the nightly CI will run for longer

[mario-bucev]

This is not stack-safe:

stainless/core/src/main/scala/stainless/equivchk/EquivalenceCheckingComponent.scala

Lines 151 to 189 in bdb782a

	def examination(): Future[ec.Results] = {
	ec.pickNextExamination() match {
	case ec.NextExamination.Done(pruned, res) =>
	debugPruned(ec)(pruned)
	printResults(ec)(res)
	context.options.findOption(equivchk.optEquivalenceOutput) match {
	case Some(out) => dumpResultsJson(out, ec)(res)
	case None => ()
	}
	Future.successful(res)
	case ec.NextExamination.NewCandidate(cand, model, strat, pruned) =>
	debugPruned(ec)(pruned)
	debugNewCandidate(ec)(cand, model, strat)
	round()
	}
	}
	def round(): Future[ec.Results] = {
	val generated = ec.prepareRound()
	val allFns = (ec.symbols.functions -- generated.map(_.id)).values.toSeq ++ generated
	val syms: trace.trees.Symbols = trace.trees.NoSymbols
	.withSorts(ec.symbols.sorts.values.map(identity.transform).toSeq)
	.withFunctions(allFns.map(identity.transform))
	val plainSyms = tracePostPipeline.extract(syms)._1
	underlyingRun.execute(generated.map(_.id), plainSyms, ExtractionSummary.NoSummary)
	.flatMap { analysis =>
	val concl = ec.concludeRound(analysis)
	concl match {
	case ec.RoundConclusion.NextRound(cand, model, strat, prunedSubFnsPairs) =>
	debugNewRound(ec)(cand, model, strat)
	debugPrunedSubFnsPairs(prunedSubFnsPairs)
	round()
	case ec.RoundConclusion.CandidateClassified(cand, classification, prunedSubFnsPairs) =>
	debugClassified(ec)(cand, classification)
	debugPrunedSubFnsPairs(prunedSubFnsPairs)
	examination()
	}
	}
	}

Edit: it is stack-safe as long as the ExecutionContext is stack-safe (see scala/bug#11256) which was not the case when parallelism is disabled because the currentThreadExecutionContext runs the runnable (the docs seems to recommand to avoid this):

stainless/core/src/main/scala/stainless/package.scala

Lines 160 to 163 in 87b66ff

	private lazy val currentThreadExecutionContext: ExecutionContext =
	ExecutionContext.fromExecutor(new java.util.concurrent.Executor {
	def execute(runnable: Runnable): Unit = { runnable.run() }
	})

Changing it to:

stainless/core/src/main/scala/stainless/package.scala

Lines 160 to 161 in b3cfda9

	private lazy val singleThreadExecutionContext: ExecutionContext =
	ExecutionContext.fromExecutor(Executors.newFixedThreadPool(1))