Commit c4a4bf4b authored by Alexander Weigl's avatar Alexander Weigl

first test for isDerivable

parent 4085d7a3
Pipeline #12138 failed with stage
in 1 minute and 31 seconds
......@@ -118,12 +118,12 @@ public class KeYMatcher implements MatcherApi<KeyData> {
* @param term
* @return null if the term is not derivable or the new state
*/
public GoalNode<KeyData> isDerivable(Proof proof, GoalNode<KeyData> kd, Term term) {
public static GoalNode<KeyData> isDerivable(Proof proof, GoalNode<KeyData> kd, Term term) {
Taclet cut = proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(CUT_TACLET_NAME);
TacletApp app = NoPosTacletApp.createNoPosTacletApp(cut);
SchemaVariable sv = (SchemaVariable) app.uninstantiatedVars().iterator().next();
TacletApp cutApp = app.addCheckedInstantiation(sv, term, proof.getServices(), true);
ImmutableList<Goal> goalList = kd.getData().getGoal().apply(app);
ImmutableList<Goal> goalList = kd.getData().getGoal().apply(cutApp);
if(goalList.size() !=2) {
throw new IllegalStateException("Cut created more than two sub goals!");
......
package edu.kit.formal.interpreter;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import org.junit.Assert;
import org.junit.Test;
import java.io.File;
/**
* Created by weigl on 15.07.2017.
*/
public class KeyMatcherDerivableTest {
@Test
public void derivable_test_1() throws Exception {
KeYProofFacade f = new KeYProofFacade();
f.loadKeyFile(new File("src/test/resources/edu/kit/formal/proofscriptparser/derivable_test_1.key"));
Proof proof = f.getProof();
Goal g = proof.getGoal(proof.root());
GoalNode<KeyData> gn = new GoalNode<>(null, new KeyData(g, f.getEnvironment(), proof));
Term termQ = new TermBuilder(f.getEnvironment().getServices().getTermFactory(),
f.getEnvironment().getServices()).parseTerm("q");
System.out.println(termQ);
GoalNode<KeyData> a = KeYMatcher.isDerivable(proof, gn, termQ);
System.out.println(proof);
Assert.assertNotNull(a);
Assert.assertEquals(1, proof.getSubtreeGoals(proof.root()).size());
}
}
\ No newline at end of file
\sorts {
s;
}
\predicates {
p;
q;
}
\problem {
!(p -> q) | !p
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment