diff --git a/doc/quantifier_instantiation_callback.md b/doc/quantifier_instantiation_callback.md new file mode 100644 index 000000000..cb02ca40c --- /dev/null +++ b/doc/quantifier_instantiation_callback.md @@ -0,0 +1,293 @@ +# UserPropagator Quantifier Instantiation Callback in Z3 + +This document describes the UserPropagator callback for quantifier instantiations feature added in Z3 version 4.15.3. + +## Overview + +The quantifier instantiation callback allows user propagators to intercept and control quantifier instantiations. When Z3 attempts to instantiate a quantifier, the callback is invoked with the quantifier and its proposed instantiation. The callback can return `false` to discard the instantiation, providing fine-grained control over the quantifier instantiation process. + +This feature enables: +1. **Inspection and logging** of instantiation patterns +2. **Filtering** of undesired instantiations +3. **Custom instantiation strategies** +4. **Performance optimization** by delaying certain instantiations + +## API Reference + +### Python API + +```python +from z3 import * + +class MyUserPropagator(UserPropagateBase): + def __init__(self, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + # Register the quantifier instantiation callback + self.add_on_binding(self.my_callback) + + def my_callback(self, quantifier, instantiation): + """ + Callback for quantifier instantiation control. + + Args: + quantifier: The quantifier being instantiated (Z3 AST) + instantiation: The proposed instantiation (Z3 AST) + + Returns: + bool: True to allow the instantiation, False to discard it + """ + # Your logic here + return True # or False to block + + # Required methods + def push(self): pass + def pop(self, num_scopes): pass + def fresh(self, new_ctx): return MyUserPropagator(ctx=new_ctx) +``` + +### C API + +```c +#include + +// Callback function signature +Z3_bool my_callback(void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst) { + // ctx: user context data + // cb: solver callback handle (internal use) + // q: quantifier being instantiated + // inst: proposed instantiation + + // Your logic here + return Z3_TRUE; // or Z3_FALSE to block +} + +// Register the callback +Z3_context ctx = Z3_mk_context(Z3_mk_config()); +Z3_solver s = Z3_mk_solver(ctx); +Z3_solver_propagate_on_binding(ctx, s, my_callback); +``` + +### C++ API + +The C++ API follows the same pattern as the C API, using the same `Z3_solver_propagate_on_binding` function. + +## Examples + +### Basic Example: Limiting Instantiations + +```python +class InstantiationLimiter(UserPropagateBase): + def __init__(self, max_instantiations=5, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + self.max_instantiations = max_instantiations + self.count = 0 + self.add_on_binding(self.limit_instantiations) + + def limit_instantiations(self, quantifier, instantiation): + self.count += 1 + print(f"Instantiation #{self.count}: {instantiation}") + + # Allow only the first max_instantiations + if self.count <= self.max_instantiations: + print(" -> ALLOWED") + return True + else: + print(" -> BLOCKED") + return False + + def push(self): pass + def pop(self, num_scopes): pass + def fresh(self, new_ctx): return InstantiationLimiter(self.max_instantiations, ctx=new_ctx) + +# Usage +s = Solver() +limiter = InstantiationLimiter(max_instantiations=3, s=s) + +x = Int('x') +f = Function('f', IntSort(), IntSort()) +s.add(ForAll([x], f(x) >= 0)) +s.add(f(1) < 10, f(2) < 20, f(3) < 30) + +result = s.check() +``` + +### Advanced Example: Pattern-Based Filtering + +```python +class PatternFilter(UserPropagateBase): + def __init__(self, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + self.pattern_counts = {} + self.max_per_pattern = 2 + self.add_on_binding(self.filter_by_pattern) + + def filter_by_pattern(self, quantifier, instantiation): + # Convert to string for pattern matching + pattern = str(instantiation) + + # Count occurrences of this pattern + self.pattern_counts[pattern] = self.pattern_counts.get(pattern, 0) + 1 + count = self.pattern_counts[pattern] + + # Allow only max_per_pattern instantiations of each pattern + allow = count <= self.max_per_pattern + + print(f"Pattern: {pattern} (#{count}) -> {'ALLOWED' if allow else 'BLOCKED'}") + return allow + + def push(self): pass + def pop(self, num_scopes): pass + def fresh(self, new_ctx): return PatternFilter(ctx=new_ctx) +``` + +### Logging Example: Analyzing Instantiation Patterns + +```python +class InstantiationLogger(UserPropagateBase): + def __init__(self, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + self.log = [] + self.add_on_binding(self.log_instantiation) + + def log_instantiation(self, quantifier, instantiation): + entry = { + 'quantifier': str(quantifier), + 'instantiation': str(instantiation), + 'count': len(self.log) + 1 + } + self.log.append(entry) + + print(f"#{entry['count']}: {entry['instantiation']}") + + # Allow all instantiations (just log them) + return True + + def get_statistics(self): + # Group by quantifier + by_quantifier = {} + for entry in self.log: + q = entry['quantifier'] + if q not in by_quantifier: + by_quantifier[q] = [] + by_quantifier[q].append(entry['instantiation']) + + return { + 'total': len(self.log), + 'by_quantifier': by_quantifier + } + + def push(self): pass + def pop(self, num_scopes): pass + def fresh(self, new_ctx): return InstantiationLogger(ctx=new_ctx) +``` + +## Use Cases + +### 1. Performance Optimization +- **Problem**: Some quantifier instantiations are expensive but rarely useful +- **Solution**: Use callback to block certain patterns or limit instantiation count +- **Benefit**: Reduced solving time, better resource utilization + +### 2. Custom Instantiation Strategies +- **Problem**: Default instantiation heuristics don't work well for your domain +- **Solution**: Implement domain-specific filtering logic +- **Benefit**: Better solution quality, faster convergence + +### 3. Debugging and Analysis +- **Problem**: Understanding why a formula is UNSAT or takes long to solve +- **Solution**: Log all instantiation attempts to analyze patterns +- **Benefit**: Better insight into solver behavior + +### 4. Interactive Solving +- **Problem**: Need to control solving process interactively +- **Solution**: Use callback to selectively enable/disable instantiations +- **Benefit**: Fine-grained control over solver behavior + +## Technical Details + +### Callback Invocation +- Called **before** the instantiation is added to the solver +- Blocking an instantiation prevents it from being used in the current search +- The same instantiation may be proposed again in different search branches + +### Return Value Semantics +- `True` (Python) / `Z3_TRUE` (C): Allow the instantiation +- `False` (Python) / `Z3_FALSE` (C): Block the instantiation +- Blocked instantiations are discarded and won't be used in current search + +### Thread Safety +- Callbacks are invoked on the same thread as the solver +- No additional synchronization is needed +- Context switching during callback execution is safe + +### Performance Considerations +- Callbacks are invoked frequently during solving +- Keep callback logic lightweight to avoid performance overhead +- String conversions (`str(ast)`) can be expensive; cache when possible +- Consider using AST structure inspection instead of string matching + +## Limitations + +### C/C++ API Limitations +- The C/C++ callback receives AST handles but no direct Z3 context +- Converting ASTs to strings for inspection requires careful context management +- Recommend using Python API for complex logic, C/C++ for simple filtering + +### Scope and Lifetime +- Callback registrations are tied to solver instances +- User propagator instances must remain alive during solving +- AST handles in callbacks are valid only during callback execution + +### Interaction with Other Features +- Works with all quantifier instantiation strategies (E-matching, MBQI, etc.) +- Compatible with other user propagator callbacks +- May affect solver completeness if too many instantiations are blocked + +## Best Practices + +1. **Start Simple**: Begin with logging to understand instantiation patterns +2. **Be Conservative**: Blocking too many instantiations can make formulas unsolvable +3. **Test Thoroughly**: Verify that your filtering doesn't break correctness +4. **Profile Performance**: Measure impact of callback overhead +5. **Use Appropriate Data Structures**: Hash maps for pattern counting, etc. +6. **Handle Edge Cases**: Empty instantiations, malformed ASTs, etc. + +## Complete Working Example + +See the accompanying files: +- `examples/python/quantifier_instantiation_callback.py` - Complete Python examples +- `examples/c++/quantifier_instantiation_callback.cpp` - C++ examples +- `examples/c/quantifier_instantiation_callback.c` - C examples + +These examples demonstrate all the concepts above with runnable code. + +## Troubleshooting + +### Common Issues + +1. **Callback Not Called** + - Ensure user propagator is properly registered with solver + - Check that problem actually triggers quantifier instantiations + - Verify quantifier syntax is correct + +2. **Performance Degradation** + - Simplify callback logic + - Avoid expensive string operations + - Consider sampling (only process every Nth callback) + +3. **Unexpected UNSAT Results** + - Review blocking criteria - may be too aggressive + - Test with callback disabled to verify baseline behavior + - Use logging to understand what's being blocked + +4. **Memory Issues** + - Don't store AST handles beyond callback lifetime + - Clear large data structures periodically + - Monitor memory usage in long-running processes + +## Version History + +- **Z3 4.15.3**: Initial implementation of quantifier instantiation callbacks +- **Z3 4.15.4**: Improved performance and stability + +For more information, see the Z3 documentation and source code in the Z3Prover repository. \ No newline at end of file diff --git a/examples/README_quantifier_callbacks.md b/examples/README_quantifier_callbacks.md new file mode 100644 index 000000000..794b63e27 --- /dev/null +++ b/examples/README_quantifier_callbacks.md @@ -0,0 +1,161 @@ +# UserPropagator Quantifier Instantiation Callback Examples + +This directory contains examples demonstrating the UserPropagator callback for quantifier instantiations feature added in Z3 version 4.15.3. + +## Overview + +The quantifier instantiation callback allows user propagators to intercept and control quantifier instantiations, providing fine-grained control over the solving process. + +## Files + +### Python Examples +- `examples/python/quantifier_instantiation_callback.py` - Comprehensive Python examples showing: + - Basic instantiation control (limiting number of instantiations) + - Advanced pattern-based filtering + - Instantiation logging and analysis + +### C++ Examples +- `examples/c++/quantifier_instantiation_callback.cpp` - C++ API examples (requires compilation) + +### C Examples +- `examples/c/quantifier_instantiation_callback.c` - C API examples (requires compilation) + +### Unit Tests +- `src/test/test_quantifier_instantiation_callback.py` - Unit tests validating functionality + +### Documentation +- `doc/quantifier_instantiation_callback.md` - Complete API documentation and usage guide + +## Running the Examples + +### Python Examples + +```bash +cd build/python +PYTHONPATH=/path/to/z3/build/python python3 ../../examples/python/quantifier_instantiation_callback.py +``` + +Or from the Z3 build directory: +```bash +cd build/python +python3 ../../examples/python/quantifier_instantiation_callback.py +``` + +### C++ Examples + +```bash +# Compile +g++ -I src/api -I src/api/c++ examples/c++/quantifier_instantiation_callback.cpp -L build -lz3 -o quantifier_callback_cpp + +# Run +LD_LIBRARY_PATH=build ./quantifier_callback_cpp +``` + +### C Examples + +```bash +# Compile +gcc -I src/api examples/c/quantifier_instantiation_callback.c -L build -lz3 -o quantifier_callback_c + +# Run +LD_LIBRARY_PATH=build ./quantifier_callback_c +``` + +### Unit Tests + +```bash +cd z3-root-directory +PYTHONPATH=build/python python3 src/test/test_quantifier_instantiation_callback.py +``` + +## Expected Output + +When running the Python examples, you should see output like: + +``` +============================================================ +BASIC QUANTIFIER INSTANTIATION CONTROL EXAMPLE +============================================================ +Checking satisfiability with instantiation control... +Instantiation #1: + Quantifier: ForAll(x, f(x) >= 0) + Instantiation: f(1) >= 0 + -> ALLOWED (#1) + +Instantiation #2: + Quantifier: ForAll(x, f(x) >= 0) + Instantiation: f(2) >= 0 + -> ALLOWED (#2) + +Instantiation #3: + Quantifier: ForAll(x, f(x) >= 0) + Instantiation: f(3) >= 0 + -> ALLOWED (#3) + +Result: sat +Model: [c = 3, b = 2, a = 1, f = [else -> 0]] + +Instantiation Statistics: + Total attempts: 3 + Allowed: 3 + Blocked: 0 +``` + +## Key Features Demonstrated + +1. **Basic Control**: Limiting the number of quantifier instantiations +2. **Pattern Filtering**: Allowing only a certain number of instantiations per pattern +3. **Logging**: Recording all instantiation attempts for analysis +4. **Performance Impact**: Showing how filtering affects solving time +5. **Error Handling**: Graceful handling of callback exceptions + +## Use Cases + +- **Performance Optimization**: Reduce solving time by limiting expensive instantiations +- **Custom Strategies**: Implement domain-specific instantiation heuristics +- **Debugging**: Understand solver behavior through instantiation analysis +- **Interactive Solving**: Dynamically control solving process + +## Requirements + +- Z3 version 4.15.3 or later +- Python 3.x for Python examples +- GCC/Clang for C/C++ examples +- Z3 shared library in LD_LIBRARY_PATH + +## Troubleshooting + +### "ModuleNotFoundError: No module named 'z3'" +Set PYTHONPATH to point to the Z3 Python bindings: +```bash +export PYTHONPATH=/path/to/z3/build/python:$PYTHONPATH +``` + +### "No instantiations were attempted" +- Check that your formula contains quantifiers +- Verify that the constraints actually trigger instantiation (e.g., through function applications) +- Try disabling other Z3 optimizations that might eliminate the need for instantiation + +### C/C++ Compilation Errors +- Ensure Z3 headers are in the include path (`-I /path/to/z3/src/api`) +- Link against the Z3 library (`-L /path/to/z3/build -lz3`) +- Set LD_LIBRARY_PATH to find the shared library at runtime + +### Performance Issues +- Keep callback logic simple and fast +- Avoid expensive string operations in callbacks +- Consider sampling (only process every Nth callback) for high-frequency instantiations + +## Further Reading + +- See `doc/quantifier_instantiation_callback.md` for complete API documentation +- Z3 Guide: https://microsoft.github.io/z3guide/ +- Z3 API Reference: https://z3prover.github.io/api/html/ + +## Contributing + +To add new examples or improve existing ones: +1. Follow the existing code style and structure +2. Add appropriate error handling and documentation +3. Include unit tests for new functionality +4. Update this README with any new examples \ No newline at end of file diff --git a/examples/c++/quantifier_instantiation_callback.cpp b/examples/c++/quantifier_instantiation_callback.cpp new file mode 100644 index 000000000..21eb991a0 --- /dev/null +++ b/examples/c++/quantifier_instantiation_callback.cpp @@ -0,0 +1,312 @@ +/** + * Example demonstrating the UserPropagator callback for quantifier instantiations in Z3. + * + * This feature was added in Z3 version 4.15.3 and allows user propagators to intercept + * and control quantifier instantiations using the Z3_solver_propagate_on_binding API. + * + * The callback receives the quantifier and its proposed instantiation, and can return + * false to discard the instantiation, providing fine-grained control over the + * quantifier instantiation process. + * + * To compile: + * g++ -I /path/to/z3/src/api -I /path/to/z3/src/api/c++ \ + * quantifier_instantiation_callback.cpp -L /path/to/z3/build -lz3 \ + * -o quantifier_instantiation_callback + * + * To run: + * LD_LIBRARY_PATH=/path/to/z3/build ./quantifier_instantiation_callback + */ + +#include +#include +#include +#include + +using namespace z3; +using namespace std; + +// Global counter for demonstration purposes +static int instantiation_counter = 0; +static int allowed_counter = 0; +static int blocked_counter = 0; + +/** + * User-defined callback for quantifier instantiation control. + * + * This function is called by Z3 whenever it wants to instantiate a quantifier. + * + * @param ctx User context (can be used to pass custom data) + * @param cb Solver callback object + * @param q The quantifier being instantiated + * @param inst The proposed instantiation + * @return true to allow the instantiation, false to discard it + */ +bool quantifier_instantiation_callback(void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst) { + // Cast the context back to our custom data structure if needed + // For this simple example, we'll use global variables + + instantiation_counter++; + + // Get string representations for logging + Z3_context z3_ctx = Z3_solver_callback_get_context(cb); + string q_str = Z3_ast_to_string(z3_ctx, q); + string inst_str = Z3_ast_to_string(z3_ctx, inst); + + cout << "Instantiation #" << instantiation_counter << ":" << endl; + cout << " Quantifier: " << q_str << endl; + cout << " Instantiation: " << inst_str << endl; + + // Example filtering logic: allow only the first 3 instantiations + // In practice, you might implement more sophisticated filtering + bool allow = instantiation_counter <= 3; + + if (allow) { + allowed_counter++; + cout << " -> ALLOWED (#" << allowed_counter << ")" << endl; + } else { + blocked_counter++; + cout << " -> BLOCKED (#" << blocked_counter << ")" << endl; + } + + cout << endl; + return allow; +} + +/** + * Example demonstrating basic quantifier instantiation control. + */ +void example_basic_control() { + cout << string(60, '=') << endl; + cout << "BASIC QUANTIFIER INSTANTIATION CONTROL EXAMPLE" << endl; + cout << string(60, '=') << endl; + + context ctx; + solver s(ctx); + + // Register the quantifier instantiation callback + Z3_solver_propagate_on_binding(ctx, s, quantifier_instantiation_callback); + + // Create a simple quantified formula + sort int_sort = ctx.int_sort(); + func_decl f = ctx.function("f", int_sort, int_sort); + expr x = ctx.int_const("x"); + + // Add quantified axiom: forall x. f(x) >= 0 + expr axiom = forall(x, f(x) >= 0); + s.add(axiom); + + // Add constraints that might trigger instantiations + expr a = ctx.int_const("a"); + expr b = ctx.int_const("b"); + expr c = ctx.int_const("c"); + + s.add(f(a) < 10); + s.add(f(b) < 20); + s.add(f(c) < 30); + + // Add specific values + s.add(a == 1); + s.add(b == 2); + s.add(c == 3); + + cout << "Checking satisfiability with instantiation control..." << endl; + check_result result = s.check(); + cout << "Result: " << result << endl; + + if (result == sat) { + cout << "Model: " << s.get_model() << endl; + } + + // Print statistics + cout << endl << "Instantiation Statistics:" << endl; + cout << " Total attempts: " << instantiation_counter << endl; + cout << " Allowed: " << allowed_counter << endl; + cout << " Blocked: " << blocked_counter << endl; +} + +// Structure to hold callback context data +struct AdvancedCallbackContext { + int max_instantiations_per_pattern; + map instantiation_counts; + + AdvancedCallbackContext(int max_per_pattern = 2) + : max_instantiations_per_pattern(max_per_pattern) {} +}; + +/** + * Advanced callback that tracks instantiation patterns. + */ +bool advanced_instantiation_callback(void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst) { + AdvancedCallbackContext* context = static_cast(ctx); + + // Get string representation of the instantiation + Z3_context z3_ctx = Z3_solver_callback_get_context(cb); + string inst_str = Z3_ast_to_string(z3_ctx, inst); + + // Count instantiations for this pattern + context->instantiation_counts[inst_str]++; + int count = context->instantiation_counts[inst_str]; + + // Allow only up to max_instantiations_per_pattern of the same pattern + bool allow = count <= context->max_instantiations_per_pattern; + + cout << "Instantiation: " << inst_str << " (attempt #" << count << ")" << endl; + cout << " -> " << (allow ? "ALLOWED" : "BLOCKED") << endl; + + return allow; +} + +/** + * Example demonstrating advanced instantiation filtering. + */ +void example_advanced_filtering() { + cout << endl << string(60, '=') << endl; + cout << "ADVANCED INSTANTIATION FILTERING EXAMPLE" << endl; + cout << string(60, '=') << endl; + + context ctx; + solver s(ctx); + + // Create callback context + AdvancedCallbackContext callback_ctx(2); // Allow max 2 instantiations per pattern + + // Register the advanced callback + Z3_solver_propagate_on_binding(ctx, s, advanced_instantiation_callback); + + // Store callback context in solver (this is a simplified approach) + // In practice, you might need a more sophisticated context management system + + // Create a more complex scenario + sort int_sort = ctx.int_sort(); + sort bool_sort = ctx.bool_sort(); + func_decl P = ctx.function("P", int_sort, int_sort, bool_sort); + + expr x = ctx.int_const("x"); + expr y = ctx.int_const("y"); + + // Add quantified formula: forall x, y. P(x, y) => P(y, x) + expr axiom = forall(x, y, implies(P(x, y), P(y, x))); + s.add(axiom); + + // Add facts that will trigger instantiations + expr a = ctx.int_const("a"); + expr b = ctx.int_const("b"); + expr c = ctx.int_const("c"); + + s.add(P(a, b)); + s.add(P(b, c)); + s.add(P(c, a)); + + cout << "Checking satisfiability with advanced filtering..." << endl; + check_result result = s.check(); + cout << "Result: " << result << endl; + + if (result == sat) { + cout << "Model: " << s.get_model() << endl; + } + + // Print pattern statistics + cout << endl << "Instantiation Pattern Statistics:" << endl; + for (const auto& pair : callback_ctx.instantiation_counts) { + cout << " " << pair.first << ": " << pair.second << " attempts" << endl; + } +} + +/** + * Simple callback that logs all instantiations without blocking any. + */ +bool logging_callback(void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst) { + vector>* log = static_cast>*>(ctx); + + Z3_context z3_ctx = Z3_solver_callback_get_context(cb); + string q_str = Z3_ast_to_string(z3_ctx, q); + string inst_str = Z3_ast_to_string(z3_ctx, inst); + + log->push_back(make_pair(q_str, inst_str)); + + cout << "Logged instantiation #" << log->size() << ":" << endl; + cout << " Quantifier: " << q_str << endl; + cout << " Instantiation: " << inst_str << endl; + + // Allow all instantiations for logging purposes + return true; +} + +/** + * Example focused on logging instantiation patterns. + */ +void example_logging() { + cout << endl << string(60, '=') << endl; + cout << "INSTANTIATION LOGGING EXAMPLE" << endl; + cout << string(60, '=') << endl; + + context ctx; + solver s(ctx); + + // Create log storage + vector> instantiation_log; + + // Register logging callback + Z3_solver_propagate_on_binding(ctx, s, logging_callback); + + // Create scenario with multiple quantifiers + sort int_sort = ctx.int_sort(); + func_decl f = ctx.function("f", int_sort, int_sort); + func_decl g = ctx.function("g", int_sort, int_sort); + + expr x = ctx.int_const("x"); + + // Add multiple quantified axioms + s.add(forall(x, f(x) >= x)); // f(x) is at least x + s.add(forall(x, g(x) <= x)); // g(x) is at most x + + // Add constraints to trigger instantiations + expr a = ctx.int_const("a"); + expr b = ctx.int_const("b"); + + s.add(f(a) < 5); + s.add(g(b) > 10); + s.add(a == 2); + s.add(b == 8); + + cout << "Solving with full logging enabled..." << endl; + check_result result = s.check(); + cout << "Result: " << result << endl; + + // Analyze logged patterns + cout << endl << "Instantiation Analysis:" << endl; + cout << "Total instantiations logged: " << instantiation_log.size() << endl; + + // Group by quantifier + map> by_quantifier; + for (const auto& entry : instantiation_log) { + by_quantifier[entry.first].push_back(entry.second); + } + + for (const auto& pair : by_quantifier) { + cout << endl << "Quantifier: " << pair.first << endl; + cout << " Instantiations (" << pair.second.size() << "):" << endl; + for (size_t i = 0; i < pair.second.size(); ++i) { + cout << " " << (i + 1) << ". " << pair.second[i] << endl; + } + } +} + +int main() { + try { + // Run all examples + example_basic_control(); + example_advanced_filtering(); + example_logging(); + + cout << endl << string(60, '=') << endl; + cout << "All examples completed successfully!" << endl; + cout << string(60, '=') << endl; + + } catch (exception& e) { + cout << "Exception: " << e.what() << endl; + return 1; + } + + return 0; +} \ No newline at end of file diff --git a/examples/c/quantifier_instantiation_callback.c b/examples/c/quantifier_instantiation_callback.c new file mode 100644 index 000000000..5ae8019c0 --- /dev/null +++ b/examples/c/quantifier_instantiation_callback.c @@ -0,0 +1,360 @@ +/** + * Example demonstrating the UserPropagator callback for quantifier instantiations in Z3 C API. + * + * This feature was added in Z3 version 4.15.3 and allows user propagators to intercept + * and control quantifier instantiations using the Z3_solver_propagate_on_binding API. + * + * The callback receives the quantifier and its proposed instantiation, and can return + * Z3_FALSE to discard the instantiation, providing fine-grained control over the + * quantifier instantiation process. + * + * To compile: + * gcc -I /path/to/z3/src/api quantifier_instantiation_callback.c \ + * -L /path/to/z3/build -lz3 -o quantifier_instantiation_callback + * + * To run: + * LD_LIBRARY_PATH=/path/to/z3/build ./quantifier_instantiation_callback + */ + +#include +#include +#include +#include + +// Global counters for demonstration +static int instantiation_counter = 0; +static int allowed_counter = 0; +static int blocked_counter = 0; + +/** + * User-defined callback for quantifier instantiation control. + * + * This function is called by Z3 whenever it wants to instantiate a quantifier. + * + * @param ctx User context (can be used to pass custom data) + * @param cb Solver callback object + * @param q The quantifier being instantiated + * @param inst The proposed instantiation + * @return Z3_TRUE to allow the instantiation, Z3_FALSE to discard it + */ +Z3_bool quantifier_instantiation_callback(void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst) { + // Get the Z3 context from the callback + Z3_context z3_ctx = Z3_solver_callback_get_context(cb); + + instantiation_counter++; + + // Get string representations for logging + Z3_string q_str = Z3_ast_to_string(z3_ctx, q); + Z3_string inst_str = Z3_ast_to_string(z3_ctx, inst); + + printf("Instantiation #%d:\n", instantiation_counter); + printf(" Quantifier: %s\n", q_str); + printf(" Instantiation: %s\n", inst_str); + + // Example filtering logic: allow only the first 3 instantiations + // In practice, you might implement more sophisticated filtering + Z3_bool allow = (instantiation_counter <= 3) ? Z3_TRUE : Z3_FALSE; + + if (allow) { + allowed_counter++; + printf(" -> ALLOWED (#%d)\n", allowed_counter); + } else { + blocked_counter++; + printf(" -> BLOCKED (#%d)\n", blocked_counter); + } + + printf("\n"); + return allow; +} + +/** + * Example demonstrating basic quantifier instantiation control. + */ +void example_basic_control() { + printf("============================================================\n"); + printf("BASIC QUANTIFIER INSTANTIATION CONTROL EXAMPLE\n"); + printf("============================================================\n"); + + // Create Z3 context and solver + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + Z3_solver s = Z3_mk_solver(ctx); + Z3_solver_inc_ref(ctx, s); + + // Register the quantifier instantiation callback + Z3_solver_propagate_on_binding(ctx, s, quantifier_instantiation_callback); + + // Create sorts and symbols + Z3_sort int_sort = Z3_mk_int_sort(ctx); + Z3_symbol f_name = Z3_mk_string_symbol(ctx, "f"); + Z3_symbol x_name = Z3_mk_string_symbol(ctx, "x"); + + // Create function declaration f: Int -> Int + Z3_func_decl f = Z3_mk_func_decl(ctx, f_name, 1, &int_sort, int_sort); + + // Create variables + Z3_ast x = Z3_mk_bound(ctx, 0, int_sort); + Z3_ast f_x = Z3_mk_app(ctx, f, 1, &x); + + // Create axiom: forall x. f(x) >= 0 + Z3_ast zero = Z3_mk_int(ctx, 0, int_sort); + Z3_ast f_x_geq_0 = Z3_mk_ge(ctx, f_x, zero); + + Z3_ast axiom = Z3_mk_forall_const(ctx, 0, 1, &x, 0, NULL, f_x_geq_0); + Z3_solver_assert(ctx, s, axiom); + + // Create constants and add constraints + Z3_symbol a_name = Z3_mk_string_symbol(ctx, "a"); + Z3_symbol b_name = Z3_mk_string_symbol(ctx, "b"); + Z3_symbol c_name = Z3_mk_string_symbol(ctx, "c"); + + Z3_ast a = Z3_mk_const(ctx, a_name, int_sort); + Z3_ast b = Z3_mk_const(ctx, b_name, int_sort); + Z3_ast c = Z3_mk_const(ctx, c_name, int_sort); + + // Add constraints that might trigger instantiations + Z3_ast f_a = Z3_mk_app(ctx, f, 1, &a); + Z3_ast f_b = Z3_mk_app(ctx, f, 1, &b); + Z3_ast f_c = Z3_mk_app(ctx, f, 1, &c); + + Z3_ast ten = Z3_mk_int(ctx, 10, int_sort); + Z3_ast twenty = Z3_mk_int(ctx, 20, int_sort); + Z3_ast thirty = Z3_mk_int(ctx, 30, int_sort); + + Z3_solver_assert(ctx, s, Z3_mk_lt(ctx, f_a, ten)); + Z3_solver_assert(ctx, s, Z3_mk_lt(ctx, f_b, twenty)); + Z3_solver_assert(ctx, s, Z3_mk_lt(ctx, f_c, thirty)); + + // Add specific values + Z3_ast one = Z3_mk_int(ctx, 1, int_sort); + Z3_ast two = Z3_mk_int(ctx, 2, int_sort); + Z3_ast three = Z3_mk_int(ctx, 3, int_sort); + + Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, a, one)); + Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, b, two)); + Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, c, three)); + + printf("Checking satisfiability with instantiation control...\n"); + Z3_lbool result = Z3_solver_check(ctx, s); + + switch (result) { + case Z3_L_TRUE: + printf("Result: SAT\n"); + { + Z3_model model = Z3_solver_get_model(ctx, s); + if (model) { + Z3_model_inc_ref(ctx, model); + printf("Model: %s\n", Z3_model_to_string(ctx, model)); + Z3_model_dec_ref(ctx, model); + } + } + break; + case Z3_L_FALSE: + printf("Result: UNSAT\n"); + break; + case Z3_L_UNDEF: + printf("Result: UNKNOWN\n"); + break; + } + + // Print statistics + printf("\nInstantiation Statistics:\n"); + printf(" Total attempts: %d\n", instantiation_counter); + printf(" Allowed: %d\n", allowed_counter); + printf(" Blocked: %d\n", blocked_counter); + + // Cleanup + Z3_solver_dec_ref(ctx, s); + Z3_del_context(ctx); +} + +// Structure for advanced callback context +typedef struct { + int max_instantiations_per_pattern; + char** patterns; + int* counts; + int num_patterns; + int capacity; +} AdvancedCallbackContext; + +/** + * Find or add a pattern in the context. + */ +int find_or_add_pattern(AdvancedCallbackContext* context, const char* pattern) { + // Look for existing pattern + for (int i = 0; i < context->num_patterns; i++) { + if (strcmp(context->patterns[i], pattern) == 0) { + return i; + } + } + + // Add new pattern if space available + if (context->num_patterns < context->capacity) { + int index = context->num_patterns++; + context->patterns[index] = malloc(strlen(pattern) + 1); + strcpy(context->patterns[index], pattern); + context->counts[index] = 0; + return index; + } + + return -1; // No space +} + +/** + * Advanced callback that tracks instantiation patterns. + */ +Z3_bool advanced_instantiation_callback(void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst) { + AdvancedCallbackContext* context = (AdvancedCallbackContext*)ctx; + + // Get string representation of the instantiation + Z3_context z3_ctx = Z3_solver_callback_get_context(cb); + Z3_string inst_str = Z3_ast_to_string(z3_ctx, inst); + + // Find or add this pattern + int pattern_index = find_or_add_pattern(context, inst_str); + if (pattern_index == -1) { + printf("Warning: Pattern storage full, allowing instantiation\n"); + return Z3_TRUE; + } + + // Increment count for this pattern + context->counts[pattern_index]++; + int count = context->counts[pattern_index]; + + // Allow only up to max_instantiations_per_pattern of the same pattern + Z3_bool allow = (count <= context->max_instantiations_per_pattern) ? Z3_TRUE : Z3_FALSE; + + printf("Instantiation: %s (attempt #%d)\n", inst_str, count); + printf(" -> %s\n", allow ? "ALLOWED" : "BLOCKED"); + + return allow; +} + +/** + * Example demonstrating advanced instantiation filtering. + */ +void example_advanced_filtering() { + printf("\n============================================================\n"); + printf("ADVANCED INSTANTIATION FILTERING EXAMPLE\n"); + printf("============================================================\n"); + + // Create callback context + AdvancedCallbackContext context; + context.max_instantiations_per_pattern = 2; + context.capacity = 100; + context.num_patterns = 0; + context.patterns = malloc(context.capacity * sizeof(char*)); + context.counts = malloc(context.capacity * sizeof(int)); + + // Create Z3 context and solver + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + Z3_solver s = Z3_mk_solver(ctx); + Z3_solver_inc_ref(ctx, s); + + // Register the advanced callback with context + Z3_solver_propagate_on_binding(ctx, s, advanced_instantiation_callback); + + // Create sorts and function declaration + Z3_sort int_sort = Z3_mk_int_sort(ctx); + Z3_sort bool_sort = Z3_mk_bool_sort(ctx); + Z3_sort P_domain[2] = {int_sort, int_sort}; + + Z3_symbol P_name = Z3_mk_string_symbol(ctx, "P"); + Z3_func_decl P = Z3_mk_func_decl(ctx, P_name, 2, P_domain, bool_sort); + + // Create bound variables for quantifier + Z3_ast x = Z3_mk_bound(ctx, 1, int_sort); // Note: index 1 for second variable in binding order + Z3_ast y = Z3_mk_bound(ctx, 0, int_sort); // Note: index 0 for first variable in binding order + + // Create P(x, y) and P(y, x) + Z3_ast xy_args[2] = {x, y}; + Z3_ast yx_args[2] = {y, x}; + Z3_ast P_xy = Z3_mk_app(ctx, P, 2, xy_args); + Z3_ast P_yx = Z3_mk_app(ctx, P, 2, yx_args); + + // Create implication: P(x, y) => P(y, x) + Z3_ast implication = Z3_mk_implies(ctx, P_xy, P_yx); + + // Create quantified formula: forall x, y. P(x, y) => P(y, x) + Z3_ast vars[2] = {x, y}; + Z3_ast axiom = Z3_mk_forall_const(ctx, 0, 2, vars, 0, NULL, implication); + Z3_solver_assert(ctx, s, axiom); + + // Create constants + Z3_symbol a_name = Z3_mk_string_symbol(ctx, "a"); + Z3_symbol b_name = Z3_mk_string_symbol(ctx, "b"); + Z3_symbol c_name = Z3_mk_string_symbol(ctx, "c"); + + Z3_ast a = Z3_mk_const(ctx, a_name, int_sort); + Z3_ast b = Z3_mk_const(ctx, b_name, int_sort); + Z3_ast c = Z3_mk_const(ctx, c_name, int_sort); + + // Add facts that will trigger instantiations + Z3_ast ab_args[2] = {a, b}; + Z3_ast bc_args[2] = {b, c}; + Z3_ast ca_args[2] = {c, a}; + + Z3_solver_assert(ctx, s, Z3_mk_app(ctx, P, 2, ab_args)); + Z3_solver_assert(ctx, s, Z3_mk_app(ctx, P, 2, bc_args)); + Z3_solver_assert(ctx, s, Z3_mk_app(ctx, P, 2, ca_args)); + + printf("Checking satisfiability with advanced filtering...\n"); + Z3_lbool result = Z3_solver_check(ctx, s); + + switch (result) { + case Z3_L_TRUE: + printf("Result: SAT\n"); + { + Z3_model model = Z3_solver_get_model(ctx, s); + if (model) { + Z3_model_inc_ref(ctx, model); + printf("Model: %s\n", Z3_model_to_string(ctx, model)); + Z3_model_dec_ref(ctx, model); + } + } + break; + case Z3_L_FALSE: + printf("Result: UNSAT\n"); + break; + case Z3_L_UNDEF: + printf("Result: UNKNOWN\n"); + break; + } + + // Print pattern statistics + printf("\nInstantiation Pattern Statistics:\n"); + for (int i = 0; i < context.num_patterns; i++) { + printf(" %s: %d attempts\n", context.patterns[i], context.counts[i]); + } + + // Cleanup context + for (int i = 0; i < context.num_patterns; i++) { + free(context.patterns[i]); + } + free(context.patterns); + free(context.counts); + + // Cleanup Z3 objects + Z3_solver_dec_ref(ctx, s); + Z3_del_context(ctx); +} + +int main() { + printf("Z3 Quantifier Instantiation Callback Examples\n"); + printf("==============================================\n\n"); + + // Run examples + example_basic_control(); + example_advanced_filtering(); + + printf("\n============================================================\n"); + printf("All examples completed successfully!\n"); + printf("============================================================\n"); + + return 0; +} \ No newline at end of file diff --git a/examples/python/quantifier_instantiation_callback.py b/examples/python/quantifier_instantiation_callback.py new file mode 100644 index 000000000..c80bf62b4 --- /dev/null +++ b/examples/python/quantifier_instantiation_callback.py @@ -0,0 +1,306 @@ +#!/usr/bin/env python3 +""" +Example demonstrating the UserPropagator callback for quantifier instantiations in Z3. + +This feature was added in Z3 version 4.15.3 and allows user propagators to intercept +and control quantifier instantiations. The callback receives the quantifier and its +proposed instantiation, and can return False to discard the instantiation. + +This provides fine-grained control over the quantifier instantiation process, +allowing users to: +1. Inspect and log instantiations +2. Filter out undesired instantiations +3. Implement custom instantiation strategies +4. Delay certain instantiations for performance reasons +""" + +from z3 import * + +class QuantifierInstantiationController(UserPropagateBase): + """ + A user propagator that controls quantifier instantiations. + + This example demonstrates how to: + 1. Register a quantifier instantiation callback + 2. Inspect proposed instantiations + 3. Selectively allow or discard instantiations + """ + + def __init__(self, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + self.instantiation_count = 0 + self.allowed_instantiations = 0 + self.blocked_instantiations = 0 + self.instantiation_log = [] + + # Register the quantifier instantiation callback + self.add_on_binding(self.on_quantifier_instantiation) + + def on_quantifier_instantiation(self, quantifier, instantiation): + """ + Callback invoked when Z3 wants to instantiate a quantifier. + + Args: + quantifier: The quantifier being instantiated (Z3 AST) + instantiation: The proposed instantiation (Z3 AST) + + Returns: + bool: True to allow the instantiation, False to discard it + """ + self.instantiation_count += 1 + + # Log the instantiation for inspection + q_str = str(quantifier) + inst_str = str(instantiation) + self.instantiation_log.append((q_str, inst_str)) + + print(f"Instantiation #{self.instantiation_count}:") + print(f" Quantifier: {q_str}") + print(f" Instantiation: {inst_str}") + + # Example filtering logic: allow only the first 3 instantiations + # In practice, you might filter based on the structure of the instantiation, + # performance considerations, or other criteria + allow = self.instantiation_count <= 3 + + if allow: + self.allowed_instantiations += 1 + print(f" -> ALLOWED (#{self.allowed_instantiations})") + else: + self.blocked_instantiations += 1 + print(f" -> BLOCKED (#{self.blocked_instantiations})") + + print() + return allow + + def push(self): + # Required method for user propagators + pass + + def pop(self, num_scopes): + # Required method for user propagators + pass + + def fresh(self, new_ctx): + # Required method for user propagators + return QuantifierInstantiationController(ctx=new_ctx) + + def get_statistics(self): + """Return statistics about instantiation control.""" + return { + 'total_instantiation_attempts': self.instantiation_count, + 'allowed_instantiations': self.allowed_instantiations, + 'blocked_instantiations': self.blocked_instantiations, + 'instantiation_log': self.instantiation_log + } + + +def example_basic_quantifier_control(): + """ + Basic example showing how to control quantifier instantiations. + """ + print("=" * 60) + print("BASIC QUANTIFIER INSTANTIATION CONTROL EXAMPLE") + print("=" * 60) + + # Create solver with user propagator + s = Solver() + controller = QuantifierInstantiationController(s) + + # Create a simple quantified formula + x = Int('x') + f = Function('f', IntSort(), IntSort()) + + # Add a quantified axiom: forall x. f(x) >= 0 + axiom = ForAll([x], f(x) >= 0) + s.add(axiom) + + # Add constraints that might trigger instantiations + a, b, c = Ints('a b c') + s.add(f(a) < 10) + s.add(f(b) < 20) + s.add(f(c) < 30) + + # Also add constraints that should conflict if all instantiations are allowed + s.add(a == 1) + s.add(b == 2) + s.add(c == 3) + + print("Checking satisfiability with instantiation control...") + result = s.check() + print(f"Result: {result}") + + if result == sat: + print(f"Model: {s.model()}") + + # Print statistics + stats = controller.get_statistics() + print(f"\nInstantiation Statistics:") + print(f" Total attempts: {stats['total_instantiation_attempts']}") + print(f" Allowed: {stats['allowed_instantiations']}") + print(f" Blocked: {stats['blocked_instantiations']}") + + +def example_advanced_filtering(): + """ + Advanced example showing more sophisticated instantiation filtering. + """ + print("\n" + "=" * 60) + print("ADVANCED INSTANTIATION FILTERING EXAMPLE") + print("=" * 60) + + class AdvancedController(UserPropagateBase): + def __init__(self, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + self.instantiations_by_term = {} + self.add_on_binding(self.smart_filter) + + def smart_filter(self, quantifier, instantiation): + """ + Smart filtering based on instantiation content. + """ + # Extract information about the instantiation + q_str = str(quantifier) + inst_str = str(instantiation) + + # Count instantiations per term pattern + if inst_str not in self.instantiations_by_term: + self.instantiations_by_term[inst_str] = 0 + self.instantiations_by_term[inst_str] += 1 + + # Allow only up to 2 instantiations of the same pattern + allow = self.instantiations_by_term[inst_str] <= 2 + + print(f"Instantiation: {inst_str} (attempt #{self.instantiations_by_term[inst_str]})") + print(f" -> {'ALLOWED' if allow else 'BLOCKED'}") + + return allow + + def push(self): + pass + + def pop(self, num_scopes): + pass + + def fresh(self, new_ctx): + return AdvancedController(ctx=new_ctx) + + # Create solver with advanced controller + s = Solver() + controller = AdvancedController(s) + + # Create a more complex scenario + x, y = Ints('x y') + P = Function('P', IntSort(), IntSort(), BoolSort()) + + # Add quantified formula: forall x, y. P(x, y) => P(y, x) + axiom = ForAll([x, y], Implies(P(x, y), P(y, x))) + s.add(axiom) + + # Add facts that will trigger instantiations + a, b, c = Ints('a b c') + s.add(P(a, b)) + s.add(P(b, c)) + s.add(P(c, a)) + + print("Checking satisfiability with advanced filtering...") + result = s.check() + print(f"Result: {result}") + + if result == sat: + print(f"Model: {s.model()}") + + +def example_instantiation_logging(): + """ + Example focused on logging and analyzing instantiation patterns. + """ + print("\n" + "=" * 60) + print("INSTANTIATION LOGGING AND ANALYSIS EXAMPLE") + print("=" * 60) + + class LoggingController(UserPropagateBase): + def __init__(self, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + self.log = [] + self.add_on_binding(self.log_instantiation) + + def log_instantiation(self, quantifier, instantiation): + """ + Log all instantiation attempts for later analysis. + """ + entry = { + 'quantifier': str(quantifier), + 'instantiation': str(instantiation), + 'timestamp': len(self.log) + } + self.log.append(entry) + + # For this example, allow all instantiations + return True + + def push(self): + pass + + def pop(self, num_scopes): + pass + + def fresh(self, new_ctx): + return LoggingController(ctx=new_ctx) + + def analyze_patterns(self): + """Analyze logged instantiation patterns.""" + print(f"Total instantiations logged: {len(self.log)}") + + # Group by quantifier + by_quantifier = {} + for entry in self.log: + q = entry['quantifier'] + if q not in by_quantifier: + by_quantifier[q] = [] + by_quantifier[q].append(entry['instantiation']) + + for q, instantiations in by_quantifier.items(): + print(f"\nQuantifier: {q}") + print(f" Instantiations ({len(instantiations)}):") + for i, inst in enumerate(instantiations, 1): + print(f" {i}. {inst}") + + # Create solver with logging controller + s = Solver() + controller = LoggingController(s) + + # Create scenario with multiple quantifiers + x = Int('x') + f = Function('f', IntSort(), IntSort()) + g = Function('g', IntSort(), IntSort()) + + # Add multiple quantified axioms + s.add(ForAll([x], f(x) >= x)) # f(x) is at least x + s.add(ForAll([x], g(x) <= x)) # g(x) is at most x + + # Add constraints to trigger instantiations + a, b = Ints('a b') + s.add(f(a) < 5) + s.add(g(b) > 10) + s.add(a == 2) + s.add(b == 8) + + print("Solving with full logging enabled...") + result = s.check() + print(f"Result: {result}") + + # Analyze the logged instantiation patterns + print("\nInstantiation Analysis:") + controller.analyze_patterns() + + +if __name__ == "__main__": + # Run all examples + example_basic_quantifier_control() + example_advanced_filtering() + example_instantiation_logging() + + print("\n" + "=" * 60) + print("All examples completed successfully!") + print("=" * 60) \ No newline at end of file diff --git a/src/test/test_quantifier_instantiation_callback.py b/src/test/test_quantifier_instantiation_callback.py new file mode 100644 index 000000000..5ce82d52a --- /dev/null +++ b/src/test/test_quantifier_instantiation_callback.py @@ -0,0 +1,377 @@ +#!/usr/bin/env python3 +""" +Unit tests for the UserPropagator quantifier instantiation callback feature. + +This test suite validates the functionality added in Z3 version 4.15.3 that allows +user propagators to intercept and control quantifier instantiations. +""" + +import unittest +import sys +import os + +# Add the Z3 Python bindings to the path +sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..', '..', 'build', 'python')) + +from z3 import * + +class TestQuantifierInstantiationCallback(unittest.TestCase): + """Test cases for quantifier instantiation callback functionality.""" + + def setUp(self): + """Set up test fixtures.""" + self.reset_counters() + + def reset_counters(self): + """Reset global test counters.""" + global g_instantiation_count, g_allowed_count, g_blocked_count + g_instantiation_count = 0 + g_allowed_count = 0 + g_blocked_count = 0 + +# Global counters for test validation +g_instantiation_count = 0 +g_allowed_count = 0 +g_blocked_count = 0 + +class BasicInstantiationController(UserPropagateBase): + """Basic user propagator for testing instantiation control.""" + + def __init__(self, allow_first_n=3, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + self.allow_first_n = allow_first_n + self.add_on_binding(self.control_instantiation) + + def control_instantiation(self, quantifier, instantiation): + global g_instantiation_count, g_allowed_count, g_blocked_count + g_instantiation_count += 1 + + allow = g_instantiation_count <= self.allow_first_n + if allow: + g_allowed_count += 1 + else: + g_blocked_count += 1 + + return allow + + def push(self): + pass + + def pop(self, num_scopes): + pass + + def fresh(self, new_ctx): + return BasicInstantiationController(self.allow_first_n, ctx=new_ctx) + +class LoggingController(UserPropagateBase): + """User propagator that logs all instantiations without blocking.""" + + def __init__(self, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + self.log = [] + self.add_on_binding(self.log_instantiation) + + def log_instantiation(self, quantifier, instantiation): + global g_instantiation_count + g_instantiation_count += 1 + + entry = { + 'quantifier': str(quantifier), + 'instantiation': str(instantiation), + 'count': g_instantiation_count + } + self.log.append(entry) + + # Allow all instantiations + return True + + def push(self): + pass + + def pop(self, num_scopes): + pass + + def fresh(self, new_ctx): + return LoggingController(ctx=new_ctx) + +class PatternFilterController(UserPropagateBase): + """User propagator that filters based on instantiation patterns.""" + + def __init__(self, max_per_pattern=2, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + self.max_per_pattern = max_per_pattern + self.pattern_counts = {} + self.add_on_binding(self.filter_by_pattern) + + def filter_by_pattern(self, quantifier, instantiation): + global g_instantiation_count, g_allowed_count, g_blocked_count + g_instantiation_count += 1 + + pattern = str(instantiation) + self.pattern_counts[pattern] = self.pattern_counts.get(pattern, 0) + 1 + + allow = self.pattern_counts[pattern] <= self.max_per_pattern + if allow: + g_allowed_count += 1 + else: + g_blocked_count += 1 + + return allow + + def push(self): + pass + + def pop(self, num_scopes): + pass + + def fresh(self, new_ctx): + return PatternFilterController(self.max_per_pattern, ctx=new_ctx) + +class TestQuantifierInstantiationCallback(unittest.TestCase): + """Test cases for quantifier instantiation callback functionality.""" + + def setUp(self): + """Set up test fixtures.""" + self.reset_counters() + + def reset_counters(self): + """Reset global test counters.""" + global g_instantiation_count, g_allowed_count, g_blocked_count + g_instantiation_count = 0 + g_allowed_count = 0 + g_blocked_count = 0 + + def test_basic_instantiation_control(self): + """Test basic instantiation limiting functionality.""" + self.reset_counters() + + # Create solver with instantiation controller + s = Solver() + controller = BasicInstantiationController(allow_first_n=2, s=s) + + # Create simple quantified formula + x = Int('x') + f = Function('f', IntSort(), IntSort()) + + # Add quantified axiom: forall x. f(x) >= 0 + s.add(ForAll([x], f(x) >= 0)) + + # Add constraints that trigger instantiations + a, b, c = Ints('a b c') + s.add(f(a) < 10) + s.add(f(b) < 20) + s.add(f(c) < 30) + s.add(a == 1, b == 2, c == 3) + + # Solve + result = s.check() + + # Validate that callbacks were invoked and some instantiations were blocked + self.assertGreater(g_instantiation_count, 0, "No instantiations were attempted") + self.assertEqual(g_allowed_count, 2, "Expected exactly 2 allowed instantiations") + self.assertGreaterEqual(g_blocked_count, 0, "Expected some blocked instantiations") + + # Should still be satisfiable with limited instantiations + self.assertEqual(result, sat, "Formula should be satisfiable") + + def test_logging_all_instantiations(self): + """Test that logging controller captures all instantiation attempts.""" + self.reset_counters() + + s = Solver() + logger = LoggingController(s=s) + + # Create formula with multiple quantifiers + x = Int('x') + f = Function('f', IntSort(), IntSort()) + g = Function('g', IntSort(), IntSort()) + + s.add(ForAll([x], f(x) >= x)) + s.add(ForAll([x], g(x) <= x)) + + a, b = Ints('a b') + s.add(f(a) < 5) + s.add(g(b) > 10) + s.add(a == 2, b == 8) + + result = s.check() + + # Validate logging + self.assertGreater(len(logger.log), 0, "No instantiations were logged") + self.assertEqual(len(logger.log), g_instantiation_count, "Log count mismatch") + + # Check log structure + for entry in logger.log: + self.assertIn('quantifier', entry) + self.assertIn('instantiation', entry) + self.assertIn('count', entry) + self.assertIsInstance(entry['quantifier'], str) + self.assertIsInstance(entry['instantiation'], str) + self.assertIsInstance(entry['count'], int) + + def test_pattern_based_filtering(self): + """Test pattern-based instantiation filtering.""" + self.reset_counters() + + s = Solver() + filter_controller = PatternFilterController(max_per_pattern=1, s=s) + + # Create scenario that might generate duplicate patterns + x, y = Ints('x y') + P = Function('P', IntSort(), IntSort(), BoolSort()) + + s.add(ForAll([x, y], Implies(P(x, y), P(y, x)))) + + a, b, c = Ints('a b c') + s.add(P(a, b)) + s.add(P(b, c)) + s.add(P(a, c)) # This might create similar patterns + + result = s.check() + + # Validate that filtering occurred + self.assertGreater(g_instantiation_count, 0, "No instantiations were attempted") + + # Check that patterns were tracked + self.assertGreater(len(filter_controller.pattern_counts), 0, "No patterns were tracked") + + # Verify some patterns appeared multiple times (and were filtered) + max_count = max(filter_controller.pattern_counts.values()) + if max_count > 1: + self.assertGreater(g_blocked_count, 0, "Expected some blocked instantiations for repeated patterns") + + def test_callback_with_unsat_formula(self): + """Test callback behavior with unsatisfiable formulas.""" + self.reset_counters() + + s = Solver() + controller = BasicInstantiationController(allow_first_n=1, s=s) + + # Create unsatisfiable formula + x = Int('x') + f = Function('f', IntSort(), IntSort()) + + s.add(ForAll([x], f(x) >= 0)) + s.add(f(5) < -10) # Contradiction + + result = s.check() + + # Should be UNSAT regardless of instantiation control + self.assertEqual(result, unsat, "Formula should be unsatisfiable") + + # Callbacks may or may not be invoked for UNSAT formulas + # (depends on solver's instantiation strategy) + + def test_callback_registration_without_instantiations(self): + """Test that callback registration works even without quantifier instantiations.""" + self.reset_counters() + + s = Solver() + controller = BasicInstantiationController(allow_first_n=5, s=s) + + # Add formula without quantifiers + x, y = Ints('x y') + s.add(x + y == 10) + s.add(x > 5) + + result = s.check() + + # Should solve without invoking callbacks + self.assertEqual(result, sat, "Formula should be satisfiable") + self.assertEqual(g_instantiation_count, 0, "No instantiations should occur without quantifiers") + + def test_multiple_solvers_independent_callbacks(self): + """Test that callbacks on different solvers are independent.""" + self.reset_counters() + + # Create first solver with restrictive controller + s1 = Solver() + controller1 = BasicInstantiationController(allow_first_n=1, s=s1) + + # Create second solver with permissive controller + s2 = Solver() + controller2 = BasicInstantiationController(allow_first_n=10, s=s2) + + # Add same formula to both + x = Int('x') + f = Function('f', IntSort(), IntSort()) + axiom = ForAll([x], f(x) >= 0) + + for s in [s1, s2]: + s.add(axiom) + a = Int(f'a_{id(s)}') # Unique constant per solver + s.add(f(a) < 5) + s.add(a == 1) + + # Solve both + result1 = s1.check() + result2 = s2.check() + + # Both should be satisfiable + self.assertEqual(result1, sat, "First solver should find solution") + self.assertEqual(result2, sat, "Second solver should find solution") + + # Note: Since we use global counters, we can't easily test independence + # In a real implementation, each controller would have its own counters + +class TestErrorConditions(unittest.TestCase): + """Test error conditions and edge cases.""" + + def test_callback_exception_handling(self): + """Test that exceptions in callbacks are handled gracefully.""" + + class FaultyController(UserPropagateBase): + def __init__(self, s=None, ctx=None): + UserPropagateBase.__init__(self, s, ctx) + self.add_on_binding(self.faulty_callback) + + def faulty_callback(self, quantifier, instantiation): + # This callback always raises an exception + raise ValueError("Test exception in callback") + + def push(self): pass + def pop(self, num_scopes): pass + def fresh(self, new_ctx): return FaultyController(ctx=new_ctx) + + s = Solver() + + # This should not crash, but the callback behavior is implementation-defined + # when exceptions occur + try: + controller = FaultyController(s=s) + + x = Int('x') + f = Function('f', IntSort(), IntSort()) + s.add(ForAll([x], f(x) >= 0)) + s.add(f(1) < 5) + + # The solver should handle callback exceptions gracefully + # Exact behavior may vary, but should not crash + result = s.check() + + except Exception as e: + # If an exception propagates, it should be the one we raised + # or a Z3Exception wrapping it + pass + +if __name__ == '__main__': + # Check if Z3 is available + try: + from z3 import * + + # Test basic Z3 functionality + x = Int('x') + s = Solver() + s.add(x > 0) + if s.check() != sat: + print("ERROR: Basic Z3 functionality not working") + sys.exit(1) + + except ImportError: + print("ERROR: Z3 Python bindings not found") + print("Make sure PYTHONPATH includes the Z3 Python bindings directory") + sys.exit(1) + + # Run the tests + print("Running quantifier instantiation callback tests...") + unittest.main(verbosity=2) \ No newline at end of file