1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "ast/rewriter/factor_rewriter.h"
8 #include "ast/bv_decl_plugin.h"
9 #include "ast/ast_pp.h"
10 #include "ast/reg_decl_plugins.h"
11
tst_factor_rewriter()12 void tst_factor_rewriter() {
13 ast_manager m;
14 reg_decl_plugins(m);
15
16 factor_rewriter_star fw(m);
17 arith_util a(m);
18 expr_ref fml1(m), fml2(m);
19 expr_ref z(m.mk_const(symbol("z"), a.mk_real()), m);
20 expr_ref two(a.mk_numeral(rational(2),false),m);
21 expr_ref zero(a.mk_numeral(rational(0),false),m);
22 fml1 = a.mk_le(zero, a.mk_mul(two, z, z));
23 fw(fml1, fml2);
24 std::cout << mk_pp(fml1, m) << " -> " << mk_pp(fml2, m) << "\n";
25 }
26