Merge pull request #33 from potassco/open-bounds

Open bounds

examples/asp/cargobike-coom.lp

@@ -0,0 +1,46 @@
+%%% COOM model
+coom_structure("product").
+coom_feature("product","totalVolume","num",1,1).
+coom_range("product","totalVolume",0,200).
+coom_feature("product","requestedVolume","num",1,1).
+coom_range("product","requestedVolume",0,200).
+coom_feature("product","bags","Bag",0,#sup).
+
+coom_structure("Bag").
+coom_feature("Bag","color","Color",1,1).
+coom_feature("Bag","size","Size",1,1).
+
+coom_enumeration("Color").
+coom_option("Color", "Green").
+coom_option("Color", "Blue").
+coom_option("Color", "Red").
+
+coom_enumeration("Size").
+coom_attribute("Size","weight","num").
+coom_attribute("Size","volume","num").
+coom_option("Size", "small").
+coom_attribute_value("Size","small","weight",10).
+coom_attribute_value("Size","small","volume",12).
+coom_option("Size", "medium").
+coom_attribute_value("Size","medium","weight",15).
+coom_attribute_value("Size","medium","volume",16).
+coom_option("Size", "large").
+coom_attribute_value("Size","large","weight",25).
+coom_attribute_value("Size","large","volume",20).
+
+coom_behavior(0).
+coom_context(0,"product").
+coom_require(0,"sum(bags.size.volume)=totalVolume").
+coom_binary("sum(bags.size.volume)=totalVolume","sum(bags.size.volume)","=","totalVolume").
+coom_function("product","sum(bags.size.volume)","sum","bags.size.volume").
+coom_path("bags.size.volume",0,"bags").
+coom_path("bags.size.volume",1,"size").
+coom_path("bags.size.volume",2,"volume").
+coom_path("totalVolume",0,"totalVolume").
+
+coom_behavior(1).
+coom_context(1,"product").
+coom_require(1,"totalVolume>=requestedVolume").
+coom_binary("totalVolume>=requestedVolume","totalVolume",">=","requestedVolume").
+coom_path("totalVolume",0,"totalVolume").
+coom_path("requestedVolume",0,"requestedVolume").

examples/coom/cargobike.coom

@@ -0,0 +1,38 @@
+product {
+    //   num /kg 0-200 totalWeight
+    //   num /kg 0-200 wantedWeight
+            num /l  0-200   totalVolume
+            num /l  0-200   requestedVolume
+    //   num     countBags
+    0..*    Bag             bags
+}
+
+structure Bag {
+    // Color color
+    Size  size
+}
+
+enumeration Color { Green Blue Red }
+
+enumeration Size {
+    attribute num weight
+    attribute num volume
+
+    small   = ( 10 12 )
+    medium  = ( 15 16 )
+    large   = ( 25 20 )
+}
+
+behavior {
+    // require sum(bags.size.maxWeight) = totalWeight
+    require sum(bags.size.volume) = totalVolume
+
+    // require totalWeight >= wantedWeight
+    require totalVolume >= requestedVolume
+
+}
+
+// behavior {
+//     imply countBags = count(bags)
+//     minimize countBags
+// }

examples/coom/travel-bike-simplified.coom

@@ -3,10 +3,10 @@
 // see Baumeister et al.: Towards Industrial-scale Product Configuration (2024).
 
 product {
-    num .#/l	0-200   totalVolume
+    num .#/l	  0-200   totalVolume
     num .#/l	200-200   requestedVolume
-    Carrier			    carrier
-    Frame			    frame
+    Carrier			      carrier
+    Frame			      frame
 }
 
 structure Carrier {

examples/coom/user-input.coom

@@ -1,6 +1,7 @@
 
-set color[0] = Yellow
+// set color[0] = Yellow
 // set size[0] = 14
 // add basket[0]
 // add carrier[0].bag[0]
 // add carrier[0].bag[1]
+set requestedVolume[0] = 95

src/coomsuite/__main__.py

@@ -3,16 +3,46 @@
 """
 
 import sys
-from tempfile import TemporaryDirectory
+from tempfile import NamedTemporaryFile, TemporaryDirectory
+from typing import List
 
 from clingo.application import clingo_main
 
 from . import convert_instance
-from .application import COOMApp
+from .application import COOMSolverApp
+from .preprocess import check_user_input, preprocess
 from .utils.logging import configure_logging, get_logger
 from .utils.parser import get_parser
 
 
+def solve(serialized_facts: List[str], max_bound: int, args, unknown_args) -> int:
+    """
+    Preprocesses and solves a serialized COOM instance.
+    """
+    # Preprocess serialized ASP facts
+    processed_facts = preprocess(
+        serialized_facts,
+        max_bound=max_bound,
+        discrete=args.solver == "clingo",
+    )
+    check_user_input(processed_facts)
+
+    with NamedTemporaryFile(mode="w", delete=False) as tmp:
+        tmp_name = tmp.name
+        tmp.write("".join(processed_facts))
+
+    # Solve the ASP instance
+    return clingo_main(
+        COOMSolverApp(
+            {
+                "solver": args.solver,
+                "output_format": args.output,
+            }
+        ),
+        [tmp_name] + unknown_args,
+    )
+
+
 def main():
     """
     Run the main function.
@@ -42,27 +72,25 @@ def main():
 
     elif args.command == "solve":
         log.info("Converting and solving COOM file %s", args.input)
+
         with TemporaryDirectory() as temp_dir:
-            clingo_options = (
-                [convert_instance(args.input, "model", temp_dir)]
-                + ([convert_instance(args.user_input, "user", temp_dir)] if args.user_input else [])
-                + unknown_args
+            # Parse COOM to ASP serialized facts
+            serialized_facts = [convert_instance(args.input, "model", temp_dir)] + (
+                [convert_instance(args.user_input, "user", temp_dir)] if args.user_input else []
             )
 
             if args.show_facts:
-                clingo_options.append("--outf=3")
-
-            options = {
-                "solver": args.solver,
-                "output_format": args.output,
-                "show_facts": args.show_facts,
-                "preprocess": True,
-            }
-
-            clingo_main(
-                COOMApp(options=options),
-                clingo_options,
-            )
+                print("\n".join(preprocess(serialized_facts)))  # nocoverage
+            elif not args.incremental_bounds:
+                solve(serialized_facts, 99, args, unknown_args=unknown_args)
+            else:
+                ret = 20
+                max_bound = 1
+
+                while ret == 20:
+                    print(f"\nSolving with max_bound = {max_bound}\n")
+                    ret = solve(serialized_facts, max_bound, args, unknown_args=unknown_args)
+                    max_bound += 1
 
 
 if __name__ == "__main__":

src/coomsuite/application.py

@@ -9,7 +9,6 @@
 from clingo import Control, Model, Symbol
 from clingo.application import Application, ApplicationOptions, Flag
 from clingo.ast import Location, Position, ProgramBuilder, Rule, parse_files
-from clingo.script import enable_python
 from clingo.symbol import Function, SymbolType
 from fclingo.__main__ import CSP, DEF, MAX_INT, MIN_INT
 from fclingo.__main__ import AppConfig as FclingoConfig
@@ -51,15 +50,12 @@ def _sym_to_prg(symbols: Sequence[Symbol], output: Optional[str] = "asp") -> str
     return "\n".join(output_list)
 
 
-class COOMApp(Application):
+class COOMSolverApp(Application):
     """
     Application class extending clingo.
     """
 
     _options: Dict[str, Any]
-    # _solver: str
-    # _output: str
-    # _show_facts: bool
     _istest: bool
     _log_level: str
     config: FclingoConfig
@@ -76,11 +72,7 @@ def __init__(
         """
         Create application.
         """
-        self._options = (
-            {"solver": "clingo", "output_format": "asp", "show_facts": False, "preprocess": True}
-            if options is None
-            else options
-        )
+        self._options = {"solver": "clingo", "output_format": "asp"} if options is None else options
         self._istest = istest
         self._log_level = "WARNING" if log_level == "" else log_level
         self.config = FclingoConfig(MIN_INT, MAX_INT, Flag(False), Flag(False), DEF)
@@ -117,33 +109,6 @@ def register_options(self, options: ApplicationOptions) -> None:  # nocoverage
         #     group, "view", "Visualize the first solution using clinguin", self._view
         # )
 
-    def _parse_user_input_unsat(self, unsat: Symbol) -> str:
-        """
-        Parses the unsat/2 predicates of the user input check
-        """
-        unsat_type = unsat.arguments[0].string
-        info = unsat.arguments[1]
-
-        if unsat_type == "not exists":
-            variable = info.string
-            msg = f"Variable {variable} is not valid."
-        elif unsat_type == "not part":
-            variable = info.string
-            msg = f"Variable {variable} cannot be added."
-        elif unsat_type == "not attribute":
-            variable = info.string
-            msg = f"No value can be set for variable {variable}."
-        elif unsat_type == "outside domain":
-            variable = info.arguments[0].string
-            if str(info.arguments[1].type) == "SymbolType.Number":
-                value = str(info.arguments[1].number)
-            else:
-                value = info.arguments[1].string
-            msg = f"Value '{value}' is not in domain of variable {variable}."
-        else:
-            raise ValueError(f"Unknown unsat type: {unsat_type}")  # nocoverage
-        return msg
-
     def on_model(self, model: Model) -> None:  # nocoverage
         """
         Function called after finding each model.
@@ -178,90 +143,38 @@ def print_model(self, model: Model, printer: Callable[[], None]) -> None:  # noc
 
         print(_sym_to_prg(output_symbols, self._options["output_format"]))
 
-    def preprocess(self, files: List[str]) -> List[str]:
-        """
-        Preprocesses COOM ASP facts into a "grounded" configuration fact format
-        """
-        # pylint: disable=not-context-manager
-        input_files = files
-        pre_ctl = Control(message_limit=0)
-        for f in input_files:
-            pre_ctl.load(f)
-
-        if self._options["preprocess"] or self._options["show_facts"]:
-            enable_python()
-            pre_ctl.load(get_encoding("preprocess.lp"))
-            if self._options["solver"] == "clingo":
-                pre_ctl.add("base", [], "discrete.")  # nocoverage
-
-        pre_ctl.ground()
-        with pre_ctl.solve(yield_=True) as handle:
-            facts = [str(s) + "." for s in handle.model().symbols(shown=True)]
-
-        return facts
-
-    def check_user_input(self, facts: str) -> list[str]:
-        """
-        Checks if the user input is valid and returns a clingo.SolveResult
-        """
-        user_input_ctl = Control(message_limit=0)
-        user_input_ctl.load(get_encoding("user-check.lp"))
-        user_input_ctl.add(facts)
-        user_input_ctl.ground()
-        with user_input_ctl.solve(yield_=True) as handle:
-            unsat = [self._parse_user_input_unsat(s) for s in handle.model().symbols(shown=True)]
-        return unsat
-
     def main(self, control: Control, files: Sequence[str]) -> None:
         """
         Main function ran on call.
         """
-        processed_facts = self.preprocess(list(files))
-
-        if self._options["show_facts"]:
-            print("\n".join(processed_facts))  # nocoverage
-        else:
-            facts = "".join(processed_facts)
+        encoding = get_encoding(f"encoding-base-{self._options['solver']}.lp")
+        for f in files:
+            control.load(f)
 
-            if self._options["solver"] == "preprocess":
-                control.add(facts)
-                control.ground()
-                control.solve()
-            else:
-                user_input_check = self.check_user_input(facts)
-                if user_input_check != []:
-                    error_msg = "User input not valid.\n" + "\n".join(user_input_check)
-                    raise ValueError(error_msg)
-
-                encoding = get_encoding(f"encoding-base-{self._options['solver']}.lp")
-
-                if self._options["solver"] == "clingo":
-                    control.load(encoding)
-                    control.add(facts)
-
-                    control.ground()
-                    control.solve()
+        if self._options["solver"] == "clingo":
+            control.load(encoding)
+            control.ground()
+            control.solve()
 
-                elif self._options["solver"] == "fclingo":
-                    self._propagator.register(control)
-                    self._propagator.configure("max-int", str(self.config.max_int))
-                    self._propagator.configure("min-int", str(self.config.min_int))
+        elif self._options["solver"] == "fclingo":
+            self._propagator.register(control)
+            self._propagator.configure("max-int", str(self.config.max_int))
+            self._propagator.configure("min-int", str(self.config.min_int))
 
-                    control.add("base", [], facts)
-                    control.add("base", [], THEORY)
+            control.add("base", [], THEORY)
 
-                    with ProgramBuilder(control) as bld:
-                        hbt = HeadBodyTransformer()
+            with ProgramBuilder(control) as bld:
+                hbt = HeadBodyTransformer()
 
-                        parse_files([encoding], lambda ast: bld.add(hbt.visit(ast)))
-                        pos = Position("<string>", 1, 1)
-                        loc = Location(pos, pos)
-                        for rule in hbt.rules_to_add:
-                            bld.add(Rule(loc, rule[0], rule[1]))  # nocoverage # Not sure when this is needed
+                parse_files([encoding], lambda ast: bld.add(hbt.visit(ast)))
+                pos = Position("<string>", 1, 1)
+                loc = Location(pos, pos)
+                for rule in hbt.rules_to_add:
+                    bld.add(Rule(loc, rule[0], rule[1]))  # nocoverage # Not sure when this is needed
 
-                    control.ground([("base", [])])
-                    translator = Translator(control, self.config, Statistic())
-                    translator.translate(control.theory_atoms)
+            control.ground([("base", [])])
+            translator = Translator(control, self.config, Statistic())
+            translator.translate(control.theory_atoms)
 
-                    self._propagator.prepare(control)
-                    control.solve(on_model=self.on_model, on_statistics=self._propagator.on_statistics)
+            self._propagator.prepare(control)
+            control.solve(on_model=self.on_model, on_statistics=self._propagator.on_statistics)

src/coomsuite/encodings/base/clingo/user.lp

@@ -1,2 +1,3 @@
-value(X,V) :- user_value(X,V).
-include(X) :- user_include(X).
+value(X,V) :- user_value(X,V), type(X,T), discrete(T), domain(T,V).
+value(X,V) :- user_value(X,V), type(X,T), integer(T), range(T,Min,Max), Min <= V <= Max.
+include(X) :- user_include(X), type(X,T), part(T).