Merge branch 'master' into highprecision

# Conflicts:
#	quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java

quickcheck/src/main/java/quickcheck/QuickCheck.java

@@ -29,6 +29,7 @@
 import static quickcheck.commands.QCConsole.infof;
 import static quickcheck.commands.QCConsole.infoln;
 import static quickcheck.commands.QCConsole.verbose;
+import static quickcheck.commands.QCConsole.verboseln;
 
 import java.lang.reflect.Constructor;
 import java.util.HashMap;
@@ -181,6 +182,8 @@ public boolean initStrategies(long timeoutSecs)
 
 		for (QCStrategy strategy: strategies)
 		{
+			verbose("------------------------ Initializing %s strategy\n", strategy.getName());
+
 			doChecks = doChecks && strategy.init(this);
 
 			if (strategy.hasErrors())
@@ -193,6 +196,7 @@ public boolean initStrategies(long timeoutSecs)
 			}
 		}
 
+		verbose("------------------------ Initialized\n");
 		return doChecks;
 	}
 
@@ -321,12 +325,12 @@ public StrategyResults getValues(ProofObligation po)
 
 			for (QCStrategy strategy: strategies)
 			{
-				verbose("Invoking %s strategy\n", strategy.getName());
+				verbose("------------------------ Invoking %s strategy on PO #%d\n", strategy.getName(), po.number);
 				StrategyResults sresults = strategy.getValues(po, binds, ictxt);
 
 				if (sresults.provedBy != null || sresults.disprovedBy != null)	// No need to go further
 				{
-					verbose("Obligation (dis)proved by %s\n", strategy.getName());
+					verbose("Obligation resolved by %s\n", strategy.getName());
 					sresults.setDuration(System.currentTimeMillis() - before);
 					sresults.setBinds(binds);
 					sresults.setInExpression(poexp);
@@ -359,6 +363,8 @@ public StrategyResults getValues(ProofObligation po)
 
 				hasAllValues = hasAllValues || sresults.hasAllValues;	// At least one has all values
 			}
+
+			verboseln("-------------------------");
 		}
 
 		for (INBindingOverride bind: binds)
@@ -383,6 +389,8 @@ public StrategyResults getValues(ProofObligation po)
 
 	public void checkObligation(ProofObligation po, StrategyResults sresults)
 	{
+		verbose("------------------------ Checking PO #%d\n", po.number);
+
 		try
 		{
 			resetErrors();		// Only flag fatal errors

quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java

@@ -25,7 +25,8 @@
 package quickcheck.strategies;
 
 import static com.fujitsu.vdmj.plugins.PluginConsole.println;
-import static com.fujitsu.vdmj.plugins.PluginConsole.verboseln;
+import static quickcheck.commands.QCConsole.verbose;
+import static quickcheck.commands.QCConsole.verboseln;
 
 import java.math.BigInteger;
 import java.util.HashSet;
@@ -128,10 +129,9 @@ private StrategyResults directCasesObligation(CasesExhaustiveObligation po)
 		try
 		{
 			long before = System.currentTimeMillis();
-			Context ctxt = Interpreter.getInstance().getInitialContext();
-
-			LexLocation loc = po.exp.location;
 			Interpreter in = Interpreter.getInstance();
+			Context ctxt = in.getInitialContext();
+			LexLocation loc = po.exp.location;
 			INExpressionList list = in.findExpressions(loc.file, loc.startLine);
 			INCasesExpression cases = null;
 
@@ -152,6 +152,8 @@ private StrategyResults directCasesObligation(CasesExhaustiveObligation po)
 				ValueList values = po.exp.expType.apply(new INGetAllValuesVisitor(), ctxt);
 				long timeout = INBindingGlobals.getInstance().getTimeout();
 
+				verbose("Checking %d values of type %s\n", values.size(), po.exp.expType);
+
 				for (Value value: values)
 				{
 					boolean matched = false;
@@ -172,6 +174,8 @@ private StrategyResults directCasesObligation(CasesExhaustiveObligation po)
 
 					if (!matched)
 					{
+						verbose("Value %s does not match any case patterns\n", value);
+
 						TCNameToken name = new TCNameToken(po.location, po.location.module, po.exp.exp.toString());
 						Context cex = new Context(po.location, "Counterexample", Interpreter.getInstance().getInitialContext());
 						cex.put(name, value);
@@ -232,24 +236,32 @@ private StrategyResults directTotalObligation(TotalFunctionObligation po)
 
 		if (exdef.bodyObligationCount > 0)
 		{
-			return new StrategyResults();	// Body can fail in principle, so not definitely total
+			verboseln("Function body raises some proof obligations, so not total");
+			return new StrategyResults();
 		}
+
+		verboseln("Function body does not raise any obligations");
 
 		if (exdef.isUndefined ||
 			!TypeComparator.isSubType(exdef.actualResult, exdef.expectedResult))
 		{
-			return new StrategyResults();	// Body may not be the right type, so not definitely total
+			verboseln("But function body type is not a subtype of the return type, so not total");
+			return new StrategyResults();
 		}
 
+		verboseln("Function body type always matches the return type");
+
 		long before = System.currentTimeMillis();
 		exdef.body.apply(visitor, null);
 
 		if (visitor.isTotal())
 		{
+			verboseln("Function body has no partial operators");
 			return new StrategyResults(getName(), "(body is total)", null, System.currentTimeMillis() - before);
 		}
 		else
 		{
+			verboseln("But function body contains some partial operators");
 			return new StrategyResults();
 		}
 	}

quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java

@@ -24,6 +24,8 @@
 
 package quickcheck.visitors;
 
+import static quickcheck.commands.QCConsole.verbose;
+
 import java.util.List;
 import java.util.Stack;
 import java.util.Vector;
@@ -276,8 +278,14 @@ else if (node.left instanceof TCIntegerLiteralExpression &&
 	@Override
 	public Boolean caseExpression(TCExpression node, Stack<TCExpression> truths)
 	{
-		if (truths.contains(node))
+		int idx = truths.indexOf(node);
+
+		if (idx >= 0)
 		{
+			TCExpression original = truths.get(idx);
+			verbose("Expression %s defined at line %d\n", original, original.location.startLine);
+			verbose("Expression %s true at line %d\n", node, node.location.startLine);
+
 			evaluated.add(Utils.deBracketed(node));		// This truth was used
 			return true;
 		}