modified get constraints to have declarations and assertions

VUISIS · Jul 8, 2024 · 6f9d2ee · 6f9d2ee
1 parent 109d16d
commit 6f9d2ee
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 12 deletions.
diff --git 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<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);
-            }
+            // // 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
@@ -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