smt

1열

1답변

QF_NRA에 0으로 나누기가 포함되어 있습니까? SMT-LIB 표준은이 점에서 혼란 스럽습니다. paper where the standard is defined은이 점에 관해서는 간단히 언급하지 않고 있습니다. 실제로 NRA와 QF_NRA는 해당 문서의 어느 곳에도 나타나지 않습니다. 일부 정보는 standard website에 제공됩니다. 실제 값은 다

1열

1답변

SMT-LIB의 QF_NRA 로직이 결정 가능합니까?

SMT-LIB의 QF_NRA 로직이 결정 가능합니까? 나는 타르 스키가 실수로 다항식의 시스템을 결정할 수 있다는 비선형 산수를 결정할 수 있다는 것을 증명했습니다. 그러나 QF_NRA에는 부서가 포함되어 있기 때문에 QF_NRA가이 우산 아래 있다는 것은 명백하지 않습니다. 따라서 첫 번째 질문은 QF_NRA의 분할이 분모가 잠재적으로 0 인 변수에 의한

1열

1답변

출력을 16 진수 형식으로 출력하는 방법

이 Boolector 프로그램 인쇄 출력을 2 진 형식으로 출력합니다. 하지만 16 진수 형식이 필요합니다. boolector에서 16 진수 형식을 인쇄하는 방법. (set-logic QF_BV) (set-info :smt-lib-version 2.0) (declare-const val1 (_ BitVec 16)) (declare-const val2

1열

2답변

SMT (Z3)에서 변수 스왑을 모델링하는 방법은 무엇입니까?

변수를 정렬하는 프로그램이 있는데 Z3으로 유효성을 검사하려고하는데 변수가 스왑 된 코드 세그먼트가 하나 있는데 SMT 구문으로 모델링하는 방법을 모르겠습니다. 여기에 원래의 코드 세그먼트입니다 : if (x > y) { temp = x; x = y; y = temp; } 내가 주장을 쓴 SMT에 대한,하지만 난 그것을 정확

0열

1답변

Z3의 해결 전략을 제어하십시오.

그래서 Z3에서 풀어야 할 큰 문제가 있다고 가정하고, 한 번에 해결하려고하면 너무 많은 시간이 걸릴 것입니다. 그래서 저는이 문제를 부분적으로 나누어서 개별적으로 풀어냅니다. 장난감 예를 들어 내 복잡한 문제가 그 3 개 방정식을 해결하는 것으로 가정 할 수 있습니다으로 : eq1: x>5 eq2: y<6 eq3: x+y = 10 그래서 제 질문은

0열

1답변

smt2 형식 예제에서 z3 해석기에 대한 여러 솔루션을 얻는 방법은 무엇입니까?

sm3 형식의 z3 해석기를 사용하여 비트 벡터 수식에 대한 여러 모델을 생성하는 방법은 무엇입니까? 비트 벡터 용 IDEA 코드를 구현하는 동안 하나의 모델이 생성됩니다. 가능한 모든 모델을 생성하는 방법은 있습니까? ex.smt2 파일 (set-logic QF_BV) (set-info :smt-lib-version 2.0) (declare-const

0열

1답변

Z3Py : eval 또는 z3.parse_smt2_string을 사용하여 표현식을 파싱

다른 것들 사이에서 큰 명제식을 z3 인스턴스로 변환해야하는 Python 프로그램을 작성 중입니다. 예를 들어 a = my_atomic_proposition("a") # Bool b = my_atomic_proposition("b", operator.ge, 42) # Real: c >= 42 c = my_atomic_proposition("c") # B

0열

1답변

angr 메모리 맵

나는 angr - 문서의 과제 중 하나 (https://github.com/angr/angr-doc/blob/2d45c9e6d9f91e83988719aa19940aec2cfd8747/examples/ekopartyctf2015_rev100/solve.py)에서 일하고 있어요하지만 내 방식에 나는이 상황이 이해 : 내가 필요 mov rdx, [rbp+var

1열

1답변

Z3에서 비트 벡터를 제로/부호 확장하는 방법은 무엇입니까?

Z3 SMT 인터페이스를 사용하여 비트 벡터에서 제로 확장을 수행 할 수 없습니다. 소스를 읽음으로써 배운 것을 보면, 다양한 바인딩 (C, C++, Python 등)을 사용할 수 있지만, SMT 인터페이스의 튜토리얼에는 호출 방법이 없습니다. SMT QF_BV 로직 표준의 zero_extend을 사용하면 Z3이 unsupported으로 표시됩니다.

1열

1답변

Z3의 C++ API를 사용하여 긴 합계를 생성 하시겠습니까?

변수 번호가 int 인 긴 합계를 만드는 데 가장 좋은 방법은 무엇입니까? expr mk_add(expr_vector args) { vector<Z3_ast> arr; for (int i = 0; i < (int)args.size(); i++) arr.push_back(args[i]); return to_expr(arg