Package daikon.simplify

Class Session

  • All Implemented Interfaces:
    Closeable, AutoCloseable
    public class Session
extends Object
implements Closeable
    A session is a channel to the Simplify theorem-proving tool. Once a session is started, commands may be applied to the session to make queries and manipulate its state.

    • Field Detail

      • dkconfig_simplify_max_iterations

        public static int dkconfig_simplify_max_iterations
        A non-negative integer, representing the largest number of iterations for which Simplify should be allowed to run on any single conjecture before giving up. Larger values may cause Simplify to run longer, but will increase the number of invariants that can be recognized as redundant. The default value is small enough to keep Simplify from running for more than a few seconds on any one conjecture, allowing it to verify most simple facts without getting bogged down in long searches. A value of 0 means not to bound the number of iterations at all, though see also the simplify_timeout parameter..

      • dkconfig_simplify_timeout

        public static int dkconfig_simplify_timeout
        A non-negative integer, representing the longest time period (in seconds) Simplify should be allowed to run on any single conjecture before giving up. Larger values may cause Simplify to run longer, but will increase the number of invariants that can be recognized as redundant. Roughly speaking, the time spent in Simplify will be bounded by this value, times the number of invariants generated, though it can be much less. A value of 0 means to not bound Simplify at all by time, though also see the option simplify_max_iterations. Beware that using this option might make Daikon's output depend on the speed of the machine it's run on.

      • dkconfig_verbose_progress

        public static int dkconfig_verbose_progress
        Positive values mean to print extra indications as each candidate invariant is passed to Simplify during the --suppress_redundant check. If the value is 1 or higher, a hyphen will be printed when each invariant is passed to Simplify, and then replaced by a T if the invariant was redundant, F if it was not found to be, and ? if Simplify gave up because of a time limit. If the value is 2 or higher, a < or > will also be printed for each invariant that is pushed onto or popped from from Simplify's assumption stack. This option is mainly intended for debugging purposes, but can also provide something to watch when Simplify takes a long time.

      • dkconfig_trace_input

        public static boolean dkconfig_trace_input
        Boolean. If true, the input to the Simplify theorem prover will also be directed to a file named simplifyN.in (where N is a number starting from 0) in the current directory. Simplify's operation can then be reproduced with a command like Simplify -nosc <simplify0.in. This is intended primarily for debugging when Simplify fails.

    • Constructor Detail

      • Session

        public Session()
        Starts a new Simplify process, which runs concurrently; I/O with this process will block. Initializes the simplify environment for interaction. Use Cmd objects to interact with this Session.

    • Method Detail

      • close

        public void close​(@GuardSatisfied Session this)
        Releases the resources held by this.
        Specified by:
        close in interface AutoCloseable
        Specified by:
        close in interface Closeable

      • main

        public static void main​(String[] args)
        for testing and playing around, not for real use
        Parameters:
        args - command-line arguments