Z3 as an alternative Datalog engine

Registered by Pierre Crégut on 2018-07-06

Z3 is an open source automatic theorem prover developed by Microsoft. This spec describes how to add Z3 as an alternative Datalog engine in Congress.

Blueprint information

Status:
Not started
Approver:
None
Priority:
Undefined
Drafter:
Pierre Crégut
Direction:
Needs approval
Assignee:
None
Definition:
New
Series goal:
None
Implementation:
Unknown
Milestone target:
None

Related branches

Sprints

Whiteboard

Gerrit topic: https://review.openstack.org/#q,topic:bp/alternative-engine-z3,n,z

Addressed by: https://review.openstack.org/582625
    WIP: Z3 engine as an alternative Datalog engine

Addressed by: https://review.openstack.org/586505
    Integration tests for Z3 engine in Congress.

Addressed by: https://review.openstack.org/616134
    builtins for z3 theories

(?)

Work Items

This blueprint contains Public information 
Everyone can see this information.