4
"팝업"으로 인해 증분 구속 조건 해결에서 "스택 모드"를 사용하는 목적이 문맥 (즉, 학습 된 보조 정리)을 완전히 파기하는 경우?점진적 해결의 장점은 무엇입니까?
이론적 근거 : 난 그냥 한 제약 (여러 conjuncts)가있는 경우는 스택에 별도의 프레임에 conjuncts을 쌓아 반대 같은 단일 쿼리를 만드는 것이 바람직 할 것이라고 상상한다. 만약 내가 에 1 개 이상의 제약이 있고 스택으로 점진적 해결을 사용하기로 결정했다면, 하나의 제약 조건을 쿼리 한 후 (아마도 적어도 하나) 팝업이 필요하고 아마도 "배운 보조 정리를 파괴 할 것입니다". 그래서, 점진적 해결 (스택 사용)의 이점은 무엇입니까? "팝에서 배운 속셈"은 실제로 무엇을 의미합니까?
관측 : 내 실험이 정말 유익 표시하지만 (noninc 동안 500 개 쿼리, 0.01 초에 완료 증분 해결의 총이있다, smt formulas를 참조 16sec에 완성 해결..) 와 모순 표시를 찾을 수 이 관찰.