Add minimization support and efficient graph creat

This commit adds minimization support to the viASP cli and the python
API. The available options are equivalent to clingo. They are passed on
to the clingo control object to be tasked with optimization.

The graph creation has been optimized to be more efficient. Programs
with many rules and correspondingly many possible sorts are now created
on demand. This is done by generating only the graph from the primary
sort in the beginning. All possible sorts are calculated and stored in
the database. When the frontend requests a graph for one of the possible
sorts, it is created while the frontend shows a loading animation.

All data is stored in the sqlite database. It is created and destroyed
when the server is started and stopped.

Resolves: #34

backend/src/viasp/__main__.py

@@ -7,14 +7,27 @@
 from viasp import Control
 from viasp.server import startup
 from viasp.shared.defaults import DEFAULT_BACKEND_HOST, DEFAULT_BACKEND_PORT, DEFAULT_FRONTEND_PORT, DEFAULT_BACKEND_PROTOCOL
+from viasp.shared.io import clingo_model_to_stable_model
 
 try:
     VERSION = importlib.metadata.version("viasp")
 except importlib.metadata.PackageNotFoundError:
     VERSION = '0.0.0'
 
+
+def _parse_opt_mode(arg):
+    parts = arg.split(',')
+    mode = parts[0]
+    if mode not in ['opt', 'enum', 'optN', 'ignore']:
+        raise argparse.ArgumentTypeError(f"Invalid opt-mode: {mode}")
+    bounds = parts[1:]
+    return (mode, bounds)
+
+
 def _get_parser():
-    parser = argparse.ArgumentParser(prog='viasp', description=textwrap.dedent(r"""
+    parser = argparse.ArgumentParser(
+        prog='viasp',
+        description=textwrap.dedent(r"""
            _        _____ _____  
           (_)  /\  / ____|  __ \ 
     __   ___  /  \| (___ | |__) |
@@ -25,23 +38,79 @@ def _get_parser():
     viASP is a package to generate interactive 
     visualizations of ASP programs and 
     their stable models. 
-    """), formatter_class=argparse.RawTextHelpFormatter)
-    parser.add_argument('paths', nargs='+', help='Runs viASP with the paths to programs to be loaded')
-    parser.add_argument('-n', '--models', type=int, help='Compute at most <n> models (0 for all)', default=0)
-    parser.add_argument('--host', type=str, help='The host for the backend and frontend', default=DEFAULT_BACKEND_HOST)
-    parser.add_argument('-p', '--port', type=int, help='The port for the backend', default=DEFAULT_BACKEND_PORT)
-    parser.add_argument('-f', '--frontend-port', type=int, help='The port for the frontend', default=DEFAULT_FRONTEND_PORT)
-    parser.add_argument('--version','-v', action='version', version=f'%(prog)s {VERSION}')
-
-    clingraph_group = parser.add_argument_group('Clingraph', 'If included, a clingraph visualization will be made.')
-    clingraph_group.add_argument('--viz_encoding', type=str, help='The path to the visualization encoding.', default=None)
-    clingraph_group.add_argument('--engine', type=str, help='The visualization engine.', default="dot")
-    clingraph_group.add_argument('--graphviz_type', type=str, help='The graph type.', default="graph")
-
-    relaxer_group = parser.add_argument_group('Relaxer', 'Options for the relaxation of integrity constraints in unsatisfiable programs.')
-    relaxer_group.add_argument('-r', '--no-relaxer', action=argparse.BooleanOptionalAction, help='Do not use the relaxer')
-    relaxer_group.add_argument('--head_name', type=str, help='The name of the head predicate.', default="unsat")
-    relaxer_group.add_argument('--no-collect-variables', action=argparse.BooleanOptionalAction, help='Do not collect variables from body as a tuple in the head literal.')
+    """),
+        formatter_class=argparse.RawTextHelpFormatter)
+    parser.add_argument(
+        'paths',
+        nargs='+',
+        help='Runs viASP with the paths to programs to be loaded')
+    parser.add_argument('-n',
+                        '--models',
+                        type=int,
+                        help='Compute at most <n> models (0 for all)',
+                        default=0)
+    parser.add_argument('--host',
+                        type=str,
+                        help='The host for the backend and frontend',
+                        default=DEFAULT_BACKEND_HOST)
+    parser.add_argument('-p',
+                        '--port',
+                        type=int,
+                        help='The port for the backend',
+                        default=DEFAULT_BACKEND_PORT)
+    parser.add_argument('-f',
+                        '--frontend-port',
+                        type=int,
+                        help='The port for the frontend',
+                        default=DEFAULT_FRONTEND_PORT)
+    parser.add_argument('--version',
+                        '-v',
+                        action='version',
+                        version=f'%(prog)s {VERSION}')
+    parser.add_argument('--opt-mode',
+                        type=_parse_opt_mode,
+                        help=textwrap.dedent("""
+    Configure optimization algorithm
+    <mode {opt|enum|optN|ignore}>[,<bound>...]
+    opt   : Find optimal model
+    enum  : Enumerate models with costs less than or equal to some fixed bound
+    optN  : Find optimum, then enumerate optimal models
+    ignore: Ignore optimize statements
+    """))
+
+    clingraph_group = parser.add_argument_group(
+        'Clingraph', 'If included, a clingraph visualization will be made.')
+    clingraph_group.add_argument(
+        '--viz_encoding',
+        type=str,
+        help='The path to the visualization encoding.',
+        default=None)
+    clingraph_group.add_argument('--engine',
+                                 type=str,
+                                 help='The visualization engine.',
+                                 default="dot")
+    clingraph_group.add_argument('--graphviz_type',
+                                 type=str,
+                                 help='The graph type.',
+                                 default="graph")
+
+    relaxer_group = parser.add_argument_group(
+        'Relaxer',
+        'Options for the relaxation of integrity constraints in unsatisfiable programs.'
+    )
+    relaxer_group.add_argument('-r',
+                               '--no-relaxer',
+                               action=argparse.BooleanOptionalAction,
+                               help='Do not use the relaxer')
+    relaxer_group.add_argument('--head_name',
+                               type=str,
+                               help='The name of the head predicate.',
+                               default="unsat")
+    relaxer_group.add_argument(
+        '--no-collect-variables',
+        action=argparse.BooleanOptionalAction,
+        help=
+        'Do not collect variables from body as a tuple in the head literal.')
 
     # TODO: transformer
 
@@ -51,8 +120,15 @@ def _get_parser():
 def backend():
     from viasp.server.factory import create_app
     parser = argparse.ArgumentParser(description='viasp backend')
-    parser.add_argument('--host', type=str, help='The host for the backend', default=DEFAULT_BACKEND_HOST)
-    parser.add_argument('-p', '--port', type=int, help='The port for the backend', default=DEFAULT_BACKEND_PORT)
+    parser.add_argument('--host',
+                        type=str,
+                        help='The host for the backend',
+                        default=DEFAULT_BACKEND_HOST)
+    parser.add_argument('-p',
+                        '--port',
+                        type=int,
+                        help='The port for the backend',
+                        default=DEFAULT_BACKEND_PORT)
     app = create_app()
     use_reloader = False
     debug = False
@@ -63,7 +139,6 @@ def backend():
     app.run(host=host, port=port, use_reloader=use_reloader, debug=debug)
 
 
-
 def start():
     parser = _get_parser()
 
@@ -79,10 +154,13 @@ def start():
     graphviz_type = args.graphviz_type
     head_name = args.head_name
     no_collect_variables = args.no_collect_variables
+    opt_mode, bounds = args.opt_mode or ('opt', [])
+    opt_mode_str = f"--opt-mode={opt_mode}" + (f",{','.join(bounds)}" if len(
+        bounds) > 0 else "")
 
     app = startup.run(host=DEFAULT_BACKEND_HOST, port=DEFAULT_BACKEND_PORT)
-    
-    options = [str(models)]
+
+    options = [str(models), opt_mode_str]
 
     backend_url = f"{DEFAULT_BACKEND_PROTOCOL}://{host}:{port}"
     enable_python()
@@ -94,15 +172,27 @@ def start():
     ctl.ground([("base", [])])
 
     with ctl.solve(yield_=True) as handle:
+        models = {}
         for m in handle:
-            print("Answer:\n{}".format(m))
+            print(f"Answer: {m.number}\n{m}")
+            if len(m.cost) > 0:
+                print(f"Optimization: {m.cost}")
+            c = m.cost[0] if len(m.cost) > 0 else 0
+            models[clingo_model_to_stable_model(m)] = c
+        for m in list(
+                filter(lambda i: models.get(i) == min(models.values()),
+                       models.keys())):
             ctl.viasp.mark(m)
         print(handle.get())
         if handle.get().unsatisfiable and not no_relaxer:
-            ctl = ctl.viasp.relax_constraints(head_name=head_name, collect_variables=not no_collect_variables)
+            ctl = ctl.viasp.relax_constraints(
+                head_name=head_name,
+                collect_variables=not no_collect_variables)
     ctl.viasp.show()
     if viz_encoding:
-        ctl.viasp.clingraph(viz_encoding=viz_encoding, engine=engine, graphviz_type=graphviz_type)
+        ctl.viasp.clingraph(viz_encoding=viz_encoding,
+                            engine=engine,
+                            graphviz_type=graphviz_type)
 
     webbrowser.open(f"http://{host}:{frontend_port}")
     app.run(host=host, port=frontend_port, use_reloader=False, debug=False)

backend/src/viasp/api.py

@@ -10,7 +10,7 @@
 """
 
 from inspect import signature
-from typing import List, cast, Union    
+from typing import List, cast, Union
 
 import clingo
 from clingo import Control as InnerControl
@@ -21,6 +21,7 @@
 
 from .shared.defaults import STDIN_TMP_STORAGE_PATH
 from .shared.io import clingo_symbols_to_stable_model
+from .shared.model import StableModel
 from .wrapper import ShowConnector, Control as viaspControl
 from .exceptions import InvalidSyntax
 
@@ -223,12 +224,12 @@ def show(**kwargs) -> None:
     connector.show()
 
 
-def mark_from_clingo_model(model: clingo_Model, **kwargs) -> None:
+def mark_from_clingo_model(model: Union[clingo_Model, StableModel], **kwargs) -> None:
     r"""
     Mark a model to be visualized. Models can be unmarked and cleared.
     The marked models are propagated to the backend when ``show`` is called.
 
-    :param model: ``clingo.solving.Model``
+    :param model: ``clingo.solving.Model`` or ``viasp.model.StableModel``
         The model to mark.
     :param \**kwargs:
         * *viasp_backend_url* (``str``) --
@@ -246,11 +247,12 @@ def mark_from_clingo_model(model: clingo_Model, **kwargs) -> None:
     connector.mark(model)
 
 
-def unmark_from_clingo_model(model: clingo_Model, **kwargs) -> None:
+def unmark_from_clingo_model(model: Union[clingo_Model, StableModel],
+                             **kwargs) -> None:
     r"""
     Unmark a model.
 
-    :param model: ``clingo.solving.Model``
+    :param model: ``clingo.solving.Model`` or ``viasp.model.StableModel``
         The model to unmark.
     :param \**kwargs:
         * *viasp_backend_url* (``str``) --

backend/src/viasp/asp/justify.py

@@ -1,19 +1,18 @@
 """This module is concerned with finding reasons for why a stable model is found."""
 from collections import defaultdict
-from typing import List, Collection, Dict, Iterable, Union, Set, cast
+from typing import List, Collection, Dict, Iterable, Union, Set
 
 import networkx as nx
 
 from clingo import Control, Symbol, Model, ast
 
 from clingo.ast import AST
-from networkx import DiGraph
 
 from .reify import ProgramAnalyzer, has_an_interval
 from .recursion import RecursionReasoner
-from .utils import insert_atoms_into_nodes, identify_reasons, harmonize_uuids, calculate_spacing_factor
+from .utils import insert_atoms_into_nodes, identify_reasons, calculate_spacing_factor
 from ..shared.model import Node, Transformation, SymbolIdentifier
-from ..shared.simple_logging import info, warn
+from ..shared.simple_logging import info
 from ..shared.util import pairwise, get_leafs_from_graph
 
 
@@ -110,7 +109,6 @@ def make_reason_path_from_facts_to_stable_model(wrapped_stable_model,
     g = nx.DiGraph()
     if len(h_syms) == 1:
         # If there is a stable model that is exactly the same as the facts.
-        warn(f"Adding a model without reasons {wrapped_stable_model}")
         if rule_mapping[min(rule_mapping.keys())].rules in recursive_transformations:
             fact_node.recursive = True
         g.add_edge(fact_node, Node(frozenset(), min(rule_mapping.keys()), frozenset(fact_node.diff)),
@@ -141,17 +139,18 @@ def make_transformation_mapping(transformations: Iterable[Transformation]):
     return {t.id: t for t in transformations}
 
 
-def append_noops(result_graph: DiGraph,
+def append_noops(result_graph: nx.DiGraph,
                  sorted_program: Iterable[Transformation],
                  pass_through: Set[AST]):
     next_transformation_id = max(t.id for t in sorted_program) + 1
     leaves = list(get_leafs_from_graph(result_graph))
     leaf: Node
     for leaf in leaves:
         noop_node = Node(frozenset(), next_transformation_id, leaf.atoms)
-        result_graph.add_edge(leaf, noop_node,
-                              transformation=Transformation(next_transformation_id,
-                                                            tuple(pass_through)))
+        result_graph.add_edge(leaf,
+                              noop_node,
+                              transformation=Transformation(
+                                  next_transformation_id, tuple(pass_through)))
 
 
 def build_graph(wrapped_stable_models: List[List[str]],