summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index b9ce2063a..92296ebac 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -101,6 +101,7 @@ namespace quantifiers {
class InstStrategyCbqi;
class InstStrategyCegqi;
class QuantDSplit;
+ class QuantAntiSkolem;
}/* CVC4::theory::quantifiers */
namespace inst {
@@ -162,6 +163,8 @@ private:
quantifiers::InstStrategyCbqi * d_i_cbqi;
/** quantifiers splitting */
quantifiers::QuantDSplit * d_qsplit;
+ /** quantifiers anti-skolemization */
+ quantifiers::QuantAntiSkolem * d_anti_skolem;
public: //effort levels
enum {
QEFFORT_CONFLICT,
@@ -260,6 +263,8 @@ public: //modules
quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
/** get quantifiers splitting */
quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; }
+ /** get quantifiers anti-skolemization */
+ quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; }
private:
/** owner of quantified formulas */
std::map< Node, QuantifiersModule * > d_owner;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback