• 设为首页
  • 点击收藏
  • 手机版
    手机扫一扫访问
    迪恩网络手机版
  • 关注官方公众号
    微信扫一扫关注
    迪恩网络公众号

Java PrettyPrinter类代码示例

原作者: [db:作者] 来自: [db:来源] 收藏 邀请

本文整理汇总了Java中kodkod.util.nodes.PrettyPrinter的典型用法代码示例。如果您正苦于以下问题:Java PrettyPrinter类的具体用法?Java PrettyPrinter怎么用?Java PrettyPrinter使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。



PrettyPrinter类属于kodkod.util.nodes包,在下文中一共展示了PrettyPrinter类的16个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Java代码示例。

示例1: main

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
/**
 * Usage: java examples.ConfigAssure <ipAddresses file> <subnets file>
 */
public static void main(String[] args) {
	if (args.length < 2)
		usage();
	try {
		final ConfigAssure ca = new ConfigAssure();
		final Solver solver = new Solver();
		solver.options().setBitwidth(32);
		solver.options().setSolver(SATFactory.MiniSat);

		final Formula formula = ca.requirements();
		final Bounds bounds = ca.bounds(args[0], args[1]);

		System.out.println("---explicit requirements (others are implicit in the bounds)---");
		System.out.println(PrettyPrinter.print(formula, 2));

		System.out.println("\n---solving with config files " + args[0] + " and " + args[1] + "---");

		final Solution sol = solver.solve(formula, bounds);

		System.out.println("\n---OUTCOME---");
		System.out.println(sol.outcome());

		System.out.println("\n---STATS---");
		System.out.println(sol.stats());

		if (sol.instance() != null) {
			System.out.println("\n---INSTANCE--");
			ca.display(sol.instance(), solver.options());
		}
	} catch (IOException ioe) {
		ioe.printStackTrace();
		usage();
	}
}
 
开发者ID:AlloyTools,项目名称:org.alloytools.alloy,代码行数:38,代码来源:ConfigAssure.java


示例2: main

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
/**
 * Usage: java examples.alloy.ToyFilesystem
 */
public static void main(String[] args) {
	final ToyFilesystem toy = new ToyFilesystem();
	final Formula f = toy.constraints();
	System.out.println(PrettyPrinter.print(f, 2));
	final Bounds b = toy.bounds();
	final Solver solver = new Solver();
	solver.options().setSolver(SATFactory.MiniSat);

	final Solution s = solver.solve(f, b);
	System.out.println(s);
}
 
开发者ID:AlloyTools,项目名称:org.alloytools.alloy,代码行数:15,代码来源:ToyFilesystem.java


示例3: printFalse

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
void printFalse(String check, Formula formula, Bounds bounds, Solution sol) {
	print(check, formula, bounds, sol.outcome(), sol.stats());
	System.out.println("trivial core:");
	for (Node f : sol.proof().highLevelCore().values()) {
		System.out.println(PrettyPrinter.print(f, 2, 100));
	}
}
 
开发者ID:AlloyTools,项目名称:org.alloytools.alloy,代码行数:8,代码来源:UCoreStats.java


示例4: printUnsat

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
void printUnsat(String check, Formula formula, Bounds bounds, Statistics stats, Set<Formula> initialCore,
		Set<Formula> minCore, long minTime) {
	print(check, formula, bounds, Solution.Outcome.UNSATISFIABLE, stats);
	System.out.println("formulas: " + Nodes.roots(formula).size());
	System.out.println("initial core: " + initialCore.size());
	System.out.println("minimized core with " + minCore.size() + " formulas found in " + minTime + " ms:");
	for (Formula f : minCore) {
		System.out.println(PrettyPrinter.print(f, 2, 100));
	}
}
 
开发者ID:AlloyTools,项目名称:org.alloytools.alloy,代码行数:11,代码来源:UCoreStats.java


示例5: flushFormula

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
private void flushFormula(Formula formula, Bounds bounds)  {
    try {
        File f = new File(System.getProperty("java.io.tmpdir"), "kk.txt");
        OutputStream os = new BufferedOutputStream(new FileOutputStream(f));
        os.write(PrettyPrinter.print(formula, 2).getBytes());
        os.write("\n================\n".getBytes());
        os.write(bounds.toString().getBytes());
        os.flush();
        os.close();
    } catch (Exception e) {
    }
}
 
开发者ID:ModelWriter,项目名称:Tarski,代码行数:13,代码来源:Solver.java


示例6: main

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
/**
 * Usage: java examples.alloy.ToyFilesystem
 */
