Skip to content

Commit

Permalink
Merge branch 'master' into highprecision
Browse files Browse the repository at this point in the history
  • Loading branch information
@nickbattle
nickbattle committed Nov 7, 2023
2 parents c7094ff + 4f5ebfe commit d8cf40e
Show file tree
Hide file tree
Showing 15 changed files with 193 additions and 94 deletions.
128 changes: 68 additions & 60 deletions examples/quickcheck/src/main/java/quickcheck/QuickCheck.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -214,36 +214,6 @@ public ProofObligationList getChosen()
return chosen;
}

public List<String> strategyNames(List<String> arglist)
{
List<String> names = new Vector<String>();
Iterator<String> iter = arglist.iterator();

while (iter.hasNext())
{
String arg = iter.next();

if (arg.equals("-s"))
{
iter.remove();

if (iter.hasNext())
{
arg = iter.next();
iter.remove();
names.add(arg);
}
else
{
errorln("-s must be followed by a strategy name");
names.add("unknown");
}
}
}

return names;
}

public ProofObligationList getPOs(ProofObligationList all, List<Integer> poList, List<String> poNames)
{
errorCount = 0;
Expand Down Expand Up @@ -333,9 +303,9 @@ public StrategyResults getValues(ProofObligation po)

INExpression exp = getINExpression(po);
List<INBindingSetter> binds = getINBindList(exp);
long before = System.currentTimeMillis();
IterableContext ictxt = addTypeParams(po, Interpreter.getInstance().getInitialContext());
boolean hasAllValues = false;
long before = System.currentTimeMillis();

while (ictxt.hasNext())
{
Expand All @@ -348,7 +318,8 @@ public StrategyResults getValues(ProofObligation po)

if (sresults.provedBy != null) // No need to go further
{
return new StrategyResults(sresults.provedBy, sresults.hasAllValues, cexamples, System.currentTimeMillis() - before);
sresults.setDuration(System.currentTimeMillis() - before);
return sresults;
}

for (String bind: cexamples.keySet())
Expand Down Expand Up @@ -378,7 +349,7 @@ public StrategyResults getValues(ProofObligation po)
}
}

return new StrategyResults(null, hasAllValues, union, System.currentTimeMillis() - before);
return new StrategyResults(union, hasAllValues, System.currentTimeMillis() - before);
}

public void checkObligation(ProofObligation po, StrategyResults results)
Expand All @@ -398,19 +369,18 @@ else if (results.provedBy != null)
{
po.setStatus(POStatus.PROVED);
po.setProvedBy(results.provedBy);
po.setMessage(results.message);
po.setWitness(results.witness);
po.setCounterexample(null);
po.setCounterMessage(null);
infof("PO #%d, PROVED by %s strategy %s\n", po.number, results.provedBy, duration(results.duration));
infof("PO #%d, PROVED by %s %s %s\n", po.number, results.provedBy, results.message, duration(results.duration));
return;
}

