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
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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 Solver slv;
28
29 SymbolManager sm(&slv);
30
31 // construct an input parser associated the solver above
32 InputParser parser(&slv, &sm);
33
34 std::stringstream ss;
35 ss << "(set-logic QF_LIA)" << std::endl;
36 ss << "(declare-fun a () Int)" << std::endl;
37 ss << "(declare-fun b () Int)" << std::endl;
38 ss << "(declare-fun c () Bool)" << std::endl;
39 parser.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss, "MyStream");
40
41 // parse commands until finished
42 Command cmd;
43 while (true)
44 {
45 cmd = parser.nextCommand();
46 if (cmd.isNull())
47 {
48 break;
49 }
50 std::cout << "Executing command " << cmd << ":" << std::endl;
51 // invoke the command on the solver and the symbol manager, print the result
52 // to std::cout
53 cmd.invoke(&slv, &sm, std::cout);
54 }
55 std::cout << "Finished parsing commands" << std::endl;
56
57 // Note that sm now has a,b,c in its symbol table.
58
59 // Now, construct a new parser with the same symbol manager. We will parse
60 // terms with it.
61 InputParser parser2(&slv, &sm);
62 std::stringstream ss2;
63 ss2 << "(+ a b)" << std::endl;
64 ss2 << "(- a 10)" << std::endl;
65 ss2 << "(>= 0 45)" << std::endl;
66 ss2 << "(and c c)" << std::endl;
67 ss2 << "true" << std::endl;
68 parser2.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss2, "MyStream2");
69
70 // parse terms until finished
71 Term t;
72 do
73 {
74 t = parser2.nextTerm();
75 std::cout << "Parsed term: " << t << std::endl;
76 } while (!t.isNull());
77 std::cout << "Finished parsing terms" << std::endl;
78}
examples/api/java/ParserSymbolManager.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2023 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 slv = cvc5.Solver()
22
23 sm = cvc5.SymbolManager(slv)
24
25 # construct an input parser associated the solver above
26 parser = cvc5.InputParser(slv, sm)
27
28 input = """
29 (set-logic QF_LIA)
30 (declare-fun a () Int)
31 (declare-fun b () Int)
32 (declare-fun c () Bool)
33 """
34
35 parser.setStringInput(cvc5.InputLanguage.SMT_LIB_2_6, input, "MyInput")
36
37 # parse commands until finished
38 while True:
39 cmd = parser.nextCommand()
40 if cmd.isNull():
41 break
42 print(f"Executing command {cmd}")
43 # invoke the command on the solver and the symbol manager, print the result
44 print(cmd.invoke(slv, sm), end="")
45
46 print("Finished parsing commands")
47
48 # Note that sm now has a,b,c in its symbol table.
49
50 # Now, construct a new parser with the same symbol manager. We will parse
51 #terms with it.
52 parser2 = cvc5.InputParser(slv, sm)
53
54 parser2.setIncrementalStringInput(cvc5.InputLanguage.SMT_LIB_2_6, "MyInput2")
55
56 input2 = """
57 (+ a b)
58 (- a 10)
59 (>= 0 45)
60 (and c c)
61 true
62 """
63 parser2.appendIncrementalStringInput(input2)
64
65 t = parser2.nextTerm()
66 while not t.isNull():
67 print(f"Parsed term: {t}")
68 t = parser2.nextTerm()
69
70 print("Finished parsing terms")