mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

add example of parsing with external declarations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-07 12:57:07 -07:00
parent 37f7c30e23
commit 5d9820f3e2
2 changed files with 27 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
examples/c++/example.cpp
View file

@ -1129,6 +1129,17 @@ void consequence_example() {
std::cout << consequences << "\n";
}
static void parse_example() {
std::cout << "parse example\n";
context c;
sort_vector sorts(c);
func_decl_vector decls(c);
sort B = c.bool_sort();
decls.push_back(c.function("a", 0, 0, B));
expr a = c.parse_string("(assert a)", sorts, decls);
std::cout << a << "\n";
}
int main() {
try {
@ -1173,6 +1184,7 @@ int main() {
param_descrs_example(); std::cout << "\n";
sudoku_example(); std::cout << "\n";
consequence_example(); std::cout << "\n";
parse_example(); std::cout << "\n";
std::cout << "done\n";
}
catch (exception & ex) {

17
src/api/c++/z3++.h
View file

@ -2460,7 +2460,6 @@ namespace z3 {
return expr(re.ctx(), r);
}
inline expr interpolant(expr const& a) {
return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
}
@ -2493,7 +2492,21 @@ namespace z3 {
return expr(*this, r);
}
// inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
array<Z3_symbol> sort_names(sorts.size());
array<Z3_symbol> decl_names(decls.size());
array<Z3_sort> sorts1(sorts);
array<Z3_func_decl> decls1(decls);
for (unsigned i = 0; i < sorts.size(); ++i) {
sort_names[i] = sorts[i].name();
}
for (unsigned i = 0; i < decls.size(); ++i) {
decl_names[i] = decls[i].name();
}
Z3_ast r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
check_error();
return expr(*this, r);
}
inline check_result context::compute_interpolant(expr const& pat, params const& p, expr_vector& i, model& m) {