diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-12 15:18:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-12 15:18:30 -0500 |
| commit | 093d5ffdfa5c1656309da6b9cbdfbbf28574a8a0 (patch) | |
| tree | 96c76652c60e286223523cf08f599b4cd84fb687 /src/theory/quantifiers/expr_miner_manager.cpp | |
| parent | ec8ea8a9c993435c4c5e671b1beea45ac088de64 (diff) | |
Add option --sygus-rr-synth-rec for considering all grammar types recursively (#2270)
Diffstat (limited to 'src/theory/quantifiers/expr_miner_manager.cpp')
| -rw-r--r-- | src/theory/quantifiers/expr_miner_manager.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index a808d386c..4de95e3a1 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -15,6 +15,8 @@ #include "theory/quantifiers/expr_miner_manager.h" #include "theory/quantifiers_engine.h" +#include "options/quantifiers_options.h" + namespace CVC4 { namespace theory { namespace quantifiers { @@ -140,7 +142,7 @@ bool ExpressionMinerManager::addTerm(Node sol, bool ret = true; if (d_doRewSynth) { - ret = d_crd.addTerm(sol, out, rew_print); + ret = d_crd.addTerm(sol, options::sygusRewSynthRec(), out, rew_print); } // a unique term, let's try the query generator |