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.

1 files changed, 73 insertions, 121 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d0c5fb00b..5477214b0 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -66,7 +66,7 @@ protected:
   /** reset instantiation */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   /** process method */
-  virtual int process( Node f, Theory::Effort effort, int e, int limitInst = 0 ) = 0;
+  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
 public:
   InstStrategy( QuantifiersEngine* ie ) : d_quantEngine( ie ){}
   virtual ~InstStrategy(){}
@@ -74,7 +74,7 @@ public:
   /** reset instantiation */
   void resetInstantiationRound( Theory::Effort effort );
   /** do instantiation round method */
-  int doInstantiation( Node f, Theory::Effort effort, int e, int limitInst = 0 );
+  int doInstantiation( Node f, Theory::Effort effort, int e );
   /** update status */
   static void updateStatus( int& currStatus, int addStatus ){
     if( addStatus==STATUS_UNFINISHED ){
@@ -99,9 +99,13 @@ public:
 };/* class InstStrategy */
 
 class QuantifiersModule {
+protected:
+  QuantifiersEngine* d_quantEngine;
 public:
-  QuantifiersModule(){}
+  QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
   ~QuantifiersModule(){}
+  //get quantifiers engine
+  QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
   /* Call during check registerQuantifier has already been called */
   virtual void check( Theory::Effort e ) = 0;
   /* Called for new quantifiers */
@@ -111,59 +115,17 @@ public:
   virtual Node explain(TNode n) = 0;
 };/* class QuantifiersModule */
 
-class TermArgTrie {
-private:
-  bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex );
-public:
-  /** the data */
-  std::map< Node, TermArgTrie > d_data;
-public:
-  bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
-};/* class TermArgTrie */
-
-class TermDb {
-private:
-  /** reference to the quantifiers engine */
-  QuantifiersEngine* d_quantEngine;
-  /** calculated no match terms */
-  bool d_matching_active;
-  /** terms processed */
-  std::map< Node, bool > d_processed;
-public:
-  TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){}
-  ~TermDb(){}
-  /** map from APPLY_UF operators to ground terms for that operator */
-  std::map< Node, std::vector< Node > > d_op_map;
-  /** map from APPLY_UF functions to trie */
-  std::map< Node, TermArgTrie > d_func_map_trie;
-  /** map from APPLY_UF predicates to trie */
-  std::map< Node, TermArgTrie > d_pred_map_trie[2];
-  /** map from type nodes to terms of that type */
-  std::map< TypeNode, std::vector< Node > > d_type_map;
-  /** add a term to the database */
-  void addTerm( Node n, std::vector< Node >& added, bool withinQuant = false );
-  /** reset (calculate which terms are active) */
-  void reset( Theory::Effort effort );
-  /** set active */
-  void setMatchingActive( bool a ) { d_matching_active = a; }
-  /** get active */
-  bool getMatchingActive() { return d_matching_active; }
-public:
-  /** parent structure (for efficient E-matching):
-      n -> op -> index -> L
-      map from node "n" to a list of nodes "L", where each node n' in L
-        has operator "op", and n'["index"] = n.
-      for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... }
-  */
-  std::map< Node, std::map< Node, std::map< int, std::vector< Node > > > > d_parents;
-};/* class TermDb */
-
 namespace quantifiers {
   class InstantiationEngine;
+  class ModelEngine;
+  class TermDb;
+  class FirstOrderModel;
 }/* CVC4::theory::quantifiers */
 