public  static void main(String[] args) {
	final ToyFilesystem toy = new ToyFilesystem();
	final Formula f = toy.constraints();
	System.out.println(PrettyPrinter.print(f, 2));
	final Bounds b = toy.bounds();
	final Solver solver = new Solver();
	solver.options().setSolver(SATFactory.MiniSat);
	
	final Solution s = solver.solve(f, b);
	System.out.println(s);
}
 
开发者ID:emina,项目名称:kodkod,代码行数:15,代码来源:ToyFilesystem.java


示例7: printEncoding

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
static final void printEncoding(ListEncoding enc) {
	
	System.out.println("\n-----------trace expressions-----------");
	System.out.println("assume invariants(this, next, data, head) && this.head != null && this.head.next != null : ");
	System.out.println(PrettyPrinter.print(enc.pre(), 2));
	System.out.println("next = "+ enc.next);
	System.out.println("head = "+ enc.head);
	
	System.out.println("\nnearNode0 = "+ enc.nearNode0());
	System.out.println("midNode0 = "+ enc.midNode0());
	System.out.println("farNode0 = "+ enc.farNode0());
	
	System.out.println("\nnext0 = "+ enc.next0());
	
	System.out.println("\nguard0 (farNode0 != null) = "+ enc.guard0());
	System.out.println("next1 = "+ enc.next1());
	System.out.println("nearNode1 = "+ enc.nearNode1());
	System.out.println("midNode1 = "+ enc.midNode1());
	System.out.println("farNode1 = "+ enc.farNode1());
	
	System.out.println("\nnext2 = "+ enc.next2());
	System.out.println("nearNode2 = "+ enc.nearNode2());
	System.out.println("midNode2 = "+ enc.midNode2());
	System.out.println("farNode2 = "+ enc.farNode2());
	System.out.println("assume loopGuard (farNode2 = null) : " + enc.loopGuard());
	
	System.out.println("\nnext3 = "+ enc.next3());
	System.out.println("head0 = "+ enc.head0());
	
	System.out.println("\nassert invariants(this, next3, data, head0) &&\n"+
			"(let nodes = this.head.*next, nodes' = this.head0.*next3, ns = nodes - nil |\n" +
			"  nodes' = nodes and next3 & (ns -> ns) = ~(next & (ns -> ns))) :" );
	System.out.println(PrettyPrinter.print(enc.post(), 2));
	System.out.println();
}
 
开发者ID:emina,项目名称:kodkod,代码行数:36,代码来源:ListViz.java


示例8: main

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
/**
 * Usage:  java BlockedNQueens <file name>
 */
public static void main(String[] args) { 
	
	
	if (args.length < 1)
		usage();
	

	try {
					
		final BlockedNQueens2 model = new BlockedNQueens2(args[0]);
		
		final Formula f = model.rules();
		final Bounds b = model.bounds();
		final Solver s = new Solver();
		System.out.println(b);
		System.out.println(PrettyPrinter.print(f, 1));

		s.options().setSolver(SATFactory.MiniSat);
		s.options().setBitwidth(33 - Integer.numberOfLeadingZeros(b.universe().size()));
		s.options().setReporter(new ConsoleReporter());
		
		final Solution sol = s.solve(f, b);
		
		if (sol.instance()!=null) { 
			System.out.println("solution:");
			model.print(sol.instance(), s.options());
		} else {
			System.out.println("no solution");
		}
		System.out.println(sol.stats());
		
	} catch (NumberFormatException nfe) { 
		usage();
	}
	
}
 
开发者ID:emina,项目名称:kodkod,代码行数:40,代码来源:BlockedNQueens2.java


示例9: main

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
/**
	 * Usage:  java BlockedNQueens <file name>
	 */
	public static void main(String[] args) { 
		
		
		if (args.length < 1)
			usage();
		
	
		try {
						
			final BlockedNQueens model = new BlockedNQueens(args[0]);
			
			final Formula f = model.rules();
			final Bounds b = model.bounds();
			final Solver s = new Solver();
//			System.out.println(b);
			System.out.println(PrettyPrinter.print(f, 1));

			s.options().setSolver(SATFactory.MiniSat);
			s.options().setBitwidth(33 - Integer.numberOfLeadingZeros((b.universe().size()/2) - 1));
			s.options().setReporter(new ConsoleReporter());
			
			final Solution sol = s.solve(f, b);
			
			if (sol.instance()!=null) { 
				System.out.println("solution:");
				model.print(sol.instance(), s.options());
			} else {
				System.out.println("no solution");
			}
			System.out.println(sol.stats());
			
		} catch (NumberFormatException nfe) { 
			usage();
		}
		
	}
 
