add relevant domain computation

diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 0339fbcd8759cb0e9ed55a1c4005ccb187134e74..80011868bcd903ab961e29e683b2c47cfa8cd504 100644 (file)
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -50,7 +50,9 @@ libquantifiers_la_SOURCES = \
        first_order_reasoning.h \
        first_order_reasoning.cpp \
        rewrite_engine.h \
-       rewrite_engine.cpp
+       rewrite_engine.cpp \
+       relevant_domain.h \
+       relevant_domain.cpp
 
 EXTRA_DIST = \
        kinds \

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 0678e230f339255ba564cee697a693fa4143680d..cb8cb8154a9055e5fcfd57f81eecc561ae41e998 100644 (file)
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -42,6 +42,11 @@ QuantifiersModule( qe ){
     d_builder = new QModelBuilderDefault( c, qe );
   }
 
+  if( options::fmfRelevantDomain() ){
+    d_rel_dom = new RelevantDomain( qe, qe->getModel() );
+  }else{
+    d_rel_dom = NULL;
+  }
 }
 
 void ModelEngine::check( Theory::Effort e ){
@@ -153,6 +158,9 @@ int ModelEngine::checkModel(){
     }
   }
   //relevant domain?
+  if( d_rel_dom ){
+    d_rel_dom->compute();
+  }
 
   d_triedLemmas = 0;
   d_addedLemmas = 0;

diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 20c677e9ceb8a76b630dd62b10245cf57922b8e3..686a2cc130f346ca5b65d146a5c7c39cb814905b 100644 (file)
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/model_builder.h"
 #include "theory/model.h"
 #include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
 namespace theory {
@@ -33,6 +34,7 @@ private:
   /** builder class */
   QModelBuilder* d_builder;
 private:    //analysis of current model:
+  RelevantDomain* d_rel_dom;
 private:
   //options
   bool optOneQuantPerRound();
@@ -51,8 +53,10 @@ private:
 public:
   ModelEngine( context::Context* c, QuantifiersEngine* qe );
   ~ModelEngine(){}
+  //get relevant domain
+  RelevantDomain * getRelevantDomain() { return d_rel_dom; }
   //get the builder
-  QModelBuilder* getModelBuilder() { return d_builder; }
+  QModelBuilder * getModelBuilder() { return d_builder; }
 public:
   void check( Theory::Effort e );
   void registerQuantifier( Node f );

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
new file mode 100755 (executable)
index 0000000..96d30bf
--- /dev/null
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -0,0 +1,182 @@
+/*********************                                                        */\r
+/*! \file relevant_domain.cpp\r
+ ** \verbatim\r
+ ** Original author: Andrew Reynolds\r
+ ** Major contributors: Morgan Deters\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Implementation of relevant domain class\r
+ **/\r
+\r
+#include "theory/quantifiers_engine.h"\r
+#include "theory/quantifiers/relevant_domain.h"\r
+#include "theory/quantifiers/term_database.h"\r
+#include "theory/quantifiers/first_order_model.h"\r
+\r
+using namespace std;\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace CVC4::context;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::quantifiers;\r
+\r
+void RelevantDomain::RDomain::merge( RDomain * r ) {\r
+  Assert( !d_parent );\r
+  Assert( !r->d_parent );\r
+  d_parent = r;\r
+  for( unsigned i=0; i<d_terms.size(); i++ ){\r
+    r->addTerm( d_terms[i] );\r
+  }\r
+  d_terms.clear();\r
+}\r
+\r
+void RelevantDomain::RDomain::addTerm( Node t ) {\r
+  if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){\r
+    d_terms.push_back( t );\r
+  }\r
+}\r
+\r
+RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() {\r
+  if( !d_parent ){\r
+    return this;\r
+  }else{\r
+    RDomain * p = d_parent->getParent();\r
+    d_parent = p;\r
+    return p;\r
+  }\r
+}\r
+\r
+void RelevantDomain::RDomain::removeRedundantTerms( FirstOrderModel * fm ) {\r
+  std::map< Node, Node > rterms;\r
+  for( unsigned i=0; i<d_terms.size(); i++ ){\r
+    Node r = d_terms[i];\r
+    if( !TermDb::hasInstConstAttr( d_terms[i] ) ){\r
+      r = fm->getRepresentative( d_terms[i] );\r
+    }\r
+    if( rterms.find( r )==rterms.end() ){\r
+      rterms[r] = d_terms[i];\r
+    }\r
+  }\r
+  d_terms.clear();\r
+  for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){\r
+    d_terms.push_back( it->second );\r
+  }\r
+}\r
+\r
+\r
+\r
+RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){\r
+\r
+}\r
+\r
+RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i ) {\r
+  if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){\r
+    d_rel_doms[n][i] = new RDomain;\r
+    d_rn_map[d_rel_doms[n][i]] = n;\r
+    d_ri_map[d_rel_doms[n][i]] = i;\r
+  }\r
+  return d_rel_doms[n][i]->getParent();\r
+}\r
+\r
+void RelevantDomain::compute(){\r
+  for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){\r
+    for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
+      it2->second->reset();\r
+    }\r
+  }\r
+  for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){\r
+    Node f = d_model->getAssertedQuantifier( i );\r
+    Node icf = d_qe->getTermDatabase()->getInstConstantBody( f );\r
+    Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;\r
+    computeRelevantDomain( icf, true, true );\r
+  }\r
+\r
+  Trace("rel-dom-debug") << "account for ground terms" << std::endl;\r
+  for( std::map< Node, std::vector< Node > >::iterator it = d_model->d_uf_terms.begin(); it != d_model->d_uf_terms.end(); ++it ){\r
+    Node op = it->first;\r
+    for( unsigned i=0; i<it->second.size(); i++ ){\r
+      Node n = it->second[i];\r
+      //if it is a non-redundant term\r
+      if( !n.getAttribute(NoMatchAttribute()) ){\r
+        for( unsigned j=0; j<n.getNumChildren(); j++ ){\r
+          RDomain * rf = getRDomain( op, j );\r
+          rf->addTerm( n[j] );\r
+        }\r
+      }\r
+    }\r
+  }\r
+  //print debug\r
+  for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){\r
+    Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl;\r
+    for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
+      Trace("rel-dom") << "   " << it2->first << " : ";\r
+      RDomain * r = it2->second;\r
+      RDomain * rp = r->getParent();\r
+      if( r==rp ){\r
+        r->removeRedundantTerms( d_model );\r
+        for( unsigned i=0; i<r->d_terms.size(); i++ ){\r
+          Trace("rel-dom") << r->d_terms[i] << " ";\r
+        }\r
+      }else{\r
+        Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) ";\r
+      }\r
+      Trace("rel-dom") << std::endl;\r
+    }\r
+  }\r
+\r
+}\r
+\r
+void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {\r
+\r
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+    if( n.getKind()==APPLY_UF ){\r
+      RDomain * rf = getRDomain( n.getOperator(), i );\r
+      if( n[i].getKind()==INST_CONSTANT ){\r
+        Node q = d_qe->getTermDatabase()->getInstConstAttr( n[i] );\r
+        //merge the RDomains\r
+        unsigned id = n[i].getAttribute(InstVarNumAttribute());\r
+        Trace("rel-dom-debug") << n[i] << " is variable # " << id << " for " << q;\r
+        Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl;\r
+        RDomain * rq = getRDomain( q, id );\r
+        if( rf!=rq ){\r
+          rq->merge( rf );\r
+        }\r
+      }else{\r
+        //term to add\r
+        rf->addTerm( n[i] );\r
+      }\r
+    }\r
+\r
+    //TODO\r
+    if( n[i].getKind()!=FORALL ){\r
+      bool newHasPol = hasPol;\r
+      bool newPol = pol;\r
+      computeRelevantDomain( n[i], newHasPol, newPol );\r
+    }\r
+  }\r
+}\r
+\r
+Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) {\r
+  RDomain * rf = getRDomain( f, i );\r
+  Trace("rel-dom-debug") << "Get relevant domain " << rf << " " << r << std::endl;\r
+  if( !d_qe->getEqualityQuery()->getEngine()->hasTerm( r ) || rf->hasTerm( r ) ){\r
+    return r;\r
+  }else{\r
+    Node rr = d_model->getRepresentative( r );\r
+    eq::EqClassIterator eqc( rr, d_qe->getEqualityQuery()->getEngine() );\r
+    while( !eqc.isFinished() ){\r
+      Node en = (*eqc);\r
+      if( rf->hasTerm( en ) ){\r
+        return en;\r
+      }\r
+      ++eqc;\r
+    }\r
+    //otherwise, may be equal to some non-ground term\r
+\r
+    return r;\r
+  }\r
+}
\ No newline at end of file

diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
new file mode 100755 (executable)
index 0000000..5939ec7
--- /dev/null
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -0,0 +1,62 @@
+/*********************                                                        */\r
+/*! \file relevant_domain.h\r
+ ** \verbatim\r
+ ** Original author: Andrew Reynolds\r
+ ** Major contributors: Morgan Deters\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief relevant domain class\r
+ **/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H\r
+#define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H\r
+\r
+#include "theory/quantifiers/first_order_model.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace quantifiers {\r
+\r
+class RelevantDomain\r
+{\r
+private:\r
+  class RDomain\r
+  {\r
+  public:\r
+    RDomain() : d_parent( NULL ) {}\r
+    void reset() { d_parent = NULL; d_terms.clear(); }\r
+    RDomain * d_parent;\r
+    std::vector< Node > d_terms;\r
+    void merge( RDomain * r );\r
+    void addTerm( Node t );\r
+    RDomain * getParent();\r
+    void removeRedundantTerms( FirstOrderModel * fm );\r
+    bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); }\r
+  };\r
+  std::map< Node, std::map< int, RDomain * > > d_rel_doms;\r
+  std::map< RDomain *, Node > d_rn_map;\r
+  std::map< RDomain *, int > d_ri_map;\r
+  RDomain * getRDomain( Node n, int i );\r
+  QuantifiersEngine* d_qe;\r
+  FirstOrderModel* d_model;\r
+  void computeRelevantDomain( Node n, bool hasPol, bool pol );\r
+public:\r
+  RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );\r
+  virtual ~RelevantDomain(){}\r
+  //compute the relevant domain\r
+  void compute();\r
+\r
+  Node getRelevantTerm( Node f, int i, Node r );\r
+};/* class RelevantDomain */\r
+\r
+}/* CVC4::theory::quantifiers namespace */\r
+}/* CVC4::theory namespace */\r
+}/* CVC4 namespace */\r
+\r
+#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */\r

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 94bc475d0afaac5d48b1a2af6a35a467f7028209..bc1a6929d2bbb158671a6e70a093a5890aeae5ac 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -640,32 +640,38 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
       sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] );
     }
     if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){
-      std::vector< Node > eqc;
-      getEquivalenceClass( r, eqc );
       //find best selection for representative
       Node r_best;
-      int r_best_score = -1;
-      for( size_t i=0; i<eqc.size(); i++ ){
-        int score = getRepScore( eqc[i], f, index );
-        if( optInternalRepSortInference() ){
-          int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]);
-          if( score>=0 && e_sortId!=sortId ){
-            score += 100;
+      if( options::fmfRelevantDomain() ){
+        Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
+        r_best = d_qe->getModelEngine()->getRelevantDomain()->getRelevantTerm( f, index, r );
+        Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
+      }else{
+        std::vector< Node > eqc;
+        getEquivalenceClass( r, eqc );
+        int r_best_score = -1;
+        for( size_t i=0; i<eqc.size(); i++ ){
+          int score = getRepScore( eqc[i], f, index );
+          if( optInternalRepSortInference() ){
+            int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]);
+            if( score>=0 && e_sortId!=sortId ){
+              score += 100;
+            }
+          }
+          //score prefers earliest use of this term as a representative
+          if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
+            r_best = eqc[i];
+            r_best_score = score;
           }
         }
-        //score prefers earliest use of this term as a representative
-        if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
-          r_best = eqc[i];
-          r_best_score = score;
+        //now, make sure that no other member of the class is an instance
+        if( !optInternalRepSortInference() ){
+          r_best = getInstance( r_best, eqc );
+        }
+        //store that this representative was chosen at this point
+        if( d_rep_score.find( r_best )==d_rep_score.end() ){
+          d_rep_score[ r_best ] = d_reset_count;
         }
-      }
-      //now, make sure that no other member of the class is an instance
-      if( !optInternalRepSortInference() ){
-        r_best = getInstance( r_best, eqc );
-      }
-      //store that this representative was chosen at this point
-      if( d_rep_score.find( r_best )==d_rep_score.end() ){
-        d_rep_score[ r_best ] = d_reset_count;
       }
       d_int_rep[sortId][r] = r_best;
       if( r_best!=a ){