From 3378e253fcdb34c753407bb16d08929da06b3aaa Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 11 Jun 2012 16:28:23 +0000 Subject: Merge from quantifiers2-trunkmerge branch. Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver. --- src/theory/uf/inst_strategy.h | 179 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 179 insertions(+) create mode 100644 src/theory/uf/inst_strategy.h (limited to 'src/theory/uf/inst_strategy.h') diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h new file mode 100644 index 000000000..906169811 --- /dev/null +++ b/src/theory/uf/inst_strategy.h @@ -0,0 +1,179 @@ +/********************* */ +/*! \file inst_strategy.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory uf instantiation strategies + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__INST_STRATEGY_H +#define __CVC4__INST_STRATEGY_H + +#include "theory/quantifiers_engine.h" + +#include "context/context.h" +#include "context/context_mm.h" + +#include "util/stats.h" +#include "theory/uf/theory_uf.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +class InstantiatorTheoryUf; + +//instantiation strategies + +class InstStrategyCheckCESolved : public InstStrategy{ +private: + /** InstantiatorTheoryUf class */ + InstantiatorTheoryUf* d_th; + /** is solved? */ + std::map< Node, bool > d_solved; + /** calc if f is solved */ + void calcSolved( Node f ); + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e, int instLimit ); +public: + InstStrategyCheckCESolved( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategy( ie ), d_th( th ){} + ~InstStrategyCheckCESolved(){} + /** identify */ + std::string identify() const { return std::string("CheckCESolved"); } +};/* class InstStrategyCheckCESolved */ + +class InstStrategyUserPatterns : public InstStrategy{ +private: + /** InstantiatorTheoryUf class */ + InstantiatorTheoryUf* d_th; + /** explicitly provided patterns */ + std::map< Node, std::vector< Trigger* > > d_user_gen; + /** counter for quantifiers */ + std::map< Node, int > d_counter; + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e, int instLimit ); +public: + InstStrategyUserPatterns( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategy( ie ), d_th( th ){} + ~InstStrategyUserPatterns(){} +public: + /** add pattern */ + void addUserPattern( Node f, Node pat ); + /** get num patterns */ + int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); } + /** get user pattern */ + Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; } + /** identify */ + std::string identify() const { return std::string("UserPatterns"); } +};/* class InstStrategyUserPatterns */ + +class InstStrategyAutoGenTriggers : public InstStrategy{ +public: + enum { + RELEVANCE_NONE, + RELEVANCE_DEFAULT, + }; +private: + /** InstantiatorTheoryUf class */ + InstantiatorTheoryUf* d_th; + /** trigger generation strategy */ + int d_tr_strategy; + /** relevance strategy */ + int d_rlv_strategy; + /** regeneration */ + bool d_regenerate; + int d_regenerate_frequency; + /** generate additional triggers */ + bool d_generate_additional; + /** triggers for each quantifier */ + std::map< Node, std::map< Trigger*, bool > > d_auto_gen_trigger; + std::map< Node, int > d_counter; + /** single, multi triggers for each quantifier */ + std::map< Node, std::vector< Node > > d_patTerms[2]; + std::map< Node, bool > d_is_single_trigger; + std::map< Node, bool > d_single_trigger_gen; + std::map< Node, bool > d_made_multi_trigger; +private: + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e, int instLimit ); + /** generate triggers */ + void generateTriggers( Node f ); +public: + 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 ); + } + ~InstStrategyAutoGenTriggers(){} +public: + /** get auto-generated trigger */ + Trigger* getAutoGenTrigger( Node f ); + /** identify */ + std::string identify() const { return std::string("AutoGenTriggers"); } + /** set regenerate frequency, if fr<0, turn off regenerate */ + void setRegenerateFrequency( int fr ){ + if( fr<0 ){ + d_regenerate = false; + }else{ + d_regenerate_frequency = fr; + d_regenerate = true; + } + } + /** set generate additional */ + void setGenerateAdditional( bool val ) { d_generate_additional = val; } +};/* class InstStrategyAutoGenTriggers */ + +#if 0 + +class InstStrategyAddFailSplits : public InstStrategy{ +private: + /** InstantiatorTheoryUf class */ + InstantiatorTheoryUf* d_th; + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e, int instLimit ); +public: + InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategy( ie ), d_th( th ){} + ~InstStrategyAddFailSplits(){} + /** identify */ + std::string identify() const { return std::string("AddFailSplits"); } +};/* class InstStrategyAddFailSplits */ + +#endif /* 0 */ + +class InstStrategyFreeVariable : public InstStrategy{ +private: + /** InstantiatorTheoryUf class */ + InstantiatorTheoryUf* d_th; + /** guessed instantiations */ + std::map< Node, bool > d_guessed; + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e, int instLimit ); +public: + InstStrategyFreeVariable( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategy( ie ), d_th( th ){} + ~InstStrategyFreeVariable(){} + /** identify */ + std::string identify() const { return std::string("FreeVariable"); } +};/* class InstStrategyFreeVariable */ + +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif -- cgit v1.2.3