'''
This module provides functions to generate options based on Z3 solver models.
'''
import itertools
from z3 import *
from random import choice, sample
from utils.auxiliary_operator import CustomSym, generate_random_indices
import time
[docs]
def get_TF_events_for_each_solution(events, solutions, require=True):
"""
Return the events that are true/false in each feasible solution from solutions.
:param events: Array of z3.Bool type.
:param solutions: Array composed of multiple Solver.model() instances.
:param require: Whether the events should be true (True) or false (False).
"""
return [[var for var in events if (model[var] == require) or (model[var] == None) ] for model in solutions]
[docs]
def get_required_non_solutions(solutions, conditions = [], num = 5):
"""
Find num infeasible solutions that satisfy the conditions (conditions) but are not in solutions, for use as incorrect options.
:param solutions: Array composed of multiple Solver.model() instances.
:param conditions: Conditions that the incorrect options need to satisfy.
:param num: The number of groups of incorrect options to return.
"""
# 创建求解器
solver = Solver()
# 排除可行解
for model in solutions:
solver.add(Or([var() != model[var] for var in model]))
# 添加额外约束
if len(conditions):
solver.add(And(*conditions))
current_num = 0
non_solutions = []
while current_num < num and solver.check() == sat:
model = solver.model() # 获取当前解
non_solutions.append(model) # 保存解
# 添加排除条件：排除当前解的所有变量赋值
block = [var() != model[var] for var in model] # model[var()] 等价 model[var]
solver.add(Or(block)) # 要求至少有一个变量与当前解不同
current_num += 1
satisfied_res, unsatisfied_res = solutions, non_solutions
def work(res):
_ans = []
for sol in res:
_res = []
for var in sol:
if sol[var] == True:
_res.append(var())
_ans.append(tuple(_res))
return _ans
return work(satisfied_res), work(unsatisfied_res)
[docs]
def find_always_TF_events(events, solutions, require=True):
"""
Identify events (events) that are always True/False in all feasible solutions (solutions).
:param events: Array of z3.Bool type.
:param solutions: Array composed of multiple Solver.model() instances.
:param require: Whether the events should be true (True) or false (False).
:return: List of events that are always True in all solutions, `satisfied_res`, and the results that do not meet the condition, `unsatisfied_res`.
"""
satisfied_res = []
unsatisfied_res = []
for event in events:
# 检查 event 是否在所有 solutions 里都为 True
# if all(solution.eval(event, model_completion=True) == True for solution in solutions):
if all(model[event] == require for model in solutions):
satisfied_res.append(event)
else:
unsatisfied_res.append(event)
return satisfied_res, unsatisfied_res
[docs]
def find_required_event_groups(events, correct_num, incorrect_num, solutions, formula, cond = "all", event_num = [2], order = None, duplicate = None, custom_cond = [], env = {}):
"""
Find event_num events that satisfy the condition among all feasible solutions.
By default, it identifies all pairs of events where at most one is true.
:param events: Array of events, similar to DerivedSymbol.source in DSL.
:param correct_num: Number of correct items.
:param incorrect_num: Number of incorrect items.
:param solutions: Array of feasible solutions (array of Z3 models).
:param formula: Similar to formula in DSL.
:param cond: Whether all solutions must satisfy ("all") or if at least one satisfying solution is enough ("any"), similar to DerivedSymbol.cond in DSL.
:param event_num: Array specifying the number of sub-events, similar to DerivedSymbol.amount in DSL.
:param order: Similar to DerivedSymbol.order in DSL, default is all False.
:param duplicate: Similar to duplicate in DSL, default is all False.
:param custom_cond: Similar to custom_cond in DSL.
:param env: Environment variables imported from the program generated by the translator.
:return: Returns a list of satisfied event pairs `satisfied` and their index list `satisfied_indices`, as well as the unsatisfied combinations `unsatisfied` and their index list `unsatisfied_indices`.
"""
if duplicate is None:
duplicate = [False for i in range(len(events))]
if order is None:
order = [False if i == 0 else True for i in range(len(events))]
for i in range(len(events)):
if len(events[i]) < event_num[i] and duplicate[i] == False:
raise Exception(f"Cannot select {event_num[i]} distinct items from {events[i]}")
if type(events[i]) != list:
if isinstance(events[i], CustomSym):
events[i] = events[i].to_list()
else:
events[i] = list(events[i])
# 生成正确项
satisfied_indices, satisfied_indices_config = generate_random_indices(events, event_num, correct_num, domain_cond=True, custom_cond=custom_cond + [{"scope": "option", "cond": cond, "formula": formula, "result": True}], duplicate=duplicate, order=order, env={**env, **globals(), "_solutions": solutions})
# 生成错误项
unsatisfied_indices, unsatisfied_indices_config = generate_random_indices(events, event_num, incorrect_num, domain_cond=True, custom_cond=custom_cond + [{"scope": "option", "cond": cond, "formula": formula, "result": False}], duplicate=duplicate, order=order, env={**env, **globals(), "_solutions": solutions})
# print(satisfied_indices, unsatisfied_indices)
# 转换为事件对象列表
satisfied = [
tuple(tuple(events[i][idx] for idx in sub_indices) for i, sub_indices in enumerate(comb))
for comb in satisfied_indices
]
unsatisfied = [
tuple(tuple(events[i][idx] for idx in sub_indices) for i, sub_indices in enumerate(comb))
for comb in unsatisfied_indices
]
return satisfied_indices_config, unsatisfied_indices_config, satisfied, unsatisfied
[docs]
def find_always_TF_combined_events(events, solutions, require=True, num=2):
"""
Analyze which combinations of num events in solutions are always true or false.
Parameters:
events: List[BoolRef], array of Z3 boolean variables (event array).
solutions: List[Model], multiple feasible solutions (array of solver.model()).
require: bool, whether the events should be true (True) or false (False).
num: int, the number of event combinations. When num = 1, it degenerates into find_always_TF_events.
Returns:
List[Tuple[BoolRef]], list of combinations of num events that satisfy the condition.
"""
result = []
# 遍历所有 num 个 events 的组合
for event_comb in itertools.combinations(events, num):
# 检查该组合是否在所有解中同时满足 require 条件
if all(all(model[event] == require for event in event_comb) for model in solutions):
result.append(event_comb)
return result
if __name__ == "__main__":
print(find_always_TF_events("abc", [{"a": True, "b": True, "c": None}, {"a": True, "b": False, "c": True}]))
print(find_always_TF_combined_events("abc", [{"a": True, "b": True, "c": True}, {"a": True, "b": False, "c": True}]))