Amira J Zaylaa
email: amira.zaylaa@ul.edu.lb

Mohamad Rashid

Mounir Shaib

Imad El Mazjoub

Imad El

A Handy Preterm Infant Incubator For Providing Intensive Care: Simulation, 3D Printed Prototype and Evaluation

Keywords: Preterm Infant, Handy Preterm Incubator, Intensive Care Methods, Simulation, 3D Printing, Feature Extraction, Emergency Control, Evaluation. Highlights preterm infant incubator;

Preterm infants encounter an abrupt delivery before their complete maturity, during the third trimester of pregnancy. Polls anticipate an increase in the rates of preterm infants for 2025, especially in middle and low income countries. Despite the abundance of intensive care methods for preterm infants, such as but not limited to commercial, transport, embrace warmer, radiant warmer and Kangaroo Mother Care methods, they are either expensive, lack the most essential requirements or specifications, or lack the maternal-preterm bond. This drove us to carry this original research and innovative idea of developing a new 3D printed prototype of a Handy preterm infant incubator. We aim to provide the most indispensable intensive care with the lowest cost. Through bestowing the low income countries with the Handy incubator's care to preserve the maternal-preterm's bond, and diminish the rate of mortality. Warmth, power supply and biomedical features were provided. Bio-compatible and isolating materials were utilized. Simulation results showed the best fit for the Handy incubator's components. Real and experimental results showed the 3D printed prototype, and the time elapsed to obtain it. Evaluation results revealed that the overall performance of the explored specifications of Kangaroo Mother Care was 75%, and the embrace warmer was 66.7±1.5%. However, our Handy incubator surpassed all the intensive care methods, with an overall performance of 91.7±1.6%. Thereby supporting its advantage and cost-effectiveness

Introduction

Preterm delivery is the abrupt occurrence of birth at less than 37 th week of pregnancy.

During the third trimester, i.e. 27-40 weeks of pregnancy when the major fetal development stage occurs, the infant undergoes a dramatic transfusion in their respiratory system which enables them to breathe for the first time. After the third trimester, the fetus is usually set to birth [START_REF] Brewer | The Pregnant Body Book[END_REF]. According to the World Health Organization (WHO) epidemiology, in every 10 new born infants, 1 infant is considered a preterm infant [START_REF] Johnson | Global, regional, and national causes of child mortality in 2000-2010[END_REF]. Fifteen million preterm infants were born in 2010. Of all the 15 million, 1 million infant died due to prematurity. The preterm deliveries were then ranked as the first cause of mortality of preterm infants, during the first month of birth and after birth. It is also globally ranked as the second cause of death for children who did not complete their 5 years [START_REF] Johnson | Global, regional, and national causes of child mortality in 2000-2010[END_REF].

Later, a study revealed that preterm birth rates decreased from 2007 to 2014, due to the decreased number of births by teens and young mothers [START_REF] Ferré | Effects of maternal age and age-specific preterm birth rates on overall preterm birth rates-united states, 2007 and 2014[END_REF]. They also reported a slight increase in the national preterm birth rate between 2014 and 2015 [START_REF]Preterm birth maternal and infant health[END_REF]. In almost all countries with reliable data, preterm birth rates are continuously increasing. Blencowe et al. systematic analysis showed a continuous increase in the rate of surviving preterm infants in most of the countries. The average annual rate of change from 2005 to 2010 was maintained to 8%, but still equivalent to 92% preterm death.

In high-income countries, almost all of these reported preterm infants survive. In lowincome settings, half of the babies born at 32 weeks or less die due to a lack of feasible, cost-effective care, such as lack in warmth, breastfeeding support and infection control, as well as the existence of breathing difficulties.

Regardless of the reasons of prematurity, many studies have focused on monitoring the maternal and fetal conditions to reduce and predict the symptoms, and thus avoid preterm deliveries [START_REF] Oudjemia | Coarse-grained multifractality analysis based on structure function measurements to discriminate healthy from distressed foetuses[END_REF][START_REF] Oudjemia | Delta-fuzzy similarity entropy to discriminate healthy from sick fetus[END_REF][START_REF] Zaylaa | Analysis and extraction of complexity parameters of biomedical signals[END_REF][START_REF] Zaylaa | Reducing sojourn points from recurrence plots to improve transition detection: Application to fetal heart rate transitions[END_REF][START_REF] Zaylaa | Unbiased recurrence plot quantification of chaotic dynamic systems by eliminating sojourn points[END_REF][START_REF] Zaylaa | n-order and maximum fuzzy similarity entropy for discrimination of signals of different complexity: Application to fetal heart rate signals[END_REF][START_REF] Zaylaa | Advanced discrimination between healthy and intrauterine growth restricted fetuses by unbiased recurrence plots[END_REF][START_REF] Zaylaa | Cascade of nonlinear entropy and statistics to discriminate fetal heart rates[END_REF]. While others focus on treating the outcome, i.e. prematurity, and directly reduce the mortality [START_REF] Goldenberg | The preterm birth syndrome: issues to consider in creating a classification system[END_REF][START_REF] Plunkett | Genetic contributions to preterm birth: implications from epidemiological and genetic association studies[END_REF][START_REF] Goldenberg | Epidemiology and causes of preterm birth[END_REF][START_REF] Gravett | Global report on preterm birth and stillbirth (2 of 7): discovery science[END_REF].

In order to treat the outcome, intensive care methods existed, such as those available in the market and utilized in research. They vary according to their design, specifications, performances. They include, but not limited to commercial incubators, transportable incubator, embrace warmer, radiant warmer and Kangaroo Mother Care (KMC) methods [START_REF] Ludington-Hoe | Breast and infant temperatures with twins during shared kangaroo care[END_REF][START_REF]on Environmental Hazards, Infant radiant warmers[END_REF][START_REF] Nimbalkar | Usage of embracetm in gujarat, india: Survey of paediatricians[END_REF]. However many drawbacks were associated with the existing intensive care techniques.

Despite the presence of intensive care methods, a study predicted the rate of surviving preterm infants for 2025 to be 9% [START_REF] Blencowe | National, regional, and worldwide estimates of preterm birth rates in the year 2010 with time trends since 1990 for selected countries: a systematic analysis and implications[END_REF]. As the global anticipated rate of preterm infant's mortality for 2025 is 91%, this drove us to tackle this problem and develop a new preterm incubator prototype to promote the intensive care with a low cost. The aim of our study is to develop and 3D print a new handy, portable and cost-effective Liquid Crystal Display (LCD)-based incubator for providing intensive care, especially in middle and low income countries. The objective is to make the Handy incubator feasible, patient friendly and meet the health requirements for preterm infants. The project focuses on the preterm infants abruptly delivered in the third trimester of pregnancy. The major vital signs including the temperature, heart rates (HRs) and the level of oxygen were monitored and advanced bio-compatible materials were carefully chosen for treating the preterm infant.

The remainder of this paper is organized as follows. In section 2, we provide the existing intensive care methods. In section 3 we introduce the Handy preterm incubator's materials.

In section 4, we set out the Handy preterm incubator's prototype. In section 5 we present the results. In section 6 we discuss the results, and in section 7 we provide a general conclusion and future work.

Preterm Infant Intensive Care Methods Existing

After searching pubmed, sciencedirect and google scholar, we summarized the literature review results and we divided them into two categories; open care and closed care. Open care is divided into two available techniques, the KMC and the radiant warmer, and the available research technique, Embrace Warmer.

Closed Care Methods

These methods include the infant incubators available in the Neonate Intensive Care Unit (NICU), it is an intensive care system that supplies the infant with warmth, in a steady stable way, through a heated air circulation over the skin. After several advancements, the infant incubator comprised humidity control, oxygen supply and other accessories. The infant incubator could be fixed, mobile or transportable [START_REF]Incubator and radiant warmer phototherapy unit[END_REF]. However, incubators lack the maternal-preterm bond, and are expensive especially in middle and low income countries. This triggered other studies to develop portable, cheaper, and feasible systems used at home [START_REF] Blennow | Noise levels in infant incubators (adverse effects?)[END_REF][START_REF] Bonner | there were more wires than him': the potential for wireless patient monitoring in neonatal intensive care[END_REF][START_REF] Maastrup | Breastfeeding progression in preterm infants is influenced by factors in infants, mothers and clinical practice: the results of a national cohort study with high breastfeeding initiation rates[END_REF].

The fixed infant incubator commonly used in NICU, due to the presence of a variety of accessories, is capable of treating any case. Fixed incubator is seen as perfect choice since it is connected to wall supplies, and provides suitable environment for the infant. Nevertheless, fixed incubators are extremely expensive and have the same concept of producing warmth by pushing heated air through fans. This technique produces noise, which affects negatively the infant [START_REF] Blennow | Noise levels in infant incubators (adverse effects?)[END_REF]. Although such incubator records HRs, it uses electrodes that have to be connected to the preterm infant all the time. Thereby, affecting the skin of the infant since its fragile [START_REF] Bonner | there were more wires than him': the potential for wireless patient monitoring in neonatal intensive care[END_REF]. Moreover, lacks breast feeding [START_REF] Maastrup | Breastfeeding progression in preterm infants is influenced by factors in infants, mothers and clinical practice: the results of a national cohort study with high breastfeeding initiation rates[END_REF] and lacks mobility which makes it extremely hard for the infant to pass from one department to another, a reason that led to the mobile incubator invention [START_REF] Ecri | HPCS Infant Incubator[END_REF][START_REF] Terrell | Handhole for infant incubator[END_REF].

Mobile incubator is a modified fixed incubator which has the same function as the fixed incubator. Mobile incubators have additional wheels, could be transported inside the hospital, merely, and requires extra tools to supply the system with electricity and oxygen [START_REF] Ecri | HPCS Infant Incubator[END_REF].

These incubators have the same drawbacks as fixed incubators. Although, mobile incubators are great solutions when the infant needs to be transported inside the hospital, they are inpractical when the infant needs to be transported outside the hospital. For this purpose transport incubators showed up [START_REF] Blennow | Noise levels in infant incubators (adverse effects?)[END_REF][START_REF] Bonner | there were more wires than him': the potential for wireless patient monitoring in neonatal intensive care[END_REF][START_REF] Maastrup | Breastfeeding progression in preterm infants is influenced by factors in infants, mothers and clinical practice: the results of a national cohort study with high breastfeeding initiation rates[END_REF].

Transport incubators are small sized portable incubators which can transport the infant using the car or airplane. Despite the fact that transport incubators are the only option for outdoor premature infant transport, transport incubators have several drawbacks, such as the extreme high cost and heaviness, thermostat failure and electrical shock hazards [START_REF] Lemburg | Transport incubator[END_REF].

Open Care Methods

KMC is a solution for the defects of preterm incubators, which yields to high disease rates and mortality of preterm infants in hospitals. It provides warmth and breastfeeding by infant-maternal skin contact. This bond/contact ensures the stability of the preterm's temperature. Although KMC was capable of reducing the infants' morbidity compared to conventional incubators [START_REF] Corner | Kangaroo mother care saving premature infant's life[END_REF], it is still restricted to different factors. KMC is not capable of monitoring the infant's temperature, HR, oxygen level, humidity, which subject the infant to a risk of instability and harmfulness. KMC needs skillful human resources like nurses, which add complexity to the intensive care.

Another open intensive care method is the Radiant warmer which functions according to the laws of radiant heat. This device provides the preterm with the necessary radiant energy as alternative process for conventional convection heating [START_REF] Bell | Infant incubators and radiant warmers[END_REF]. Radiant warmer comprises a bed, an overhead heating unit and a temperature sensor [START_REF] Bell | Infant incubators and radiant warmers[END_REF]. Radiant warmers suffer from a dramatic increase in the heat loss due to the evaporation [START_REF] Oh | Phototherapy and insensible water loss in the newborn infant[END_REF][START_REF] Bell | The effects of thermal environment on heat balance and insensible water loss in low-birth-weight infants[END_REF].

Embrace Warmers, made up of three parts: a baby estimated sleeping bag or infant interface, a compartment of phase change material and a warmer [START_REF] Chen | Embrace designed for extreme affordability[END_REF], are great solutions for regulating premature infant's body temperature. Meanwhile, Embrace warmers do not provide any monitoring for the infant's essential parameters, and lacks emergency alarms. Also, it requires continuous phase change which causes fluctuation in the infant's temperature and omits any therapeutic support.

All the aforementioned problems led us to develop the new Handy preterm infant incubator.

Handy Preterm Infant Incubator's Materials

The novel Handy incubator required several materials and tools, due to the diverse contributions that were embedded in it.

At the third trimester, the fetus is almost formed and ready for birth [START_REF] Brewer | The Pregnant Body Book[END_REF][START_REF] Oh | Phototherapy and insensible water loss in the newborn infant[END_REF]. Thereby, the average size, weight, height, head circumferences and abdominal circumferences of a premature infant [START_REF]Premature and newborn size chart, Touching Little Lives[END_REF] were carefully chosen. Noteworthy, during the last three months of pregnancy, the infant brain remains to expand so the head circumference increases from around 11 in (28 cm) to 15 in (38 cm). At the same time, the fetus total body length rises roughly from 15 in (38 cm) to 19 in (48 cm). The fetus average weight rises from 3lb (1.4 kg) to 7.5lb (3.4 kg) [START_REF]Premature and newborn size chart, Touching Little Lives[END_REF].

Electric and Electronic Components

The Handy incubator required several components, the Atmega328 microcontroller [START_REF] Barrett | Arduino microcontroller processing for everyone![END_REF] to launch and store the data.

The Arduino micro was used to assist the microcontroller, as the microcontroller required an overwhelming setup circuits and assembly language. Arduino micro assists the microcontroller with regulators, with a framework of free libraries and others. The framework provides easier programming, avoids losing time on low-level programming language and register addresses [START_REF] Senthil | Microprocessors and Microcontrollers[END_REF].

The Atmega328 soldered with push button to reset, some LED to show data transitions and reception, and pins labeled with the corresponding pin on Atmega328. Its rear part allows the communication with USB and regulator Integrated Chip (IC) to provide stable voltage to the Atmega328. Also, the oximeter MAX30100 was also utilized. It is an optical sensor which carries the Maxim's integrated pulse oximeter and HR sensor. Regulator, thermometer and mikroBUS'"Inter-integrated Communication (I2C) IC were impeded on the rear to provide a 3.3 V supply, measure the temperature and provide a serial communication.

Ultra fire batteries were 18650 Li-ion 3.7 V rechargeable batteries with 9800 mAh capacity [START_REF] Buchmann | Whats the best battery[END_REF]. By referring to Eq. 1, the energy stored was 36.26 Wh. Thereby, a set of 4 batteries has been used to achieve 9800 mAh, increase the voltage to 15 V, and obtain a stored energy of 147 Wh.

E = V × C, (1)

Biocompatible Materials and 3D Printer

Three major biocompatible materials were utilized in our Handy incubator, the silnylon, mylar sheets and bamboo fabric. Silnylon was utilized as an outer layer due to its ultralight weight, windproof, and capability to isolate the system and the infant from the outer environment [START_REF] Outdoors | Working with silnylon[END_REF]. The mylar sheet, was used due to its high tensile strength, chemical and dimensional stability, transparency, reflectivity, gas and aroma barrier properties, and electrical insulation [START_REF] Demeuse | Biaxial stretching of film: Principles and applications[END_REF]. The bamboo fabric, was utilized due to its antibacterial property, smoothness, breathable property and great absorbent of water [START_REF] Teli | Antibacterial and acid and cationic dyeable bamboo cellulose (rayon) fabric on grafting[END_REF]. The ZONESTAR 3D

printer was used to establish our Handy incubator due to its several parameters:

• Frame structure materials including, printing speed (40-100 mm/s), maximum printable size (220x220x220 mm) and nozzle size (0.4 mm);

• Printing materials supports: Poly-Lactic Acid (PLA) and others, with a diameter including positioning accuracy in X & Y (0.01 mm) and in Z (0.00025 mm);

• Hot bed power: 12V 140W;

• Printing software: Cura, Repetier-Host Kisslicer, etc., and operating system in Windows, Linux and Mac;

• Melting Temperature: 157-170°C, tensile strength: 61-66 MPa, and flexural strength:

48-110 MPa.

Moreover, another advantage of the ZONESTAR 3D printer is the fact that it is based on the Fused Deposition Modeling (FDM) printer, which is common, cost-effective, provides a customized geometry and higher performance [START_REF] Hoy | 3d printing: making things at the library[END_REF].

Heat Transfer Components

Two major heat transfer components were embedded in our Handy incubator, the cartridge heater riprap and hot/cold packs. The cartridge heater riprap was the first source of heart energy, which converts electrical energy stored in the batteries into thermal energy, which is in tern stored and transferred to the infant. Cartridge heaters are made from stainless steel and powered with 12 V DC with a power of 40 Watts. The heating probe has cylindrical shape of 6 mm diameter, and 20 mm length. This small probe was chosen to ensure that all the thermal energy is transferred to the gel sack. The second component, the hot/cold pack which is a chemical wax that conserves thermal energy and transfer it to the patient via conductance.

Handy Preterm Infant Incubator's Prototype

The novel steps for obtaining the prototype of the Handy incubator and the testing steps are provided.

[Figure 1 about here.]

Prototype's Implementation Steps

The steps are divided into two major parts, the real and simulated prototype steps part, and the real prototype testing steps part. The block diagram showcased in Fig. 1 represents our incubator's real prototype steps. After the preterm infant is placed in the novel incubator, three vital signs and features, HR, temperature and SpO 2 , were continuously monitored (diagnosed) through the microcontroller. Monitored parameters were then displayed on the handy incubator's LCD. And the power source of the system followed a Battery Management System (BMS).

At any drop out of the normal range of either the oxygen level or the temperature of the preterm, a buzzer is turned on for an emergency interference (therapy), such as releasing oxygen or turning heaters on. This system is supported by a battery management system which ensures the mobility of our novel incubator. The simulated steps start by drawing, via Autocad, all the required parts present in the block diagram in Fig. 1, according to the aforementioned size and the weight of the preterm infant. In order to design a compact incubator that ensures breastfeeding and can be held by hand (Handy).

Following the simulation steps, the real prototype steps can be reproduced as follows:

• Program the microcontroller to communicate with the sensors and other parts.

• Integrate MAX30100 to ensure the reading from infant leg.

• Monitor HR, SpO 2 biological features noninvasively, by MAX30100. MAX30100 measures the absorption of two different wavelengths of light, it measures the absorbency of pulsed blood, by measuring red and infrared waves reflected from hemoglobin (HbO 2 )

and deoxy-hemoglobin (Hb). The different intensities are due to their different absorption coefficients.

• Measure the temperature via MAX30100, as it contains a built-in temperature sensor on its chip;

• Process the signal by a low noise analog signal processing unit;

• Choose the size of the novel prototype to be compatible with the size of a third trimester infant [START_REF]Premature and newborn size chart, Touching Little Lives[END_REF];

• Prepare the mylar fabric, cut it according to the dimensions, glue the mylar layer on both sides of a cardboard and mount the silinylon on the top of the mylar;

• Sew the mylar and silinylon to attach them to our handy incubator.

• Use several sacks of the heating unit, each heating unit comprises a pack of 5 identical sack gels to ensure a uniform heat distribution. Each sack has its own heater and thermistor to regulate the temperature.

• Control the heaters and the temperature reading of each sack by the microcontroller.

Such that, when the temperature decreases under a specific threshold, the microcontroller orders the heater to turn ON in the low temperature sack.

• For safety, allow the manual control of the temperature by turning ON/OFF the heaters using push buttons on the LCD, in case of an error in the temperature reading or autocontrol of the temperature.

• Design the novel incubator's circuit (PCB) using EAGLE. EAGLE board design assigns our preferable dimension of the circuit's components in a compact way, traces the connections of these components through copper, and transforms our idealized design into a precise, real dimension and routed PCB.

• Use the ZONESTAR 3D printer to build the Handy incubator's parts. The printer releases beads of heated thermoplastic by the nozzle while it moves, hence building the designed parts in thin layers. Such printing process is gradually repeated over and over, permitting precise control of the location and the amount of each bead deposit to form each layer. By then, as each layer of the thermoplastic cools, it hardens, gradually building up the Handy incubator's parts as the layers are completely formed. To achieve this point the following three steps are needed:

Step One: Design the novel incubator parts in 3D modeling software.

-Illustrate the 3D model parts of the novel incubator on AutoCAD, a 3D modeling software;

-Taking into consideration every dimension precisely;

Step Two: Import your 3D model file to a printing software.

-Export the AutoCad file in an Standard Triangle Language (.STL) file format so Cura can understand it.

-Cura slices the model, offering us the chance to preview, scale and adjust its settings.

Step Three: 3D print the model on your 3D Printer.

-Finally, save the slices on a Secure Digital (SD) memory card, which is inserted into the ZONESTAR 3D printer machine, and ready for print.

• Develop the circuit by adding copper layers, then sandwich the double layer copper board with the layer image.

• Use an Ultraviolet (UV) source to burn the epoxy and clone the circuit on the board;

• Drill the holes and solder the parts and connectors;

• Design the user interface to show an LCD and four push buttons, and display the extracted features and the battery state;

• In case of emergency, associate a beep or alarm when the level of oxygen diminishes;

• Connect a set of 4 rechargeable Li-ion batteries in series, to obtain 15 V battery of 9600 mAh capacity, and charge the batteries with 15 V charger when needed.

• Estimate the duration of turning ON the 40 W power heater. Eq. 2 shows that the 147 W power can drive 40 W power heater more than 3 hours and 40 minutes, continuously.

t = E P . (2)
• For electric safety, connect the batteries using a special port, and control the batteries with a BMS to avoid over charge or over discharge.

Handy Preterm Infant Incubator's Prototype Testing Steps

As we were keen on monitoring the infants' HRs, we chose MAX30100. By measuring the intensity of Hb and HbO 2 in blood, we calculated the oxygen saturation (SO 2 ). SO 2 commonly referred to as "sats", measures the percentage of HbO 2 binding sites in the bloodstream which is enriched with oxygen [START_REF] Schnapp | Pulse oximetry: uses and abuses[END_REF]. The HR was calculated by calculating the number of beats per minute (bpm). The heart pumps blood via pulsing, this leads to high intensity of cells on the head of each pulse, then the pulse is detected by detecting a high number of cells. The high intensity in the head of a pulse leads to high reflection, which decreases as the intensity decreases forming pulses.

These pulses can be caught by establishing a threshold, when the infrared light (reflected signal) exceeds this threshold, the beat is counted. This was tested in the laboratory on a normal man.

The heaters were tested on water, and the temperature sensors were tested on the heated and cooled water. Finally, the batteries capacity were tested using a voltmeter.

Results

Handy Preterm Infant Incubator's Results

After applying all the implementation steps in section 3, we present the simulated and 3D printed (real) prototype results of our Handy incubator, in addition to the testing and evaluation results.

Simulated Prototype

The simulated prototype of the real dimensions of the Handy incubator are showcased in Fig. 2 (a) from a side view, and Fig. 2 (b) top view in centimeters (cm). A plastic shield, gel pack and the infant are colored green, red, and yellow, respectively. The total length of the Handy incubator is 61.23 cm and the length of the box is 8 cm (included within the 61.23 cm). The plastic shield thickness is 0.5 cm, and the mylar and bamboo layers are 0.55 mm each. The thickness of the gel pack is 2 cm. The blue, green, red and yellow colors in Fig. 2 (b) represent the outer layer, plastic shield, gel pack and the infant, respectively. The outer layer surrounds the infant, thereby it contains a hall of radius 10 cm and three small rectangles. The purpose of the hall was to give the infant the space to inhale oxygen from the environment and ensure breastfeeding. The three small rectangular fabrics, were used to hold the two ends of the fabric.

[Figure 2 about here.]

The closed simulation of the Handy incubator is represented in Fig. 2 (c), where the infant (colored in yellow), is placed inside and surrounded by the outer layer (colored in blue). The green rectangle and four circles on top of the box are the LCD displays and push buttons. Fig. 2 (d) showcases the overall size of the simulated Handy incubator while the mother is holding it by hands.

[Figure 3 about here.]

The novel incubator's simulated the base part is showcased in Fig. 3 Moreover, the box contains two large holes for oxygen bottle fixation, a hole for the power source deluge, and On/Off switch. In addition to a gear handle that fixes the gear in its place using screws. Fig. 3 (b) provides the simulation of all the parts required to form our novel incubator. The plastic shield forms the skeleton of our handy incubator (its total length is around 62 cm). The plastic shield was decomposed into four parts connected with screws and nuts. Fig. 3 (c) shows the simulation of the warming unit, the red object is the package that represents the gel sacks and the blue object is the fabric surrounding the preterm. The gel package comprises 5 sacks; each sack is composed of a gel, in addition to a heater and thermometer to control the generated heat.

[Figure 4 about here.]

The oxygen release part, shown in Fig. 3 (d), was simulated to be above the infant's face, by means of a tube-like mechanical valve, a stepper motor with a gear and an oxygen bottle.

The oxygen source is colored in brown, and the oxygen bottle was simulated inside the box.

Noteworthy, the oxygen transmission tubes are embedded inside the plastic shield, to avoid any crash from the external mechanical load.

Preliminary 3D Printed Prototype

3D printing was the second step towards obtaining the real prototype parts. AutoCAD files were imported to the 3D printer by the means of a memory card to print out the parts.

The model and printing duration are reported in Fig. 4. The hamlet took ∼20 hours. The box label took ∼17 hours and 40 minutes, the cover of the box took ∼20 hours and the two shields 20 hours. The total duration to get all the parts printed was 66 hours and 40 minutes.

The fabric layers sewing, assembly and circuitry were illustrated in Fig. 5 (a) and (b).

[Figure 5 about here.]

The PCB process is represented in Fig. 5 for testing the warming system components.

[Figure 6 about here.]

The overall real prototype of the Handy incubator is shown in Fig. 6 closed form. The blue color of fabric is the color of the silnaylon that is the outer layer. At the boundaries of the infant circumscribe's fabric there are stick tags that provide easy opening and closing of the system. Also the Bamboo fabric is attached to the infant circumscribe fabric using stick tags, thus the bamboo fabric can easily be removed, cleaned and re-installed.

Handy Preterm Infant Incubator's Testing Results

After presenting both the hardware parts of the handy preterm infant incubator, we present the testing and debugging processes. The (i) electric testing results for the batteries that are intended to supply the system, the (ii) thermal energy released and the warming system and (ii) the infrared testing. Also, the evaluation and management of the handy preterm incubator's specifications and cost are provided and compared to the existing intensive care methods.

Electrical testing of the capacity of batteries was obtained by fully charging the battery (until the battery voltage became 4.2 V), producing a simple circuit that needs specific current (known as the testing current), and measuring the time needed to completely discharge (until the battery voltage became 2.5 V), which was the capacity.

The test was repeated on Ultra Fire TR 18650 5 Ah 3.7 V with the testing currents I∈ {0.2, 0.5, 1, 2, 3, 5A} the results obtained are 1.124, 1.123, 1.095, 1.052, 0.955, and 0.626, respectively and the capacity was not enough. For that, we used two sets of series batteries connected in parallel instead of a single set, to achieve an energy of 23.853 KJ. This energy was capable of heating the system one time, and can maintain the warmth for about 16 hours.

The results of both the warming system embedded in the Handy incubator, and the thermal energy testing was provided in our previous publication [START_REF] Shaib | Advanced portable preterm baby incubator[END_REF].

[Figure 7 about here.]

Pertaining to the insulation, the incubator's fabric and biocompatible materials provided a good insulation.

Infrared testing included MAX30100, the results were compared to those of oximetry sensors used in mobile phones, a medical equipment specialist for monitoring SpO 2 , and HRs using oximetry sensors. MAX30100 results were reliable and closer to the medical equipment than to the mobile sensor.

Handy Preterm Infant Incubator Evaluation Versus Preterm Infant Intensive Care Methods

Evaluation of our Handy incubator included comparing it with peer intensive care methods. Three bar graphs of several crucial factors with the standard deviations imposed on the bar graphs were plot and shown in Fig. 7 and Fig. 8. These specifications are the price, environment, measurements, mother bond, prototype, mobility, and other factors. Each specification was associated a color in each bar graph, from light green to a dark green color.

The Handy incubator was compared to the commercial incubators, transport incubator, radiant warmer, embrace warmer and our Handy incubator is provided in Fig. 7. The variation of the type of monitored features or measurements recorded for instance, are represented by a bar graph in Fig. 7 (a) relative to the intensive care methods. The variation of the maternal-preterm infant bond and the variation of the mobility specifications or system mobility versus the intensive care methods are also reported. The variation of the therapeutic support, environment type of the system and the design model were evaluated and compared versus the intensive care methods in Fig. 7 (b).

The monitored features, evaluated in Fig. 7 (a), are the vital sign that each method can measure. A maximum value of 100% was associated with the maximum number of features extracted, and a null value of 0% was associated with the absence of any measured feature by the system. The highest number 100% of extracted features, including SpO 2 , humidity, HR and temperature were monitored using both the commercial and transport incubators.

Moreover, 75% of extracted features, including SpO 2 , HR and temperature were extracted by the Handy incubator, and null otherwise.

The maternal-preterm infant bond, evaluated in Fig. 7 (a), is the preterm infant contact with the mother. A maximum value of 100% (with a small standard deviation) was associated with the maximum maternal-preterm infant contact ensured by the system . A null value of 0% was associated with the absence of any contact between the infant and mother, i.e. when the infant is placed in a fully closed incubator in the NICU. The maternal-preterm infant bond exists fully 100% in KMC, the embrace warmer and our Handy incubator. It is totally absent in the commercial and transport incubators.

[Figure 8 about here.]

The system mobility, evaluated also in Fig. 7 (a), is the capability of mobilizing the intensive care system. A maximum value of 100% was associated with the maximum feasible mobility, and a null value of 0% was associated with a fixed method. The maximum performance of the system mobility was associated with KMC, embrace warmer and the Handy incubator.

incubators conserve a suitable temperature for the infant and monitor the basic parameter, but they differ in the weight, size, cost, and compatible accessories [START_REF]Infant incubator[END_REF]. The major advantage of a radiant warmer is the open access care it provides to preterm infants, which supports procedures like endotracheal intubation [START_REF] Gorski | Stages of behavioral organization in the high-risk neonate: theoretical and clinical considerations[END_REF][START_REF] Van Rooyen | The value of kangaroo mother care at kalafong hospital[END_REF]. This was in accordance with the 100% environment type performance of the radiant warmer observed in our work. However, the overall performance was 37.5±0.9% as reported in Table 1.

KMC is an open care technique, a recent review reported a 40% reduction in the risk of post-discharge mortality [START_REF]Hypothermia: Causes, symptoms, and treatment[END_REF]. Other benefits included increased breastfeeding, maternalinfant bonding and developmental outcomes [START_REF] Conde-Agudelo | Nifedipine in the management of preterm labor: a systematic review and metaanalysis[END_REF]. This was reflected in the 100% performance of KMC, when studying the presence/absence of the maternal-infant bond. The aforementioned findings and the endoresemt of WHO to KMC [START_REF] Dieterich | Breastfeeding and health outcomes for the mother-infant dyad[END_REF] support the good overall performance of KMC observed in our results (75±1.4%). The absence of the remaining 25% could be due to limiting the lower weight to 800g as suggested by Lawn et al. [START_REF] Lawn | Kangaroo mother care to prevent neonatal deaths due to preterm birth complications[END_REF].

Incubators are rather widely used, most units consist of two operating modes: the airtemperature manual control, and the skin-temperature automatic control [START_REF] Nobel | Infant incubators[END_REF]. Most units enable the user to measure the relative humidity [START_REF] Singh | Design and development of micro controller based temperature and humidity controller for infant incubator[END_REF], and provide support of oxygen to the infant when needed [START_REF] Nobel | Infant incubators[END_REF]. These facts were in agreement with our findings, were the commercial incubator was associated a 100% performance in feature extraction and therapeutic support, with an almost negligible standard deviation.

Regarding the handy incubator prototype information, Fallon involved the use of the cardiopulmonary machine to monitor and display data on an LCD screen [START_REF] Zaichkin | Newborn Intensive Care: What Every Parent Needs to Know[END_REF]. If the infant's HR becomes too slow or too fast, it gives an alarm [START_REF] Zaichkin | Newborn Intensive Care: What Every Parent Needs to Know[END_REF]. Analogous to the work of Fallon, we programmed our Handy incubator to give an alarm when there is a drop in the features extracted.

Recently, scientists in Baby Center published [START_REF]Equipment used to care for babies in the NICU[END_REF] a blood pressure monitor by connecting a miniaturized blood pressure cuff around the infant's leg or arm in order to monitor the blood pressure [START_REF]Equipment used to care for babies in the NICU[END_REF]. Analogous to their work, we used an oximetry and connected the miniaturized blood pressure cuff to the infant's leg.

Our handy incubator can be easily carried by the mother and affordable in middle income and low income countries. Unlike the mOm system provided by James et al. which lacks the maternal-infant bond and breastfeeding [START_REF] Roberts | mOm Incubators[END_REF][START_REF] Smithers | Mom', the inflatable incubator[END_REF]. In our system, the infant can benefit from the physiological advantage of breastfeeding from one side as provided by the KCM [START_REF] Corner | Kangaroo mother care saving premature infant's life[END_REF][START_REF] Gorski | Stages of behavioral organization in the high-risk neonate: theoretical and clinical considerations[END_REF][START_REF] Van Rooyen | The value of kangaroo mother care at kalafong hospital[END_REF][START_REF]Kangaroo mother care: a practical guide[END_REF][START_REF]SSC with Safe Technique[END_REF], and ensures a warm and anti-bacterial environment from the other side.

Our handy system also provides the biomedical feature extraction of the preterm HR, temperature, and SpO 2 level and display them on an LCD, this was reflected by the 75±1.5% performance in Fig. 7 (b). The absence of the approximately remaining 25% is due to the lack of measuring the humidity.

Noteworthy that overuse/under-use of oxygen supply to preterm infants can harm them, thereby SpO 2 was monitored in our Handy incubator and was maintained between 90 and 93% to avoid diseases. Pulse oximetry is an advantageous method of oxygenation monitoring, since it is continuous and noninvasive [START_REF] Chang | Optimal oxygen saturation in premature infants[END_REF].

In case of emergency, we programmed the system to provide temporary oxygen supply.

We also ensured to have a cost-effect handy incubator as compared to other intensive care methods [START_REF]Incubator and radiant warmer phototherapy unit[END_REF][START_REF] Blennow | Noise levels in infant incubators (adverse effects?)[END_REF][START_REF] Bonner | there were more wires than him': the potential for wireless patient monitoring in neonatal intensive care[END_REF][START_REF] Maastrup | Breastfeeding progression in preterm infants is influenced by factors in infants, mothers and clinical practice: the results of a national cohort study with high breastfeeding initiation rates[END_REF][START_REF] Corner | Kangaroo mother care saving premature infant's life[END_REF][START_REF] Bell | Infant incubators and radiant warmers[END_REF][START_REF] Chen | Embrace designed for extreme affordability[END_REF][START_REF]Kangaroo mother care: a practical guide[END_REF][START_REF]SSC with Safe Technique[END_REF][START_REF] Swart | Knowledge and attitude towards mother care[END_REF]].

Testing our incubator was necessary to control the quality of the electric, thermal and the graphic design of the incubator.

The Handy incubator provides a good therapeutic treatment such as oxygen supply and warmth. This paves the way for physician to monitor the premature infant state, through diagnosing the three vital signs showcased on the LCD and saving it in the memory.

In addition to the nice shape, the system does not produce any noise during turning on or moving, due to absence of fans, and due to the choice of the materials used in fabrication.

The KMC's overall performance (75±1.4%) was better than the embrace warmer (66.7±1.5%) in our explored specifications. However, our Handy incubator surpassed all the intensive care methods, with an overall performance of 91.7±1.6% (Table 1). Handy incubator is a user friendly technique. Despite our incubator took time to be 3D printed, its cost was reasonable as compared to expensive commercial incubators. Thereby, Handy incubators are promising, especially in middle income and low income countries.

Conclusion and Perspectives

Our original research is composed of both hardware and software contributions. The software implementation involved programming the processor platform via Arduino. The hardware execution involved 3D printing the Handy incubator, its circuit and connecting them to the Arduino. Our Handy incubator is designed to be portable, not heavy, and cost-effective.

With the progress of our novel 3D printed prototype of the Handy preterm infant incubator, many lives could be saved. Due to the lack of cost-effective intensive care methods for monitoring all vital signs, saving data and lack of a system that can be held by hands, we took the challenge in designing our handy and cost-effective infant incubator. Our design monitors the vital signals (Temperature, HR, and SpO 2 ), and display them. The Handy incubator ensures breastfeeding and is cost-effective. The evaluated percentages of performance shows that it surpasses existing intensive care methods.

Our system solved many of the challenges but still there is a margin for more improvement.

