projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 231eaa4) | patch
Add support for get learned literals in the API (#8099)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 4 Mar 2022 14:37:54 +0000 (08:37 -0600)
committerGitHub <noreply@github.com>
Fri, 4 Mar 2022 14:37:54 +0000 (14:37 +0000)
commit8bd0cb485ecdc405102e7cbace37baf5c687f1b8
tree7a205104135943a456b6b92fc0be576c1d89b246tree
parent231eaa4afb7f65d14e75170ef74c75a6d1def7bccommit | diff
Add support for get learned literals in the API (#8099)

This command will eventually take a mode; for now it assumes a default implementation. I've opened cvc5/cvc5-wishues#104 to track this.

This is a feature requested by Certora.
27 files changed:
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5.h diff | blob | history
src/api/java/io/github/cvc5/api/Solver.java diff | blob | history
src/api/java/jni/solver.cpp diff | blob | history
src/api/python/cvc5.pxd diff | blob | history
src/api/python/cvc5.pxi diff | blob | history
src/options/smt_options.toml 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/prop/prop_engine.cpp diff | blob | history
src/prop/prop_engine.h diff | blob | history
src/prop/theory_proxy.cpp diff | blob | history
src/prop/theory_proxy.h diff | blob | history
src/prop/zero_level_learner.cpp diff | blob | history
src/prop/zero_level_learner.h diff | blob | history
src/smt/command.cpp diff | blob | history
src/smt/command.h diff | blob | history
src/smt/solver_engine.cpp diff | blob | history
src/smt/solver_engine.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/get-learned-literals.smt2 [new file with mode: 0644] blob
test/unit/api/cpp/solver_black.cpp diff | blob | history
test/unit/api/java/SolverTest.java diff | blob | history
test/unit/api/python/test_solver.py diff | blob | history