Import PySMT-0.9.0 as math/py-smt.

pySMT is a solver-agnostic library for SMT Formulae manipulation and
solving.

4 files changed, 429 insertions, 0 deletions

diff --git a/math/py-smt/DESCR b/math/py-smt/DESCR
new file mode 100644
index 00000000000..17c4514fec2
--- /dev/null
+++ b/math/py-smt/DESCR
@@ -0,0 +1,13 @@
+pySMT is a solver-agnostic library for SMT Formulae manipulation and
+solving.
+
+pySMT makes working with Satisfiability Modulo Theory simple:
+
+- Define formulae in a simple, intuitive, and solver independent way
+
+- Solve your formulae using one of the native solvers, or by wrapping
+  any SMT-Lib compliant solver,
+
+- Dump your problems in the SMT-Lib format,
+
+- and more...
diff --git a/math/py-smt/Makefile b/math/py-smt/Makefile
new file mode 100644
index 00000000000..77caca0cded
--- /dev/null
+++ b/math/py-smt/Makefile
@@ -0,0 +1,36 @@
+#	$NetBSD: Makefile,v 1.1 2020/08/18 20:14:33 riastradh Exp $
+
+VERSION=	0.9.0
+DISTNAME=	PySMT-${VERSION}
+PKGNAME=	${PYPKGPREFIX}-smt-${VERSION}
+CATEGORIES=	math
+MASTER_SITES=	${MASTER_SITE_GITHUB:=pysmt/}
+GITHUB_PROJECT=	pysmt
+GITHUB_TAG=	v${VERSION}
+
+MAINTAINER=	pkgsrc-users@NetBSD.org
+HOMEPAGE=	http://www.pysmt.org/
+COMMENT=	Library for SMT formula manipulation and solving
+LICENSE=	apache-2.0
+
+PYTHON_VERSIONS_INCOMPATIBLE=	27
+
+DEPENDS+=	${PYPKGPREFIX}-six>=0:../../lang/py-six
+
+TEST_DEPENDS+=	${PYPKGPREFIX}-nose>=0:../../devel/py-nose
+TEST_DEPENDS+=	${PYPKGPREFIX}-z3>=0:../../math/py-z3
+
+SUBST_CLASSES+=		python3
+SUBST_STAGE.python3=	pre-test
+SUBST_MESSAGE.python3=	Fixing python3 interpreter
+SUBST_SED.python3+=	-e 's,python3 ,${PYTHONBIN} ,'
+SUBST_FILES.python3+=	run_tests.sh
+
+do-test:
+	${RUN} cd ${WRKSRC} && \
+	${SETENV} ${TEST_ENV} \
+	${SH} run_tests.sh
+
+.include "../../lang/python/egg.mk"
+.include "../../lang/python/application.mk"
+.include "../../mk/bsd.pkg.mk"
diff --git a/math/py-smt/PLIST b/math/py-smt/PLIST
new file mode 100644
index 00000000000..2d51b4352ad
--- /dev/null
+++ b/math/py-smt/PLIST
@@ -0,0 +1,374 @@
+@comment $NetBSD: PLIST,v 1.1 2020/08/18 20:14:33 riastradh Exp $
+bin/pysmt-install
+${PYSITELIB}/${EGG_INFODIR}/PKG-INFO
+${PYSITELIB}/${EGG_INFODIR}/SOURCES.txt
+${PYSITELIB}/${EGG_INFODIR}/dependency_links.txt
+${PYSITELIB}/${EGG_INFODIR}/entry_points.txt
+${PYSITELIB}/${EGG_INFODIR}/requires.txt
+${PYSITELIB}/${EGG_INFODIR}/top_level.txt
+${PYSITELIB}/pysmt/__init__.py
+${PYSITELIB}/pysmt/__init__.pyc
+${PYSITELIB}/pysmt/__init__.pyo
+${PYSITELIB}/pysmt/__main__.py
+${PYSITELIB}/pysmt/__main__.pyc
+${PYSITELIB}/pysmt/__main__.pyo
+${PYSITELIB}/pysmt/cmd/__init__.py
+${PYSITELIB}/pysmt/cmd/__init__.pyc
+${PYSITELIB}/pysmt/cmd/__init__.pyo
+${PYSITELIB}/pysmt/cmd/check_version.py
+${PYSITELIB}/pysmt/cmd/check_version.pyc
+${PYSITELIB}/pysmt/cmd/check_version.pyo
+${PYSITELIB}/pysmt/cmd/install.py
+${PYSITELIB}/pysmt/cmd/install.pyc
+${PYSITELIB}/pysmt/cmd/install.pyo
+${PYSITELIB}/pysmt/cmd/installers/__init__.py
+${PYSITELIB}/pysmt/cmd/installers/__init__.pyc
+${PYSITELIB}/pysmt/cmd/installers/__init__.pyo
+${PYSITELIB}/pysmt/cmd/installers/base.py
+${PYSITELIB}/pysmt/cmd/installers/base.pyc
+${PYSITELIB}/pysmt/cmd/installers/base.pyo
+${PYSITELIB}/pysmt/cmd/installers/bdd.py
+${PYSITELIB}/pysmt/cmd/installers/bdd.pyc
+${PYSITELIB}/pysmt/cmd/installers/bdd.pyo
+${PYSITELIB}/pysmt/cmd/installers/btor.py
+${PYSITELIB}/pysmt/cmd/installers/btor.pyc
+${PYSITELIB}/pysmt/cmd/installers/btor.pyo
+${PYSITELIB}/pysmt/cmd/installers/cvc4.py
+${PYSITELIB}/pysmt/cmd/installers/cvc4.pyc
+${PYSITELIB}/pysmt/cmd/installers/cvc4.pyo
+${PYSITELIB}/pysmt/cmd/installers/msat.py
+${PYSITELIB}/pysmt/cmd/installers/msat.pyc
+${PYSITELIB}/pysmt/cmd/installers/msat.pyo
+${PYSITELIB}/pysmt/cmd/installers/pico.py
+${PYSITELIB}/pysmt/cmd/installers/pico.pyc
+${PYSITELIB}/pysmt/cmd/installers/pico.pyo
+${PYSITELIB}/pysmt/cmd/installers/yices.py
+${PYSITELIB}/pysmt/cmd/installers/yices.pyc
+${PYSITELIB}/pysmt/cmd/installers/yices.pyo
+${PYSITELIB}/pysmt/cmd/installers/z3.py
+${PYSITELIB}/pysmt/cmd/installers/z3.pyc
+${PYSITELIB}/pysmt/cmd/installers/z3.pyo
+${PYSITELIB}/pysmt/cmd/shell.py
+${PYSITELIB}/pysmt/cmd/shell.pyc
+${PYSITELIB}/pysmt/cmd/shell.pyo
+${PYSITELIB}/pysmt/configuration.py
+${PYSITELIB}/pysmt/configuration.pyc
+${PYSITELIB}/pysmt/configuration.pyo
+${PYSITELIB}/pysmt/constants.py
+${PYSITELIB}/pysmt/constants.pyc
+${PYSITELIB}/pysmt/constants.pyo
+${PYSITELIB}/pysmt/decorators.py
+${PYSITELIB}/pysmt/decorators.pyc
+${PYSITELIB}/pysmt/decorators.pyo
+${PYSITELIB}/pysmt/environment.py
+${PYSITELIB}/pysmt/environment.pyc
+${PYSITELIB}/pysmt/environment.pyo
+${PYSITELIB}/pysmt/exceptions.py
+${PYSITELIB}/pysmt/exceptions.pyc
+${PYSITELIB}/pysmt/exceptions.pyo
+${PYSITELIB}/pysmt/factory.py
+${PYSITELIB}/pysmt/factory.pyc
+${PYSITELIB}/pysmt/factory.pyo
+${PYSITELIB}/pysmt/fnode.py
+${PYSITELIB}/pysmt/fnode.pyc
+${PYSITELIB}/pysmt/fnode.pyo
+${PYSITELIB}/pysmt/formula.py
+${PYSITELIB}/pysmt/formula.pyc
+${PYSITELIB}/pysmt/formula.pyo
+${PYSITELIB}/pysmt/logics.py
+${PYSITELIB}/pysmt/logics.pyc
+${PYSITELIB}/pysmt/logics.pyo
+${PYSITELIB}/pysmt/operators.py
+${PYSITELIB}/pysmt/operators.pyc
+${PYSITELIB}/pysmt/operators.pyo
+${PYSITELIB}/pysmt/oracles.py
+${PYSITELIB}/pysmt/oracles.pyc
+${PYSITELIB}/pysmt/oracles.pyo
+${PYSITELIB}/pysmt/parsing.py
+${PYSITELIB}/pysmt/parsing.pyc
+${PYSITELIB}/pysmt/parsing.pyo
+${PYSITELIB}/pysmt/printers.py
+${PYSITELIB}/pysmt/printers.pyc
+${PYSITELIB}/pysmt/printers.pyo
+${PYSITELIB}/pysmt/rewritings.py
+${PYSITELIB}/pysmt/rewritings.pyc
+${PYSITELIB}/pysmt/rewritings.pyo
+${PYSITELIB}/pysmt/shortcuts.py
+${PYSITELIB}/pysmt/shortcuts.pyc
+${PYSITELIB}/pysmt/shortcuts.pyo
+${PYSITELIB}/pysmt/simplifier.py
+${PYSITELIB}/pysmt/simplifier.pyc
+${PYSITELIB}/pysmt/simplifier.pyo
+${PYSITELIB}/pysmt/smtlib/__init__.py
+${PYSITELIB}/pysmt/smtlib/__init__.pyc
+${PYSITELIB}/pysmt/smtlib/__init__.pyo
+${PYSITELIB}/pysmt/smtlib/annotations.py
+${PYSITELIB}/pysmt/smtlib/annotations.pyc
+${PYSITELIB}/pysmt/smtlib/annotations.pyo
+${PYSITELIB}/pysmt/smtlib/commands.py
+${PYSITELIB}/pysmt/smtlib/commands.pyc
+${PYSITELIB}/pysmt/smtlib/commands.pyo
+${PYSITELIB}/pysmt/smtlib/parser/__init__.py
+${PYSITELIB}/pysmt/smtlib/parser/__init__.pyc
+${PYSITELIB}/pysmt/smtlib/parser/__init__.pyo
+${PYSITELIB}/pysmt/smtlib/parser/parser.py
+${PYSITELIB}/pysmt/smtlib/parser/parser.pyc
+${PYSITELIB}/pysmt/smtlib/parser/parser.pyo
+${PYSITELIB}/pysmt/smtlib/printers.py
+${PYSITELIB}/pysmt/smtlib/printers.pyc
+${PYSITELIB}/pysmt/smtlib/printers.pyo
+${PYSITELIB}/pysmt/smtlib/script.py
+${PYSITELIB}/pysmt/smtlib/script.pyc
+${PYSITELIB}/pysmt/smtlib/script.pyo
+${PYSITELIB}/pysmt/smtlib/solver.py
+${PYSITELIB}/pysmt/smtlib/solver.pyc
+${PYSITELIB}/pysmt/smtlib/solver.pyo
+${PYSITELIB}/pysmt/solvers/__init__.py
+${PYSITELIB}/pysmt/solvers/__init__.pyc
+${PYSITELIB}/pysmt/solvers/__init__.pyo
+${PYSITELIB}/pysmt/solvers/bdd.py
+${PYSITELIB}/pysmt/solvers/bdd.pyc
+${PYSITELIB}/pysmt/solvers/bdd.pyo
+${PYSITELIB}/pysmt/solvers/btor.py
+${PYSITELIB}/pysmt/solvers/btor.pyc
+${PYSITELIB}/pysmt/solvers/btor.pyo
+${PYSITELIB}/pysmt/solvers/cvc4.py
+${PYSITELIB}/pysmt/solvers/cvc4.pyc
+${PYSITELIB}/pysmt/solvers/cvc4.pyo
+${PYSITELIB}/pysmt/solvers/eager.py
+${PYSITELIB}/pysmt/solvers/eager.pyc
+${PYSITELIB}/pysmt/solvers/eager.pyo
+${PYSITELIB}/pysmt/solvers/interpolation.py
+${PYSITELIB}/pysmt/solvers/interpolation.pyc
+${PYSITELIB}/pysmt/solvers/interpolation.pyo
+${PYSITELIB}/pysmt/solvers/msat.py
+${PYSITELIB}/pysmt/solvers/msat.pyc
+${PYSITELIB}/pysmt/solvers/msat.pyo
+${PYSITELIB}/pysmt/solvers/options.py
+${PYSITELIB}/pysmt/solvers/options.pyc
+${PYSITELIB}/pysmt/solvers/options.pyo
+${PYSITELIB}/pysmt/solvers/pico.py
+${PYSITELIB}/pysmt/solvers/pico.pyc
+${PYSITELIB}/pysmt/solvers/pico.pyo
+${PYSITELIB}/pysmt/solvers/portfolio.py
+${PYSITELIB}/pysmt/solvers/portfolio.pyc
+${PYSITELIB}/pysmt/solvers/portfolio.pyo
+${PYSITELIB}/pysmt/solvers/qelim.py
+${PYSITELIB}/pysmt/solvers/qelim.pyc
+${PYSITELIB}/pysmt/solvers/qelim.pyo
+${PYSITELIB}/pysmt/solvers/smtlib.py
+${PYSITELIB}/pysmt/solvers/smtlib.pyc
+${PYSITELIB}/pysmt/solvers/smtlib.pyo
+${PYSITELIB}/pysmt/solvers/solver.py
+${PYSITELIB}/pysmt/solvers/solver.pyc
+${PYSITELIB}/pysmt/solvers/solver.pyo
+${PYSITELIB}/pysmt/solvers/yices.py
+${PYSITELIB}/pysmt/solvers/yices.pyc
+${PYSITELIB}/pysmt/solvers/yices.pyo
+${PYSITELIB}/pysmt/solvers/z3.py
+${PYSITELIB}/pysmt/solvers/z3.pyc
+${PYSITELIB}/pysmt/solvers/z3.pyo
+${PYSITELIB}/pysmt/substituter.py
+${PYSITELIB}/pysmt/substituter.pyc
+${PYSITELIB}/pysmt/substituter.pyo
+${PYSITELIB}/pysmt/test/__init__.py
+${PYSITELIB}/pysmt/test/__init__.pyc
+${PYSITELIB}/pysmt/test/__init__.pyo
+${PYSITELIB}/pysmt/test/examples.py
+${PYSITELIB}/pysmt/test/examples.pyc
+${PYSITELIB}/pysmt/test/examples.pyo
+${PYSITELIB}/pysmt/test/smtlib/__init__.py
+${PYSITELIB}/pysmt/test/smtlib/__init__.pyc
+${PYSITELIB}/pysmt/test/smtlib/__init__.pyo
+${PYSITELIB}/pysmt/test/smtlib/parser_utils.py
+${PYSITELIB}/pysmt/test/smtlib/parser_utils.pyc
+${PYSITELIB}/pysmt/test/smtlib/parser_utils.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_annotations.py
+${PYSITELIB}/pysmt/test/smtlib/test_annotations.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_annotations.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_fuzzed.py
+${PYSITELIB}/pysmt/test/smtlib/test_fuzzed.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_fuzzed.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_generic_wrapper.py
+${PYSITELIB}/pysmt/test/smtlib/test_generic_wrapper.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_generic_wrapper.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_griggio.py
+${PYSITELIB}/pysmt/test/smtlib/test_griggio.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_griggio.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_examples.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_examples.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_examples.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_extensibility.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_extensibility.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_extensibility.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_lra.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_lra.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_lra.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_arrays.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_arrays.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_arrays.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_lia.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_lia.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_lia.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_lira.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_lira.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_lira.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_lra.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_lra.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_lra.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_nia.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_nia.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_nia.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_nra.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_nra.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_nra.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_ufbv.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_ufbv.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_qf_ufbv.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_parser_type_error.py
+${PYSITELIB}/pysmt/test/smtlib/test_parser_type_error.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_parser_type_error.pyo
+${PYSITELIB}/pysmt/test/smtlib/test_smtlibscript.py
+${PYSITELIB}/pysmt/test/smtlib/test_smtlibscript.pyc
+${PYSITELIB}/pysmt/test/smtlib/test_smtlibscript.pyo
+${PYSITELIB}/pysmt/test/test_array.py
+${PYSITELIB}/pysmt/test/test_array.pyc
+${PYSITELIB}/pysmt/test/test_array.pyo
+${PYSITELIB}/pysmt/test/test_back.py
+${PYSITELIB}/pysmt/test/test_back.pyc
+${PYSITELIB}/pysmt/test/test_back.pyo
+${PYSITELIB}/pysmt/test/test_bdd.py
+${PYSITELIB}/pysmt/test/test_bdd.pyc
+${PYSITELIB}/pysmt/test/test_bdd.pyo
+${PYSITELIB}/pysmt/test/test_bv.py
+${PYSITELIB}/pysmt/test/test_bv.pyc
+${PYSITELIB}/pysmt/test/test_bv.pyo
+${PYSITELIB}/pysmt/test/test_bv_simplification.py
+${PYSITELIB}/pysmt/test/test_bv_simplification.pyc
+${PYSITELIB}/pysmt/test/test_bv_simplification.pyo
+${PYSITELIB}/pysmt/test/test_cnf.py
+${PYSITELIB}/pysmt/test/test_cnf.pyc
+${PYSITELIB}/pysmt/test/test_cnf.pyo
+${PYSITELIB}/pysmt/test/test_configuration.py
+${PYSITELIB}/pysmt/test/test_configuration.pyc
+${PYSITELIB}/pysmt/test/test_configuration.pyo
+${PYSITELIB}/pysmt/test/test_constants.py
+${PYSITELIB}/pysmt/test/test_constants.pyc
+${PYSITELIB}/pysmt/test/test_constants.pyo
+${PYSITELIB}/pysmt/test/test_cvc4_quantifiers.py
+${PYSITELIB}/pysmt/test/test_cvc4_quantifiers.pyc
+${PYSITELIB}/pysmt/test/test_cvc4_quantifiers.pyo
+${PYSITELIB}/pysmt/test/test_dwf.py
+${PYSITELIB}/pysmt/test/test_dwf.pyc
+${PYSITELIB}/pysmt/test/test_dwf.pyo
+${PYSITELIB}/pysmt/test/test_eager_model.py
+${PYSITELIB}/pysmt/test/test_eager_model.pyc
+${PYSITELIB}/pysmt/test/test_eager_model.pyo
+${PYSITELIB}/pysmt/test/test_env.py
+${PYSITELIB}/pysmt/test/test_env.pyc
+${PYSITELIB}/pysmt/test/test_env.pyo
+${PYSITELIB}/pysmt/test/test_euf.py
+${PYSITELIB}/pysmt/test/test_euf.pyc
+${PYSITELIB}/pysmt/test/test_euf.pyo
+${PYSITELIB}/pysmt/test/test_formula.py
+${PYSITELIB}/pysmt/test/test_formula.pyc
+${PYSITELIB}/pysmt/test/test_formula.pyo
+${PYSITELIB}/pysmt/test/test_hr_parsing.py
+${PYSITELIB}/pysmt/test/test_hr_parsing.pyc
+${PYSITELIB}/pysmt/test/test_hr_parsing.pyo
+${PYSITELIB}/pysmt/test/test_imports.py
+${PYSITELIB}/pysmt/test/test_imports.pyc
+${PYSITELIB}/pysmt/test/test_imports.pyo
+${PYSITELIB}/pysmt/test/test_int.py
+${PYSITELIB}/pysmt/test/test_int.pyc
+${PYSITELIB}/pysmt/test/test_int.pyo
+${PYSITELIB}/pysmt/test/test_interpolation.py
+${PYSITELIB}/pysmt/test/test_interpolation.pyc
+${PYSITELIB}/pysmt/test/test_interpolation.pyo
+${PYSITELIB}/pysmt/test/test_lira.py
+${PYSITELIB}/pysmt/test/test_lira.pyc
+${PYSITELIB}/pysmt/test/test_lira.pyo
+${PYSITELIB}/pysmt/test/test_logics.py
+${PYSITELIB}/pysmt/test/test_logics.pyc
+${PYSITELIB}/pysmt/test/test_logics.pyo
+${PYSITELIB}/pysmt/test/test_models.py
+${PYSITELIB}/pysmt/test/test_models.pyc
+${PYSITELIB}/pysmt/test/test_models.pyo
+${PYSITELIB}/pysmt/test/test_native_qe.py
+${PYSITELIB}/pysmt/test/test_native_qe.pyc
+${PYSITELIB}/pysmt/test/test_native_qe.pyo
+${PYSITELIB}/pysmt/test/test_nlira.py
+${PYSITELIB}/pysmt/test/test_nlira.pyc
+${PYSITELIB}/pysmt/test/test_nlira.pyo
+${PYSITELIB}/pysmt/test/test_oracles.py
+${PYSITELIB}/pysmt/test/test_oracles.pyc
+${PYSITELIB}/pysmt/test/test_oracles.pyo
+${PYSITELIB}/pysmt/test/test_portfolio.py
+${PYSITELIB}/pysmt/test/test_portfolio.pyc
+${PYSITELIB}/pysmt/test/test_portfolio.pyo
+${PYSITELIB}/pysmt/test/test_printing.py
+${PYSITELIB}/pysmt/test/test_printing.pyc
+${PYSITELIB}/pysmt/test/test_printing.pyo
+${PYSITELIB}/pysmt/test/test_qe.py
+${PYSITELIB}/pysmt/test/test_qe.pyc
+${PYSITELIB}/pysmt/test/test_qe.pyo
+${PYSITELIB}/pysmt/test/test_regressions.py
+${PYSITELIB}/pysmt/test/test_regressions.pyc
+${PYSITELIB}/pysmt/test/test_regressions.pyo
+${PYSITELIB}/pysmt/test/test_rewritings.py
+${PYSITELIB}/pysmt/test/test_rewritings.pyc
+${PYSITELIB}/pysmt/test/test_rewritings.pyo
+${PYSITELIB}/pysmt/test/test_shannon_expansion.py
+${PYSITELIB}/pysmt/test/test_shannon_expansion.pyc
+${PYSITELIB}/pysmt/test/test_shannon_expansion.pyo
+${PYSITELIB}/pysmt/test/test_simplify.py
+${PYSITELIB}/pysmt/test/test_simplify.pyc
+${PYSITELIB}/pysmt/test/test_simplify.pyo
+${PYSITELIB}/pysmt/test/test_size.py
+${PYSITELIB}/pysmt/test/test_size.pyc
+${PYSITELIB}/pysmt/test/test_size.pyo
+${PYSITELIB}/pysmt/test/test_solving.py
+${PYSITELIB}/pysmt/test/test_solving.pyc
+${PYSITELIB}/pysmt/test/test_solving.pyo
+${PYSITELIB}/pysmt/test/test_sorts.py
+${PYSITELIB}/pysmt/test/test_sorts.pyc
+${PYSITELIB}/pysmt/test/test_sorts.pyo
+${PYSITELIB}/pysmt/test/test_string.py
+${PYSITELIB}/pysmt/test/test_string.pyc
+${PYSITELIB}/pysmt/test/test_string.pyo
+${PYSITELIB}/pysmt/test/test_typechecker.py
+${PYSITELIB}/pysmt/test/test_typechecker.pyc
+${PYSITELIB}/pysmt/test/test_typechecker.pyo
+${PYSITELIB}/pysmt/test/test_unsat_cores.py
+${PYSITELIB}/pysmt/test/test_unsat_cores.pyc
+${PYSITELIB}/pysmt/test/test_unsat_cores.pyo
+${PYSITELIB}/pysmt/test/test_walker_ext.py
+${PYSITELIB}/pysmt/test/test_walker_ext.pyc
+${PYSITELIB}/pysmt/test/test_walker_ext.pyo
+${PYSITELIB}/pysmt/test/test_walkers.py
+${PYSITELIB}/pysmt/test/test_walkers.pyc
+${PYSITELIB}/pysmt/test/test_walkers.pyo
+${PYSITELIB}/pysmt/type_checker.py
+${PYSITELIB}/pysmt/type_checker.pyc
+${PYSITELIB}/pysmt/type_checker.pyo
+${PYSITELIB}/pysmt/typing.py
+${PYSITELIB}/pysmt/typing.pyc
+${PYSITELIB}/pysmt/typing.pyo
+${PYSITELIB}/pysmt/utils.py
+${PYSITELIB}/pysmt/utils.pyc
+${PYSITELIB}/pysmt/utils.pyo
+${PYSITELIB}/pysmt/walkers/__init__.py
+${PYSITELIB}/pysmt/walkers/__init__.pyc
+${PYSITELIB}/pysmt/walkers/__init__.pyo
+${PYSITELIB}/pysmt/walkers/dag.py
+${PYSITELIB}/pysmt/walkers/dag.pyc
+${PYSITELIB}/pysmt/walkers/dag.pyo
+${PYSITELIB}/pysmt/walkers/generic.py
+${PYSITELIB}/pysmt/walkers/generic.pyc
+${PYSITELIB}/pysmt/walkers/generic.pyo
+${PYSITELIB}/pysmt/walkers/identitydag.py
+${PYSITELIB}/pysmt/walkers/identitydag.pyc
+${PYSITELIB}/pysmt/walkers/identitydag.pyo
+${PYSITELIB}/pysmt/walkers/tree.py
+${PYSITELIB}/pysmt/walkers/tree.pyc
+${PYSITELIB}/pysmt/walkers/tree.pyo
diff --git a/math/py-smt/distinfo b/math/py-smt/distinfo
new file mode 100644
index 00000000000..380611bfe95
--- /dev/null
+++ b/math/py-smt/distinfo
@@ -0,0 +1,6 @@
+$NetBSD: distinfo,v 1.1 2020/08/18 20:14:33 riastradh Exp $
+
+SHA1 (PySMT-0.9.0.tar.gz) = 37dd2bed1de65039b87db2c6538ba39ae76a38bd
+RMD160 (PySMT-0.9.0.tar.gz) = ebf5be54396134910a95b1d05caa4aec693c8a3b
+SHA512 (PySMT-0.9.0.tar.gz) = 1ac42909b25529999779590899fe57d43f81d8aa2afcd52e41935795115ea34d2600a198010136c5643d99133c5179d1270e7d550af5d4653783ed26a2993623
+Size (PySMT-0.9.0.tar.gz) = 1130338 bytes