Fix: Dafny server API for counterexamples

Source/DafnyCore/CounterExampleGeneration/PartialState.cs

@@ -83,6 +83,42 @@ private Expression GetCompactConjunction(List<Expression> conjuncts) {
     return new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, left, right);
   }
 
+  public Dictionary<string, string> AsVariableValueDictionary() {
+    var variableToValue = new Dictionary<PartialValue, Expression>();
+    var variables = ExpandedVariableSet().ToArray();
+    var constraintSet = new HashSet<Constraint>();
+
+    foreach (var variable in variables) {
+      foreach (var constraint in variable.Constraints) {
+        constraintSet.Add(constraint);
+      }
+    }
+
+    Constraint.ResolveAndOrder(variableToValue, constraintSet.ToList(), true, true);
+
+    var variableValuesDictionary = new Dictionary<string, string>();
+    foreach (var variable in variables) {
+      var variableValue = variableToValue[variable].ToString();
+      foreach (var constraint in variable.Constraints.OfType<DefinitionConstraint>()
+                 .Where(constraint => constraint.DefinedValue == variable &&
+                 (constraint is not LiteralExprConstraint) &&
+                 (constraint is not DatatypeValueConstraint) &&
+                 (constraint is not SeqDisplayConstraint))) {
+        if (constraint.ReferencedValues.Any(value => !variableToValue.ContainsKey(value))) {
+          continue;
+        }
+        var variableNameAsExpression = constraint.RightHandSide(variableToValue);
+        var variableNameAsString = variableNameAsExpression.ToString();
+        if (variableValue == variableNameAsString) {
+          continue;
+        }
+        variableValuesDictionary[variableNameAsString] = variableValue + ",";
+      }
+    }
+
+    return variableValuesDictionary;
+  }
+
   /// <summary>
   /// Convert this counterexample state into an assumption that could be inserted in Dafny source code
   /// </summary>

Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs

@@ -4,12 +4,14 @@
 namespace Microsoft.Dafny.LanguageServer.Handlers.Custom {
   public class CounterExampleItem {
     public Position Position { get; }
+    public IDictionary<string, string> Variables { get; }
 
     public string Assumption { get; }
 
-    public CounterExampleItem(Position position, string assumption) {
+    public CounterExampleItem(Position position, IDictionary<string, string> variables, string assumption) {
       Position = position;
+      Variables = variables;
       Assumption = assumption;
     }
   }
-}
+}

Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs

@@ -109,7 +109,8 @@ private IEnumerable<CounterExampleItem> GetCounterExamples(DafnyModel model) {
       private CounterExampleItem GetCounterExample(PartialState state) {
         return new(
           new Position(state.GetLineId() - 1, state.GetCharId()),
-           state.AsAssumption().ToString()
+           state.AsVariableValueDictionary(),
+          state.AsAssumption().ToString()
          );
       }
     }

docs/dev/news/5847.fix

@@ -0,0 +1 @@
+Fixed a bug preventing counterexamples from being displayed in the IDE