| 1032 | // / Shows how to read an SMT2 file. |
| 1033 | |
| 1034 | void smt2FileTest(String filename) |
| 1035 | { |
| 1036 | Date before = new Date(); |
| 1037 | |
| 1038 | System.out.println("SMT2 File test "); |
| 1039 | System.gc(); |
| 1040 | |
| 1041 | { |
| 1042 | HashMap<String, String> cfg = new HashMap<String, String>(); |
| 1043 | cfg.put("model", "true"); |
| 1044 | Context ctx = new Context(cfg); |
| 1045 | BoolExpr a = ctx.mkAnd(ctx.parseSMTLIB2File(filename, null, null, null, null)); |
| 1046 | |
| 1047 | long t_diff = ((new Date()).getTime() - before.getTime()) / 1000; |
| 1048 | |
| 1049 | System.out.println("SMT2 file read time: " + t_diff + " sec"); |
| 1050 | |
| 1051 | // Iterate over the formula. |
| 1052 | |
| 1053 | LinkedList<Expr> q = new LinkedList<Expr>(); |
| 1054 | q.add(a); |
| 1055 | int cnt = 0; |
| 1056 | while (q.size() > 0) |
| 1057 | { |
| 1058 | AST cur = (AST) q.removeFirst(); |
| 1059 | cnt++; |
| 1060 | |
| 1061 | if (cur.getClass() == Expr.class) |
| 1062 | if (!(cur.isVar())) |
| 1063 | for (Expr c : ((Expr) cur).getArgs()) |
| 1064 | q.add(c); |
| 1065 | } |
| 1066 | System.out.println(cnt + " ASTs"); |
| 1067 | } |
| 1068 | |
| 1069 | long t_diff = ((new Date()).getTime() - before.getTime()) / 1000; |
| 1070 | System.out.println("SMT2 file test took " + t_diff + " sec"); |
| 1071 | } |
| 1072 | |
| 1073 | // / Shows how to use Solver(logic) |
| 1074 | |