The publications and research associated with this software is currently under review in the "Journal of Systems and Software". Nemo2 (Numbers, fEatures, MOdels, version 2) Nemo2 is a boolean and numerical constraint language and tool with first-class support for numerical feature modeling based in a collaboration between Universidad de Malaga and University of Texas in Austin. It is licensed under the MIT license. For Nemo version 1, we refer stakeholders to its repository: https://github.com/danieljmg/Nemo_tool At a glance Nemo2 support extending classic variability models with numerical features and arithmetic in the formats DIMACS and Universal Variability Language (UVL) Numerical Feature Models (NFMs) must be defined in Nemo2 by using Nemo's modeling language in a .txt file. Nemo2 transforms and optimize NFMs by means of Bit-Blasting into classic variability models which then are supported by any first-order logic reasoner. Nemo2 outputs support three formats: a) a UVL model, b) a propositional formula, and c) a Tseitin's Conjunctive Normal Form (CNF) propositional formula. Besides the transformed model, we make use of comment lines to identify each original feature name and domain (i.e., boolean or numerical) with their respectives bit-blasted features. Nemo2 is a cross-platform tool that have been developed in Python 3.11.x. Supported Definitions Feature types: boolean, natural and integers. Numerical definitions: constant, ranges and enumerated. Constraint operations: cross-tree constraints (equivalence, implication and negation), inequalities (e.g., greater or equal) and mathematical operators (e.g., multiplication). Modeling Language As one image is worth a thousand words, the following extended example shows most of the possibilities. def A bool 0 # 0 means new featuredef B bool f8 # named in adjunt FM as f8def C bool 0def D_unsigned [0:1]def E_unsigned [0:3]def F_signed [-1:1]def G_enum_signed [-9, -3, 0, 3]def H_constant [-2]ct C -> Bct A -> (G = 0)ct A or Bct (G_enum_signed*H_constant) ≤ E_unsigned Real world models pre and post transformation, as well as the proper Nemo2 inputs, are to be found in their respective folders in this github page. Installation Nemo has been tested in Python 3.11 x86_64 at the moment, with up-to-date libraries (pycosat, files, re and z3py modules must be installed). To install pycosat in windows: Install Microsoft Build Tools for Visual Studio 16 Select: Workloads → C++ build tools. Select only "Windows 10 SDK" (assuming the computer is Windows 10). To use MSVC cl.exe C / C++ compiler from the command line, additionally select the C++ build tools. pip install pycosat To simply install Z3py: pip install z3-solver Now you can pull/download and run Nemo. Usage Run main.py You will be asked: Do you want to run the model in the Z3 SMT solver (y)? Answer y to run the model in the Z3 SMT solver. The enumerated generated solutions are written in the smtsolutions.txt file. Do you want to transform the model into UVL (uvl), classic PF (pf), or Tseitin DIMACS (td)? The three options bit-blast the mode. Answer uvl to transform it into a UVL with .uvl extension. Answer pf to transform it into a classic proposional formula with .txt extension. Answer td to transform it into a Tseitin's CNF proposional formula with .dimacs extension. Which is the model .txt to transform? You must write the path/name of the .txt file. If in the same folder, just the name is necessary. If you are extending a DIMACS model, please write its name, BLANK otherwise. You must write the path/name of the .dimacs file to evolve. If in the same folder, just the name is necessary. If you are not evolving, press Enter. The transformed model is available in the transformedmodel.{uvl/txt/dimacs} file. At all cases, in the terminal are presented: Runtimes in seconds. Calculated Defined features following the (Name, Adjusted_width, Type) format. Calculated Adjusted constraints of the model. Test The next tiny example is the definition of A + B >= C of 2-bits variables. def A [0:3]def B [0:3]def C [0:3]ct A + B >= c It must produce 54 different valid solutions. Contact Author and Code Management Daniel-Jesus Munoz: ITIS, CAOSD, Dpt. LCC, Universidad de Málaga, Andalucía Tech, Spain Other Tool Authors Mónica Pinto: ITIS, CAOSD, Dpt. LCC, Universidad de Málaga, Andalucía Tech, Spain Lidia Fuentes: ITIS, CAOSD, Dpt. LCC, Universidad de Málaga, Andalucía Tech, Spain Publication Supporters Don Batory: Department of Computer Science Austin, Texas, USA Credits Besides common Python modules, Nemo makes use of the tactics functionality of Z3py, as means to base its transformations in a solid library. Tactics is a side functionality, do not confuse it with the Z3 SMT solver. Additional corrections and pre-processing optimizations are encoded aside the library; any Z3py modification had occurred and all credits and issues are referred to its github page.

Munoz, Pinto and Fuentes work is supported by the European Union's H2020 research and innovation programme under grant agreement DAEMON 101017109, by the projects co-financed by FEDER funds LEIA UMA18-FEDERJA-15, IRIS PID2021-122812OB-I00 (MCI/AEI), and the PRE2019-087496 grant from the Ministerio de Ciencia e Innovación. Batory is retired, writing free textbooks \cite{BatoryText}, and is walking dogs for wages.