IdealCVC3HybridProver.java

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

import java.util.Map;

import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.prove.IF.TheoremProverException;
import edu.udel.cis.vsl.tass.prove.IF.TheoremProverIF;
import edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProverFactory;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicConstantIF;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicExpressionIF;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicUniverseIF;
import edu.udel.cis.vsl.tass.util.TernaryResult.ResultType;

/**
 * A hybrid prover for symbolic expressions in the ideal canonical form. It
 * first attempts to prove the query using the SimpleIdealProver. If this does
 * not yield a conclusive result, it then attempts the CVC3 prover (which is
 * much more expensive).
 */
public class IdealCVC3HybridProver implements TheoremProverIF {

	private SymbolicUniverseIF universe;

	private TheoremProverIF simpleProver, cvc3Prover;

	public IdealCVC3HybridProver(SymbolicUniverseIF universe,
			RunConfiguration config) {
		simpleProver = new SimpleIdealProver(universe);
		cvc3Prover = CVC3TheoremProverFactory.newCVC3TheoremProver(universe,
				config);
		this.universe = universe;
	}

	public void close() {
		simpleProver.close();
		cvc3Prover.close();
	}

	public void reset() {
		simpleProver.reset();
		cvc3Prover.reset();
	}

	public SymbolicUniverseIF universe() {
		return universe;
	}

	public ResultType valid(SymbolicExpressionIF assumption,
			SymbolicExpressionIF expr) {
		ResultType result = simpleProver.valid(assumption, expr);

		if (result == ResultType.MAYBE) {
			result = cvc3Prover.valid(assumption, expr);
		}
		return result;
	}
	
	public Map<SymbolicConstantIF, SymbolicExpressionIF> findModel(SymbolicExpressionIF context) throws TheoremProverException{
		return cvc3Prover.findModel(context);
	}

	@Override
	public int numInternalValidCalls() {
		return cvc3Prover.numValidCalls();
	}

	@Override
	public int numValidCalls() {
		return simpleProver.numValidCalls();
	}

}