1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26 package org.sat4j.reader.csp;
27
28 import java.io.FileNotFoundException;
29 import java.io.IOException;
30 import java.io.InputStreamReader;
31 import java.net.URL;
32 import java.util.HashMap;
33 import java.util.Map;
34
35 import org.mozilla.javascript.Context;
36 import org.mozilla.javascript.Script;
37 import org.mozilla.javascript.Scriptable;
38 import org.sat4j.core.Vec;
39 import org.sat4j.specs.ContradictionException;
40 import org.sat4j.specs.ISolver;
41 import org.sat4j.specs.IVec;
42
43
44
45
46
47
48 public class Predicate implements Clausifiable {
49
50 private String expr;
51
52 private Encoding encoding;
53
54 private final IVec<String> variables = new Vec<String>();
55
56 private static Context cx;
57
58 private static Scriptable scope;
59
60 static {
61 cx = Context.enter();
62
63 scope = cx.initStandardObjects();
64
65
66 try {
67 URL url = Predicate.class.getResource("predefinedfunctions.js");
68 cx.evaluateReader(scope, new InputStreamReader(url.openStream()),
69 "predefinedfunctions.js", 1, null);
70
71 } catch (FileNotFoundException e) {
72
73 e.printStackTrace();
74 } catch (IOException e) {
75
76 e.printStackTrace();
77 }
78 }
79
80 public Predicate() {
81 }
82
83 public void setExpression(String expr) {
84 this.expr = expr;
85 }
86
87 public void addVariable(String name) {
88 variables.push(name);
89 }
90
91 private boolean evaluate(int[] values) {
92 assert values.length == variables.size();
93 for (int i = 0; i < variables.size(); i++) {
94 scope.put(variables.get(i), scope, values[i]);
95 }
96 Object result = myscript.exec(cx, scope);
97 return Context.toBoolean(result);
98 }
99
100 public void toClause(ISolver solver, IVec<Var> vscope, IVec<Evaluable> vars)
101 throws ContradictionException {
102 if (myscript == null) {
103 myscript = cx.compileString(expr, "rhino.log", 1, null);
104 }
105 if (vscope.size() == 2) {
106 encoding = BinarySupportEncoding.instance();
107 } else {
108 encoding = DirectEncoding.instance();
109 }
110 encoding.onInit(solver, vscope);
111 int[] tuple = new int[vars.size()];
112 valuemapping.clear();
113 find(tuple, 0, vscope, vars, solver);
114 encoding.onFinish(solver, vscope);
115 }
116
117 private final Map<Evaluable, Integer> valuemapping = new HashMap<Evaluable, Integer>();
118
119 private Script myscript;
120
121 private void find(int[] tuple, int n, IVec<Var> scope,
122 IVec<Evaluable> vars, ISolver solver) throws ContradictionException {
123 if (valuemapping.size() == scope.size()) {
124 for (int i = 0; i < tuple.length; i++) {
125 Evaluable ev = vars.get(i);
126 Integer value = valuemapping.get(ev);
127 if (value == null) {
128 tuple[i] = ev.domain().get(0);
129 } else {
130 tuple[i] = value;
131 }
132 }
133 if (evaluate(tuple)) {
134 encoding.onSupport(solver, scope, valuemapping);
135 } else {
136 encoding.onNogood(solver, scope, valuemapping);
137 }
138 } else {
139 Var var = scope.get(n);
140 Domain domain = var.domain();
141 for (int i = 0; i < domain.size(); i++) {
142 valuemapping.put(var, domain.get(i));
143 find(tuple, n + 1, scope, vars, solver);
144 }
145 valuemapping.remove(var);
146 }
147 }
148 }