projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e86726d) | patch
Properly restrict PBE symmetry breaking for abduction queries (#7269)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 29 Sep 2021 21:23:27 +0000 (16:23 -0500)
committerGitHub <noreply@github.com>
Wed, 29 Sep 2021 21:23:27 +0000 (16:23 -0500)
commit7d859b19c2755dc5071f4bedbbeab8a37870e69a
treefb3027464d75317ad87696828b14ebf00e80e9cftree
parente86726da4cf3883888a765aacf81ae76c7611c54commit | diff
Properly restrict PBE symmetry breaking for abduction queries (#7269)

This ensures we infer when a conjecture is PBE based on the conjecture plus the side condition for abduction. This fixes issues where the sygus solver was over-pruning solutions for abduction queries.

It also changes the names of internal symbols used for abduction/interpolation queries. These names are used when the experimental sygus-stream is used. These symbols are changed (from "A") to avoid confusion with user symbols.
src/smt/abduction_solver.cpp diff | blob | history
src/smt/interpolation_solver.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 [new file with mode: 0644] blob