From: Andrew Reynolds Date: Tue, 9 Jul 2013 20:43:28 +0000 (-0500) Subject: add relevant domain computation X-Git-Tag: cvc5-1.0.0~7287^2~71 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a15f4a0e27ab42fb49f1d0cc9197e286862b8426;p=cvc5.git add relevant domain computation --- diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 0339fbcd8..80011868b 100644 --- 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 0678e230f..cb8cb8154 100644 --- 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 20c677e9c..686a2cc13 100644 --- 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 index 000000000..96d30bf37 --- /dev/null +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -0,0 +1,182 @@ +/********************* */ +/*! \file relevant_domain.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of relevant domain class + **/ + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +void RelevantDomain::RDomain::merge( RDomain * r ) { + Assert( !d_parent ); + Assert( !r->d_parent ); + d_parent = r; + for( unsigned i=0; iaddTerm( d_terms[i] ); + } + d_terms.clear(); +} + +void RelevantDomain::RDomain::addTerm( Node t ) { + if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){ + d_terms.push_back( t ); + } +} + +RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() { + if( !d_parent ){ + return this; + }else{ + RDomain * p = d_parent->getParent(); + d_parent = p; + return p; + } +} + +void RelevantDomain::RDomain::removeRedundantTerms( FirstOrderModel * fm ) { + std::map< Node, Node > rterms; + for( unsigned i=0; igetRepresentative( d_terms[i] ); + } + if( rterms.find( r )==rterms.end() ){ + rterms[r] = d_terms[i]; + } + } + d_terms.clear(); + for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){ + d_terms.push_back( it->second ); + } +} + + + +RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){ + +} + +RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i ) { + if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){ + d_rel_doms[n][i] = new RDomain; + d_rn_map[d_rel_doms[n][i]] = n; + d_ri_map[d_rel_doms[n][i]] = i; + } + return d_rel_doms[n][i]->getParent(); +} + +void RelevantDomain::compute(){ + for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){ + for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + it2->second->reset(); + } + } + for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ + Node f = d_model->getAssertedQuantifier( i ); + Node icf = d_qe->getTermDatabase()->getInstConstantBody( f ); + Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl; + computeRelevantDomain( icf, true, true ); + } + + Trace("rel-dom-debug") << "account for ground terms" << std::endl; + for( std::map< Node, std::vector< Node > >::iterator it = d_model->d_uf_terms.begin(); it != d_model->d_uf_terms.end(); ++it ){ + Node op = it->first; + for( unsigned i=0; isecond.size(); i++ ){ + Node n = it->second[i]; + //if it is a non-redundant term + if( !n.getAttribute(NoMatchAttribute()) ){ + for( unsigned j=0; jaddTerm( n[j] ); + } + } + } + } + //print debug + for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){ + Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl; + for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + Trace("rel-dom") << " " << it2->first << " : "; + RDomain * r = it2->second; + RDomain * rp = r->getParent(); + if( r==rp ){ + r->removeRedundantTerms( d_model ); + for( unsigned i=0; id_terms.size(); i++ ){ + Trace("rel-dom") << r->d_terms[i] << " "; + } + }else{ + Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) "; + } + Trace("rel-dom") << std::endl; + } + } + +} + +void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { + + for( unsigned i=0; igetTermDatabase()->getInstConstAttr( n[i] ); + //merge the RDomains + unsigned id = n[i].getAttribute(InstVarNumAttribute()); + Trace("rel-dom-debug") << n[i] << " is variable # " << id << " for " << q; + Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl; + RDomain * rq = getRDomain( q, id ); + if( rf!=rq ){ + rq->merge( rf ); + } + }else{ + //term to add + rf->addTerm( n[i] ); + } + } + + //TODO + if( n[i].getKind()!=FORALL ){ + bool newHasPol = hasPol; + bool newPol = pol; + computeRelevantDomain( n[i], newHasPol, newPol ); + } + } +} + +Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) { + RDomain * rf = getRDomain( f, i ); + Trace("rel-dom-debug") << "Get relevant domain " << rf << " " << r << std::endl; + if( !d_qe->getEqualityQuery()->getEngine()->hasTerm( r ) || rf->hasTerm( r ) ){ + return r; + }else{ + Node rr = d_model->getRepresentative( r ); + eq::EqClassIterator eqc( rr, d_qe->getEqualityQuery()->getEngine() ); + while( !eqc.isFinished() ){ + Node en = (*eqc); + if( rf->hasTerm( en ) ){ + return en; + } + ++eqc; + } + //otherwise, may be equal to some non-ground term + + return 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 index 000000000..5939ec727 --- /dev/null +++ b/src/theory/quantifiers/relevant_domain.h @@ -0,0 +1,62 @@ +/********************* */ +/*! \file relevant_domain.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief relevant domain class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H +#define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H + +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class RelevantDomain +{ +private: + class RDomain + { + public: + RDomain() : d_parent( NULL ) {} + void reset() { d_parent = NULL; d_terms.clear(); } + RDomain * d_parent; + std::vector< Node > d_terms; + void merge( RDomain * r ); + void addTerm( Node t ); + RDomain * getParent(); + void removeRedundantTerms( FirstOrderModel * fm ); + bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); } + }; + std::map< Node, std::map< int, RDomain * > > d_rel_doms; + std::map< RDomain *, Node > d_rn_map; + std::map< RDomain *, int > d_ri_map; + RDomain * getRDomain( Node n, int i ); + QuantifiersEngine* d_qe; + FirstOrderModel* d_model; + void computeRelevantDomain( Node n, bool hasPol, bool pol ); +public: + RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ); + virtual ~RelevantDomain(){} + //compute the relevant domain + void compute(); + + Node getRelevantTerm( Node f, int i, Node r ); +};/* class RelevantDomain */ + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 94bc475d0..bc1a6929d 100644 --- 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; igetTheoryEngine()->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; igetTheoryEngine()->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=0 && ( r_best_score<0 || score