Versioned Reasoners

A reasoner implementation is not necessarily frozen code. It may evolve in time, to fix bugs or modify the behaviour (new antecedent, a different WD predicate, ...), even after the old implementation was used to prove models. This entails potential problems: what happens if we try to reuse/replay a proof rule serialized by the old reasoner implementation ? There might be unexpected failures, or even worse: silent false successes. Thus, we have to be aware of reasoner implementation changes. This is achieved through a reasoner versioning mechanism.

A new published interface

The IVersionedReasoner interface extends the existing IReasoner interface and provides a method to get the reasoner version (getVersion()), which is defined as a non-negative integer.

To maintain backward compatibility with existing, potentially externally contributed, reasoners, it is not possible to impose the new interface to all reasoners. There will then exist versioned and non-versioned reasoners, all working together.

Version serialization

To be efficient, the version must also be stored in proof rules, so that it can be checked when trying to reuse them. Rather than adding yet another xml attribute into proof files, it has been decided to concatenate the version to the reasoner name, using the following syntax:

reasonerName:version

When reusing a proof, version conflicts between serialized version and currently registered reasoner version are detected and processed, by trying to apply the latest one.

Example

The following is an example implementation of the new IVersionedReasoner interface:

public class Example implements IVersionedReasoner {
	
	private static final String REASONER_ID = PLUGIN_ID + ".example";
	private static final int VERSION = 15;
	
	public void serializeInput(IReasonerInput input, IReasonerInputWriter writer)
			throws SerializeException {
		// as usual
	}

	public IReasonerInput deserializeInput(IReasonerInputReader reader)
			throws SerializeException {
		// as usual
	}

	public IReasonerOutput apply(IProverSequent seq, IReasonerInput input,
			IProofMonitor pm) {
		// as usual
	}

	public String getReasonerID() {
		return REASONER_ID;
	}

	public int getVersion() {
		return VERSION;
	}

}