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 /src/theory/quantifiers/expr_miner.h | |
| parent | 1d81aaef0d3a3f6a9cadc57d0e667506138af003 (diff) | |
Improve conversion to skolems in expression miner (#7019)
Work towards a new expression miner for caching satisfiability queries.
Diffstat (limited to 'src/theory/quantifiers/expr_miner.h')
| -rw-r--r-- | src/theory/quantifiers/expr_miner.h | 8 |
1 files changed, 5 insertions, 3 deletions
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); |