Okay, but I'm still confused. Now you don't have the val part of the side
condition at all? Why not?
On Apr 9, 2014 2:30 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);
>
> Ok, fair point. One method already exists, I'll just have to create the
> other one.
>
> Oh, I'm afraid I have confused you with isBool(val(X, B) > 0), which is
> not what I generate. Sorry for that, it's a little late for me...
> The actual thing I'm generating in that case is just:
> isInt(n) /\ checkSat(n > 0 /\ notBool(n=/=0)) == "unsat"
>
> However, if you have a function which has the smtlib attribute when
> defined in K then that function can be sent to the solver. Let us consider
> that function being the greatest common divisor - gcd. Then from the path
> condition n > 0 and the rule condition gcd(A, B) > 0 /\ n =/= 0 /\ isInt(n)
> I have to generate:
>
> isInt(n) /\ isInt(A) /\ isInt(B) /\ checkSat(n > 0 /\ notBool(gcd(A, B) >0
> /\ n=/=0)) == "unsat"
>
> --
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/338/files#r11454532>
> .
>