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.
61 lines
1.8 KiB
Python
61 lines
1.8 KiB
Python
###############################################################################
|
|
# Top contributors (to current version):
|
|
# Andrew Reynolds
|
|
#
|
|
# 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.
|
|
# #############################################################################
|
|
#
|
|
# Unit tests for synth result API.
|
|
#
|
|
# Obtained by translating test/unit/api/synth_result_black.cpp
|
|
##
|
|
|
|
import pytest
|
|
import cvc5
|
|
from cvc5 import SynthResult
|
|
|
|
|
|
@pytest.fixture
|
|
def solver():
|
|
return cvc5.Solver()
|
|
|
|
|
|
def test_is_null(solver):
|
|
res_null = SynthResult(solver)
|
|
assert res_null.isNull()
|
|
assert not res_null.hasSolution()
|
|
assert not res_null.hasNoSolution()
|
|
assert not res_null.isUnknown()
|
|
|
|
def test_has_solution(solver):
|
|
solver.setOption("sygus", "true")
|
|
f = solver.synthFun("f", [], solver.getBooleanSort())
|
|
boolTerm = solver.mkBoolean(True)
|
|
solver.addSygusConstraint(boolTerm)
|
|
res = solver.checkSynth()
|
|
assert not res.isNull()
|
|
assert res.hasSolution()
|
|
assert not res.hasNoSolution()
|
|
assert not res.isUnknown()
|
|
assert str(res) == '(SOLUTION)'
|
|
|
|
def test_has_no_solution(solver):
|
|
res_null = SynthResult(solver)
|
|
assert not res_null.hasNoSolution()
|
|
|
|
def test_has_is_unknown(solver):
|
|
solver.setOption("sygus", "true")
|
|
f = solver.synthFun("f", [], solver.getBooleanSort())
|
|
boolTerm = solver.mkBoolean(False)
|
|
solver.addSygusConstraint(boolTerm)
|
|
res = solver.checkSynth()
|
|
assert not res.isNull()
|
|
assert not res.hasSolution()
|
|
assert res.hasNoSolution()
|
|
assert not res.isUnknown()
|