12367760548

Committed 17 Dec 2024 06:41AM UTC coverage: 65.285% (-0.6%) from 65.92%

Build # 12367760548

Build Type

push

github

Committed by

web-flow

Commit Message

Fixes GitHub coverage issue (#544)

* Update action.yml

* Update action.yml

Run Details

81020 of 124102 relevant lines covered (65.29%)

1509382.01 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

81.82

/src/io/yices_pp.h

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * PRETTY PRINTER FOR YICES TYPES AND TERMS
 */

#ifndef __YICES_PP_H
#define __YICES_PP_H

#include <stdint.h>
#include <stdio.h>
#include <stdbool.h>
#include <gmp.h>

#include "io/pretty_printer.h"
#include "terms/rationals.h"
#include "utils/object_stores.h"
#include "utils/string_buffers.h"
#include "model/concrete_values.h"


/*
 * ATOMIC OBJECTS
 */

/*
 * Each atomic tokens stores a basic object to be printed as
 * a single string. It consists of a pp_atomic_token prefix +
 * extra data that describes the actual object to be printed.
 * The user_tag field in the prefix stores the object type.
 */
typedef enum pp_atom_type {
  PP_CHAR_ATOM,       // content = a single char
  PP_STRING_ATOM,     // content = string terminated by '\0'
  PP_ID_ATOM,         // identifier = concatenation of a string and an index
  PP_VARID_ATOM,      // variant id = concatenation of a string, '!', and an index
  PP_TRUE_ATOM,       // true
  PP_FALSE_ATOM,      // false
  PP_INT32_ATOM,      // signed integer
  PP_UINT32_ATOM,     // unsigned integer
  PP_DOUBLE_ATOM,     // double number
  PP_RATIONAL_ATOM,   // rational
  PP_FINITEFIELD_ATOM, // finite field
  PP_BV64_ATOM,       // bitvector constant stored in a 64bit unsigned integer
  PP_BV_ATOM,         // bitvector constant stored in an array of words
  PP_BV_ZERO_ATOM,    // bitvector constant 0b00...00
  PP_BV_ONE_ATOM,     // bitvector constant 0b00...01
  PP_BV_NEGONE_ATOM,  // bitvector constant 0b11...11
  PP_QSTRING_ATOM,    // content = string with open and close quotes
  PP_SMT2_BV64_ATOM,  // like PP_BV64_ATOM but with SMT2 #b prefix
  PP_SMT2_BV_ATOM,    // like PP_BV_ATOM but with SMT2 prefix
  PP_SMT2_INTEGER_AS_REAL,   // print <integer>.0
  PP_SMT2_QID_ATOM,   // like PP_ID_ATOM with quotes
} pp_atom_type_t;

#define NUM_PP_ATOMS ((uint32_t) (PP_QID_ATOM+1))


/*
 * Descriptors of STRING, ID, BV, BV64 atoms
 * - for all atoms that have a string component, we optionally
 *   make a clone of the string  when the atom is created.
 * - if so, we set cloned to true.
 * - if not, we set cloned to false.
 * - same convention for the integer array bv in pp_bv_s
 */
typedef struct pp_string_s  {
  const char *string;
  bool cloned;
} pp_string_t;

typedef struct pp_id_s {
  const char *prefix;
  int32_t index;
  bool cloned;
} pp_id_t;

typedef struct pp_ff_s {
  mpz_t value;
  mpz_t mod;
} pp_ff_t;

typedef struct pp_bv64_s {
  uint64_t bv;
  uint32_t nbits;
} pp_bv64_t;

typedef struct pp_bv_s {
  uint32_t *bv;
  uint32_t nbits;
  bool cloned;
} pp_bv_t;


/*
 * Descriptor of quoted string atoms
 * - quote[0] = open quote
 * - quote[1] = close_quote
 * - str = what's between the quotes
 */
typedef struct pp_qstr_s {
  const char *str;
  char quote[2];
  bool cloned;
} pp_qstr_t;


/*
 * Descriptor of quoted id
 */
typedef struct pp_qid_s {
  const char *prefix;
  int32_t index;
  char quote[2];
  bool cloned;
} pp_qid_t;


/*
 * Full atomic token
 */
typedef struct pp_atom_s {
  pp_atomic_token_t tk; // prefix defined in pretty_printer.h
  union {
    char c;
    pp_string_t string;
    pp_id_t id;
    int32_t i32;
    uint32_t u32;
    double dbl;
    rational_t rat;
    pp_ff_t ff;
    pp_bv64_t bv64;
    pp_bv_t bv;
    pp_qstr_t qstr;
    pp_qid_t qid;
  } data;
} pp_atom_t;



/*
 * OPEN-BLOCK TOKENS
 */

/*
 * Each open-block token is defined by an identifier.
 * For each identifier, the module maintains the following
 * information in internal tables:
 * - string label
 * - label size
 * - preferred format for that block
 * - indentation and short indentation
 * - two boolean flags (sep allowed + parenthesis for that block)
 */

// list of open-block identifiers
typedef enum {
  PP_OPEN,               // empty label, no parenthesis, HMT layout
  PP_OPEN_PAR,           // empty label, open parenthesis, HMT layout
  PP_OPEN_VPAR,          // empty label, open parenthesis, V layout

  PP_OPEN_BV_TYPE,
  PP_OPEN_FF_TYPE,
  PP_OPEN_FUN_TYPE,
  PP_OPEN_TUPLE_TYPE,

  PP_OPEN_ITE,
  PP_OPEN_UPDATE,
  PP_OPEN_TUPLE,
  PP_OPEN_SELECT,
  PP_OPEN_EQ,
  PP_OPEN_NEQ,
  PP_OPEN_DISTINCT,
  PP_OPEN_FORALL,
  PP_OPEN_EXISTS,
  PP_OPEN_LAMBDA,
  PP_OPEN_NOT,
  PP_OPEN_OR,
  PP_OPEN_AND,
  PP_OPEN_XOR,
  PP_OPEN_IMPLIES,
  PP_OPEN_BIT,
  PP_OPEN_PROD,
  PP_OPEN_POWER,
  PP_OPEN_SUM,
  PP_OPEN_DIV,
  PP_OPEN_MINUS,
  PP_OPEN_GE,
  PP_OPEN_LT,
  PP_OPEN_ROOT_ATOM,

  PP_OPEN_BV_ARRAY,
  PP_OPEN_BV_SIGN_EXTEND,
  PP_OPEN_BV_ZERO_EXTEND,
  PP_OPEN_BV_EXTRACT,
  PP_OPEN_BV_CONCAT,
  PP_OPEN_BV_SUM,
  PP_OPEN_BV_PROD,
  PP_OPEN_BV_POWER,
  PP_OPEN_BV_DIV,
  PP_OPEN_BV_REM,
  PP_OPEN_BV_SDIV,
  PP_OPEN_BV_SREM,
  PP_OPEN_BV_SMOD,
  PP_OPEN_BV_SHL,
  PP_OPEN_BV_LSHR,
  PP_OPEN_BV_ASHR,
  PP_OPEN_BV_GE,
  PP_OPEN_BV_LT,
  PP_OPEN_BV_SGE,
  PP_OPEN_BV_SLT,

  // more arithmetic stuff
  PP_OPEN_IS_INT,
  PP_OPEN_FLOOR,
  PP_OPEN_CEIL,
  PP_OPEN_ABS,
  PP_OPEN_IDIV,
  PP_OPEN_IMOD,
  PP_OPEN_DIVIDES,

  // blocks used in pp_model
  PP_OPEN_FUNCTION,   // (function ...)
  PP_OPEN_TYPE,       // (type ..)
  PP_OPEN_DEFAULT,    // (default x)

  PP_OPEN_CONST_DEF,  // (constant i of <type>)
  PP_OPEN_UNINT_DEF,  // (unint i of <type>)
  PP_OPEN_VAR_DEF,    // (var i of <type>)

  // more for the SMT2 model syntax
  PP_OPEN_SMT2_BV_DEC, // (_ bv... ..)
  PP_OPEN_SMT2_BV_TYPE, // (_ BitVec ...)
  PP_OPEN_SMT2_FF_DEC, // (_ ff... ..)
  PP_OPEN_SMT2_FF_TYPE, // (_ FiniteField ...)
  PP_OPEN_SMT2_MODEL,   // (model ...)
  PP_OPEN_SMT2_DEF,     // (define-fun ...)
  PP_OPEN_SMT2_STORE,   // (store <array> <index> <value>)
  PP_OPEN_SMT2_AS_CONST,  // (as const <type> <value>)  (for constant arrays. type is the array type).
  PP_OPEN_SMT2_AS,        // (as <identifier> <type> )
} pp_open_type_t;

#define NUM_PP_OPENS ((uint32_t) (PP_OPEN_SMT2_AS + 1))



/*
 * CLOSE-BLOCK TOKENS
 */

/*
 * Two versions: close with a parenthesis or close with nothing
 */
typedef enum {
  PP_CLOSE,
  PP_CLOSE_PAR,
} pp_close_type_t;




/*
 * FULL PRETTY PRINTER
 */

/*
 * - pp: pretty printer object
 * - open_store: for allocation of open-block tokens
 * - atom_store: for allocation of atomic tokens
 * - two statically allocated close tokens
 * - a string buffer for conversion of atoms to strings
 */
typedef struct yices_pp_s {
  pp_t pp;
  object_store_t open_store;
  object_store_t atom_store;
  pp_close_token_t close_nopar;
  pp_close_token_t close_par;
  void *close[2];  // close[0] = nopar, close[1] = par
  string_buffer_t buffer;
} yices_pp_t;




/*
 * Initialize the internal table of open-token descriptors
 * - this must be called first.
 */
extern void init_yices_pp_tables(void);

/*
 * Initialize a pretty printer
 * - file = output file (must be NULL or a stream open for write)
 * - area = display area (cf. pretty_printer.h) 
 * - mode = initial print mode (cf. pretty printer.h)
 * - indent = initial indentation
 *
 * If file is NULL, then the pretty printer is initialized for 
 * a string buffer. Otherwise, it writes to file.
 *
 * If area is NULL, then the default is used (cf. pretty_printer.h)
 */
extern void init_yices_pp(yices_pp_t *printer, FILE *file, pp_area_t *area,
                          pp_print_mode_t mode, uint32_t indent);


/*
 * Variant: use default mode and indent
 */
static inline void init_default_yices_pp(yices_pp_t *printer, FILE *file, pp_area_t *area) {
  init_yices_pp(printer, file, area, PP_VMODE, 0);
}


/*
 * Flush: print everything pending + a newline
 * - then reset the line counter to 0
 */
extern void flush_yices_pp(yices_pp_t *printer);


/*
 * Extract the string constructed by printer
 * - printer must be initialized for a string (i.e., with file = NULL)
 * - this must be called after flush
 * - the string length is stored in *len
 * - the returned string must be deleted when no-longer needed using free.
 */
extern char *yices_pp_get_string(yices_pp_t *printer, uint32_t *len);


/*
 * Delete a pretty printer
 * - if flush is true, print everything pending + a newline
 * - then free all memory used
 */
extern void delete_yices_pp(yices_pp_t *printer, bool flush);


/*
 * Check for saturation: when this is true, we should stop sending tokens
 */
static inline bool yices_pp_is_full(yices_pp_t *printer) {
  return pp_is_full(&printer->pp);
}


/*
 * Get the print depth = number of open blocks sent to the printer
 */
static inline uint32_t yices_pp_depth(yices_pp_t *printer) {
  return pp_depth(&printer->pp);
}


/*
 * Check for print error and error code
 */
static inline bool yices_pp_print_failed(yices_pp_t *printer) {
  return writer_failed(&printer->pp.printer.writer);
}

static inline int yices_pp_errno(yices_pp_t *printer) {
  return writer_errno(&printer->pp.printer.writer);
}



/*
 * PRINT ATOMS
 */

/*
 * Safe atoms:
 * - pp_rational make an internal copy of q
 * - pp_mpz, pp_mpq: the z or the q is translated to a rational
 * - pp_algebraic: converted to a double
 */
extern void pp_char(yices_pp_t *printer, char c);
extern void pp_bool(yices_pp_t *printer, bool tt);
extern void pp_int32(yices_pp_t *printer, int32_t x);
extern void pp_uint32(yices_pp_t *printer, uint32_t x);
extern void pp_mpz(yices_pp_t *printer, mpz_t z);
extern void pp_mpq(yices_pp_t *printer, mpq_t q);
extern void pp_rational(yices_pp_t *printer, const rational_t *q);
extern void pp_bv64(yices_pp_t *printer, uint64_t bv, uint32_t n);
extern void pp_finitefield(yices_pp_t *printer, const value_ff_t *v);
extern void pp_algebraic(yices_pp_t *printer, const void *a);

/*
 * String and bv atoms without cloning
 * - pp_id(printer, prefix, id): prints <prefix><id>
 *   (example, pp_id(printer, "tau_", 23) prints "tau_23")
 * - pp_varid(printer, prefix, id): prints <prefix>!<id>
 * - for pp_bv64 and pp_bv, n is the number of bits (n must be positive)
 *
 * Function pp_string does not make a copy of the string s so s must
 * remain valid until the printer is deleted. Same thing for prefix
 * function in pp_id. Function pp_bv does not make a copy
 * of the word array *bv either.
 */
extern void pp_string(yices_pp_t *printer, const char *s);
extern void pp_id(yices_pp_t *printer, const char *prefix, int32_t id);
extern void pp_varid(yices_pp_t *printer, const char *prefix, int32_t id);
extern void pp_bv(yices_pp_t *printer, uint32_t *bv, uint32_t n);

/*
 * String and bv atoms with cloning
 * - these print the same  thing as above but they make an internal
 *   copy of the string or bv array.
 */
extern void pp_clone_string(yices_pp_t *printer, const char *s);
extern void pp_clone_id(yices_pp_t *printer, const char *prefix, int32_t id);
extern void pp_clone_varid(yices_pp_t *printer, const char *prefix, int32_t id);
extern void pp_clone_bv(yices_pp_t *printer, uint32_t *bv, uint32_t n);



/*
 * Print 0b0...0, 0b0...01, or 0b1...1: n = number of bits
 */
extern void pp_bv_zero(yices_pp_t *printer, uint32_t n);
extern void pp_bv_one(yices_pp_t *printer, uint32_t n);
extern void pp_bv_minus_one(yices_pp_t *printer, uint32_t n);


/*
 * Separator token: same as a string, but the pretty printer
 * does not add spaces before and after the token
 */
extern void pp_separator(yices_pp_t *printer, const char *s);

/*
 * Quoted string:
 * - open_quote = character before the string (or '\0' if nothing needed)
 * - close_quote = character after the string (or '\0' if nothing needed)
 *
 * Examples
 *   pp_qstring(printer, '"', '"', "abcde") will print "abcde" (quotes included)
 *   pp_qstring(printer, '\'', '\0', "abcde") will print 'abcde
 *
 * The default version does not make a copy of s, so s must remain valid until
 * the printer is flushed. The clone  version makes an internal copy of s.
 */
extern void pp_qstring(yices_pp_t *printer, char open_quote, char close_quote, const char *s);
extern void pp_clone_qstring(yices_pp_t *printer, char open_quote, char close_quote, const char *s);

/*
 * Quoted id:
 * - same as pp_id but with open and close quote
 *
 * Examples: pp_quoted_id(printer, "x!", 20, '|', '|') will print |x!20|
 *
 * The default version does not make a copy of prefix, so prefix must remain valid until
 * the printer is flushed. The clone  version makes an internal copy of prefix.
 */
extern void pp_quoted_id(yices_pp_t *printer, const char *prefix, int32_t id, char open_quote, char close_quote);
extern void pp_clone_quoted_id(yices_pp_t *printer, const char *prefix, int32_t id, char open_quote, char close_quote);

/*
 * Variant(s) for SMT2 atoms
 * - pp_smt2_bv uses the prefix #b instead of 0b
 *
 * pp_smt2_bv: does not make a copy of bv.
 * pp_clone_smt2_bv: makes an internal copy.
 */
extern void pp_smt2_bv64(yices_pp_t *printer, uint64_t bv, uint32_t n);
extern void pp_smt2_bv(yices_pp_t *printer, uint32_t *bv, uint32_t n);
extern void pp_clone_smt2_bv(yices_pp_t *printer, uint32_t *bv, uint32_t n);

/*
 * Another SMT2 special
 * - print an integer converted to real as in 12.0 instead of 12
 * - the value is provided as a rational but the denominator must be one.
 */
extern void pp_smt2_integer_as_real(yices_pp_t *printer, rational_t *q);


/*
 * PRINT UTILITIES BORROWED FROM SMT2 PRINTER
 */

/*
 * Default printer for bitvector
 */
extern void pp_bitvector(yices_pp_t *printer, value_bv_t *b);

/*
 * For uninterpreted constants: always print an abstract name
 */
extern void pp_unint_name(yices_pp_t *printer, value_t c);

/*
 * Function: always use a default name, even if fun has a name
 */
extern void pp_fun_name(yices_pp_t *printer, value_t c);

/*
 * Format to display a function:
 * (function <name>
 *   (type (-> tau_1 ... tau_n sigma))
 *   (= (<name> x_1 ... x_n) y_1)
 *    ...
 *   (default z))
 */
extern void pp_function_header(yices_pp_t *printer, value_table_t *table, value_t c, type_t tau);

/*
 * Print the function c
 * - if show_default is true, also print the default falue
 */
extern void pp_function(yices_pp_t *printer, value_table_t *table, value_t c, bool show_default);

/*
 * Expand update c and print it as a function
 * - the name "@fun_c"
 * - if show_default is true, also print the default value
 */
extern void normalize_and_pp_update(yices_pp_t *printer, value_table_t *table, value_t c, bool show_default);

/*
 * Print object c on stream f
 *
 * There's no support for tuples or mappings in SMT2. They should never occur here.
 */
extern void pp_object(yices_pp_t *printer, value_table_t *table, value_t c);

/*
 * Print object c on FILE f
 *
 */
extern void pp_value(FILE *f, value_table_t *table, value_t c);



/*
 * OPEN AND CLOSE BLOCK
 */

/*
 * Start an block given the open-block id
 */
extern void pp_open_block(yices_pp_t *printer, pp_open_type_t id);

/*
 * Close a block
 * - par: true if a parenthesis is required
 *        false to close and print nothing
 */
extern void pp_close_block(yices_pp_t *printer, bool par);


#endif /* __YICES_PP_H */

1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	/*
20	* PRETTY PRINTER FOR YICES TYPES AND TERMS
21	*/
22
23	#ifndef __YICES_PP_H
24	#define __YICES_PP_H
25
26	#include <stdint.h>
27	#include <stdio.h>
28	#include <stdbool.h>
29	#include <gmp.h>
30
31	#include "io/pretty_printer.h"
32	#include "terms/rationals.h"
33	#include "utils/object_stores.h"
34	#include "utils/string_buffers.h"
35	#include "model/concrete_values.h"
36
37
38	/*
39	* ATOMIC OBJECTS
40	*/
41
42	/*
43	* Each atomic tokens stores a basic object to be printed as
44	* a single string. It consists of a pp_atomic_token prefix +
45	* extra data that describes the actual object to be printed.
46	* The user_tag field in the prefix stores the object type.
47	*/
48	typedef enum pp_atom_type {
49	PP_CHAR_ATOM, // content = a single char
50	PP_STRING_ATOM, // content = string terminated by '\0'
51	PP_ID_ATOM, // identifier = concatenation of a string and an index
52	PP_VARID_ATOM, // variant id = concatenation of a string, '!', and an index
53	PP_TRUE_ATOM, // true
54	PP_FALSE_ATOM, // false
55	PP_INT32_ATOM, // signed integer
56	PP_UINT32_ATOM, // unsigned integer
57	PP_DOUBLE_ATOM, // double number
58	PP_RATIONAL_ATOM, // rational
59	PP_FINITEFIELD_ATOM, // finite field
60	PP_BV64_ATOM, // bitvector constant stored in a 64bit unsigned integer
61	PP_BV_ATOM, // bitvector constant stored in an array of words
62	PP_BV_ZERO_ATOM, // bitvector constant 0b00...00
63	PP_BV_ONE_ATOM, // bitvector constant 0b00...01
64	PP_BV_NEGONE_ATOM, // bitvector constant 0b11...11
65	PP_QSTRING_ATOM, // content = string with open and close quotes
66	PP_SMT2_BV64_ATOM, // like PP_BV64_ATOM but with SMT2 #b prefix
67	PP_SMT2_BV_ATOM, // like PP_BV_ATOM but with SMT2 prefix
68	PP_SMT2_INTEGER_AS_REAL, // print <integer>.0
69	PP_SMT2_QID_ATOM, // like PP_ID_ATOM with quotes
70	} pp_atom_type_t;
71
72	#define NUM_PP_ATOMS ((uint32_t) (PP_QID_ATOM+1))
73
74
75	/*
76	* Descriptors of STRING, ID, BV, BV64 atoms
77	* - for all atoms that have a string component, we optionally
78	* make a clone of the string when the atom is created.
79	* - if so, we set cloned to true.
80	* - if not, we set cloned to false.
81	* - same convention for the integer array bv in pp_bv_s
82	*/
83	typedef struct pp_string_s {
84	const char *string;
85	bool cloned;
86	} pp_string_t;
87
88	typedef struct pp_id_s {
89	const char *prefix;
90	int32_t index;
91	bool cloned;
92	} pp_id_t;
93
94	typedef struct pp_ff_s {
95	mpz_t value;
96	mpz_t mod;
97	} pp_ff_t;
98
99	typedef struct pp_bv64_s {
100	uint64_t bv;
101	uint32_t nbits;
102	} pp_bv64_t;
103
104	typedef struct pp_bv_s {
105	uint32_t *bv;
106	uint32_t nbits;
107	bool cloned;
108	} pp_bv_t;
109
110
111	/*
112	* Descriptor of quoted string atoms
113	* - quote[0] = open quote
114	* - quote[1] = close_quote
115	* - str = what's between the quotes
116	*/
117	typedef struct pp_qstr_s {
118	const char *str;
119	char quote[2];
120	bool cloned;
121	} pp_qstr_t;
122
123
124	/*
125	* Descriptor of quoted id
126	*/
127	typedef struct pp_qid_s {
128	const char *prefix;
129	int32_t index;
130	char quote[2];
131	bool cloned;
132	} pp_qid_t;
133
134
135	/*
136	* Full atomic token
137	*/
138	typedef struct pp_atom_s {
139	pp_atomic_token_t tk; // prefix defined in pretty_printer.h
140	union {
141	char c;
142	pp_string_t string;
143	pp_id_t id;
144	int32_t i32;
145	uint32_t u32;
146	double dbl;
147	rational_t rat;
148	pp_ff_t ff;
149	pp_bv64_t bv64;
150	pp_bv_t bv;
151	pp_qstr_t qstr;
152	pp_qid_t qid;
153	} data;
154	} pp_atom_t;
155
156
157
158	/*
159	* OPEN-BLOCK TOKENS
160	*/
161
162	/*
163	* Each open-block token is defined by an identifier.
164	* For each identifier, the module maintains the following
165	* information in internal tables:
166	* - string label
167	* - label size
168	* - preferred format for that block
169	* - indentation and short indentation
170	* - two boolean flags (sep allowed + parenthesis for that block)
171	*/
172
173	// list of open-block identifiers
174	typedef enum {
175	PP_OPEN, // empty label, no parenthesis, HMT layout
176	PP_OPEN_PAR, // empty label, open parenthesis, HMT layout
177	PP_OPEN_VPAR, // empty label, open parenthesis, V layout
178
179	PP_OPEN_BV_TYPE,
180	PP_OPEN_FF_TYPE,
181	PP_OPEN_FUN_TYPE,
182	PP_OPEN_TUPLE_TYPE,
183
184	PP_OPEN_ITE,
185	PP_OPEN_UPDATE,
186	PP_OPEN_TUPLE,
187	PP_OPEN_SELECT,
188	PP_OPEN_EQ,
189	PP_OPEN_NEQ,
190	PP_OPEN_DISTINCT,
191	PP_OPEN_FORALL,
192	PP_OPEN_EXISTS,
193	PP_OPEN_LAMBDA,
194	PP_OPEN_NOT,
195	PP_OPEN_OR,
196	PP_OPEN_AND,
197	PP_OPEN_XOR,
198	PP_OPEN_IMPLIES,
199	PP_OPEN_BIT,
200	PP_OPEN_PROD,
201	PP_OPEN_POWER,
202	PP_OPEN_SUM,
203	PP_OPEN_DIV,
204	PP_OPEN_MINUS,
205	PP_OPEN_GE,
206	PP_OPEN_LT,
207	PP_OPEN_ROOT_ATOM,
208
209	PP_OPEN_BV_ARRAY,
210	PP_OPEN_BV_SIGN_EXTEND,
211	PP_OPEN_BV_ZERO_EXTEND,
212	PP_OPEN_BV_EXTRACT,
213	PP_OPEN_BV_CONCAT,
214	PP_OPEN_BV_SUM,
215	PP_OPEN_BV_PROD,
216	PP_OPEN_BV_POWER,
217	PP_OPEN_BV_DIV,
218	PP_OPEN_BV_REM,
219	PP_OPEN_BV_SDIV,
220	PP_OPEN_BV_SREM,
221	PP_OPEN_BV_SMOD,
222	PP_OPEN_BV_SHL,
223	PP_OPEN_BV_LSHR,
224	PP_OPEN_BV_ASHR,
225	PP_OPEN_BV_GE,
226	PP_OPEN_BV_LT,
227	PP_OPEN_BV_SGE,
228	PP_OPEN_BV_SLT,
229
230	// more arithmetic stuff
231	PP_OPEN_IS_INT,
232	PP_OPEN_FLOOR,
233	PP_OPEN_CEIL,
234	PP_OPEN_ABS,
235	PP_OPEN_IDIV,
236	PP_OPEN_IMOD,
237	PP_OPEN_DIVIDES,
238
239	// blocks used in pp_model
240	PP_OPEN_FUNCTION, // (function ...)
241	PP_OPEN_TYPE, // (type ..)
242	PP_OPEN_DEFAULT, // (default x)
243
244	PP_OPEN_CONST_DEF, // (constant i of <type>)
245	PP_OPEN_UNINT_DEF, // (unint i of <type>)
246	PP_OPEN_VAR_DEF, // (var i of <type>)
247
248	// more for the SMT2 model syntax
249	PP_OPEN_SMT2_BV_DEC, // (_ bv... ..)
250	PP_OPEN_SMT2_BV_TYPE, // (_ BitVec ...)
251	PP_OPEN_SMT2_FF_DEC, // (_ ff... ..)
252	PP_OPEN_SMT2_FF_TYPE, // (_ FiniteField ...)
253	PP_OPEN_SMT2_MODEL, // (model ...)
254	PP_OPEN_SMT2_DEF, // (define-fun ...)
255	PP_OPEN_SMT2_STORE, // (store <array> <index> <value>)
256	PP_OPEN_SMT2_AS_CONST, // (as const <type> <value>) (for constant arrays. type is the array type).
257	PP_OPEN_SMT2_AS, // (as <identifier> <type> )
258	} pp_open_type_t;
259
260	#define NUM_PP_OPENS ((uint32_t) (PP_OPEN_SMT2_AS + 1))
261
262
263
264	/*
265	* CLOSE-BLOCK TOKENS
266	*/
267
268	/*
269	* Two versions: close with a parenthesis or close with nothing
270	*/
271	typedef enum {
272	PP_CLOSE,
273	PP_CLOSE_PAR,
274	} pp_close_type_t;
275
276
277
278
279	/*
280	* FULL PRETTY PRINTER
281	*/
282
283	/*
284	* - pp: pretty printer object
285	* - open_store: for allocation of open-block tokens
286	* - atom_store: for allocation of atomic tokens
287	* - two statically allocated close tokens
288	* - a string buffer for conversion of atoms to strings
289	*/
290	typedef struct yices_pp_s {
291	pp_t pp;
292	object_store_t open_store;
293	object_store_t atom_store;
294	pp_close_token_t close_nopar;
295	pp_close_token_t close_par;
296	void *close[2]; // close[0] = nopar, close[1] = par
297	string_buffer_t buffer;
298	} yices_pp_t;
299
300
301
302
303	/*
304	* Initialize the internal table of open-token descriptors
305	* - this must be called first.
306	*/
307	extern void init_yices_pp_tables(void);
308
309	/*
310	* Initialize a pretty printer
311	* - file = output file (must be NULL or a stream open for write)
312	* - area = display area (cf. pretty_printer.h)
313	* - mode = initial print mode (cf. pretty printer.h)
314	* - indent = initial indentation
315	*
316	* If file is NULL, then the pretty printer is initialized for
317	* a string buffer. Otherwise, it writes to file.
318	*
319	* If area is NULL, then the default is used (cf. pretty_printer.h)
320	*/
321	extern void init_yices_pp(yices_pp_t printer, FILE file, pp_area_t *area,
322	pp_print_mode_t mode, uint32_t indent);
323
324
325	/*
326	* Variant: use default mode and indent
327	*/
328	static inline void init_default_yices_pp(yices_pp_t printer, FILE file, pp_area_t *area) {	2✔
329	init_yices_pp(printer, file, area, PP_VMODE, 0);	2✔
330	}	2✔
331
332
333	/*
334	* Flush: print everything pending + a newline
335	* - then reset the line counter to 0
336	*/
337	extern void flush_yices_pp(yices_pp_t *printer);
338
339
340	/*
341	* Extract the string constructed by printer
342	* - printer must be initialized for a string (i.e., with file = NULL)
343	* - this must be called after flush
344	* - the string length is stored in *len
345	* - the returned string must be deleted when no-longer needed using free.
346	*/
347	extern char yices_pp_get_string(yices_pp_t printer, uint32_t *len);
348
349
350	/*
351	* Delete a pretty printer
352	* - if flush is true, print everything pending + a newline
353	* - then free all memory used
354	*/
355	extern void delete_yices_pp(yices_pp_t *printer, bool flush);
356
357
358	/*
359	* Check for saturation: when this is true, we should stop sending tokens
360	*/
361	static inline bool yices_pp_is_full(yices_pp_t *printer) {	349✔
362	return pp_is_full(&printer->pp);	349✔
363	}
364
365
366	/*
367	* Get the print depth = number of open blocks sent to the printer
368	*/
369	static inline uint32_t yices_pp_depth(yices_pp_t *printer) {	250✔
370	return pp_depth(&printer->pp);	250✔
371	}
372
373
374	/*
375	* Check for print error and error code
376	*/
377	static inline bool yices_pp_print_failed(yices_pp_t *printer) {	2✔
378	return writer_failed(&printer->pp.printer.writer);	2✔
379	}
380
381	static inline int yices_pp_errno(yices_pp_t *printer) {	×
382	return writer_errno(&printer->pp.printer.writer);	×
383	}
384
385
386
387	/*
388	* PRINT ATOMS
389	*/
390
391	/*
392	* Safe atoms:
393	* - pp_rational make an internal copy of q
394	* - pp_mpz, pp_mpq: the z or the q is translated to a rational
395	* - pp_algebraic: converted to a double
396	*/
397	extern void pp_char(yices_pp_t *printer, char c);
398	extern void pp_bool(yices_pp_t *printer, bool tt);
399	extern void pp_int32(yices_pp_t *printer, int32_t x);
400	extern void pp_uint32(yices_pp_t *printer, uint32_t x);
401	extern void pp_mpz(yices_pp_t *printer, mpz_t z);
402	extern void pp_mpq(yices_pp_t *printer, mpq_t q);
403	extern void pp_rational(yices_pp_t printer, const rational_t q);
404	extern void pp_bv64(yices_pp_t *printer, uint64_t bv, uint32_t n);
405	extern void pp_finitefield(yices_pp_t printer, const value_ff_t v);
406	extern void pp_algebraic(yices_pp_t printer, const void a);
407
408	/*
409	* String and bv atoms without cloning
410	* - pp_id(printer, prefix, id): prints <prefix><id>
411	* (example, pp_id(printer, "tau_", 23) prints "tau_23")
412	* - pp_varid(printer, prefix, id): prints <prefix>!<id>
413	* - for pp_bv64 and pp_bv, n is the number of bits (n must be positive)
414	*
415	* Function pp_string does not make a copy of the string s so s must
416	* remain valid until the printer is deleted. Same thing for prefix
417	* function in pp_id. Function pp_bv does not make a copy
418	* of the word array *bv either.
419	*/
420	extern void pp_string(yices_pp_t printer, const char s);
421	extern void pp_id(yices_pp_t printer, const char prefix, int32_t id);
422	extern void pp_varid(yices_pp_t printer, const char prefix, int32_t id);
423	extern void pp_bv(yices_pp_t printer, uint32_t bv, uint32_t n);
424
425	/*
426	* String and bv atoms with cloning
427	* - these print the same thing as above but they make an internal
428	* copy of the string or bv array.
429	*/
430	extern void pp_clone_string(yices_pp_t printer, const char s);
431	extern void pp_clone_id(yices_pp_t printer, const char prefix, int32_t id);
432	extern void pp_clone_varid(yices_pp_t printer, const char prefix, int32_t id);
433	extern void pp_clone_bv(yices_pp_t printer, uint32_t bv, uint32_t n);
434
435
436
437	/*
438	* Print 0b0...0, 0b0...01, or 0b1...1: n = number of bits
439	*/
440	extern void pp_bv_zero(yices_pp_t *printer, uint32_t n);
441	extern void pp_bv_one(yices_pp_t *printer, uint32_t n);
442	extern void pp_bv_minus_one(yices_pp_t *printer, uint32_t n);
443
444
445	/*
446	* Separator token: same as a string, but the pretty printer
447	* does not add spaces before and after the token
448	*/
449	extern void pp_separator(yices_pp_t printer, const char s);
450
451	/*
452	* Quoted string:
453	* - open_quote = character before the string (or '\0' if nothing needed)
454	* - close_quote = character after the string (or '\0' if nothing needed)
455	*
456	* Examples
457	* pp_qstring(printer, '"', '"', "abcde") will print "abcde" (quotes included)
458	* pp_qstring(printer, '\'', '\0', "abcde") will print 'abcde
459	*
460	* The default version does not make a copy of s, so s must remain valid until
461	* the printer is flushed. The clone version makes an internal copy of s.
462	*/
463	extern void pp_qstring(yices_pp_t printer, char open_quote, char close_quote, const char s);
464	extern void pp_clone_qstring(yices_pp_t printer, char open_quote, char close_quote, const char s);
465
466	/*
467	* Quoted id:
468	* - same as pp_id but with open and close quote
469	*
470	* Examples: pp_quoted_id(printer, "x!", 20, '\|', '\|') will print \|x!20\|
471	*
472	* The default version does not make a copy of prefix, so prefix must remain valid until
473	* the printer is flushed. The clone version makes an internal copy of prefix.
474	*/
475	extern void pp_quoted_id(yices_pp_t printer, const char prefix, int32_t id, char open_quote, char close_quote);
476	extern void pp_clone_quoted_id(yices_pp_t printer, const char prefix, int32_t id, char open_quote, char close_quote);
477
478	/*
479	* Variant(s) for SMT2 atoms
480	* - pp_smt2_bv uses the prefix #b instead of 0b
481	*
482	* pp_smt2_bv: does not make a copy of bv.
483	* pp_clone_smt2_bv: makes an internal copy.
484	*/
485	extern void pp_smt2_bv64(yices_pp_t *printer, uint64_t bv, uint32_t n);
486	extern void pp_smt2_bv(yices_pp_t printer, uint32_t bv, uint32_t n);
487	extern void pp_clone_smt2_bv(yices_pp_t printer, uint32_t bv, uint32_t n);
488
489	/*
490	* Another SMT2 special
491	* - print an integer converted to real as in 12.0 instead of 12
492	* - the value is provided as a rational but the denominator must be one.
493	*/
494	extern void pp_smt2_integer_as_real(yices_pp_t printer, rational_t q);
495
496
497	/*
498	* PRINT UTILITIES BORROWED FROM SMT2 PRINTER
499	*/
500
501	/*
502	* Default printer for bitvector
503	*/
504	extern void pp_bitvector(yices_pp_t printer, value_bv_t b);
505
506	/*
507	* For uninterpreted constants: always print an abstract name
508	*/
509	extern void pp_unint_name(yices_pp_t *printer, value_t c);
510
511	/*
512	* Function: always use a default name, even if fun has a name
513	*/
514	extern void pp_fun_name(yices_pp_t *printer, value_t c);
515
516	/*
517	* Format to display a function:
518	* (function <name>
519	* (type (-> tau_1 ... tau_n sigma))
520	* (= (<name> x_1 ... x_n) y_1)
521	* ...
522	* (default z))
523	*/
524	extern void pp_function_header(yices_pp_t printer, value_table_t table, value_t c, type_t tau);
525
526	/*
527	* Print the function c
528	* - if show_default is true, also print the default falue
529	*/
530	extern void pp_function(yices_pp_t printer, value_table_t table, value_t c, bool show_default);
531
532	/*
533	* Expand update c and print it as a function
534	* - the name "@fun_c"
535	* - if show_default is true, also print the default value
536	*/
537	extern void normalize_and_pp_update(yices_pp_t printer, value_table_t table, value_t c, bool show_default);
538
539	/*
540	* Print object c on stream f
541	*
542	* There's no support for tuples or mappings in SMT2. They should never occur here.
543	*/
544	extern void pp_object(yices_pp_t printer, value_table_t table, value_t c);
545
546	/*
547	* Print object c on FILE f
548	*
549	*/
550	extern void pp_value(FILE f, value_table_t table, value_t c);
551
552
553
554	/*
555	* OPEN AND CLOSE BLOCK
556	*/
557
558	/*
559	* Start an block given the open-block id
560	*/
561	extern void pp_open_block(yices_pp_t *printer, pp_open_type_t id);
562
563	/*
564	* Close a block
565	* - par: true if a parenthesis is required
566	* false to close and print nothing
567	*/
568	extern void pp_close_block(yices_pp_t *printer, bool par);
569
570
571	#endif /* __YICES_PP_H */

SRI-CSL / yices2 / 12367760548

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous