simplifying z3 formulas further with custom simpifier

dtree_synth.py

@@ -5,6 +5,7 @@ from typing import Callable, Dict, Hashable, List, Literal, Tuple
 
 import numpy as np
 import z3
+from z3 import *
 from learner_base import LearnerBase
 from teacher_base import TeacherBase
 import time
@@ -53,12 +54,82 @@ def synth_dtree(learner: LearnerBase, teacher: TeacherBase, num_max_iterations:
             continue
         elif result == z3.unsat:
             print("we are done!")
-            return True, (k, z3.simplify(candidate, arith_lhs=True)), (teacher_time,learner_time)
+            return True, (k, tacticSimplify(z3.simplify(candidate, arith_lhs=True))), (teacher_time,learner_time)
         else:
             return False, f"Reason Unknown {teacher.reason_unknown()}", (teacher_time,learner_time)
 
     return False, f"Reached max iteration {num_max_iterations}.", (teacher_time,learner_time)
 
+def tacticSimplify(formula:BoolRef):
+        print("in custom simplify" + "-"*50)
+        gtdc = formula
+        
+        set_option(max_args = 10000000, max_lines = 1000000, max_depth = 10000000, max_visited = 1000000)
+        set_option(html_mode=False)
+        set_fpa_pretty(flag=False)
+
+        g = Goal()
+        g.add(gtdc)
+        
+        works = Repeat(Then( 
+        Repeat(OrElse(Tactic('split-clause'),Tactic('skip'))),
+        OrElse(Tactic('ctx-solver-simplify'),Tactic('skip')),
+        OrElse(Tactic('unit-subsume-simplify'),Tactic('skip')),
+        OrElse(Tactic('propagate-ineqs'),Tactic('skip')),
+        OrElse(Tactic('purify-arith'),Tactic('skip')),
+        OrElse(Tactic('ctx-simplify'),Tactic('skip')),
+        OrElse(Tactic('dom-simplify'),Tactic('skip')),
+        OrElse(Tactic('propagate-values'),Tactic('skip')),
+        OrElse(Tactic('simplify'),Tactic('skip')),
+        OrElse(Tactic('aig'),Tactic('skip')),
+        OrElse(Tactic('degree-shift'),Tactic('skip')),
+        OrElse(Tactic('factor'),Tactic('skip')),
+        OrElse(Tactic('lia2pb'),Tactic('skip')),
+        OrElse(Tactic('recover-01'),Tactic('skip')),
+        OrElse(Tactic('elim-term-ite'),Tactic('skip')), #must to remove ite
+        OrElse(Tactic('injectivity'),Tactic('skip')),
+        OrElse(Tactic('snf'),Tactic('skip')),
+        OrElse(Tactic('reduce-args'),Tactic('skip')),
+        OrElse(Tactic('elim-and'),Tactic('skip')),
+        OrElse(Tactic('symmetry-reduce'),Tactic('skip')),
+        OrElse(Tactic('macro-finder'),Tactic('skip')),
+        OrElse(Tactic('quasi-macros'),Tactic('skip')),
+        ))
+        
+        
+        result = works(g)
+        #result = works1(g)
+        # split_all =
+
+        # print str(result)
+        # result = [[ "d1", "d2", "d3"], #= conjunct && conjunct
+        #           [ "d4", "d5", "d6"]]
+
+        # remove empty subgoals and check if resultant list is empty.
+        result = filter(None, result)
+        if not result:
+            print("there is an error in the custom simplify Z3")
+            sys.exit(-9)
+        
+        # return result
+        results = list(result)
+        completeConjunct = []
+        for i in range(0,len(results)):
+            conjunction = results[i]
+            completeDisjunct = []
+            for literal in conjunction:
+                #if i >= 1 and  literal in result[i-1]:
+                #    continue
+                completeDisjunct.append(literal)
+
+            completeConjunct.append(z3.simplify(And(completeDisjunct)))
+        if len(completeConjunct) == 1:
+            print(completeConjunct[0])
+            return completeConjunct[0]
+        simplifiedGtdc = Or(completeConjunct)
+        print("custom simplified gtdc" + "-"*50)
+        print(simplifiedGtdc)
+        return simplifiedGtdc
 
 def validate_cexs(teacher: TeacherBase,
                   candidate: z3.BoolRef,
@@ -92,6 +163,7 @@ def synth_dtree_per_part(
         feature_domain: Literal["concat", "diff"] = "diff") -> List[Dict]:
     result = []
     for i, (part, dataset) in enumerate(part_to_examples.items()):
+        
         safe_dps, unsafe_dps, num_nan = dataset.safe_dps, dataset.unsafe_dps, dataset.num_nan_dps
 
         # if a partition has no safe datapoints, then skip the partion