diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-19 20:59:51 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-19 20:59:51 -0500 |
commit | ccc301aa495153b3a2bd1b3958cc49cef65b09cc (patch) | |
tree | fdea3fc3cf84d060703f6fad39315a8b10a7f82c /src/theory/quantifiers/expr_miner_manager.cpp | |
parent | ce8c429281fd1f7e4ac4d2b7133152c1d370df0c (diff) |
Sygus streaming non-implied predicates (#2660)
Diffstat (limited to 'src/theory/quantifiers/expr_miner_manager.cpp')
-rw-r--r-- | src/theory/quantifiers/expr_miner_manager.cpp | 40 |
1 files changed, 32 insertions, 8 deletions
diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index 010b5a4ab..cc97888e3 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -22,6 +22,7 @@ namespace quantifiers { ExpressionMinerManager::ExpressionMinerManager() : d_doRewSynth(false), d_doQueryGen(false), + d_doFilterImplied(false), d_use_sygus_type(false), d_qe(nullptr), d_tds(nullptr) @@ -35,6 +36,7 @@ void ExpressionMinerManager::initialize(const std::vector<Node>& vars, { d_doRewSynth = false; d_doQueryGen = false; + d_doFilterImplied = false; d_sygus_fun = Node::null(); d_use_sygus_type = false; d_qe = nullptr; @@ -50,6 +52,7 @@ void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe, { d_doRewSynth = false; d_doQueryGen = false; + d_doFilterImplied = false; d_sygus_fun = f; d_use_sygus_type = useSygusType; d_qe = qe; @@ -104,22 +107,43 @@ void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh) d_qg.setThreshold(deqThresh); } +void ExpressionMinerManager::enableFilterImpliedSolutions() +{ + d_doFilterImplied = true; + std::vector<Node> vars; + d_sampler.getVariables(vars); + d_solf.initialize(vars, &d_sampler); +} + bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out, bool& rew_print) { - bool ret = d_crd.addTerm(sol, out, rew_print); + // set the builtin version + Node solb = sol; + if (d_use_sygus_type) + { + solb = d_tds->sygusToBuiltin(sol); + } + + // add to the candidate rewrite rule database + bool ret = true; + if (d_doRewSynth) + { + ret = d_crd.addTerm(sol, out, rew_print); + } + + // a unique term, let's try the query generator if (ret && d_doQueryGen) { - // use the builtin version if d_use_sygus_type is true - Node solb = sol; - if (d_use_sygus_type) - { - solb = d_tds->sygusToBuiltin(sol); - } - // a unique term, let's try the query generator d_qg.addTerm(solb, out); } + + // filter if it's implied + if (ret && d_doFilterImplied) + { + ret = d_solf.addTerm(solb, out); + } return ret; } |