Newer
Older
RDLProofSystem / src / main / java / Main.java
@Sakoda2269 Sakoda2269 20 days ago 3 KB right sub実装まで
import com.google.common.collect.TreeMultimap;

import java.util.HashMap;
import java.util.List;
import java.util.Map;

import constants.Types;
import inference.axioms.RightSubstitution;
import models.algebra.Constant;
import models.algebra.Expression;
import models.algebra.Type;
import models.algebra.Variable;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.terms.DependencyTerm;
import models.terms.Resource;
import models.terms.meta.MetaDynamicDependency;
import models.terms.meta.MetaDynamicDependencyTerm;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResource;
import models.terms.meta.MetaTermGenerator;

public class Main {

	static Type INT = Types.typeInt;

	public static void main(String[] args) {
		//
		sandbox();
		sandbox2();
		sandbox3();
		sandbox4();
		sandbox5();
	}
	
	
	static void sandbox() {
		Expression tmp = utils.ExpressionUitls.parse("x");
		System.out.println(tmp);
		tmp = utils.ExpressionUitls.parse("(x + 5) * 3");
		Map<Variable, Integer> nums = new HashMap<>();
		int a = utils.ExpressionUitls.getCoefficientAndConstantsFromExpression(tmp, nums, 1);
		System.out.println(tmp);
		System.out.println(a);
		System.out.println(nums);
		
		int b = utils.ExpressionUitls.getConstantValue(new  Constant("3"));
		System.out.println(b);
	}
	
	static void sandbox2() {
		TreeMultimap<Integer, Integer> tmp = TreeMultimap.create();
		tmp.put(1, 1);
		tmp.put(1, 2);
		tmp.put(1, 1);
		tmp.put(1, 3);
		System.out.println(tmp.get(1));
	}
	
	static void sandbox3() {
		MetaDynamicDependency d1 = new MetaDynamicDependency((ci, cd, mi, md, context) -> new MetaResource(new Variable("x" + ci)));
		MetaDynamicDependency d2 = new MetaDynamicDependency(new MetaTermGenerator() {
			@Override
			public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
				if (curIndex == 0 && curDepth < maxDepth) return new MetaDynamicDependency(this);
				else return new MetaResource(new Variable("x" + curIndex + "_" + curDepth));
			} 
		});
		d2.generate(0, 2, 2, null);
		System.out.println(d2.generate(0, 2, 2, null));
	}
	
	static void sandbox4() {
		MetaDynamicDependencyTerm t1 = new MetaDynamicDependencyTerm((ci, cd, mi, md, contex) -> new MetaResource(new Variable("x" + ci)));
		MetaDynamicDependencyTerm t2 = new MetaDynamicDependencyTerm(new MetaTermGenerator() {
			@Override
			public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
				if (curDepth == 0 && curIndex != 0 && curIndex % 2 == 0) {
					return new MetaDynamicDependencyTerm(this);
				}
				return new MetaResource(new Variable("x" + curDepth + "_" + curIndex));
			}
		});
		System.out.println(t1.generate(0, 5, 0, null));
		System.out.println(t2.generate(0, 3, 2, null));
	}
	
	static void sandbox5() {
		RightSubstitution rs = new RightSubstitution();
		Resource a = new Resource("a", 1);
		Resource b = new Resource("b", 1);
		Resource c = new Resource("c", 1);
		Resource d = new Resource("d", 1);
		Resource e = new Resource("e", 1);
		Resource f = new Resource("f", 1);
		Resource g = new Resource("f", 1);
		Resource h = new Resource("h", 1);
		Resource i = new Resource("i", 1);
		Resource j = new Resource("j", 1);
		Resource k = new Resource("k", 1);
		Resource l = new Resource("l", 1);
		EquationFormula eq = new EquationFormula(a, b);
		DependencyFormula dep = new DependencyFormula(c, d);
		EquationFormula eq2 = new EquationFormula(new DependencyTerm(d, e, f), a);
		System.out.println(rs.apply(List.of(eq, dep, eq2)));
		DependencyTerm t1 = new DependencyTerm(c, d, a);
		System.out.println(rs.generateRightSideHand(List.of(eq, dep, eq2), t1));
		DependencyFormula dep2 = new DependencyFormula(c, g);
		EquationFormula eq3 = new EquationFormula(new DependencyTerm(g, h, i), j);
		System.out.println(rs.apply(List.of(eq, eq2, eq3, dep, dep2)));
	}
	
}