Refactoring of Generators

README.md

@@ -159,11 +159,11 @@ You can download and compile these solvers from the [MaxSAT 2023 evaluation](htt
 You can import Popper and use it in your Python code like so:
 
 ```python
-from popper.util import Settings, print_prog_score
+from popper.util import Settings
 from popper.loop import learn_solution
 
 settings = Settings(kbpath='input_dir')
 prog, score, stats = learn_solution(settings)
 if prog != None:
-    print_prog_score(prog, score)
+    settings.print_prog_score(prog, score)
 ```

popper.py

@@ -6,7 +6,7 @@
 if __name__ == '__main__':
     settings = Settings(cmd_line=True)
     prog, score, stats = learn_solution(settings)
-    if prog != None:
+    if prog is not None:
         settings.print_prog_score(prog, score)
     else:
         print('NO SOLUTION')

popper/abs_generate.py

@@ -0,0 +1,108 @@
+import abc
+from collections import defaultdict
+from typing import Set, TYPE_CHECKING, List, Optional
+
+import clingo
+
+from . type_defs import Literal, RuleBase
+
+
+if TYPE_CHECKING:
+    from . util import Settings
+
+
+class Generator(abc.ABC):
+    settings: 'Settings'
+    solver: clingo.Control
+    handle: Optional[clingo.SolveHandle]
+    model: Optional[clingo.Model]
+
+    @abc.abstractmethod
+    def get_prog(self) -> RuleBase:
+        pass
+
+    # @abc.abstractmethod
+    # def gen_symbol(self, literal, backend):
+    #     pass
+
+    @abc.abstractmethod
+    def update_solver(self, size):
+        pass
+
+    # @abc.abstractmethod
+    # def update_number_of_literals(self, size):
+    #     pass
+
+    # @abc.abstractmethod
+    # def update_number_of_vars(self, size):
+    #     pass
+
+    # @abc.abstractmethod
+    # def update_number_of_rules(self, size):
+    #     pass
+
+    @abc.abstractmethod
+    def prune_size(self, size):
+        pass
+
+    # @abc.abstractmethod
+    # def get_ground_rules(self, rule):
+    #     pass
+
+    # @abc.abstractmethod
+    # def parse_handles(self, new_handles):
+    #     pass
+
+    @abc.abstractmethod
+    def constrain(self, tmp_new_cons):
+        pass
+
+    @abc.abstractmethod
+    def build_encoding(self, bkcons: List, settings: "Settings") -> str:
+        """Build and return a string for an ASP solver."""
+
+    @abc.abstractmethod
+    def init_solver(self, encoding: str) -> clingo.Control:
+        """Incorporate the `encoding` into a new solver and return it."""
+
+    def parse_model_pi(self, model) -> RuleBase:
+        settings = self.settings
+        # directions = defaultdict(lambda: defaultdict(lambda: '?'))
+        rule_index_to_body = defaultdict(set)
+        rule_index_to_head = {}
+        # rule_index_ordering = defaultdict(set)
+
+        for atom in model:
+            args = atom.arguments
+            name = atom.name
+
+            if name == 'body_literal':
+                rule_index = args[0].number
+                predicate = args[1].name
+                atom_args = args[3].arguments
+                atom_args = settings.cached_atom_args[tuple(atom_args)]
+                arity = len(atom_args)
+                body_literal = (predicate, atom_args, arity)
+                rule_index_to_body[rule_index].add(body_literal)
+
+            elif name == 'head_literal':
+                rule_index = args[0].number
+                predicate = args[1].name
+                atom_args = args[3].arguments
+                atom_args = settings.cached_atom_args[tuple(atom_args)]
+                arity = len(atom_args)
+                head_literal = (predicate, atom_args, arity)
+                rule_index_to_head[rule_index] = head_literal
+
+        prog = []
+
+        for rule_index in rule_index_to_head:  # pylint: ignore=C0206
+            head_pred, head_args, _head_arity = rule_index_to_head[rule_index]
+            head = Literal(head_pred, head_args)
+            body: Set[Literal] = set()
+            for (body_pred, body_args, _body_arity) in rule_index_to_body[rule_index]:
+                body.add(Literal(body_pred, body_args))
+            rule = head, frozenset(body)
+            prog.append((rule))
+
+        return frozenset(prog)

popper/bkcons.py

@@ -1,16 +1,16 @@
+import numbers
+import sys
+import traceback
+from collections import defaultdict
+from itertools import product
+from traceback import format_tb
+
 import clingo
 import clingo.script
-import numbers
-import operator
-import pkg_resources
-import time
-from . util import rule_is_recursive, format_rule, Constraint, order_prog, Literal, suppress_stdout_stderr
 from clingo import Function, Number, Tuple_
-from collections import defaultdict
-from itertools import permutations, product
-from pysat.card import *
-from pysat.formula import CNF
-from pysat.solvers import Solver
+
+from .util import suppress_stdout_stderr
+
 clingo.script.enable_python()
 
 tmp_map = {}
@@ -52,7 +52,8 @@
 #     return (head_pred, arity), body_preds
 
 
-from itertools import permutations, combinations
+from itertools import permutations
+
 all_myvars = ['A','B','C','D','E','F','G','H']
 
 def connected(xs, ys):
@@ -628,7 +629,6 @@ def atom_to_symbol(pred, args):
     return Function(name = pred, arguments = xs)
 
 def deduce_bk_cons(settings, tester):
-    import re
     prog = []
     lookup2 = {k: f'({v})' for k,v in tmp_map.items()}
     lookup1 = {k:v for k,v in lookup2.items()}
@@ -1110,4 +1110,4 @@ def deduce_non_singletons(settings):
         cons.append(con)
 
     # exit()
-    return cons
+    return cons

popper/combine.py

@@ -258,7 +258,7 @@ def find_combination(self, timeout):
 
             else:
                 if not self.settings.lex:
-                    print("ERROR: Combining rec or pi programs not supported with MDL objective. Exiting.")
+                    self.settings.logger.error("ERROR: Combining rec or pi programs not supported with MDL objective. Exiting.")
                     assert(False)
 
                 model_inconsistent = self.tester.test_prog_inconsistent(model_prog)