Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
90   189   13   15
6   147   0.14   6
6     2.17  
1    
 
  ProofFinderImplTest       Line # 44 90 13 96.1% 0.9607843
 
  (3)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15    package org.qedeq.kernel.bo.logic.proof.finder;
16   
17    import java.io.File;
18    import java.io.IOException;
19    import java.io.OutputStream;
20    import java.io.PrintStream;
21    import java.util.HashMap;
22    import java.util.Map;
23   
24    import org.qedeq.base.io.Parameters;
25    import org.qedeq.kernel.bo.KernelContext;
26    import org.qedeq.kernel.bo.log.ModuleLogListenerImpl;
27    import org.qedeq.kernel.bo.logic.proof.common.ProofFinder;
28    import org.qedeq.kernel.bo.logic.proof.common.ProofFoundException;
29    import org.qedeq.kernel.bo.logic.proof.common.ProofNotFoundException;
30    import org.qedeq.kernel.bo.module.KernelNodeBo;
31    import org.qedeq.kernel.bo.module.KernelQedeqBo;
32    import org.qedeq.kernel.bo.test.QedeqBoTestCase;
33    import org.qedeq.kernel.se.base.module.FormalProofLineList;
34    import org.qedeq.kernel.se.base.module.Proposition;
35    import org.qedeq.kernel.se.common.DefaultModuleAddress;
36    import org.qedeq.kernel.se.common.ModuleAddress;
37    import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
38   
39    /**
40    * For testing of finding formal proofs.
41    *
42    * @author Michael Meyling
43    */
 
44    public class ProofFinderImplTest extends QedeqBoTestCase {
45   
46    /**
47    * Find a proof.
48    *
49    * @throws Exception
50    */
 
51  1 toggle public void testFind() throws Exception {
52  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
53    "sample/qedeq_sample3.xml"));
54  1 KernelContext.getInstance().checkWellFormedness(address);
55  1 final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address);
56  1 assertTrue(bo.isWellFormed());
57  1 assertNotNull(bo.getWarnings());
58  1 assertEquals(0, bo.getWarnings().size());
59  1 assertEquals(0, bo.getErrors().size());
60  1 final KernelNodeBo node = bo.getLabels().getNode("proposition:one");
61  1 final Proposition prop = node.getNodeVo().getNodeType().getProposition();
62  1 final ProofFinder finder = new ProofFinderImpl();
63  1 final FormalProofLineList original = prop.getFormalProofList().get(0)
64    .getFormalProofLineList();
65  1 final FormalProofLineListVo list = new FormalProofLineListVo();
66  5 for (int i = 0; i < 4; i++) {
67  4 list.add(original.get(i));
68    }
69  1 final Map parameters = new HashMap();
70  1 parameters.put("extraVars", "0");
71  1 parameters.put("maximumProofLines", "100000");
72  1 parameters.put("propositionVariableOrder", "2");
73  1 parameters.put("propositionVariableWeight", "3");
74  1 parameters.put("partFormulaWeight", "0");
75  1 parameters.put("disjunctionOrder", "1");
76  1 parameters.put("disjunctionWeight", "3");
77  1 parameters.put("implicationWeight", "0");
78  1 parameters.put("negationWeight", "0");
79  1 parameters.put("conjunctionWeight", "0");
80  1 parameters.put("equivalenceWeight", "0");
81  1 try {
82  1 finder.findProof(prop.getFormula().getElement(), list,
83    DefaultModuleAddress.MEMORY.createModuleContext(), new Parameters(parameters),
84    new ModuleLogListenerImpl("memory", new PrintStream(new OutputStream() {
 
85  2339 toggle public void write(int b) throws IOException {
86    }})), bo.getElement2Utf8());
87  0 fail("no proof found");
88    } catch (ProofFoundException e) {
89  1 assertNotNull(e.getProofLines());
90    }
91    }
92   
93    /**
94    * Find a proof.
95    *
96    * @throws Exception
97    */
 
