Skip to content

Commit

Permalink
try
Browse files Browse the repository at this point in the history
  • Loading branch information
VeraZhang0311 committed Jul 3, 2024
1 parent a0ff9d4 commit 2d33653
Show file tree
Hide file tree
Showing 2 changed files with 69 additions and 23 deletions.
88 changes: 65 additions & 23 deletions Src/CommandLine/CommandInterface.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2136,51 +2136,93 @@ private void DoInteractiveHelp(string s)
}
}

private void DoFetchConstraints(string s)
private void DoFetchConstraints(string s)
{
// Split the command string to get task id and file index
var cmdParts = s.Split(cmdSplitChars, StringSplitOptions.RemoveEmptyEntries);
if (cmdParts.Length != 3)
var cmdParts = s.Split(cmdSplitChars, 4, StringSplitOptions.RemoveEmptyEntries);
if (cmdParts.Length < 2 || cmdParts.Length > 5)
{
sink.WriteMessageLine(ExtractMsg, SeverityKind.Warning);
return;
}

int taskId;
int solNum = 0;
bool isAppExtract = cmdParts.Length % 2 == 0;
var modName = isAppExtract ? cmdParts[1].Trim() : cmdParts[2].Trim();

if (!int.TryParse(cmdParts[0], out taskId))
{
sink.WriteMessageLine(string.Format("{0} is not task id", cmdParts[0]), SeverityKind.Warning);
return;
}
else if (string.IsNullOrEmpty(modName))
{
sink.WriteMessageLine("Invalid command format. Expected format: 'ct <task_id> <file_index>'", SeverityKind.Warning);
sink.WriteMessageLine(ExtractMsg, SeverityKind.Warning);
return;
}
// Parse task id and file index
if (!int.TryParse(cmdParts[1], out int taskId))
else if (!isAppExtract && !int.TryParse(cmdParts[1], out solNum))
{
sink.WriteMessageLine(string.Format("{0} is not a valid task id", cmdParts[1]), SeverityKind.Warning);
sink.WriteMessageLine(string.Format("{0} is not solution number", cmdParts[1]), SeverityKind.Warning);
return;
}

// 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);
sink.WriteMessageLine(string.Format("{0} is not an task id", cmdParts[0]), SeverityKind.Warning);
return;
}

// Ensure the task is completed
if (!task.IsCompleted)
else if (isAppExtract && kind != TaskKind.Apply)
{
sink.WriteMessageLine(string.Format("Task {0} is still running.", taskId), SeverityKind.Warning);
sink.WriteMessageLine(string.Format("{0} is not an apply id", cmdParts[0]), SeverityKind.Warning);
return;
}
else if (!isAppExtract && kind != TaskKind.Solve)
{
sink.WriteMessageLine(string.Format("{0} is not an solve id", cmdParts[0]), SeverityKind.Warning);
return;
}
else if (!task.IsCompleted)
{
sink.WriteMessageLine(string.Format("Task {0} is still running.", cmdParts[0]), SeverityKind.Warning);
return;
}

// Fetch the Solver object from the task result
SolveResult result = ((System.Threading.Tasks.Task<SolveResult>)task).Result;
var solver = result.Solver;
System.Threading.Tasks.Task<AST<Program>> bldTask = null;
if (isAppExtract)
{
var result = ((System.Threading.Tasks.Task<ApplyResult>)task).Result;
bldTask = result.GetOutputModel(
modName,
new ProgramName(string.Format("{0}{1}.4ml", ProgramName.EnvironmentScheme, modName)),
modName);

// Fetch and print constraints in SMT-LIB2 format
using (var writer = new System.IO.StringWriter())
if (bldTask == null)
{
sink.WriteMessageLine(string.Format("There is no output named {0}.", modName), SeverityKind.Warning);
return;
}

bldTask.Wait();
}
else
{
solver.ToSMT2(writer);
string smtLib2Format = writer.ToString();
sink.WriteMessageLine(smtLib2Format);
SolveResult result = ((System.Threading.Tasks.Task<SolveResult>)task).Result;
var assertions = result.getConstraints();
// Fetch and print constraints in SMT-LIB2 format
using (var writer = new System.IO.StringWriter())
{
foreach (var assertion in assertions)
{
writer.WriteLine(assertion.ToString()); // Adjust this if there's a specific method to get SMT-LIB2 format
}
string smtLib2Format = writer.ToString();
sink.WriteMessageLine(smtLib2Format);
}
}
}

}


private void DoConfigHelp(string s)
Expand Down
4 changes: 4 additions & 0 deletions Src/Core/API/Results/SolveResult.cs
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,10 @@ public Env Env
private set;
}

public Z3.BoolExpr[] getConstraints(){
return solver.Z3Solver.Assertions;
}

public DateTime StopTime
{
get;
Expand Down

0 comments on commit 2d33653

Please sign in to comment.