// Path: src/main/java/bixie/prover/ProverFun.java
// public interface ProverFun {
// 
// 	ProverExpr mkExpr(ProverExpr[] args);
// 
// }
// 
// Path: src/main/java/bixie/prover/ProverType.java
// public interface ProverType {
// 
// }


import scala.collection.mutable.ArrayBuffer;
import ap.basetypes.IdealInt$;
import ap.parser.IExpression$;
import ap.parser.IFunApp;
import ap.parser.IFunction;
import ap.parser.IIntLit;
import ap.parser.ITerm;
import ap.parser.ITermITE;
import bixie.prover.ProverExpr;
import bixie.prover.ProverFun;
import bixie.prover.ProverType;
package bixie.prover.princess;


class PrincessFun implements ProverFun {

	private final IFunction fun;
	private final ProverType resType;

	PrincessFun(IFunction fun, ProverType resType) {
		this.fun = fun;
		this.resType = resType;
	}

	public ProverExpr mkExpr(ProverExpr[] args) {
		final ArrayBuffer<ITerm> argsBuf = new ArrayBuffer<ITerm>();
		for (int i = 0; i < args.length; ++i) {
			ITerm termArg;
			if (args[i].getType() == BoolType.INSTANCE)
				termArg = new ITermITE(((FormulaExpr) args[i]).formula,
						new IIntLit(IdealInt$.MODULE$.apply(0)), new IIntLit(
// Path: src/main/java/bixie/prover/ProverFun.java
// public interface ProverFun {
// 
// 	ProverExpr mkExpr(ProverExpr[] args);
// 
// }
// 
// Path: src/main/java/bixie/prover/ProverType.java
// public interface ProverType {
// 
// }


// Path: src/main/java/bixie/prover/princess/PrincessFun.java
import scala.collection.mutable.ArrayBuffer;
import ap.basetypes.IdealInt$;
import ap.parser.IExpression$;
import ap.parser.IFunApp;
import ap.parser.IFunction;
import ap.parser.IIntLit;
import ap.parser.ITerm;
import ap.parser.ITermITE;
import bixie.prover.ProverExpr;
import bixie.prover.ProverFun;
import bixie.prover.ProverType;

package bixie.prover.princess;


class PrincessFun implements ProverFun {

	private final IFunction fun;
	private final ProverType resType;

	PrincessFun(IFunction fun, ProverType resType) {
		this.fun = fun;
		this.resType = resType;
	}

	public ProverExpr mkExpr(ProverExpr[] args) {
		final ArrayBuffer<ITerm> argsBuf = new ArrayBuffer<ITerm>();
		for (int i = 0; i < args.length; ++i) {
			ITerm termArg;
			if (args[i].getType() == BoolType.INSTANCE)
				termArg = new ITermITE(((FormulaExpr) args[i]).formula,
						new IIntLit(IdealInt$.MODULE$.apply(0)), new IIntLit(
								IdealInt$.MODULE$.apply(1)));