[solvers/symex] Add minimal symbolic execution engine

[copybara-service]

[solvers/symex] Add minimal symbolic execution engine

Implements a symbolic execution engine for XLS IR functions that systematically
discovers feasible execution paths through multiplexers and generates concrete
test vectors for each path.

Architecture:
Uses a clean, decoupled two-phase architecture:

1. Up-front IR Encoding (Z3EncodingVisitor):
   The entire function DAG is translated into Z3 ASTs in a single post-order
   pass up-front. By subclassing IrTranslator, all 50+ IR op translations
   (arithmetic, bitwise, tuples, bit-slices, comparisons) are reused directly.
   Multiplexers (Select, PrioritySelect) are intercepted and translated as
   unconstrained symbolic SSA variables rather than folded into monolithic
   nested ite(...) trees.

2. Incremental SMT Decision-Tree Traversal (SymExEngine):
   Path exploration operates as a depth-first search over multiplexer branch
   choices in topological order. At each branch, a solver frame is pushed
   (Z3_solver_push), the branch condition (C_k) and arm equality (V_mux == A_k)
   are asserted, and satisfiability is checked. Unsatisfiable branches are
   pruned immediately, backtracking early without exploring downstream nodes.

3. Leaf Test Generation:
   When a feasible leaf is reached, concrete satisfying parameter assignments
   are extracted from the solver model into a SymbolicPath.

Files:

• symex_engine.{h,cc}: Path exploration engine and solver orchestration.
• z3_encoding_visitor.{h,cc}: Subclass of IrTranslator providing free SSA mux
  variables and branch condition / arm equality encodings.
• z3_ir_translator.h: Moved context-borrowing constructor and NoteTranslation
  to protected, and added translations() const accessor to enable subclass
  extension.
• symbolic_path.{h,cc}: Data structures for paths, decisions, and tests.
• Tests:
  • symex_engine_test.cc: Path exploration, early pruning, and coverage.
  • z3_encoding_visitor_test.cc: Opcode, tuple, and mux translation.
  • symbolic_path_test.cc: Path condition and test vector accessors.
  • symex_e2e_test.cc: E2E ALU execution test with interpreter validation.