From 65798541fa437278cde0c759ab70fd9fa4fe9638 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Jul 2012 18:30:15 +0000 Subject: merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this. --- src/theory/uf/inst_strategy.h | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'src/theory/uf/inst_strategy.h') diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h index 906169811..09b8087f2 100644 --- a/src/theory/uf/inst_strategy.h +++ b/src/theory/uf/inst_strategy.h @@ -45,9 +45,9 @@ private: void calcSolved( Node f ); /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e, int instLimit ); + int process( Node f, Theory::Effort effort, int e ); public: - InstStrategyCheckCESolved( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategyCheckCESolved( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : InstStrategy( ie ), d_th( th ){} ~InstStrategyCheckCESolved(){} /** identify */ @@ -64,9 +64,9 @@ private: std::map< Node, int > d_counter; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e, int instLimit ); + int process( Node f, Theory::Effort effort, int e ); public: - InstStrategyUserPatterns( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategyUserPatterns( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : InstStrategy( ie ), d_th( th ){} ~InstStrategyUserPatterns(){} public: @@ -109,11 +109,11 @@ private: private: /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e, int instLimit ); + int process( Node f, Theory::Effort effort, int e ); /** generate triggers */ void generateTriggers( Node f ); public: - InstStrategyAutoGenTriggers( InstantiatorTheoryUf* th, QuantifiersEngine* ie, int tstrt, int rstrt, int rgfr = -1 ) : + InstStrategyAutoGenTriggers( InstantiatorTheoryUf* th, QuantifiersEngine* ie, int tstrt, int rstrt, int rgfr = -1 ) : InstStrategy( ie ), d_th( th ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){ setRegenerateFrequency( rgfr ); } @@ -144,9 +144,9 @@ private: InstantiatorTheoryUf* d_th; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e, int instLimit ); + int process( Node f, Theory::Effort effort, int e ); public: - InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : InstStrategy( ie ), d_th( th ){} ~InstStrategyAddFailSplits(){} /** identify */ @@ -163,9 +163,9 @@ private: std::map< Node, bool > d_guessed; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e, int instLimit ); + int process( Node f, Theory::Effort effort, int e ); public: - InstStrategyFreeVariable( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategyFreeVariable( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : InstStrategy( ie ), d_th( th ){} ~InstStrategyFreeVariable(){} /** identify */ -- cgit v1.2.3