开发者ID:emina,项目名称:kodkod,代码行数:40,代码来源:BlockedNQueens.java


示例10: unsatCore

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
@Override
public String unsatCore() {
    Proof proof = solution.proof();
    if (proof == null)
        return "unknown";
    ReductionStrategy strategy = new AdaptiveRCEStrategy(proof.log()); 
    proof.minimize(strategy);
    int minCore = proof.highLevelCore().size();
    StringBuilder sb = new StringBuilder(); 
    sb.append("Core (size="+minCore+"):\n");
    for(Node n : proof.highLevelCore().values()) { 
        sb.append(PrettyPrinter.print(n, 0)).append("\n");
    }
    return sb.toString();
}
 
开发者ID:aleksandarmilicevic,项目名称:squander,代码行数:16,代码来源:SquanderKodkodImpl.java


示例11: main

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
/**
 * Usage: java examples.Hotel [scope]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final Hotel model = new Hotel();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSatProver);
		solver.options().setLogTranslation(1);

		final Formula f = model.checkNoBadEntry();
		final Bounds b = model.bounds(n);

		// System.out.println(PrettyPrinter.print(f, 2, 100));

		final Solution sol = solver.solve(f, b);
		System.out.println(sol);

		if (sol.instance() == null) {
			final Proof proof = sol.proof();
			System.out.println("top-level formulas: " + proof.log().roots().size());
			System.out.println("initial core: " + proof.highLevelCore().size());
			System.out.print("\nminimizing core ... ");
			final long start = System.currentTimeMillis();
			proof.minimize(new RCEStrategy(proof.log()));
			final Set<Formula> core = Nodes.minRoots(f, proof.highLevelCore().values());
			final long end = System.currentTimeMillis();
			System.out.println("done (" + (end - start) + " ms).");
			System.out.println("minimal core: " + core.size());
			for (Formula u : core) {
				System.out.println(PrettyPrinter.print(u, 2, 100));
			}
			checkMinimal(core, b);
		} else {
			System.out.println(sol);
		}
	} catch (NumberFormatException nfe) {
		usage();
	}
}
 
开发者ID:AlloyTools,项目名称:org.alloytools.alloy,代码行数:47,代码来源:Hotel.java


示例12: main

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
/**
	 * Usage: java examples.Hotel [scope]
	 */
	public static void main(String[] args) {
		if (args.length < 1)
			usage();
		
		try {
			final int n = Integer.parseInt(args[0]);
			if (n < 1)
				usage();
			final Hotel model = new Hotel();
			final Solver solver = new Solver();
			solver.options().setSolver(SATFactory.MiniSatProver);
			solver.options().setLogTranslation(1);
			
			final Formula f = model.checkNoBadEntry();
			final Bounds b = model.bounds(n);
	
//			System.out.println(PrettyPrinter.print(f, 2, 100));
			
			final Solution sol = solver.solve(f, b);
			System.out.println(sol);
		
			if (sol.instance()==null) { 
				final Proof proof = sol.proof();
				System.out.println("top-level formulas: " + proof.log().roots().size());
				System.out.println("initial core: " + proof.highLevelCore().size());
				System.out.print("\nminimizing core ... ");
				final long start = System.currentTimeMillis();
				proof.minimize(new RCEStrategy(proof.log()));
				final Set<Formula> core = Nodes.minRoots(f, proof.highLevelCore().values());
				final long end = System.currentTimeMillis();
				System.out.println("done (" + (end-start) + " ms).");
				System.out.println("minimal core: " + core.size());
				for(Formula u : core) { 
					System.out.println(PrettyPrinter.print(u, 2, 100));
				}
				checkMinimal(core, b);
			} else {
				System.out.println(sol);
			}
		} catch (NumberFormatException nfe) {
			usage();
		}
	}
 
开发者ID:emina,项目名称:kodkod,代码行数:47,代码来源:Hotel.java


示例13: print

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
void print(Set<Formula> core) { 
	System.out.println(PrettyPrinter.print(core, 3));
}
 
开发者ID:emina,项目名称:kodkod,代码行数:4,代码来源:ListDebug.java


示例14: main

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
/**
	 * Usage:  java NQueens <number of queens> <encoding: int | log | rel>
	 */
	public static void main(String[] args) { 
		if (args.length < 2)
			usage();
		
		try {
			final int n = Integer.parseInt(args[0]);
			if (n < 1 || n <= 0)
				usage();
			
			final NQueens model; 
			if (args[1].compareToIgnoreCase("int")==0) {
				model = new IntQueens(n);
			} else if (args[1].compareToIgnoreCase("log")==0) {
				model = new LogQueens(n);
			} else if (args[1].compareToIgnoreCase("rel")==0) {
				model = new RelQueens(n);
			} else {
				usage();
				return;
			}
			
			final Formula f = model.rules();
			final Bounds b = model.bounds();
			final Solver s = new Solver();
//			System.out.println(b);
			System.out.println("encoding:");
			System.out.println(PrettyPrinter.print(f, 1));

			s.options().setSolver(SATFactory.MiniSat);
			s.options().setBitwidth(33 - Integer.numberOfLeadingZeros(n - 1));
			s.options().setReporter(new ConsoleReporter());
			
			final Solution sol = s.solve(f, b);
			
			if (sol.instance()!=null) { 
				System.out.println("solution:");
				model.print(sol.instance(), s.options());
			} else {
				System.out.println("no solution");
			}
			System.out.println(sol.stats());
			
		} catch (NumberFormatException nfe) { 
			usage();
		}
		
	}
 
开发者ID:emina,项目名称:kodkod,代码行数:51,代码来源:NQueens.java


示例15: exeSpec

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
@Override
    protected IEvaluator exeSpec(ForgeExpression spec, Set<GlobalVariable> modifies, ForgeConverter fconv) {
        this.modifies = modifies;
        this.fconv = fconv;
        this.forgeScene = fconv.forgeScene();
        this.program = forgeScene.program();

        init();
        
        createRelations();
          
        Bounds bounds = createBounds();
        Log.log(printBoundsSummary(bounds));
        
        Formula formula = convertSpec(spec);
        
        Solver solver = new Solver();
        Log.log("Using bitwidth: " + fconv.bw()); 
        solver.options().setBitwidth(fconv.bw());
//        solver.options().setFlatten(false);
        solver.options().setReporter(SquanderGlobalOptions.INSTANCE.reporter.kkReporter());
        solver.options().setNoOverflow(SquanderGlobalOptions.INSTANCE.noOverflow);
        if (SquanderGlobalOptions.INSTANCE.unsat_core) {
            solver.options().setLogTranslation(1);
            solver.options().setSolver(SATFactory.MiniSatProver); // TODO: read from global options
            solver.options().setCoreGranularity(3);
        } else {
            solver.options().setLogTranslation(0);
            solver.options().setSolver(SquanderGlobalOptions.INSTANCE.sat_solver); 
        }
        
        boolean solveAll = false;
        Options opts = fconv.javaScene().methodSpec().options();
        if (opts != null)
            solveAll = opts.solveAll();
        
        if (solveAll)
            solver.options().setSymmetryBreaking(1000);
        
        Log.debug("==============================================");
        Log.debug("------------- Solving kk formula -------------");
        Log.debug("==============================================");
        Log.debug(PrettyPrinter.print(formula, 2));
        Log.debug("\n" + bounds);
        IEvaluator eval;
        //new KKSimplifier().simplify(formula, bounds);
        if (solveAll) {
            Iterator<Solution> solutions = solver.solveAll(formula, bounds);
            eval = getEval(solutions, solver.options());
        } else {
            Solution solution = solver.solve(formula, bounds);
            eval = getEval(Collections.singleton(solution).iterator(), solver.options());
        }
        return eval;
    }
 
开发者ID:aleksandarmilicevic,项目名称:squander,代码行数:56,代码来源:SquanderKodkodImpl.java


示例16: simplify

import kodkod.util.nodes.PrettyPrinter; //导入依赖的package包/类
public Formula simplify(Formula f, Bounds b) {
    System.out.println(PrettyPrinter.print(f, 0));
    System.exit(23);
    return null;
}
 
开发者ID:aleksandarmilicevic,项目名称:squander,代码行数:6,代码来源:KKSimplifier.java



注:本文中的kodkod.util.nodes.PrettyPrinter类示例整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。


鲜花

握手

雷人

路过

鸡蛋
该文章已有0人参与评论

请发表评论

全部评论

专题导读
上一篇:
Java DebouncingOnClickListener类代码示例发布时间:2022-05-22
下一篇:
Java IRI类代码示例发布时间:2022-05-22
热门推荐
阅读排行榜

扫描微信二维码

查看手机版网站

随时了解更新最新资讯

139-2527-9053

在线客服(服务时间 9:00~18:00)

在线QQ客服
地址:深圳市南山区西丽大学城创智工业园
电邮:jeky_zhao#qq.com
移动电话:139-2527-9053

Powered by 互联科技 X3.4© 2001-2213 极客世界.|Sitemap