From f7d5e4fc12b47fb5c66b422b27a5c61941d60ed7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20R=C3=BChling?= Date: Tue, 7 Jan 2025 14:22:18 +0100 Subject: [PATCH 1/9] added cargobike with open bounds --- examples/coom/cargobike.coom | 38 +++++++++++++++++++++++ examples/coom/travel-bike-simplified.coom | 6 ++-- 2 files changed, 41 insertions(+), 3 deletions(-) create mode 100644 examples/coom/cargobike.coom diff --git a/examples/coom/cargobike.coom b/examples/coom/cargobike.coom new file mode 100644 index 0000000..9e90768 --- /dev/null +++ b/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 CargoBike { + // require sum(bags.size.maxWeight) = totalWeight + require sum(bags.size.volume) = totalVolume + + // require totalWeight >= wantedWeight + require totalVolume >= requestedVolume + +} + +// behavior CargoBike { +// imply countBags = count(bags) +// minimize countBags +// } diff --git a/examples/coom/travel-bike-simplified.coom b/examples/coom/travel-bike-simplified.coom index 5ce75e3..9779de3 100644 --- a/examples/coom/travel-bike-simplified.coom +++ b/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 { From 6dd04013773dac2b04908abd38677d5e6df782a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20R=C3=BChling?= Date: Tue, 7 Jan 2025 21:56:38 +0100 Subject: [PATCH 2/9] added converted cargobike file --- examples/asp/cargobike-coom.lp | 40 ++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 examples/asp/cargobike-coom.lp diff --git a/examples/asp/cargobike-coom.lp b/examples/asp/cargobike-coom.lp new file mode 100644 index 0000000..1a1faaf --- /dev/null +++ b/examples/asp/cargobike-coom.lp @@ -0,0 +1,40 @@ +%%% 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","size","Size",1,1). + +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,"CargoBike"). +coom_require(0,"sum(bags.size.volume)=totalVolume"). +coom_binary("sum(bags.size.volume)=totalVolume","sum(bags.size.volume)","=","totalVolume"). +coom_function("CargoBike","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,"CargoBike"). +coom_require(1,"totalVolume>=requestedVolume"). +coom_binary("totalVolume>=requestedVolume","totalVolume",">=","requestedVolume"). +coom_path("totalVolume",0,"totalVolume"). +coom_path("requestedVolume",0,"requestedVolume"). From 005e6ae5736a77d6c718af52e6859485e9f2d0cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20R=C3=BChling?= Date: Fri, 10 Jan 2025 15:39:01 +0100 Subject: [PATCH 3/9] udpated cargobike example --- examples/asp/cargobike-coom.lp | 12 +++++++++--- examples/coom/cargobike.coom | 12 ++++++------ examples/coom/user-input.coom | 3 ++- 3 files changed, 17 insertions(+), 10 deletions(-) diff --git a/examples/asp/cargobike-coom.lp b/examples/asp/cargobike-coom.lp index 1a1faaf..40b979a 100644 --- a/examples/asp/cargobike-coom.lp +++ b/examples/asp/cargobike-coom.lp @@ -7,8 +7,14 @@ 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"). @@ -23,17 +29,17 @@ coom_attribute_value("Size","large","weight",25). coom_attribute_value("Size","large","volume",20). coom_behavior(0). -coom_context(0,"CargoBike"). +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("CargoBike","sum(bags.size.volume)","sum","bags.size.volume"). +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,"CargoBike"). +coom_context(1,"product"). coom_require(1,"totalVolume>=requestedVolume"). coom_binary("totalVolume>=requestedVolume","totalVolume",">=","requestedVolume"). coom_path("totalVolume",0,"totalVolume"). diff --git a/examples/coom/cargobike.coom b/examples/coom/cargobike.coom index 9e90768..5246e92 100644 --- a/examples/coom/cargobike.coom +++ b/examples/coom/cargobike.coom @@ -1,10 +1,10 @@ product { // num /kg 0-200 totalWeight // num /kg 0-200 wantedWeight - num /l 0-200 totalVolume - num /l 0-200 requestedVolume + num /l 0-200 totalVolume + num /l 0-200 requestedVolume // num countBags - 0..* Bag bags + 0..* Bag bags } structure Bag { @@ -12,7 +12,7 @@ structure Bag { Size size } -// enumeration Color { Green Blue Red } +enumeration Color { Green Blue Red } enumeration Size { attribute num weight @@ -23,7 +23,7 @@ enumeration Size { large = ( 25 20 ) } -behavior CargoBike { +behavior { // require sum(bags.size.maxWeight) = totalWeight require sum(bags.size.volume) = totalVolume @@ -32,7 +32,7 @@ behavior CargoBike { } -// behavior CargoBike { +// behavior { // imply countBags = count(bags) // minimize countBags // } diff --git a/examples/coom/user-input.coom b/examples/coom/user-input.coom index 5c22947..53f679a 100644 --- a/examples/coom/user-input.coom +++ b/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 From 4b1bf18aac4d6fefcd3403e82d08a74d34ab6cac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20R=C3=BChling?= Date: Mon, 13 Jan 2025 19:50:24 +0100 Subject: [PATCH 4/9] refactored solving option. separated preprocessing from main application class --- src/coomsuite/__main__.py | 52 ++++++++----- src/coomsuite/application.py | 139 +++++++---------------------------- src/coomsuite/preprocess.py | 75 +++++++++++++++++++ 3 files changed, 134 insertions(+), 132 deletions(-) create mode 100644 src/coomsuite/preprocess.py diff --git a/src/coomsuite/__main__.py b/src/coomsuite/__main__.py index 6d3f9a4..2d7f57c 100644 --- a/src/coomsuite/__main__.py +++ b/src/coomsuite/__main__.py @@ -3,12 +3,13 @@ """ import sys -from tempfile import TemporaryDirectory +from tempfile import NamedTemporaryFile, TemporaryDirectory 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 @@ -43,27 +44,40 @@ 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 + 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, + # clingo_options = ( + # [convert_instance(args.input, "model", temp_dir)] + # + ([convert_instance(args.user_input, "user", temp_dir)] if args.user_input else []) + # + unknown_args + # ) + + processed_facts = preprocess( + serialized_facts, + discrete=args.solver == "clingo", ) + if args.show_facts: + print("\n".join(processed_facts)) # nocoverage + else: + check_user_input(processed_facts) + + with NamedTemporaryFile(mode="w", delete=False) as tmp: + tmp_name = tmp.name + tmp.write("".join(processed_facts)) + + clingo_main( + COOMSolverApp( + options={ + "solver": args.solver, + "output_format": args.output, + } + ), + [tmp_name] + unknown_args, + ) + if __name__ == "__main__": main() diff --git a/src/coomsuite/application.py b/src/coomsuite/application.py index bac1a7c..642d885 100644 --- a/src/coomsuite/application.py +++ b/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("", 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("", 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) diff --git a/src/coomsuite/preprocess.py b/src/coomsuite/preprocess.py new file mode 100644 index 0000000..d8e57ef --- /dev/null +++ b/src/coomsuite/preprocess.py @@ -0,0 +1,75 @@ +from typing import List + +from clingo import Control +from clingo.script import enable_python +from clingo.symbol import Symbol + +from .utils import get_encoding + + +def preprocess(files: List[str], discrete: bool = True) -> List[str]: + """ + Preprocesses COOM ASP facts into a "grounded" configuration fact format + """ + # pylint: disable=not-context-manager + input_files = files + ctl = Control(message_limit=0) + for f in input_files: + ctl.load(f) + + # if self._options["preprocess"] or self._options["show_facts"]: + enable_python() + ctl.load(get_encoding("preprocess.lp")) + # if self._options["solver"] == "clingo": + if discrete: + ctl.add("base", [], "discrete.") # nocoverage + + ctl.ground() + with ctl.solve(yield_=True) as handle: + facts = [str(s) + "." for s in handle.model().symbols(shown=True)] + + return facts + + +def check_user_input(facts: str): + """ + Checks if the user input is valid and returns a clingo.SolveResult + """ + ctl = Control(message_limit=0) + ctl.load(get_encoding("user-check.lp")) + ctl.add("".join(facts)) + ctl.ground() + with ctl.solve(yield_=True) as handle: + unsat = [_parse_user_input_unsat(s) for s in handle.model().symbols(shown=True)] + + if unsat != []: + error_msg = "User input not valid.\n" + "\n".join(unsat) + raise ValueError(error_msg) + + +def _parse_user_input_unsat(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 From a81715d9772dfee851081be4293aeff523cc3a05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20R=C3=BChling?= Date: Mon, 13 Jan 2025 20:59:48 +0100 Subject: [PATCH 5/9] refactored tests --- src/coomsuite/preprocess.py | 3 +- tests/__init__.py | 39 ++++++++++--------- tests/clintests/tests_solve.py | 54 +------------------------- tests/test_solve.py | 46 +--------------------- tests/test_user_input.py | 70 ++++++++++++++++++++++++++++++++++ 5 files changed, 95 insertions(+), 117 deletions(-) create mode 100644 tests/test_user_input.py diff --git a/src/coomsuite/preprocess.py b/src/coomsuite/preprocess.py index d8e57ef..01fcd2f 100644 --- a/src/coomsuite/preprocess.py +++ b/src/coomsuite/preprocess.py @@ -17,10 +17,9 @@ def preprocess(files: List[str], discrete: bool = True) -> List[str]: for f in input_files: ctl.load(f) - # if self._options["preprocess"] or self._options["show_facts"]: enable_python() ctl.load(get_encoding("preprocess.lp")) - # if self._options["solver"] == "clingo": + if discrete: ctl.add("base", [], "discrete.") # nocoverage diff --git a/tests/__init__.py b/tests/__init__.py index 5c21703..b944664 100644 --- a/tests/__init__.py +++ b/tests/__init__.py @@ -9,10 +9,11 @@ from antlr4 import InputStream from clingo import Application, Control -from clintest.solver import Solver -from clintest.test import Test +from clintest.solver import Clingo, Solver +from clintest.test import Context, Test -from coomsuite.application import COOMApp +from coomsuite.application import COOMSolverApp +from coomsuite.preprocess import preprocess from coomsuite.utils import run_antlr4_visitor @@ -39,7 +40,8 @@ def unpack_test(test_name: str, tests: dict[str, Any], fclingo: bool = False) -> test = test_dict.get("ftest", test_dict["test"]) else: test = test_dict["test"] - return test, program, files + test_with_name = Context(test, str_=lambda test: f"{test_name} \n\n {test.__str__()}") + return test_with_name, program, files def run_test( @@ -62,15 +64,23 @@ def run_test( options = { "solver": solver, "output_format": kwargs.get("output_format", "asp"), - "show_facts": False, - "preprocess": is_preprocess, } - coom_app = COOMApp(options=options, istest=True) file_paths = ( - [join("examples", "tests", "solve" if not is_preprocess else "preprocess", f) for f in files] if files else None + [join("examples", "tests", "solve" if not is_preprocess else "preprocess", f) for f in files] if files else [] ) + if program: + with tempfile.NamedTemporaryFile(mode="w", delete=False) as tmp: + tmp_name = tmp.name + tmp.write(program) + file_paths.append(tmp_name) ctl_args = [] if ctl_args is None else ctl_args - solver = AppSolver(application=coom_app, files=file_paths, program=program, arguments=ctl_args) + + if is_preprocess: + solver = Clingo(program="".join(preprocess(file_paths, discrete=False))) + else: + coom_app = COOMSolverApp(options=options, istest=True) + solver = AppSolver(application=coom_app, files=file_paths, arguments=ctl_args) + test_copy = deepcopy(test) solver.solve(test_copy) test_copy.assert_() @@ -143,19 +153,12 @@ class AppSolver(Solver): def __init__( self, application: Application, - files: Optional[List[str]] = None, - program: Optional[str] = None, + files: List[str], arguments: Optional[List[str]] = None, ) -> None: self.__application = application self.__arguments = [] if arguments is None else arguments - self.__program = "" if program is None else program - self.__files = [] if files is None else files - if self.__program: - with tempfile.NamedTemporaryFile(mode="w", delete=False) as tmp: - tmp_name = tmp.name - tmp.write(self.__program) - self.__files.append(tmp_name) + self.__files = files def solve(self, test: Test) -> None: """Solves with clintest.""" diff --git a/tests/clintests/tests_solve.py b/tests/clintests/tests_solve.py index 3f9a5aa..8c8a58b 100644 --- a/tests/clintests/tests_solve.py +++ b/tests/clintests/tests_solve.py @@ -10,7 +10,7 @@ from typing import Any -from clintest.assertion import Equals, SubsetOf, True_ +from clintest.assertion import Equals, SubsetOf from clintest.quantifier import Exact from clintest.test import And, Assert @@ -717,56 +717,4 @@ part("A"). user_include("root.a[0]").""", }, - "set_invalid_variable": { - "test": True_(), # Output does not matter, tests whether Exception is raised - "program": """ - user_value("root.color[0]","Yellow").""", - }, - "add_invalid_variable": { - "test": True_(), # Output does not matter, tests whether Exception is raised - "program": """ - user_include("root.basket[0]").""", - }, - "set_invalid_type": { - "test": True_(), # Output does not matter, tests whether Exception is raised - "program": """ - part("product"). - part("Basket"). - type("root.basket[0]","Basket"). - parent("root.basket[0]","root"). - index("root.basket[0]",0). - user_value("root.basket[0]","Yellow").""", - }, - "add_invalid_type": { - "test": True_(), # Output does not matter, tests whether Exception is raised - "program": """ - part("product"). - discrete("Basket"). - type("root.basket[0]","Basket"). - parent("root.basket[0]","root"). - index("root.basket[0]",0). - user_include("root.basket[0]").""", - }, - "set_invalid_value_discrete": { - "test": True_(), # Output does not matter, tests whether Exception is raised - "program": """ - part("product"). - discrete("Color"). - domain("Color","Red"). - type("root.color[0]","Color"). - parent("root.color[0]","root"). - index("root.color[0]",0). - user_value("root.color[0]","Yellow").""", - }, - "set_invalid_value_num": { - "test": True_(), # Output does not matter, tests whether Exception is raised - "program": """ - part("product"). - integer("product.size"). - range("product.size",1,10). - type("root.size[0]","product.size"). - parent("root.size[0]","root"). - index("root.size[0]",0). - user_value("root.size[0]",11).""", - }, } diff --git a/tests/test_solve.py b/tests/test_solve.py index cce6e15..f1713a5 100644 --- a/tests/test_solve.py +++ b/tests/test_solve.py @@ -121,33 +121,12 @@ def test_aggregates(self) -> None: def test_user_input(self) -> None: """ - Test user input (clingo) + Test solving user input """ - - def user_check(test: str, expected_msg: str) -> None: - """ - Runs a test checking the user input for validity. - """ - with self.assertRaises(ValueError) as ctx: - self.run_test(test) - self.assertEqual(str(ctx.exception), expected_msg) - self.run_test("user_value_discrete") self.run_test("user_value_integer") self.run_test("user_include") - user_check("set_invalid_variable", "User input not valid.\nVariable root.color[0] is not valid.") - user_check("add_invalid_variable", "User input not valid.\nVariable root.basket[0] is not valid.") - user_check("set_invalid_type", "User input not valid.\nNo value can be set for variable root.basket[0].") - user_check("add_invalid_type", "User input not valid.\nVariable root.basket[0] cannot be added.") - user_check( - "set_invalid_value_discrete", - "User input not valid.\nValue 'Yellow' is not in domain of variable root.color[0].", - ) - user_check( - "set_invalid_value_num", "User input not valid.\nValue '11' is not in domain of variable root.size[0]." - ) - class TestFclingo(TestCase): """ @@ -260,29 +239,8 @@ def test_aggregates(self) -> None: def test_user_input(self) -> None: """ - Test user input (fclingo) + Test solving user input """ - - def user_check(test: str, expected_msg: str) -> None: - """ - Runs a test checking the user input for validity. - """ - with self.assertRaises(ValueError) as ctx: - self.run_test(test) - self.assertEqual(str(ctx.exception), expected_msg) - self.run_test("user_value_discrete") self.run_test("user_value_integer") self.run_test("user_include") - - user_check("set_invalid_variable", "User input not valid.\nVariable root.color[0] is not valid.") - user_check("add_invalid_variable", "User input not valid.\nVariable root.basket[0] is not valid.") - user_check("set_invalid_type", "User input not valid.\nNo value can be set for variable root.basket[0].") - user_check("add_invalid_type", "User input not valid.\nVariable root.basket[0] cannot be added.") - user_check( - "set_invalid_value_discrete", - "User input not valid.\nValue 'Yellow' is not in domain of variable root.color[0].", - ) - user_check( - "set_invalid_value_num", "User input not valid.\nValue '11' is not in domain of variable root.size[0]." - ) diff --git a/tests/test_user_input.py b/tests/test_user_input.py new file mode 100644 index 0000000..4a30d42 --- /dev/null +++ b/tests/test_user_input.py @@ -0,0 +1,70 @@ +from unittest import TestCase + +from coomsuite.preprocess import check_user_input + + +class TestUserInputCheck(TestCase): + """ + Test user input check + """ + + def user_check(self, test: str, expected_msg: str) -> None: + """ + Runs a test checking the user input for validity. + """ + with self.assertRaises(ValueError) as ctx: + check_user_input(checks[test]) + self.assertEqual(str(ctx.exception), expected_msg) + + def test_user_input_check(self) -> None: + """ + Test user input check + """ + self.user_check("set_invalid_variable", "User input not valid.\nVariable root.color[0] is not valid.") + self.user_check("add_invalid_variable", "User input not valid.\nVariable root.basket[0] is not valid.") + self.user_check("set_invalid_type", "User input not valid.\nNo value can be set for variable root.basket[0].") + self.user_check("add_invalid_type", "User input not valid.\nVariable root.basket[0] cannot be added.") + self.user_check( + "set_invalid_value_discrete", + "User input not valid.\nValue 'Yellow' is not in domain of variable root.color[0].", + ) + self.user_check( + "set_invalid_value_num", "User input not valid.\nValue '11' is not in domain of variable root.size[0]." + ) + + +checks = { + "set_invalid_variable": """user_value("root.color[0]","Yellow").""", + "add_invalid_variable": """ + user_include("root.basket[0]").""", + "set_invalid_type": """ + part("product"). + part("Basket"). + type("root.basket[0]","Basket"). + parent("root.basket[0]","root"). + index("root.basket[0]",0). + user_value("root.basket[0]","Yellow").""", + "add_invalid_type": """ + part("product"). + discrete("Basket"). + type("root.basket[0]","Basket"). + parent("root.basket[0]","root"). + index("root.basket[0]",0). + user_include("root.basket[0]").""", + "set_invalid_value_discrete": """ + part("product"). + discrete("Color"). + domain("Color","Red"). + type("root.color[0]","Color"). + parent("root.color[0]","root"). + index("root.color[0]",0). + user_value("root.color[0]","Yellow").""", + "set_invalid_value_num": """ + part("product"). + integer("product.size"). + range("product.size",1,10). + type("root.size[0]","product.size"). + parent("root.size[0]","root"). + index("root.size[0]",0). + user_value("root.size[0]",11).""", +} From cdab7985f2c33924506fc656d91561d22edaae2a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20R=C3=BChling?= Date: Mon, 13 Jan 2025 21:03:13 +0100 Subject: [PATCH 6/9] fix linting and typing --- src/coomsuite/__main__.py | 9 +++------ src/coomsuite/preprocess.py | 6 +++++- tests/__init__.py | 2 +- tests/test_user_input.py | 4 ++++ 4 files changed, 13 insertions(+), 8 deletions(-) diff --git a/src/coomsuite/__main__.py b/src/coomsuite/__main__.py index 2d7f57c..07da02c 100644 --- a/src/coomsuite/__main__.py +++ b/src/coomsuite/__main__.py @@ -44,16 +44,12 @@ def main(): elif args.command == "solve": log.info("Converting and solving COOM file %s", args.input) with TemporaryDirectory() as temp_dir: + # 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 [] ) - # clingo_options = ( - # [convert_instance(args.input, "model", temp_dir)] - # + ([convert_instance(args.user_input, "user", temp_dir)] if args.user_input else []) - # + unknown_args - # ) - + # Preprocess serialized ASP facts processed_facts = preprocess( serialized_facts, discrete=args.solver == "clingo", @@ -68,6 +64,7 @@ def main(): tmp_name = tmp.name tmp.write("".join(processed_facts)) + # Solve the ASP instance clingo_main( COOMSolverApp( options={ diff --git a/src/coomsuite/preprocess.py b/src/coomsuite/preprocess.py index 01fcd2f..6841490 100644 --- a/src/coomsuite/preprocess.py +++ b/src/coomsuite/preprocess.py @@ -1,3 +1,7 @@ +""" +Contains functions for preprocessing COOM ASP facts and checking user input +""" + from typing import List from clingo import Control @@ -30,7 +34,7 @@ def preprocess(files: List[str], discrete: bool = True) -> List[str]: return facts -def check_user_input(facts: str): +def check_user_input(facts: str) -> None: """ Checks if the user input is valid and returns a clingo.SolveResult """ diff --git a/tests/__init__.py b/tests/__init__.py index b944664..449f65f 100644 --- a/tests/__init__.py +++ b/tests/__init__.py @@ -40,7 +40,7 @@ def unpack_test(test_name: str, tests: dict[str, Any], fclingo: bool = False) -> test = test_dict.get("ftest", test_dict["test"]) else: test = test_dict["test"] - test_with_name = Context(test, str_=lambda test: f"{test_name} \n\n {test.__str__()}") + test_with_name = Context(test, str_=lambda test: f"{test_name} \n\n {str(test)}") return test_with_name, program, files diff --git a/tests/test_user_input.py b/tests/test_user_input.py index 4a30d42..bfdd616 100644 --- a/tests/test_user_input.py +++ b/tests/test_user_input.py @@ -1,3 +1,7 @@ +""" +Test cases for checking the user input for validity. +""" + from unittest import TestCase from coomsuite.preprocess import check_user_input From d9f19b46490e4b2d76e4a6ccbb67a1786993fa56 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20R=C3=BChling?= Date: Tue, 14 Jan 2025 21:12:08 +0100 Subject: [PATCH 7/9] very simple incremental bound --- src/coomsuite/__main__.py | 53 +++++++++++-------- .../encodings/preprocess/instantiate.lp | 9 +++- src/coomsuite/preprocess.py | 4 +- 3 files changed, 39 insertions(+), 27 deletions(-) diff --git a/src/coomsuite/__main__.py b/src/coomsuite/__main__.py index 07da02c..875fdab 100644 --- a/src/coomsuite/__main__.py +++ b/src/coomsuite/__main__.py @@ -49,31 +49,38 @@ def main(): [convert_instance(args.user_input, "user", temp_dir)] if args.user_input else [] ) - # Preprocess serialized ASP facts - processed_facts = preprocess( - serialized_facts, - discrete=args.solver == "clingo", - ) - if args.show_facts: - print("\n".join(processed_facts)) # nocoverage + print("\n".join(preprocess(serialized_facts))) # nocoverage else: - 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 - clingo_main( - COOMSolverApp( - options={ - "solver": args.solver, - "output_format": args.output, - } - ), - [tmp_name] + unknown_args, - ) + ret = 20 + max_bound = 1 + + while ret == 20: + print(f"\nSolving with max_bound = {max_bound}") + + # 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 + ret = clingo_main( + COOMSolverApp( + options={ + "solver": args.solver, + "output_format": args.output, + } + ), + [tmp_name] + unknown_args, + ) + max_bound += 1 if __name__ == "__main__": diff --git a/src/coomsuite/encodings/preprocess/instantiate.lp b/src/coomsuite/encodings/preprocess/instantiate.lp index a6f4bba..55612f7 100644 --- a/src/coomsuite/encodings/preprocess/instantiate.lp +++ b/src/coomsuite/encodings/preprocess/instantiate.lp @@ -1,10 +1,15 @@ +% Max bound for unbounded cardinalities +#const max_bound = 100. + %%% Instantiate complete instance tree % Root is always included type_aux((),"product") :- coom_structure("product"). % Create auxiliary predicate for every feature -type_aux((F,(X,I)),T) :- coom_feature(Ctx,F,T,_,Max), type_aux(X,Ctx), I = 0..Max-1, T != "num". -type_aux((F,(X,I)),@join(Ctx,F)) :- coom_feature(Ctx,F,"num",_,Max), type_aux(X,Ctx), I = 0..Max-1. +type_aux((F,(X,I)),T) :- coom_feature(Ctx,F,T,_, Max), type_aux(X,Ctx), I = 0..Max-1, T != "num". +type_aux((F,(X,I)),T) :- coom_feature(Ctx,F,T,Min,#sup), type_aux(X,Ctx), I = 0..Min+max_bound-1, T != "num". +type_aux((F,(X,I)),@join(Ctx,F)) :- coom_feature(Ctx,F,"num",_, Max), type_aux(X,Ctx), I = 0..Max-1. +type_aux((F,(X,I)),@join(Ctx,F)) :- coom_feature(Ctx,F,"num",Min,#sup), type_aux(X,Ctx), I = 0..Min+max_bound-1. % Create auxiliary prediate for attribute variables type_aux((A,(X,0)),A) :- type_aux(X,T), coom_enumeration(T), coom_attribute_value(T,_,A,_). diff --git a/src/coomsuite/preprocess.py b/src/coomsuite/preprocess.py index 6841490..dcd864f 100644 --- a/src/coomsuite/preprocess.py +++ b/src/coomsuite/preprocess.py @@ -11,13 +11,13 @@ from .utils import get_encoding -def preprocess(files: List[str], discrete: bool = True) -> List[str]: +def preprocess(files: List[str], max_bound: int = 99, discrete: bool = False) -> List[str]: """ Preprocesses COOM ASP facts into a "grounded" configuration fact format """ # pylint: disable=not-context-manager input_files = files - ctl = Control(message_limit=0) + ctl = Control(["-c", f"max_bound={max_bound}"], message_limit=0) for f in input_files: ctl.load(f) From 13cd68934ab33a736cb7b78a5c19e181e1cb16be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20R=C3=BChling?= Date: Wed, 15 Jan 2025 14:18:33 +0100 Subject: [PATCH 8/9] user errors are warnings. fixed corresponding tests. added new test macro. --- src/coomsuite/__main__.py | 4 +- src/coomsuite/encodings/base/clingo/user.lp | 5 +- src/coomsuite/encodings/user-check.lp | 16 +- src/coomsuite/preprocess.py | 37 +-- tests/clintests/__init__.py | 16 +- tests/clintests/tests_preprocess.py | 76 +++--- tests/clintests/tests_solve.py | 264 ++++++++++---------- tests/test_solve.py | 7 + tests/test_user_input.py | 65 ++--- 9 files changed, 242 insertions(+), 248 deletions(-) diff --git a/src/coomsuite/__main__.py b/src/coomsuite/__main__.py index 875fdab..434cc04 100644 --- a/src/coomsuite/__main__.py +++ b/src/coomsuite/__main__.py @@ -56,7 +56,7 @@ def main(): max_bound = 1 while ret == 20: - print(f"\nSolving with max_bound = {max_bound}") + print(f"\nSolving with max_bound = {max_bound}\n") # Preprocess serialized ASP facts processed_facts = preprocess( @@ -64,7 +64,7 @@ def main(): max_bound=max_bound, discrete=args.solver == "clingo", ) - # check_user_input(processed_facts) + check_user_input(processed_facts) with NamedTemporaryFile(mode="w", delete=False) as tmp: tmp_name = tmp.name diff --git a/src/coomsuite/encodings/base/clingo/user.lp b/src/coomsuite/encodings/base/clingo/user.lp index 515f50d..b364688 100644 --- a/src/coomsuite/encodings/base/clingo/user.lp +++ b/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). diff --git a/src/coomsuite/encodings/user-check.lp b/src/coomsuite/encodings/user-check.lp index 5b346de..28a5621 100644 --- a/src/coomsuite/encodings/user-check.lp +++ b/src/coomsuite/encodings/user-check.lp @@ -1,16 +1,16 @@ % Check that variables exist -unsat("not exists",X) :- user_value(X,_), not type(X,_). -unsat("not exists",X) :- user_include(X), not type(X,_). +warning("not exists",X) :- user_value(X,_), not type(X,_). +warning("not exists",X) :- user_include(X), not type(X,_). % Check variable type -unsat("not part",X) :- user_include(X), type(X,T), not part(T). -unsat("not attribute",X) :- user_value(X,V), type(X,T), #false : discrete(T); #false : integer(T). +warning("not part",X) :- user_include(X), type(X,T), not part(T). +warning("not attribute",X) :- user_value(X,V), type(X,T), #false : discrete(T); #false : integer(T). % Check valid domain -unsat("outside domain",(X,V)) :- user_value(X,V), type(X,T), discrete(T), not domain(T,V). -unsat("outside domain",(X,V)) :- user_value(X,V), type(X,T), integer(T), range(T,Min,Max), V < Min. -unsat("outside domain",(X,V)) :- user_value(X,V), type(X,T), integer(T), range(T,Min,Max), V > Max. +warning("outside domain",(X,V)) :- user_value(X,V), type(X,T), discrete(T), not domain(T,V). +warning("outside domain",(X,V)) :- user_value(X,V), type(X,T), integer(T), range(T,Min,Max), V < Min. +warning("outside domain",(X,V)) :- user_value(X,V), type(X,T), integer(T), range(T,Min,Max), V > Max. % Check max cardinality not exceeded % For now this is covered by line 3 (only max amount of objects is grounded) -#show unsat/2. +#show warning/2. diff --git a/src/coomsuite/preprocess.py b/src/coomsuite/preprocess.py index dcd864f..2da7822 100644 --- a/src/coomsuite/preprocess.py +++ b/src/coomsuite/preprocess.py @@ -9,6 +9,9 @@ from clingo.symbol import Symbol from .utils import get_encoding +from .utils.logging import get_logger + +log = get_logger("main") def preprocess(files: List[str], max_bound: int = 99, discrete: bool = False) -> List[str]: @@ -43,30 +46,32 @@ def check_user_input(facts: str) -> None: ctl.add("".join(facts)) ctl.ground() with ctl.solve(yield_=True) as handle: - unsat = [_parse_user_input_unsat(s) for s in handle.model().symbols(shown=True)] + warnings = [_parse_user_input_warnings(s) for s in handle.model().symbols(shown=True)] - if unsat != []: - error_msg = "User input not valid.\n" + "\n".join(unsat) - raise ValueError(error_msg) + if warnings != []: + msg = "User input not valid.\n" + "\n".join(warnings) + # raise ValueError(error_msg) + # warn(msg) + log.warning(msg) -def _parse_user_input_unsat(unsat: Symbol) -> str: +def _parse_user_input_warnings(warning: Symbol) -> str: """ - Parses the unsat/2 predicates of the user input check + Parses the warning/2 predicates of the user input check """ - unsat_type = unsat.arguments[0].string - info = unsat.arguments[1] + warning_type = warning.arguments[0].string + info = warning.arguments[1] - if unsat_type == "not exists": + if warning_type == "not exists": variable = info.string - msg = f"Variable {variable} is not valid." - elif unsat_type == "not part": + msg = f"Variable {variable} is not valid: Does not exist." + elif warning_type == "not part": variable = info.string - msg = f"Variable {variable} cannot be added." - elif unsat_type == "not attribute": + msg = f"Variable {variable} cannot be added: Not a part." + elif warning_type == "not attribute": variable = info.string - msg = f"No value can be set for variable {variable}." - elif unsat_type == "outside domain": + msg = f"No value can be set for variable {variable}: Not an attribute." + elif warning_type == "outside domain": variable = info.arguments[0].string if str(info.arguments[1].type) == "SymbolType.Number": value = str(info.arguments[1].number) @@ -74,5 +79,5 @@ def _parse_user_input_unsat(unsat: Symbol) -> str: 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 + raise ValueError(f"Unknown warning type: {warning_type}") # nocoverage return msg diff --git a/tests/clintests/__init__.py b/tests/clintests/__init__.py index 4fe897a..c60716e 100644 --- a/tests/clintests/__init__.py +++ b/tests/clintests/__init__.py @@ -8,7 +8,7 @@ from clingo.solving import Model from clintest.assertion import Equals, False_, SubsetOf, SupersetOf, True_ from clintest.quantifier import All, Exact -from clintest.test import Assert, Test +from clintest.test import And, Assert, Test TEST_EMPTY = Assert(All(), SubsetOf(set())) TEST_UNSAT = Assert(Exact(0), False_()) @@ -21,14 +21,18 @@ def NumModels(n: int) -> Test: # pylint: disable=invalid-name return Assert(Exact(n), True_()) -def SingleModelEquals(model: set[Symbol | str]) -> Test: # pylint: disable=invalid-name +def StableModels(*args: set[Symbol | str], fclingo: bool = False) -> Test: # pylint: disable=invalid-name """ - clintest.Test for checking that a program has a single model that is equal to the given argument + clintest.Test for checking that a program has a certain set of stable models Args: - model (set[str]): The single model as a set of strings or clingo symbols + args: The set of stable models as a set of sets of strings or clingo symbols + fclingo (bool): Whether to prepare the test for use with the fclingo solver """ - return Assert(All(), Equals(model)) + if not fclingo: + return And(NumModels(len(args)), *(Assert(Exact(1), Equals(a)) for a in args)) + else: + return And(NumModels(len(args)), *(Assert(Exact(1), SupersetOfTheory(a, check_theory=True)) for a in args)) class SupersetOfTheory(SupersetOf): @@ -48,7 +52,7 @@ def __init__(self, symbols: Set[Union[Symbol, str]], check_theory: bool = False) def holds_for(self, model: Model) -> bool: if self.__check_theory: return set(model.symbols(shown=True, theory=True)).issuperset(self.__symbols) - return super().holds_for(model) + return super().holds_for(model) # nocoverage # class EqualsTheory(Equals): diff --git a/tests/clintests/tests_preprocess.py b/tests/clintests/tests_preprocess.py index 1e82122..9c98db4 100644 --- a/tests/clintests/tests_preprocess.py +++ b/tests/clintests/tests_preprocess.py @@ -10,16 +10,16 @@ # pylint: disable=line-too-long, too-many-lines from typing import Any -from . import TEST_EMPTY, SingleModelEquals +from . import TEST_EMPTY, StableModels TESTS_PREPROCESS: dict[str, dict[str, Any]] = { "empty": {"test": TEST_EMPTY, "program": ""}, "empty_product": { - "test": SingleModelEquals({'part("product")', 'type("root","product")'}), + "test": StableModels({'part("product")', 'type("root","product")'}), "program": 'coom_structure("product").', }, "structure_mandatory": { - "test": SingleModelEquals( + "test": StableModels( { 'part("product")', 'part("Wheel")', @@ -37,7 +37,7 @@ coom_structure("Wheel").""", }, "structure_optional": { - "test": SingleModelEquals( + "test": StableModels( { 'part("product")', 'part("Wheel")', @@ -55,7 +55,7 @@ coom_structure("Wheel").""", }, "structure_nested": { - "test": SingleModelEquals( + "test": StableModels( { 'part("product")', 'part("Carrier")', @@ -81,7 +81,7 @@ coom_structure("Bag").""", }, "structure_nested_optional": { - "test": SingleModelEquals( + "test": StableModels( { 'part("product")', 'part("Carrier")', @@ -111,7 +111,7 @@ coom_structure("Bag").""", }, "enumeration": { - "test": SingleModelEquals( + "test": StableModels( { 'discrete("Color")', 'part("product")', @@ -135,7 +135,7 @@ coom_option("Color", "Blue").""", }, "bool_enumeration": { - "test": SingleModelEquals( + "test": StableModels( { 'discrete("Bool")', 'part("product")', @@ -154,7 +154,7 @@ coom_feature("product","boolean","Bool",1,1).""", }, "attribute": { - "test": SingleModelEquals( + "test": StableModels( { 'discrete("Wheel")', 'integer("Wheel.size")', @@ -188,7 +188,7 @@ coom_attribute_value("Wheel","W14","size",14).""", }, "require_undef": { - "test": SingleModelEquals({'constant("Silver")', 'part("product")', 'type("root","product")'}), + "test": StableModels({'constant("Silver")', 'part("product")', 'type("root","product")'}), "program": """ coom_structure("product"). @@ -199,7 +199,7 @@ coom_constant("Silver").""", }, "require_with_number": { - "test": SingleModelEquals( + "test": StableModels( { 'discrete("Wheel")', 'integer("Wheel.size")', @@ -233,7 +233,7 @@ "files": ["require_with_number.lp"], }, "require_with_number_ge": { - "test": SingleModelEquals( + "test": StableModels( { 'discrete("Wheel")', 'integer("Wheel.size")', @@ -267,7 +267,7 @@ "files": ["require_with_number_ge.lp"], }, "require_with_constant": { - "test": SingleModelEquals( + "test": StableModels( { 'constant("W28")', 'discrete("Wheel")', @@ -287,7 +287,7 @@ "files": ["require_with_constant.lp"], }, "require_two_wheels": { - "test": SingleModelEquals( + "test": StableModels( { 'discrete("Wheel")', 'integer("Wheel.size")', @@ -333,7 +333,7 @@ "files": ["require_two_wheels.lp"], }, "conditional_require": { - "test": SingleModelEquals( + "test": StableModels( { 'constant("True")', 'constant("Small")', @@ -365,7 +365,7 @@ "files": ["conditional_require.lp"], }, "conditional_require_undef": { - "test": SingleModelEquals( + "test": StableModels( { 'constant("Silver")', 'constant("Big")', @@ -384,7 +384,7 @@ "files": ["conditional_require_undef.lp"], }, "require_multiple_instances": { - "test": SingleModelEquals( + "test": StableModels( { 'constant("W28")', 'discrete("Size")', @@ -421,7 +421,7 @@ "files": ["require_multiple_instances.lp"], }, "require_with_partonomy": { - "test": SingleModelEquals( + "test": StableModels( { 'constant("Red")', 'discrete("Color")', @@ -447,7 +447,7 @@ "files": ["require_with_partonomy.lp"], }, "require_with_partonomy2": { - "test": SingleModelEquals( + "test": StableModels( { 'constant("Red")', 'discrete("Color")', @@ -484,7 +484,7 @@ "files": ["require_with_partonomy2.lp"], }, "require_with_partonomy_multiple_instances": { - "test": SingleModelEquals( + "test": StableModels( { 'constant("Red")', 'discrete("Color")', @@ -555,7 +555,7 @@ "files": ["require_with_partonomy_multiple_instances.lp"], }, "combination": { - "test": SingleModelEquals( + "test": StableModels( { 'discrete("Wheel")', 'discrete("Bool")', @@ -591,7 +591,7 @@ "files": ["combination.lp"], }, "combination_with_structure": { - "test": SingleModelEquals( + "test": StableModels( { 'discrete("Size")', 'discrete("Bool")', @@ -644,7 +644,7 @@ "files": ["combination_with_structure.lp"], }, "combination_at_part_with_wildcard": { - "test": SingleModelEquals( + "test": StableModels( { 'discrete("Size")', 'discrete("Material")', @@ -706,7 +706,7 @@ "files": ["combination_at_part_with_wildcard.lp"], }, "combination_at_part_multiple_instances": { - "test": SingleModelEquals( + "test": StableModels( { 'discrete("Wheel")', 'discrete("Material")', @@ -789,7 +789,7 @@ "files": ["combination_at_part_multiple_instances.lp"], }, "simple_numeric_feature": { - "test": SingleModelEquals( + "test": StableModels( { 'integer("product.size")', 'part("product")', @@ -808,7 +808,7 @@ coom_range("product","size",1,3).""", }, "simple_arithmetic_plus": { - "test": SingleModelEquals( + "test": StableModels( { 'integer("product.a")', 'integer("product.b")', @@ -835,7 +835,7 @@ "files": ["simple_arithmetic_plus.lp"], }, "simple_arithmetic_minus": { - "test": SingleModelEquals( + "test": StableModels( { 'integer("product.a")', 'integer("product.b")', @@ -862,7 +862,7 @@ "files": ["simple_arithmetic_minus.lp"], }, "simple_arithmetic_multiplication": { - "test": SingleModelEquals( + "test": StableModels( { 'integer("product.a")', 'integer("product.b")', @@ -889,7 +889,7 @@ "files": ["simple_arithmetic_multiplication.lp"], }, "simple_arithmetic_plus_default_right": { - "test": SingleModelEquals( + "test": StableModels( { 'integer("product.a")', 'part("product")', @@ -908,7 +908,7 @@ "files": ["simple_arithmetic_plus_default_right.lp"], }, "simple_arithmetic_plus_default_left": { - "test": SingleModelEquals( + "test": StableModels( { 'integer("product.b")', 'part("product")', @@ -927,7 +927,7 @@ "files": ["simple_arithmetic_plus_default_left.lp"], }, "simple_arithmetic_minus_default_right": { - "test": SingleModelEquals( + "test": StableModels( { 'integer("product.a")', 'part("product")', @@ -944,7 +944,7 @@ "files": ["simple_arithmetic_minus_default_right.lp"], }, "simple_arithmetic_minus_default_left": { - "test": SingleModelEquals( + "test": StableModels( { 'integer("product.b")', 'part("product")', @@ -961,7 +961,7 @@ "files": ["simple_arithmetic_minus_default_left.lp"], }, "parentheses": { - "test": SingleModelEquals( + "test": StableModels( { 'integer("product.a")', 'integer("product.b")', @@ -987,7 +987,7 @@ "files": ["parentheses.lp"], }, "count": { - "test": SingleModelEquals( + "test": StableModels( { 'part("product")', 'part("Bag")', @@ -1014,7 +1014,7 @@ "files": ["count.lp"], }, "sum": { - "test": SingleModelEquals( + "test": StableModels( { 'integer("product.x")', 'part("product")', @@ -1042,15 +1042,15 @@ "files": ["sum.lp"], }, "set_constant": { - "test": SingleModelEquals({'user_value("root.color[0]","Yellow")'}), + "test": StableModels({'user_value("root.color[0]","Yellow")'}), "program": 'coom_user_value("root.color[0]","Yellow").', }, "set_number": { - "test": SingleModelEquals({'user_value("root.size[0]",5)'}), + "test": StableModels({'user_value("root.size[0]",5)'}), "program": 'coom_user_value("root.size[0]",5).', }, "add": { - "test": SingleModelEquals({'user_include("root.bag[0]")'}), + "test": StableModels({'user_include("root.bag[0]")'}), "program": 'coom_user_include("root.bag[0]").', }, } diff --git a/tests/clintests/tests_solve.py b/tests/clintests/tests_solve.py index 8c8a58b..91f90da 100644 --- a/tests/clintests/tests_solve.py +++ b/tests/clintests/tests_solve.py @@ -10,18 +10,15 @@ from typing import Any -from clintest.assertion import Equals, SubsetOf from clintest.quantifier import Exact from clintest.test import And, Assert -from . import TEST_EMPTY, TEST_UNSAT, NumModels, SingleModelEquals, SupersetOfTheory +from . import TEST_EMPTY, TEST_UNSAT, NumModels, StableModels, SupersetOfTheory TESTS_SOLVE: dict[str, dict[str, Any]] = { "empty": {"test": TEST_EMPTY, "program": ""}, "optional_part": { - "test": And( - NumModels(2), Assert(Exact(1), SubsetOf(set())), Assert(Exact(1), Equals({'include("root.a[0]")'})) - ), + "test": StableModels({'include("root.a[0]")'}, set()), "program": """ type("root","product"). type("root.a[0]","A"). @@ -31,7 +28,7 @@ part("A").""", }, "mandatory_part": { - "test": SingleModelEquals({'include("root.a[0]")'}), + "test": StableModels({'include("root.a[0]")'}), "program": """ type("root","product"). type("root.a[0]","A"). @@ -43,11 +40,7 @@ part("A").""", }, "part_with_cardinality": { - "test": And( - NumModels(2), - Assert(Exact(1), Equals({'include("root.a[0]")'})), - Assert(Exact(1), Equals({'include("root.a[0]")', 'include("root.a[1]")'})), - ), + "test": StableModels({'include("root.a[0]")'}, {'include("root.a[0]")', 'include("root.a[1]")'}), "program": """ type("root","product"). type("root.a[0]","A"). @@ -63,11 +56,7 @@ part("A").""", }, "optional_part_with_subpart": { - "test": And( - NumModels(2), - Assert(Exact(1), SubsetOf(set())), - Assert(Exact(1), Equals({'include("root.a[0]")', 'include("root.a[0].b[0]")'})), - ), + "test": StableModels(set(), {'include("root.a[0]")', 'include("root.a[0].b[0]")'}), "program": """ type("root","product"). type("root.a[0]","A"). @@ -83,11 +72,7 @@ part("B").""", }, "simple_discrete": { - "test": And( - NumModels(2), - Assert(Exact(1), Equals({'value("root.a[0]","A1")'})), - Assert(Exact(1), Equals({'value("root.a[0]","A2")'})), - ), + "test": StableModels({'value("root.a[0]","A1")'}, {'value("root.a[0]","A2")'}), "program": """ type("root","product"). type("root.a[0]","A"). @@ -101,12 +86,7 @@ part("product").""", }, "optional_discrete": { - "test": And( - NumModels(3), - Assert(Exact(1), Equals(set())), - Assert(Exact(1), Equals({'value("root.a[0]","A1")'})), - Assert(Exact(1), Equals({'value("root.a[0]","A2")'})), - ), + "test": StableModels(set(), {'value("root.a[0]","A1")'}, {'value("root.a[0]","A2")'}), "program": """ type("root","product"). type("root.a[0]","A"). @@ -118,12 +98,11 @@ part("product").""", }, "multiple_discrete": { - "test": And( - NumModels(4), - Assert(Exact(1), Equals({'value("root.a[0]","A1")', 'value("root.a[1]","A1")'})), - Assert(Exact(1), Equals({'value("root.a[0]","A1")', 'value("root.a[1]","A2")'})), - Assert(Exact(1), Equals({'value("root.a[0]","A2")', 'value("root.a[1]","A1")'})), - Assert(Exact(1), Equals({'value("root.a[0]","A2")', 'value("root.a[1]","A2")'})), + "test": StableModels( + {'value("root.a[0]","A1")', 'value("root.a[1]","A1")'}, + {'value("root.a[0]","A1")', 'value("root.a[1]","A2")'}, + {'value("root.a[0]","A2")', 'value("root.a[1]","A1")'}, + {'value("root.a[0]","A2")', 'value("root.a[1]","A2")'}, ), "program": """ type("root","product"). @@ -142,16 +121,8 @@ part("product").""", }, "simple_integer": { - "test": And( - NumModels(2), - Assert(Exact(1), SupersetOfTheory({'value("root.a[0]",1)'})), - Assert(Exact(1), SupersetOfTheory({'value("root.a[0]",2)'})), - ), - "ftest": And( - NumModels(2), - Assert(Exact(1), SupersetOfTheory({'value("root.a[0]",1)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.a[0]",2)'}, check_theory=True)), - ), + "test": StableModels({'value("root.a[0]",1)'}, {'value("root.a[0]",2)'}), + "ftest": StableModels({'value("root.a[0]",1)'}, {'value("root.a[0]",2)'}, fclingo=True), "program": """ type("root","product"). type("root.a[0]","A"). @@ -164,12 +135,7 @@ part("product").""", }, "optional_integer": { - "test": And( - NumModels(3), - Assert(Exact(1), Equals(set())), - Assert(Exact(1), Equals({'value("root.a[0]",1)'})), - Assert(Exact(1), Equals({'value("root.a[0]",2)'})), - ), + "test": StableModels(set(), {'value("root.a[0]",1)'}, {'value("root.a[0]",2)'}), "ftest": And( NumModels(3), # Assert(Exact(1), SubsetOf({})), # How to check empty set for fclingo (with regards to output atoms)? @@ -186,19 +152,18 @@ part("product").""", }, "multiple_integer": { - "test": And( - NumModels(4), - Assert(Exact(1), Equals({'value("root.a[0]",1)', 'value("root.a[1]",1)'})), - Assert(Exact(1), Equals({'value("root.a[0]",1)', 'value("root.a[1]",2)'})), - Assert(Exact(1), Equals({'value("root.a[0]",2)', 'value("root.a[1]",1)'})), - Assert(Exact(1), Equals({'value("root.a[0]",2)', 'value("root.a[1]",2)'})), + "test": StableModels( + {'value("root.a[0]",1)', 'value("root.a[1]",1)'}, + {'value("root.a[0]",1)', 'value("root.a[1]",2)'}, + {'value("root.a[0]",2)', 'value("root.a[1]",1)'}, + {'value("root.a[0]",2)', 'value("root.a[1]",2)'}, ), - "ftest": And( - NumModels(4), - Assert(Exact(1), SupersetOfTheory({'value("root.a[0]",1)', 'value("root.a[1]",1)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.a[0]",1)', 'value("root.a[1]",2)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.a[0]",2)', 'value("root.a[1]",1)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.a[0]",2)', 'value("root.a[1]",2)'}, check_theory=True)), + "ftest": StableModels( + {'value("root.a[0]",1)', 'value("root.a[1]",1)'}, + {'value("root.a[0]",1)', 'value("root.a[1]",2)'}, + {'value("root.a[0]",2)', 'value("root.a[1]",1)'}, + {'value("root.a[0]",2)', 'value("root.a[1]",2)'}, + fclingo=True, ), "program": """ type("root","product"). @@ -395,64 +360,56 @@ unary("!x","!","x").""", }, "table_discrete": { - "test": And( - NumModels(4), - Assert(Exact(1), Equals({'value("root.x[0]","A1")', 'value("root.y[0]","A2")'})), - Assert(Exact(1), Equals({'value("root.x[0]","A1")', 'value("root.y[0]","A3")'})), - Assert(Exact(1), Equals({'value("root.x[0]","A2")', 'value("root.y[0]","A1")'})), - Assert(Exact(1), Equals({'value("root.x[0]","A3")', 'value("root.y[0]","A2")'})), + "test": StableModels( + {'value("root.x[0]","A1")', 'value("root.y[0]","A2")'}, + {'value("root.x[0]","A1")', 'value("root.y[0]","A3")'}, + {'value("root.x[0]","A2")', 'value("root.y[0]","A1")'}, + {'value("root.x[0]","A3")', 'value("root.y[0]","A2")'}, ), "files": ["table_discrete.lp"], }, "table_integer": { - "test": And( - NumModels(4), - Assert(Exact(1), Equals({'value("root.x[0]",1)', 'value("root.y[0]",2)'})), - Assert(Exact(1), Equals({'value("root.x[0]",1)', 'value("root.y[0]",3)'})), - Assert(Exact(1), Equals({'value("root.x[0]",2)', 'value("root.y[0]",1)'})), - Assert(Exact(1), Equals({'value("root.x[0]",3)', 'value("root.y[0]",2)'})), + "test": StableModels( + {'value("root.x[0]",1)', 'value("root.y[0]",2)'}, + {'value("root.x[0]",1)', 'value("root.y[0]",3)'}, + {'value("root.x[0]",2)', 'value("root.y[0]",1)'}, + {'value("root.x[0]",3)', 'value("root.y[0]",2)'}, ), - "ftest": And( - NumModels(4), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]",1)', 'value("root.y[0]",2)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]",1)', 'value("root.y[0]",3)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]",2)', 'value("root.y[0]",1)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]",3)', 'value("root.y[0]",2)'}, check_theory=True)), + "ftest": StableModels( + {'value("root.x[0]",1)', 'value("root.y[0]",2)'}, + {'value("root.x[0]",1)', 'value("root.y[0]",3)'}, + {'value("root.x[0]",2)', 'value("root.y[0]",1)'}, + {'value("root.x[0]",3)', 'value("root.y[0]",2)'}, + fclingo=True, ), "files": ["table_integer.lp"], }, "table_mixed": { - "test": And( - NumModels(4), - Assert(Exact(1), Equals({'value("root.x[0]","A1")', 'value("root.y[0]",2)'})), - Assert(Exact(1), Equals({'value("root.x[0]","A1")', 'value("root.y[0]",3)'})), - Assert(Exact(1), Equals({'value("root.x[0]","A2")', 'value("root.y[0]",1)'})), - Assert(Exact(1), Equals({'value("root.x[0]","A3")', 'value("root.y[0]",2)'})), + "test": StableModels( + {'value("root.x[0]","A1")', 'value("root.y[0]",2)'}, + {'value("root.x[0]","A1")', 'value("root.y[0]",3)'}, + {'value("root.x[0]","A2")', 'value("root.y[0]",1)'}, + {'value("root.x[0]","A3")', 'value("root.y[0]",2)'}, ), - "ftest": And( - NumModels(4), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]","A1")', 'value("root.y[0]",2)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]","A1")', 'value("root.y[0]",3)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]","A2")', 'value("root.y[0]",1)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]","A3")', 'value("root.y[0]",2)'}, check_theory=True)), + "ftest": StableModels( + {'value("root.x[0]","A1")', 'value("root.y[0]",2)'}, + {'value("root.x[0]","A1")', 'value("root.y[0]",3)'}, + {'value("root.x[0]","A2")', 'value("root.y[0]",1)'}, + {'value("root.x[0]","A3")', 'value("root.y[0]",2)'}, + fclingo=True, ), "files": ["table_mixed.lp"], }, "table_wildcard": { - "test": And( - NumModels(3), - Assert(Exact(1), Equals({'value("root.x[0]","A1")', 'value("root.y[0]","A1")'})), - Assert(Exact(1), Equals({'value("root.x[0]","A2")', 'value("root.y[0]","A1")'})), - Assert(Exact(1), Equals({'value("root.x[0]","A2")', 'value("root.y[0]","A2")'})), + "test": StableModels( + {'value("root.x[0]","A1")', 'value("root.y[0]","A1")'}, + {'value("root.x[0]","A2")', 'value("root.y[0]","A1")'}, + {'value("root.x[0]","A2")', 'value("root.y[0]","A2")'}, ), "files": ["table_wildcard.lp"], }, "table_undef": { - "test": And( - NumModels(2), - Assert(Exact(1), Equals({'value("root.x[0]","A1")'})), - Assert(Exact(1), Equals({'value("root.x[0]","A2")'})), - ), + "test": StableModels({'value("root.x[0]","A1")'}, {'value("root.x[0]","A2")'}), "files": ["table_undef.lp"], }, "table_undef2": { @@ -634,47 +591,41 @@ number("6",6).""", }, "count": { - "test": SingleModelEquals({'include("root.x[0]")', 'include("root.x[1]")'}), + "test": StableModels({'include("root.x[0]")', 'include("root.x[1]")'}), "files": ["count.lp"], }, "sum": { - "test": And( - NumModels(2), - Assert(Exact(1), Equals({'value("root.x[0]",1)', 'value("root.x[1]",2)'})), - Assert(Exact(1), Equals({'value("root.x[0]",2)', 'value("root.x[1]",1)'})), + "test": StableModels( + {'value("root.x[0]",1)', 'value("root.x[1]",2)'}, {'value("root.x[0]",2)', 'value("root.x[1]",1)'} ), - "ftest": And( - NumModels(2), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]",1)', 'value("root.x[1]",2)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]",2)', 'value("root.x[1]",1)'}, check_theory=True)), + "ftest": StableModels( + {'value("root.x[0]",1)', 'value("root.x[1]",2)'}, + {'value("root.x[0]",2)', 'value("root.x[1]",1)'}, + fclingo=True, ), "files": ["sum.lp"], }, "min": { - "test": And( - NumModels(3), - Assert(Exact(1), Equals({'value("root.x[0]",4)', 'value("root.x[1]",3)'})), - Assert(Exact(1), Equals({'value("root.x[0]",3)', 'value("root.x[1]",3)'})), - Assert(Exact(1), Equals({'value("root.x[0]",3)', 'value("root.x[1]",4)'})), + "test": StableModels( + {'value("root.x[0]",4)', 'value("root.x[1]",3)'}, + {'value("root.x[0]",3)', 'value("root.x[1]",3)'}, + {'value("root.x[0]",3)', 'value("root.x[1]",4)'}, ), - "ftest": And( - NumModels(3), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]",4)', 'value("root.x[1]",3)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]",3)', 'value("root.x[1]",3)'}, check_theory=True)), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]",3)', 'value("root.x[1]",4)'}, check_theory=True)), + "ftest": StableModels( + {'value("root.x[0]",4)', 'value("root.x[1]",3)'}, + {'value("root.x[0]",3)', 'value("root.x[1]",3)'}, + {'value("root.x[0]",3)', 'value("root.x[1]",4)'}, + fclingo=True, ), "files": ["min.lp"], }, "max": { - "test": SingleModelEquals({'value("root.x[0]",3)', 'value("root.x[1]",3)'}), - "ftest": And( - NumModels(1), - Assert(Exact(1), SupersetOfTheory({'value("root.x[0]",3)', 'value("root.x[1]",3)'}, check_theory=True)), - ), + "test": StableModels({'value("root.x[0]",3)', 'value("root.x[1]",3)'}), + "ftest": StableModels({'value("root.x[0]",3)', 'value("root.x[1]",3)'}, fclingo=True), "files": ["max.lp"], }, "user_value_discrete": { - "test": SingleModelEquals({'value("root.a[0]","A1")'}), + "test": StableModels({'value("root.a[0]","A1")'}), "program": """ type("root","product"). type("root.a[0]","A"). @@ -689,11 +640,8 @@ user_value("root.a[0]","A1").""", }, "user_value_integer": { - "test": SingleModelEquals({'value("root.a[0]",1)'}), - "ftest": And( - NumModels(1), - Assert(Exact(1), SupersetOfTheory({'value("root.a[0]",1)'}, check_theory=True)), - ), + "test": StableModels({'value("root.a[0]",1)'}), + "ftest": StableModels({'value("root.a[0]",1)'}, fclingo=True), "program": """ type("root","product"). type("root.a[0]","A"). @@ -707,7 +655,7 @@ user_value("root.a[0]",1).""", }, "user_include": { - "test": SingleModelEquals({'include("root.a[0]")'}), + "test": StableModels({'include("root.a[0]")'}), "program": """ type("root","product"). type("root.a[0]","A"). @@ -717,4 +665,56 @@ part("A"). user_include("root.a[0]").""", }, + "set_invalid_variable": {"test": StableModels(set()), "program": """user_value("root.color[0]","Yellow")."""}, + "add_invalid_variable": { + "test": StableModels(set()), + "program": """ + user_include("root.basket[0]").""", + }, + "set_invalid_type": { + "test": StableModels(set(), {'include("root.basket[0]")'}), + "program": """ + part("product"). + part("Basket"). + type("root.basket[0]","Basket"). + parent("root.basket[0]","root"). + index("root.basket[0]",0). + user_value("root.basket[0]","Yellow").""", + }, + "add_invalid_type": { + "test": StableModels(set()), + "program": """ + part("product"). + discrete("Basket"). + type("root.basket[0]","Basket"). + parent("root.basket[0]","root"). + index("root.basket[0]",0). + user_include("root.basket[0]").""", + }, + "set_invalid_value_discrete": { + "test": StableModels({'value("root.color[0]","Red")'}), + "program": """ + part("product"). + discrete("Color"). + domain("Color","Red"). + type("root.color[0]","Color"). + parent("root.color[0]","root"). + index("root.color[0]",0). + user_value("root.color[0]","Yellow"). + constraint(("root.color",1),"lowerbound"). + set("root.color","root.color[0]").""", + }, + "set_invalid_value_num": { + "test": StableModels({'value("root.size[0]",1)'}, {'value("root.size[0]",2)'}, {'value("root.size[0]",3)'}), + "program": """ + part("product"). + integer("product.size"). + range("product.size",1,3). + type("root.size[0]","product.size"). + parent("root.size[0]","root"). + index("root.size[0]",0). + user_value("root.size[0]",11). + constraint(("root.size",1),"lowerbound"). + set("root.size","root.size[0]").""", + }, } diff --git a/tests/test_solve.py b/tests/test_solve.py index f1713a5..8893dfd 100644 --- a/tests/test_solve.py +++ b/tests/test_solve.py @@ -127,6 +127,13 @@ def test_user_input(self) -> None: self.run_test("user_value_integer") self.run_test("user_include") + self.run_test("set_invalid_variable") + self.run_test("add_invalid_variable") + self.run_test("set_invalid_type") + self.run_test("add_invalid_type") + self.run_test("set_invalid_value_discrete") + self.run_test("set_invalid_value_num") + class TestFclingo(TestCase): """ diff --git a/tests/test_user_input.py b/tests/test_user_input.py index bfdd616..992283d 100644 --- a/tests/test_user_input.py +++ b/tests/test_user_input.py @@ -5,6 +5,11 @@ from unittest import TestCase from coomsuite.preprocess import check_user_input +from coomsuite.utils.logging import get_logger + +from .clintests.tests_solve import TESTS_SOLVE + +log = get_logger("main") class TestUserInputCheck(TestCase): @@ -16,18 +21,27 @@ def user_check(self, test: str, expected_msg: str) -> None: """ Runs a test checking the user input for validity. """ - with self.assertRaises(ValueError) as ctx: - check_user_input(checks[test]) - self.assertEqual(str(ctx.exception), expected_msg) + with self.assertLogs(log, level="WARNING") as ctx: + check_user_input(TESTS_SOLVE[test]["program"]) + self.assertEqual(ctx.output, [f"WARNING:main:{expected_msg}"]) def test_user_input_check(self) -> None: """ Test user input check """ - self.user_check("set_invalid_variable", "User input not valid.\nVariable root.color[0] is not valid.") - self.user_check("add_invalid_variable", "User input not valid.\nVariable root.basket[0] is not valid.") - self.user_check("set_invalid_type", "User input not valid.\nNo value can be set for variable root.basket[0].") - self.user_check("add_invalid_type", "User input not valid.\nVariable root.basket[0] cannot be added.") + self.user_check( + "set_invalid_variable", "User input not valid.\nVariable root.color[0] is not valid: Does not exist." + ) + self.user_check( + "add_invalid_variable", "User input not valid.\nVariable root.basket[0] is not valid: Does not exist." + ) + self.user_check( + "set_invalid_type", + "User input not valid.\nNo value can be set for variable root.basket[0]: Not an attribute.", + ) + self.user_check( + "add_invalid_type", "User input not valid.\nVariable root.basket[0] cannot be added: Not a part." + ) self.user_check( "set_invalid_value_discrete", "User input not valid.\nValue 'Yellow' is not in domain of variable root.color[0].", @@ -35,40 +49,3 @@ def test_user_input_check(self) -> None: self.user_check( "set_invalid_value_num", "User input not valid.\nValue '11' is not in domain of variable root.size[0]." ) - - -checks = { - "set_invalid_variable": """user_value("root.color[0]","Yellow").""", - "add_invalid_variable": """ - user_include("root.basket[0]").""", - "set_invalid_type": """ - part("product"). - part("Basket"). - type("root.basket[0]","Basket"). - parent("root.basket[0]","root"). - index("root.basket[0]",0). - user_value("root.basket[0]","Yellow").""", - "add_invalid_type": """ - part("product"). - discrete("Basket"). - type("root.basket[0]","Basket"). - parent("root.basket[0]","root"). - index("root.basket[0]",0). - user_include("root.basket[0]").""", - "set_invalid_value_discrete": """ - part("product"). - discrete("Color"). - domain("Color","Red"). - type("root.color[0]","Color"). - parent("root.color[0]","root"). - index("root.color[0]",0). - user_value("root.color[0]","Yellow").""", - "set_invalid_value_num": """ - part("product"). - integer("product.size"). - range("product.size",1,10). - type("root.size[0]","product.size"). - parent("root.size[0]","root"). - index("root.size[0]",0). - user_value("root.size[0]",11).""", -} From 006c37893dd4554e8e8b084c0a54b8a9209e631e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20R=C3=BChling?= Date: Tue, 21 Jan 2025 15:34:02 +0100 Subject: [PATCH 9/9] added option for incremental bound increase --- src/coomsuite/__main__.py | 56 +++++++++++++++++++++-------------- src/coomsuite/utils/parser.py | 5 ++++ tests/clintests/__init__.py | 3 +- 3 files changed, 39 insertions(+), 25 deletions(-) diff --git a/src/coomsuite/__main__.py b/src/coomsuite/__main__.py index 434cc04..db06e18 100644 --- a/src/coomsuite/__main__.py +++ b/src/coomsuite/__main__.py @@ -4,6 +4,7 @@ import sys from tempfile import NamedTemporaryFile, TemporaryDirectory +from typing import List from clingo.application import clingo_main @@ -14,6 +15,34 @@ 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. @@ -43,6 +72,7 @@ def main(): elif args.command == "solve": log.info("Converting and solving COOM file %s", args.input) + with TemporaryDirectory() as temp_dir: # Parse COOM to ASP serialized facts serialized_facts = [convert_instance(args.input, "model", temp_dir)] + ( @@ -51,35 +81,15 @@ def main(): if args.show_facts: 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") - - # 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 - ret = clingo_main( - COOMSolverApp( - options={ - "solver": args.solver, - "output_format": args.output, - } - ), - [tmp_name] + unknown_args, - ) + ret = solve(serialized_facts, max_bound, args, unknown_args=unknown_args) max_bound += 1 diff --git a/src/coomsuite/utils/parser.py b/src/coomsuite/utils/parser.py index 7dd4367..ed86b5e 100644 --- a/src/coomsuite/utils/parser.py +++ b/src/coomsuite/utils/parser.py @@ -100,4 +100,9 @@ def get(levels: list[tuple[str, int]], name: str) -> Optional[int]: "--output", "-o", type=str, help="Set console output format", choices=["asp", "coom"], default="asp" ) parser_solve.add_argument("--show-facts", action="store_true", help="Show preprocessed fact format") + parser_solve.add_argument( + "--incremental-bounds", + action="store_true", + help="Incrementally increase the maximum for unbounded cardinalities.", + ) return parser diff --git a/tests/clintests/__init__.py b/tests/clintests/__init__.py index c60716e..32b250e 100644 --- a/tests/clintests/__init__.py +++ b/tests/clintests/__init__.py @@ -31,8 +31,7 @@ def StableModels(*args: set[Symbol | str], fclingo: bool = False) -> Test: # py """ if not fclingo: return And(NumModels(len(args)), *(Assert(Exact(1), Equals(a)) for a in args)) - else: - return And(NumModels(len(args)), *(Assert(Exact(1), SupersetOfTheory(a, check_theory=True)) for a in args)) + return And(NumModels(len(args)), *(Assert(Exact(1), SupersetOfTheory(a, check_theory=True)) for a in args)) class SupersetOfTheory(SupersetOf):