Parser

This example shows how to use the parser via the parser API.

/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * A simple demonstration of using the parser via C++ API.
 */

#include <cvc5/cvc5.h>
#include <cvc5/cvc5_parser.h>

#include <iostream>

using namespace cvc5;
using namespace cvc5::parser;

int main()
{
  TermManager tm;
  Solver slv(tm);

  // set that we should print success after each successful command
  slv.setOption("print-success", "true");

  // construct an input parser associated the solver above
  InputParser parser(&slv);

  std::stringstream ss;
  ss << "(set-logic QF_LIA)" << std::endl;
  ss << "(declare-fun a () Int)" << std::endl;
  ss << "(declare-fun b () Int)" << std::endl;
  ss << "(declare-fun c () Int)" << std::endl;
  ss << "(assert (> a (+ b c)))" << std::endl;
  ss << "(assert (< a b))" << std::endl;
  ss << "(assert (> c 0))" << std::endl;
  parser.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss, "MyStream");

  // get the symbol manager of the parser, used when invoking commands below
  SymbolManager* sm = parser.getSymbolManager();

  // parse commands until finished
  Command cmd;
  while (true)
  {
    cmd = parser.nextCommand();
    if (cmd.isNull())
    {
      break;
    }
    std::cout << "Executing command " << cmd << ":" << std::endl;
    // invoke the command on the solver and the symbol manager, print the result
    // to std::cout
    cmd.invoke(&slv, sm, std::cout);
  }
  std::cout << "Finished parsing commands" << std::endl;

  // now, check sat with the solver
  Result r = slv.checkSat();
  std::cout << "expected: unsat" << std::endl;
  std::cout << "result: " << r << std::endl;
}

examples/api/c/parser.c

/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * A simple demonstration of using the parser via the C API.
 */

#include <assert.h>
#include <cvc5/c/cvc5.h>
#include <cvc5/c/cvc5_parser.h>
#include <stdio.h>

int main()
{
  Cvc5TermManager* tm = cvc5_term_manager_new();
  Cvc5* slv = cvc5_new(tm);

  // set that we should print success after each successful command
  cvc5_set_option(slv, "print-success", "true");

  // construct an input parser associated the solver above
  Cvc5InputParser* parser = cvc5_parser_new(slv, NULL);
  cvc5_parser_set_str_input(
      parser,
      CVC5_INPUT_LANGUAGE_SMT_LIB_2_6,
      "(set-logic QF_LIA)\n(declare-fun a () Int)\n(declare-fun b () "
      "Int)\n(declare-fun c () Int)\n(assert (> a (+ b c)))\n(assert (< a "
      "b))\n(assert (> c 0))\n",
      "foo");

  // get the symbol manager of the parser, used when invoking commands below
  Cvc5SymbolManager* sm = cvc5_parser_get_sm(parser);

  // parse commands until finished
  Cvc5Command cmd;
  do
  {
    const char* error_msg;
    cmd = cvc5_parser_next_command(parser, &error_msg);
    assert(error_msg == NULL);
    if (cmd)
    {
      printf("Executing command %s:\n", cvc5_cmd_to_string(cmd));
      // invoke the command on the solver and the symbol manager, print the
      // result to stdout
      printf("%s", cvc5_cmd_invoke(cmd, slv, sm));
    }
  } while (cmd);
  printf("Finished parsing commands\n");

  // now, check sat with the solver
  Cvc5Result r = cvc5_check_sat(slv);
  printf("expected: unsat\n");
  printf("result: %s\n", cvc5_result_to_string(r));
  cvc5_delete(slv);
  cvc5_term_manager_delete(tm);
}

examples/api/java/Parser.java

/******************************************************************************
 * Top contributors (to current version):
 *   Mudathir Mohamed, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * A simple demonstration of using the parser via Java API.
 */

import io.github.cvc5.*;
import io.github.cvc5.modes.*;
public class Parser
{
  public static void main(String args[]) throws CVC5ApiException
  {
    TermManager tm = new TermManager();
    Solver slv = new Solver(tm);

    // set that we should print success after each successful command
    slv.setOption("print-success", "true");

    // construct an input parser associated the solver above
    InputParser parser = new InputParser(slv);

    String ss = "";
    ss += "(set-logic QF_LIA)\n";
    ss += "(declare-fun a () Int)\n";
    ss += "(declare-fun b () Int)\n";
    ss += "(declare-fun c () Int)\n";
    ss += "(assert (> a (+ b c)))\n";
    ss += "(assert (< a b))\n";
    ss += "(assert (> c 0))\n";
    parser.setStringInput(InputLanguage.SMT_LIB_2_6, ss, "MyStream");

    // get the symbol manager of the parser, used when invoking commands below
    SymbolManager sm = parser.getSymbolManager();

    // parse commands until finished
    Command cmd;
    while (true)
    {
      cmd = parser.nextCommand();
      if (cmd.isNull())
      {
        break;
      }
      System.out.println("Executing command " + cmd + ":");
      // invoke the command on the solver and the symbol manager, print the result
      // to standard output
      System.out.println(cmd.invoke(slv, sm));
    }
    System.out.println("Finished parsing commands");

    // now, check sat with the solver
    Result r = slv.checkSat();
    System.out.println("expected: unsat");
    System.out.println("result: " + r);
  }
}

examples/api/python/parser.py

#!/usr/bin/env python
###############################################################################
# Top contributors (to current version):
#   Daniel Larraz, Andrew Reynolds
#
# This file is part of the cvc5 project.
#
# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
# in the top-level source directory and their institutional affiliations.
# All rights reserved.  See the file COPYING in the top-level source
# directory for licensing information.
# #############################################################################
#
# A simple demonstration of using the parser via Python API
##

import cvc5

if __name__ == "__main__":
    tm = cvc5.TermManager()
    slv = cvc5.Solver()

    # set that we should print success after each successful command
    slv.setOption("print-success", "true")

    # construct an input parser associated the solver above
    parser = cvc5.InputParser(slv)

    input = """
        (set-logic QF_LIA)
        (declare-fun a () Int)
        (declare-fun b () Int)
        (declare-fun c () Int)
        (assert (> a (+ b c)))
        (assert (< a b))
        (assert (> c 0))
    """

    parser.setStringInput(cvc5.InputLanguage.SMT_LIB_2_6, input, "MyInput")

    # get the symbol manager of the parser, used when invoking commands below
    sm = parser.getSymbolManager()

    # parse commands until finished
    while True:
        cmd = parser.nextCommand()
        if cmd.isNull():
            break
        print(f"Executing command {cmd}:")
        # invoke the command on the solver and the symbol manager, print the result
        print(cmd.invoke(slv, sm), end="")

    print("Finished parsing commands")

    # now, check sat with the solver
    r = slv.checkSat()
    print("expected: unsat")
    print(f"result: {r}")

examples/api/smtlib/parser.smt2

(set-logic QF_LIA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (> a (+ b c)))
(assert (< a b))
(assert (> c 0))
(check-sat)