LICENSE-Z3.txt
LICENSE.txt
README.md
setup.py
jz3/__init__.py
jz3/solver.py
jz3.egg-info/PKG-INFO
jz3.egg-info/SOURCES.txt
jz3.egg-info/dependency_links.txt
jz3.egg-info/requires.txt
jz3.egg-info/top_level.txt
jz3/analysis/__init__.py
jz3/analysis/compare_easy_sudokus.py
jz3/analysis/plot_comparison.py
jz3/analysis/archive/__init__.py
jz3/analysis/archive/export_to_excel.py
jz3/solvers/__init__ 2.py
jz3/solvers/__init__.py
jz3/solvers/cvc5-main/__init__ 2.py
jz3/solvers/cvc5-main/__init__.py
jz3/solvers/cvc5-main/build/__init__.py
jz3/solvers/cvc5-main/build/deps/__init__.py
jz3/solvers/cvc5-main/build/deps/src/__init__.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/__init__.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/examples/__init__.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/examples/cad/__init__.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/examples/cad/cad.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/examples/cad/plot.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/examples/cad/sign_table.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/__init__.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/__init__.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/check.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/polypy_test.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/__init__.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/algebraic_number.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/polynomial_arithmetic.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/polynomial_eval.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/polynomial_factorization.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/polynomial_feasibility.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/polynomial_gcd.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/polynomial_mgcd.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/polynomial_resultants.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/polynomial_roots.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/polynomial_sgn.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/upolynomial_factor.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/upolynomial_gcd.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/upolynomial_roots.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/value.py
jz3/solvers/cvc5-main/build/deps/src/Poly-EP/test/python/tests/variable.py
jz3/solvers/cvc5-main/contrib/__init__ 2.py
jz3/solvers/cvc5-main/contrib/__init__.py
jz3/solvers/cvc5-main/contrib/learn_resource_weights.py
jz3/solvers/cvc5-main/contrib/make-release.py
jz3/solvers/cvc5-main/contrib/uncovered-api-functions.py
jz3/solvers/cvc5-main/contrib/packaging_python/__init__.py
jz3/solvers/cvc5-main/contrib/packaging_python/mk_build_dir.py
jz3/solvers/cvc5-main/contrib/packaging_python/mk_wheel.py
jz3/solvers/cvc5-main/docs/__init__.py
jz3/solvers/cvc5-main/docs/ext/__init__.py
jz3/solvers/cvc5-main/docs/ext/autoenum.py
jz3/solvers/cvc5-main/docs/ext/examples.py
jz3/solvers/cvc5-main/docs/ext/include_build_file.py
jz3/solvers/cvc5-main/docs/ext/run_command.py
jz3/solvers/cvc5-main/docs/ext/smtliblexer.py
jz3/solvers/cvc5-main/examples/__init__ 2.py
jz3/solvers/cvc5-main/examples/__init__.py
jz3/solvers/cvc5-main/examples/api/__init__.py
jz3/solvers/cvc5-main/examples/api/python/__init__.py
jz3/solvers/cvc5-main/examples/api/python/bags.py
jz3/solvers/cvc5-main/examples/api/python/bitvectors.py
jz3/solvers/cvc5-main/examples/api/python/bitvectors_and_arrays.py
jz3/solvers/cvc5-main/examples/api/python/combination.py
jz3/solvers/cvc5-main/examples/api/python/datatypes.py
jz3/solvers/cvc5-main/examples/api/python/exceptions.py
jz3/solvers/cvc5-main/examples/api/python/extract.py
jz3/solvers/cvc5-main/examples/api/python/finite_field.py
jz3/solvers/cvc5-main/examples/api/python/floating_point.py
jz3/solvers/cvc5-main/examples/api/python/helloworld.py
jz3/solvers/cvc5-main/examples/api/python/id.py
jz3/solvers/cvc5-main/examples/api/python/linear_arith.py
jz3/solvers/cvc5-main/examples/api/python/quickstart.py
jz3/solvers/cvc5-main/examples/api/python/relations.py
jz3/solvers/cvc5-main/examples/api/python/sequences.py
jz3/solvers/cvc5-main/examples/api/python/sets.py
jz3/solvers/cvc5-main/examples/api/python/strings.py
jz3/solvers/cvc5-main/examples/api/python/sygus-fun.py
jz3/solvers/cvc5-main/examples/api/python/sygus-inv.py
jz3/solvers/cvc5-main/examples/api/python/transcendentals.py
jz3/solvers/cvc5-main/examples/api/python/utils.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/__init__.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/bitvectors.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/bitvectors_and_arrays.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/combination.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/datatypes.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/exceptions.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/extract.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/floating_point.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/helloworld.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/id.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/linear_arith.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/quickstart.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/sets.py
jz3/solvers/cvc5-main/examples/api/python/pythonic/transcendentals.py
jz3/solvers/cvc5-main/src/__init__.py
jz3/solvers/cvc5-main/src/api/__init__.py
jz3/solvers/cvc5-main/src/api/parseenums.py
jz3/solvers/cvc5-main/src/api/java/__init__.py
jz3/solvers/cvc5-main/src/api/python/__init__.py
jz3/solvers/cvc5-main/src/base/__init__.py
jz3/solvers/cvc5-main/src/base/collect_tags.py
jz3/solvers/cvc5-main/src/options/__init__.py
jz3/solvers/cvc5-main/src/options/mkoptions.py
jz3/solvers/cvc5-main/src/rewriter/__init__.py
jz3/solvers/cvc5-main/src/rewriter/mkrewrites.py
jz3/solvers/cvc5-main/src/rewriter/node.py
jz3/solvers/cvc5-main/src/rewriter/rule 2.py
jz3/solvers/cvc5-main/src/rewriter/rule.py
jz3/solvers/cvc5-main/src/rewriter/rw_parser.py
jz3/solvers/cvc5-main/src/rewriter/util.py
jz3/solvers/cvc5-main/test/__init__ 2.py
jz3/solvers/cvc5-main/test/__init__.py
jz3/solvers/cvc5-main/test/api/__init__.py
jz3/solvers/cvc5-main/test/api/python/__init__.py
jz3/solvers/cvc5-main/test/api/python/boilerplate.py
jz3/solvers/cvc5-main/test/api/python/finite_field.py
jz3/solvers/cvc5-main/test/api/python/issue4889.py
jz3/solvers/cvc5-main/test/api/python/issue5074.py
jz3/solvers/cvc5-main/test/api/python/issue6111.py
jz3/solvers/cvc5-main/test/api/python/proj-issue306.py
jz3/solvers/cvc5-main/test/api/python/reset_assertions.py
jz3/solvers/cvc5-main/test/api/python/sep_log_api.py
jz3/solvers/cvc5-main/test/api/python/two_solvers.py
jz3/solvers/cvc5-main/test/binary/__init__.py
jz3/solvers/cvc5-main/test/binary/interactive_shell.py
jz3/solvers/cvc5-main/test/regress/__init__.py
jz3/solvers/cvc5-main/test/regress/cli/__init__.py
jz3/solvers/cvc5-main/test/regress/cli/run_regression.py
jz3/solvers/cvc5-main/test/unit/__init__.py
jz3/solvers/cvc5-main/test/unit/api/__init__.py
jz3/solvers/cvc5-main/test/unit/api/python/__init__.py
jz3/solvers/cvc5-main/test/unit/api/python/test_datatype_api.py
jz3/solvers/cvc5-main/test/unit/api/python/test_finite_field.py
jz3/solvers/cvc5-main/test/unit/api/python/test_grammar.py
jz3/solvers/cvc5-main/test/unit/api/python/test_op.py
jz3/solvers/cvc5-main/test/unit/api/python/test_proof.py
jz3/solvers/cvc5-main/test/unit/api/python/test_result.py
jz3/solvers/cvc5-main/test/unit/api/python/test_solver.py
jz3/solvers/cvc5-main/test/unit/api/python/test_sort.py
jz3/solvers/cvc5-main/test/unit/api/python/test_synth_result.py
jz3/solvers/cvc5-main/test/unit/api/python/test_term.py
jz3/solvers/cvc5-main/test/unit/api/python/test_to_python_obj.py
jz3/src/__init__.py
jz3/src/clean_up.py
jz3/src/run_solvers.py
jz3/src/z3_quick_start_guide.py
jz3/src/z3_wrapper.py
jz3/src/SMTs/SMTs.py
jz3/src/SMTs/__init__.py
jz3/src/Sudokus/Sudoku.py
jz3/src/Sudokus/__init__.py
jz3/src/Sudokus/sudoku_exhaustive_search_condition.py
jz3/src/Sudokus/sudoku_heuristic_search_condition.py
jz3/tests/__init__.py
jz3/tests/test_solver.py