You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The below program queries for scenario_enabled, based on facts rule1, rule2, rule3.. If you look at the first answer in the output it doesnt return fact about rule2 that helped with the derivation of query.. I am not able to understand why this is happening. Appreciate any help with this.. Thanks!
from z3 import *
fp = Fixedpoint()
fp.set(engine='datalog')
fp.set('datalog.generate_explanations', True)
r = z3.BitVecSort(8)
scnario_enabled = z3.Function('scnario_enabled', r, r, r, z3.BoolSort())
rule1 = z3.Function('rule1', r, z3.BoolSort())
rule2 = z3.Function('rule2', r, z3.BoolSort())
rule3 = z3.Function('rule3', r, z3.BoolSort())
fp.register_relation(scnario_enabled, rule1, rule2, rule3)
a, b, c = z3.Consts('a b c', r)
fp.declare_var(a, b, c)
fp.rule(scnario_enabled(a, b, c), [
rule1(a),
rule2(b),
rule3(c),
])
for i in range(20):
fp.fact(rule1(i))
fp.fact(rule2(i+1))
fp.fact(rule3(i+2))
print(fp.query(scnario_enabled(a,b,c)))
def get_instructions(answers):
for ans in answers.children():
lastAnd = ans.children()[-1]
trace = lastAnd.children()[-1]
print_instructions(trace)
print("===========================")
def print_instructions(exp):
if len(exp.children()) == 0:
print(str(exp.decl()).replace('<null>:\n', ''))
return
for child_exp in exp.children():
print_instructions(child_exp)
get_instructions(fp.get_answer())
The below program queries for scenario_enabled, based on facts rule1, rule2, rule3.. If you look at the first answer in the output it doesnt return fact about rule2 that helped with the derivation of query.. I am not able to understand why this is happening. Appreciate any help with this.. Thanks!
Output
The text was updated successfully, but these errors were encountered: