From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 25 Mar 2022 19:19:35 +0000 (-0500)
Subject: Change output of abduction/interpolation for failed inputs (#8396)
X-Git-Tag: cvc5-1.0.0~172
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=219e2763d670e7bad8d6178fa4dd80b5bf1f6ea8;p=cvc5.git

Change output of abduction/interpolation for failed inputs (#8396)

Changes from "none" to "fail" to be consistent with SyGuS standard. Note that this means that we don't know if an abduct/interpolant exists.
---

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 4222ef4a6..04dbc77bb 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1953,7 +1953,7 @@ void GetInterpolCommand::printResult(std::ostream& out) const
     }
     else
     {
-      out << "none" << std::endl;
+      out << "fail" << std::endl;
     }
   }
 }
@@ -2020,7 +2020,7 @@ void GetInterpolNextCommand::printResult(std::ostream& out) const
     }
     else
     {
-      out << "none" << std::endl;
+      out << "fail" << std::endl;
     }
   }
 }
@@ -2110,7 +2110,7 @@ void GetAbductCommand::printResult(std::ostream& out) const
     }
     else
     {
-      out << "none" << std::endl;
+      out << "fail" << std::endl;
     }
   }
 }
@@ -2173,7 +2173,7 @@ void GetAbductNextCommand::printResult(std::ostream& out) const
     }
     else
     {
-      out << "none" << std::endl;
+      out << "fail" << std::endl;
     }
   }
 }
diff --git a/test/regress/cli/regress1/abduction/issue5848-3-trivial-no-abduct.smt2 b/test/regress/cli/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
index b64e27b45..bd2e379c7 100644
--- a/test/regress/cli/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
+++ b/test/regress/cli/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --produce-abducts
-; EXPECT: none
+; EXPECT: fail
 (set-logic ALL)
 (assert (= 0.0 (sqrt 1.0)))
 (get-abduct A false)
diff --git a/test/regress/cli/regress1/abduction/issue5848-4.smt2 b/test/regress/cli/regress1/abduction/issue5848-4.smt2
index 93cd8f52b..4bb4125a7 100644
--- a/test/regress/cli/regress1/abduction/issue5848-4.smt2
+++ b/test/regress/cli/regress1/abduction/issue5848-4.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --produce-abducts
-; EXPECT: none
+; EXPECT: fail
 (set-logic UFLRA)
 (declare-sort S0 0)
 (declare-fun S0-0 () S0)