graph noodler: cnf support #1

noodler/formula.py

@@ -23,7 +23,7 @@
     ID of transition in automaton
 """
 
-from typing import Dict, Type, Union, Sequence, Set
+from typing import Dict, Type, Union, Sequence, Set, Optional
 from enum import Enum
 from dataclasses import dataclass
 from collections import defaultdict
@@ -194,6 +194,40 @@ def __init__(self, tp: ConstraintType, left_side: "StringConstraint", right_side
         self.right = right_side
 
 
+    def is_eq_restr(self) -> bool:
+        if self.op == ConstraintType.AND:
+            if self.left.op == ConstraintType.EQ and self.right.op == ConstraintType.RE:
+                return True
+        return False
+
+
+    def is_cnf(self) -> bool:
+        for con in self.gather_op(ConstraintType.AND):
+            for lf in con.gather_op(ConstraintType.OR):
+                print(lf)
+                if lf.op != ConstraintType.EQ and lf.op != ConstraintType.RE and not lf.is_eq_restr():
+                    return False
+        return True
+
+
+    def get_cnf_list(self) -> Optional[Sequence[Sequence[StringEquation]]]:
+        ret = []
+        for con in self.gather_op(ConstraintType.AND):
+            lst = []
+            for lf in con.gather_op(ConstraintType.OR):
+                if lf.op == ConstraintType.RE:
+                    continue
+                elif lf.op == ConstraintType.EQ:
+                    lst.append(lf.left)
+                elif lf.is_eq_restr():
+                    lst.append(lf.left.left)
+                else:
+                    return None
+            if len(lst) > 0:
+                ret.append(lst)
+        return ret
+
+
     def to_dnf(self) -> "StringConstraint":
         """!
         Convert a string constraint to DNF.
@@ -258,8 +292,10 @@ def __str__(self) -> str:
 
         @return: String representation
         """
-        if self.op == ConstraintType.EQ or self.op == ConstraintType.RE:
-            return str(self.left)
+        if self.op == ConstraintType.EQ:
+            return "EQ: " + str(self.left)
+        if self.op == ConstraintType.RE:
+            return "RE: " + str(self.left)
         if self.op == ConstraintType.AND:
             return "({0} AND {1})".format(str(self.left), str(self.right))
         if self.op == ConstraintType.OR:

noodler/graph_formula.py

@@ -171,7 +171,7 @@ def straight_line(self) -> "StringEqGraph":
         eqs = set()
         for v in cp.vertices:
             if v.eq.is_straightline():
-                if len(v.eq.get_side("right")) == 1:
+                if not v.eq.switched in eqs and len(v.eq.get_side("left")) == 1:
                     eqs.add(v.eq)
             else:
                 return None
@@ -180,7 +180,7 @@ def straight_line(self) -> "StringEqGraph":
         for v in cp.vertices:
             succp = []
             for prime in v.succ:
-                if len(v.eq.get_vars() & prime.eq.get_vars_side("right")) == 0:
+                if len(v.eq.get_vars() & prime.eq.get_vars_side("left")) == 0:
                     continue
                 succp.append(prime)
             v.succ = succp
@@ -218,7 +218,7 @@ def to_graphwiz(self) -> str:
 
 
     @staticmethod
-    def get_eqs_graph(equations: Sequence[StringEquation]) -> "StringEqGraph":
+    def get_eqs_graph(equations: Sequence[Sequence[StringEquation]]) -> "StringEqGraph":
         """!
         Get graph of equations. Each node is an equation. We distinguish L=R and
         R=L. Two equations are adjacent if they share a variable.
@@ -230,20 +230,25 @@ def get_eqs_graph(equations: Sequence[StringEquation]) -> "StringEqGraph":
         nodes: Dict[StringEquation, StringEqNode] = dict()
         all_nodes = []
         c = 0
-        for eq in equations:
-            nn: StringEqNode = StringEqNode([], eq, c)
-            nodes[eq] = nn
-            nnpr: StringEqNode = StringEqNode([], eq.switched, c+1)
-            nodes[eq.switched] = nnpr
-            all_nodes.append(nn)
-            all_nodes.append(nnpr)
-            c += 2
+        for clause in equations:
+            for eq in clause:
+                nn: StringEqNode = StringEqNode([], eq, c)
+                nodes[eq] = nn
+                nnpr: StringEqNode = StringEqNode([], eq.switched, c+1)
+                nodes[eq.switched] = nnpr
+                nn.succ.append(nnpr)
+                nnpr.succ.append(nn)
+                all_nodes.append(nn)
+                all_nodes.append(nnpr)
+                c += 2
 
         for v1 in all_nodes:
-            for v2 in all_nodes:
-                if v1.eq == v2.eq:
+            for clause in equations:
+                if v1.eq in clause or v1.eq.switched in clause:
                     continue
-                if len(v1.eq.get_vars() & v2.eq.get_vars()) != 0:
-                    v1.succ.append(v2)
+                for v2 in clause:
+                    if len(v1.eq.get_vars() & v2.get_vars()) != 0:
+                        v1.succ.append(nodes[v2])
+                        v1.succ.append(nodes[v2.switched])
 
         return StringEqGraph(all_nodes)

noodler/parser.py

@@ -305,7 +305,10 @@ def z3_concat_to_var_list(z3_ref: z3.SeqRef) -> Collection[str]:
         res_left = z3_concat_to_var_list(left)
         res_right = z3_concat_to_var_list(right)
         constr = StringConstraint(ConstraintType.RE, aux_vars)
-        return StringConstraint(ConstraintType.AND, StringConstraint(ConstraintType.EQ, StringEquation(list(res_left), list(res_right))), constr)
+        eq = StringConstraint(ConstraintType.EQ, StringEquation(list(res_left), list(res_right)))
+        if len(aux_vars) == 0:
+            return eq
+        return StringConstraint(ConstraintType.AND, eq, constr)
 
     def parse_re_constraint(self, ref: z3.BoolRef) -> REConstraints:
         """
@@ -361,8 +364,8 @@ def parse_bool_expression(self, ref: z3.BoolRef) -> StringConstraint:
         @param ref: z3.BoolRef
         @return StringConstraint instance
         """
-        if is_assignment(ref):
-            return self.process_assignment(ref)
+        # if is_assignment(ref):
+        #     return self.process_assignment(ref)
 
         if is_equation(ref):
             return self.parse_equation(ref)

noodler/sequery.py

@@ -419,7 +419,22 @@ def _merge_constraints(cnstr: Sequence[AutConstraints]) -> AutConstraints:
         return res
 
 
-    def get_sequeries(self) -> Sequence[MultiSEQuery]:
+    def _gather_aut_constraints(self) -> AutConstraints:
+        constr = [create_automata_constraints(c.left) for c in self.constraint.gather_leafs(ConstraintType.RE)]
+        constr_dict = StringConstraintQuery._merge_constraints(constr)
+        vars = self.constraint.get_vars()
+
+        sigma_star: RE = awalipy_allchar(self.alphabet).star()
+        for var in vars:
+            constr_dict.setdefault(var, awalipy.Automaton(sigma_star).proper().minimal_automaton().trim())
+        return constr_dict
+
+
+    def get_queries_cnf(self):
+        return self.constraint.get_cnf_list(), self._gather_aut_constraints()
+
+
+    def get_sequeries_dnf(self) -> Sequence[MultiSEQuery]:
         """!
         Get subqueries for solving of the string constraint.