Z3에서 사용자 정의 단순화 전술을 구현하는 방법은 무엇입니까?

Question

제 도구에서 상수를 정수 변수와 비교하는 조건을 사용합니다 (예 : y < 100). 종종 하나의 변수에 대해 여러 조건이 있으며 이러한 경우를 단순화하고자합니다. 예를 들면 다음과 같습니다. y & y! = 99는 y <이되어야합니다. 단순화 전술은이 작업을 수행하지 않으며 도움이되는 것처럼 소리를 단순화하기위한 인수도 없습니다. 코드에서

: 최종 수익률

context c; 
goal g(c); 
expr x = c.int_const("x"); 
expr y = c.int_const("y"); 
solver s(c); 
expr F = y < 100 && y != 99; 
g.add(F); 
tactic t = tactic(c, "simplify"); 
apply_result r = t(g); 
for (unsigned i = 0; i < r.size(); i++) { 
    std::cout << "subgoal " << i << "\n" << r[i] << "\n"; 
} 

출력 : 내가 원하는대로 유사한 subgoal 0 (goal (not (<= 100 y)) (not (= y 99)))

하지 subgoal 0(goal(not(<= 99 y)) 또는 뭔가.

따라서 저는 단순화 전술을 구현하고 싶습니다. 불행히도 나는 이것을하는 방법을 찾을 수 없습니다. 전술이 C++로 구현되어야한다는 것을 알고 있지만 Z3에 내 ​​전술을 어떻게 소개 할 수 있습니까?

Answer 1

Z3 전술은 src/tactic 디렉토리에 저장됩니다. 산술 관련 전술은 서브 디렉토리 arith에 있습니다. 전술을 구현하기위한 "템플릿"으로 기존 전술을 사용해야합니다. 좋은 예는 https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/normalize_bounds_tactic.cpp

는 API 및 SMT 2.0 프런트 엔드의 새로운 전술을 사용할 수 있도록하기 위해, 우리는 ADD_TACTIC 명령이 포함 된 주석을 포함해야합니다. 이 명령은 Z3 mk_make 스크립트에 모든 것을 연결하도록 지시합니다. 인수는 전술 이름, 설명 및 전술을 작성하기위한 C++ 코드입니다. https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/propagate_ineqs_tactic.cpp

:

/* 
    ADD_TACTIC("normalize-bounds", 
      "replace a variable x with lower bound k <= x with x' = x - k.", 
      "mk_normalize_bounds_tactic(m, p)") 
*/ 

BTW, 당신은 또한 같은 기존의 전술을 확장하여 새로운 기능을 구현하려고 할 수 있습니다