Properly guard commands in the SyGuS API (#8390)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 25 Mar 2022 02:21:44 +0000 (21:21 -0500)
committerGitHub <noreply@github.com>
Fri, 25 Mar 2022 02:21:44 +0000 (02:21 +0000)
commit7ae28c60383ca156cba69cfcc43062195ff59d3a
treed19188fbf9b955481de49d2ef9583cc5322157d7
parent59e78c5cab0da7973c76c67818dac6154f5ff1b0
Properly guard commands in the SyGuS API (#8390)

This commit ensures we don't segfault in the SyGuS API (for non-text inputs) if the option sygus is not set to true. It also renames mkSygusVar to declareSygusVar for consistency with the sygus input format.

For SyGuS API inputs, we now use the option sygus to true instead of setting the language to sygus2.

This furthermore changes a few details in set-defaults regarding the relationship between the language, the sygus option, and when to apply default options for sygus.

It also adds a unit test for checkSynth.
28 files changed:
examples/api/cpp/sygus-fun.cpp
examples/api/cpp/sygus-grammar.cpp
examples/api/cpp/sygus-inv.cpp
examples/api/java/SygusFun.java
examples/api/java/SygusGrammar.java
examples/api/java/SygusInv.java
examples/api/python/sygus-fun.py
examples/api/python/sygus-grammar.py
examples/api/python/sygus-inv.py
src/api/cpp/cvc5.cpp
src/api/cpp/cvc5.h
src/api/java/io/github/cvc5/api/Solver.java
src/api/java/jni/solver.cpp
src/api/python/cvc5.pxd
src/api/python/cvc5.pxi
src/main/driver_unified.cpp
src/parser/smt2/Smt2.g
src/smt/set_defaults.cpp
src/theory/quantifiers/sygus/cegis_core_connective.cpp
src/theory/sets/theory_sets_private.cpp
test/regress/cli/CMakeLists.txt
test/regress/cli/regress1/abduction/abduction_1255.corecstrs.readable.smt2
test/unit/api/cpp/grammar_black.cpp
test/unit/api/cpp/solver_black.cpp
test/unit/api/java/GrammarTest.java
test/unit/api/java/SolverTest.java
test/unit/api/python/test_grammar.py
test/unit/api/python/test_solver.py