openstack
/
congress
Code Issues Proposed changes

Adding Neutron action descriptions 

Adding realistic (though obviously not perfect)
action descriptions of the core Neutron API.

Networks, subnets, ports are done.  Outstanding issues
are listed at the top of examples/neutron.action.  Some of these
need to be addressed, but the goal of this was to understand
the extent to which Neutron/Nova/etc. actions could be expressed
and reasoned about.  Plan is to revisit the list of issues
after a similar investigation into Nova.

- Added rudimentary tests for networks, subnets, ports.

- Also fixed a bug for theory inclusion in top_down_evaluation.

- Made minor improvements to the code (e.g. there is now a Theory obj
that all the theories inherit from).

- Increased syntax to include several atoms in the head of each rule.
Necessary to describe update sequence for testing Neutron API.

All tests pass

Issue: #
Change-Id: I63b188acbe51b07e0ceffc9c747b5b62c46c92bf
This commit is contained in:
Tim Hinrichs 2013-10-17 16:22:55 -07:00
parent c3066ebf44
commit 2aafba8f97
6 changed files with 895 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

424
examples/neutron.action Normal file
View File

@ -0,0 +1,424 @@
// import("options")
// import("mac")
// import("ip")
///////////////////////////////////////////////////////////
// Issues
///////////////////////////////////////////////////////////
// Some actions invoke other actions (e.g. delete_network invokes
// delete_subnet). There's a simple way of writing this, but
// when we do projection, we would need to use a fixed-point
// computation to compute all the changes. Seemingly simple to do
// but haven't done it; hence, the delete_network example has this
// fragment commented out. Note: this impacts how we store/represent
// results.
// Notion of 'results' is clunky and may be problematic down the road.
// Need mapping from real neutron actions to these actions when simulating.
// - Each Bulk operation maps to a sequence of our actions
// - Subnet creation maps to one subnet_create and a series of
// assign_subnet_allocation_pools
// Not capturing all of the constraints on when an action can be execed
// - create_subnet and delete_subnet require manipulating IP addresses
// - see notes
// Not properly handling access control policy -- additional conditions should
// be grafted onto the policy below, after analyzing AC policy
// Because we're not necessarily grounding everything, builtins/negation
// may be encountered that are not ground. Perhaps the right answer is
// to delay their evaluation until they are ground. For builtins, it
// is probably okay to just return the unground ones, e.g. that way
// skolemization turns into constraint solving. For negatives,
// it is an error if we never get to evaluate them. I suppose this is
// just a variant of abduction. But it means that we should always be using
// abduction when processing the action theory.
// Should be 'import'ing modules that we care about. Implementationally,
// this is straightforward to implement using theory includes. Need
// to enable cycles through imports, which would cause an infinite loop
// during top_down_evaluation. But since we
// are always querying the top-level action theory, we should be
// able to eliminate cycles. Or we could modify top_down_includes
// to avoid the infinite loop.
///////////////////////////////////////////////////////////
// Congress-defined "actions"/builtins
///////////////////////////////////////////////////////////
// Representing optional parameters to API calls with options:value
// Maybe use 'support' instead of 'action' so that during
// abduction we can save both 'support' and 'action' but
// we do not get confused about what the legit actions are.
action("options:value")
// hacks to avoid dealing with builtins
action("sys:userid") // the name of the user currently logged in
action("sys:user") // a list of all users
action("sys:mac_address") // 'list' of all mac addresses
action("cms:admin") // group of users considered administrators
// Options module
// Check if a key is present
options:present(options, key) :-
options:value(options, key, value)
// Compute value of one of the options, providing a default if not present
// options:lookup(options, key, default, result)
options:lookup(options, key, old, old) :-
not options:present(options, key)
options:lookup(options, key, old, new) :-
options:value(options, key, new)
// Mac address module
// mac:mac_address(mac) //builtin
// IP module
// ip:ip_address(ip) // builtin
// ip:ip_in_range(ip, start, end) //builtin
///////////////////////////////////////////////////////////
// Neutron helpers
///////////////////////////////////////////////////////////
// tenant_id creation
// If not present or not admin, login ID
// Otherwise, supplied value
neutron:compute.create.tenant(options, userid) :-
sys:user(userid),
not options:present(options, "tenant_id")
neutron:compute.create.tenant(options, userid) :-
sys:user(userid),
not cms:admin(userid)
neutron:compute.create.tenant(options, value) :-
sys:user(userid),
cms:admin(userid),
options:value(options, "tenant_id", value)
// tenant_id update
// Cannot update tenant_id unless user requesting action is admin
neutron:compute.update.tenant(options, old, old) :-
not options:present(options, "tenant_id")
neutron:compute.update.tenant(options, old, tenant_op) :-
options:present(options, "tenant_id"),
options:value(options, "tenant_id", tenant_op),
sys:user(userid),
cms:admin(userid)
///////////////////////////////////////////////////////////
// Ports
///////////////////////////////////////////////////////////
/////////////////////////////
// Create port
// Modeling differences from reality:
// - Fixed_ips and security_groups cannot be provided at creation-time
// - Fixed_ips and security_groups can only be updated after creation
// - Storing fixed_ips and security_groups in separate tables, keyed
// on the port's ID.
// Tables we're manipulating:
// neutron:port(id, name, network_id, mac_address, device_id, device_owner, status, admin_state_up, tenant_id)
// neutron:port.ip(id, ip)
// neutron:available_ip(ip)
// neutron:port.security_group(id, group_id)
action("neutron:create_port")
result(id) :-
neutron:port+(id, network_id, name, mac_address, "null", "null", status, admin_state_up, tenant_id)
neutron:port+(id, network_id, name, mac_address, "null", "null", status, admin_state_up, tenant_id) :-
neutron:create_port(network_id, options),
options:lookup(options, "name", "", name),
neutron:create_port.compute.mac_address(options, mac_address),
neutron:compute.create.tenant(options, tenant_id)
// If given value but not mac_address, it's a noop.
neutron:create_port.compute.mac_address(options, mac_address) :-
not options:present(options, "mac_address")
neutron:create_port.compute.mac_address(options, value) :-
options:value(options, "mac_address", value),
mac:mac_address(value)
/////////////////////////////
// Update port
// Note: updating a port is not the same as deleting old and adding new
// but that's how we have to model it. If we generate a remediation
// with both a delete and an add, we need to postprocess it to create
// an update. Of course, that requires knowing what the add/delete/update
// actions are and how to combine an add and a delete to produce an update.
// Annoying, but no way around it I can see. Maybe for the common case
// we'd want a macro language that spits out the code above and below.
// Semantics: first delete and then insert
action("neutron:update_port")
result(id) :-
neutron:port+(id, network_id, name, mac_address, device_id, device_owner, status, admin_state_up, tenant_id)
// delete the old
neutron:port-(id, network_id_old, name_old, mac_address_old, device_id_old, device_owner_old, status_old, admin_state_up_old, tenant_id_old) :-
neutron:update_port(id, options),
neutron:port(id, network_id_old, name_old, mac_address_old, device_id_old, device_owner_old, status_old, admin_state_up_old, tenant_id_old)
// add the new
neutron:port+(id, network_id, name, mac_address, device_id, device_owner, status, admin_state_up, tenant_id) :-
neutron:update_port(id, options),
neutron:port(id, network_id_old, name_old, mac_address_old, device_id_old, device_owner_old, status_old, admin_state_up_old, tenant_id_old),
// look up optional params -- old if not present
options:lookup(options, "network_id", network_id_old, network_id),
options:lookup(options, "name", name_old, name),
options:lookup(options, "mac_address", mac_address_old, mac_address),
options:lookup(options, "device_id", device_id_old, device_id),
options:lookup(options, "device_owner", device_owner_old, device_owner),
neutron:compute.update.tenant(options, tenant_id_old, tenant_id)
// Since options:value is a relation, we can handle sets natively.
// We don't have an ordering on those sets, though I could imagine
// making options:value ternary so that we at least have the index.
// This seems like a bad idea though--since we're then writing code
// that updates the index of port.ip, for example.
// However, we won't *generate* a single API call that adds multiple
// ports. Again, post-processing should be able to help; we just need
// to know how to combine multiple API calls into a single one:
// create_port(1, x), options:value(x,"ports","a")
// + create_port(1, y), options:value(y,"ports","b")
// --------------------------------------------------
// create_port(1,z), options:value(z, "ports", "a"),
// options:value(z, "ports", "b")
// Should be more careful here so as to not depend on the conflict
// resolution semantics: delete before insert. Arguably, if an action
// results in both the insertion and deletion of a tuple, then
// there's something wrong with the policy.
// delete old IPs, if value included
neutron:port.ip-(id, ip) :-
neutron:update_port(id, options),
options:present(options, "ip")
neutron:port.ip(id, ip)
// add new ports
neutron:port.ip+(id, ip) :-
neutron:update_port(id, options),
options:value(options, "ip", ip),
neutron:available_ip(ip)
// old IPs become available
neutron:available_ip+(ip) :-
neutron:update_port(id, options),
options:present(options, "ip"),
neutron:port.ip(id, ip)
// new IPs become unavailable
neutron:available_ip-(ip) :-
neutron:update_port(id, options),
options:value(options, "ip", ip)
// delete old groups, if value included
neutron:port.security_group-(id, group) :-
neutron:update_port(id, options),
options:present(options, "security_group"),
neutron:port.security_group(id, group)
// add new ports
neutron:port.security_group+(id, group) :-
neutron:update_port(id, options),
options:value(options, "security_group", group)
/////////////////////////////
// Delete port
action("neutron:delete_port")
neutron:port-(id, network_id, name, mac_address, device_id, device_owner, status, admin_state_up, tenant_id) :-
neutron:delete_port(id),
neutron:port(id, network_id, name, mac_address, device_id, device_owner, status, admin_state_up, tenant_id)
neutron:port.ip-(id,ip) :-
neutron:delete_port(id),
neutron:port.ip(id, ip)
neutron:available_ip+(ip) :-
neutron:delete_port(id),
neutron:port.ip(id, ip)
neutron:port.security_group-(id, group) :-
neutron:delete_port(id),
neutron:port.security_group(id, group)
///////////////////////////////////////////////////////////
// Subnets
///////////////////////////////////////////////////////////
// Tables:
// neutron:subnet(id, name, network_id, gateway_ip, ip_version, cidr, enable_dhcp, tenant_id)
// neutron:subnet.allocation_pool(subnetid, start, end)
// Modeling approximation: instead of creating a subnet and including
// unchangeable allocation pools, we create a subnet and then execute
// the action "neutron:extend_subnet_allocation_pools" several times
/////////////////////////////
// Create subnet
action("neutron:create_subnet")
result(id) :-
neutron:subnet+(id, name, network_id, gateway_ip, ip_version, cidr, enable_dhcp, tenant_id)
// What do we do about the fact that in reality you must supply
// a valid IP if you provide a gateway_ip. Could add that constraint
// but then our simulation will be *generating*
// an IP address here WITHIN the logic. One option:
// we extract constraints (builtins that are unground)
// and then satisfy them when skolemizing.
// We can always bail out since this is an approximation anyway.
neutron:subnet+(id, name, network_id, gateway_ip, ip_version, cidr, enable_dhcp, tenant_id) :-
neutron:create_subnet(network_id, cidr, options),
options:lookup(options, "name", "", name),
options:lookup(options, "gateway_ip", gateway_ip, gateway_ip),
options:lookup(options, "ip_version", 4, ip_version),
options:lookup(options, "enable_dhcp", "true", enable_dhcp),
neutron:compute.create.tenant(options, tenant_id)
action("neutron:assign_subnet_allocation_pools")
neutron:subnet.allocation_pool+(id, start, end) :-
neutron:assign_subnet_allocation_pools(id, start, end)
/////////////////////////////
// Update subnet
action("neutron:update_subnet")
neutron:subnet-(id, name, network_id, gateway_ip, ip_version, cidr, enable_dhcp, tenant_id) :-
neutron:update_subnet(id, options),
neutron:subnet(id, name, network_id, gateway_ip, ip_version, cidr, enable_dhcp, tenant_id)
neutron:subnet+(id, name, network_id, gateway_ip, ip_version, cidr, enable_dhcp, tenant_id) :-
neutron:update_subnet(id, options),
neutron:subnet(id, name_old, network_id_old, gateway_ip_old, ip_version, cidr, enable_dhcp_old, tenant_id_old),
options:lookup(options, "name", name_old, name),
options:lookup(options, "network_id", network_id_old, network_id),
options:lookup(options, "gateway_ip", gateway_ip_old, gateway_ip),
options:lookup(options, "enable_dhcp", enable_dhcp_old, enable_dhcp),
neutron:compute.update.tenant(options, tenant_id_old, tenant_id)
/////////////////////////////
// Delete subnet
action("neutron:delete_subnet")
neutron:subnet-(id, name, network_id, gateway_ip, ip_version, cidr, enable_dhcp, tenant_id) :-
neutron:delete_subnet(id),
not neutron:some_allocated_ip(id),
neutron:subnet(id, name, network_id, gateway_ip, ip_version, cidr, enable_dhcp, tenant_id)
some_allocated_ip(subnet_id) :-
neutron:port(port_id, ip),
neutron:subnet.allocation_pool(subnet_id, start, end),
ip:ip_in_range(ip, start, end) // empty until we attach it
///////////////////////////////////////////////////////////
// Networks
///////////////////////////////////////////////////////////
// Tables:
// neutron:network(id, name, status, admin_state, shared, tenant_ID)
// neutron:network.subnets(id, subnet)
/////////////////////////////
// Create network
result(id) :-
neutron:network+(id, name, status, admin_state, shared, tenant_id)
action("neutron:create_network")
neutron:network+(id, name, status, admin_state, shared, tenant_id) :-
neutron:create_network(options),
options:lookup(options, "name", "", name),
options:lookup(options, "admin_state", "true", admin_state),
options:lookup(options, "shared", "true", shared),
neutron:compute.create.tenant(options, tenant_id)
/////////////////////////////
// Update network
// Note: updating a port is not the same as deleting old and adding new
// but that's how we have to model it. If we generate a remediation
// with both a delete and an add, we need to postprocess it to create
// an update. Of course, that requires knowing what the add/delete/update
// actions are and how to combine an add and a delete to produce an update.
// Annoying, but no way around it I can see. Maybe for the common case
// we'd want a macro language that spits out the code above and below.
// Semantics: first delete and then insert
action("neutron:update_network")
result(id) :-
neutron:network+(id, name, status, admin_state, shared, tenant_id)
// delete the old
neutron:network-(id, name, status, admin_state, shared, tenant_id) :-
neutron:update_network(id, options),
neutron:network(id, name, status, admin_state, shared, tenant_id)
// add the new
neutron:network+(id, name, status, admin_state, shared, tenant_id) :-
neutron:update_network(id, options),
neutron:network(id, name_old, status, admin_state_old, shared_old, tenant_id_old),
// look up optional params -- old if not present
options:lookup(options, "name", name_old, name),
options:lookup(options, "admin_state", admin_state_old, admin_state),
options:lookup(options, "shared", shared_old, shared),
neutron:compute.update.tenant(options, tenant_id_old, tenant_id)
// Should be more careful here so as to not depend on the conflict
// resolution semantics: delete before insert. Arguably, if a change
// results in both the insertion and deletion of a tuple, then
// there's something wrong with the policy.
// delete old subnets, if value included
neutron:network.subnet-(id, subnet) :-
neutron:update_network(id, options),
options:present(options, "subnet")
neutron:network.subnet(id, subnet)
// add new subnets
neutron:network.subnet+(id, subnet) :-
neutron:update_network(id, options),
options:value(options, "subnet", subnet)
/////////////////////////////
// Delete network
// Can only be executed if no ports configured for network
action("neutron:delete_network")
neutron:network-(id, name, status, admin_state, shared, tenant_id) :-
neutron:delete_network(id),
not neutron:some_port_configured(id),
neutron:network(id, name, status, admin_state, shared, tenant_id)
neutron:network.subnet-(id,subnet) :-
neutron:delete_network(id),
not some_port_configured(id),
neutron:network.subnet(id, subnet)
// CASCADING DELETE -- WANT TO BE ABLE TO SAY THAT DELETE_NETWORK CAUSES
// DELETE_SUBNET. CAN'T REALLY DO THAT. MAYBE WE WANT TO DO IT OUTSIDE.
// neutron:delete_subnet*(subnet_id) :-
// neutron:delete_network(id),
// not some_port_configured(id),
// neutron:network.subnet(id, subnet_id)
neutron:some_port_configured(network) :-
neutron:port+(id, network, name, mac_address, device_id, device_owner, status, admin_state_up, tenant_id)

