макрос определения веселья и регулярное выражение в привязке Z3 C ++ - PullRequest
Новая
       5

макрос определения веселья и регулярное выражение в привязке Z3 C ++

1 голос
/ 13 февраля 2020

Я пишу некоторый код, который использует строки Z3 для оценки разрешений в ACL. Пока что с SMT2 это было относительно просто. Например, код того, что я пытаюсь получить: 

(declare-const Group String)
(declare-const Resource String)

(define-fun acl1() Bool
  (or (and
       (= Group "employee")
       (str.prefixof "shared/News_" Resource))
      (and
       (= Group "manager")
       (or (str.prefixof "shared/Internal_" Resource)
           (str.prefixof "shared/News_" Resource))
       )))

(define-fun acl2() Bool
  (and (and (str.prefixof "shared/" Resource)
            (str.in.re Group re.allchar))
       (not (and (str.prefixof "shared/Internal_" Resource)
                 (= Group "employee")))))

;; perm(acl1) <= perm(acl) iff acl1 => acl2
(define-fun conjecture() Bool
  (=> (= acl1 true)
      (= acl2 true)))

(assert (not conjecture))
(check-sat)

Читая привязки z3 c ++, я пока не могу понять, как привязать функцию z3 :: к этому. До сих пор, предполагая, что define-fun - это просто макрос lisp, у меня есть это. 

#include <z3++.h>

z3::expr acl1(z3::context& c, z3::expr& G, z3::expr& R)
{
  return (((G == c.string_val("employee")) &&
           z3::prefixof(c.string_val("shared/News_"), R)) ||
          ((G == c.string_val("manager")) &&
           (z3::prefixof(c.string_val("shared/Internal_"), R) ||
            z3::prefixof(c.string_val("shared/News_"), R))));
}

z3::expr acl2(z3::context& c, z3::expr& G, z3::expr& R)
{
  return ((z3::prefixof(c.string_val(""), G) &&
           z3::prefixof(c.string_val("shared/"), R)) &&
          !((G == c.string_val("employee")) &&
            (z3::prefixof(c.string_val("shared/Internal"), R))));
}

z3::expr MakeStringFunction(z3::context* c, std::string s) {
  z3::sort sort = c->string_sort();
  z3::symbol name = c->str_symbol(s.c_str());
  return c->constant(name, sort);
}

void acl_eval()
{
  z3::context c;
  auto Group = MakeStringFunction(&c, "Group");
  auto Resource = MakeStringFunction(&c, "Resource");
  auto acl1_f = acl1(c, Group, Resource);
  auto acl2_f = acl2(c, Group, Resource);
  auto conjecture = implies(acl1_f == c.bool_val(true),
                            acl2_f == c.bool_val(true));

  z3::solver s(c);
  s.add(!conjecture);
  std::cout << s.to_smt2() << std::endl;
  switch(s.check()){
  case z3::unsat: std::cout<< "Valid Conjecture" << std::endl; break;
  case z3::sat: std::cout << "Invalid Conjecture" << std::endl; break;
  case z3::unknown: [[fallthrough]]
  default:
    std::cout << "Unknown" << std::endl;
  }
}

int main(){
  acl_eval();
  return 0;
}

Это так, как это должно быть сделано с функциями в привязках C ++? в то время как код smt2, сгенерированный привязками C ++, не совсем похож на другой, я вижу в выражении целый expr с привязками let, что делает то, что я хочу. Кроме того, я также хочу знать, поддерживают ли привязки C ++ функции регулярных выражений, такие как SMT lib из z3? Я не могу найти никаких примеров, и документы не очень ясны.

1 Ответ

1 голос
/ 14 февраля 2020

Как правило, вам не нужно создавать «функции» в SMTLib, когда вы используете C ++ (или любой другой высокоуровневый) API. Вместо этого вы просто пишете функции на тех языках, которые генерируют необходимый код напрямую. Сначала это звучит странно, но это предполагаемый вариант использования: функции SMTLib заменяются функциями на языке хоста. Запуск их на главном языке приводит к созданию необходимых синтаксических деревьев на объектном языке; то есть, внутреннее представление AST Z3. Особенно в вашем случае вам не нужны никакие «аргументы», передаваемые этим функциям, поэтому вам вообще не нужно их создавать. Итак, то, что вы здесь сделали, правильно.

(Примечание: может быть сценарий ios, в котором вы действительно хотите выплевывать функции в SMTLib. Например, если вы хотите использовать неинтерпретированные функции. Или, возможно, вы Я хочу использовать определения рекурсивных функций, которые вы на самом деле не можете сделать на языке хоста. Но давайте не будем связывать вопросы здесь. Если вы чувствуете, что они действительно нужны, пожалуйста, задайте отдельный вопрос об этом. Из вашего описания я вижу нет причин для них.)

Относительно выражений регулярных выражений: все они доступны в C ++ API, посмотрите здесь: https://z3prover.github.io/api/html/z3_09_09_8h_source.html#l03334

В частности следующие функции:

  • in_re : для проверки членства
  • re_full : регулярное выражение, принимающее все строки ( Несколько сбивает с толку, SMTLibs allchar в C ++ API называется re_full.)

Надеюсь, это поможет вам начать!

...