package syguslib-utils

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Log and Stats modules

syguslib-utils
- Syguslib
  - Parser
  - Semantic
    
    Command
    
    Ident
    
    Lit
    
    Sort
    
    Term
  - Serializer
  - Solvers
    
    EmptyLog
    
    Logger
    
    NoStat
    
    SolverSystemConfig
    
    Statistics
    
    SygusSolver
    
    Config
    
    Log
    
    Stats
  - Sygus

Legend:
Library
Module
Module type
Parameter
Class
Class type

This module contains functions to interface with syntax-guided synthesis solvers using the SyGuS Language Standard Version 2 or 1 defined in Sygus. The synchronous and asynchronous solvers defined here are functors parametric on Logger and Statistics modules to automate logging on some output and collecting statistics on solver usage.

Log and Stats modules

module type Logger = sig ... end

The Logger module must provide some basic logging functionality, including error, debug and verbose messages. One can also set log_queries to true with a file, which allows the solver to write queries to a separate file.

module EmptyLog : Logger

An empty logger that ignores messages, and can be used to construct a solver if no logging is desired.

module type Statistics = sig ... end

The statistics modules allows logging start/termination time of subprocesses used to solve the syntax-guided synthesis instances. It should also provide a function that returns the time elapsed in the program.

module NoStat : Statistics

An empty Stats module that does nothing.

module type SolverSystemConfig = sig ... end

A module to provide the system configuration for syntax-guided synthesis solver. It indicates the path to the solver executables on the system. CVC4 and CVC5 are treted as one solver, with the boolean use_cvc5 () setting which version of CVC to use.

type solver_instance = {

s_name : string;
s_pid : int;
s_input_file : string;
s_output_file : string;
s_process : Lwt_process.process_out;

}

val online_solvers : (int * solver_instance) list ref

val mk_tmp_sl : string -> string

val commands_to_file : Sygus.program -> string -> unit

module SygusSolver
  (Stats : Statistics)
  (Log : Logger)
  (Config : SolverSystemConfig) : 
  sig ... end