projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2aaa6ec) | patch
Add new method for enumerating unsat queries with SyGuS (#7459)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 25 Oct 2021 21:39:02 +0000 (16:39 -0500)
committerGitHub <noreply@github.com>
Mon, 25 Oct 2021 21:39:02 +0000 (21:39 +0000)
commitcb748679157eb658ce5d1173d8f26957daf8f3df
tree024859338fd336e43bba8b1775db5c0a9caeeca3tree
parent2aaa6ec1dfc3d7a41f120ef5361272b63363347bcommit | diff
Add new method for enumerating unsat queries with SyGuS (#7459)

This adds a new option for --sygus-query-gen=unsat to generate unsat queries (previously, only satisfiable queries were supported).

The algorithm can be seen as a variant of abduction where we conjoin predicates that both (1) refine the current model and (2) avoid repeated unsat cores.

It does some minor refactoring of ExprMinerManager to support the new module.
src/CMakeLists.txt diff | blob | history
src/options/quantifiers_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/expr_miner.cpp diff | blob | history
src/theory/quantifiers/expr_miner_manager.cpp diff | blob | history
src/theory/quantifiers/expr_miner_manager.h diff | blob | history
src/theory/quantifiers/query_generator_unsat.cpp [new file with mode: 0644] blob
src/theory/quantifiers/query_generator_unsat.h [new file with mode: 0644] blob
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress2/sygus/qgu-bools.sy [new file with mode: 0644] blob