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)13static 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()32void 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