From 27b472240649f4fc6a9a2819282711300b426ba6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Mar 2022 18:26:37 -0600 Subject: [PATCH] Always ensure literal when requiring phase via inference manager (#8292) Also to be safe, ensures we clear pending in quantifiers engine. Fixes cvc5/cvc5-projects#484. --- src/theory/quantifiers_engine.cpp | 1 + src/theory/theory_inference_manager.cpp | 3 ++- test/api/cpp/CMakeLists.txt | 1 + test/api/cpp/proj-issue484.cpp | 36 +++++++++++++++++++++++++ 4 files changed, 40 insertions(+), 1 deletion(-) create mode 100644 test/api/cpp/proj-issue484.cpp diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 124198883..dd510a861 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -507,6 +507,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ //output debug stats d_qim.getInstantiate()->debugPrintModel(); } + d_qim.clearPending(); } void QuantifiersEngine::notifyCombineTheories() { diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index b4add920a..97019d101 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -609,7 +609,8 @@ DecisionManager* TheoryInferenceManager::getDecisionManager() void TheoryInferenceManager::requirePhase(TNode n, bool pol) { - return d_out.requirePhase(n, pol); + Node en = d_theoryState.getValuation().ensureLiteral(n); + return d_out.requirePhase(en, pol); } void TheoryInferenceManager::spendResource(Resource r) diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt index e110ec075..c250a0598 100644 --- a/test/api/cpp/CMakeLists.txt +++ b/test/api/cpp/CMakeLists.txt @@ -60,3 +60,4 @@ cvc5_add_api_test(proj-issue377) cvc5_add_api_test(proj-issue395) cvc5_add_api_test(proj-issue399) cvc5_add_api_test(proj-issue445) +cvc5_add_api_test(proj-issue484) diff --git a/test/api/cpp/proj-issue484.cpp b/test/api/cpp/proj-issue484.cpp new file mode 100644 index 000000000..10db4c8d0 --- /dev/null +++ b/test/api/cpp/proj-issue484.cpp @@ -0,0 +1,36 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Test for project issue #445 + * + */ + +#include + +#include "api/cpp/cvc5.h" + +using namespace cvc5::api; + +int main(void) +{ + Solver slv; + Sort s1 = slv.getIntegerSort(); + Term t1 = slv.mkVar(s1, "_x0"); + Term t3 = slv.mkInteger("8072314426184292007005683562403"); + Term t7 = slv.mkTerm(Kind::ADD, {t1, t1, t1, t3}); + Term t8 = slv.mkTerm(slv.mkOp(Kind::DIVISIBLE, 2319436191), {t7}); + Term vl = slv.mkTerm(Kind::VARIABLE_LIST, {t1}); + Term t10 = slv.mkTerm(Kind::FORALL, {vl, t8}); + slv.checkSatAssuming({t10}); + slv.assertFormula({t10}); + slv.checkSat(); +} -- 2.30.2