mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

add example from #2138

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-16 10:30:44 -08:00
parent 7f51cc7931
commit 886c62ef41
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1166,6 +1166,14 @@ static void parse_example() {
// expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))"); // expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))");
} }
static void parse_string() {
std::cout << "parse string\n";
z3::context c;
z3::solver s(c);
s.from_string("(declare-const x Int)(assert (> x 10))");
std::cout << s.check() << "\n";
}
void mk_model_example() { void mk_model_example() {
context c; context c;
@ -1252,6 +1260,7 @@ int main() {
sudoku_example(); std::cout << "\n"; sudoku_example(); std::cout << "\n";
consequence_example(); std::cout << "\n"; consequence_example(); std::cout << "\n";
parse_example(); std::cout << "\n"; parse_example(); std::cout << "\n";
parse_string(); std::cout << "\n";
mk_model_example(); std::cout << "\n"; mk_model_example(); std::cout << "\n";
recfun_example(); std::cout << "\n"; recfun_example(); std::cout << "\n";
std::cout << "done\n"; std::cout << "done\n";