From 0f32fff652b6bac70cc18fbaa49f922ca27c58e6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 1 Aug 2019 22:11:08 -0500 Subject: [PATCH] Enable sygus logic when produce-abducts is true (#3144) --- src/smt/smt_engine.cpp | 9 ++------- test/regress/CMakeLists.txt | 1 + test/regress/regress0/opt-abd-no-use.smt2 | 6 ++++++ 3 files changed, 9 insertions(+), 7 deletions(-) create mode 100644 test/regress/regress0/opt-abd-no-use.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 709df6c9f..df46fc924 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1260,13 +1260,8 @@ void SmtEngine::setDefaults() { // sygus inference may require datatypes if (!d_isInternalSubsolver) { - if (options::produceAbducts()) - { - // we may invoke a sygus conjecture, hence we need options related to - // sygus - is_sygus = true; - } - if (options::sygusInference() || options::sygusRewSynthInput()) + if (options::produceAbducts() || options::sygusInference() + || options::sygusRewSynthInput()) { // since we are trying to recast as sygus, we assume the input is sygus is_sygus = true; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1b1f87bfc..2c65c7e14 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -546,6 +546,7 @@ set(regress_0_tests regress0/nl/very-easy-sat.smt2 regress0/nl/very-simple-unsat.smt2 regress0/options/invalid_dump.smt2 + regress0/opt-abd-no-use.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 diff --git a/test/regress/regress0/opt-abd-no-use.smt2 b/test/regress/regress0/opt-abd-no-use.smt2 new file mode 100644 index 000000000..65f1f3ae5 --- /dev/null +++ b/test/regress/regress0/opt-abd-no-use.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_LIA) +(set-info :status sat) +(set-option :produce-abducts true) +(declare-fun x () Int) +(assert (> x 0)) +(check-sat) -- 2.30.2