Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

1 files changed, 179 insertions, 0 deletions

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