+
 class QuantifiersEngine {
   friend class quantifiers::InstantiationEngine;
+  friend class quantifiers::ModelEngine;
   friend class InstMatch;
 private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
@@ -171,41 +133,35 @@ private:
   TheoryEngine* d_te;
   /** vector of modules for quantifiers */
   std::vector< QuantifiersModule* > d_modules;
+  /** instantiation engine */
+  quantifiers::InstantiationEngine* d_inst_engine;
+  /** model engine */
+  quantifiers::ModelEngine* d_model_engine;
   /** equality query class */
   EqualityQuery* d_eq_query;
 
-  /** list of all quantifiers */
+  /** list of all quantifiers (pre-rewrite) */
   std::vector< Node > d_quants;
-  /** list of quantifiers asserted in the current context */
-  context::CDList<Node> d_forall_asserts;
-  /** map from universal quantifiers to the list of variables */
-  std::map< Node, std::vector< Node > > d_vars;
-  /** map from universal quantifiers to the list of skolem constants */
-  std::map< Node, std::vector< Node > > d_skolem_constants;
-  /** map from universal quantifiers to their skolemized body */
-  std::map< Node, Node > d_skolem_body;
-  /** map from universal quantifiers to their bound body */
-  std::map< Node, Node > d_bound_body;
-  /** instantiation constants to universal quantifiers */
-  std::map< Node, Node > d_inst_constants_map;
-  /** map from universal quantifiers to their counterexample body */
-  std::map< Node, Node > d_counterexample_body;
-  /** map from universal quantifiers to the list of instantiation constants */
-  std::map< Node, std::vector< Node > > d_inst_constants;
+  /** list of all quantifiers (post-rewrite) */
+  std::vector< Node > d_r_quants;
   /** map from quantifiers to whether they are active */
   BoolMap d_active;
   /** lemmas produced */
   std::map< Node, bool > d_lemmas_produced;
   /** lemmas waiting */
   std::vector< Node > d_lemmas_waiting;
+  /** has added lemma this round */
+  bool d_hasAddedLemma;
   /** inst matches produced for each quantifier */
   std::map< Node, InstMatchTrie > d_inst_match_trie;
-  /** free variable for instantiation constant type */
-  std::map< TypeNode, Node > d_free_vars;
   /** owner of quantifiers */
   std::map< Node, Theory* > d_owner;
   /** term database */
-  TermDb* d_term_db;
+  quantifiers::TermDb* d_term_db;
+  /** extended model object */
+  quantifiers::FirstOrderModel* d_model;
+  /** has the model been set? */
+  bool d_model_set;
   /** universal quantifiers that have been rewritten */
   std::map< Node, std::vector< Node > > d_quant_rewritten;
   /** map from rewritten universal quantifiers to the quantifier they are the consequence of */
@@ -223,12 +179,6 @@ private:
 private:
   /** helper functions compute phase requirements */
   static void computePhaseReqs2( Node n, bool polarity, std::map< Node, int >& phaseReqs );
-  /** set instantiation level attr */
-  void setInstantiationLevelAttr( Node n, uint64_t level );
-  /** set instantiation constant attr */
-  void setInstantiationConstantAttr( Node n, Node f );
-  /** make instantiation constants for */
-  void makeInstantiationConstantsFor( Node f );
 
   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
 
@@ -241,11 +191,17 @@ public:
   TheoryEngine* getTheoryEngine() { return d_te; }
   /** get equality query object */
   EqualityQuery* getEqualityQuery() { return d_eq_query; }
-  /** set equality query object */
-  void setEqualityQuery( EqualityQuery* eq ) { d_eq_query = eq; }
+  /** get instantiation engine */
+  quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
+  /** get model engine */
+  quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
+  /** get default sat context for quantifiers engine */
+  context::Context* getSatContext();
+  /** get default output channel for the quantifiers engine */
+  OutputChannel& getOutputChannel();
+  /** get default valuation for the quantifiers engine */
+  Valuation& getValuation();
 public:
-  /** add module */
-  void addModule( QuantifiersModule* qm ) { d_modules.push_back( qm ); }
   /** check at level */
   void check( Theory::Effort e );
   /** register (non-rewritten) quantifier */
@@ -256,19 +212,24 @@ public:
   void assertNode( Node f );
   /** propagate */
   void propagate( Theory::Effort level );
+  /** reset instantiation round */
+  void resetInstantiationRound( Theory::Effort level );
+
+  //create inst variable
+  std::vector<Node> createInstVariable( std::vector<Node> & vars );
 public:
   /** add lemma lem */
   bool addLemma( Node lem );
   /** instantiate f with arguments terms */
   bool addInstantiation( Node f, std::vector< Node >& terms );
   /** do instantiation specified by m */
-  bool addInstantiation( Node f, InstMatch& m, bool addSplits = false );
+  bool addInstantiation( Node f, InstMatch& m );
   /** split on node n */
   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
   /** add split equality */
   bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
   /** has added lemma */
-  bool hasAddedLemma() { return !d_lemmas_waiting.empty(); }
+  bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
   /** flush lemmas */
   void flushLemmas( OutputChannel* out );
   /** get number of waiting lemmas */
@@ -278,24 +239,6 @@ public:
   int getNumQuantifiers() { return (int)d_quants.size(); }
   /** get quantifier */
   Node getQuantifier( int i ) { return d_quants[i]; }
-  /** get number of asserted quantifiers */
-  int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
-  /** get asserted quantifier */
-  Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
-  /** get instantiation constants */
-  void getInstantiationConstantsFor( Node f, std::vector< Node >& ics ) {
-    ics.insert( ics.begin(), d_inst_constants[f].begin(), d_inst_constants[f].end() );
-  }
-  /** get the i^th instantiation constant of f */
-  Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; }
-  /** get number of instantiation constants for f */
-  int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); }
-  std::vector<Node> createInstVariable( std::vector<Node> & vars );
-public:
-  /** get the ce body f[e/x] */
-  Node getCounterexampleBody( Node f );
-  /** get the skolemized body f[e/x] */
-  Node getSkolemizedBody( Node f );
   /** set active */
   void setActive( Node n, bool val ) { d_active[n] = val; }
   /** get active */
