minor bug of double checker fixed

Author: Chronosymbolic

horndb/horndb.py

@@ -595,15 +595,15 @@ class DoubleChecker:
     """
     Double check the result of the learner
     """
-    def __init__(self, file_name, logger):
+    def __init__(self, file_name, logger, free_vars_prefix='Var_'):
         self.solver = z3.Solver()
         self.solver.set(timeout=120000)
         db = load_horn_db_from_file(file_name, original=True)
         self.rules = list(reversed(db.get_rules()))  # "query" is always trivial
         self.rels = list(reversed(db.get_rels_list()))
         self.rel_decls = [r.decl() for r in self.rels]
         self.logger = logger
-        self.free_vars_prefix = 'Var_'  # None for v1 and v2
+        self.free_vars_prefix = free_vars_prefix  # None for v1 and v2, 'Var_' for Chronosymbolic
 
 
     def get_def(self, rule, cand_map, rel=None):

learner/learner.py

@@ -80,6 +80,7 @@ def __init__(self, db: HornClauseDb, params, ClassDT, log_path='log.txt', file_n
         self.unknowns = {}
         self.mod_nums = OrderedSet(self.params['MOD'])
         self.div_nums = OrderedSet(self.params['DIV'])
+        self.free_vars_prefix = None
         if not os.path.exists('tmp'):
             os.makedirs('tmp')
 

test.py

@@ -26,8 +26,8 @@
 
 
 # --- Set agent and DT algorithm here ---
-# ClassAgent = Chronosymbolic
-ClassAgent = DataDrivenLearner  # LinearArbitrary like
+ClassAgent = Chronosymbolic
+# ClassAgent = DataDrivenLearner  # LinearArbitrary like
 # ClassAgent = DataDrivenLearner_v2  # LinearArbitrary like, optimized
 
 ClassDT = C5DT  # C5.0
@@ -88,7 +88,7 @@ def run_single_file(args, logger, agent_params):
     is_successful, _, is_correct = run_Agent(Agent, logger)
     if is_correct and is_successful:
         learner_cand_map = None if Agent.__class__.__name__ != 'Chronosymbolic' else Agent.learner_cand_map
-        _ = double_check(args.file_name, logger, Agent.cand_map, learner_cand_map)
+        _ = double_check(args.file_name, logger, Agent.cand_map, learner_cand_map, Agent.free_vars_prefix)
 
 
 def run_dir_mode(args, logger, agent_params):
@@ -157,7 +157,7 @@ def run_dir_mode(args, logger, agent_params):
 
             if is_correct and is_successful:
                 learner_cand_map = None if Agent.__class__.__name__ != 'Chronosymbolic' else Agent.learner_cand_map
-                _ = double_check(path_file, logger, Agent.cand_map, learner_cand_map)
+                _ = double_check(path_file, logger, Agent.cand_map, learner_cand_map, Agent.free_vars_prefix)
 
             logger.warning('\n\n')
 
@@ -253,7 +253,7 @@ def run_filelist_mode(args, logger, agent_params):
 
         if is_correct and is_successful:
             learner_cand_map = None if Agent.__class__.__name__ != 'Chronosymbolic' else Agent.learner_cand_map
-            _ = double_check(file_name, logger, Agent.cand_map, learner_cand_map)
+            _ = double_check(file_name, logger, Agent.cand_map, learner_cand_map, Agent.free_vars_prefix)
 
         logger.warning('\n\n')
 

utils/la_utils.py

@@ -15,15 +15,15 @@ def load_yaml(config_path):
         params = yaml.load(f, Loader=yaml.SafeLoader)
     return params
 
-def double_check(file_name, logger, cand_map, learner_cand_map=None):
+def double_check(file_name, logger, cand_map, learner_cand_map=None, free_vars_prefix='Var_'):
     from horndb.horndb import DoubleChecker
-    double_checker = DoubleChecker(file_name, logger)
+    double_checker = DoubleChecker(file_name, logger, free_vars_prefix)
     res = False
     try:
         logger.warning('\n************** Double Check **************')
         res = double_checker.check(cand_map)
     except RuntimeError:
-        logger.warning('CHC System Double Check TIMEOUT')
+        logger.warning('CHC System Double Check ERROR/TIMEOUT')
     except KeyboardInterrupt:
         logger.warning('CHC System Double Check KILLED')