001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.service.logic;
017
018 import java.io.File;
019
020 import org.qedeq.base.io.Parameters;
021 import org.qedeq.base.trace.Trace;
022 import org.qedeq.base.utility.YodaUtility;
023 import org.qedeq.kernel.bo.common.PluginExecutor;
024 import org.qedeq.kernel.bo.log.ModuleLogListener;
025 import org.qedeq.kernel.bo.log.QedeqLog;
026 import org.qedeq.kernel.bo.logic.ProofFinderFactoryImpl;
027 import org.qedeq.kernel.bo.logic.proof.common.ProofFinder;
028 import org.qedeq.kernel.bo.logic.proof.common.ProofFinderFactory;
029 import org.qedeq.kernel.bo.logic.proof.common.ProofFoundException;
030 import org.qedeq.kernel.bo.logic.proof.common.ProofNotFoundException;
031 import org.qedeq.kernel.bo.module.ControlVisitor;
032 import org.qedeq.kernel.bo.module.KernelQedeqBo;
033 import org.qedeq.kernel.bo.module.QedeqFileDao;
034 import org.qedeq.kernel.se.base.module.Axiom;
035 import org.qedeq.kernel.se.base.module.FormalProofLineList;
036 import org.qedeq.kernel.se.base.module.FunctionDefinition;
037 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
038 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
039 import org.qedeq.kernel.se.base.module.PredicateDefinition;
040 import org.qedeq.kernel.se.base.module.Proposition;
041 import org.qedeq.kernel.se.base.module.Rule;
042 import org.qedeq.kernel.se.common.LogicalModuleState;
043 import org.qedeq.kernel.se.common.ModuleDataException;
044 import org.qedeq.kernel.se.common.Plugin;
045 import org.qedeq.kernel.se.common.SourceFileExceptionList;
046 import org.qedeq.kernel.se.dto.module.AddVo;
047 import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
048 import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
049 import org.qedeq.kernel.se.dto.module.FormalProofVo;
050 import org.qedeq.kernel.se.dto.module.FormulaVo;
051 import org.qedeq.kernel.se.dto.module.PropositionVo;
052
053
054 /**
055 * Finds simple formal proofs.
056 *
057 * @author Michael Meyling
058 */
059 public final class SimpleProofFinderExecutor extends ControlVisitor implements PluginExecutor {
060
061 /** This class. */
062 private static final Class CLASS = SimpleProofFinderExecutor.class;
063
064 /** Factory for generating new checkers. */
065 private ProofFinderFactory finderFactory = null;
066
067 /** List of axioms, definitions and propositions. */
068 private FormalProofLineListVo validFormulas;
069
070 /** Save changed modules directly? */
071 private boolean noSave;
072
073 /** Currently running proof finder. */
074 private ProofFinder finder;
075
076 /** All parameters for this search. */
077 private Parameters parameters;
078
079 /**
080 * Constructor.
081 *
082 * @param plugin This plugin we work for.
083 * @param qedeq QEDEQ BO object.
084 * @param parameters Parameters.
085 */
086 SimpleProofFinderExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
087 final Parameters parameters) {
088 super(plugin, qedeq);
089 final String method = "SimpleProofFinderExecutor(Plugin, KernelQedeqBo, Map)";
090 final String finderFactoryClass = parameters.getString("checkerFactory");
091 if (finderFactoryClass != null && finderFactoryClass.length() > 0) {
092 try {
093 Class cl = Class.forName(finderFactoryClass);
094 finderFactory = (ProofFinderFactory) cl.newInstance();
095 } catch (ClassNotFoundException e) {
096 Trace.fatal(CLASS, this, method, "ProofFinderFactory class not in class path: "
097 + finderFactoryClass, e);
098 } catch (InstantiationException e) {
099 Trace.fatal(CLASS, this, method, "ProofFinderFactory class could not be instanciated: "
100 + finderFactoryClass, e);
101 } catch (IllegalAccessException e) {
102 Trace.fatal(CLASS, this, method,
103 "Programming error, access for instantiation failed for model: "
104 + finderFactoryClass, e);
105 } catch (RuntimeException e) {
106 Trace.fatal(CLASS, this, method,
107 "Programming error, instantiation failed for model: " + finderFactoryClass, e);
108 }
109 }
110 // fallback is the default finder factory
111 if (finderFactory == null) {
112 finderFactory = new ProofFinderFactoryImpl();
113 }
114 noSave = parameters.getBoolean("noSave");
115 this.parameters = parameters;
116 }
117
118 public Object executePlugin() {
119 getServices().checkModule(getQedeqBo().getModuleAddress());
120 QedeqLog.getInstance().logRequest("Trying to create formal proofs", getQedeqBo().getUrl());
121 try {
122 validFormulas = new FormalProofLineListVo();
123 traverse();
124 QedeqLog.getInstance().logSuccessfulReply(
125 "Proof creation finished for", getQedeqBo().getUrl());
126 } catch (SourceFileExceptionList e) {
127 final String msg = "Proof creation not (fully?) successful";
128 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage());
129 return Boolean.FALSE;
130 } finally {
131 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
132 }
133 return Boolean.TRUE;
134 }
135
136 public void visitEnter(final Axiom axiom) throws ModuleDataException {
137 if (axiom == null) {
138 return;
139 }
140 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
141 new AddVo(getNodeBo().getNodeVo().getId())));
142 setBlocked(true);
143 }
144
145 public void visitLeave(final Axiom axiom) {
146 setBlocked(false);
147 }
148
149 public void visitEnter(final PredicateDefinition definition)
150 throws ModuleDataException {
151 if (definition == null) {
152 return;
153 }
154 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
155 new AddVo(getNodeBo().getNodeVo().getId())));
156 setBlocked(true);
157 }
158
159 public void visitLeave(final PredicateDefinition definition) {
160 setBlocked(false);
161 }
162
163 public void visitEnter(final InitialPredicateDefinition definition)
164 throws ModuleDataException {
165 setBlocked(true);
166 }
167
168 public void visitLeave(final InitialPredicateDefinition definition) {
169 setBlocked(false);
170 }
171
172 public void visitEnter(final InitialFunctionDefinition definition)
173 throws ModuleDataException {
174 setBlocked(true);
175 }
176
177 public void visitLeave(final InitialFunctionDefinition definition) {
178 setBlocked(false);
179 }
180
181 public void visitEnter(final FunctionDefinition definition)
182 throws ModuleDataException {
183 if (definition == null) {
184 return;
185 }
186 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
187 new AddVo(getNodeBo().getNodeVo().getId())));
188 setBlocked(true);
189 }
190
191 public void visitLeave(final FunctionDefinition definition) {
192 setBlocked(false);
193 }
194
195 public void visitEnter(final Proposition proposition)
196 throws ModuleDataException {
197 final String method = "visitEnter(Proposition)";
198 Trace.begin(CLASS, this, method);
199 if (proposition == null) {
200 Trace.end(CLASS, this, method);
201 return;
202 }
203 if (proposition.getFormalProofList() == null) {
204 FormalProofLineList proof = null;
205 // we try finding a proof
206 try {
207 finder = finderFactory.createProofFinder();
208 finder.findProof(proposition.getFormula().getElement(), validFormulas,
209 getCurrentContext(), parameters, new ModuleLogListener() {
210 public void logMessageState(final String text) {
211 QedeqLog.getInstance().logMessageState(text, getQedeqBo().getUrl());
212 }
213 }, getQedeqBo().getElement2Utf8());
214 } catch (ProofFoundException e) {
215 proof = e.getProofLines();
216 } catch (ProofNotFoundException e) {
217 proof = null;
218 addWarning(e);
219 } finally {
220 finder = null; // so we always new if we are currently searching
221 }
222 if (proof != null) {
223 QedeqLog.getInstance().logMessage("proof found for "
224 + super.getLocationDescription());
225 // TODO 20110323 m31: we do a dirty cast to modify the current module
226 Object state;
227 try {
228 state = YodaUtility.getFieldValue(getQedeqBo(), "stateManager");
229 YodaUtility.executeMethod(state, "setLogicalState", new Class[] {
230 LogicalModuleState.class},
231 new Object[] {LogicalModuleState.STATE_UNCHECKED});
232 ((PropositionVo) proposition).addFormalProof(new FormalProofVo(proof));
233 YodaUtility.executeMethod(state, "setErrors", new Class[] {
234 SourceFileExceptionList.class},
235 new Object[] {null});
236 } catch (Exception e) {
237 final String msg = "changing properties failed";
238 Trace.fatal(CLASS, "visitEnter(Proposition)", msg, e);
239 QedeqLog.getInstance().logMessage(msg + " " + e.toString());
240 }
241 } else {
242 QedeqLog.getInstance().logMessage("proof not found for "
243 + super.getLocationDescription());
244 }
245 if (proof != null && !noSave) {
246 final File file = getServices().getLocalFilePath(
247 getQedeqBo().getModuleAddress());
248 try {
249 QedeqLog.getInstance().logMessage(
250 "Saving file \"" + file + "\"");
251 QedeqFileDao dao = getServices().getQedeqFileDao();
252 dao.saveQedeq(getQedeqBo(), file);
253 if (!getQedeqBo().getModuleAddress().isFileAddress()) {
254 QedeqLog.getInstance().logMessage("Only the the buffered file changed!");
255 }
256 } catch (Exception e) {
257 final String msg = "Saving file \"" + file + "\" failed";
258 Trace.fatal(CLASS, "visitEnter(Proposition)", msg, e);
259 QedeqLog.getInstance().logMessage(msg + " " + e.toString());
260 }
261 }
262 } else {
263 Trace.info(CLASS, method, "has already a proof: "
264 + super.getLocationDescription());
265 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
266 new AddVo(getNodeBo().getNodeVo().getId())));
267 }
268 setBlocked(true);
269 Trace.end(CLASS, this, method);
270 }
271
272 public void visitLeave(final Proposition definition) {
273 setBlocked(false);
274 }
275
276 public void visitEnter(final Rule rule) throws ModuleDataException {
277 if (rule == null) {
278 return;
279 }
280 setBlocked(true);
281 }
282
283 public void visitLeave(final Rule rule) {
284 setBlocked(false);
285 }
286
287 public String getLocationDescription() {
288 final String s = super.getLocationDescription();
289 if (finder == null) {
290 return s;
291 }
292 return s + " " + finder.getExecutionActionDescription();
293 }
294
295 }
|