Okay, yeah, that's what I thought. In that case it should be trivially
translatable into a method to check validity very similar to the one you
already have. Go ahead and make that change if you haven't already.
On Apr 10, 2014 12:12 AM, "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);
>
> Err.. I meant:
> isInt(n) /\ val(X, B) > 0 /\ checkSat(n > 0 /\ notBool(n=/=0)) == "unsat"
>
> val(X, B) > 0 stays in there. I wanted to delete only the predicate. The
> idea is that those functions that are not translatable to SMT remain
> untouched, while those which can be translated to the SMT go inside
> checkSat and I also generate predicates for them.
>
> --
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/338/files#r11470038>
> .
>