1 /*++
2 Copyright (c) 2015 Microsoft Corporation
3
4 --*/
5
6 #include "ast/rewriter/arith_rewriter.h"
7 #include "ast/bv_decl_plugin.h"
8 #include "ast/ast_pp.h"
9 #include "ast/reg_decl_plugins.h"
10 #include "ast/rewriter/th_rewriter.h"
11 #include "model/model.h"
12 #include "parsers/smt2/smt2parser.h"
13
14
parse_fml(ast_manager & m,char const * str)15 static expr_ref parse_fml(ast_manager& m, char const* str) {
16 expr_ref result(m);
17 cmd_context ctx(false, &m);
18 ctx.set_ignore_check(true);
19 std::ostringstream buffer;
20 buffer << "(declare-const x Real)\n"
21 << "(declare-const y Real)\n"
22 << "(declare-const z Real)\n"
23 << "(declare-const a Real)\n"
24 << "(declare-const b Real)\n"
25 << "(assert " << str << ")\n";
26 std::istringstream is(buffer.str());
27 VERIFY(parse_smt2_commands(ctx, is));
28 ENSURE(!ctx.assertions().empty());
29 result = ctx.assertions().get(0);
30 return result;
31 }
32
33 static char const* example1 = "(<= (+ (* 1.3 x y) (* 2.3 y y) (* (- 1.1 x x))) 2.2)";
34 static char const* example2 = "(= (+ 4 3 (- (* 3 x x) (* 5 y)) y) 0)";
35
36
tst_arith_rewriter()37 void tst_arith_rewriter() {
38 ast_manager m;
39 reg_decl_plugins(m);
40 arith_rewriter ar(m);
41 arith_util au(m);
42 expr_ref t1(m), t2(m), result(m);
43 t1 = au.mk_numeral(rational(0),false);
44 t2 = au.mk_numeral(rational(-3),false);
45 expr* args[2] = { t1, t2 };
46 ar.mk_mul(2, args, result);
47 std::cout << mk_pp(result, m) << "\n";
48
49
50 th_rewriter rw(m);
51 expr_ref fml = parse_fml(m, example1);
52 rw(fml);
53 std::cout << mk_pp(fml, m) << "\n";
54
55
56 fml = parse_fml(m, example2);
57 rw(fml);
58 std::cout << mk_pp(fml, m) << "\n";
59 }
60