diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-17 00:24:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-17 05:24:39 +0000 |
commit | c783a90bc4dbf43a2d054a4e04ae0cae280bea30 (patch) | |
tree | cb0faf6a9599074964c01a3d54ea0db8fd709429 | |
parent | 1d81aaef0d3a3f6a9cadc57d0e667506138af003 (diff) |
Improve conversion to skolems in expression miner (#7019)
Work towards a new expression miner for caching satisfiability queries.
-rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 37 | ||||
-rw-r--r-- | src/theory/quantifiers/expr_miner.h | 8 |
2 files changed, 14 insertions, 31 deletions
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 72605e9d1..0f46fa790 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -38,38 +38,19 @@ void ExprMiner::initialize(const std::vector<Node>& vars, SygusSampler* ss) Node ExprMiner::convertToSkolem(Node n) { - std::vector<Node> fvs; - TermUtil::computeVarContains(n, fvs); - if (fvs.empty()) + if (d_skolems.empty()) { - return n; - } - std::vector<Node> sfvs; - std::vector<Node> sks; - // map to skolems - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - for (unsigned i = 0, size = fvs.size(); i < size; i++) - { - Node v = fvs[i]; - // only look at the sampler variables - if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end()) + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + for (const Node& v : d_vars) { - sfvs.push_back(v); - std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v); - if (itf == d_fv_to_skolem.end()) - { - Node sk = sm->mkDummySkolem("rrck", v.getType()); - d_fv_to_skolem[v] = sk; - sks.push_back(sk); - } - else - { - sks.push_back(itf->second); - } + Node sk = sm->mkDummySkolem("rrck", v.getType()); + d_skolems.push_back(sk); + d_fv_to_skolem[v] = sk; } } - return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end()); + return n.substitute( + d_vars.begin(), d_vars.end(), d_skolems.begin(), d_skolems.end()); } void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 36fae1549..79d0c6650 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -62,13 +62,15 @@ class ExprMiner protected: /** the set of variables used by this class */ std::vector<Node> d_vars; - /** pointer to the sygus sampler object we are using */ - SygusSampler* d_sampler; /** - * Maps to skolems for each free variable that appears in a check. This is + * The set of skolems corresponding to the above variables. These are * used during initializeChecker so that query (which may contain free * variables) is converted to a formula without free variables. */ + std::vector<Node> d_skolems; + /** pointer to the sygus sampler object we are using */ + SygusSampler* d_sampler; + /** Maps to skolems for each free variable based on d_vars/d_skolems. */ std::map<Node, Node> d_fv_to_skolem; /** convert */ Node convertToSkolem(Node n); |