# On the Semantics of Hybrid ASP Systems Based on Clingo
## 5 Answer Set Solving Modulo Linear Equations
### clingcon  
In clingcon, all theory atoms are external, that is \(\mathcal{E}=\mathcal{T}\), and may indistinctly occur in the head or in the body. As we already mentioned, one interesting feature of clingcon is that it does not only show the \(\langle\mathfrak{L},\mathcal{E}\rangle\)-stable models but also allows for enumerating all \(\langle\mathfrak{L},\mathcal{E}\rangle\)-answer sets for those stable models. To illustrate differences between \(\langle\mathfrak{L},\mathcal{E}\rangle\)-stable models and \(\langle\mathfrak{L},\mathcal{E}\rangle\)-answer sets, consider Listing 1, which contains a program calculating the overall taxes in the language of clingcon. To interpret this program in our notation, we consider \".\" to be the separation between the rules of the program, \":-\" is the implication \(\leftarrow\), \"not\" is the negation \(\
eg\), and the choice rule eligible is an abbreviation for the rule eligible\(\leftarrow\
eg\
eg\)eligible. The program contains one propositional variable, eligible, signifying whether one is eligible for a tax deduction, and three integer variables tax, deduction, and overall that are used in theory atoms and represent taxes before deduction, possible tax deduction, and the overall taxes to pay, respectively. Lines 1 and 2 describe the domain of the integer variables tax and deduction via theory atoms that state that tax is greater or equal to zero and smaller or equal to two, and deduction is greater or equal to zero and at most, the value of tax. Line 3 allows propositional atoms eligible to be freely chosen. Overall, Lines 1 to 3 describe the solution space with six overall combinations of values for the integer variables that are doubled by the possible truth values of eligible to a total of twelve combinations. In practice, these values would, of course, be subject to more complex computations. Lines 5 and 6 then calculate the value of the integer variable overall. The former, by subtracting the value of deduction from tax if eligible, is true, and the latter sets overall equal to tax if eligible is false. ```
1&sum{tax}>=0.&sum{tax}<=2. 2&sum{deduction}>=0.&sum{deduction}<=tax. 3{eligible}. 4
5&sum{tax;-deduction}=overall:-eligible. 6&sum{tax}=overall:-noteligible. ```  
**Listing 1**clingcon-program calculating taxes  
In the following, the set \(\mathcal{T}\) is comprised of the theory atoms occurring in Listing 1 and their complement. The clingcon-program has four \(\langle\mathfrak{L},\mathcal{E}\rangle\)-stable models:  
```
{&sum{tax}>=0,&sum{tax}<=2, &sum{deduction}>=0,&sum{deduction}<=tax, &sum{tx;-deduction}=overall,&sum{tax}!=overall,eligible}
```  
```
{&sum{tax}>=0,&sum{tax}<=2, &sum{deduction}>=0,&sum{deduction}<=tax, &sum{tx;-deduction}=overall,&sum{tax}=overall,eligible}
```  
**Listing 2**clingcon-program calculating taxes  
{&sum{tax}>=0, &sum{tax}<=2,  &sum{deduction}>=0, &sum{deduction}<=tax,  &sum{tax}=overall, &sum{tax;-deduction}!=overall} and  {&sum{tax}>=0, &sum{tax}<=2,  &sum{deduction}>=0, &sum{deduction}<=tax,  &sum{tax}=overall, &sum{tax;-deduction}=overall} We have four stable models since variable deduction can be zero, so whether we are eligible or not, we may have tax=tax-deduction=overall. These four \(\langle\mathfrak{L},\mathcal{E}\rangle\)-stable models yield the following twelve answer sets:  
\[