Skip to content

Commit

Permalink
Be more persistent for unknown results in inductive process
Browse files Browse the repository at this point in the history
agacek committed Nov 6, 2014
1 parent 85fbb7e commit 61fb0ef
Showing 3 changed files with 25 additions and 8 deletions.
19 changes: 12 additions & 7 deletions jkind/src/jkind/processes/InductiveProcess.java
Original file line number Diff line number Diff line change
@@ -116,8 +116,8 @@ private void checkProperties(int k) {
while (!possiblyValid.isEmpty()) {
Result result = solver.query(getInductiveQuery(k, possiblyValid));

if (result instanceof SatResult) {
Model model = ((SatResult) result).getModel();
if (result instanceof SatResult || result instanceof UnknownResult) {
Model model = getModel(result);
Iterator<String> iterator = possiblyValid.iterator();
while (iterator.hasNext()) {
String p = iterator.next();
@@ -133,15 +133,20 @@ private void checkProperties(int k) {
addPropertiesAsInvariants(k, possiblyValid);
sendValid(possiblyValid, k);
return;
} else if (result instanceof UnknownResult) {
properties.removeAll(possiblyValid);
// We report nothing in hopes that the base process at least
// finds a counterexample
return;
}
}
}

private Model getModel(Result result) {
if (result instanceof SatResult) {
return ((SatResult) result).getModel();
} else if (result instanceof UnknownResult) {
return ((UnknownResult) result).getModel();
} else {
throw new IllegalArgumentException();
}
}

private void addPropertiesAsInvariants(int k, List<String> valid) {
List<Invariant> propertiesAsInvariants = new ArrayList<>();
for (String property : valid) {
9 changes: 9 additions & 0 deletions jkind/src/jkind/solvers/UnknownResult.java
Original file line number Diff line number Diff line change
@@ -1,5 +1,14 @@
package jkind.solvers;

public class UnknownResult extends Result {
final private Model model;

public UnknownResult(Model model) {
super();
this.model = model;
}

public Model getModel() {
return model;
}
}
5 changes: 4 additions & 1 deletion jkind/src/jkind/solvers/z3/Z3Solver.java
Original file line number Diff line number Diff line change
@@ -50,7 +50,10 @@ public Result query(Sexp sexp) {
} else if (isUnsat(status)) {
result = new UnsatResult();
} else {
result = new UnknownResult();
// Even for unknown we can get a partial model
send("(get-model)");
send("(echo \"" + DONE + "\")");
result = new UnknownResult(parseModel(readFromSolver()));
}

return result;

0 comments on commit 61fb0ef

Please sign in to comment.