Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open bounds #33

Merged
merged 9 commits into from
Jan 21, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 46 additions & 0 deletions examples/asp/cargobike-coom.lp
Original file line number Diff line number Diff line change
@@ -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").
38 changes: 38 additions & 0 deletions examples/coom/cargobike.coom
Original file line number Diff line number Diff line change
@@ -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
// }
6 changes: 3 additions & 3 deletions examples/coom/travel-bike-simplified.coom
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
3 changes: 2 additions & 1 deletion examples/coom/user-input.coom
Original file line number Diff line number Diff line change
@@ -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
66 changes: 47 additions & 19 deletions src/coomsuite/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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__":
Expand Down
139 changes: 26 additions & 113 deletions src/coomsuite/application.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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)
5 changes: 3 additions & 2 deletions src/coomsuite/encodings/base/clingo/user.lp
Original file line number Diff line number Diff line change
@@ -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).
Loading
Loading