From 6f9d2ee19abfbdb5682d7b64ef2d70a9b57ff290 Mon Sep 17 00:00:00 2001 From: VeraZhang0311 Date: Mon, 8 Jul 2024 11:34:23 -0500 Subject: [PATCH] modified get constraints to have declarations and assertions --- Src/CommandLine/CommandInterface.cs | 21 +++++++++++---------- Src/Core/API/Results/SolveResult.cs | 4 ++-- 2 files changed, 13 insertions(+), 12 deletions(-) diff --git a/Src/CommandLine/CommandInterface.cs b/Src/CommandLine/CommandInterface.cs index 9614311..8c5210b 100755 --- a/Src/CommandLine/CommandInterface.cs +++ b/Src/CommandLine/CommandInterface.cs @@ -2174,16 +2174,17 @@ private void DoFetchConstraints(string s) SolveResult result = ((System.Threading.Tasks.Task)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); - } + // // 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); + // } + sink.WriteMessageLine(assertions); } private void DoConfigHelp(string s) diff --git a/Src/Core/API/Results/SolveResult.cs b/Src/Core/API/Results/SolveResult.cs index 218d00e..aba7b18 100644 --- a/Src/Core/API/Results/SolveResult.cs +++ b/Src/Core/API/Results/SolveResult.cs @@ -31,8 +31,8 @@ public Env Env private set; } - public Z3.BoolExpr[] getConstraints(){ - return solver.Z3Solver.Assertions; + public string getConstraints(){ + return solver.Z3Solver.ToString(); } public DateTime StopTime