git.libre-soc.org Git - cvc5.git/commit

author	Andres Noetzli <andres.noetzli@gmail.com>
	Fri, 1 Apr 2022 16:26:14 +0000 (09:26 -0700)
committer	GitHub <noreply@github.com>
	Fri, 1 Apr 2022 16:26:14 +0000 (16:26 +0000)
commit	f02847cdee29a810dbf8e25af1502458fcbdd562
tree	6e3c89bbaec1b3180b46b04e3834afcd45d4cf4f	tree
parent	6987d112496849d72b34d93d482c3555d1634fea	commit \| diff

[API] Add mode argument for `Solver::blockModel()` (#8521)

This commit changes Solver::blockModel() to take a mode as an argument
instead of relying on an option.

27 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/java/CMakeLists.txt		diff \| blob \| history
src/api/java/genenums.py.in		diff \| blob \| history
src/api/java/io/github/cvc5/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/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/smt2/smt2.h		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/model_blocker.cpp		diff \| blob \| history
src/smt/model_blocker.h		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/solver_engine.h		diff \| blob \| history
test/regress/cli/regress1/model-blocker-simple.smt2		diff \| blob \| history
test/regress/cli/regress1/model-blocker-values.smt2		diff \| blob \| history
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

RSS Atom