diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-01 17:35:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-01 22:35:13 +0000 |
| commit | b4e98013a8e2572545ec3f637dd1caa06e3f7207 (patch) | |
| tree | 5d133f561aebe035a33c8f9256fb7097877be003 /src/smt/optimization_solver.cpp | |
| parent | c2a5fcf1ae85d007bccd8fa294a7b66287972c65 (diff) | |
Add recursive function definitions to subsolver in sygus (#6824)
This passes recursive function definitions to the verification subsolver in sygus, with a default bounded limit of 3. This required improving the interface for setting up subsolvers by allowing custom options; the sygus solver statically computes an instance of the options that it uses in all calls.
This allows us to solve non-PBE sygus problems with recursive function definitions. The PR adds an example.
Diffstat (limited to 'src/smt/optimization_solver.cpp')
| -rw-r--r-- | src/smt/optimization_solver.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index a46452004..027ba71ec 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -84,7 +84,7 @@ std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout( std::unique_ptr<SmtEngine> optChecker; // initializeSubSolver will copy the options and theories enabled // from the current solver to optChecker and adds timeout - theory::initializeSubsolver(optChecker, needsTimeout, timeout); + theory::initializeSubsolver(optChecker, nullptr, needsTimeout, timeout); // we need to be in incremental mode for multiple objectives since we need to // push pop we need to produce models to inrement on our objective optChecker->setOption("incremental", "true"); |