Gluttonous-Snake2/lab2.cpp at master · Bessss-zyw/Gluttonous-Snake2 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
#include "common.h"

using namespace z3;

bool func1(int data[4][5], int answer[4])
{
    int i = 0;

    context con;

    expr a = con.int_const("a");
    expr b = con.int_const("b");
    expr c = con.int_const("c");
    expr d = con.int_const("d");

    solver s(con);

    //TODO : your solution here
    //assert(0);
    for(i = 0;i < 4;++i)
        s.add(a*data[i][0]+b*data[i][1]+c*data[i][2]+d*data[i][3] == data[i][4]);

    if(sat == s.check())
    {
        model m = s.get_model();
        answer[0] = m.eval(a).get_numeral_int();
        answer[1] = m.eval(b).get_numeral_int();
        answer[2] = m.eval(c).get_numeral_int();
        answer[3] = m.eval(d).get_numeral_int();

        return true;
    }

    return false;
}

int func2(int data[][2], unsigned n)
{
    unsigned i = 0;

    context ctx;

    expr a = ctx.int_const("a");
    solver s(ctx);

    //TODO : your solution here
    //assert(0);

    for(i = 0;i < n;++i){
        s.add(a%data[i][0] == data[i][1]);
        s.add(a != data[i][1]);
    }

    s.add(a < 1000000);

    if(sat == s.check())
    {
        model m = s.get_model();
        return m.eval(a).get_numeral_int();
    }

    return -1;
}

bool func3(int node_num, int color, int graph[20][20])
{
    int i=0, j=0,k = 0;

    context c;
    expr_vector x(c); // x is a vector of expr.

    for ( i = 0; i < node_num; ++i)
        for ( j = 0; j < node_num; ++j)
        {
            std::stringstream x_name;
            x_name << "x_" << i << '_' << j;// every uninterpreted consts need a unique name
            x.push_back(c.int_const(x_name.str().c_str()));// add a new integer consts
        }
    //x[i * node_num + j] denotes the color of edge between node i and node j

    solver s(c);

    //TODO : your solution here
    //assert(0);
    for(i = 0;i < node_num;++i)
        for(j = 0;j < node_num;++j)
        {
            if(j <= i)
                s.add(x[i * node_num + j] == 0);
            else{
                s.add(x[i * node_num + j] > 0);
                s.add(x[i * node_num + j] <= color);

                for(k = j+1;k < node_num;++k)
                {
                    s.add(!((x[i * node_num + j] == x[i * node_num + k])&&(x[i * node_num + j] == x[j * node_num + k])));
                }
            }
        }

    if( unsat == s.check() )
        return false;

    model m = s.get_model();

    for(i=0; i<node_num; ++i)
    {
        for( j=i+1; j<node_num; ++j)
        {
            //x[i * node_num + j] denotes the color of edge between node i and node j
            graph[i][j] = m.eval( x[i * node_num + j] ).get_numeral_int();
        }
    }
    return true;
}