Skip to content

Commit

Permalink
Added some verbose calls
Browse files Browse the repository at this point in the history
  • Loading branch information
nickbattle committed Dec 9, 2023
1 parent 1afd378 commit 66b118c
Showing 1 changed file with 20 additions and 8 deletions.
28 changes: 20 additions & 8 deletions quickcheck/src/main/java/quickcheck/QuickCheck.java
Original file line number Diff line number Diff line change
Expand Up @@ -314,24 +314,36 @@ public StrategyResults getValues(ProofObligation po)

for (QCStrategy strategy: strategies)
{
verbose("Invoking %s strategy\n", strategy.getName());
StrategyResults sresults = strategy.getValues(po, exp, binds, ictxt);
Map<String, ValueList> cexamples = sresults.counterexamples;

if (sresults.provedBy != null) // No need to go further
{
verbose("Obligation proved by %s\n", strategy.getName());
sresults.setDuration(System.currentTimeMillis() - before);
return sresults;
}

for (String bind: cexamples.keySet())
if (cexamples.isEmpty())
{
if (union.containsKey(bind))
{
union.get(bind).addAll(cexamples.get(bind));
}
else
verbose("No bindings returned by %s\n", strategy.getName());
}
else
{
for (String bind: cexamples.keySet())
{
union.put(bind, cexamples.get(bind));
ValueList values = cexamples.get(bind);
verbose("%s returned %d values for %s\n", strategy.getName(), values.size(), bind);

if (union.containsKey(bind))
{
union.get(bind).addAll(values);
}
else
{
union.put(bind, values);
}
}
}

Expand Down Expand Up @@ -419,7 +431,7 @@ else if (results.provedBy != null)

try
{
verbose("PO #%d, starting...\n", po.number);
verbose("PO #%d, starting evaluation...\n", po.number);

// Suspend annotation execution by the interpreter, because the
// expressions and statements in the PO can invoke them.
Expand Down

0 comments on commit 66b118c

Please sign in to comment.