Skip to content

Commit

Permalink
trying to retrieve the solver
Browse files Browse the repository at this point in the history
  • Loading branch information
VeraZhang0311 committed Jul 3, 2024
1 parent 57c9865 commit a0ff9d4
Showing 1 changed file with 39 additions and 4 deletions.
43 changes: 39 additions & 4 deletions Src/CommandLine/CommandInterface.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2138,16 +2138,51 @@ private void DoInteractiveHelp(string s)

private void DoFetchConstraints(string s)
{
var cmdParts = s.Split(cmdSplitChars, 3, StringSplitOptions.RemoveEmptyEntries);
if (cmdParts.Length < 2 || cmdParts.Length > 3)
// Split the command string to get task id and file index
var cmdParts = s.Split(cmdSplitChars, StringSplitOptions.RemoveEmptyEntries);
if (cmdParts.Length != 3)
{
sink.WriteMessageLine("Invalid command format. Expected format: 'ct <task_id> <file_index>'", SeverityKind.Warning);
return;
}
// Parse task id and file index
if (!int.TryParse(cmdParts[1], out int taskId))
{
sink.WriteMessageLine(FetchConstraintsMsg, SeverityKind.Warning);
sink.WriteMessageLine(string.Format("{0} is not a valid task id", cmdParts[1]), SeverityKind.Warning);
return;
}

sink.WriteMessageLine("Fetching constraints...");
// Retrieve the task
TaskKind kind;
System.Threading.Tasks.Task task;
if (!taskManager.TryGetTask(taskId, out task, out kind))
{
sink.WriteMessageLine(string.Format("{0} is not a valid task id", taskId), SeverityKind.Warning);
return;
}

// Ensure the task is completed
if (!task.IsCompleted)
{
sink.WriteMessageLine(string.Format("Task {0} is still running.", taskId), SeverityKind.Warning);
return;
}

// Fetch the Solver object from the task result
SolveResult result = ((System.Threading.Tasks.Task<SolveResult>)task).Result;
var solver = result.Solver;

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build (ubuntu-latest)

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build (ubuntu-latest)

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build (ubuntu-latest)

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build (ubuntu-latest)

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build (ubuntu-latest)

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build (ubuntu-latest)

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build-macos

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build-macos

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build-macos

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build-macos

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build-macos

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

Check failure on line 2173 in Src/CommandLine/CommandInterface.cs

View workflow job for this annotation

GitHub Actions / build-macos

'SolveResult' does not contain a definition for 'Solver' and no accessible extension method 'Solver' accepting a first argument of type 'SolveResult' could be found (are you missing a using directive or an assembly reference?)

// Fetch and print constraints in SMT-LIB2 format
using (var writer = new System.IO.StringWriter())
{
solver.ToSMT2(writer);
string smtLib2Format = writer.ToString();
sink.WriteMessageLine(smtLib2Format);
}

}


private void DoConfigHelp(string s)
{
sink.WriteMessageLine("Use collections to bind plugins to names.");
Expand Down

0 comments on commit a0ff9d4

Please sign in to comment.