Skip to content
Snippets Groups Projects
Commit 514d278f authored by Sebastian Krings's avatar Sebastian Krings
Browse files

remove old code

parent 4eeb0eac
Branches
Tags
No related merge requests found
...@@ -109,8 +109,7 @@ public class DisproverReasoner implements IReasoner { ...@@ -109,8 +109,7 @@ public class DisproverReasoner implements IReasoner {
final ICounterExample counterExample, final IProverSequent sequent, final ICounterExample counterExample, final IProverSequent sequent,
final IReasonerInput input) { final IReasonerInput input) {
Predicate goal = sequent.goal();// makeNewGoal((CounterExample) Predicate goal = sequent.goal();
// counterExample,sequent);
IAntecedent ante = ProverFactory.makeAntecedent(goal); IAntecedent ante = ProverFactory.makeAntecedent(goal);
...@@ -129,41 +128,12 @@ public class DisproverReasoner implements IReasoner { ...@@ -129,41 +128,12 @@ public class DisproverReasoner implements IReasoner {
IConfidence.DISCHARGED_MAX, IConfidence.DISCHARGED_MAX,
"No Counter-Example found (ProB)", ante); "No Counter-Example found (ProB)", ante);
// Predicate ng = sequent.getFormulaFactory().makeAssociativePredicate(
// Formula.LAND,
// makeNewHyps((CounterExample) counterExample, sequent),
// new SourceLocation(0, 0));
return ProverFactory.makeProofRule(this, input, null, null, return ProverFactory.makeProofRule(this, input, null, null,
IConfidence.PENDING, IConfidence.PENDING,
"Counter-Example: " + counterExample.toString(), ante); "Counter-Example: " + counterExample.toString(), ante);
} }
// private Set<Predicate> makeNewHyps(final CounterExample counterExample,
// final IProverSequent sequent) {
// FormulaFactory ff = sequent.getFormulaFactory();
// SourceLocation noloc = new SourceLocation(0, 0);
// Set<Predicate> p = new HashSet<Predicate>();
// p.add(sequent.goal());
//
// Set<Entry<String, String>> entries = counterExample.state.entrySet();
// for (Entry<String, String> entry : entries) {
// String predstring = "( " + entry.getKey() + " = "
// + entry.getValue() + " )";
// String unicode = UnicodeTranslator.toUnicode(predstring);
// IParseResult parseResult = ff.parsePredicate(unicode,
// LanguageVersion.V1, null);
// if (!parseResult.getProblems().isEmpty()) {
// return Collections.emptySet();
// }
// p.add(parseResult.getParsedPredicate());
//
// }
//
// return p;
// }
@Override @Override
public IReasonerInput deserializeInput(final IReasonerInputReader reader) public IReasonerInput deserializeInput(final IReasonerInputReader reader)
throws SerializeException { throws SerializeException {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment