Java PrettyPrinter类代码示例

OGeek|极客世界-中国程序员成长平台 › 门户 › 编程› Java›Java编程经验

原作者: [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人参与评论

请发表评论

全部评论

专题导读

More+

10-27 六六分期app的软件客服如何联系？(六六分期

11-06 可心卡盟:win10系统火狐flash插件崩溃怎么

11-06 亲亲特价:怎么删除回收站图标

11-06 济南大学虚拟社区:鲁大师节能降温的具体办

11-06 xlueops.exe:无线网络安装向导

11-06 女斗合众国:win7系统cf与主机连接不稳定怎

11-06 0xc000022-[cf烟雾头]cf怎么调烟雾头

11-06 qizideyouhuo:应用程序无法正常启动0xc0000

11-06 ipz-185:win7系统vcf文件怎么打开

11-06 傻哥蹦迪:win10系统s4怎么打开usb调试

11-06 八神浩树gtaste:回收站清空了怎么恢复

11-06 妖尾之黑色守护:win10系统电脑没有1440x900

11-06 校园至尊魔王小说:win7系统浏览网页时字体

11-06 女斗合众国:win10系统访问共享文件夹提示请

11-06 tokyo hot n0654:恢复win7系统默认字体一招

11-06 雨酷仙境:设置win7系统转移临时文件夹腾出

11-06 阿穆纳伊之杖:win7系统开始菜单在右边还原

11-06 tunespotting:win10系统火狐flash插件总是

11-06 甘尔葛分析师：计谋网站seo关键词暴涨有什

11-06 蔡贵霖: 计谋网站seo关键词暴涨有什么秘密

11-06 博益网首页:ao3网页版进入不了解决方法

11-06 漏斗子专栏: 网站数据分析小白易懂精华篇

11-06 见证双虹怎么做:win7系统开启telnet命令的

11-06 颾狐蝶蜋:系统资源不足无法完成请求的服务

11-06 国光中学校歌:提交网站到alexa查询详细步骤

11-06 西安有情天:静态网页和动态网页的区别

11-06 红木雅尚斋:外部链接构造对网站的好处

11-06 前官礼遇：防止域名劫持–增强域安全性的10

11-06 密传二转答案: 中文分词算法有哪些

11-06 金泉家园邮编:百度快照劫持的表现及应对方

Java DebouncingOnClickListener类代码示例发布时间：2022-05-22

Java IRI类代码示例发布时间：2022-05-22

剪的笔顺,诠释剪的笔画,认识剪的部首

1 六六分期app的软件客服如何联系？(六六分期

六六分期app的软件客服如何联系？不知道吗？加qq群【895510560】即可！标题：六六分期

阅读：18271|2023-10-27

2 可心卡盟:win10系统火狐flash插件崩溃怎么

今天小编告诉大家如何处理win10系统火狐flash插件总是崩溃的问题，可能很多用户都不知

阅读：9677|2022-11-06

3 亲亲特价:怎么删除回收站图标

今天小编告诉大家如何对win10系统删除桌面回收站图标进行设置，可能很多用户都不知道

阅读：8179|2022-11-06

4 济南大学虚拟社区:鲁大师节能降温的具体办

今天小编告诉大家如何对win10系统电脑设置节能降温的设置方法，想必大家都遇到过需要

阅读：8549|2022-11-06

5 xlueops.exe:无线网络安装向导

我们在使用xp系统的过程中,经常需要对xp系统无线网络安装向导设置进行设置，可能很多

阅读：8457|2022-11-06

6 女斗合众国:win7系统cf与主机连接不稳定怎

今天小编告诉大家如何处理win7系统玩cf老是与主机连接不稳定的问题，可能很多用户都不

阅读：9392|2022-11-06

7 0xc000022-[cf烟雾头]cf怎么调烟雾头

电脑对日常生活的重要性小编就不多说了，可是一旦碰到win7系统设置cf烟雾头的问题，很

阅读：8430|2022-11-06

8 qizideyouhuo:应用程序无法正常启动0xc0000

我们在日常使用电脑的时候，有的小伙伴们可能在打开应用的时候会遇见提示应用程序无法

阅读：7865|2022-11-06

9 ipz-185:win7系统vcf文件怎么打开

今天小编告诉大家如何对win7系统打开vcf文件进行设置，可能很多用户都不知道怎么对win

阅读：8415|2022-11-06

10 傻哥蹦迪:win10系统s4怎么打开usb调试

今天小编告诉大家如何对win10系统s4开启USB调试模式进行设置，可能很多用户都不知道怎

阅读：7394|2022-11-06

客服电话

电子邮件

Java PrettyPrinter类代码示例

示例1: main

示例2: main

示例3: printFalse

示例4: printUnsat

示例5: flushFormula

示例6: main

示例7: printEncoding

示例8: main

示例9: main

示例10: unsatCore

示例11: main

示例12: main

示例13: print

示例14: main

示例15: exeSpec

示例16: simplify

请发表评论

全部评论

上一篇：

下一篇：

creativetimofficial/material-dashboard-r

CVE-2022-30517

pngwn/MDsveX: A markdown preprocessor fo

kubernetes/examples: Kubernetes applicat

中国4a广告公司100强图谱

剪的笔顺,诠释剪的笔画,认识剪的部首

六六分期app的软件客服如何联系？(六六分期

florent37/ViewAnimator: A fluent Android

florent37/Shrine-MaterialDesign2: implem

CVE-2020-36276

SimpleSoftwareIO/simple-sms: Send and re

关于我们

产品与服务

解决方案

139-2527-9053