summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_util.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
-rw-r--r--src/theory/quantifiers/quant_util.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 5e0f511e0..2186e03fd 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -77,8 +77,10 @@ private:
/** helper functions compute phase requirements */
void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );
public:
+ QuantPhaseReq(){}
QuantPhaseReq( Node n, bool computeEq = false );
~QuantPhaseReq(){}
+ void initialize( Node n, bool computeEq );
/** is phase required */
bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }
/** get phase requirement */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback