diff --git a/dist/macq-0.3.6.tar.gz b/dist/macq-0.3.6.tar.gz deleted file mode 100644 index 5a9ceeb4..00000000 Binary files a/dist/macq-0.3.6.tar.gz and /dev/null differ diff --git a/dist/macq-0.3.6-py3-none-any.whl b/dist/macq-0.3.7-py3-none-any.whl similarity index 84% rename from dist/macq-0.3.6-py3-none-any.whl rename to dist/macq-0.3.7-py3-none-any.whl index 031890d3..3c350e06 100644 Binary files a/dist/macq-0.3.6-py3-none-any.whl and b/dist/macq-0.3.7-py3-none-any.whl differ diff --git a/dist/macq-0.3.7.tar.gz b/dist/macq-0.3.7.tar.gz new file mode 100644 index 00000000..999a0250 Binary files /dev/null and b/dist/macq-0.3.7.tar.gz differ diff --git a/docs/macq/extract.html b/docs/macq/extract.html index 45aca497..b278877c 100644 --- a/docs/macq/extract.html +++ b/docs/macq/extract.html @@ -6277,180 +6277,182 @@
Inherited Members
321 print("Update according to observations.") 322 for obj in to_obs: 323 f_str = raw_fluent_factored[obj]["fluent"].name -324 print("\nfluent: " + f_str) -325 print("\npossible expl. for fluent being true:") -326 for f in phi["pos expl"]: -327 if f == top: -328 print("true") -329 elif f == bottom: -330 print("false") -331 else: -332 e.pprint(f) -333 print("\npossible expl. for fluent being false:") -334 for f in phi["neg expl"]: -335 if f == top: -336 print("true") -337 elif f == bottom: -338 print("false") -339 else: -340 e.pprint(f) -341 print("\npossible expl. for fluent being unaffected:") -342 for f in phi["neutral"]: -343 if f == top: -344 print("true") -345 elif f == bottom: -346 print("false") -347 else: -348 e.pprint(f) -349 print() -350 -351 """Steps 1. (a)-(c) and Step 2 of AS-STRIPS-SLAF are taken care of in this loop.""" -352 a = token.action -353 # ensures that the action is not None (happens on the last step of a trace) -354 if a: -355 # iterate through every fluent in the fluent-factored transition belief formula -356 for phi in raw_fluent_factored.values(): -357 f = phi["fluent"] -358 -359 # create action propositions -360 pos_precond = Var(f"({f} is a precondition of {a})") -361 neg_precond = Var(f"(~{f} is a precondition of {a})") -362 pos_effect = Var(f"({a} causes {f})") -363 neg_effect = Var(f"({a} causes ~{f})") -364 neutral = Var(f"({a} has no effect on {f})") -365 -366 all_var.update( -367 [pos_precond, neg_precond, pos_effect, neg_effect, neutral] -368 ) -369 -370 # update the fluent-factored formula -371 all_phi_pos = [p.simplify() for p in phi["pos expl"]] -372 all_phi_neg = [n.simplify() for n in phi["neg expl"]] -373 all_phi_neut = [n.simplify() for n in phi["neutral"]] -374 phi["pos expl"] = set() -375 phi["neg expl"] = set() -376 -377 """Steps 1 (a-c) - Update every fluent in the fluent-factored transition belief formula -378 with information from the last step.""" -379 -380 """Step 1 (a) - update the neutral effects.""" -381 phi["neutral"].update( -382 [(~pos_precond | p).simplify() for p in all_phi_pos] -383 ) -384 phi["neutral"].update( -385 [(~neg_precond | n).simplify() for n in all_phi_neg] -386 ) -387 -388 """Step 1 (b) - update the positive effects.""" -389 phi["pos expl"].add(pos_effect | neutral) -390 phi["pos expl"].add(pos_effect | ~neg_precond) -391 phi["pos expl"].update( -392 [(pos_effect | p).simplify() for p in all_phi_pos] -393 ) -394 -395 """Step 1 (c) - update the negative effects.""" -396 phi["neg expl"].add(neg_effect | neutral) -397 phi["neg expl"].add(neg_effect | ~pos_precond) -398 phi["neg expl"].update( -399 [(neg_effect | n).simplify() for n in all_phi_neg] -400 ) -401 -402 """add validity constraints (from section 5.2 of the SLAF paper).""" -403 validity_constraints.add(pos_effect | neg_effect | neutral) -404 validity_constraints.add((~pos_effect | ~neg_effect)) -405 validity_constraints.add(~neg_effect | ~neutral) -406 validity_constraints.add(~pos_effect | ~neutral) -407 validity_constraints.add(~pos_precond | ~neg_precond) -408 -409 """Step 2 - eliminate subsumed clauses in phi.""" -410 SLAF.__remove_subsumed_clauses(phi["pos expl"]) -411 SLAF.__remove_subsumed_clauses(phi["neg expl"]) -412 SLAF.__remove_subsumed_clauses(phi["neutral"]) -413 # display current updates -414 if debug_mode: -415 if a: -416 print("\nAction taken: " + str(a) + "\n") -417 for obj in to_obs: -418 f_str = raw_fluent_factored[obj]["fluent"].name -419 print("\nfluent: " + f_str) -420 print( -421 "\npossible expl. for fluent being true after " -422 + str(a) -423 + ":" -424 ) -425 for f in phi["pos expl"]: -426 if f == top: -427 print("true") -428 elif f == bottom: -429 print("false") -430 else: -431 e.pprint(f) -432 print( -433 "\npossible expl. for fluent being false after " -434 + str(a) -435 + ":" -436 ) -437 for f in phi["neg expl"]: -438 if f == top: -439 print("true") -440 elif f == bottom: -441 print("false") -442 else: -443 e.pprint(f) -444 print( -445 "\npossible expl. for fluent being unaffected after " -446 + str(a) -447 + ":" -448 ) -449 for f in phi["neutral"]: -450 if f == top: -451 print("true") -452 elif f == bottom: -453 print("false") -454 else: -455 e.pprint(f) -456 print() -457 user_input = input("Hit enter to continue.\n") -458 -459 formula = set() -460 """Convert to formula once you have stepped through all observations and applied all transformations. -461 NOTE: This would have to be refactored if the functionality for multiple traces was added, as each trace would -462 have to store its own separate formulas, and the conjunction would be taken at the end.""" -463 for phi in raw_fluent_factored.values(): -464 f = phi["fluent"] -465 # convert to formula for each fluent -466 all_phi_pos = [p.simplify() for p in phi["pos expl"]] -467 all_phi_neg = [n.simplify() for n in phi["neg expl"]] -468 all_phi_neut = [n.simplify() for n in phi["neutral"]] -469 formula.update([(~f | p).simplify() for p in all_phi_pos]) -470 formula.update([(f | n).simplify() for n in all_phi_neg]) -471 formula.update([n for n in all_phi_neut]) -472 # add the validity constraints -473 formula.update(validity_constraints) -474 # create CNF formula -475 full_formula = And({*[f.simplify() for f in formula]}).simplify() -476 cnf_formula = And(map(SLAF.__or_refactor, full_formula.children)) -477 -478 entailed = set() -479 if sample: -480 with config(sat_backend="kissat"): -481 sol = cnf_formula.solve() -482 if sol: -483 for f in all_var: -484 if sol[str(f)]: -485 entailed.add(f) -486 else: -487 children = set(cnf_formula.children) -488 # iterate through all fluents, gathering those that are entailed -489 for f in all_var: -490 children.add(Or([~f])) -491 check_theory = And(children) -492 # if False, then f is entailed -493 with config(sat_backend="kissat"): -494 if not check_theory.solve(): -495 entailed.add(f) -496 children.discard(Or([~f])) -497 return entailed +324 phi = raw_fluent_factored[f_str] +325 print("\nfluent: " + f_str) +326 print("\npossible expl. for fluent being true:") +327 for f in phi["pos expl"]: +328 if f == top: +329 print("true") +330 elif f == bottom: +331 print("false") +332 else: +333 e.pprint(f) +334 print("\npossible expl. for fluent being false:") +335 for f in phi["neg expl"]: +336 if f == top: +337 print("true") +338 elif f == bottom: +339 print("false") +340 else: +341 e.pprint(f) +342 print("\npossible expl. for fluent being unaffected:") +343 for f in phi["neutral"]: +344 if f == top: +345 print("true") +346 elif f == bottom: +347 print("false") +348 else: +349 e.pprint(f) +350 print() +351 +352 """Steps 1. (a)-(c) and Step 2 of AS-STRIPS-SLAF are taken care of in this loop.""" +353 a = token.action +354 # ensures that the action is not None (happens on the last step of a trace) +355 if a: +356 # iterate through every fluent in the fluent-factored transition belief formula +357 for phi in raw_fluent_factored.values(): +358 f = phi["fluent"] +359 +360 # create action propositions +361 pos_precond = Var(f"({f} is a precondition of {a})") +362 neg_precond = Var(f"(~{f} is a precondition of {a})") +363 pos_effect = Var(f"({a} causes {f})") +364 neg_effect = Var(f"({a} causes ~{f})") +365 neutral = Var(f"({a} has no effect on {f})") +366 +367 all_var.update( +368 [pos_precond, neg_precond, pos_effect, neg_effect, neutral] +369 ) +370 +371 # update the fluent-factored formula +372 all_phi_pos = [p.simplify() for p in phi["pos expl"]] +373 all_phi_neg = [n.simplify() for n in phi["neg expl"]] +374 all_phi_neut = [n.simplify() for n in phi["neutral"]] +375 phi["pos expl"] = set() +376 phi["neg expl"] = set() +377 +378 """Steps 1 (a-c) - Update every fluent in the fluent-factored transition belief formula +379 with information from the last step.""" +380 +381 """Step 1 (a) - update the neutral effects.""" +382 phi["neutral"].update( +383 [(~pos_precond | p).simplify() for p in all_phi_pos] +384 ) +385 phi["neutral"].update( +386 [(~neg_precond | n).simplify() for n in all_phi_neg] +387 ) +388 +389 """Step 1 (b) - update the positive effects.""" +390 phi["pos expl"].add(pos_effect | neutral) +391 phi["pos expl"].add(pos_effect | ~neg_precond) +392 phi["pos expl"].update( +393 [(pos_effect | p).simplify() for p in all_phi_pos] +394 ) +395 +396 """Step 1 (c) - update the negative effects.""" +397 phi["neg expl"].add(neg_effect | neutral) +398 phi["neg expl"].add(neg_effect | ~pos_precond) +399 phi["neg expl"].update( +400 [(neg_effect | n).simplify() for n in all_phi_neg] +401 ) +402 +403 """add validity constraints (from section 5.2 of the SLAF paper).""" +404 validity_constraints.add(pos_effect | neg_effect | neutral) +405 validity_constraints.add((~pos_effect | ~neg_effect)) +406 validity_constraints.add(~neg_effect | ~neutral) +407 validity_constraints.add(~pos_effect | ~neutral) +408 validity_constraints.add(~pos_precond | ~neg_precond) +409 +410 """Step 2 - eliminate subsumed clauses in phi.""" +411 SLAF.__remove_subsumed_clauses(phi["pos expl"]) +412 SLAF.__remove_subsumed_clauses(phi["neg expl"]) +413 SLAF.__remove_subsumed_clauses(phi["neutral"]) +414 # display current updates +415 if debug_mode: +416 if a: +417 print("\nAction taken: " + str(a) + "\n") +418 for obj in to_obs: +419 f_str = raw_fluent_factored[obj]["fluent"].name +420 phi = raw_fluent_factored[f_str] +421 print("\nfluent: " + f_str) +422 print( +423 "\npossible expl. for fluent being true after " +424 + str(a) +425 + ":" +426 ) +427 for f in phi["pos expl"]: +428 if f == top: +429 print("true") +430 elif f == bottom: +431 print("false") +432 else: +433 e.pprint(f) +434 print( +435 "\npossible expl. for fluent being false after " +436 + str(a) +437 + ":" +438 ) +439 for f in phi["neg expl"]: +440 if f == top: +441 print("true") +442 elif f == bottom: +443 print("false") +444 else: +445 e.pprint(f) +446 print( +447 "\npossible expl. for fluent being unaffected after " +448 + str(a) +449 + ":" +450 ) +451 for f in phi["neutral"]: +452 if f == top: +453 print("true") +454 elif f == bottom: +455 print("false") +456 else: +457 e.pprint(f) +458 print() +459 user_input = input("Hit enter to continue.\n") +460 +461 formula = set() +462 """Convert to formula once you have stepped through all observations and applied all transformations. +463 NOTE: This would have to be refactored if the functionality for multiple traces was added, as each trace would +464 have to store its own separate formulas, and the conjunction would be taken at the end.""" +465 for phi in raw_fluent_factored.values(): +466 f = phi["fluent"] +467 # convert to formula for each fluent +468 all_phi_pos = [p.simplify() for p in phi["pos expl"]] +469 all_phi_neg = [n.simplify() for n in phi["neg expl"]] +470 all_phi_neut = [n.simplify() for n in phi["neutral"]] +471 formula.update([(~f | p).simplify() for p in all_phi_pos]) +472 formula.update([(f | n).simplify() for n in all_phi_neg]) +473 formula.update([n for n in all_phi_neut]) +474 # add the validity constraints +475 formula.update(validity_constraints) +476 # create CNF formula +477 full_formula = And({*[f.simplify() for f in formula]}).simplify() +478 cnf_formula = And(map(SLAF.__or_refactor, full_formula.children)) +479 +480 entailed = set() +481 if sample: +482 with config(sat_backend="kissat"): +483 sol = cnf_formula.solve() +484 if sol: +485 for f in all_var: +486 if sol[str(f)]: +487 entailed.add(f) +488 else: +489 children = set(cnf_formula.children) +490 # iterate through all fluents, gathering those that are entailed +491 for f in all_var: +492 children.add(Or([~f])) +493 check_theory = And(children) +494 # if False, then f is entailed +495 with config(sat_backend="kissat"): +496 if not check_theory.solve(): +497 entailed.add(f) +498 children.discard(Or([~f])) +499 return entailed