From 65c2e1688d83dfeb913b689c10d9b43c5dc89cc0 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 27 Jun 2015 09:30:06 +0200 Subject: Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression. --- src/theory/quantifiers/model_builder.h | 4 ---- 1 file changed, 4 deletions(-) (limited to 'src/theory/quantifiers/model_builder.h') diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index d9ed3f092..8e84f15e2 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -123,10 +123,6 @@ public: QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); virtual ~QModelBuilderIG() throw() {} public: - //whether to add inst-gen lemmas - virtual bool optInstGen(); - //whether to only consider only quantifier per round of inst-gen - virtual bool optOneQuantPerRoundInstGen(); /** statistics class */ class Statistics { public: -- cgit v1.2.3