1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 simple_parser.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2008-06-14.
15
16 Revision History:
17
18 --*/
19 #include "util/warning.h"
20 #include "ast/arith_decl_plugin.h"
21 #include "ast/ast_pp.h"
22 #include "ast/well_sorted.h"
23 #include "ast/cost_evaluator.h"
24 #include "ast/reg_decl_plugins.h"
25 #include "parsers/util/cost_parser.h"
26
27
tst_simple_parser()28 void tst_simple_parser() {
29 ast_manager m;
30 reg_decl_plugins(m);
31 arith_util m_util(m);
32 cost_parser p(m);
33 var_ref_vector vs(m);
34 cost_evaluator eval(m);
35 p.add_var("x");
36 p.add_var("y");
37 expr_ref r(m);
38 p.parse_string("(+ x (* y x))", r);
39 TRACE("simple_parser", tout << mk_pp(r, m) << "\n";);
40 p.parse_string("(+ x (* y x) x)", r);
41 float vals[2] = { 2.0f, 3.0f };
42 (void)vals;
43 TRACE("simple_parser",
44 tout << mk_pp(r, m) << "\n";
45 tout << "val: " << eval(r, 2, vals) << "\n";);
46 p.parse_string("(+ x (* y x) x", r); // << error
47 p.parse_string("(x)", r); // << error
48 p.parse_string("(+ x))", r); // <<< this is accepted
49 TRACE("simple_parser", tout << mk_pp(r, m) << "\n";);
50 p.parse_string(")x)", r); // error
51 p.parse_string("(+ x (* 10 y) 2)", r);
52 TRACE("simple_parser",
53 tout << mk_pp(r, m) << "\n";
54 tout << "val: " << eval(r, 2, vals) << "\n";);
55 p.parse_string("(ite (and (> x 3) (<= y 4)) 2 10)", r);
56 TRACE("simple_parser",
57 tout << mk_pp(r, m) << "\n";
58 tout << "val: " << eval(r, 2, vals) << "\n";);
59 p.parse_string("(ite (or (> x 3) (<= y 4)) 2 10)", r);
60 TRACE("simple_parser",
61 tout << mk_pp(r, m) << "\n";
62 tout << "val: " << eval(r, 2, vals) << "\n";);
63 }
64
65