Quantifiers subdirectories (#1608)

1 files changed, 202 insertions, 0 deletions

diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
new file mode 100644
index 000000000..4eb592b3e
--- /dev/null
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -0,0 +1,202 @@
+/*********************                                                        */
+/*! \file model_builder.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Model Builder class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
+#define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_model_builder.h"
+#include "theory/uf/theory_uf_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+
+class QModelBuilder : public TheoryEngineModelBuilder
+{
+protected:
+  //quantifiers engine
+  QuantifiersEngine* d_qe;
+  bool preProcessBuildModel(TheoryModel* m); //must call preProcessBuildModelStd
+  bool preProcessBuildModelStd(TheoryModel* m);
+  /** number of lemmas generated while building model */
+  unsigned d_addedLemmas;
+  unsigned d_triedLemmas;
+public:
+  QModelBuilder( context::Context* c, QuantifiersEngine* qe );
+
+  //do exhaustive instantiation  
+  // 0 :  failed, but resorting to true exhaustive instantiation may work
+  // >0 : success
+  // <0 : failed
+  virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
+  //whether to construct model
+  virtual bool optUseModel();
+  /** exist instantiation ? */
+  virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
+  //debug model
+  virtual void debugModel( TheoryModel* m );
+  //statistics 
+  unsigned getNumAddedLemmas() { return d_addedLemmas; }
+  unsigned getNumTriedLemmas() { return d_triedLemmas; }
+};
+
+
+
+
+
+class TermArgBasisTrie {
+public:
+  /** the data */
+  std::map< Node, TermArgBasisTrie > d_data;
+  /** add term to the trie */
+  bool addTerm(FirstOrderModel* fm, Node n, unsigned argIndex = 0);
+};/* class TermArgBasisTrie */
+
+/** model builder class
+  *  This class is capable of building candidate models based on the current quantified formulas
+  *  that are asserted.  Use:
+  *  (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel
+  *  (2) if candidate model is determined to be a real model,
+           then call QModelBuilder::buildModel( m, true );
+  */
+class QModelBuilderIG : public QModelBuilder
+{
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
+
+ protected:
+  BoolMap d_basisNoMatch;
+  //map from operators to model preference data
+  std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
+  //built model uf
+  std::map< Node, bool > d_uf_model_constructed;
+  //whether inst gen was done
+  bool d_didInstGen;
+  /** process build model */
+  virtual bool processBuildModel( TheoryModel* m );
+
+ protected:
+  //reset
+  virtual void reset( FirstOrderModel* fm ) = 0;
+  //initialize quantifiers, return number of lemmas produced
+  virtual int initializeQuantifier(Node f, Node fp, FirstOrderModel* fm);
+  //analyze model
+  virtual void analyzeModel( FirstOrderModel* fm );
+  //analyze quantifiers
+  virtual void analyzeQuantifier( FirstOrderModel* fm, Node f ) = 0;
+  //do InstGen techniques for quantifier, return number of lemmas produced
+  virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0;
+  //theory-specific build models
+  virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0;
+
+ protected:
+  //map from quantifiers to if are SAT
+  //std::map< Node, bool > d_quant_sat;
+  //which quantifiers have been initialized
+  std::map< Node, bool > d_quant_basis_match_added;
+  //map from quantifiers to model basis match
+  std::map< Node, InstMatch > d_quant_basis_match;
+
+ protected:  // helper functions
+  /** term has constant definition */
+  bool hasConstantDefinition( Node n );
+
+ public:
+  QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
+
+ public:
+  /** statistics class */
+  class Statistics {
+  public:
+    IntStat d_num_quants_init;
+    IntStat d_num_partial_quants_init;
+    IntStat d_init_inst_gen_lemmas;
+    IntStat d_inst_gen_lemmas;
+    IntStat d_eval_formulas;
+    IntStat d_eval_uf_terms;
+    IntStat d_eval_lits;
+    IntStat d_eval_lits_unknown;
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
+  // is term selected
+  virtual bool isTermSelected( Node n ) { return false; }
+  /** quantifier has inst-gen definition */
+  virtual bool hasInstGen( Node f ) = 0;
+  /** did inst gen this round? */
+  bool didInstGen() { return d_didInstGen; }
+  // is quantifier active?
+  bool isQuantifierActive( Node f );
+  //do exhaustive instantiation
+  int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+
+  //temporary stats
+  int d_numQuantSat;
+  int d_numQuantInstGen;
+  int d_numQuantNoInstGen;
+  int d_numQuantNoSelForm;
+  //temporary stat
+  int d_instGenMatches;
+};/* class QModelBuilder */
+
+
+class QModelBuilderDefault : public QModelBuilderIG
+{
+ private:  /// information for (old) InstGen
+  // map from quantifiers to their selection literals
+  std::map< Node, Node > d_quant_selection_lit;
+  std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates;
+  //map from quantifiers to their selection literal terms
+  std::map< Node, std::vector< Node > > d_quant_selection_lit_terms;
+  //map from terms to the selection literals they exist in
+  std::map< Node, Node > d_term_selection_lit;
+  //map from operators to terms that appear in selection literals
+  std::map< Node, std::vector< Node > > d_op_selection_terms;
+  //get selection score
+  int getSelectionScore( std::vector< Node >& uf_terms );
+
+ protected:
+  //reset
+  void reset(FirstOrderModel* fm) override;
+  //analyze quantifier
+  void analyzeQuantifier(FirstOrderModel* fm, Node f) override;
+  //do InstGen techniques for quantifier, return number of lemmas produced
+  int doInstGen(FirstOrderModel* fm, Node f) override;
+  //theory-specific build models
+  void constructModelUf(FirstOrderModel* fm, Node op) override;
+
+ protected:
+  std::map< Node, QuantPhaseReq > d_phase_reqs;
+
+ public:
+  QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
+
+  //options
+  bool optReconsiderFuncConstants() { return true; }
+  //has inst gen
+  bool hasInstGen(Node f) override
+  {
+    return !d_quant_selection_lit[f].isNull();
+  }
+};
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */