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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 14 Mar 2022 18:29:30 +0000 (13:29 -0500)
committer	GitHub <noreply@github.com>
	Mon, 14 Mar 2022 18:29:30 +0000 (18:29 +0000)
commit	2f1483e2e3e61c50e8bf6d7b7d86ea49f69371c6
tree	54eb45a5da738112a1581b7513b87724a494db15	tree
parent	434596534ef68bcc7c7162f16687f8827c8d8c50	commit \| diff

Remove unecessary methods from the API (#8260)

Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.

Updates examples and unit tests.

86 files changed:

examples/SimpleVC.java		diff \| blob \| history
examples/api/cpp/bitvectors.cpp		diff \| blob \| history
examples/api/cpp/combination.cpp		diff \| blob \| history
examples/api/cpp/extract.cpp		diff \| blob \| history
examples/api/cpp/helloworld.cpp		diff \| blob \| history
examples/api/cpp/linear_arith.cpp		diff \| blob \| history
examples/api/cpp/sets.cpp		diff \| blob \| history
examples/api/java/BitVectors.java		diff \| blob \| history
examples/api/java/Combination.java		diff \| blob \| history
examples/api/java/Extract.java		diff \| blob \| history
examples/api/java/HelloWorld.java		diff \| blob \| history
examples/api/java/LinearArith.java		diff \| blob \| history
examples/api/java/Sets.java		diff \| blob \| history
examples/api/python/bitvectors.py		diff \| blob \| history
examples/api/python/combination.py		diff \| blob \| history
examples/api/python/extract.py		diff \| blob \| history
examples/api/python/helloworld.py		diff \| blob \| history
examples/api/python/linear_arith.py		diff \| blob \| history
examples/api/python/sets.py		diff \| blob \| history
examples/simple_vc_cxx.cpp		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/cpp/cvc5_checks.h		diff \| blob \| history
src/api/java/io/github/cvc5/api/Result.java		diff \| blob \| history
src/api/java/io/github/cvc5/api/Solver.java		diff \| blob \| history
src/api/java/io/github/cvc5/api/Sort.java		diff \| blob \| history
src/api/java/jni/result.cpp		diff \| blob \| history
src/api/java/jni/solver.cpp		diff \| blob \| history
src/api/java/jni/sort.cpp		diff \| blob \| history
src/api/python/cvc5.pxd		diff \| blob \| history
src/api/python/cvc5.pxi		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/smt/assertions.cpp		diff \| blob \| history
src/smt/assertions.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/quant_elim_solver.cpp		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/smt/smt_solver.h		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/solver_engine.h		diff \| blob \| history
src/smt/sygus_solver.cpp		diff \| blob \| history
test/api/cpp/boilerplate.cpp		diff \| blob \| history
test/api/cpp/issue5074.cpp		diff \| blob \| history
test/api/cpp/proj-issue344.cpp		diff \| blob \| history
test/api/cpp/proj-issue345.cpp		diff \| blob \| history
test/api/cpp/two_solvers.cpp		diff \| blob \| history
test/api/python/boilerplate.py		diff \| blob \| history
test/api/python/issue5074.py		diff \| blob \| history
test/api/python/two_solvers.py		diff \| blob \| history
test/regress/regress0/bug398.smt2		diff \| blob \| history
test/regress/regress0/tptp/ARI086=1.p		diff \| blob \| history
test/regress/regress0/tptp/DAT001=1.p		diff \| blob \| history
test/regress/regress0/tptp/MGT019+2.p		diff \| blob \| history
test/regress/regress0/tptp/PUZ131_1.p		diff \| blob \| history
test/regress/regress0/tptp/SYN000+1.p		diff \| blob \| history
test/regress/regress0/tptp/SYN000=2.p		diff \| blob \| history
test/regress/regress0/tptp/SYN000_1.p		diff \| blob \| history
test/regress/regress0/tptp/is_rat_simple.p		diff \| blob \| history
test/regress/regress0/tptp/parse-neg-rational.p		diff \| blob \| history
test/regress/regress0/tptp/tff0-arith.p		diff \| blob \| history
test/regress/regress0/tptp/tff0.p		diff \| blob \| history
test/regress/regress0/tptp/tptp_parser10.p		diff \| blob \| history
test/regress/regress0/tptp/tptp_parser9.p		diff \| blob \| history
test/regress/regress1/bug800.smt2		diff \| blob \| history
test/regress/regress1/ho/NUM925^1.p		diff \| blob \| history
test/regress/regress1/ho/fta0328.lfho.p		diff \| blob \| history
test/regress/regress1/ho/store-ax-min.p		diff \| blob \| history
test/regress/regress2/ho/bug_instfalse_SEU882^5.p		diff \| blob \| history
test/regress/regress2/ho/involved_parsing_ALG248^3.p		diff \| blob \| history
test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p		diff \| blob \| history
test/unit/api/cpp/datatype_api_black.cpp		diff \| blob \| history
test/unit/api/cpp/result_black.cpp		diff \| blob \| history
test/unit/api/cpp/solver_black.cpp		diff \| blob \| history
test/unit/api/cpp/sort_black.cpp		diff \| blob \| history
test/unit/api/cpp/theory_arith_nl_black.cpp		diff \| blob \| history
test/unit/api/cpp/theory_uf_ho_black.cpp		diff \| blob \| history
test/unit/api/java/DatatypeTest.java		diff \| blob \| history
test/unit/api/java/ResultTest.java		diff \| blob \| history
test/unit/api/java/SolverTest.java		diff \| blob \| history
test/unit/api/java/SortTest.java		diff \| blob \| history
test/unit/api/python/test_datatype_api.py		diff \| blob \| history
test/unit/api/python/test_result.py		diff \| blob \| history
test/unit/api/python/test_solver.py		diff \| blob \| history
test/unit/api/python/test_sort.py		diff \| blob \| history
test/unit/api/python/test_to_python_obj.py		diff \| blob \| history

RSS Atom