From bf7bd719996501a52a1d757d5c268b5ddc03dd14 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Jun 2022 07:03:04 -0500 Subject: [PATCH] Make interpolation robust to conjectures with no shared variables (#8840) Fixes #8833. --- src/theory/quantifiers/sygus/sygus_interpol.cpp | 12 +++++++++--- test/regress/cli/CMakeLists.txt | 1 + .../regress0/issue8833-interpol-no-shared-var.smt2 | 5 +++++ 3 files changed, 15 insertions(+), 3 deletions(-) create mode 100644 test/regress/cli/regress0/issue8833-interpol-no-shared-var.smt2 diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 1894c889c..8ce073b93 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -90,7 +90,10 @@ void SygusInterpol::createVariables(bool needsShared) } } // make the sygus variable list - d_ibvlShared = nm->mkNode(kind::BOUND_VAR_LIST, d_vlvsShared); + if (!d_vlvsShared.empty()) + { + d_ibvlShared = nm->mkNode(kind::BOUND_VAR_LIST, d_vlvsShared); + } Trace("sygus-interpol-debug") << "...finish" << std::endl; } @@ -234,12 +237,15 @@ void SygusInterpol::mkSygusConjecture(Node itp, // set the sygus bound variable list Trace("sygus-interpol-debug") << "Set attributes..." << std::endl; - itp.setAttribute(SygusSynthFunVarListAttribute(), d_ibvlShared); + if (!d_ibvlShared.isNull()) + { + itp.setAttribute(SygusSynthFunVarListAttribute(), d_ibvlShared); + } Trace("sygus-interpol-debug") << "...finish" << std::endl; // Fa( x ) Trace("sygus-interpol-debug") << "Make conjecture body..." << std::endl; - Node Fa = axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms); + Node Fa = nm->mkAnd(axioms); // Fa( x ) => A( x ) Node firstImplication = nm->mkNode(kind::IMPLIES, Fa, itpApp); Trace("sygus-interpol-debug") diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 39d9d92bc..4ffe4421e 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -755,6 +755,7 @@ set(regress_0_tests regress0/issue6738.smt2 regress0/issue6741.smt2 regress0/issue8807-model-core-partial.smt2 + regress0/issue8833-interpol-no-shared-var.smt2 regress0/issue8834-model-core-nconst.smt2 regress0/ite_arith.smt2 regress0/ite_real_int_type.smtv1.smt2 diff --git a/test/regress/cli/regress0/issue8833-interpol-no-shared-var.smt2 b/test/regress/cli/regress0/issue8833-interpol-no-shared-var.smt2 new file mode 100644 index 000000000..758df0086 --- /dev/null +++ b/test/regress/cli/regress0/issue8833-interpol-no-shared-var.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --produce-interpolants -q +; EXPECT: fail +(set-logic ALL) +(declare-fun a () Int) +(get-interpolant A (> a 0)) -- 2.30.2