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}