Merge pull request #178 from alwilson/rand_info_nested_soft_176

Nested soft constraint support

src/vsc/model/__init__.py

@@ -37,6 +37,7 @@
 from .constraint_block_model import ConstraintBlockModel
 from .constraint_expr_model import ConstraintExprModel
 from .constraint_if_else_model import ConstraintIfElseModel
+from .constraint_soft_model import ConstraintSoftModel
 from .constraint_implies_model import ConstraintImpliesModel
 from .constraint_scope_model import ConstraintScopeModel
 from .constraint_unique_model import ConstraintUniqueModel

src/vsc/model/constraint_expr_model.py

@@ -33,7 +33,7 @@ def __init__(self, e):
         super().__init__()
         self.e = e
 
-    def build(self, btor):
+    def build(self, btor, soft=False):
         return ExprModel.toBool(btor, self.e.build(btor))
 
     def accept(self, visitor):

src/vsc/model/constraint_foreach_model.py

@@ -27,7 +27,7 @@ def __init__(self, lhs : 'FieldArrayModel'):
             False)
 
 
-    def build(self, btor)->'BoolectorNode':
+    def build(self, btor, soft=False)->'BoolectorNode':
         # Unroll the constraints
         size = int(self.lhs.size.get_val())
         ret_l = []
@@ -39,7 +39,7 @@ def build(self, btor)->'BoolectorNode':
             # Build out the constraints for this index
             # Note: some could be redundant
             for c in self.constraint_l:
-                ret_l.append(c.build(btor))
+                ret_l.append(c.build(btor, soft))
 
         return btor.And(*ret_l)
 

src/vsc/model/constraint_if_else_model.py

