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