Future steps may include:

• Collecting more data on the infrared sensor MAX30100 that we assigned in our system to improve the oximetry reading.

• Concerning the hardware, as the sensor consists of two LEDs and photo-receptor with microprocessor which provide wide variety of pulse width and light intensity, and as the code provided by the manufacturer was not merely for medical use, rendering and updating the software to meet the medicine criteria are necessary.

• Using Peltier cell (semiconductor-based electronic component that operates as a small heat pump according to the "Peltier effect") instead of the heater.

• Modifying the electronic board by adding charge control (maximum power point tracking) to search for maximum power point, by searching for the load resistance resonance with the resistance of supply that has the maximum efficiency of charging.

• Finally, improving the software and providing a web-server for telehealth achievement and research purposes.

  (a), and the box label in Fig. 3 (b). The red space represents the position where the PCB is secured. The blue part represents the batteries handle; batteries handle can withstand up to eight batteries.

  (a), from both the bottom and top layers that were printed, UV light source to the PCB board after washing it with water. The sewing steps are shown in Fig. 5 (b). It represents gluing mylar with cardboard, the outcome of glued silinylon with mylar and card box, how the obtained fabric is attached to the Handy incubator, and represents the bamboo fabric which is held on top of the gel packs were the infant lies in the open Handy incubator. Fig. 5 (c) represents the laboratory setup utilized

Figure 1 :Figure 2 :Figure 3 :Figure 4 :

 1234 Figure 1: Handy Incubator Block Diagram.

Figure 5 :

 5 Figure 5: Demonstration of the Real Prototype's Implementation and Testing. (a) PCB Process. (b) Sewer Process. (c) The Laboratory Setup Utilized for Testing the Warming System Component's of the Handy Incubator.

Figure 6 :

 6 Figure 6: The Novel Handy Preterm Incubator When In a Closed Mode.

Figure 7 :

 7 Figure 7: The Evaluation of the Handy Incubator Compared to the Intensive Care Methods; Commercial Incubator, Transport Incubator, Radiant Incubator, Kangaroo Mother Care (KMC), Embrace Warmer and Handy Incubator. (a) The Variation of the Monitored Features or Measurements Recorded, the Maternal-Preterm Bond and the System Mobility Versus the Methods. (b) The Variation of the Therapeutic Support, Environment Type and the Design Model Versus the Methods.

Figure 8 :

 8 Figure 8: The Evaluation of the Handy Incubator Compared to the Intensive Care Methods; Commercial Incubator, Transport Incubator, Radiant Warmer, Embrace Warmer and Handy Incubator. The Bar Graph Represents the Cost (in 1000 $).

Table 1 :

 1 The Overall Percentage of Performance of the Commercial Incubator, Transport Incubator, Radiant Warmer, Kangaroo Care Method (KMC), Embrace Warmer and the Handy Incubator.

	Preterm Infant Intensive Care Method	Overall Performance (%)
	Commercial Incubator	33.3±0.8 %
	Transport Incubator	41.7±0.7%
	Radiant Warmer	37.5±0.9 %
	Kangaroo Care Method (KMC) *	75.0±1.4 %
	Embrace Warmer *	66.7±1.5%
	Handy Incubator *	91.7±1.6%

Acknowledgements

The authors would like to thank Dr. Mohammad Arnaout and Dr. Lara Hamawy and Miss Alaa Zaylaa for their supportive information.

Funding

This project was funded by the Lebanese University and the University of Texas, MD Anderson Cancer Center, Houston USA.

The therapeutic support, evaluated in Fig. 7 (b), is the preterm infant contact with the mother. A maximum value of 100% was associated with the maximum therapeutic support and treatment ensured by the system. A null value of 0% was associated with the minimum therapeutic support. The maximum performance 100% of the therapeutic support was associated with the commercial and Handy incubators.

The environment, evaluated in Fig. 7 (b), is the nature of the interface of the method with the surrounding. A closed environment is the total isolation of the preterm infant, while the open environment is the insulation permitting the aspiration of the preterm infant from the surrounding ambient air. Noteworthy, the insulation permitting the inhalation was associated the highest performance (100%). The performance of the environment type was maximum in the radiant warmer, KMC, embrace warmer and the Handy incubator.

The design model, evaluated also in Fig. 7 (b) is the capability of mobilizing the intensive care system. The maximum performance 100% of the design model was associated with KMC, then 75% was associated with the Handy incubator.

The cost (in 1000 $) of the Handy incubator was represented and compared to the cost of the commercial incubator, transport incubator, radiant warmer, embrace warmer and our Handy incubator is shown in Fig. 8. The range of the standard deviation is due to the presence of different commercial incubator's designs having different specifications. The cost is the average cost of these existing incubators. As shown in Fig. 8, the highest incubator's cost is associated with the commercial incubator. Noteworthy that the gross price reported depends on the company and accessories. The KMC is cost-less, and the cost of both the Handy incubator and the embrace warmer is about 300$. While that of commercial incubator is on average 32 K$ (it ranges between 1 K$ and 55 K$).

[Table 1 about here.]

Discussion

Although there are advantanges associated with existing intensive care methods, whether open care or closed care. The commercial infant incubators, fixed, mobile, and transportable

Conflict of Interest

All the authors declare no competing financial or non-financial interests.

List of Figures


Heytem Zitoun

Claude Michel

Michel Rueher

Laurent Michel

Sub-domain Selection Strategies For Floating Point Constraint Systems

Program verification is a key issue for critical applications such as aviation, aerospace, or embedded systems. Bounded model checking (BMC) and constraint programming (CBMC, CBPV, ...) approaches are based on counter-examples that violate a property of the program to verify. Searching for such counter-examples can be very long and costly when the programs to check contains floating point computations. This stems from the fact that existing search strategies have been designed for discrete domains and, to a lesser extent, continuous domains. In [12], we have introduced a set of variable choice strategies that take advantages of the specificities of the floats, e.g., domain density, cancellation and absorption phenomena. In this paper we introduce new sub-domain selection strategies targeting domains involved in absorption and using techniques derived from higher order consistencies. Preliminary experiments on a significant set of benchmarks are very promising.

Introduction

Programs with floating-point computations control complex and critical systems in numerous domains, including cars and other transportation systems, nuclear energy plants, or medical devices. Floating-point computations are derived from mathematical models on real numbers [START_REF] Goldberg | What every computer scientist should know about floating-point arithmetic[END_REF], but computations on floating-point numbers are different from computations on real numbers. For instance, with binary floating-point numbers, some real numbers cannot be represented (e.g., 0.1 does not have an exact representation). Floating point arithmetic operators are neither associative nor distributive, and may be subject to phenomena such as absorption and cancellation. Furthermore, the behavior of programs containing floating-point computations varies with the programming language, the compiler, the operating system, or the hardware architecture.

Figure 1 illustrates how the flow of a very simple program over the floats (F) can differs from the expected flow over the reals (R). When interpreting the program over reals, the instruction doThenPart should be executed. However, an absorption on the floats (the value 1 is absorbed by 1e8f 3 ) leads the program through the else branch. In [START_REF] Heytem Zitoun | Search strategies for floating point constraint systems[END_REF], we have introduced a set of variable selection strategies based on specific properties of floats like domain density, cancellation and absorption phenomena. The resulting search strategies are much more efficient but do not really scale for harder and more realistic benchmarks. Indeed, like in other applications of constraint techniques, efficient solvers not only requires appropriate variable selection strategies but also need relevant value selection strategies. So, this paper focuses on value selection strategies for floating-point constraint solvers dedicated to the search of counter-examples in program verification applications.

