refine

Author: cutelimination

smtfuzz/bet/bet_mutator.py

@@ -17,7 +17,29 @@
 import random
 
 from z3 import *
-from z3.z3util import get_vars
+# from z3.z3util import get_vars  # this one is slow
+
+
+def get_vars(exp):
+    try:
+        syms = set()
+        stack = [exp]
+
+        while stack:
+            e = stack.pop()
+            if z3.is_app(e):
+                if e.num_args() == 0 and e.decl().kind() == z3.Z3_OP_UNINTERPRETED:
+                    syms.add(e)
+                else:
+                    # Add children in reverse order
+                    # This maintains DFS traversal order when using pop()
+                    # stack.extend(reversed(e.children())) # shoud we?
+                    stack.extend(e.children())
+
+        return list(syms)
+    except z3.Z3Exception as ex:
+        print(ex)
+        return False
 
 
 def get_atoms(z3expr):

smtfuzz/bet/op_mutator.py

@@ -1,9 +1,9 @@
 import random
 
-from smtfuzz.mutators.smt2_generator import generate_from_grammar_as_str
+from smtfuzz.bet.smt2_generator import generate_from_grammar_as_str
 
-from smtfuzz.mutators.cvc4option_mutator import mutate_cvc4_option
-from smtfuzz.mutators.z3option_mutator import mutate_z3_option
+from smtfuzz.options.cvc4option_mutator import mutate_cvc4_option
+from smtfuzz.options.z3option_mutator import mutate_z3_option
 
 # import timeout_decorator
 

smtfuzz/bet/smt2_generator.py

@@ -7,7 +7,7 @@
 currentdir = os.path.dirname(os.path.abspath(inspect.getfile(inspect.currentframe())))
 parentdir = os.path.dirname(currentdir)
 
-generator = 'smtfuzz'   # FIXME: directly use the smtfuzz.py file?
+generator = os.path.join(parentdir, 'smtfuzz.py')  # Fixed: use the actual smtfuzz.py file
 
 strategies = ['noinc', 'noinc', 'CNFexp', 'cnf', 'ncnf', 'bool', 'bool']
 

smtfuzz/cli.py

@@ -6,33 +6,12 @@
 """
 
 import sys
-from .smtfuzz import *
+from .smtfuzz import main
 
 
 def cli_main():
     """Entry point for the smtfuzz command."""
-    # Check if inter-theory mode is requested
-    if len(sys.argv) > 1 and sys.argv[1] == 'inter':
-        # Remove 'inter' from args and call inter-theory CLI
-        sys.argv = [sys.argv[0]] + sys.argv[2:]
-        from .inter.cli import main as inter_main
-        inter_main()
-    elif len(sys.argv) > 1 and sys.argv[1] == 'mutate':
-        # Remove 'mutate' from args and call mutation CLI
-        sys.argv = [sys.argv[0]] + sys.argv[2:]
-        from .bet.bet_mutator import main as mutate_main
-        mutate_main()
-    else:
-        # Default generation mode
-        print("SMTFuzz - A fuzzer for SMT solvers")
-        print("Modes: generation (default), mutate, inter")
-        main()
-
-
-def main():
-    """Main entry point for the package."""
-    cli_main()
-
+    main()
 
 if __name__ == '__main__':
     cli_main()