From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 4 Jun 2020 16:31:55 +0000 (-0500)
Subject: Fix abduction with datatypes (#4566)
X-Git-Tag: cvc5-1.0.0~3259
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8c467723be3746ed711c609fa6dafb19a5a49e8b;p=cvc5.git

Fix abduction with datatypes (#4566)

Previously we were treating constructor/selector/tester symbols as arguments to the abduct-to-synthesize.
---

diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index a58c5d841..22b56eb6b 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -58,6 +58,12 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
   for (const Node& s : symset)
   {
     TypeNode tn = s.getType();
+    if (tn.isConstructor() || tn.isSelector() || tn.isTester())
+    {
+      // datatype symbols should be considered interpreted symbols here, not
+      // (higher-order) variables.
+      continue;
+    }
     // Notice that we allow for non-first class (e.g. function) variables here.
     // This is applicable to the case where we are doing get-abduct in a logic
     // with UF.
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 801f38b29..290fca6bc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1200,6 +1200,7 @@ set(regress_0_tests
 # Regression level 1 tests
 
 set(regress_1_tests
+  regress1/abduct-dt.smt2
   regress1/arith/arith-int-004.cvc
   regress1/arith/arith-int-011.cvc
   regress1/arith/arith-int-012.cvc
diff --git a/test/regress/regress1/abduct-dt.smt2 b/test/regress/regress1/abduct-dt.smt2
new file mode 100644
index 000000000..d72d15a21
--- /dev/null
+++ b/test/regress/regress1/abduct-dt.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))
+(declare-fun x () List)
+(assert (distinct x nil))
+(get-abduct A (= x (cons (head x) (tail x))))