Project

General

Profile

Feature #3832

Construct Z3 functions prior to basic constraints

Added by Alexander Diewald 12 months ago. Updated 26 days ago.

Status:
Feedback
Priority:
Normal
Assignee:
Category:
SMT
Target version:
Start date:
10/01/2019
Due date:
% Done:

0%

Estimated time:
4.00 h

Description

Problem

Currently, Z3 functions are created on the fly when DSEML expressions are translated. This requires a certain order in the constraints passed to the Transformator. This hidden requirement already led to issues in the past when basic constraints or the AF3<->Backend interface has been adjusted.

Resolution

Create all Z3 functions when the DSEML -> Z3 transformator is created such that the existence of known Z3 functions is always guaranteed independent of the constraint order passed to the transformator.

History

#1 Updated by Alexander Diewald 12 months ago

  • Target version changed from AF3 2.16 RC1 (Feature Freeze) to AF3 2.17 (Feature Freeze)

#2 Updated by Alexander Diewald 8 months ago

  • Target version changed from AF3 2.17 (Feature Freeze) to Backlog

#3 Updated by Alexander Diewald 26 days ago

  • Status changed from New to Feedback
  • Assignee changed from Alexander Diewald to Johannes Eder

Please decide if this will/should be done by someone. I don't think it is efficient if I would do it. Could also be rejected.

Also available in: Atom PDF