Cannot make constraint under if_then soft

[felixdube]

I have a constraint under an if_then, and I would like to make it soft, but it does not seem to work properly.
Here is a minimal example, which produce the following error:
vsc.model.solve_failure.SolveFailure: solve failure

import vsc

@vsc.randobj
class my_item():
    def __init__(self):
        self.a = vsc.rand_uint32_t()
        self.b = vsc.rand_uint32_t()

    @vsc.constraint
    def ab_c(self):
        vsc.solve_order(self.a, self.b)
        self.a > 10
        with vsc.if_then(self.a > 10):
            vsc.soft(self.b == 1)

item = my_item()
with item.randomize_with() as i:
    i.b == 10
print(item.b)

[alwilson]

Yeah, that if_then didn't get marked as a soft constraint when setting randomize_with(debug=1). I guess there could be a mix of soft and hard constraints nested under an if_then that would have to be separated out to do that correctly.

  Field: a is_rand=True [[11, 4294967295]]
  Field: b is_rand=True [[10, 10]]
  Constraint: (a > 10);

  Constraint: if ((a > 10)) {
(b == 1)}

  Constraint: (b == 10);

I tried to reference a dynamic constraint inside vsc.soft but hit a "TODO: support lambda references".

    @vsc.dynamic_constraint
    def b_1_c(self):
        with vsc.if_then(self.a > 10):
            self.b == 1

    @vsc.constraint
    def ab_c(self):
        vsc.solve_order(self.a, self.b)
        self.a > 10
        vsc.soft(self.b_1_c)

[mballance]

@felixdube, @alwilson, Yes, unfortunately soft constraints are currently only supported as top-level constraints (not under if/else). @alwilson, I agree with your conclusion that soft constraints will need to be broken out during processing to ensure the proper conditional context is associated with each nested soft constraint. I can certainly see that getting a bit complicated...

@felixdube, any feedback on how complex your intended usecase is? In other words, do you intend to have soft constraints nested under multiple levels of 'if'? Intend to have soft constraints nested in if/elsif/elsif/else structures?

Let me give thought to how best to approach this.

[felixdube]

@mballance I don't think I'll be using multiple levels of 'if', but maybe if/elsif/elsif/else. That being said, I've been disabling that constraint when I use randomize_with to force a specific value on that random attribute. So far, it's not a blocking issue for me.

[alwilson]

I explored supporting nested soft constraints by extending push_constraint_stmt(). Instead of adding a nested soft constraint to the current constraint scope it duplicates the current constraint stack without the other hard constraints and places it inside a ConstraintSoftModel. I only targeted and tested if_then, but I don't think it would be much cover others. I'm not sure how ForEach and arrays might work, although I think arrays get expanded later, which would still work if they were a standalone constraint.

alwilson@dcc61a1

Oh, and some debug output to see what it looks like with this method. The empty if looks weird, but boolector should throw away all of those, yeah?

Final Model:
  <anonymous> {
    rand unsigned [32] a
    rand unsigned [32] b
    constraint ab_c {
        if ((a > 10)) {
            soft (b == 1)
        }
        solve a before b
        (a > 10);
        if ((a > 10)) {
        }
    }
}

  constraint inline {
    (b == 10);
}

RandSet[0]
  Field: a is_rand=True [[11, 4294967295]]
  Field: b is_rand=True [[10, 10]]
  Constraint: (a > 10);

  Constraint: if ((a > 10)) {
}

  Constraint: (b == 10);

  SoftConstraint: if ((a > 10)) {
    soft (b == 1)
}

[mballance]

@alwilson, thanks for starting to look into this! The approach I had in mind was to update the rand_info_builder as follows:

• Add a stack to track if/implies conditions
• When you enter the 'true' block of an if/else or the body of an implies, push the condition. Pop the condition stack when leaving the 'true'/body block.
• When you enter the 'false' block of an if/else, push a new UnaryExprNot(condition) on the stack. Pop the condition stack when leaving the 'false block.
• When you encounter a soft constraint
  • If the condition stack is empty, add the soft constraint to the rand set
  • Else:
    • Build a condition by ANDing the expressions on the stack together
    • Create an implies constraint to represent the soft constraint: (AND_condition) -> soft_constraint
    • Add the implies constraint to the list of soft constraints in the rand set

What do you think?

Looking at an example:

@vsc.randobj
class my_item():
    def __init__(self):
        self.a = vsc.rand_uint32_t()
        self.b = vsc.rand_uint32_t()

    @vsc.constraint
    def ab_c(self):
        vsc.solve_order(self.a, self.b)
        self.a > 10
        with vsc.if_then(self.a > 10):
            vsc.soft(self.b == 1)
        with vsc.else_then:
            vsc.soft(self.b == 2)
            with vsc.if_then(self.a > 0):
                vsc.soft(self.b == 3)

• When we enter if_then(a>10), we would push (a>10)
• The soft constraint inside would get added to the rand set as: (a>10) -> self.b==1
• When we enter the else clause, we would push !(a>10)
• The soft constraint inside the 'else' clause would get added to the rand set as (!(a>10) -> self.b==2
• When we enter the nested if clause, we would push (a>0)
• The soft constraint inside would get added to the rand set as (!(a>10) && (a > 0)) -> self.b == 3

[alwilson]

@mballance Ah, so wait till after all the constraint expansion and bounds exploration. Then build up the soft constraint condition rather than reproduce the entire constraint stack. Does the bounds exploration take into account nested soft constraint? Or is there another bounds calculation after soft constraints are eliminated?

[mballance]

@alwilson, my thinking would be to do this after expansion and before initial SAT and elimination of conflicting soft constraints. So:

• Foreach expansion
• Rand-set building (and identification of relevant soft constraints)
• Foreach rand-set
  • SAT and eliminate any conflicting soft constraints. Here's where we need to ensure the soft constraints are properly conditioned
  • Bounds-exploration
  • Variable swizzling

[alwilson]

@mballance Alright, I think I get what you described for overriding the rand_info_builder visitors to get if_then and implies to add conditions to a stack and then on the soft constraint visitor create an implies of all those conditions for the soft constraint. I added in a bit in there to remove the soft constraint from the original constraint_l, but I think that permanently changes the model such that future calls don't work since there are no soft constraints in the model.

alwilson@4d6b4fc

Is there a way to disable or prevent building the original nested soft constraints? I started looking at the rand_set_node_builder, but I'm still trying to grok what it's doing in rs_node_builder.build(rs), where it builds the boolector node and ignores the return, versus a few lines later where it builds and stores the boolector nodes in constraint_l and soft_constraint_l.

[mballance]

@alwilson, really good point about the soft constraint being referenced from two places. Constraint objects are responsible for building themselves in the current PyVSC (and I regret that design decision every time we come to one of these issues...). Here's what I'm currently thinking:

• We have two build modes for soft constraints:

  • Normal -- called during build of the hard constraints
  • Special -- called during build of the soft constraints

• In 'Normal' mode, we cause the soft constraints to be ignored entirely and not rolled into the hard-constraint network

• In 'Special' mode, we build out the soft constraints knowing that they will be used as the body of our specially-constructed soft constraints implication constraints

• Change the 'build' method to accept an optional second parameter that controls whether the constraint is actually built, or if the method just returns None. This parameter should get a default of 'False' so it must be invoked specially to actually build and return the node.

pyvsc/src/vsc/model/constraint_soft_model.py

Lines 20 to 21 in a4fc51c

	def build(self, btor):
	return self.expr.build(btor)

• Change the 'build' method of constraint scope to be tolerant of sub-build calls that return None. Basically, a result of None should be ignored
  

  pyvsc/src/vsc/model/constraint_scope_model.py

  Lines 39 to 51 in a4fc51c

  	def build(self, btor):
  	ret = None
  	for c in self.constraint_l:
  	if ret is None:
  	ret = c.build(btor)
  	else:
  	ret = btor.And(ret, c.build(btor))
  	if ret is None:
  	# An empty block defaults to 'true'
  	ret = btor.Const(1, 1)
  	return ret

• Augment RandSetNodeBuilder to specifically iterate through the collected soft constraints of a randset to build them. This is needed because we re explicitly ignoring them during hard-constraint build.

What do you think?

With respect the RandSetNodeBuilder, it's doing the following:

• Ensure a solver variable is built for each field and referenced field by iterating through fields and constraints to identify referenced fields.
• Build solver constraint objects for each constraint by iterating through the constraints (phase==1)

In the current PyVSC, each field/constraint object holds its own solver data structure. So, RandSetNodeBuilder only ensures that all these objects are built and stored (it's just a visitor). The code you reference in 'Randomizer' creates lists of (PyObj,SolveObj) pairs. I don't remember why I called the build() method again vs grabbing the cached object, but the build() method is smart enough to only build the constraint if it hasn't been built yet.

[alwilson]

One issue with this approach is that it's hard to see and debug what has actually happened with the constraints and Boolector objects. btor.Dump() doesn't help much either and isn't easy to parse. Even the Dump(format='smt2') is hard to follow. It would be nice if the pretty print for the constraints reflected what's happened.

So in rand_set_node_builder there's a phase 0 and 1, and in phase 1 it's easy enough to intercept the c.build() on ConstraintSoftModel and use something like self.soft_phase to enable/disable building the soft constraint, but the part with the lists of (PyObj, SolveObj) it calls c.build() on each base constraint. I guess I could extend all build calls with the optional soft argument so that it gets passed down. Otherwise what I'm running into right now is that the rand_set_node_builder does the right thing by building hard constraints without soft and soft constraints with them enabled. Then build gets called again for those lists of tuples and it defaults to None for soft constraints in both hard and soft constraints and all soft constraints are lost. Maybe I missing a way to get that passed down. Hehe, I could also use a ConstraintSoftModel static variable to disable/enable building it globally, but that sounds like bad software design. :)

[alwilson]

Actually, I complained about adding the optional arg to the constraint_model build functions, but there's not that many that have build functions and it was pretty straightforward to pass down. So maybe it's not that bad! Seems to be passing tests now, although I probably should write new unit tests to really exercise nested soft constraints.

[mballance]

The fixes that @alwilson provided to support nested soft constraints are in the 0.8.3 release. Please try this release and let us know of any issues.

[felixdube]

Just confirming that the fix works fine on my side! Thank you