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.log.ModuleLogListener;
024 import org.qedeq.kernel.bo.log.QedeqLog;
025 import org.qedeq.kernel.bo.logic.ProofFinderFactoryImpl;
026 import org.qedeq.kernel.bo.logic.proof.common.ProofFinder;
027 import org.qedeq.kernel.bo.logic.proof.common.ProofFinderFactory;
028 import org.qedeq.kernel.bo.logic.proof.common.ProofFoundException;
029 import org.qedeq.kernel.bo.logic.proof.common.ProofNotFoundException;
030 import org.qedeq.kernel.bo.module.ControlVisitor;
031 import org.qedeq.kernel.bo.module.InternalServiceProcess;
032 import org.qedeq.kernel.bo.module.KernelQedeqBo;
033 import org.qedeq.kernel.bo.module.PluginExecutor;
034 import org.qedeq.kernel.bo.module.QedeqFileDao;
035 import org.qedeq.kernel.se.base.module.Axiom;
036 import org.qedeq.kernel.se.base.module.FormalProofLineList;
037 import org.qedeq.kernel.se.base.module.FunctionDefinition;
038 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
039 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
040 import org.qedeq.kernel.se.base.module.PredicateDefinition;
041 import org.qedeq.kernel.se.base.module.Proposition;
042 import org.qedeq.kernel.se.base.module.Rule;
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 import org.qedeq.kernel.se.state.WellFormedState;
053
054
055 /**
056 * Finds simple formal proofs.
057 *
058 * @author Michael Meyling
059 */
060 public final class SimpleProofFinderExecutor extends ControlVisitor implements PluginExecutor {
061
062 /** This class. */
063 private static final Class CLASS = SimpleProofFinderExecutor.class;
064
065 /** Factory for generating new checkers. */
066 private ProofFinderFactory finderFactory = null;
067
068 /** List of axioms, definitions and propositions. */
069 private FormalProofLineListVo validFormulas;
070
071 /** Save changed modules directly? */
072 private boolean noSave;
073
074 /** Currently running proof finder. */
075 private ProofFinder finder;
076
077 /** All parameters for this search. */
078 private Parameters parameters;
079
080 /**
081 * Constructor.
082 *
083 * @param plugin This plugin we work for.
084 * @param qedeq QEDEQ BO object.
085 * @param parameters Parameters.
086 */
087 SimpleProofFinderExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
088 final Parameters parameters) {
089 super(plugin, qedeq);
090 final String method = "SimpleProofFinderExecutor(Plugin, KernelQedeqBo, Map)";
091 final String finderFactoryClass = parameters.getString("checkerFactory");
092 if (finderFactoryClass != null && finderFactoryClass.length() > 0) {
093 try {
094 Class cl = Class.forName(finderFactoryClass);
095 finderFactory = (ProofFinderFactory) cl.newInstance();
096 } catch (ClassNotFoundException e) {
097 Trace.fatal(CLASS, this, method, "ProofFinderFactory class not in class path: "
098 + finderFactoryClass, e);
099 } catch (InstantiationException e) {
100 Trace.fatal(CLASS, this, method, "ProofFinderFactory class could not be instanciated: "
101 + finderFactoryClass, e);
102 } catch (IllegalAccessException e) {
103 Trace.fatal(CLASS, this, method,
104 "Programming error, access for instantiation failed for model: "
105 + finderFactoryClass, e);
106 } catch (RuntimeException e) {
107 Trace.fatal(CLASS, this, method,
108 "Programming error, instantiation failed for model: " + finderFactoryClass, e);
109 }
110 }
111 // fallback is the default finder factory
112 if (finderFactory == null) {
113 finderFactory = new ProofFinderFactoryImpl();
114 }
115 noSave = parameters.getBoolean("noSave");
116 this.parameters = parameters;
117 }
118
119 public Object executePlugin(final InternalServiceProcess process, final Object data) {
120 getServices().checkWellFormedness(getQedeqBo(), process);
121 QedeqLog.getInstance().logRequest("Trying to create formal proofs", getQedeqBo().getUrl());
122 try {
123 validFormulas = new FormalProofLineListVo();
124 traverse(process);
125 QedeqLog.getInstance().logSuccessfulReply(
126 "Proof creation finished for", getQedeqBo().getUrl());
127 } catch (SourceFileExceptionList e) {
128 final String msg = "Proof creation not (fully?) successful";
129 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage());
130 return Boolean.FALSE;
131 } finally {
132 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
133 }
134 return Boolean.TRUE;
135 }
136
137 public void visitEnter(final Axiom axiom) throws ModuleDataException {
138 if (axiom == null) {
139 return;
140 }
141 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
142 new AddVo(getNodeBo().getNodeVo().getId())));
143 setBlocked(true);
144 }
145
146 public void visitLeave(final Axiom axiom) {
147 setBlocked(false);
148 }
149
150 public void visitEnter(final PredicateDefinition definition)
151 throws ModuleDataException {
152 if (definition == null) {
153 return;
154 }
155 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
156 new AddVo(getNodeBo().getNodeVo().getId())));
157 setBlocked(true);
158 }
159
160 public void visitLeave(final PredicateDefinition definition) {
161 setBlocked(false);
162 }
163
164 public void visitEnter(final InitialPredicateDefinition definition)
165 throws ModuleDataException {
166 setBlocked(true);
167 }
168
169 public void visitLeave(final InitialPredicateDefinition definition) {
170 setBlocked(false);
171 }
172
173 public void visitEnter(final InitialFunctionDefinition definition)
174 throws ModuleDataException {
175 setBlocked(true);
176 }
177
178 public void visitLeave(final InitialFunctionDefinition definition) {
179 setBlocked(false);
180 }
181
182 public void visitEnter(final FunctionDefinition definition)
183 throws ModuleDataException {
184 if (definition == null) {
185 return;
186 }
187 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
188 new AddVo(getNodeBo().getNodeVo().getId())));
189 setBlocked(true);
190 }
191
192 public void visitLeave(final FunctionDefinition definition) {
193 setBlocked(false);
194 }
195
196 public void visitEnter(final Proposition proposition)
197 throws ModuleDataException {
198 final String method = "visitEnter(Proposition)";
199 Trace.begin(CLASS, this, method);
200 if (proposition == null) {
201 Trace.end(CLASS, this, method);
202 return;
203 }
204 if (proposition.getFormalProofList() == null) {
205 FormalProofLineList proof = null;
206 // we try finding a proof
207 try {
208 finder = finderFactory.createProofFinder();
209 finder.findProof(proposition.getFormula().getElement(), validFormulas,
210 getCurrentContext(), parameters, new ModuleLogListener() {
211 public void logMessageState(final String text) {
212 QedeqLog.getInstance().logMessageState(text, getQedeqBo().getUrl());
213 }
214 }, getQedeqBo().getElement2Utf8());
215 } catch (ProofFoundException e) {
216 proof = e.getProofLines();
217 } catch (ProofNotFoundException e) {
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, "setWellFormedState", new Class[] {
230 WellFormedState.class},
231 new Object[] {WellFormedState.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(getServiceProcess(), 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 }
|