Standard value selection strategies over the floats are derived from subdomain selection strategies used over the reals; sub-domains being generated by using various splitting techniques, eg,

x ≤ v or x > v with v = x+x 2 .
In this paper we introduces four new sub-domain selection strategies. The first one, exploits absorption phenomena, the second one embraces ideas derived from strong consistency and the two last ones extend strategies introduced in [START_REF] Heytem Zitoun | Search strategies for floating point constraint systems[END_REF]. We have evaluated these new sub-domain selection strategies on a significant set of benchmarks originate with program verification. We implemented a set of over 300 search strategies that are combinations of variable selection strategies previously introduced, sub-domain selection strategies presented in the following pages and variations of different criteria like filtering. All strategies were implemented in Objective-CP, the optimization tool introduced in [START_REF] Van | The objective-cp optimization system[END_REF].

In summary, the contributions are new sub-domain selection strategies dedicated to float system. The rest of this article is organized as follows. Section 2 presents some notations, and definitions necessary for understanding this document. Section 3 provides a brief reminder of the strategies presented in [START_REF] Heytem Zitoun | Search strategies for floating point constraint systems[END_REF]. Section 4 explains the new splitting strategies we propose. Section 5 is devoted to an analysis of the experimental results. Finally, Section 6 discusses the work in progress and the perspectives.

Floating point numbers

Floating point numbers approximate real numbers. The IEEE754-2008 standard for floating point numbers [9] sets floating point formats, as well as, some floating point arithmetic properties. The two most common formats defined in the IEEE754 standard are simple and double floating point number precision which, respectively, use 32 bits and 64 bits. A floating point number is a triple (s, m, e) where s ∈ {0, 1} represents the sign, the mantissa m (also called significant), which is p bits long, and, e the exponent [START_REF] Goldberg | What every computer scientist should know about floating-point arithmetic[END_REF]. A normalized floating point number is defined by: (-1)

s 1.m × 2 e
To allow gradual underflow, IEEE754 introduces denormalized numbers whose value is given by: (-1) s 0.m × 2 0

Note that simple precision are represented with 32 bits and a 23 bits mantissa (p = 23) while doubles use 64 bits and a 52 bits mantissa (p = 52).

Absorption

Absorption occurs when adding two floating point numbers with different order of magnitude. The result of such an addition is the furthest from zero. For instance, in C, using simple floating point numbers with a rounding mode set "to the nearest even", 10 8 + 1.0 evaluates to 10 8 . Thus, 1.0 is absorbed by 10 8 .

Notations

In the sequel, x, y and z denote variables and x, y and z, their respective domains. When required, x F , y F and z F denote variables over F and x F , y F and z F , their respective domains while x R , y R and z R denote variables over R and x R , y R and z R , their respective domains. Note that

x F = [x F , x F ] = {x F ∈ F, x F ≤ x F ≤ x F } with x F ∈ F and x F ∈ F. Likewise, x R = [x R , x R ] = {x R ∈ R, x R ≤ x R ≤ x R } with x R ∈ F and x R ∈ F. Let x F ∈ F, then x +
F is the smallest floating point number strictly superior to x F and x - F is the biggest floating point number strictly inferior to x F . In a similar way, x

+[N ] F is the N th floating point strictly superior to x F and x -[N ] F
is the N th floating point strictly inferior to x F . In addition, given a constraint c, vars(c) denotes the set of floating point variables appearing in c. Finally, given a set s, |s| denotes the cardinality of s.

Search strategies based on floating-point properties

In [START_REF] Heytem Zitoun | Search strategies for floating point constraint systems[END_REF], we have introduced a set of variable selection strategies based on specific properties of floats like domain density, cancellation and absorption phenomena. The resulting search strategies are much more efficient but do not really scale for harder and more realistic benchmarks.

Absorption-based strategy

Let's recall that absorption occurs when adding two floating point numbers with different order of magnitude. The result of such an addition is the number the furthest from zero.

The objective of the splitAbs strategy is to concentrate on the most relevant absorption phenomena, in other words, giving priority to the sub-domains of x and y most likely to lead to an absorption.

Before going into the details of this absorption-based sub-domain selection strategy, let us recall the key points of M axAbs, the variable strategy introduced in [START_REF] Heytem Zitoun | Search strategies for floating point constraint systems[END_REF]. M axAbs is a variable selection strategy that picks the variable "absorbing the most". More precisely, this variable selection strategy needs to branch on two variables involved in absorption. The first variable -represented by x in Figure 2must have the highest absorption rate. After selection of variable x, strategy M axAbs examines addition and subtraction constraints to select a variable y, the values of which are most absorbed by the values of by x. Coordinated branching on these variables is performed to exploit the latent absorption.

Sub-domain selection strategy : splitAbs Once these two variables are selected, the sub-domain selection heuristic will perform at most three splits on each variable. Figure 2 illustrates an instance where two sub-domains are generated (match with the case where domains are positive). It's easy to extend it to the others cases by symmetry. In this Figure, most interesting sub-domains are for x : [2 e x , x] and for y : y ∩ [0, 2 e x -p-1 ] (where p is the mantissa size). The first represents the sub-domain of x values absorbing y values. The second represents the sub-domain of y totally absorbed by x.

Example 1. Consider the function in Figure 3 and assume that inputs are coming from sensors, and their ranges are [0.0, 1e+04] for x, and [-16.0, 4.0] for y. The else branch corresponds to an unstable state of the system. Determining if this state is reachable and from which input values is a legitimate question. This problem is reduced to identifying if z can be equal to x which corresponds to absorption. Figure 4 This strategy can also be combined with another strategy, which is called whenever x has no values that absorb y.

Splitting strategy inspired by 3B-consistency : 3BSplit

Our next sub-domain splitting strategy, called 3Bsplit, is inspired by a higher consistency named 3B-consistency [START_REF] Lhomme | Consistency techniques for numeric csps[END_REF]. 3B-Consistency is a relaxation on continuous domains of path consistency, a higher order extension of arc-consistency. Roughly speaking, 3B-Consistency checks whether 2B-consistency (or Hull consistency) can be enforced when the domain of a variable is reduced to the value of one of its bounds in the whole system [START_REF] Collavizza | Comparing partial consistencies[END_REF]. 3B-consistency is in practice very effective on problems with multiple occurrence variables. However, insuring such consistency could be costly: the 3B-algorithm might attempt many times to unsuccessfully refute sub-domains near the bounds of the initial domain by means of a 2B-consistency.

The 3Bsplit sub-domain selection also attempts to enforce the consistency at the bounds of a domain at a single variable level. A key observation here is that if a small sub-domain at the bounds of the initial domain, e.g. sd = [x, x + δ], is immediately refuted in the next search node, then the resulting domain, [x+δ, x], offers a better lower bound than the one of the initial domain. Moreover, there is probably room to still improve this bound if the same step is reiterated using a wider sub-domain like [x, x + 2δ]. Indeed, such a process is similar to a shaving applied to the initial domain but without requiring additional domain state management: in the case of a 3Bsplit, the capability to return to the initial state is naturally supported by the search.

A sub-domain split might not be refuted immediately in the next search node. It might be refuted either after exploring a deeper search sub-tree or it might provide one or more solutions. Both cases underline some difficulties to improve the bound under examination. The next step of the splitting strategy thus switch to the next bound or, if both bounds have been checked, to another search node or strategy. Figure 5 illustrates 3Bsplit behavior.

To summarize, 3Bsplit exploits information on the sub-tree to decide whether enforcing the current bound has a chance to be done effortlessly or if it would be wiser to go to the next step. As a result, this strategy dynamically splits the current domain according to the behavior of the search in sub-trees. Note also that choosing an initial small sub-domain at the bounds of the domain is similar to the next strategy (Section 4.3), i.e., 3Bsplit also provides opportunities to find solutions the neighbourhood of the current bounds.

Mixing sub-domain and enumeration

This sub-domain selection strategy extends strategies from [START_REF] Collavizza | Searching critical values for floating-point programs[END_REF]. We propose two ways to extend these strategies. The first one Enum-N, enumerates N values of both bound and one in the middle before considering the rest of the domain. The second one, Delta-N, instead of enumerating each N values of the bounds, builds the sub-domains implied by N floating point numbers. Due to the huge number of evaluated strategies, the value of N is arbitrarily limited to 5 in the experiment part.

Enum-N

This sub-domain selection strategy is a direct generalization of [START_REF] Collavizza | Searching critical values for floating-point programs[END_REF]. Generally, the filtering process tightens the bounds until a support is found. This sub-domain selection strategy is optimistic and hope that filtering will lead to find a solution close to the bounds. To achieve this goal, it enumerates few values at the bounds. Figure 6a illustrates this strategy. The domains is split in 2 * N + 3 sub domains. For instance, with N = 5, the 13 following domains will be generated :

• [min, min] • • • • • [min +[N ] , min +[N ] ] • [min +[N +1] , mid -] • [mid, mid] • [mid + , max -[N +1] ] • [max -[N ] , max -[N ] ] • • • • • [max, max]
If the cardinality of the domain is lower than 2 * N + 3, all values will be enumerated.

Delta-N

The first objective of this strategy is to find a solution at the bounds.

Enumerating can lead the search to explore a deep sub-tree before finding a Starting the search by a classic bisection (N = |α|) and reducing its value might be a good idea. Figure 6b illustrates this strategy. Regardless the value of N and the cardinality of the domain, at most the 5 following sub-domains will be generated :

• • • • • • min N f loats
• [min, min

+[N ] ] • [min +[N +1] , mid -] • [mid, mid] • [mid + , max -[N +1] ] • [max -[N ] , max]
If the cardinality of the domain is lower than 2 * N + 3, the last two sub-domains will not be generated, and the first two will be balanced with respect to the middle of the domain.

Experimental Evaluation

The experiments combine different variable selection strategies with sub-domain selection strategies on a set of 49 benchmarks. They also consider variations on the type of consistency for the strategies, sub-cuts, and the reselection (or not) of the same variable at the next node. Sub-cut corresponds to an alternative subdomain selection strategy and is relevant for splitAbs and 3Bsplit. For splitAbs, sub-cut is called when no absorptions occur. For 3Bsplit, it is called to refute small sub-domains. In the state of the art, the standard strategy is based on lexicographic variable ordering, and a bisection based on 2B-consistency. These options result in no less than 325 unique strategies evaluated on all 49 benchmarks.

All experiments were performed on a Linux system, with an Intel Xeon processor running at 2.40GHz and with 12GB of memory. All strategies have been implemented into the Objective-CP solver. All the floating point computations are performed in simple precision and with a rounding mode "to the nearest even".

Benchmarks

The benchmarks used in these experiments come from test and program verification. SMTLib [START_REF] Barrett | The Satisfiability Modulo Theories Library (SMT-LIB)[END_REF], FPBench [START_REF] Damouche | Toward a standard benchmark format and suite for floating-point analysis[END_REF], and CBMC [START_REF] Clarke | A tool for checking ansi-c programs[END_REF] (but also [START_REF] Collavizza | Cpbpv: A constraint-programming framework for bounded program verification[END_REF][START_REF] Collavizza | Searching critical values for floating-point programs[END_REF][START_REF] Vijay | Numeric bounds analysis with conflict-driven learning[END_REF]) are the main sources. In each case, the goal is to find a counter-example, hence the majority of instances are satisfiable. The number of constraints and variables varies from 2 to about 3000. Table summarizes thoses results of all the strategies on the satisfiable instances can be found at www.i3s.unice.fr/~hzitoun/dp18/ benchmark.html.

Analysis

In results Tables, the standard strategy (lexicographic order with bisection, 2B filtering at 5% and reselection allowed) is at the 194 th position on 325 strategies. So, 193 strategies among those introduced, are clearly more efficient than the standard strategy for solving this kind of problem. The Virtual Best Strategy is 120 times faster than the reference strategy. The best strategy (column 1) is 4 times faster than the reference strategy. Using the specificities of floats to guide the search has a clear impact on the resolution time. Among the strategies that are efficient on this set of benchmarks, the variable selection strategies are based on lexicographic order, number of occurrences, density or absorption. While strategies based on width, a conventional variable selection strategy for integer domains, struggle to solve problems as soon as it becomes a bit realistic. Strategies based on cardinality are also in the same cases. The best search based on MaxCard and MaxWidth are at 160 th and 161 th positions.

Sub-domain selection strategies introduced in this article are working well. Indeed, the faster strategy exploiting Delta-N is in second position, whereas Enum-N is at 6 th position. The best 3BSplit is placed at 11 th . SplitAbs, for its part, is at 112 th position. SplitAbs performance are clearly related to the percentage of absorption of the problem. Indeed, as shown in the online tables, the set of benchmarks limited to those with at least 5% of absorption are resolved without timeout. All these strategies perform better than the standard one.

Eight of the 10 best strategies prohibit the repeated selection of a variable at subsequent search nodes. Among the 10 worst, only one of them prohibits reselection. It appears that "reselection" impacts the ability to deliver solutions faster.

Conclusion

A previous article proposed a set of variable selection strategies using the specificities of floats to guide the search. These variable selection strategies improve the search of a counter-example outlining a property violation in a program to verify, but aren't sufficient to scale for harder and more realistic benchmarks. Dedicated sub-domain selection strategies for floats are needed. Contributions of this article are a set of sub-domain selection strategies over floats. The first one, exploits absorption phenomena, the second one embraces ideas derived from strong consistency and the two last ones extend strategies introduced in [START_REF] Collavizza | Searching critical values for floating-point programs[END_REF]. These strategies are compared on a set of satisfiable benchmarks. Several strategies presented, perform well, and obtain much better results than the standard strategy used to solve this kind of problem.

Fig. 1 .

 1 Fig. 1. Motivation example

1 -Fig. 2 .

 12 Fig. 2. Sub-domains generated by splitAbs (x > 0 and y > 0)

- 4 , 4 -Fig. 4 .

 444 Fig. 3. A program with absorptions

Fig. 5 .

 5 Fig. 5. Illustration of 3BSplit

Fig. 6 .

 6 Fig. 6. Illustration of new strategies solution or performing reduction. Here, considering the sub-domain implied by N floating-point numbers instead of a single value, gives opportunities to the filtering process to operate some pruning through propagation. It also improves the chance to find a solution or to remove all N values without enumerating any of them. This sub-domain selection strategy is very flexible. Indeed, by adapting the value of N , the whole strategy behavior change. For instance, if N = |α|, with α = [x, x+x 2 ], this sub-domain strategy becomes a classic bisection. Finally, a dynamic modification of the value of N during the search can be interesting.Starting the search by a classic bisection (N = |α|) and reducing its value might be a good idea. Figure6billustrates this strategy. Regardless the value of N and the cardinality of the domain, at most the 5 following sub-domains will be generated :• [min, min+[N ] ] • [min +[N +1] , mid -] • [mid, mid]

This work was partially supported by ANR COVERIF (ANR-15-CE25-0002).