Do not make SyGuS subsolver in unsat state after solving (#7759)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 9 Dec 2021 14:38:28 +0000 (08:38 -0600)
committerGitHub <noreply@github.com>
Thu, 9 Dec 2021 14:38:28 +0000 (14:38 +0000)
commitfd58b474ac339da44dc27ddbad12fefaf3fbbd4e
tree6ecd92576c2b9700d9ae49389e52865e68a83e88
parent5429a0bc6d0fc041e1a70966dee40e530862fb86
Do not make SyGuS subsolver in unsat state after solving (#7759)

This makes subsolvers answer "unknown" instead of "unsat" when solving SyGuS inputs, by setting unknown when a SyGuS input is solved instead of asserting the negation of the input. Knowing whether the call was successful is simply obtained by calling getSynthSolutions.

This will allow for multiple solutions for the same conjecture.
12 files changed:
src/preprocessing/passes/sygus_inference.cpp
src/smt/abduction_solver.cpp
src/smt/smt_solver.cpp
src/smt/sygus_solver.cpp
src/smt/sygus_solver.h
src/theory/incomplete_id.cpp
src/theory/incomplete_id.h
src/theory/inference_id.cpp
src/theory/inference_id.h
src/theory/quantifiers/sygus/synth_conjecture.cpp
src/theory/theory_engine.cpp
src/theory/theory_engine.h