7
src/policy/Congress.g
View File

@ -21,6 +21,7 @@ tokens {
LITERAL;
ATOM;
NOT;
AND;
// Terms
VARIABLE;
@ -50,11 +51,11 @@ bare_formula
;
rule
: atom COLONMINUS literal_list -> ^(RULE atom literal_list)
: literal_list COLONMINUS literal_list -> ^(RULE literal_list literal_list)
;
literal_list
: literal (COMMA literal)* -> literal+
: literal (COMMA literal)* -> ^(AND literal+)
;
literal
@ -88,7 +89,7 @@ object_constant
;
variable
: ID -> ^(VARIABLE ID)
: ID -> ^(VARIABLE ID)
;
relation_constant

84
src/policy/compile.py
View File

@ -317,31 +317,43 @@ class Literal(Atom):
class Rule (object):
""" Represents a rule, e.g. p(x) :- q(x). """
def __init__(self, head, body, location=None):
self.head = head
# self.head is self.heads[0]
# Keep self.head around since a rule with multiple
# heads is not used by reasoning algorithms.
# Most code ignores self.heads entirely.
if isinstance(head, Atom):
self.head = head
self.heads = [head]
else:
self.heads = head
self.head = self.heads[0]
self.body = body
self.location = location
def __str__(self):
return "{} :- {}".format(
str(self.head),
", ".join([str(lit) for lit in self.heads]),
", ".join([str(atom) for atom in self.body]))
def __eq__(self, other):
return (self.head == other.head and
return (len(self.heads) == len(other.heads) and
len(self.body) == len(other.body) and
all(self.heads[i] == other.heads[i]
for i in xrange(0, len(self.heads))) and
all(self.body[i] == other.body[i]
for i in xrange(0, len(self.body))))
for i in xrange(0, len(self.body))))
def __repr__(self):
return "Rule(head={}, body={}, location={})".format(
repr(self.head),
"[" + ",".join(repr(arg) for arg in self.heads) + "]",
repr(self.location),
"[" + ",".join(repr(arg) for arg in self.body) + "]",
repr(self.location))
def __hash__(self):
# won't properly treat a positive literal and an atom as the same
return hash("Rule(head={}, body={})".format(
repr(self.head),
"[" + ",".join(repr(arg) for arg in self.heads) + "]",
"[" + ",".join(repr(arg) for arg in self.body) + "]"))
def is_atom(self):
@ -354,30 +366,42 @@ class Rule (object):
return self.head.table
def variables(self):
vs = self.head.variables()
vs = set()
for lit in self.heads:
vs |= lit.variables()
for lit in self.body:
vs |= lit.variables()
return vs
def variable_names(self):
vs = self.head.variable_names()
vs = set()
for lit in self.heads:
vs |= lit.variable_names()
for lit in self.body:
vs |= lit.variable_names()
return vs
def plug(self, binding, caller=None):
newhead = self.head.plug(binding, caller=caller)
newbody = [lit.plug(binding, caller=caller) for lit in self.body]
return Rule(newhead, newbody)
newheads = self.plug_heads(binding, caller)
newbody = self.plug_body(binding, caller)
return Rule(newheads, newbody)
def plug_body(self, binding, caller=None):
return [lit.plug(binding, caller=caller) for lit in self.body]
def plug_heads(self, binding, caller=None):
return [atom.plug(binding, caller=caller) for atom in self.heads]
def invert_update(self):
new = copy.copy(self)
new.head = self.head.invert_update()
new.heads = [atom.invert_update() for atom in self.heads]
new.head = new.heads[0]
return new
def drop_update(self):
new = copy.copy(self)
new.head = self.head.drop_update()
new.heads = [atom.drop_update() for atom in self.heads]
new.head = new.heads[0]
return new
@ -400,6 +424,19 @@ def is_update(x):
else:
return False
def is_result(x):
""" Returns T iff x is a formula or tablename representing the result of
an action invocation. """
if isinstance(x, basestring):
return x == 'result'
elif isinstance(x, Atom):
return is_update(x.table)
elif isinstance(x, Rule):
return is_update(x.head.table)
else:
return False
##############################################################################
## Compiler
##############################################################################
@ -519,15 +556,19 @@ class CongressSyntax (object):
@classmethod
def create_rule(cls, antlr):
# (RULE (ATOM LITERAL1 ... LITERALN))
# Makes body a list of literals
head = cls.create_atom(antlr.children[0])
body = []
for i in xrange(1, len(antlr.children)):
body.append(cls.create_literal(antlr.children[i]))
# (RULE AND1 AND2)
heads = cls.create_and(antlr.children[0])
body = cls.create_and(antlr.children[1])
loc = Location(line=antlr.children[0].token.line,
col=antlr.children[0].token.charPositionInLine)
return Rule(head, body, location=loc)
return Rule(heads, body, location=loc)
@classmethod
def create_and(cls, antlr):
# (AND (ARG1 ... ARGN))
# For now we represent ANDs as simple lists. Convenient
# since we only have rules.
return [cls.create(child) for child in antlr.children]
@classmethod
def create_literal(cls, antlr):
@ -586,7 +627,8 @@ class CongressSyntax (object):
ObjectConstant.FLOAT,
location=loc)
elif op == 'VARIABLE':
return Variable(antlr.children[0].getText(), location=loc)
name = "".join([child.getText() for child in antlr.children])
return Variable(name, location=loc)
else:
raise CongressException("Unknown term operator: {}".format(op))

185
src/policy/runtime.py
View File

@ -2,9 +2,10 @@
import collections
import logging
import copy
import compile
import unify
import copy
class Tracer(object):
def __init__(self):
@ -65,7 +66,7 @@ class Event(object):
iterstr(self.proofs))
def iterstr(iter):
return "[" + ",".join([str(x) for x in iter]) + "]"
return "[" + ";".join([str(x) for x in iter]) + "]"
##############################################################################
## Logical Building Blocks
@ -128,7 +129,29 @@ class DeltaRule(object):
## Abstract Theories
##############################################################################
class TopDownTheory(object):
class Theory(object):
def __init__(self, name=None, abbr=None):
self.includes = []
self.tracer = Tracer()
if name is None:
self.name = repr(self)
else:
self.name = name
if abbr is None:
self.abbr = "th"
else:
self.abbr = abbr
if len(self.abbr) > 4:
self.trace_prefix = self.abbr[0:4]
else:
self.trace_prefix = (" " * (4 - len(self.abbr))) + self.abbr
def log(self, table, msg, depth=0):
self.tracer.log(table, self.trace_prefix + ": " + msg, depth)
class TopDownTheory(Theory):
""" Class that holds the Top-Down evaluation routines. Classes
will inherit from this class if they want to import and specialize
those routines. """
@ -168,11 +191,14 @@ class TopDownTheory(object):
ANSWERS is populated by top-down evaluation: it is the list of
VARIABLES instances that the search process proved true."""
def __init__(self, variables, binding, find_all=True, save=None):
def __init__(self, variables, binding, theory,
find_all=True, save=None):
# an iterable of variable objects
self.variables = variables
# a bi-unifier
self.binding = binding
# the top-level theory (for included theories)
self.theory = theory
# a boolean
self.find_all = find_all
# The results of top-down-eval: a list of TopDownResults
@ -190,6 +216,9 @@ class TopDownTheory(object):
iterstr(self.variables), str(self.binding), str(self.find_all),
iterstr(self.results), repr(self.save), iterstr(self.support)))
#########################################
## External interface
def select(self, query, find_all=True):
""" Return list of instances of QUERY that are true.
If FIND_ALL is False, the return list has at most 1 element."""
@ -299,8 +328,8 @@ class TopDownTheory(object):
would not make sense. Returns a list of TopDownResults. """
if binding is None:
binding = self.new_bi_unifier()
caller = self.TopDownCaller(variables, binding, find_all=find_all,
save=save)
caller = self.TopDownCaller(variables, binding, self,
find_all=find_all, save=save)
if len(literals) == 0:
self.top_down_finish(None, caller)
else:
@ -309,6 +338,9 @@ class TopDownTheory(object):
self.top_down_eval(context, caller)
return list(set(caller.results))
#########################################
## Internal implementation
def top_down_eval(self, context, caller):
""" Compute all instances of LITERALS (from LITERAL_INDEX and above)
that are true according to the theory (after applying the
@ -343,7 +375,7 @@ class TopDownTheory(object):
new_context = self.TopDownContext([lit.complement()],
0, context.binding, None, context.depth + 1)
new_caller = self.TopDownCaller(caller.variables, caller.binding,
find_all=False, save=None)
caller.theory, find_all=False, save=None)
# Make sure new_caller has find_all=False, so we stop as soon
# as we can.
# Ensure save=None so that abduction does not save anything.
@ -354,8 +386,19 @@ class TopDownTheory(object):
else:
# don't need bindings b/c LIT must be ground
return self.top_down_finish(context, caller, redo=False)
elif lit.tablename() == 'true':
self.print_call(lit, context.binding, context.depth)
return self.top_down_finish(context, caller, redo=False)
elif lit.tablename() == 'false':
self.print_fail(lit, context.binding, context.depth)
return False
else:
return self.top_down_includes(context, caller)
return self.top_down_truth(context, caller)
def top_down_truth(self, context, caller):
""" Do top-down evaluation over the root theory at which
the call was made and all the included theories. """
return caller.theory.top_down_includes(context, caller)
def top_down_includes(self, context, caller):
""" Top-down evaluation of all the theories included in this theory. """
@ -363,7 +406,7 @@ class TopDownTheory(object):
if is_true and not caller.find_all:
return True
for th in self.includes:
is_true = th.top_down_eval(context, caller)
is_true = th.top_down_includes(context, caller)
if is_true and not caller.find_all:
return True
return False
@ -459,8 +502,8 @@ class TopDownTheory(object):
literal.plug(binding)))
return False
def log(self, table, msg, depth=0):
self.tracer.log(table, "TDT: " + msg, depth)
#########################################
## Routines for specialization
@classmethod
def new_bi_unifier(cls, dictionary=None):
@ -632,7 +675,8 @@ class Database(TopDownTheory):
return None
return changes
def __init__(self):
def __init__(self, name=None, abbr=None):
super(Database, self).__init__(name=name, abbr=abbr)
self.data = {}
self.tracer = Tracer()
self.includes = []
@ -683,9 +727,6 @@ class Database(TopDownTheory):
def table_names(self):
return self.data.keys()
def log(self, table, msg, depth=0):
self.tracer.log(table, "DB: " + msg, depth)
def is_noop(self, event):
""" Returns T if EVENT is a noop on the database. """
# insert/delete same code but with flipped return values
@ -783,7 +824,8 @@ class Database(TopDownTheory):
class NonrecursiveRuleTheory(TopDownTheory):
""" A non-recursive collection of Rules. """
def __init__(self, rules=None):
def __init__(self, rules=None, name=None, abbr=None):
super(NonrecursiveRuleTheory, self).__init__(name=name, abbr=abbr)
# dictionary from table name to list of rules with that table in head
self.contents = {}
# list of other theories that are implicitly included in this one
@ -800,7 +842,8 @@ class NonrecursiveRuleTheory(TopDownTheory):
""" Insert RULE and return True iff the theory changed. """
if isinstance(rule, compile.Atom):
rule = compile.Rule(rule, [], rule.location)
self.log(rule.head.table, "Insert: {}".format(str(rule)))
self.log(rule.head.table,
"Insert: {}".format(str(rule)))
table = rule.head.table
if table in self.contents:
if rule not in self.contents[table]: # eliminate dups
@ -835,12 +878,16 @@ class NonrecursiveRuleTheory(TopDownTheory):
""" Deletes contents of theory. """
self.contents = {}
def log(self, table, msg, depth=0):
self.tracer.log(table, "NRT: " + msg, depth)
def content(self):
results = []
for table in self.contents:
results.extend(self.contents[table])
return results
class DeltaRuleTheory (object):
class DeltaRuleTheory (Theory):
""" A collection of DeltaRules. """
def __init__(self):
def __init__(self, name=None, abbr=None):
super(DeltaRuleTheory, self).__init__(name=name, abbr=abbr)
# dictionary from table name to list of rules with that table as trigger
self.contents = {}
# dictionary from delta_rule to the rule from which it was derived
@ -987,11 +1034,12 @@ class MaterializedRuleTheory(TopDownTheory):
""" A theory that stores the table contents explicitly.
Recursive rules are allowed. """
def __init__(self):
def __init__(self, name=None, abbr=None):
super(MaterializedRuleTheory, self).__init__(name=name, abbr=abbr)
# queue of events left to process
self.queue = EventQueue()
# collection of all tables
self.database = Database()
self.database = Database(abbr="DB")
# tracer object
self.tracer = Tracer()
# rules that dictate how database changes in response to events
@ -1035,9 +1083,6 @@ class MaterializedRuleTheory(TopDownTheory):
############### Interface implementation ###############
def log(self, table, msg, depth=0):
self.tracer.log(table, "MRT: " + msg, depth)
def explain_aux(self, query, depth):
self.log(query.table, "Explaining {}".format(str(query)), depth)
# Bail out on negated literals. Need different
@ -1214,9 +1259,11 @@ class MaterializedRuleTheory(TopDownTheory):
return [table for table in self.database.table_names()
if not self.is_view(table)]
def top_down_eval(self, context, caller):
return self.database.top_down_eval(context, caller)
def top_down_th(self, context, caller):
return self.database.top_down_th(context, caller)
def content(self):
return self.database.content()
##############################################################################
## Runtime
##############################################################################
@ -1228,6 +1275,7 @@ class Runtime (object):
CLASSIFY_THEORY = "classification"
SERVICE_THEORY = "service"
ACTION_THEORY = "action"
OPERATIONS_THEORY = "operations"
def __init__(self):
@ -1237,7 +1285,7 @@ class Runtime (object):
self.theory = {}
# CLASSIFY_THEORY: the policy
# Allow negation for sure. Currently supports recursion.
self.theory[self.CLASSIFY_THEORY] = MaterializedRuleTheory()
self.theory[self.CLASSIFY_THEORY] = MaterializedRuleTheory(abbr='Clas')
# ACTION_THEORY: describes how actions affect tables
# non-recursive, with semi-positive negation over base tables
# of CLASSIFY_THEORY, i.e. no negation over views of
@ -1251,14 +1299,16 @@ class Runtime (object):
# of rules or any other tables defined in ACTION_THEORY.
# Should throw warning if referencing table not appearing
# in either and provide special table False.
self.theory[self.ACTION_THEORY] = NonrecursiveRuleTheory()
self.theory[self.ACTION_THEORY] = NonrecursiveRuleTheory(abbr='Act')
self.theory[self.ACTION_THEORY].includes.append(
self.theory[self.CLASSIFY_THEORY])
# SERVICE_THEORY: describes bindings for tables to real-world
# software.
# Need bindings for every base-table in CLASSIFY_THEORY
# and every action in ACTION_THEORY.
self.theory[self.SERVICE_THEORY] = NonrecursiveRuleTheory()
self.theory[self.SERVICE_THEORY] = NonrecursiveRuleTheory(abbr='Serv')
# OPERATIONS_THEORY: describes what actions to take and when
self.theory[self.OPERATIONS_THEORY] = NonrecursiveRuleTheory(abbr='Ops')
def get_target(self, name):
if name is None:
@ -1273,7 +1323,7 @@ class Runtime (object):
return [action.arguments[0].name for action in actions]
def log(self, table, msg, depth=0):
self.tracer.log(table, "RT: " + msg, depth)
self.tracer.log(table, " RT: " + msg, depth)
def debug_mode(self):
tracer = Tracer()
@ -1282,6 +1332,7 @@ class Runtime (object):
self.theory[self.CLASSIFY_THEORY].tracer = tracer
self.theory[self.SERVICE_THEORY].tracer = tracer
self.theory[self.ACTION_THEORY].tracer = tracer
self.theory[self.OPERATIONS_THEORY].tracer = tracer
self.theory[self.CLASSIFY_THEORY].database.tracer = tracer
def production_mode(self):
@ -1290,6 +1341,7 @@ class Runtime (object):
self.theory[self.CLASSIFY_THEORY].tracer = tracer
self.theory[self.SERVICE_THEORY].tracer = tracer
self.theory[self.ACTION_THEORY].tracer = tracer
self.theory[self.OPERATIONS_THEORY].tracer = tracer
self.theory[self.CLASSIFY_THEORY].database.tracer = tracer
############### External interface ###############
@ -1467,7 +1519,7 @@ class Runtime (object):
# terms of base tables, despite us asking for base tables--
# because of negation.)
leaves = [leaf for leaf in proofs[0].leaves()
if (isinstance(leaf, compile.Literal) and
if (isinstance(leaf, compile.Atom) and
leaf.table in base_tables)]
logging.debug("Leaves: {}".format(iterstr(leaves)))
# Query action theory for abductions of negated base tables
@ -1501,12 +1553,18 @@ class Runtime (object):
assert all(isinstance(x, compile.Rule) or isinstance(x, compile.Atom)
for x in sequence), "Sequence must be an iterable of Rules"
# apply SEQUENCE
self.log(query.tablename(), "** Simulate: Applying sequence {}".format(
iterstr(sequence)))
undo = self.project(sequence)
# query the resulting state
self.log(query.tablename(), "** Simulate: Querying {}".format(
str(query)))
result = self.theory[self.CLASSIFY_THEORY].select(query)
self.log(query.tablename(), "Result of {} is {}".format(
str(query), iterstr(result)))
# rollback the changes
self.log(query.tablename(), "** Simulate: Rolling back")
self.project(undo)
return result
@ -1515,34 +1573,71 @@ class Runtime (object):
Return an update sequence that will undo the projection. """
actth = self.theory[self.ACTION_THEORY]
# apply changes to the state
newth = NonrecursiveRuleTheory()
newth = NonrecursiveRuleTheory(abbr="Temp")
newth.tracer.trace('*')
actth.includes.append(newth)
actions = self.get_actions()
self.log(None, "Actions: " + str(actions))
self.log(None, "Actions: " + iterstr(actions))
undos = [] # a list of updates that will undo SEQUENCE
self.log(None, "Projecting: " + iterstr(sequence))
last_results = []
for formula in sequence:
if formula.is_atom():
tablename = formula.table
self.log(None, "** Updating with {}".format(str(formula)))
self.log(None, "Actions: " + iterstr(actions))
self.log(None, "Last_results: " + iterstr(last_results))
tablename = formula.tablename()
if tablename not in actions:
updates = [formula]
else:
tablename = formula.head.table
if tablename in actions:
self.log(tablename, "* Projecting " + str(formula))
# add action to theory
self.log(tablename, "Projecting " + str(formula))
# define extension of current Actions theory
if formula.is_atom():
assert formula.is_ground(), \
"Projection atomic updates must be ground"
assert not formula.is_negated(), \
"Projection atomic updates must be positive"
newth.define([formula])
else:
newth.define([formula.head] + formula.body)
# instantiate action using prior results
newth.define(last_results)
self.log(tablename, "newth (with prior results) {} ".format(
iterstr(newth.content())))
bindings = actth.top_down_evaluation(formula.variables(),
formula.body, find_all=False)
if len(bindings) == 0:
continue
grounds = formula.plug_heads(bindings[0])
grounds = [act for act in grounds if
act.is_ground()]
assert all(not lit.is_negated() for lit in grounds)
newth.define(grounds)
self.log(tablename, "newth contents (after action insertion): {}".format(
iterstr(newth.content())))
# self.log(tablename, "action contents: {}".format(
# iterstr(actth.content())))
# self.log(tablename, "action.includes[1] contents: {}".format(
# iterstr(actth.includes[1].content())))
# self.log(tablename, "newth contents: {}".format(
# iterstr(newth.content())))
# compute updates caused by action
updates = actth.consequences(compile.is_update)
updates = self.resolve_conflicts(updates)
else:
updates = [formula]
updates = unify.skolemize(updates)
self.log(tablename, "Computed updates: " + iterstr(updates))
# compute results for next time
for update in updates:
newth.insert(update)
last_results = actth.consequences(compile.is_result)
last_results = set([atom for atom in last_results
if atom.is_ground()])
# apply updates
for update in updates:
undo = self.update_classifier(update)
if undo is not None:
undos.append(undo)
return reversed(undos)
undos.reverse()
actth.includes.remove(newth)
return undos
def update_classifier(self, delta):
""" Takes an atom/rule DELTA with update head table

185
src/policy/tests/test_runtime.py
View File

@ -70,12 +70,17 @@ class TestRuntime(unittest.TestCase):
self.close(msg)
def check_equal(self, actual_code, correct_code, msg=None, equal=None):
def minus(iter1, iter2):
def minus(iter1, iter2, invert=False):
extra = []
for i1 in iter1:
found = False
for i2 in iter2:
if equal(i1, i2):
# for asymmetric equality checks
if invert:
test_result = equal(i2, i1)
else:
test_result = equal(i1, i2)
if test_result:
found = True
break
if not found:
@ -87,14 +92,21 @@ class TestRuntime(unittest.TestCase):
actual = compile.parse(actual_code)
correct = compile.parse(correct_code)
extra = minus(actual, correct)
missing = minus(correct, actual)
# in case EQUAL is asymmetric, always supply actual as the first arg
missing = minus(correct, actual, invert=True)
self.output_diffs(extra, missing, msg)
logging.debug("** Finished: {} **".format(msg))
def check_same(self, actual_code, correct_code, msg=None):
""" Checks if ACTUAL_CODE is a variable-renaming of CORRECT_CODE. """
return self.check_equal(actual_code, correct_code, msg=msg,
equal=lambda x,y: unify.same(x,y) is not None)
def check_instance(self, actual_code, correct_code, msg=None):
""" Checks if ACTUAL_CODE is an instance of CORRECT_CODE. """
return self.check_equal(actual_code, correct_code, msg=msg,
equal=lambda x,y: unify.instance(x,y) is not None)
def check_proofs(self, run, correct, msg=None):
""" Check that the proofs stored in runtime RUN are exactly
those in CORRECT. """
@ -576,10 +588,23 @@ class TestRuntime(unittest.TestCase):
self.fail()
self.close(msg)
def test_instance(self):
""" Test whether the INSTANCE computation is correct. """
def assertIsNotNone(x):
self.assertTrue(x is not None)
def assertIsNone(x):
self.assertTrue(x is None)
assertIsNotNone(unify.instance(str2form('p(1)'), str2form('p(y)')))
assertIsNotNone(unify.instance(str2form('p(1,2)'), str2form('p(x,y)')))
assertIsNotNone(unify.instance(str2form('p(1,x)'), str2form('p(x,y)')))
assertIsNotNone(unify.instance(str2form('p(1,x,1)'), str2form('p(x,y,x)')))
assertIsNotNone(unify.instance(str2form('p(1,x,1)'), str2form('p(x,y,z)')))
assertIsNone(unify.instance(str2form('p(1,2)'), str2form('p(x,x)')))
def test_same(self):
""" Test whether the SAME computation is correct. """
def str2form(formula_string):
return compile.parse(formula_string)[0]
def assertIsNotNone(x):
self.assertTrue(x is not None)
def assertIsNone(x):
@ -818,10 +843,24 @@ class TestRuntime(unittest.TestCase):
"False embedded negation with existentials")
def test_theory_inclusion(self):
""" Test evaluation routines when one theory includes another. """
# spread out across inclusions
th1 = runtime.NonrecursiveRuleTheory()
th2 = runtime.NonrecursiveRuleTheory()
th3 = runtime.NonrecursiveRuleTheory()
th1.includes.append(th2)
th2.includes.append(th3)
th1.insert(str2form('p(x) :- q(x), r(x), s(2)'))
th2.insert(str2form('q(1)'))
th1.insert(str2form('r(1)'))
th3.insert(str2form('s(2)'))
self.check_equal(pol2str(th1.select(str2form('p(x)'))),
'p(1)', 'Data spread across inclusions')
# real deal
actth = runtime.Runtime.ACTION_THEORY
clsth = runtime.Runtime.CLASSIFY_THEORY
run = self.prep_runtime(msg="Theory Inclusion")
@ -831,7 +870,7 @@ class TestRuntime(unittest.TestCase):
run.insert('r(1)', target=actth)
run.insert('r(2)', target=clsth)
self.check_equal(run.select('p(x)', target=actth),
"p(1) p(2)", "Theory inclusion")
"p(1) p(2)", "Real deal")
# TODO(tim): add tests for explanations
def test_materialized_explain(self):
@ -1042,7 +1081,7 @@ class TestRuntime(unittest.TestCase):
classify_code = ('')
run = create(action_code, classify_code)
# ordered so that consequences will be p+(1) p-(1)
action_sequence = 'q(1) :- r(1)'
action_sequence = 'q(1), r(1) :- true'
check(run, action_sequence, 'p(x)', 'p(1)',
classify_code, "Deletion before insertion")
@ -1098,7 +1137,7 @@ class TestRuntime(unittest.TestCase):
'action("q") action("r")')
classify_code = 'p(1,2)'
run = create(action_code, classify_code)
action_sequence = 'q(1,2) :- r(2,3)'
action_sequence = 'q(1,2), r(2,3) :- true'
check(run, action_sequence, 'p(x,y)', 'p(1,2) p(1,3)',
classify_code, 'Action with additional info')
@ -1118,5 +1157,131 @@ class TestRuntime(unittest.TestCase):
check(run, action_sequence, 'p(x)', 'p(1)',
classify_code, 'Rule update')
# action with query
action_code = ('p+(x, y) :- q(x, y)'
'action("q")')
classify_code = ('r(1)')
run = create(action_code, classify_code)
action_sequence = 'q(x, 0) :- r(x)'
check(run, action_sequence, 'p(x,y)', 'p(1,0)',
classify_code, 'Action with query')
# action sequence with results
action_code = ('p+(id, val) :- create(val)'
'p+(id, val) :- update(id, val)'
'p-(id, val) :- update(id, newval), p(id, val)'
'action("create")'
'action("update")'
'result(x) :- create(val), p+(x,val)')
classify_code = 'hasval(val) :- p(x, val)'
run = create(action_code, classify_code)
action_sequence = 'create(0) update(x,1) :- result(x)'
check(run, action_sequence, 'hasval(x)', 'hasval(1)',
classify_code, 'Action with query')
def test_neutron_actions(self):
""" Test our encoding of the Neutron actions. Use simulation.
Just the basics. """
def check(query, action_sequence, correct, msg):
actual = run.simulate(query, action_sequence)
logging.debug("Simulate results: {}".format(
str(actual)))
self.check_instance(actual, correct, msg)
full_path = os.path.realpath(__file__)
path = os.path.dirname(full_path)
neutron_path = path + "/../../../examples/neutron.action"
run = runtime.Runtime()
run.debug_mode()
run.load_file(neutron_path, target=run.ACTION_THEORY)
#### Ports
query = 'neutron:port(x1, x2, x3, x4, x5, x6, x7, x8, x9)'
acts = 'neutron:create_port("net1", 17), sys:user("tim") :- true'
correct = 'neutron:port(id, "net1", name, mac, "null", "null", z, w, "tim")'
check(query, acts, correct, 'Simple port creation')
query = 'neutron:port(x1, x2, x3, x4, x5, x6, x7, x8, x9)'
# result(uuid): simulation-specific table that holds the results
# of the last action invocation
acts = ('neutron:create_port("net1", 17), sys:user("tim") :- true '
'neutron:update_port(uuid, 18), sys:user("tim"), '
' options:value(18, "name", "tims port") :- result(uuid) ')
correct = 'neutron:port(id, "net1", "tims port", mac, "null", "null", z, w, "tim")'
check(query, acts, correct, 'Port create, update')
query = 'neutron:port(x1, x2, x3, x4, x5, x6, x7, x8, x9)'
# result(uuid): simulation-specific table that holds the results
# of the last action invocation
acts = ('neutron:create_port("net1", 17), sys:user("tim") :- true '
'neutron:update_port(uuid, 18), sys:user("tim"), '
' options:value(18, "name", "tims port") :- result(uuid) '
'neutron:delete_port(uuid), sys:user("tim")'
' :- result(uuid) ')
correct = ''
check(query, acts, correct, 'Port create, update, delete')
#### Networks
query = 'neutron:network(id, name, status, admin_state, shared, tenenant_id)'
acts = 'neutron:create_network(17), sys:user("tim") :- true'
correct = 'neutron:network(id, "", status, "true", "true", "tim")'
check(query, acts, correct, 'Simple network creation')
query = 'neutron:network(id, name, status, admin_state, shared, tenenant_id)'
acts = ('neutron:create_network(17), sys:user("tim") :- true '
'neutron:update_network(uuid, 18), sys:user("tim"), '
' options:value(18, "admin_state", "false") :- result(uuid)')
correct = 'neutron:network(id, "", status, "false", "true", "tim")'
check(query, acts, correct, 'Network creation, update')
query = 'neutron:network(id, name, status, admin_state, shared, tenenant_id)'
acts = ('neutron:create_network(17), sys:user("tim") :- true '
'neutron:update_network(uuid, 18), sys:user("tim"), '
' options:value(18, "admin_state", "false") :- result(uuid)'
'neutron:delete_network(uuid) :- result(uuid)')
correct = ''
check(query, acts, correct, 'Network creation, update')
#### Subnets
query = ('neutron:subnet(id, name, network_id, '
'gateway_ip, ip_version, cidr, enable_dhcp, tenant_id)')
acts = ('neutron:create_subnet("net1", "10.0.0.1/24", 17), '
'sys:user("tim") :- true')
correct = ('neutron:subnet(id, "", "net1", gateway_ip, 4, '
'"10.0.0.1/24", "true", "tim")')
check(query, acts, correct, 'Simple subnet creation')
query = ('neutron:subnet(id, name, network_id, '
'gateway_ip, ip_version, cidr, enable_dhcp, tenant_id)')
acts = ('neutron:create_subnet("net1", "10.0.0.1/24", 17), '
'sys:user("tim") :- true '
'neutron:update_subnet(uuid, 17), sys:user("tim"), '
' options:value(17, "enable_dhcp", "false") :- result(uuid)')
correct = ('neutron:subnet(id, "", "net1", gateway_ip, 4, '
'"10.0.0.1/24", "false", "tim")')
check(query, acts, correct, 'Subnet creation, update')
query = ('neutron:subnet(id, name, network_id, '
'gateway_ip, ip_version, cidr, enable_dhcp, tenant_id)')
acts = ('neutron:create_subnet("net1", "10.0.0.1/24", 17), '
'sys:user("tim") :- true '
'neutron:update_subnet(uuid, 17), sys:user("tim"), '
' options:value(17, "enable_dhcp", "false") :- result(uuid)'
'neutron:delete_subnet(uuid) :- result(uuid)')
correct = ''
check(query, acts, correct, 'Subnet creation, update, delete')
def str2form(formula_string):
return compile.parse1(formula_string)
def str2pol(policy_string):
return compile.parse(policy_string)
def pol2str(policy):
return " ".join(str(x) for x in policy)
def form2str(formula):
return str(formula)
if __name__ == '__main__':
unittest.main()

89
src/policy/unify.py
View File

@ -2,6 +2,7 @@
import logging
import compile
import uuid
# A unifier designed for the bi_unify_atoms routine
# which is used by a backward-chaining style datalog implementation.
@ -316,3 +317,91 @@ def same_atoms(atom1, unifier1, atom2, unifier2, bound2):
return die()
return changes
def instance(formula1, formula2):
""" Determine if FORMULA1 is an instance of FORMULA2, i.e. if there is
some binding that when applied to FORMULA1 results in FORMULA2.
Returns None or a unifier. """
logging.debug("instance({}, {})".format(str(formula1), str(formula2)))
if isinstance(formula1, compile.Atom):
if isinstance(formula2, compile.Rule):
return None
else:
u = BiUnifier()
if instance_atoms(formula1, formula2, u) is not None:
return u
return None
elif isinstance(formula1, compile.Rule):
if isinstance(formula2, compile.Atom):
return None
else:
if len(formula1.body) != len(formula2.body):
return None
u = BiUnifier()
result = instance_atoms(formula1.head, formula2.head, u)
if result is None:
return None
for i in xrange(0, len(formula1.body)):
result = same_atoms(
formula1.body[i], formula2.body[i], u)
if result is None:
return None
return u
else:
return None
def instance_atoms(atom1, atom2, unifier2):
""" Adds bindings to UNIFIER2 to make ATOM1 equal to ATOM2
after applying UNIFIER2 to ATOM2 only. Returns None if
no such bindings make equality hold. """
def die():
undo_all(changes)
return None
logging.debug("instance_atoms({}, {})".format(str(atom1), str(atom2)))
if atom1.table != atom2.table:
return None
if len(atom1.arguments) != len(atom2.arguments):
return None
unifier1 = BiUnifier()
changes = []
for i in xrange(0, len(atom1.arguments)):
val1, binding1 = unifier1.apply_full(atom1.arguments[i])
val2, binding2 = unifier2.apply_full(atom2.arguments[i])
# logging.debug("val1: {} at {}; val2: {} at {}".format(
# str(val1), str(binding1), str(val2), str(binding2)))
if val1.is_variable() and val2.is_variable():
if bi_var_equal(val1, binding1, val2, binding2):
continue
# if we already bound either of these variables, not INSTANCE
if not bi_var_equal(val1, binding1, atom1.arguments[i], unifier1):
# logging.debug("instance_atoms: arg1 already bound")
return die()
if not bi_var_equal(val2, binding2, atom2.arguments[i], unifier2):
# logging.debug("instance_atoms: arg2 already bound")
return die()
# add binding to UNIFIER2
changes.append(binding2.add(val2, val1, binding1))
elif val1.is_variable():
return die()
elif val2.is_variable():
changes.append(binding2.add(val2, val1, binding1))
# logging.debug("var2 is a variable")
elif val1 != val2:
# unmatching object constants
# logging.debug("val1 != val2")
return die()
return changes
def skolemize(formulas):
""" Given a list of formulas, instantiate all variables
consistently with UUIDs. """
# create binding then plug it in.
variables = set()
for formula in formulas:
variables |= formula.variables()
binding = {}
for var in variables:
binding[var] = compile.Term.create_from_python(str(uuid.uuid4()))
return [formula.plug(binding) for formula in formulas]