Parser with Shared Symbol Manager
This example shows how to use the parser via the parser API and use it to parse additional terms in another input source.
examples/api/cpp/parser_sym_manager.cpp
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 * A simple demonstration of using multiple parsers with the same symbol manager
11 * via C++ API.
12 */
13
14#include <cvc5/cvc5.h>
15#include <cvc5/cvc5_parser.h>
16
17#include <iostream>
18
19using namespace cvc5;
20using namespace cvc5::parser;
21
22int main()
23{
24 TermManager tm;
25 Solver slv(tm);
26
27 SymbolManager sm(tm);
28
29 // construct an input parser associated the solver above
30 InputParser parser(&slv, &sm);
31
32 std::stringstream ss;
33 ss << "(set-logic QF_LIA)" << std::endl;
34 ss << "(declare-fun a () Int)" << std::endl;
35 ss << "(declare-fun b () Int)" << std::endl;
36 ss << "(declare-fun c () Bool)" << std::endl;
37 parser.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss, "MyStream");
38
39 // parse commands until finished
40 Command cmd;
41 while (true)
42 {
43 cmd = parser.nextCommand();
44 if (cmd.isNull())
45 {
46 break;
47 }
48 std::cout << "Executing command " << cmd << ":" << std::endl;
49 // invoke the command on the solver and the symbol manager, print the result
50 // to std::cout
51 cmd.invoke(&slv, &sm, std::cout);
52 }
53 std::cout << "Finished parsing commands" << std::endl;
54
55 // Note that sm now has a,b,c in its symbol table.
56
57 // Now, construct a new parser with the same symbol manager. We will parse
58 // terms with it.
59 InputParser parser2(&slv, &sm);
60 std::stringstream ss2;
61 ss2 << "(+ a b)" << std::endl;
62 ss2 << "(- a 10)" << std::endl;
63 ss2 << "(>= 0 45)" << std::endl;
64 ss2 << "(and c c)" << std::endl;
65 ss2 << "true" << std::endl;
66 parser2.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss2, "MyStream2");
67
68 // parse terms until finished
69 Term t;
70 do
71 {
72 t = parser2.nextTerm();
73 std::cout << "Parsed term: " << t << std::endl;
74 } while (!t.isNull());
75 std::cout << "Finished parsing terms" << std::endl;
76}
examples/api/c/parser_sym_manager.c
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 * A simple demonstration of using multiple parsers with the same symbol manager
11 * via the C API.
12 */
13
14#include <assert.h>
15#include <cvc5/c/cvc5.h>
16#include <cvc5/c/cvc5_parser.h>
17#include <stdio.h>
18
19int main()
20{
21 Cvc5TermManager* tm = cvc5_term_manager_new();
22 Cvc5* slv = cvc5_new(tm);
23
24 Cvc5SymbolManager* sm = cvc5_symbol_manager_new(tm);
25
26 // construct an input parser associated the solver above
27 Cvc5InputParser* parser1 = cvc5_parser_new(slv, sm);
28
29 cvc5_parser_set_str_input(
30 parser1,
31 CVC5_INPUT_LANGUAGE_SMT_LIB_2_6,
32 "(set-logic QF_LIA)\n(declare-fun a () Int)\n(declare-fun b () "
33 "Int)\n(declare-fun c () Bool)\n",
34 "foo");
35
36 // parse commands until finished
37 Cvc5Command cmd;
38 do
39 {
40 const char* error_msg;
41 cmd = cvc5_parser_next_command(parser1, &error_msg);
42 if (cmd)
43 {
44 printf("Executing command %s:\n", cvc5_cmd_to_string(cmd));
45 // invoke the command on the solver and the symbol manager, print the
46 // result to stdout
47 printf("%s", cvc5_cmd_invoke(cmd, slv, sm));
48 }
49 } while (cmd);
50 printf("Finished parsing commands\n");
51
52 // Note that sm now has a,b,c in its symbol table.
53
54 // Now, construct a new parser with the same symbol manager. We will parse
55 // terms with it.
56 Cvc5InputParser* parser2 = cvc5_parser_new(slv, sm);
57 cvc5_parser_set_str_input(parser2,
58 CVC5_INPUT_LANGUAGE_SMT_LIB_2_6,
59 "(+ a b)\n(- a 10)\n(>= 0 45)\n(and c c)\ntrue\n",
60 "bar");
61
62 // parse terms until finished
63 Cvc5Term t = NULL;
64 do
65 {
66 const char* error_msg;
67 t = cvc5_parser_next_term(parser2, &error_msg);
68 assert(error_msg == NULL);
69 printf("Parsed term: %s\n", t ? cvc5_term_to_string(t) : "null");
70 } while (t);
71 printf("Finished parsing terms\n");
72
73 cvc5_delete(slv);
74 cvc5_term_manager_delete(tm);
75}
examples/api/java/ParserSymbolManager.java
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 * A simple demonstration of using multiple parsers with the same symbol manager
11 * via Java API.
12 */
13
14import io.github.cvc5.*;
15import io.github.cvc5.modes.*;
16public class ParserSymbolManager
17{
18 public static void main(String args[]) throws CVC5ApiException
19 {
20 TermManager tm = new TermManager();
21 Solver slv = new Solver(tm);
22
23 SymbolManager sm = new SymbolManager(slv);
24
25 // construct an input parser associated the solver above
26 InputParser parser = new InputParser(slv, sm);
27
28 String ss = "";
29 ss += "(set-logic QF_LIA)\n";
30 ss += "(declare-fun a () Int)\n";
31 ss += "(declare-fun b () Int)\n";
32 ss += "(declare-fun c () Bool)\n";
33 parser.setStringInput(InputLanguage.SMT_LIB_2_6, ss, "MyStream");
34
35 // parse commands until finished
36 Command cmd;
37 while (true)
38 {
39 cmd = parser.nextCommand();
40 if (cmd.isNull())
41 {
42 break;
43 }
44 System.out.println("Executing command " + cmd + ":");
45 // invoke the command on the solver and the symbol manager, print the
46 // result to std::cout
47 System.out.print(cmd.invoke(slv, sm));
48 }
49 System.out.println("Finished parsing commands");
50
51 // Note that sm now has a,b,c in its symbol table.
52
53 // Now, construct a new parser with the same symbol manager. We will parse
54 // terms with it.
55 InputParser parser2 = new InputParser(slv, sm);
56 String ss2 = "";
57 ss2 += "(+ a b)\n";
58 ss2 += "(- a 10)\n";
59 ss2 += "(>= 0 45)\n";
60 ss2 += "(and c c)\n";
61 ss2 += "true\n";
62 parser2.setIncrementalStringInput(InputLanguage.SMT_LIB_2_6, "MyStream2");
63 parser2.appendIncrementalStringInput(ss2);
64
65 // parse terms until finished
66 Term t;
67 do
68 {
69 t = parser2.nextTerm();
70 System.out.println("Parsed term: " + t);
71 } while (!t.isNull());
72 System.out.println("Finished parsing terms");
73 }
74}
examples/api/python/parser_sym_manager.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of using multiple parsers with the same symbol manager
12# via Python API
13##
14
15import cvc5
16
17if __name__ == "__main__":
18 tm = cvc5.TermManager()
19 slv = cvc5.Solver(tm)
20
21 sm = cvc5.SymbolManager(tm)
22
23 # construct an input parser associated the solver above
24 parser = cvc5.InputParser(slv, sm)
25
26 input = """
27 (set-logic QF_LIA)
28 (declare-fun a () Int)
29 (declare-fun b () Int)
30 (declare-fun c () Bool)
31 """
32
33 parser.setStringInput(cvc5.InputLanguage.SMT_LIB_2_6, input, "MyInput")
34
35 # parse commands until finished
36 while True:
37 cmd = parser.nextCommand()
38 if cmd.isNull():
39 break
40 print(f"Executing command {cmd}")
41 # invoke the command on the solver and the symbol manager, print the result
42 print(cmd.invoke(slv, sm), end="")
43
44 print("Finished parsing commands")
45
46 # Note that sm now has a,b,c in its symbol table.
47
48 # Now, construct a new parser with the same symbol manager. We will parse
49 #terms with it.
50 parser2 = cvc5.InputParser(slv, sm)
51
52 parser2.setIncrementalStringInput(cvc5.InputLanguage.SMT_LIB_2_6, "MyInput2")
53
54 input2 = """
55 (+ a b)
56 (- a 10)
57 (>= 0 45)
58 (and c c)
59 true
60 """
61 parser2.appendIncrementalStringInput(input2)
62
63 t = parser2.nextTerm()
64 while not t.isNull():
65 print(f"Parsed term: {t}")
66 t = parser2.nextTerm()
67
68 print("Finished parsing terms")