tpmmthomas / abc_fol Goto Github PK

a top-level interface from ABC that can just give yes/no answer about if the input theory is consistency. i.e. no need to run repairs.

Please add all the non-terminated input under a cutline so that we can investigate the reason and may come up with some useful heuristics if it is a general reason. Thanks.

------------------- Cutline 1 for input 1----------------------

put information such as conference specific instruction in a branch, keep the main clean for general purpose

• Change output file to json format

Find input theories that demonstrate the bugs

We discovered that the rules in PS would be checked in every round (even if other faults are not fully repaired), but sometimes when the other faults are fully repaired the rules in PS would be satisfied by then - worth discussing whether we need to check those rules every round or only at the end (when all other faults repaired)

To improve scalability and address the termination problem for some input theories,

• make analysis on the relation of the size of search space and variables and predicates in the theory (and the patterns of definition).
• Write a user guidance to help reduce the search space by modifying the input theory. Also, a FAQ to answer questions such as how many predicates are too many, and what kind of definition should be avoided to constrain the search space?