package org.clafer.ir.analysis.deduction;

import org.clafer.domain.Domain;
import org.clafer.ir.IrSetExpr;
import org.clafer.ir.IrSetMin;

/**
 *
 * @author jimmy
 */
class SetMinDeducer implements IntDeducer<IrSetMin> {

    @Override
    public void deduce(IrSetMin ir, Domain domain, Deduction deduction) {
        IrSetExpr set = ir.getSet();

        boolean nonEmpty = set.getCard().getLowBound() > 0
                || !domain.contains(ir.getDefaultValue());

        if (nonEmpty && !set.getKer().intersects(domain)) {
            deduction.cardGreaterThanEqual(set, set.getKer().size() + 1);
            if (set.getKer().size() + 1 == set.getCard().getHighBound()) {
                deduction.envSubsetOf(set, set.getEnv().intersection(domain).union(set.getKer()));
            }
        }
    }
}

@@ -69,16 +69,50 @@
 Domain;%0A
+import org.clafer.domain.Domains;%0A
 import o
@@ -135,16 +135,16 @@
 etExpr;%0A
-
 import o
@@ -519,12 +519,28 @@
 mpty
- && 
+) %7B%0A            if (
 !set
@@ -567,24 +567,74 @@
 (domain)) %7B%0A
+                // Set needs another element.%0A    
             
@@ -695,16 +695,20 @@
 ) + 1);%0A
+    
         
@@ -770,24 +770,87 @@
 hBound()) %7B%0A
+                    // Set can take only one more element.%0A    
             
@@ -936,16 +936,485 @@
 er()));%0A
+                %7D%0A            %7D%0A            int min = domain.getLowBound();%0A            if (!set.getKer().isEmpty()) %7B%0A                min = Math.min(min, set.getKer().getLowBound());%0A            %7D%0A            if (set.getEnv().getLowBound() %3C min) %7B%0A                deduction.envRemove(set, Domains.boundDomain(set.getEnv().getLowBound(), min - 1));%0A            %7D%0A            if (domain.isConstant()) %7B%0A                deduction.kerContains(set, domain.getLowBound());%0A
         

Improve set min deduction.