From 67623ee1e6d62b36cb598c28ad9b871b6957a9dd Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 9 Apr 2016 13:07:11 -0500
Subject: Minor refactoring of entailment tests and quantifiers util. Initial
 draft of instantiation propagator.

---
 src/theory/quantifiers_engine.h | 51 +++++++++--------------------------------
 1 file changed, 11 insertions(+), 40 deletions(-)

(limited to 'src/theory/quantifiers_engine.h')

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index cdf7c3b89..9ee967eb0 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -44,47 +44,10 @@ namespace quantifiers {
   class TermDbSygus;
 }
 
-class QuantifiersModule {
-protected:
-  QuantifiersEngine* d_quantEngine;
-public:
-  QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
-  virtual ~QuantifiersModule(){}
-  //get quantifiers engine
-  QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
-  /** presolve */
-  virtual void presolve() {}
-  /* whether this module needs to check this round */
-  virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
-  /* whether this module needs a model built */
-  virtual unsigned needsModel( Theory::Effort e );
-  /* reset at a round */
-  virtual void reset_round( Theory::Effort e ){}
-  /* Call during quantifier engine's check */
-  virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
-  /* check was complete (e.g. no lemmas implies a model) */
-  virtual bool checkComplete() { return true; }
-  /* Called for new quantified formulas */
-  virtual void preRegisterQuantifier( Node q ) { }
-  /* Called for new quantifiers after owners are finalized */
-  virtual void registerQuantifier( Node q ) = 0;
-  virtual void assertNode( Node n ) {}
-  virtual void propagate( Theory::Effort level ){}
-  virtual Node getNextDecisionRequest() { return TNode::null(); }
-  /** Identify this module (for debugging, dynamic configuration, etc..) */
-  virtual std::string identify() const = 0;
-public:
-  eq::EqualityEngine * getEqualityEngine();
-  bool areDisequal( TNode n1, TNode n2 );
-  bool areEqual( TNode n1, TNode n2 );
-  TNode getRepresentative( TNode n );
-  quantifiers::TermDb * getTermDatabase();
-};/* class QuantifiersModule */
-
 class InstantiationNotify {
 public:
   InstantiationNotify(){}
-  virtual void notifyInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+  virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
 };
 
 namespace quantifiers {
@@ -109,6 +72,7 @@ namespace quantifiers {
   class QuantDSplit;
   class QuantAntiSkolem;
   class EqualityInference;
+  class InstPropagator;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -132,6 +96,8 @@ class QuantifiersEngine {
 private:
   /** reference to theory engine object */
   TheoryEngine* d_te;
+  /** vector of utilities for quantifiers */
+  std::vector< QuantifiersUtil* > d_util;
   /** vector of modules for quantifiers */
   std::vector< QuantifiersModule* > d_modules;
   /** instantiation notify */
@@ -174,6 +140,8 @@ private:
   quantifiers::QuantDSplit * d_qsplit;
   /** quantifiers anti-skolemization */
   quantifiers::QuantAntiSkolem * d_anti_skolem;
+  /** quantifiers instantiation propagtor */
+  quantifiers::InstPropagator * d_inst_prop;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -427,11 +395,15 @@ private:
   Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */
   int getRepScore( Node n, Node f, int index, TypeNode v_tn );
+  /** flatten representatives */
+  void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
 public:
   EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
   virtual ~EqualityQueryQuantifiersEngine();
   /** reset */
   bool reset( Theory::Effort e );
+  /** identify */
+  std::string identify() const { return "EqualityQueryQE"; }
   /** general queries about equality */
   bool hasTerm( Node a );
   Node getRepresentative( Node a );
@@ -439,13 +411,12 @@ public:
   bool areDisequal( Node a, Node b );
   eq::EqualityEngine* getEngine();
   void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+  TNode getCongruentTerm( Node f, std::vector< TNode >& args );
   /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
       If cbqi is active, this will return a term in the equivalence class of "a" that does
       not contain instantiation constants, if such a term exists.
    */
   Node getInternalRepresentative( Node a, Node f, int index );
-  /** flatten representatives */
-  void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
   /** get quantifiers equality inference */
   quantifiers::EqualityInference * getEqualityInference() { return d_eq_inference; }
 }; /* EqualityQueryQuantifiersEngine */
-- 
cgit v1.2.3