projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d34e563) | patch
Support sygus version 2.1 command assume (#7081)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 14 Sep 2021 21:29:32 +0000 (16:29 -0500)
committerGitHub <noreply@github.com>
Tue, 14 Sep 2021 21:29:32 +0000 (21:29 +0000)
commit74c5067d81b8384701cff7f6e7b697d7fe67cf58
tree686d06c8fe27f122a0c8a6ad05d74c487570e966tree
parentd34e563fe48c42aa06eea44191a21dcf29772339commit | diff
Support sygus version 2.1 command assume (#7081)

Adds support for global assumptions in sygus files.

Also guards against cases of declare-const, which should be prohibited in sygus.
18 files changed:
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5.h diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/printer/printer.cpp diff | blob | history
src/printer/printer.h diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.h diff | blob | history
src/smt/command.cpp diff | blob | history
src/smt/command.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/smt/sygus_solver.cpp diff | blob | history
src/smt/sygus_solver.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/assume-simple.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy diff | blob | history
test/regress/regress1/sygus/replicate-mod-assume.sy [new file with mode: 0644] blob
test/unit/api/solver_black.cpp diff | blob | history