General/instance vars in precision

[s0mark]

Putting the general versions of variables into the precision instead of the instance versions makes Theta not be able to verify some tasks, while allowing some previously unverified tasks to be verified.

theta/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrecRefiner.kt

Lines 45 to 57 in 22257ee

	val reverseLookup = trace.states[i].processes.values.map {
	it.varLookup.map {
	it.map {
	Pair(it.value, it.key)
	}
	}.flatten()
	}.flatten().toMap()
	val additionalLookup = if (i > 0) getTempLookup(
	trace.actions[i - 1].edge.label).entries.associateBy(
	{ it.value }) { it.key } else emptyMap()
	val varLookup = if (checkForPop) additionalLookup else (reverseLookup + additionalLookup)
	val precFromRef = refToPrec.toPrec(refutation, i).changeVars(varLookup)
	runningPrec = refToPrec.join(runningPrec, precFromRef)

General versions of variables are put into the precision if both reverseLookup and additionalLookup are used in changeVars, while instances are used if reverseLookup is omitted.

For recursive tasks:

• Fibonacci02.c, fibo_10-2.c, fibo_2calls_10-1.c, fibo_2calls_6-1.c, fibo_2calls_8-1.c, fibo_7-1.c can only be verified with general vars, not with instances,
• Ackermann02.c, Addition02.c, BallRajamani-SPIN2000-Fig1.c can only be verified with instances, not with general vars.
• Explicit abstraction performs better with general vars (49 vs. 39), while predicate abstraction solves significantly more tasks with instances (15 vs. 44).

For multithreaded tasks, general vars are preferred, as there were over 200 tasks that Theta can only solve with general vars and not with instances (see #244 (comment)).

This behavior does not seem to be by-design and should be investigated.