summaryrefslogtreecommitdiff
path: root/examples/api/cpp/utils.h
blob: 69cddee26c77bc4e87a3a1f3b1b2524e69894867 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
/******************************************************************************
 * Top contributors (to current version):
 *   Abdalrhman Mohamed
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * Utility methods.
 */

#ifndef CVC5__UTILS_H
#define CVC5__UTILS_H

#include <cvc5/cvc5.h>

/**
 * Print solutions for synthesis conjecture to the standard output stream.
 * @param terms the terms for which the synthesis solutions were retrieved
 * @param sols the synthesis solutions of the given terms
 */
void printSynthSolutions(const std::vector<cvc5::api::Term>& terms,
                         const std::vector<cvc5::api::Term>& sols);

#endif  // CVC5__UTILS_H
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback