Как получить все модели или все выпуклые оценки? - PullRequest
Новая
       9

Как получить все модели или все выпуклые оценки?

1 голос
/ 11 мая 2019

Я новичок в Z3-Solver с API на C ++ и хочу решить группу неравенств и найти результаты.

Я прочитал ответ, который написан на Python и пытаюсь написать его на C ++, но повторяет печать одной модели. 

5 <= x + y + z <= 16
AND -4 <= x - y <= 6
AND 1 <= y - z <= 3
AND -1 <= x - z <= 7
AND x >= 0 AND y >= 0 AND z >= 0

Были добавлены неравенствав решатель, и есть много оценок.

c - это контекст, а s - это решатель. 

    vector<const char*> variables {"x", "y", "z"};

    // ...

    // till here, s was added into several constraints
    while(s.check() == sat){
        model m = s.get_model();
        cout << m << "\n######\n";
        expr tmp = c.bool_val(false);
        for(int i = 0; i < variables.size(); ++ i){
            tmp = tmp || (m[c.int_const(variables[i])] != c.int_const(variables[i]));
        }
        s.add(tmp);
    }

И результат: 

(define-fun z () Int
  0)
(define-fun y () Int
  2)
(define-fun x () Int
  3)
######
(define-fun z () Int
  0)
(define-fun y () Int
  2)
(define-fun x () Int
  3)
######
(define-fun z () Int
  0)
...

И он просто печатает одну модель.Я не уверен, где не так.

Как я могу получить все модели или получить один или несколько выпуклых множеств (таких как {l1 <= x <= u1 и l2 <= x - y <= u2 и ...}), но неПройдите все оценки. </p>

Кстати, на Python есть много обучающих программ (таких как this ), где я могу выучить z3 на c ++ как пример и API Doc. не легко начать.

1 Ответ

0 голосов
/ 12 мая 2019

Ваш цикл "опровержения модели" не совсем корректен. Поскольку вы не опубликовали весь свой код, трудно сказать, могут ли быть другие проблемы, но я бы так решил: 

#include<vector>
#include"z3++.h"

using namespace std;
using namespace z3;

int main(void) {
    context c;

    expr_vector variables(c);
    variables.push_back(c.int_const("x"));
    variables.push_back(c.int_const("y"));
    variables.push_back(c.int_const("z"));
    expr x = variables[0];
    expr y = variables[1];
    expr z = variables[2];

    solver s(c);

    s.add(5 <= x+y+z);
    s.add(x+y+z <= 16);
    s.add(-4 <= x-y);
    s.add(x-y <= 6);
    s.add(-1 <= x-z);
    s.add(x-z <= 7);
    s.add(x >= 0);
    s.add(y >= 0);
    s.add(z >= 0);

    while (s.check() == sat) {
        model m = s.get_model();
        cout << m << endl;
        cout << "#######" << endl;
        expr tmp = c.bool_val(false);
        for(int i = 0; i < variables.size(); ++i) {
            tmp = tmp || (variables[i] != m.eval(variables[i]));
        }
        s.add(tmp);
    }

    return 0;
}

Этот код запускает и перечисляет все "конкретные" модели. Исходя из вашего вопроса, я полагаю, вы также задаетесь вопросом, можете ли вы получить «символические» модели: это невозможно с решателем SMT. Решатели SMT производят только конкретные (т.е. все наземные) модели, поэтому, если вам нужно обобщить их, вам придется делать это за пределами границы z3.

...