diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-29 14:28:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-09-29 14:28:52 -0500 |
commit | b48120e1c224208eaef28f86e77830f211852f9b (patch) | |
tree | 28d9329c1cc13d5e99e8ac38212efb88c20c7ffa /src/theory/quantifiers_engine.h | |
parent | 8011f2715fa6ba312fd766cab5249648598310d4 (diff) |
Simplify representation of inversion Skolems for bv cegqi (#1164)
* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression.
* Enable other regression
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 7d8f5354b..443bbd643 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -48,16 +48,20 @@ public: }; namespace quantifiers { + //TODO: organize this more/review this, github issue #1163 + //utilities class TermDb; class TermDbSygus; class FirstOrderModel; - //modules + class RelevantDomain; + class BvInverter; + class InstPropagator; + //modules, these are "subsolvers" of the quantifiers theory. class InstantiationEngine; class ModelEngine; class BoundedIntegers; class QuantConflictFind; class RewriteEngine; - class RelevantDomain; class QModelBuilder; class ConjectureGenerator; class CegInstantiation; @@ -71,7 +75,6 @@ namespace quantifiers { class QuantDSplit; class QuantAntiSkolem; class EqualityInference; - class InstPropagator; }/* CVC4::theory::quantifiers */ namespace inst { @@ -108,6 +111,8 @@ private: QuantRelevance * d_quant_rel; /** relevant domain */ quantifiers::RelevantDomain* d_rel_dom; + /** inversion utility for BV instantiation */ + quantifiers::BvInverter * d_bv_invert; /** alpha equivalence */ quantifiers::AlphaEquivalence * d_alpha_equiv; /** model builder */ @@ -225,6 +230,8 @@ public: Valuation& getValuation(); /** get relevant domain */ quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; } + /** get the BV inverter utility */ + quantifiers::BvInverter * getBvInverter() { return d_bv_invert; } /** get quantifier relevance */ QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } /** get the model builder */ |