| 1 | /* This file is part of the project "Hilbert II" - http://www.qedeq.org |
| 2 | * |
| 3 | * Copyright 2000-2014, 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 | |
| 16 | package org.qedeq.kernel.bo.service.logic; |
| 17 | |
| 18 | import java.io.File; |
| 19 | |
| 20 | import org.qedeq.base.io.Parameters; |
| 21 | import org.qedeq.base.trace.Trace; |
| 22 | import org.qedeq.base.utility.YodaUtility; |
| 23 | import org.qedeq.kernel.bo.log.ModuleLogListener; |
| 24 | import org.qedeq.kernel.bo.log.QedeqLog; |
| 25 | import org.qedeq.kernel.bo.logic.ProofFinderFactoryImpl; |
| 26 | import org.qedeq.kernel.bo.logic.proof.common.ProofFinder; |
| 27 | import org.qedeq.kernel.bo.logic.proof.common.ProofFinderFactory; |
| 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.InternalModuleServiceCall; |
| 31 | import org.qedeq.kernel.bo.module.KernelQedeqBo; |
| 32 | import org.qedeq.kernel.bo.module.QedeqFileDao; |
| 33 | import org.qedeq.kernel.bo.service.basis.ControlVisitor; |
| 34 | import org.qedeq.kernel.bo.service.basis.ModuleServicePluginExecutor; |
| 35 | import org.qedeq.kernel.se.base.module.Axiom; |
| 36 | import org.qedeq.kernel.se.base.module.FormalProofLineList; |
| 37 | import org.qedeq.kernel.se.base.module.FunctionDefinition; |
| 38 | import org.qedeq.kernel.se.base.module.InitialFunctionDefinition; |
| 39 | import org.qedeq.kernel.se.base.module.InitialPredicateDefinition; |
| 40 | import org.qedeq.kernel.se.base.module.PredicateDefinition; |
| 41 | import org.qedeq.kernel.se.base.module.Proposition; |
| 42 | import org.qedeq.kernel.se.base.module.Rule; |
| 43 | import org.qedeq.kernel.se.common.ModuleDataException; |
| 44 | import org.qedeq.kernel.se.common.ModuleService; |
| 45 | import org.qedeq.kernel.se.common.SourceFileExceptionList; |
| 46 | import org.qedeq.kernel.se.dto.module.AddVo; |
| 47 | import org.qedeq.kernel.se.dto.module.FormalProofLineListVo; |
| 48 | import org.qedeq.kernel.se.dto.module.FormalProofLineVo; |
| 49 | import org.qedeq.kernel.se.dto.module.FormalProofVo; |
| 50 | import org.qedeq.kernel.se.dto.module.FormulaVo; |
| 51 | import org.qedeq.kernel.se.dto.module.PropositionVo; |
| 52 | import org.qedeq.kernel.se.state.WellFormedState; |
| 53 | import org.qedeq.kernel.se.visitor.InterruptException; |
| 54 | |
| 55 | |
| 56 | /** |
| 57 | * Finds simple formal proofs. |
| 58 | * |
| 59 | * @author Michael Meyling |
| 60 | */ |
| 61 | public final class SimpleProofFinderExecutor extends ControlVisitor implements ModuleServicePluginExecutor { |
| 62 | |
| 63 | /** This class. */ |
| 64 | private static final Class CLASS = SimpleProofFinderExecutor.class; |
| 65 | |
| 66 | /** Factory for generating new checkers. */ |
| 67 | private ProofFinderFactory finderFactory = null; |
| 68 | |
| 69 | /** List of axioms, definitions and propositions. */ |
| 70 | private FormalProofLineListVo validFormulas; |
| 71 | |
| 72 | /** Save changed modules directly? */ |
| 73 | private boolean noSave; |
| 74 | |
| 75 | /** Currently running proof finder. */ |
| 76 | private ProofFinder finder; |
| 77 | |
| 78 | /** All parameters for this search. */ |
| 79 | private Parameters parameters; |
| 80 | |
| 81 | /** |
| 82 | * Constructor. |
| 83 | * |
| 84 | * @param plugin This plugin we work for. |
| 85 | * @param qedeq QEDEQ BO object. |
| 86 | * @param parameters Parameters. |
| 87 | */ |
| 88 | SimpleProofFinderExecutor(final ModuleService plugin, final KernelQedeqBo qedeq, |
| 89 | final Parameters parameters) { |
| 90 | super(plugin, qedeq); |
| 91 | final String method = "SimpleProofFinderExecutor(Plugin, KernelQedeqBo, Map)"; |
| 92 | final String finderFactoryClass = parameters.getString("checkerFactory"); |
| 93 | if (finderFactoryClass != null && finderFactoryClass.length() > 0) { |
| 94 | try { |
| 95 | Class cl = Class.forName(finderFactoryClass); |
| 96 | finderFactory = (ProofFinderFactory) cl.newInstance(); |
| 97 | } catch (ClassNotFoundException e) { |
| 98 | Trace.fatal(CLASS, this, method, "ProofFinderFactory class not in class path: " |
| 99 | + finderFactoryClass, e); |
| 100 | } catch (InstantiationException e) { |
| 101 | Trace.fatal(CLASS, this, method, "ProofFinderFactory class could not be instanciated: " |
| 102 | + finderFactoryClass, e); |
| 103 | } catch (IllegalAccessException e) { |
| 104 | Trace.fatal(CLASS, this, method, |
| 105 | "Programming error, access for instantiation failed for model: " |
| 106 | + finderFactoryClass, e); |
| 107 | } catch (RuntimeException e) { |
| 108 | Trace.fatal(CLASS, this, method, |
| 109 | "Programming error, instantiation failed for model: " + finderFactoryClass, e); |
| 110 | } |
| 111 | } |
| 112 | // fallback is the default finder factory |
| 113 | if (finderFactory == null) { |
| 114 | finderFactory = new ProofFinderFactoryImpl(); |
| 115 | } |
| 116 | noSave = parameters.getBoolean("noSave"); |
| 117 | this.parameters = parameters; |
| 118 | } |
| 119 | |
| 120 | private ModuleService getPlugin() { |
| 121 | return (ModuleService) getService(); |
| 122 | } |
| 123 | |
| 124 | public Object executePlugin(final InternalModuleServiceCall call, final Object data) throws InterruptException { |
| 125 | getServices().checkWellFormedness(call.getInternalServiceProcess(), getKernelQedeqBo()); |
| 126 | QedeqLog.getInstance().logRequest("Trying to create formal proofs", getKernelQedeqBo().getUrl()); |
| 127 | try { |
| 128 | validFormulas = new FormalProofLineListVo(); |
| 129 | traverse(call.getInternalServiceProcess()); |
| 130 | QedeqLog.getInstance().logSuccessfulReply( |
| 131 | "Proof creation finished for", getKernelQedeqBo().getUrl()); |
| 132 | } catch (SourceFileExceptionList e) { |
| 133 | final String msg = "Proof creation not (fully?) successful"; |
| 134 | QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(), e.getMessage()); |
| 135 | return Boolean.FALSE; |
| 136 | } finally { |
| 137 | getKernelQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList()); |
| 138 | } |
| 139 | return Boolean.TRUE; |
| 140 | } |
| 141 | |
| 142 | public void visitEnter(final Axiom axiom) throws ModuleDataException { |
| 143 | if (axiom == null) { |
| 144 | return; |
| 145 | } |
| 146 | validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()), |
| 147 | new AddVo(getNodeBo().getNodeVo().getId()))); |
| 148 | setBlocked(true); |
| 149 | } |
| 150 | |
| 151 | public void visitLeave(final Axiom axiom) { |
| 152 | setBlocked(false); |
| 153 | } |
| 154 | |
| 155 | public void visitEnter(final PredicateDefinition definition) |
| 156 | throws ModuleDataException { |
| 157 | if (definition == null) { |
| 158 | return; |
| 159 | } |
| 160 | validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()), |
| 161 | new AddVo(getNodeBo().getNodeVo().getId()))); |
| 162 | setBlocked(true); |
| 163 | } |
| 164 | |
| 165 | public void visitLeave(final PredicateDefinition definition) { |
| 166 | setBlocked(false); |
| 167 | } |
| 168 | |
| 169 | public void visitEnter(final InitialPredicateDefinition definition) |
| 170 | throws ModuleDataException { |
| 171 | setBlocked(true); |
| 172 | } |
| 173 | |
| 174 | public void visitLeave(final InitialPredicateDefinition definition) { |
| 175 | setBlocked(false); |
| 176 | } |
| 177 | |
| 178 | public void visitEnter(final InitialFunctionDefinition definition) |
| 179 | throws ModuleDataException { |
| 180 | setBlocked(true); |
| 181 | } |
| 182 | |
| 183 | public void visitLeave(final InitialFunctionDefinition definition) { |
| 184 | setBlocked(false); |
| 185 | } |
| 186 | |
| 187 | public void visitEnter(final FunctionDefinition definition) |
| 188 | throws ModuleDataException { |
| 189 | if (definition == null) { |
| 190 | return; |
| 191 | } |
| 192 | validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()), |
| 193 | new AddVo(getNodeBo().getNodeVo().getId()))); |
| 194 | setBlocked(true); |
| 195 | } |
| 196 | |
| 197 | public void visitLeave(final FunctionDefinition definition) { |
| 198 | setBlocked(false); |
| 199 | } |
| 200 | |
| 201 | public void visitEnter(final Proposition proposition) |
| 202 | throws ModuleDataException { |
| 203 | final String method = "visitEnter(Proposition)"; |
| 204 | Trace.begin(CLASS, this, method); |
| 205 | if (proposition == null) { |
| 206 | Trace.end(CLASS, this, method); |
| 207 | return; |
| 208 | } |
| 209 | if (proposition.getFormalProofList() == null) { |
| 210 | FormalProofLineList proof = null; |
| 211 | // we try finding a proof |
| 212 | try { |
| 213 | finder = finderFactory.createProofFinder(); |
| 214 | finder.findProof(proposition.getFormula().getElement(), validFormulas, |
| 215 | getCurrentContext(), parameters, new ModuleLogListener() { |
| 216 | public void logMessageState(final String text) { |
| 217 | QedeqLog.getInstance().logMessageState(text, getKernelQedeqBo().getUrl()); |
| 218 | } |
| 219 | }, getKernelQedeqBo().getElement2Utf8()); |
| 220 | } catch (ProofFoundException e) { |
| 221 | proof = e.getProofLines(); |
| 222 | } catch (ProofNotFoundException e) { |
| 223 | addWarning(e); |
| 224 | } finally { |
| 225 | finder = null; // so we always new if we are currently searching |
| 226 | } |
| 227 | if (proof != null) { |
| 228 | QedeqLog.getInstance().logMessage("proof found for " |
| 229 | + super.getLocationDescription()); |
| 230 | // TODO 20110323 m31: we do a dirty cast to modify the current module |
| 231 | Object state; |
| 232 | try { |
| 233 | state = YodaUtility.getFieldValue(getKernelQedeqBo(), "stateManager"); |
| 234 | YodaUtility.executeMethod(state, "setWellFormedState", new Class[] { |
| 235 | WellFormedState.class}, |
| 236 | new Object[] {WellFormedState.STATE_UNCHECKED}); |
| 237 | ((PropositionVo) proposition).addFormalProof(new FormalProofVo(proof)); |
| 238 | YodaUtility.executeMethod(state, "setErrors", new Class[] { |
| 239 | SourceFileExceptionList.class}, |
| 240 | new Object[] {null}); |
| 241 | } catch (Exception e) { |
| 242 | final String msg = "changing properties failed"; |
| 243 | Trace.fatal(CLASS, "visitEnter(Proposition)", msg, e); |
| 244 | QedeqLog.getInstance().logMessage(msg + " " + e.toString()); |
| 245 | } |
| 246 | } else { |
| 247 | QedeqLog.getInstance().logMessage("proof not found for " |
| 248 | + super.getLocationDescription()); |
| 249 | } |
| 250 | if (proof != null && !noSave) { |
| 251 | final File file = getServices().getLocalFilePath( |
| 252 | getKernelQedeqBo().getModuleAddress()); |
| 253 | try { |
| 254 | QedeqLog.getInstance().logMessage( |
| 255 | "Saving file \"" + file + "\""); |
| 256 | QedeqFileDao dao = getServices().getQedeqFileDao(); |
| 257 | dao.saveQedeq(getInternalServiceCall().getInternalServiceProcess(), getKernelQedeqBo(), file); |
| 258 | if (!getKernelQedeqBo().getModuleAddress().isFileAddress()) { |
| 259 | QedeqLog.getInstance().logMessage("Only the the buffered file changed!"); |
| 260 | } |
| 261 | } catch (Exception e) { |
| 262 | final String msg = "Saving file \"" + file + "\" failed"; |
| 263 | Trace.fatal(CLASS, "visitEnter(Proposition)", msg, e); |
| 264 | QedeqLog.getInstance().logMessage(msg + " " + e.toString()); |
| 265 | } |
| 266 | } |
| 267 | } else { |
| 268 | Trace.info(CLASS, method, "has already a proof: " |
| 269 | + super.getLocationDescription()); |
| 270 | validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()), |
| 271 | new AddVo(getNodeBo().getNodeVo().getId()))); |
| 272 | } |
| 273 | setBlocked(true); |
| 274 | Trace.end(CLASS, this, method); |
| 275 | } |
| 276 | |
| 277 | public void visitLeave(final Proposition definition) { |
| 278 | setBlocked(false); |
| 279 | } |
| 280 | |
| 281 | public void visitEnter(final Rule rule) throws ModuleDataException { |
| 282 | if (rule == null) { |
| 283 | return; |
| 284 | } |
| 285 | setBlocked(true); |
| 286 | } |
| 287 | |
| 288 | public void visitLeave(final Rule rule) { |
| 289 | setBlocked(false); |
| 290 | } |
| 291 | |
| 292 | public String getLocationDescription() { |
| 293 | final String s = super.getLocationDescription(); |
| 294 | if (finder == null) { |
| 295 | return s; |
| 296 | } |
| 297 | return s + " " + finder.getExecutionActionDescription(); |
| 298 | } |
| 299 | |
| 300 | } |