I'm not sure I'm following this. Can you show me the before and after of
both types of side conditions for me to compare side-by-side?


On Wed, Apr 9, 2014 at 1:24 PM, Andrei Arusoaie <notifications@github.com>wrote:

> In
> src/javasources/KTool/src/org/kframework/backend/symbolic/ResolveLtlAttributes.java:
>
> > +                    // check if the path condition implies the rule condition
> > +                    // step 1: filter the condition and separate the smtValid part
> > +                    //         of it (operations which can be sent to the
> > +                    //         SMT solver) from the smtInvalid clauses.
> > +                    //         For the latter add predicates in condition.
> > +                    ConditionTransformer ct = new ConditionTransformer(context);
> > +                    Term smtInvalidCondition = (Term) requires.accept(ct);
> > +                    List<Term> filtered = ct.getFilteredTerms();
> > +                    filtered.add(BoolBuiltin.TRUE);
> > +                    Term smtValidCondition = AddPathCondition.andBool(filtered);
> > +                    Term predicates = AddPathCondition.andBool(ct.getGeneratedPredicates());
> > +
> > +                    // step 2: check the implication using the SMT solver using 'checkSat;
> > +                    // Note that we use smtValid instead of the rule condition because
> > +                    // predicates are not important when checking the implication.
> > +                    Term conditionNegation = KApp.of(KLabelConstant.NOTBOOL_KLABEL, smtValidCondition);
>
> It seemed to me too that this particular piece of code should be already
> present in the symbolic backend, but in fact it's not. The symbolic backend
> filters the rule condition and appends a call to checkSat, which verifies
> whether the (path condition /\ filtered rule condition) is NOT unsat. This
> is equivalent with detecting if the next possible program state is feasible.
> On the other hand, here we construct a different argument for checkSat
> which checks a logical implication (we want the argument (formula) sent to
> checkSat TO BE unsat) and we also add some predicates in the rule's side
> condition. Technically speaking, in two different places we build two
> different side conditions for rules. The common part is the replacement of
> the rule's condition, which I think it's easier to be done using
> rule.setRequires(newCondition) than creating a new Transformer for this.
> If you think the above explanation is not ok, then we can go into deeper
> the details of this.
>
> --
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/338/files#r11450406>
> .
>