98  1 toggle public void testFind2() throws Exception {
99  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
100    "sample/qedeq_sample3.xml"));
101  1 KernelContext.getInstance().checkWellFormedness(address);
102  1 final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address);
103  1 assertTrue(bo.isWellFormed());
104  1 assertNotNull(bo.getWarnings());
105  1 assertEquals(0, bo.getWarnings().size());
106  1 assertEquals(0, bo.getErrors().size());
107  1 final KernelNodeBo node = bo.getLabels().getNode("proposition:two");
108  1 final Proposition prop = node.getNodeVo().getNodeType().getProposition();
109  1 final ProofFinder finder = new ProofFinderImpl();
110  1 final FormalProofLineList original = prop.getFormalProofList().get(0)
111    .getFormalProofLineList();
112  1 final FormalProofLineListVo list = new FormalProofLineListVo();
113  4 for (int i = 0; i < 3; i++) {
114  3 list.add(original.get(i));
115    }
116  1 final Map parameters = new HashMap();
117  1 parameters.put("extraVars", "0");
118  1 parameters.put("maximumProofLines", "100000");
119  1 parameters.put("propositionVariableOrder", "2");
120  1 parameters.put("propositionVariableWeight", "3");
121  1 parameters.put("partFormulaWeight", "0");
122  1 parameters.put("disjunctionOrder", "1");
123  1 parameters.put("disjunctionWeight", "3");
124  1 parameters.put("implicationWeight", "0");
125  1 parameters.put("negationWeight", "0");
126  1 parameters.put("conjunctionWeight", "0");
127  1 parameters.put("equivalenceWeight", "0");
128  1 try {
129  1 finder.findProof(prop.getFormula().getElement(), list,
130    DefaultModuleAddress.MEMORY.createModuleContext(), new Parameters(parameters),
131    new ModuleLogListenerImpl("memory", new PrintStream(new OutputStream() {
 
132  2281 toggle public void write(int b) throws IOException {
133    }})), bo.getElement2Utf8());
134  0 fail("no proof found");
135    } catch (ProofFoundException e) {
136  1 assertNotNull(e.getProofLines());
137    }
138    }
139   
140    /**
141    * Find a proof.
142    *
143    * @throws Exception
144    */
 
145  1 toggle public void testFind3() throws Exception {
146  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
147    "sample/qedeq_sample3.xml"));
148  1 KernelContext.getInstance().checkWellFormedness(address);
149  1 final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address);
150  1 assertTrue(bo.isWellFormed());
151  1 assertNotNull(bo.getWarnings());
152  1 assertEquals(0, bo.getWarnings().size());
153  1 assertEquals(0, bo.getErrors().size());
154  1 final KernelNodeBo node = bo.getLabels().getNode("proposition:one");
155  1 final Proposition prop = node.getNodeVo().getNodeType().getProposition();
156  1 final ProofFinder finder = new ProofFinderImpl();
157  1 final FormalProofLineList original = prop.getFormalProofList().get(0)
158    .getFormalProofLineList();
159  1 final FormalProofLineListVo list = new FormalProofLineListVo();
160  5 for (int i = 0; i < 4; i++) {
161  4 list.add(original.get(i));
162    }
163  1 final Map parameters = new HashMap();
164  1 parameters.put("extraVars", "0");
165  1 parameters.put("maximumProofLines", "10");
166  1 parameters.put("propositionVariableOrder", "2");
167  1 parameters.put("propositionVariableWeight", "3");
168  1 parameters.put("partFormulaWeight", "0");
169  1 parameters.put("disjunctionOrder", "1");
170  1 parameters.put("disjunctionWeight", "3");
171  1 parameters.put("implicationWeight", "0");
172  1 parameters.put("negationWeight", "0");
173  1 parameters.put("conjunctionWeight", "0");
174  1 parameters.put("equivalenceWeight", "0");
175  1 try {
176  1 finder.findProof(prop.getFormula().getElement(), list,
177    DefaultModuleAddress.MEMORY.createModuleContext(), new Parameters(parameters),
178    new ModuleLogListenerImpl("memory", new PrintStream(new OutputStream() {
 
179  562 toggle public void write(int b) throws IOException {
180    }})), bo.getElement2Utf8());
181  0 fail("no proof found");
182    } catch (ProofFoundException e) {
183  0 fail("should not find a proof");
184    } catch (ProofNotFoundException e) {
185    // expected
186    }
187    }
188   
189    }
 
CloverReport generated by Clover Code Coverage v3.1.10
Fri May 24 2013 13:47:32 UTC.		   Clover: Open Source License registered to qedeq.org .