mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
4df373ae99
Due to previous refactoring, the SMT solver called by the SyGuS solver no longer answers unsat when the synthesis problem has a valid solution. This PR makes it so that unsat from the underlying SMT solver is now interpreted as "infeasible" and is officially returned as such by the SyGuS solver. Note that we return unsat when e.g. a CEGIS refinement lemma is equivalent to false. On the other hand, we do not yet answer unsat when we run out of terms (e.g. for finite grammars), as this is still guarded. A followup PR will address this. To make the SMT solver answer unsat for infeasible conjectures, we do not guard CEGIS lemmas with the "feasible guard", instead we use the conjecture itself, similar to quantifier instantiation lemmas. This further removes the "feasible guard" from the internal sygus solver, which was used as a way to prevent unsat due to the infeasibility of CEGIS refinement lemmas.
77 lines
2.1 KiB
C++
77 lines
2.1 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Andrew Reynolds, Mathias Preiner, Aina Niemetz
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2022 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.
|
|
* ****************************************************************************
|
|
*
|
|
* Black box testing of the SynthResult class
|
|
*/
|
|
|
|
#include "test_api.h"
|
|
|
|
namespace cvc5::internal {
|
|
|
|
namespace test {
|
|
|
|
class TestApiBlackSynthResult : public TestApi
|
|
{
|
|
};
|
|
|
|
TEST_F(TestApiBlackSynthResult, isNull)
|
|
{
|
|
cvc5::SynthResult res_null;
|
|
ASSERT_TRUE(res_null.isNull());
|
|
ASSERT_FALSE(res_null.hasSolution());
|
|
ASSERT_FALSE(res_null.hasNoSolution());
|
|
ASSERT_FALSE(res_null.isUnknown());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSynthResult, hasSolution)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
|
|
Term boolTerm = d_solver.mkTrue();
|
|
d_solver.addSygusConstraint(boolTerm);
|
|
cvc5::SynthResult res = d_solver.checkSynth();
|
|
ASSERT_FALSE(res.isNull());
|
|
ASSERT_TRUE(res.hasSolution());
|
|
ASSERT_FALSE(res.hasNoSolution());
|
|
ASSERT_FALSE(res.isUnknown());
|
|
ASSERT_EQ(res.toString(), "(SOLUTION)");
|
|
{
|
|
std::stringstream ss;
|
|
ss << res;
|
|
ASSERT_EQ(res.toString(), ss.str());
|
|
}
|
|
}
|
|
|
|
TEST_F(TestApiBlackSynthResult, hasNoSolution)
|
|
{
|
|
// note that we never return synth result for which hasNoSolution is true
|
|
// currently
|
|
cvc5::SynthResult res_null;
|
|
ASSERT_FALSE(res_null.hasNoSolution());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSynthResult, isUnknown)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
|
|
Term boolTerm = d_solver.mkFalse();
|
|
d_solver.addSygusConstraint(boolTerm);
|
|
cvc5::SynthResult res = d_solver.checkSynth();
|
|
ASSERT_FALSE(res.isNull());
|
|
ASSERT_FALSE(res.hasSolution());
|
|
ASSERT_TRUE(res.hasNoSolution());
|
|
ASSERT_FALSE(res.isUnknown());
|
|
}
|
|
|
|
} // namespace test
|
|
} // namespace cvc5::internal
|