View Javadoc

1   /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    * 
4    * Based on the original minisat specification from:
5    * 
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    * 
10   * This library is free software; you can redistribute it and/or modify it under
11   * the terms of the GNU Lesser General Public License as published by the Free
12   * Software Foundation; either version 2.1 of the License, or (at your option)
13   * any later version.
14   * 
15   * This library is distributed in the hope that it will be useful, but WITHOUT
16   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18   * details.
19   * 
20   * You should have received a copy of the GNU Lesser General Public License
21   * along with this library; if not, write to the Free Software Foundation, Inc.,
22   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
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   * A predicate is a formula given in intension.
45   * 
46   * @author daniel
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          // cx.setOptimizationLevel(1);
63          scope = cx.initStandardObjects();
64          // System.out.println("scope "+vscope);
65          // System.out.println("params "+vars);
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              // TODO Auto-generated catch block
73              e.printStackTrace();
74          } catch (IOException e) {
75              // TODO Auto-generated catch block
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 }