mirror of
https://github.com/Z3Prover/z3
synced 2025-08-05 19:00:25 +00:00
8e772b428b
Using a base exception class, derived from z3_exception, makes it possible to recover gracefully if something goes wrong during the computation of interpolants.
36 lines
558 B
C++
36 lines
558 B
C++
/*++
|
|
Copyright (c) 2013 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
iz3pp.cpp
|
|
|
|
Abstract:
|
|
|
|
Pretty-print interpolation problems
|
|
|
|
Author:
|
|
|
|
Ken McMillan (kenmcmil)
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
|
|
#ifndef IZ3_PP_H
|
|
#define IZ3_PP_H
|
|
|
|
#include "iz3mgr.h"
|
|
|
|
/** Exception thrown in case of mal-formed tree interpoloation
|
|
specification */
|
|
|
|
struct iz3pp_bad_tree: public iz3_exception {
|
|
iz3pp_bad_tree(): iz3_exception("iz3pp_bad_tree") {}
|
|
};
|
|
|
|
void iz3pp(ast_manager &m,
|
|
const ptr_vector<expr> &cnsts_vec,
|
|
expr *tree,
|
|
std::ostream& out);
|
|
#endif
|