try
{
Map<String, ValueList> cexamples = results.counterexamples;

for (INBindingSetter mbind: bindings)
{
ValueList values = cexamples.get(mbind.toString());
ValueList values = results.counterexamples.get(mbind.toString());

if (values != null)
{
Expand All @@ -419,7 +389,7 @@ else if (results.provedBy != null)
}
else
{
errorln("PO #" + po.number + ": No range defined for " + mbind);
errorln("PO #" + po.number + ": No bind values defined for " + mbind);
errorCount++;
}
}
Expand All @@ -441,7 +411,7 @@ else if (results.provedBy != null)

IterableContext ictxt = addTypeParams(po, ctxt);
Value execResult = new BooleanValue(false);
ContextException exception = null;
ContextException execException = null;
boolean execCompleted = false;
long before = System.currentTimeMillis();

Expand Down Expand Up @@ -477,7 +447,7 @@ else if (e.number == 4024) // 'not yet specified' expression reached
else
{
execResult = new BooleanValue(false);
exception = e;
execException = e;
}
}
finally
Expand Down Expand Up @@ -511,6 +481,8 @@ else if (execResult instanceof BooleanValue)
{
POStatus outcome = null;
String message = "";
po.setWitness(null);
po.setProvedBy(null);

if (didTimeout)
{
Expand All @@ -519,10 +491,14 @@ else if (execResult instanceof BooleanValue)
else if (po.isExistential())
{
outcome = POStatus.PROVED; // An "exists" PO is PROVED, if true.
Context path = getWitness(bindings);
String w = stringOfContext(path);
po.setWitness(w);
if (w != null) message = " witness " + w;
String witness = stringOfContext(findWitness(bindings));
po.setWitness(witness);

if (witness != null)
{
message = " by witness " + witness;
po.setProvedBy("witness");
}
}
else if (results.hasAllValues && execCompleted)
{
Expand All @@ -538,7 +514,7 @@ else if (results.hasAllValues && execCompleted)
infof("PO #%d, %s%s %s\n", po.number, outcome.toString().toUpperCase(), message, duration(before, after));
po.setStatus(outcome);
po.setCounterexample(null);
po.setCounterMessage(null);
po.setMessage(null);
}
else
{
Expand All @@ -547,31 +523,34 @@ else if (results.hasAllValues && execCompleted)
infof("PO #%d, TIMEOUT %s\n", po.number, duration(before, after));
po.setStatus(POStatus.TIMEOUT);
po.setCounterexample(null);
po.setCounterMessage(null);
po.setMessage(null);
po.setWitness(null);
}
else if (po.isExistential()) // Principal exp is "exists..."
{
infof("PO #%d, MAYBE %s\n", po.number, duration(before, after));
po.setStatus(POStatus.MAYBE);
po.setCounterexample(null);
po.setCounterMessage(null);
po.setMessage(null);
po.setWitness(null);
}
else
{
infof("PO #%d, FAILED %s: ", po.number, duration(before, after));
po.setStatus(POStatus.FAILED);
printCounterexample(bindings);
po.setCounterexample(getCounterexample(bindings));
po.setCounterexample(findCounterexample(bindings));
po.setWitness(null);

if (exception != null)
if (execException != null)
{
String msg = "Causes " + exception.getMessage();
String msg = "Causes " + execException.getMessage();
infoln(msg);
po.setCounterMessage(msg);
po.setMessage(msg);
}
else
{
po.setCounterMessage(null);
po.setMessage(null);
}

infoln("----");
Expand All @@ -585,7 +564,7 @@ else if (po.isExistential()) // Principal exp is "exists..."
infoln(msg);
po.setStatus(POStatus.FAILED);
po.setCounterexample(null);
po.setCounterMessage(msg);
po.setMessage(msg);
infoln("----");
printBindings(bindings);
infoln("----");
Expand All @@ -599,7 +578,7 @@ else if (po.isExistential()) // Principal exp is "exists..."
infoln(msg);
po.setStatus(POStatus.FAILED);
po.setCounterexample(null);
po.setCounterMessage(msg);
po.setMessage(msg);
infoln("----");
printBindings(bindings);
infoln("----");
Expand All @@ -610,8 +589,7 @@ else if (po.isExistential()) // Principal exp is "exists..."
{
for (INBindingSetter mbind: bindings)
{
mbind.setBindValues(null, 0);
mbind.setCounterexample(null, false);
mbind.setBindValues(null, 0); // Clears everything
}
}
}
Expand All @@ -622,6 +600,36 @@ else if (po.isExistential()) // Principal exp is "exists..."
}
}

private List<String> strategyNames(List<String> arglist)
{
List<String> names = new Vector<String>();
Iterator<String> iter = arglist.iterator();

while (iter.hasNext())
{
String arg = iter.next();

if (arg.equals("-s"))
{
iter.remove();

if (iter.hasNext())
{
arg = iter.next();
iter.remove();
names.add(arg);
}
else
{
errorln("-s must be followed by a strategy name");
names.add("unknown");
}
}
}

return names;
}

private IterableContext addTypeParams(ProofObligation po, Context ctxt)
{
IterableContext ictxt = new IterableContext(po.location, "Type params", ctxt);
Expand Down Expand Up @@ -694,7 +702,7 @@ private void printBindings(List<INBindingSetter> bindings)
}
}

private Context getCounterexample(List<INBindingSetter> bindings)
private Context findCounterexample(List<INBindingSetter> bindings)
{
Context ctxt = null;

Expand All @@ -711,7 +719,7 @@ private Context getCounterexample(List<INBindingSetter> bindings)
return ctxt;
}

private Context getWitness(List<INBindingSetter> bindings)
private Context findWitness(List<INBindingSetter> bindings)
{
Context ctxt = null;

Expand All @@ -730,7 +738,7 @@ private Context getWitness(List<INBindingSetter> bindings)

private void printCounterexample(List<INBindingSetter> bindings)
{
Context path = getCounterexample(bindings);
Context path = findCounterexample(bindings);
String cex = stringOfContext(path);

if (cex == null)
Expand Down
2 changes: 1 addition & 1 deletion examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ public StrategyResults getValues(ProofObligation po, INExpression exp, List<INBi
// The current bind may be finite, but others may not be.
boolean hasAll = (po.typeParams == null);

return new StrategyResults(null, hasAll, result, System.currentTimeMillis() - before);
return new StrategyResults(result, hasAll, System.currentTimeMillis() - before);
}

@Override
Expand Down
2 changes: 1 addition & 1 deletion examples/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -542,7 +542,7 @@ public StrategyResults getValues(ProofObligation po, INExpression exp, List<INBi
println(e);
}

return new StrategyResults(null, false, values, System.currentTimeMillis() - before);
return new StrategyResults(values, false, System.currentTimeMillis() - before);
}

@Override
Expand Down
2 changes: 1 addition & 1 deletion examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ public StrategyResults getValues(ProofObligation po, INExpression exp, List<INBi
}
}

return new StrategyResults(null, false, result, System.currentTimeMillis() - before);
return new StrategyResults(result, false, System.currentTimeMillis() - before);
}

@Override
Expand Down
2 changes: 1 addition & 1 deletion examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,7 @@ public StrategyResults getValues(ProofObligation po, INExpression exp, List<INBi
}
}

return new StrategyResults(null, false, result, System.currentTimeMillis() - before);
return new StrategyResults(result, false, System.currentTimeMillis() - before);
}

@Override
Expand Down
40 changes: 33 additions & 7 deletions examples/quickcheck/src/main/java/quickcheck/strategies/StrategyResults.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,24 +39,50 @@
*/
public class StrategyResults
{
public final String provedBy; // If set, proved already
public final boolean hasAllValues; // Contains all possible values from all binds
public final String provedBy; // If set, proved by the strategy
public final String message; // Any message along with the result
public final String witness; // Any witness found

public final Map<String, ValueList> counterexamples;
public final long duration; // time to generate counterexamples, in millisecs
public final boolean hasAllValues; // Contains all possible values from all binds

public long duration; // time to generate counterexamples, in millisecs

public StrategyResults()
{
this.provedBy = null;
this.hasAllValues = false;
this.message = null;
this.witness = null;

this.counterexamples = new HashMap<String, ValueList>();
this.hasAllValues = false;
this.duration = 0;
}

public StrategyResults(String proved, boolean hasAllValues, Map<String, ValueList> counterexamples, long duration)
public StrategyResults(Map<String, ValueList> counterexamples, boolean hasAllValues, long duration)
{
this.provedBy = proved;
this.hasAllValues = hasAllValues;
this.provedBy = null;
this.message = null;
this.witness = null;

this.counterexamples = counterexamples;
this.hasAllValues = hasAllValues;
this.duration = duration;
}

public StrategyResults(String provedBy, String message, String witness, long duration)
{
this.provedBy = provedBy;
this.message = message;
this.witness = witness;

this.counterexamples = new HashMap<String, ValueList>();
this.hasAllValues = false;
this.duration = duration;
}

public void setDuration(Long duration)
{
this.duration = duration;
}
}
Loading

0 comments on commit d8cf40e

Please sign in to comment.