Incremental Popper fixes.

Author: rpgoldman

popper/abs_generate.py

@@ -1,10 +1,17 @@
 import abc
+from typing import FrozenSet, Tuple, TYPE_CHECKING
 
+if TYPE_CHECKING:
+    from . util import Literal, Settings
+
+Rule = Tuple['Literal', FrozenSet['Literal']]
+RuleBase = FrozenSet[Rule]
 
 class Generator(abc.ABC):
+    settings: 'Settings'
 
     # @profile
-    def get_prog(self):
+    def get_prog(self) -> RuleBase:
         pass
 
     def gen_symbol(self, literal, backend):

popper/generate.py

@@ -1,20 +1,24 @@
-import time
 import re
-from pysat.formula import CNF
-from pysat.solvers import Solver
-from pysat.card import *
-import clingo
-import operator
+from typing import Optional, Sequence, Set
+
 import numbers
+import operator
+import re
+from collections import defaultdict
+from typing import Optional, Sequence, Set
+
+import clingo
 import clingo.script
 import pkg_resources
-from collections import defaultdict
-from . util import rule_is_recursive, Constraint, Literal, format_rule, remap_variables
+
+from .util import rule_is_recursive, Constraint, Literal, remap_variables
+
 clingo.script.enable_python()
-from clingo import Function, Number, Tuple_
+from clingo import Function, Number, Tuple_, Model, Symbol
 from itertools import permutations
 import dataclasses
 from . abs_generate import Generator as AbstractGenerator
+from . abs_generate import Rule, RuleBase
 
 @dataclasses.dataclass(frozen=True)
 class Var:
@@ -78,6 +82,7 @@ def build_rule_literals(rule, rule_var, pi=False):
 
 class Generator(AbstractGenerator):
 
+    model: Optional[Model]
     def __init__(self, settings, bkcons=[]):
         self.savings = 0
         self.settings = settings
@@ -245,13 +250,13 @@ def __init__(self, settings, bkcons=[]):
         self.solver = solver
 
     # @profile
-    def get_prog(self):
+    def get_prog(self) -> Optional[RuleBase]:
         if self.handle is None:
             self.handle = iter(self.solver.solve(yield_ = True))
         self.model = next(self.handle, None)
         if self.model is None:
             return None
-        atoms = self.model.symbols(shown = True)
+        atoms: Sequence[Symbol] = self.model.symbols(shown = True)
 
         if self.settings.single_solve:
             return self.parse_model_single_rule(atoms)
@@ -271,7 +276,7 @@ def gen_symbol(self, literal, backend):
             self.seen_symbols[k] = symbol
         return symbol
 
-    def parse_model_recursion(self, model):
+    def parse_model_recursion(self, model) -> RuleBase:
         settings = self.settings
         rule_index_to_body = defaultdict(set)
         head = settings.head_literal
@@ -293,21 +298,21 @@ def parse_model_recursion(self, model):
 
         return frozenset(prog)
 
-    def parse_model_single_rule(self, model):
+    def parse_model_single_rule(self, model: Sequence[Symbol]) -> RuleBase:
         settings = self.settings
-        head = settings.head_literal
-        body = set()
+        head: Literal = settings.head_literal
+        body: Set[Literal] = set()
         cached_literals = settings.cached_literals
         for atom in model:
             args = atom.arguments
             predicate = args[1].name
             atom_args = tuple(args[3].arguments)
             literal = cached_literals[(predicate, atom_args)]
             body.add(literal)
-        rule = head, frozenset(body)
+        rule: Rule = head, frozenset(body)
         return frozenset([rule])
 
-    def parse_model_pi(self, model):
+    def parse_model_pi(self, model) -> RuleBase:
         settings = self.settings
         # directions = defaultdict(lambda: defaultdict(lambda: '?'))
         rule_index_to_body = defaultdict(set)

popper/loop.py

@@ -186,6 +186,7 @@ def run(self, bkcons):
                 new_cons = []
 
                 # generate a program
+                # prog: Optional[Program]
                 with settings.stats.duration('generate'):
                     prog = generator.get_prog()
                     settings.logger.info("Generated prog: {}".format(prog))

popper/util.py

@@ -5,11 +5,13 @@
 from contextlib import contextmanager
 from itertools import permutations
 from time import perf_counter
-from typing import NamedTuple, Optional, Dict
+from typing import NamedTuple, Optional, Dict, Tuple, Any
 
 import clingo
 import clingo.script
 
+from popper.abs_generate import Rule
+
 
 class Literal(NamedTuple):
     predicate: str
@@ -260,6 +262,7 @@ class Settings:
     showcons: bool
     datalog: bool
     show_failures: bool  # display detailed FP and FN information
+    cached_literals: Dict[Tuple[str, Any], Literal]
 
     def __init__(self, cmd_line=False, info=True, debug=False, show_stats=True, max_literals=MAX_LITERALS,
                  timeout=TIMEOUT, quiet=False, eval_timeout=EVAL_TIMEOUT, max_examples=MAX_EXAMPLES, max_body=None,
@@ -814,7 +817,7 @@ def prog_hash(prog):
     return hash(new_prog)
 
 
-def remap_variables(rule):
+def remap_variables(rule: Tuple[Any, Any]) -> Rule:
     head, body = rule
 
     head_vars = frozenset(head.arguments) if head else frozenset()