1 
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4 
5 --*/
6 
7 #include "smt/arith_eq_solver.h"
8 #include "smt/params/smt_params.h"
9 
10 typedef rational numeral;
11 typedef vector<numeral> row;
12 
test_solve_integer_equations(arith_eq_solver & asimp,vector<row> & rows)13 static void test_solve_integer_equations(
14     arith_eq_solver& asimp,
15     vector<row>& rows
16     )
17 {
18     row r_unsat;
19 
20     if (asimp.solve_integer_equations(rows, r_unsat)) {
21         std::cout << "solved\n";
22     }
23     else {
24         std::cout << "not solved\n";
25         for (unsigned i = 0; i < r_unsat.size(); ++i) {
26             std::cout << " " << r_unsat[i];
27         }
28         std::cout << "\n";
29     }
30 }
31 
tst_arith_simplifier_plugin()32 void tst_arith_simplifier_plugin() {
33     smt_params params;
34     ast_manager m;
35     arith_eq_solver asimp(m);
36 
37     row r1;
38     row r2;
39 
40     r1.push_back(numeral(1));
41     r1.push_back(numeral(2));
42     r1.push_back(numeral(1));
43     r1.push_back(numeral(2));
44 
45     r2.push_back(numeral(1));
46     r2.push_back(numeral(2));
47     r2.push_back(numeral(1));
48     r2.push_back(numeral(2));
49 
50     vector<row> rows;
51     rows.push_back(r1);
52     rows.push_back(r2);
53 
54 #if 0
55     test_solve_integer_equations(asimp, rows);
56 
57     rows[1][3] = numeral(3);
58     test_solve_integer_equations(asimp, rows);
59 #endif
60 
61     rows[0][0] = numeral(1);
62     rows[0][1] = numeral(3);
63     rows[0][2] = numeral(0);
64     rows[0][3] = numeral(0);
65 
66     rows[1][0] = numeral(1);
67     rows[1][1] = numeral(0);
68     rows[1][2] = numeral(3);
69     rows[1][3] = numeral(1);
70 
71     test_solve_integer_equations(asimp, rows);
72 
73 }
74