congress

Z3 as an alternative Datalog engine

Registered by Pierre Crégut

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.