Skip to content

No output of last term when using LogicPrinter.printSemisequent #243

Description

@wadoon

This issue was created at git.key-project.org where the discussions are preserved.


  • Mantis: MT-1584
  • Submitted on: 2016-04-01 by (at)weigl
  • Updated: 2016-04-01

Description

If you print a Semisequent through LogicPrinter.{printSemisequent,quickPrintSemisequent} the last term is not written.
Constructing a Sequent with the same Semisequent and calling LogicPrinter.quickPrintSequent results in the correct output.

The attached program produces the following output:

---8<----------------------
[false,p]
false,

false, p ==> false, p
--------------------->8----

You should see, that p is missing.

Steps to reproduce

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.op.Function;
import de.uka.ilkd.key.logic.op.Junctor;
import de.uka.ilkd.key.logic.sort.Sort;
import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.pp.NotationInfo;
import de.uka.ilkd.key.pp.ProgramPrinter;

import java.io.IOException;
import java.util.HashMap;

public class TestCaseBug1 {
    public static void main(String argv[]) {
        TermFactory termFactory = new TermFactory(new HashMap<>());
        Term p = termFactory.createTerm(new Function(new Name("p"), Sort.FORMULA));
        Term flse = termFactory.createTerm(Junctor.FALSE);

        SequentFormula b = new SequentFormula(p);
        SequentFormula c = new SequentFormula(flse);

        Semisequent a = new Semisequent(b);
        Semisequent d = a.insertFirst(c).semisequent();

        System.out.println(d);
        System.out.println(LogicPrinter.quickPrintSemisequent(d, null));

        Sequent s = new Sequent(d, d);
        System.out.println(LogicPrinter.quickPrintSequent(s, null));


    }
}

Additional Information

I tracked down the problem to Layouter.print. 
The term "p" (in the above example) is enqueued into the stream, but never dequeued. 
 

Files

History

  • (at)weigl -- (NEW_BUG) 2016-04-01

Attributes

  • Category: CLI
  • Status: NEW
  • Severity: MINOR
  • OS:
  • Target Version:
  • Resolution: OPEN
  • Priority: NORMAL
  • Reproducibility: ALWAYS
  • Platform: Linux
  • Commit: 5d09dae7fd1162f3343d1b91bdd5b2033cd1d182
  • Build:
  • Tags []
  • Labels: ~Command Line Interface ~Bug ~NORMAL
  • Version: 2.6

View in Mantis


Information:

  • created_at: 2017-05-29T02:32:55.942Z
  • updated_at: 2017-05-29T02:32:56.184Z
  • closed_at: None (closed_by: )
  • milestone:
  • user_notes_count: 0

Metadata

Metadata

Assignees

No one assigned

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions