pkgsrc/math, branch TNF

Initial import of Yices 2, version 2.6.1.

2019-08-24T22:09:16Z

Yices 2 is an SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, real and integer arithmetic, bitvectors, scalar types, and tuples. Yices 2 supports both linear and nonlinear arithmetic. Yices 2 can process input written in the SMT-LIB notation (both versions 2.0 and 1.2 are supported). Alternatively, you can write specifications using Yices 2's own specification language, which includes tuples and scalar types. You can also use Yices 2 as a library in your software.

CRFSuite is an implementation of Conditional Random Fields (CRFs) for

2014-10-29T23:13:21Z

labeling sequential data. The first priority of this software is to train and use CRF models as fast as possible even at the expense of its memory space and code generality. CRFsuite runs 5.4 - 61.8 times faster than C++ implementations for training. CRFsuite supports parameter estimation with L1 regularization (Laplacian prior) using Orthant-Wise Limited-memory Quasi-Newton (OW-LQN) method and L2 regularization (Gaussian prior) using Limited-memory BFGS (L-BFGS) method.

This library is a C port of the implementation of Limited-memory

2014-10-29T23:10:29Z

Broyden-Fletcher-Goldfarb-Shanno (L-BFGS) method written by Jorge Nocedal. The original FORTRAN source code is available at: http://www.ece.northwestern.edu/~nocedal/lbfgs.html

LibShortText is an open source tool for short-text classification and

2014-10-29T17:06:40Z

analysis. It can handle the classification of, for example, titles, questions, sentences, and short messages. Main features of LibShortText include * It is more efficient than general text-mining packages. On a typical computer, processing and training 10 million short texts takes only around half an hour. * The fast training and testing is built upon the linear classifier * LIBLINEAR * Default options often work well without tedious tuning. * An interactive tool for error analysis is included. Based on the property that each short text contains few words, LibShortText provides details in predicting each text.

Add liblinear.

2014-10-19T09:57:21Z

LIBLINEAR is a linear classifier for data with millions of instances and features. It supports L2-regularized classifiers L2-loss linear SVM, L1-loss linear SVM, and logistic regression (LR) L1-regularized classifiers (after version 1.4) L2-loss linear SVM and logistic regression (LR) L2-regularized support vector regression (after version 1.9) L2-loss linear SVR and L1-loss linear SVR. Main features of LIBLINEAR include Same data format as LIBSVM, our general-purpose SVM solver, and also similar usage Multi-class classification: 1) one-vs-the rest, 2) Crammer & Singer Cross validation for model selection Probability estimates (logistic regression only) Weights for unbalanced data MATLAB/Octave, Java, Python, Ruby interfaces

Import IPOPT version 3.11.5 as math/ipopt

2013-11-14T15:04:12Z

Ipopt (Interior Point OPTimizer, pronounced eye-pea-Opt) is a software package for large-scale nonlinear optimization. It is designed to find (local) solutions of mathematical optimization problems of the form min_{x in R^n} f(x) s.t. g_L <= g(x) <= g_U x_L <= x <= x_U where f(x): R^n --> R is the objective function, and g(x): R^n --> R^m are the constraint functions. The vectors g_L and g_U denote the lower and upper bounds on the constraints, and the vectors x_L and x_U are the bounds on the variables x. The functions f(x) and g(x) can be nonlinear and nonconvex, but should be twice continuously differentiable. Note that equality constraints can be formulated in the above formulation by setting the corresponding components of g_L and g_U to the same value. Ipopt is part of the COIN-OR Initiative.

Import MiniSat version 2.2.0 as math/minisat.

2013-10-28T04:15:11Z

MiniSat is a minimalistic, industrial strength, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.

Import libint-2.0.0 as math/libint

2013-03-08T07:09:04Z

Libint is two things: 1. a library of C/C++ functions for efficient evaluation of several kinds of two-body molecular integrals over Gaussian functions; 2. the optimizing compiler that generates a Libint library. In molecular electronic structure theory Gaussian basis sets are standard because they allow efficient evaluation of matrix elements of operators (molecular integrals). Modern electronic structure programs spend considerable portion of their runtime computing the Coulomb two-electron integrals. While anyone can compute Gaussian integrals using simple formulas, the efficient evaluation of many-body can be (relatively) complicated. Libint is an open library that anyone can use to compute a variety of two-electron integrals, most importantly the Coulomb two-electron integrals and their arbitrary-order geometric derivatives, over Gaussians of arbitrary angular momentum. Among other notable features is the support for the nonstandard two-electron integrals that appear in explicitly correlated R12 methods.

Initial import of py-munkres-1.0.5.4:

2012-05-30T11:05:30Z

The Munkres module provides an implementation of the Munkres algorithm (also called the Hungarian algorithm or the Kuhn-Munkres algorithm), useful for solving the Assignment Problem. Assignment Problem: Let C be an nxn matrix representing the costs of each of n workers to perform any of n jobs. The assignment problem is to assign jobs to workers in a way that minimizes the total cost. Since each worker can perform only one job and each job can be assigned to only one worker the assignments represent an independent set of the matrix C.

Import ARPACK 96 as math/arpack.

2012-05-29T16:38:01Z

Contributed to pkgsrc-wip by Jason Bacon. ARPACK is a collection of Fortran77 subroutines designed to solve large scale eigenvalue problems. The package is designed to compute a few eigenvalues and corresponding eigenvectors of a general n by n matrix A. It is most appropriate for large sparse or structured matrices A where structured means that a matrix-vector product w <- Av requires order n rather than the usual order n**2 floating point operations. This software is based upon an algorithmic variant of the Arnoldi process called the Implicitly Restarted Arnoldi Method (IRAM). When the matrix A is symmetric it reduces to a variant of the Lanczos process called the Implicitly Restarted Lanczos Method (IRLM). These variants may be viewed as a synthesis of the Arnoldi/Lanczos process with the Implicitly Shifted QR technique that is suitable for large scale problems. For many standard problems, a matrix factorization is not required. Only the action of the matrix on a vector is needed. ARPACK software is capable of solving large scale symmetric, nonsymmetric, and generalized eigenproblems from significant application areas. The software is designed to compute a few (k) eigenvalues with user specified features such as those of largest real part or largest magnitude. Storage requirements are on the order of n*k locations. No auxiliary storage is required. A set of Schur basis vectors for the desired k-dimensional eigen-space is computed which is numerically orthogonal to working precision. Numerically accurate eigenvectors are available on request. Important Features: o Reverse Communication Interface. o Single and Double Precision Real Arithmetic Versions for Symmetric, Non-symmetric, Standard or Generalized Problems. o Single and Double Precision Complex Arithmetic Versions for Standard or Generalized Problems. o Routines for Banded Matrices - Standard or Generalized Problems. o Routines for The Singular Value Decomposition. o Example driver routines that may be used as templates to implement numerous Shift-Invert strategies for all problem types, data types and precision.