deleted unused code

VUISIS · Jul 3, 2024 · 109d16d · 109d16d
1 parent 40a69bc
commit 109d16d
Showing 1 changed file with 13 additions and 52 deletions.
diff --git a/Src/CommandLine/CommandInterface.cs b/Src/CommandLine/CommandInterface.cs
@@ -9,6 +9,7 @@ namespace Microsoft.Formula.CommandLine
     using System.Linq;
     using System.Threading;
     using System.Threading.Tasks;
+
 
     using API;
     using API.Nodes;
@@ -2138,33 +2139,20 @@ private void DoInteractiveHelp(string s)
 
         private void DoFetchConstraints(string s)
         {
-            var cmdParts = s.Split(cmdSplitChars, 4, StringSplitOptions.RemoveEmptyEntries);
-            if (cmdParts.Length < 2 || cmdParts.Length > 5)
+            var cmdParts = s.Split(cmdSplitChars, 3, StringSplitOptions.RemoveEmptyEntries);
+            if (cmdParts.Length < 2 || cmdParts.Length > 3)
             {
                 sink.WriteMessageLine(FetchConstraintsMsg, 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(ExtractMsg, SeverityKind.Warning);
-                return;
-            }
-            else if (!isAppExtract && !int.TryParse(cmdParts[1], out solNum))
-            {
-                sink.WriteMessageLine(string.Format("{0} is not solution number", cmdParts[1]), SeverityKind.Warning);
-                return;
-            }
+
 
             TaskKind kind;
             System.Threading.Tasks.Task task;
@@ -2173,12 +2161,7 @@ private void DoFetchConstraints(string s)
                 sink.WriteMessageLine(string.Format("{0} is not an task id", cmdParts[0]), SeverityKind.Warning);
                 return;
             }
-            else if (isAppExtract && kind != TaskKind.Apply)
-            {
-                sink.WriteMessageLine(string.Format("{0} is not an apply id", cmdParts[0]), SeverityKind.Warning);
-                return;
-            }
-            else if (!isAppExtract && kind != TaskKind.Solve)
+            else if (kind != TaskKind.Solve)
             {
                 sink.WriteMessageLine(string.Format("{0} is not an solve id", cmdParts[0]), SeverityKind.Warning);
                 return;
@@ -2189,42 +2172,20 @@ private void DoFetchConstraints(string s)
                 return;
             }
 
-            System.Threading.Tasks.Task<AST<Program>> bldTask = null;
-            if (isAppExtract)
+            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())
             {
-                var result = ((System.Threading.Tasks.Task<ApplyResult>)task).Result;
-                bldTask = result.GetOutputModel(
-                    modName,
-                    new ProgramName(string.Format("{0}{1}.4ml", ProgramName.EnvironmentScheme, modName)),
-                    modName);
-
-                if (bldTask == null)
+                foreach (var assertion in assertions)
                 {
-                    sink.WriteMessageLine(string.Format("There is no output named {0}.", modName), SeverityKind.Warning);
-                    return;
-                }
-
-                bldTask.Wait();
-            }
-            else
-            {
-                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);
+                    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)
         {
             sink.WriteMessageLine("Use collections to bind plugins to names.");