From: ajreynol Date: Sat, 17 Sep 2016 00:06:05 +0000 (-0500) Subject: Use matching heuristics for EPR instantiation. X-Git-Tag: cvc5-1.0.0~6028^2~43^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=349c84b95cea084f28ff637c7cd4e99710692aeb;p=cvc5.git Use matching heuristics for EPR instantiation. --- diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 9e704691a..3fc589b5c 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -304,6 +304,8 @@ option cbqiNestedQE --cbqi-nested-qe bool :default false option quantEpr --quant-epr bool :default false :read-write infer whether in effectively propositional fragment, use for cbqi +option quantEprMatching --quant-epr-match bool :default true + use matching heuristics for EPR instantiation ### local theory extensions options diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 5876c7377..987b69522 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -21,7 +21,9 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" +#include "theory/quantifiers/term_database.h" #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" @@ -1379,17 +1381,16 @@ Node CegInstantiator::getModelValue( Node n ) { void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) { if( n.getKind()==FORALL ){ d_is_nested_quant = true; - }else{ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( TermDb::isBoolConnective( n.getKind() ) ){ - for( unsigned i=0; idoAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); + if( options::quantEprMatching() ){ + Assert( pv_coeff.isNull() ); + d_equal_terms.push_back( n ); + return false; + }else{ + return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); + } } +void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ) { + if( index==catom.getNumChildren() ){ + Assert( tat->hasNodeData() ); + Node gcatom = tat->getNodeData(); + Trace("epr-inst") << "Matched : " << catom << " and " << gcatom << std::endl; + for( unsigned i=0; i::iterator it = tat->d_data.find( arg_reps[index] ); + if( it!=tat->d_data.end() ){ + computeMatchScore( ci, pv, catom, arg_reps, &it->second, index+1, match_score ); + } + } +} + +void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) { + if( inst::Trigger::isAtomicTrigger( catom ) && TermDb::containsTerm( catom, pv ) ){ + Trace("epr-inst") << "Find matches for " << catom << "..." << std::endl; + std::vector< Node > arg_reps; + for( unsigned j=0; jgetQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( catom[j] ) ); + } + if( ci->getQuantifiersEngine()->getMasterEqualityEngine()->hasTerm( eqc ) ){ + Node rep = ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( eqc ); + Node op = ci->getQuantifiersEngine()->getTermDatabase()->getMatchOperator( catom ); + TermArgTrie * tat = ci->getQuantifiersEngine()->getTermDatabase()->getTermArgTrie( rep, op ); + Trace("epr-inst") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl; + if( tat ){ + computeMatchScore( ci, pv, catom, arg_reps, tat, 0, match_score ); + } + } + } +} + +struct sortEqTermsMatch { + std::map< Node, int > d_match_score; + bool operator() (Node i, Node j) { + int match_score_i = d_match_score[i]; + int match_score_j = d_match_score[j]; + return match_score_i>match_score_j || ( match_score_i==match_score_j && i& eqc, unsigned effort ) { - //TODO: heuristic for best matching constant + if( options::quantEprMatching() ){ + //heuristic for best matching constant + sortEqTermsMatch setm; + for( unsigned i=0; igetNumCEAtoms(); i++ ){ + Node catom = ci->getCEAtom( i ); + computeMatchScore( ci, pv, catom, catom, setm.d_match_score ); + } + //sort by match score + std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm ); + Node pv_coeff; + for( unsigned i=0; idoAddInstantiationInc( pv, d_equal_terms[i], pv_coeff, 0, sf, effort ) ){ + return true; + } + } + } return false; } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 3b949c237..259c604dc 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -140,8 +140,6 @@ private: Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ); void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); - //get model value - Node getModelValue( Node n ); private: int solve_arith( Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ); Node solve_dt( Node v, Node a, Node b, Node sa, Node sb ); @@ -157,9 +155,14 @@ public: //interface for instantiators public: + //get quantifiers engine + QuantifiersEngine* getQuantifiersEngine() { return d_qe; } void pushStackVariable( Node v ); void popStackVariable(); bool doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ); + Node getModelValue( Node n ); + unsigned getNumCEAtoms() { return d_ce_atoms.size(); } + Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; } }; @@ -237,10 +240,17 @@ public: std::string identify() const { return "Dt"; } }; +class TermArgTrie; + class EprInstantiator : public Instantiator { +private: + std::vector< Node > d_equal_terms; + void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ); + void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ); public: EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~EprInstantiator(){} + void reset( Node pv, unsigned effort ); bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); std::string identify() const { return "Epr"; } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index bac2aa35c..522f4dfce 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1853,7 +1853,7 @@ void MatchGen::setInvalid() { } bool MatchGen::isHandledBoolConnective( TNode n ) { - return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ); + return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ) && n.getKind()!=SEP_STAR; } bool MatchGen::isHandledUfTerm( TNode n ) { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index dee4952bd..ff11babc9 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1958,7 +1958,7 @@ bool TermDb::isComm( Kind k ) { } bool TermDb::isBoolConnective( Kind k ) { - return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT; + return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT || k==SEP_STAR; } void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){