Prove.java

package edu.udel.cis.vsl.tass.prove;

import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.prove.IF.TheoremProverIF;
import edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProverFactory;
import edu.udel.cis.vsl.tass.prove.ideal.IdealCVC3HybridProver;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicUniverseIF;

public class Prove {

	public static TheoremProverIF newIdealCVC3HybridProver(
			SymbolicUniverseIF universe, RunConfiguration configuration) {
		return new IdealCVC3HybridProver(universe, configuration);
	}

	public static TheoremProverIF newCVC3Prover(SymbolicUniverseIF universe,
			RunConfiguration configuration) {
		return CVC3TheoremProverFactory.newCVC3TheoremProver(universe,
				configuration);
	}
}