@@ -317,26 +260,6 @@ public:
   /** compute phase requirements */
   void generatePhaseReqs( Node f, Node n );
 public:
-  /** returns node n with bound vars of f replaced by instantiation constants of f
-      node n : is the futur pattern
-      node f : is the quantifier containing which bind the variable
-      return a pattern where the variable are replaced by variable for
-      instantiation.
-   */
-  Node getSubstitutedNode( Node n, Node f );
-  /** same as before but node f is just linked to the new pattern by the
-      applied attribute
-      vars the bind variable
-      nvars the same variable but with an attribute
-  */
-  Node convertNodeToPattern( Node n, Node f,
-                             const std::vector<Node> & vars,
-                             const std::vector<Node> & nvars);
-  /** get free variable for instantiation constant */
-  Node getFreeVariableForInstConstant( Node n );
-  /** get bound variable for variable */
-  Node getBoundVariableForVariable( Node n );
-public:
   /** has owner */
   bool hasOwner( Node f ) { return d_owner.find( f )!=d_owner.end(); }
   /** get owner */
@@ -344,8 +267,10 @@ public:
   /** set owner */
   void setOwner( Node f, Theory* t ) { d_owner[f] = t; }
 public:
+  /** get model */
+  quantifiers::FirstOrderModel* getModel() { return d_model; }
   /** get term database */
-  TermDb* getTermDatabase() { return d_term_db; }
+  quantifiers::TermDb* getTermDatabase() { return d_term_db; }
   /** add term to database */
   void addTermToDatabase( Node n, bool withinQuant = false );
 private:
@@ -380,8 +305,35 @@ public:
     ~Statistics();
   };/* class QuantifiersEngine::Statistics */
   Statistics d_statistics;
+public:
+  /** options */
+  bool d_optInstCheckDuplicate;
+  bool d_optInstMakeRepresentative;
+  bool d_optInstAddSplits;
+  bool d_optMatchIgnoreModelBasis;
+  bool d_optInstLimitActive;
+  int d_optInstLimit;
 };/* class QuantifiersEngine */
 
+
+
+/** equality query object using theory engine */
+class EqualityQueryQuantifiersEngine : public EqualityQuery
+{
+private:
+  /** pointer to theory engine */
+  QuantifiersEngine* d_qe;
+public:
+  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ){}
+  ~EqualityQueryQuantifiersEngine(){}
+  /** general queries about equality */
+  bool hasTerm( Node a );
+  Node getRepresentative( Node a );
+  bool areEqual( Node a, Node b );
+  bool areDisequal( Node a, Node b );
+  Node getInternalRepresentative( Node a );
+}; /* EqualityQueryQuantifiersEngine */
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */