Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
39   148   11   5,57
18   95   0,44   7
7     2,43  
1    
 
  Predicate       Line # 48 39 11 0% 0.0
 
No Tests
 
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  0 toggle static {
61  0 cx = Context.enter();
62    // cx.setOptimizationLevel(1);
63  0 scope = cx.initStandardObjects();
64    // System.out.println("scope "+vscope);
65    // System.out.println("params "+vars);
66  0 try {
67  0 URL url = Predicate.class.getResource("predefinedfunctions.js");
68  0 cx.evaluateReader(scope, new InputStreamReader(url.openStream()),
69    "predefinedfunctions.js", 1, null);
70   
71    } catch (FileNotFoundException e) {
72    // TODO Auto-generated catch block
73  0 e.printStackTrace();
74    } catch (IOException e) {
75    // TODO Auto-generated catch block
76  0 e.printStackTrace();
77    }
78    }
79   
 
80  0 toggle public Predicate() {
81    }
82   
 
83  0 toggle public void setExpression(String expr) {
84  0 this.expr = expr;
85    }
86   
 
87  0 toggle public void addVariable(String name) {
88  0 variables.push(name);
89    }
90   
 
91  0 toggle private boolean evaluate(int[] values) {
92  0 assert values.length == variables.size();
93  0 for (int i = 0; i < variables.size(); i++) {
94  0 scope.put(variables.get(i), scope, values[i]);
95    }
96  0 Object result = myscript.exec(cx, scope);
97  0 return Context.toBoolean(result);
98    }
99   
 
100  0 toggle public void toClause(ISolver solver, IVec<Var> vscope, IVec<Evaluable> vars)
101    throws ContradictionException {
102  0 if (myscript == null) {
103  0 myscript = cx.compileString(expr, "rhino.log", 1, null);
104    }
105  0 if (vscope.size() == 2) {
106  0 encoding = BinarySupportEncoding.instance();
107    } else {
108  0 encoding = DirectEncoding.instance();
109    }
110  0 encoding.onInit(solver, vscope);
111  0 int[] tuple = new int[vars.size()];
112  0 valuemapping.clear();
113  0 find(tuple, 0, vscope, vars, solver);
114  0 encoding.onFinish(solver, vscope);
115    }
116   
117    private final Map<Evaluable, Integer> valuemapping = new HashMap<Evaluable, Integer>();
118   
119    private Script myscript;
120   
 
121  0 toggle private void find(int[] tuple, int n, IVec<Var> scope,
122    IVec<Evaluable> vars, ISolver solver) throws ContradictionException {
123  0 if (valuemapping.size() == scope.size()) {
124  0 for (int i = 0; i < tuple.length; i++) {
125  0 Evaluable ev = vars.get(i);
126  0 Integer value = valuemapping.get(ev);
127  0 if (value == null) {
128  0 tuple[i] = ev.domain().get(0);
129    } else {
130  0 tuple[i] = value;
131    }
132    }
133  0 if (evaluate(tuple)) {
134  0 encoding.onSupport(solver, scope, valuemapping);
135    } else {
136  0 encoding.onNogood(solver, scope, valuemapping);
137    }
138    } else {
139  0 Var var = scope.get(n);
140  0 Domain domain = var.domain();
141  0 for (int i = 0; i < domain.size(); i++) {
142  0 valuemapping.put(var, domain.get(i));
143  0 find(tuple, n + 1, scope, vars, solver);
144    }
145  0 valuemapping.remove(var);
146    }
147    }
148    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.