Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * "Ouroborous" test: does cvc5 read its own output?
11 : : *
12 : : * The "Ouroborous" test, named after the serpent that swallows its
13 : : * own tail, ensures that cvc5 can parse some input, output it again
14 : : * (in any of its languages) and then parse it again. The result of
15 : : * the first parse must be equal to the result of the second parse;
16 : : * both strings and expressions are compared for equality.
17 : : *
18 : : * To add a new test, simply add a call to run_test_string() under
19 : : * run_test(), below. If you don't specify an input language,
20 : : * LANG_SMTLIB_V2 is used. If your example depends on symbolic constants,
21 : : * you'll need to declare them in the "declarations" global, just
22 : : * below, in SMT-LIBv2 form (but they're good for all languages).
23 : : */
24 : :
25 : : #include <assert.h>
26 : : #include <cvc5/c/cvc5.h>
27 : : #include <cvc5/c/cvc5_parser.h>
28 : : #include <stdio.h>
29 : : #include <stdlib.h>
30 : : #include <string.h>
31 : :
32 : 12 : char* parse(const char* instr, const char* inlang, const char* outlang)
33 : : {
34 [ - + ]: 12 : assert(strcmp(inlang, "smt2") == 0);
35 [ - + ]: 12 : assert(strcmp(outlang, "smt2") == 0);
36 : :
37 : 12 : const char* declarations =
38 : : "(set-logic ALL)\n"
39 : : "(declare-sort U 0)\n"
40 : : "(declare-fun f (U) U)\n"
41 : : "(declare-fun x () U)\n"
42 : : "(declare-fun y () U)\n"
43 : : "(assert (= (f x) x))\n"
44 : : "(declare-fun a () (Array U (Array U U)))\n";
45 : :
46 : 12 : Cvc5TermManager* tm = cvc5_term_manager_new();
47 : 12 : Cvc5* solver = cvc5_new(tm);
48 : :
49 : 12 : cvc5_set_option(solver, "input-language", inlang);
50 : 12 : cvc5_set_option(solver, "output-language", outlang);
51 : :
52 : 12 : Cvc5SymbolManager* smgr = cvc5_symbol_manager_new(tm);
53 : 12 : Cvc5InputParser* parser = cvc5_parser_new(solver, smgr);
54 : 12 : cvc5_parser_set_str_input(
55 : : parser, CVC5_INPUT_LANGUAGE_SMT_LIB_2_6, declarations, "ouroborous");
56 : :
57 : : // we don't need to execute the commands, but we DO need to parse them to
58 : : // get the declarations
59 : : Cvc5Command cmd;
60 : : do
61 : : {
62 : : const char* error_msg;
63 : 96 : cmd = cvc5_parser_next_command(parser, &error_msg);
64 [ - + ]: 96 : assert(error_msg == NULL);
65 [ + + ]: 96 : if (cmd)
66 : : {
67 : 84 : cvc5_cmd_invoke(cmd, solver, smgr);
68 : : }
69 [ + + ]: 96 : } while (cmd);
70 [ - + ]: 12 : assert(cvc5_parser_done(parser)); // parser should be done
71 : 12 : cvc5_parser_set_str_input(
72 : : parser, CVC5_INPUT_LANGUAGE_SMT_LIB_2_6, instr, "ouroborous");
73 : : const char* error_msg;
74 : 12 : Cvc5Term e = cvc5_parser_next_term(parser, &error_msg);
75 [ - + ]: 12 : assert(!error_msg);
76 : 12 : char* s = strdup(cvc5_term_to_string(e));
77 [ - + ]: 12 : assert(!cvc5_parser_next_term(parser, &error_msg));
78 [ - + ]: 12 : assert(!error_msg);
79 : 12 : cvc5_parser_delete(parser);
80 : 12 : cvc5_symbol_manager_delete(smgr);
81 : 12 : cvc5_delete(solver);
82 : 12 : cvc5_term_manager_delete(tm);
83 : 12 : return s;
84 : : }
85 : :
86 : 6 : char* translate(const char* str, const char* inlang, const char* outlang)
87 : : {
88 [ - + ]: 6 : assert(strcmp(inlang, "smt2") == 0);
89 [ - + ]: 6 : assert(strcmp(outlang, "smt2") == 0);
90 : :
91 : 6 : printf("==============================================\n");
92 : 6 : printf("translating from %s to %s this string:\n%s\n", inlang, outlang, str);
93 : 6 : char* outstr = parse(str, inlang, outlang);
94 : 6 : printf("got this:\n%s\n", outstr);
95 : 6 : printf("reparsing as %s\n", outlang);
96 : 6 : char* poutstr = parse(outstr, outlang, outlang);
97 [ - + ]: 6 : assert(strcmp(outstr, poutstr) == 0);
98 : 6 : printf("got same expressions %s and %s\n", outstr, poutstr);
99 : 6 : printf("==============================================\n");
100 : 6 : free(poutstr);
101 : 6 : return outstr;
102 : : }
103 : :
104 : 3 : void run_test_string(const char* str, const char* lang)
105 : : {
106 : 3 : printf("\n");
107 : 3 : printf("starting with: %s\n", str);
108 : 3 : printf(" in language %s\n", lang);
109 : 3 : char* smt2str = translate(str, lang, "smt2");
110 : 3 : printf("in SMT2 : %s\n", smt2str);
111 : 3 : char* outstr = translate(smt2str, "smt2", "smt2");
112 : 3 : printf("to SMT2 : %s\n\n", outstr);
113 : :
114 [ - + ]: 3 : assert(strcmp(outstr, smt2str) == 0); // differences in output
115 : 3 : free(smt2str);
116 : 3 : free(outstr);
117 : 3 : }
118 : :
119 : 1 : int main()
120 : : {
121 : 1 : run_test_string("(= (f (f y)) x)", "smt2");
122 : 1 : run_test_string("(= ((_ extract 2 1) (bvnot (bvadd #b000 #b011))) #b10)",
123 : : "smt2");
124 : 1 : run_test_string("((_ extract 2 0) (bvnot (bvadd (bvmul #b001 #b011) #b011)))",
125 : : "smt2");
126 : 1 : return 0;
127 : : }
|