@@ -39,15 +39,15 @@ def __init__(self,
         self.true_c : ConstraintModel = true_c
         self.false_c : ConstraintModel = false_c
 
-    def build(self, btor):
+    def build(self, btor, soft=False):
         from vsc.visitors.model_pretty_printer import ModelPrettyPrinter
         cond = ExprModel.toBool(btor, self.cond.build(btor))
-        true_c = self.true_c.build(btor)
+        true_c = self.true_c.build(btor, soft)
 
         if self.false_c == None:
             ret = btor.Implies(cond, true_c)
         else:
-            false_c = self.false_c.build(btor)
+            false_c = self.false_c.build(btor, soft)
             ret = btor.Cond(cond, true_c, false_c)
 
         return ret

src/vsc/model/constraint_implies_model.py

@@ -30,9 +30,9 @@ def __init__(self, cond, constraints=None):
         super().__init__(constraints)
         self.cond = cond
 
-    def build(self, btor):
+    def build(self, btor, soft=False):
         cond = ExprModel.toBool(btor, self.cond.build(btor))
-        body = super().build(btor)
+        body = super().build(btor, soft)
 
         return btor.Implies(cond, body)
 

src/vsc/model/constraint_model.py

@@ -32,7 +32,7 @@ def __init__(self):
     def dispose(self):
         self.node = None
 
-    def build(self, btor)->BoolectorNode:
+    def build(self, btor, soft=False)->BoolectorNode:
         raise Exception("build unimplemented for constraint " + str(type(self)))
 
     def get_nodes(self, node_l):

src/vsc/model/constraint_override_model.py

@@ -15,8 +15,8 @@ def __init__(self, orig_constraint, new_constraint):
         self.orig_constraint = orig_constraint
         self.depth = 1
 
-    def build(self, btor):
-        return self.new_constraint.build(btor)
+    def build(self, btor, soft=False):
+        return self.new_constraint.build(btor, soft)
 
     def accept(self, v):
         v.visit_constraint_override(self)

src/vsc/model/constraint_scope_model.py

@@ -36,13 +36,15 @@ def addConstraint(self, c) -> ConstraintModel:
         self.constraint_l.append(c)
         return c
 
-    def build(self, btor):
+    def build(self, btor, soft=False):
         ret = None
         for c in self.constraint_l:
             if ret is None:
-                ret = c.build(btor)
+                ret = c.build(btor, soft)
             else:
-                ret = btor.And(ret, c.build(btor))
+                b = c.build(btor, soft)
+                if b is not None:
+                    ret = btor.And(ret, b)
 
         if ret is None:
             # An empty block defaults to 'true'

src/vsc/model/constraint_soft_model.py

@@ -17,9 +17,12 @@ def __init__(self, e : ExprModel):
         self.expr = e
         self.priority = 0
 
-    def build(self, btor):
-        return self.expr.build(btor)
-
+    def build(self, btor, soft=False):
+        if soft:
+            return self.expr.build(btor)
+        else:
+            return None
+
     def accept(self, v):
         v.visit_constraint_soft(self)
 

src/vsc/model/constraint_unique_model.py

@@ -33,7 +33,7 @@ def __init__(self, unique_l):
         self.unique_l = unique_l
         self.expr = None 
 
-    def build(self, btor):
+    def build(self, btor, soft=False):
         ret = None
 
         # Elements in the unique list might be arrays        

src/vsc/model/rand_info_builder.py

@@ -30,13 +30,20 @@
 from vsc.model.constraint_expr_model import ConstraintExprModel
 from vsc.model.constraint_model import ConstraintModel
 from vsc.model.constraint_soft_model import ConstraintSoftModel
+from vsc.model.constraint_if_else_model import ConstraintIfElseModel
+from vsc.model.constraint_implies_model import ConstraintImpliesModel
+from vsc.model.constraint_scope_model import ConstraintScopeModel
 from vsc.model.constraint_solve_order_model import ConstraintSolveOrderModel
 from vsc.model.covergroup_model import CovergroupModel
 from vsc.model.coverpoint_bin_array_model import CoverpointBinArrayModel
 from vsc.model.coverpoint_model import CoverpointModel
 from vsc.model.expr_array_subscript_model import ExprArraySubscriptModel
 from vsc.model.expr_dynref_model import ExprDynRefModel
 from vsc.model.expr_literal_model import ExprLiteralModel
+from vsc.model.expr_unary_model import ExprUnaryModel
+from vsc.model.expr_bin_model import ExprBinModel
+from vsc.model.unary_expr_type import UnaryExprType
+from vsc.model.bin_expr_type import BinExprType
 from vsc.model.field_array_model import FieldArrayModel
 from vsc.model.field_model import FieldModel
 from vsc.model.model_visitor import ModelVisitor
@@ -78,11 +85,12 @@ def __init__(self, rng):
 
         self._order_m = {}
         self._expr2fm = Expr2FieldVisitor()
+        self._soft_cond_l = []
 
     @staticmethod
     def build(
-            field_model_l : [FieldModel],
-            constraint_l : [ConstraintModel],
+            field_model_l : List[FieldModel],
+            constraint_l : List[ConstraintModel],
             rng=None) ->RandInfo:
         if rng is None:
 #            rng = Random()
@@ -240,12 +248,44 @@ def visit_constraint_soft(self, c:ConstraintSoftModel):
         # Update the priority of this constraint
         c.priority += self._soft_priority
         self._soft_priority += 1
-
+
+        if self._pass == 1 and len(self._soft_cond_l) > 0:
+            # AND all soft conditions together
+            and_cond = self._soft_cond_l[0]
+            for soft_cond in self._soft_cond_l[1:]:
+                and_cond = ExprBinModel(and_cond, BinExprType.And, soft_cond)
+
+            # TODO Is it okay to add priority attr to root Constraint so
+            #      add_constraint can detect them and randomize can sort
+            #      soft constraints more easily?
+            soft_implies = ConstraintImpliesModel(and_cond, [c])
+            soft_implies.priority = c.priority
+            self._active_randset.add_constraint(soft_implies)
+
         super().visit_constraint_soft(c)
 
         if RandInfoBuilder.EN_DEBUG:
             print("<-- RandInfoBuilder::visit_constraint_soft")
-
+
+    def visit_constraint_if_else(self, c : ConstraintIfElseModel):
+        self.visit_constraint_stmt_enter(c)
+        self._soft_cond_l.append(c.cond)
+        c.cond.accept(self)
+        c.true_c.accept(self)
+        if c.false_c != None:
+            self._soft_cond_l[-1] = ExprUnaryModel(UnaryExprType.Not, c.cond)
+            c.false_c.accept(self)
+        self._soft_cond_l.pop()
+        self.visit_constraint_stmt_leave(c)
+
+    def visit_constraint_implies(self, c : ConstraintImpliesModel):
+        self.visit_constraint_stmt_enter(c)
+        self._soft_cond_l.append(c.cond)
+        c.cond.accept(self)
+        self.visit_constraint_scope(c)
+        self._soft_cond_l.pop()
+        self.visit_constraint_stmt_leave(c)
+
     def visit_expr_array_subscript(self, s : ExprArraySubscriptModel):
         fm = s.getFieldModel()
         if self._pass == 1:

src/vsc/model/rand_set.py

@@ -76,9 +76,9 @@ def rand_fields(self):
 
     def all_fields(self)->List[FieldModel]:
         return self.all_field_l
-        
+
     def add_constraint(self, c):
-        if isinstance(c, ConstraintSoftModel):
+        if isinstance(c, ConstraintSoftModel) or hasattr(c, 'priority'):
             if c not in self.soft_constraint_s:
                 self.soft_constraint_s.add(c)
                 self.soft_constraint_l.append(c)

src/vsc/model/rand_set_node_builder.py

@@ -4,6 +4,7 @@
 @author: ballance
 '''
 from vsc.model.constraint_model import ConstraintModel
+from vsc.model.constraint_soft_model import ConstraintSoftModel
 from vsc.model.enum_field_model import EnumFieldModel
 from vsc.model.field_scalar_model import FieldScalarModel
 from vsc.model.model_visitor import ModelVisitor
@@ -16,22 +17,30 @@ def __init__(self, btor):
         super().__init__()
         self.btor = btor
         self.phase = 0
+        self.soft_phase = 0
 
     def build(self, rs : RandSet):
         self.phase = 0
+        self.soft_phase = 0
         for f in rs.fields():
             f.accept(self)
         for c in rs.constraints():
             c.accept(self)
         self.phase = 1
         for c in rs.constraints():
             c.accept(self)
+        self.soft_phase = 1
+        for c in rs.soft_constraints():
+            c.accept(self)
 
     def visit_constraint_stmt_enter(self, c:ConstraintModel):
         from ..visitors.model_pretty_printer import ModelPrettyPrinter
         if self.phase == 1:
-            c.build(self.btor)
-
+            if isinstance(c, ConstraintSoftModel):
+                c.build(self.btor, self.soft_phase)
+            else:
+                c.build(self.btor)
+
     def visit_scalar_field(self, f:FieldScalarModel):
         if self.phase == 0:
             f.build(self.btor)

src/vsc/model/randomizer.py

@@ -176,9 +176,8 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
                 rs_node_builder.build(rs)
                 n_fields += len(all_fields)
 
-#                constraint_l.extend(list(map(lambda c:(c,c.build(btor),isinstance(c,ConstraintSoftModel)), rs.constraints())))
-                constraint_l.extend(list(map(lambda c:(c,c.build(btor)), rs.constraints())))
-                soft_constraint_l.extend(list(map(lambda c:(c,c.build(btor)), rs.soft_constraints())))
+                constraint_l.extend(list(map(lambda c:(c,c.build(btor, False)), rs.constraints())))
+                soft_constraint_l.extend(list(map(lambda c:(c,c.build(btor, True)), rs.soft_constraints())))
 
                 # Sort the list in descending order so we know which constraints
                 # to prioritize

src/vsc/visitors/model_pretty_printer.py

@@ -133,16 +133,23 @@ def visit_constraint_if_else(self, c:vm.ConstraintIfElseModel):
             self.dec_indent()
 
         self.writeln("}")
-
+
+    def visit_constraint_soft(self, c:vm.ConstraintSoftModel):
+        self.write(self.ind + "soft ")
+        c.expr.accept(self)
+        self.write("\n")
+
     def visit_constraint_implies(self, c:vm.ConstraintImpliesModel):
         self.write(self.ind)
         c.cond.accept(self)
-        self.write(" -> {")
+        self.write(" -> {\n")
 
+        self.inc_indent()
         for sc in c.constraint_l:
             sc.accept(self)
-
-        self.write("}\n")
+        self.dec_indent()
+
+        self.write(self.ind + "}\n")
 
     def visit_constraint_solve_order(self, c:ConstraintSolveOrderModel):
         self.write(self.ind)

ve/unit/test_constraint_soft.py

@@ -275,4 +275,45 @@ def fixed_c(self):
 
         print(rand_a.a_field)
         pass
-
+
+    def test_soft_nested(self):
+        """Test various nested soft constraint scenarios"""
+
+        @vsc.randobj
+        class Nested:
+            def __init__(self):
+                self.a = vsc.rand_uint8_t(8)
+                self.b = vsc.rand_uint8_t(8)
+                self.c = vsc.rand_uint8_t(8)
+                self.d = vsc.rand_uint8_t(8)
+                self.e = vsc.rand_uint8_t(8)
+                self.f = vsc.rand_uint8_t(8)
+                self.arr = vsc.rand_list_t(vsc.uint8_t(), 10)
+
+            @vsc.constraint
+            def default_c(self):
+                self.a > 10
+                self.b == 20
+                self.c == 30
+                vsc.soft(self.e == 50)
+                with vsc.implies(self.a == self.a):
+                    with vsc.if_then(self.a > 5):
+                        with vsc.if_then(self.a > 10):
+                            vsc.soft(self.b != 20)
+                            vsc.soft(self.d == 40)
+                            self.f == 60
+                        with vsc.implies(self.a > 10):
+                            vsc.soft(self.c != 30)
+                        with vsc.foreach(self.arr, idx=True) as i:
+                            vsc.soft(self.arr[i] == i)
+
+        nested = Nested()
+
+        nested.randomize(debug=1)
+        self.assertEqual(nested.b, 20)
+        self.assertEqual(nested.c, 30)
+        self.assertEqual(nested.d, 40)
+        self.assertEqual(nested.e, 50)
+        self.assertEqual(nested.f, 60)
+        for i in range(len(nested.arr)):
+            self.assertEqual(nested.arr[i], i)