From a2bba0806dab0e0d4728bbba8e4e6b4160335eeb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Nov 2018 15:39:13 -0600 Subject: [PATCH] Make (T)NodeTrie a general utility (#2489) This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it. --- src/expr/CMakeLists.txt | 2 + src/expr/node_trie.cpp | 95 +++++++++++++++ src/expr/node_trie.h | 112 ++++++++++++++++++ src/theory/datatypes/theory_datatypes.cpp | 53 +++++---- src/theory/datatypes/theory_datatypes.h | 12 +- .../cegqi/ceg_epr_instantiator.cpp | 10 +- .../quantifiers/cegqi/ceg_epr_instantiator.h | 5 +- .../quantifiers/conjecture_generator.cpp | 2 +- src/theory/quantifiers/conjecture_generator.h | 7 +- .../ematching/candidate_generator.cpp | 2 +- .../ematching/inst_match_generator.cpp | 23 ++-- .../ematching/inst_match_generator.h | 6 +- src/theory/quantifiers/inst_propagator.h | 28 +++-- src/theory/quantifiers/local_theory_ext.cpp | 30 ++++- src/theory/quantifiers/local_theory_ext.h | 18 ++- .../quantifiers/quant_conflict_find.cpp | 8 +- src/theory/quantifiers/quant_conflict_find.h | 6 +- src/theory/quantifiers/term_database.cpp | 58 ++------- src/theory/quantifiers/term_database.h | 78 ++---------- src/theory/sets/theory_sets_private.cpp | 48 +++++--- src/theory/sets/theory_sets_private.h | 19 ++- src/theory/strings/theory_strings.cpp | 47 +++++--- src/theory/strings/theory_strings.h | 11 +- src/theory/uf/theory_uf.cpp | 50 +++++--- src/theory/uf/theory_uf.h | 19 ++- 25 files changed, 465 insertions(+), 284 deletions(-) create mode 100644 src/expr/node_trie.cpp create mode 100644 src/expr/node_trie.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 35ef34dfa..61ab7b3fb 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -27,6 +27,8 @@ libcvc4_add_sources( node_manager_listeners.cpp node_manager_listeners.h node_self_iterator.h + node_trie.cpp + node_trie.h node_value.cpp node_value.h pickle_data.cpp diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp new file mode 100644 index 000000000..4404e78ca --- /dev/null +++ b/src/expr/node_trie.cpp @@ -0,0 +1,95 @@ +/********************* */ +/*! \file node_trie.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of a trie class for Nodes and TNodes. + **/ + +#include "expr/node_trie.h" + +namespace CVC4 { +namespace theory { + +template +NodeTemplate NodeTemplateTrie::existsTerm( + const std::vector>& reps) const +{ + const NodeTemplateTrie* tnt = this; + typename std::map, + NodeTemplateTrie>::const_iterator it; + for (const NodeTemplate r : reps) + { + it = tnt->d_data.find(r); + if (it == tnt->d_data.end()) + { + // didn't find this child, return null + return Node::null(); + } + tnt = &it->second; + } + if (tnt->d_data.empty()) + { + return Node::null(); + } + return tnt->d_data.begin()->first; +} + +template TNode NodeTemplateTrie::existsTerm( + const std::vector& reps) const; +template Node NodeTemplateTrie::existsTerm( + const std::vector& reps) const; + +template +NodeTemplate NodeTemplateTrie::addOrGetTerm( + NodeTemplate n, const std::vector>& reps) +{ + NodeTemplateTrie* tnt = this; + for (const NodeTemplate r : reps) + { + tnt = &(tnt->d_data[r]); + } + if (tnt->d_data.empty()) + { + // Store n in d_data. This should be interpretted as the "data" and not as a + // reference to a child. + tnt->d_data[n].clear(); + return n; + } + return tnt->d_data.begin()->first; +} + +template TNode NodeTemplateTrie::addOrGetTerm( + TNode n, const std::vector& reps); +template Node NodeTemplateTrie::addOrGetTerm( + Node n, const std::vector& reps); + +template +void NodeTemplateTrie::debugPrint(const char* c, + unsigned depth) const +{ + for (const std::pair, + NodeTemplateTrie>& p : d_data) + { + for (unsigned i = 0; i < depth; i++) + { + Trace(c) << " "; + } + Trace(c) << p.first << std::endl; + p.second.debugPrint(c, depth + 1); + } +} + +template void NodeTemplateTrie::debugPrint(const char* c, + unsigned depth) const; +template void NodeTemplateTrie::debugPrint(const char* c, + unsigned depth) const; + +} // namespace theory +} // namespace CVC4 diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h new file mode 100644 index 000000000..d0c0f0627 --- /dev/null +++ b/src/expr/node_trie.h @@ -0,0 +1,112 @@ +/********************* */ +/*! \file node_trie.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A trie class for Nodes and TNodes. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__EXPR__NODE_TRIE_H +#define __CVC4__EXPR__NODE_TRIE_H + +#include +#include "expr/node.h" + +namespace CVC4 { +namespace theory { + +/** NodeTemplate trie class + * + * This is a trie data structure whose distinguishing feature is that it has + * no "data" members and only references to children. The motivation for having + * no data members is efficiency. + * + * One use of this class is to represent "term indices" or a "signature tables" + * for symbols with fixed arities. In this use case, we "index" terms by the + * list of representatives of their arguments. + * + * For example, consider the equivalence classes : + * + * { a, d, f( d, c ), f( a, c ) } + * { b, f( b, d ) } + * { c, f( b, b ) } + * + * where the first elements ( a, b, c ) are the representatives of these + * classes. The NodeTemplateTrie t we may build for f is : + * + * t : + * t.d_data[a] : + * t.d_data[a].d_data[c] : + * t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf) + * t.d_data[b] : + * t.d_data[b].d_data[b] : + * t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf) + * t.d_data[b].d_data[d] : + * t.d_data[b].d_data[d].d_data[f(b,d)] : (leaf) + * + * Leaf nodes store the terms that are indexed by the arguments, for example + * term f(d,c) is indexed by the representative arguments (a,c), and is stored + * as a the (single) key in the data of t.d_data[a].d_data[c]. + */ +template +class NodeTemplateTrie +{ + public: + /** The children of this node. */ + std::map, NodeTemplateTrie> d_data; + /** For leaf nodes : does this node have data? */ + bool hasData() const { return !d_data.empty(); } + /** For leaf nodes : get the node corresponding to this leaf. */ + NodeTemplate getData() const { return d_data.begin()->first; } + /** + * Returns the term that is indexed by reps, if one exists, or + * or returns null otherwise. + */ + NodeTemplate existsTerm( + const std::vector>& reps) const; + /** + * Returns the term that is previously indexed by reps, if one exists, or + * adds n to the trie, indexed by reps, and returns n. + */ + NodeTemplate addOrGetTerm( + NodeTemplate n, + const std::vector>& reps); + /** + * Returns false if a term is previously indexed by reps. + * Returns true if no term is previously indexed by reps, + * and adds n to the trie, indexed by reps. + */ + inline bool addTerm(NodeTemplate n, + const std::vector>& reps); + /** Debug print this trie on Trace c with indentation depth. */ + void debugPrint(const char* c, unsigned depth = 0) const; + /** Clear all data from this trie. */ + void clear() { d_data.clear(); } + /** Is this trie empty? */ + bool empty() const { return d_data.empty(); } +}; /* class NodeTemplateTrie */ + +template +bool NodeTemplateTrie::addTerm( + NodeTemplate n, const std::vector>& reps) +{ + return addOrGetTerm(n, reps) == n; +} + +/** Reference-counted version of the above data structure */ +typedef NodeTemplateTrie NodeTrie; +/** Non-reference-counted version of the above data structure */ +typedef NodeTemplateTrie TNodeTrie; + +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__EXPR__NODE_TRIE_H */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 77579489a..5ed623190 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -26,7 +26,6 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/term_database.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" #include "theory/valuation.h" @@ -1334,13 +1333,16 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){ return EQUALITY_FALSE_IN_MODEL; } - - -void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ){ +void TheoryDatatypes::addCarePairs(TNodeTrie* t1, + TNodeTrie* t2, + unsigned arity, + unsigned depth, + unsigned& n_pairs) +{ if( depth==arity ){ if( t2!=NULL ){ - Node f1 = t1->getNodeData(); - Node f2 = t2->getNodeData(); + Node f1 = t1->getData(); + Node f2 = t2->getData(); if( !areEqual( f1, f2 ) ){ Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl; vector< pair > currentPairs; @@ -1371,13 +1373,17 @@ void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers:: if( t2==NULL ){ if( depth<(arity-1) ){ //add care pairs internal to each child - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - addCarePairs( &it->second, NULL, arity, depth+1, n_pairs ); + for (std::pair& tt : t1->d_data) + { + addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs); } } //add care pairs based on each pair of non-disequal arguments - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it; + for (std::map::iterator it = t1->d_data.begin(); + it != t1->d_data.end(); + ++it) + { + std::map::iterator it2 = it; ++it2; for( ; it2 != t1->d_data.end(); ++it2 ){ if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ @@ -1389,11 +1395,15 @@ void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers:: } }else{ //add care pairs based on product of indices, non-disequal arguments - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){ - if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ - if( !areCareDisequal(it->first, it2->first) ){ - addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs ); + for (std::pair& tt1 : t1->d_data) + { + for (std::pair& tt2 : t2->d_data) + { + if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false)) + { + if (!areCareDisequal(tt1.first, tt2.first)) + { + addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs); } } } @@ -1406,7 +1416,7 @@ void TheoryDatatypes::computeCareGraph(){ unsigned n_pairs = 0; Trace("dt-cg-summary") << "Compute graph for dt..." << d_functionTerms.size() << " " << d_sharedTerms.size() << std::endl; Trace("dt-cg") << "Build indices..." << std::endl; - std::map< TypeNode, std::map< Node, quantifiers::TermArgTrie > > index; + std::map > index; std::map< Node, unsigned > arity; //populate indices unsigned functionTerms = d_functionTerms.size(); @@ -1432,10 +1442,13 @@ void TheoryDatatypes::computeCareGraph(){ } } //for each index - for( std::map< TypeNode, std::map< Node, quantifiers::TermArgTrie > >::iterator iti = index.begin(); iti != index.end(); ++iti ){ - for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = iti->second.begin(); itii != iti->second.end(); ++itii ){ - Trace("dt-cg") << "Process index " << itii->first << ", " << iti->first << "..." << std::endl; - addCarePairs( &itii->second, NULL, arity[ itii->first ], 0, n_pairs ); + for (std::pair >& tt : index) + { + for (std::pair& t : tt.second) + { + Trace("dt-cg") << "Process index " << tt.first << ", " << t.first << "..." + << std::endl; + addCarePairs(&t.second, nullptr, arity[t.first], 0, n_pairs); } } Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 0a3017058..a7b40e282 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -25,6 +25,7 @@ #include "context/cdlist.h" #include "expr/attribute.h" #include "expr/datatype.h" +#include "expr/node_trie.h" #include "theory/datatypes/datatypes_sygus.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -32,11 +33,6 @@ namespace CVC4 { namespace theory { - -namespace quantifiers{ - class TermArgTrie; -} - namespace datatypes { class TheoryDatatypes : public Theory { @@ -253,7 +249,11 @@ private: TNode getEqcConstructor( TNode r ); protected: - void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ); + void addCarePairs(TNodeTrie* t1, + TNodeTrie* t2, + unsigned arity, + unsigned depth, + unsigned& n_pairs); /** compute care graph */ void computeCareGraph() override; diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp index 3535b57b7..df6690273 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp @@ -107,14 +107,14 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci, Node pv, Node catom, std::vector& arg_reps, - TermArgTrie* tat, + TNodeTrie* tat, unsigned index, std::map& match_score) { if (index == catom.getNumChildren()) { - Assert(tat->hasNodeData()); - Node gcatom = tat->getNodeData(); + Assert(tat->hasData()); + Node gcatom = tat->getData(); Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom << std::endl; for (unsigned i = 0, nchild = catom.getNumChildren(); i < nchild; i++) @@ -132,7 +132,7 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci, } return; } - std::map::iterator it = tat->d_data.find(arg_reps[index]); + std::map::iterator it = tat->d_data.find(arg_reps[index]); if (it != tat->d_data.end()) { computeMatchScore( @@ -165,7 +165,7 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci, TermDb* tdb = ci->getQuantifiersEngine()->getTermDatabase(); Node rep = ee->getRepresentative(eqc); Node op = tdb->getMatchOperator(catom); - TermArgTrie* tat = tdb->getTermArgTrie(rep, op); + TNodeTrie* tat = tdb->getTermArgTrie(rep, op); Trace("cegqi-epr") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat != NULL) << std::endl; if (tat) diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h index b4378e1d2..f5057ad86 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h @@ -19,14 +19,13 @@ #include #include +#include "expr/node_trie.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" namespace CVC4 { namespace theory { namespace quantifiers { -class TermArgTrie; - /** Effectively Propositional (EPR) Instantiator * * This implements a selection function for the EPR fragment. @@ -93,7 +92,7 @@ class EprInstantiator : public Instantiator Node pv, Node catom, std::vector& arg_reps, - TermArgTrie* tat, + TNodeTrie* tat, unsigned index, std::map& match_score); void computeMatchScore(CegInstantiator* ci, diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 1d2f9a322..7408678e7 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1630,7 +1630,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, //initial binding TNode f = s->getTgFunc( d_typ, d_status_num ); Assert( !eqc.isNull() ); - TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f ); + TNodeTrie* tat = s->getTermDatabase()->getTermArgTrie(eqc, f); if( tat ){ d_match_children.push_back( tat->d_data.begin() ); d_match_children_end.push_back( tat->d_data.end() ); diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 450bd7991..8fff7eafe 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -18,6 +18,7 @@ #define CONJECTURE_GENERATOR_H #include "context/cdhashmap.h" +#include "expr/node_trie.h" #include "theory/quantifiers_engine.h" #include "theory/type_enumerator.h" @@ -25,8 +26,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class TermArgTrie; - //algorithm for computing candidate subgoals class ConjectureGenerator; @@ -105,8 +104,8 @@ class TermGenerator //2 : variables must map to non-ground terms unsigned d_match_mode; //children - std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children; - std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children_end; + std::vector::iterator> d_match_children; + std::vector::iterator> d_match_children_end; void reset( TermGenEnv * s, TypeNode tn ); bool getNextTerm( TermGenEnv * s, unsigned depth ); diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 3f404c17f..612a1938a 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -57,7 +57,7 @@ void CandidateGeneratorQE::reset( Node eqc ){ }else{ eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); if( ee->hasTerm( eqc ) ){ - quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op ); + TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, d_op); if( tat ){ //create an equivalence class iterator in eq class eqc Node rep = ee->getRepresentative( eqc ); diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 646208ec6..f26df5b79 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -1028,7 +1028,7 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, Trigger* tparent) { int addedLemmas = 0; - quantifiers::TermArgTrie* tat; + TNodeTrie* tat; if( d_eqc.isNull() ){ tat = qe->getTermDatabase()->getTermArgTrie( d_op ); }else{ @@ -1040,10 +1040,12 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, if (tat && !qe->inConflict()) { Node r = qe->getEqualityQuery()->getRepresentative(d_eqc); - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - if( it->first!=r ){ + for (std::pair& t : tat->d_data) + { + if (t.first != r) + { InstMatch m( q ); - addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); + addInstantiations(m, qe, addedLemmas, 0, &(t.second)); if( qe->inConflict() ){ break; } @@ -1066,13 +1068,13 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, unsigned argIndex, - quantifiers::TermArgTrie* tat) + TNodeTrie* tat) { Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl; if (argIndex == d_match_pattern.getNumChildren()) { Assert( !tat->d_data.empty() ); - TNode t = tat->getNodeData(); + TNode t = tat->getData(); Debug("simple-trigger") << "Actual term is " << t << std::endl; //convert to actual used terms for (std::map::iterator it = d_var_num.begin(); @@ -1096,14 +1098,15 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){ int v = d_var_num[argIndex]; if( v!=-1 ){ - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - Node t = it->first; + for (std::pair& tt : tat->d_data) + { + Node t = tt.first; Node prev = m.get( v ); //using representatives, just check if equal Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) ); if( prev.isNull() || prev==t ){ m.setValue( v, t); - addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); + addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second)); m.setValue( v, prev); if( qe->inConflict() ){ break; @@ -1115,7 +1118,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, //inst constant from another quantified formula, treat as ground term TODO: remove this? } Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); - std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); + std::map::iterator it = tat->d_data.find(r); if( it!=tat->d_data.end() ){ addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); } diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index abf269f3e..83d4ce82e 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -18,15 +18,13 @@ #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H #include +#include "expr/node_trie.h" #include "theory/quantifiers/inst_match_trie.h" namespace CVC4 { namespace theory { class QuantifiersEngine; -namespace quantifiers{ - class TermArgTrie; -} namespace inst { @@ -662,7 +660,7 @@ class InstMatchGeneratorSimple : public IMGenerator { QuantifiersEngine* qe, int& addedLemmas, unsigned argIndex, - quantifiers::TermArgTrie* tat); + TNodeTrie* tat); };/* class InstMatchGeneratorSimple */ } } diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index dc1bf6908..1ba359228 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -22,9 +22,9 @@ #include #include #include "expr/node.h" +#include "expr/node_trie.h" #include "expr/type_node.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -72,17 +72,21 @@ public: TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp ); private: /** term index */ - std::map< Node, TermArgTrie > d_uf_func_map_trie; - /** union find for terms beyond what is stored in equality engine */ - std::map< Node, Node > d_uf; - std::map< Node, std::vector< Node > > d_uf_exp; - Node getUfRepresentative( Node a, std::vector< Node >& exp ); - /** disequality list, stores explanations */ - std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list; - /** add arg */ - void addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch ); - /** register term */ - void registerUfTerm( TNode n ); + std::map d_uf_func_map_trie; + /** union find for terms beyond what is stored in equality engine */ + std::map d_uf; + std::map > d_uf_exp; + Node getUfRepresentative(Node a, std::vector& exp); + /** disequality list, stores explanations */ + std::map > > d_diseq_list; + /** add arg */ + void addArgument(Node n, + std::vector& args, + std::vector& watch, + bool is_watch); + /** register term */ + void registerUfTerm(TNode n); + public: enum { STATUS_CONFLICT, diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index 93b220ea9..752d61489 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -196,9 +196,17 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { } } -void LtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, - std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, TermArgTrie * curr, - unsigned pindex, unsigned paindex, unsigned iindex ){ +void LtePartialInst::getPartialInstantiations(std::vector& conj, + Node q, + Node bvl, + std::vector& vars, + std::vector& terms, + std::vector& types, + TNodeTrie* curr, + unsigned pindex, + unsigned paindex, + unsigned iindex) +{ if( iindex==vars.size() ){ Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); if( bvl.isNull() ){ @@ -231,9 +239,19 @@ void LtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q //start traversing term index for the operator curr = d_quantEngine->getTermDatabase()->getTermArgTrie( pat.getOperator() ); } - for( std::map< TNode, TermArgTrie >::iterator it = curr->d_data.begin(); it != curr->d_data.end(); ++it ){ - terms[d_pat_var_order[q][iindex]] = it->first; - getPartialInstantiations( conj, q, bvl, vars, terms, types, &it->second, pindex, paindex+1, iindex+1 ); + for (std::pair& t : curr->d_data) + { + terms[d_pat_var_order[q][iindex]] = t.first; + getPartialInstantiations(conj, + q, + bvl, + vars, + terms, + types, + &t.second, + pindex, + paindex + 1, + iindex + 1); } } }else{ diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 63e810645..b8b0e34fa 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -17,15 +17,14 @@ #ifndef __CVC4__THEORY__LOCAL_THEORY_EXT_H #define __CVC4__THEORY__LOCAL_THEORY_EXT_H -#include "theory/quantifiers_engine.h" #include "context/cdo.h" +#include "expr/node_trie.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { namespace quantifiers { -class TermArgTrie; - class LtePartialInst : public QuantifiersModule { private: // was this module invoked @@ -46,9 +45,16 @@ private: void reset(); /** get instantiations */ void getInstantiations( std::vector< Node >& lemmas ); - void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, - std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, TermArgTrie * curr, - unsigned pindex, unsigned paindex, unsigned iindex ); + void getPartialInstantiations(std::vector& conj, + Node q, + Node bvl, + std::vector& vars, + std::vector& inst, + std::vector& types, + TNodeTrie* curr, + unsigned pindex, + unsigned paindex, + unsigned iindex); /** get eligible inst variables */ void getEligibleInstVars( Node n, std::map< Node, bool >& vars ); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 95ec24df9..5b57af14c 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1293,7 +1293,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { Assert( isHandledUfTerm( d_n ) ); TNode f = getMatchOperator( p, d_n ); Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl; - TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f ); + TNodeTrie* qni = p->getTermDatabase()->getTermArgTrie(Node::null(), f); if (qni == nullptr || qni->empty()) { //inform irrelevant quantifiers @@ -1672,7 +1672,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { }else{ //binding a variable d_qni_bound[index] = repVar; - std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.begin(); + std::map::iterator it = + d_qn[index]->d_data.begin(); if( it != d_qn[index]->d_data.end() ) { d_qni.push_back( it ); //set the match @@ -1699,7 +1700,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { } if( !val.isNull() ){ //constrained by val - std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.find( val ); + std::map::iterator it = + d_qn[index]->d_data.find(val); if( it!=d_qn[index]->d_data.end() ){ Debug("qcf-match-debug") << " Match" << std::endl; d_qni.push_back( it ); diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 0469e958b..9fa37a96c 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -22,7 +22,7 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" -#include "theory/quantifiers/term_database.h" +#include "expr/node_trie.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -45,8 +45,8 @@ private: MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; } //MatchGen * getChild( int i ) { return &d_children[i]; } //current matching information - std::vector< TermArgTrie * > d_qn; - std::vector< std::map< TNode, TermArgTrie >::iterator > d_qni; + std::vector d_qn; + std::vector::iterator> d_qni; bool doMatching( QuantConflictFind * p, QuantInfo * qi ); //for matching : each index is either a variable or a ground term unsigned d_qni_size; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 482acacc2..44c5586c3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -32,49 +32,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) { - if( argIndex==(int)reps.size() ){ - if( d_data.empty() ){ - return Node::null(); - }else{ - return d_data.begin()->first; - } - }else{ - std::map< TNode, TermArgTrie >::iterator it = d_data.find( reps[argIndex] ); - if( it==d_data.end() ){ - return Node::null(); - }else{ - return it->second.existsTerm( reps, argIndex+1 ); - } - } -} - -bool TermArgTrie::addTerm( TNode n, std::vector< TNode >& reps, int argIndex ){ - return addOrGetTerm( n, reps, argIndex )==n; -} - -TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex ) { - if( argIndex==(int)reps.size() ){ - if( d_data.empty() ){ - //store n in d_data (this should be interpretted as the "data" and not as a reference to a child) - d_data[n].clear(); - return n; - }else{ - return d_data.begin()->first; - } - }else{ - return d_data[reps[argIndex]].addOrGetTerm( n, reps, argIndex+1 ); - } -} - -void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { - for( std::map< TNode, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - for( unsigned i=0; ifirst << std::endl; - it->second.debugPrint( c, n, depth+1 ); - } -} - TermDb::TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe) : d_quantEngine(qe), @@ -1056,12 +1013,13 @@ bool TermDb::reset( Theory::Effort effort ){ return true; } -TermArgTrie * TermDb::getTermArgTrie( Node f ) { +TNodeTrie* TermDb::getTermArgTrie(Node f) +{ if( options::ufHo() ){ f = getOperatorRepresentative( f ); } computeUfTerms( f ); - std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f ); + std::map::iterator itut = d_func_map_trie.find(f); if( itut!=d_func_map_trie.end() ){ return &itut->second; }else{ @@ -1069,19 +1027,21 @@ TermArgTrie * TermDb::getTermArgTrie( Node f ) { } } -TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) { +TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f) +{ if( options::ufHo() ){ f = getOperatorRepresentative( f ); } computeUfEqcTerms( f ); - std::map< Node, TermArgTrie >::iterator itut = d_func_map_eqc_trie.find( f ); + std::map::iterator itut = d_func_map_eqc_trie.find(f); if( itut==d_func_map_eqc_trie.end() ){ return NULL; }else{ if( eqc.isNull() ){ return &itut->second; }else{ - std::map< TNode, TermArgTrie >::iterator itute = itut->second.d_data.find( eqc ); + std::map::iterator itute = + itut->second.d_data.find(eqc); if( itute!=itut->second.d_data.end() ){ return &itute->second; }else{ @@ -1096,7 +1056,7 @@ TNode TermDb::getCongruentTerm( Node f, Node n ) { f = getOperatorRepresentative( f ); } computeUfTerms( f ); - std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f ); + std::map::iterator itut = d_func_map_trie.find(f); if( itut!=d_func_map_trie.end() ){ computeArgReps( n ); return itut->second.existsTerm( d_arg_reps[n] ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 7e3806e8c..cc9a24d08 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -21,9 +21,10 @@ #include #include "expr/attribute.h" +#include "expr/node_trie.h" +#include "theory/quantifiers/quant_util.h" #include "theory/theory.h" #include "theory/type_enumerator.h" -#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { @@ -37,69 +38,6 @@ namespace inst{ namespace quantifiers { -/** Term arg trie class -* -* This also referred to as a "term index" or a "signature table". -* -* This data structure stores a set expressions, indexed by representatives of -* their arguments. -* -* For example, consider the equivalence classes : -* -* { a, d, f( d, c ), f( a, c ) } -* { b, f( b, d ) } -* { c, f( b, b ) } -* -* where the first elements ( a, b, c ) are the representatives of these classes. -* The TermArgTrie t we may build for f is : -* -* t : -* t.d_data[a] : -* t.d_data[a].d_data[c] : -* t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf) -* t.d_data[b] : -* t.d_data[b].d_data[b] : -* t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf) -* t.d_data[b].d_data[d] : -* t.d_data[b].d_data[d].d_data[f(b,d)] : (leaf) -* -* Leaf nodes store the terms that are indexed by the arguments, for example -* term f(d,c) is indexed by the representative arguments (a,c), and is stored -* as a the (single) key in the data of t.d_data[a].d_data[c]. -*/ -class TermArgTrie { -public: - /** the data */ - std::map< TNode, TermArgTrie > d_data; -public: - /** for leaf nodes : does this trie have data? */ - bool hasNodeData() { return !d_data.empty(); } - /** for leaf nodes : get term corresponding to this leaf */ - TNode getNodeData() { return d_data.begin()->first; } - /** exists term - * Returns the term that is indexed by reps, if one exists, or - * or returns null otherwise. - */ - TNode existsTerm(std::vector& reps, int argIndex = 0); - /** add or get term - * Returns the term that is previously indexed by reps, if one exists, or - * Adds n to the trie, indexed by reps, and returns n. - */ - TNode addOrGetTerm(TNode n, std::vector& reps, int argIndex = 0); - /** add term - * Returns false if a term is previously indexed by reps. - * Returns true if no term is previously indexed by reps, - * and adds n to the trie, indexed by reps, and returns n. - */ - bool addTerm(TNode n, std::vector& reps, int argIndex = 0); - /** debug print this trie */ - void debugPrint(const char* c, Node n, unsigned depth = 0); - /** clear all data from this trie */ - void clear() { d_data.clear(); } - /** is empty */ - bool empty() { return d_data.empty(); } -};/* class TermArgTrie */ - namespace fmcheck { class FullModelChecker; } @@ -121,12 +59,12 @@ class TermGenEnv; * The primary responsibilities for this class are to : * (1) Maintain a list of all ground terms that exist in the quantifier-free * solvers, as notified through the master equality engine. - * (2) Build TermArgTrie objects that index all ground terms, per operator. + * (2) Build TNodeTrie objects that index all ground terms, per operator. * * Like other utilities, its reset(...) function is called * at the beginning of full or last call effort checks. * This initializes the database for the round. However, - * notice that TermArgTrie objects are computed + * notice that TNodeTrie objects are computed * lazily for performance reasons. */ class TermDb : public QuantifiersUtil { @@ -213,10 +151,10 @@ class TermDb : public QuantifiersUtil { */ Node getMatchOperator(Node n); /** get term arg index for all f-applications in the current context */ - TermArgTrie* getTermArgTrie(Node f); + TNodeTrie* getTermArgTrie(Node f); /** get the term arg trie for f-applications in the equivalence class of eqc. */ - TermArgTrie* getTermArgTrie(Node eqc, Node f); + TNodeTrie* getTermArgTrie(Node eqc, Node f); /** get congruent term * If possible, returns a term t such that: * (1) t is a term that is currently indexed by this database, @@ -358,8 +296,8 @@ class TermDb : public QuantifiersUtil { /** mapping from terms to representatives of their arguments */ std::map< TNode, std::vector< TNode > > d_arg_reps; /** map from operators to trie */ - std::map< Node, TermArgTrie > d_func_map_trie; - std::map< Node, TermArgTrie > d_func_map_eqc_trie; + std::map d_func_map_trie; + std::map d_func_map_eqc_trie; /** mapping from operators to their representative relevant domains */ std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom; /** has map */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index ec6406a6a..83c66c2d3 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -21,7 +21,6 @@ #include "expr/node_algorithm.h" #include "options/sets_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/term_database.h" #include "theory/sets/normal_form.h" #include "theory/sets/theory_sets.h" #include "theory/theory_model.h" @@ -1774,11 +1773,16 @@ void TheorySetsPrivate::addSharedTerm(TNode n) { d_equalityEngine.addTriggerTerm(n, THEORY_SETS); } -void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ){ +void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, + TNodeTrie* t2, + unsigned arity, + unsigned depth, + unsigned& n_pairs) +{ if( depth==arity ){ if( t2!=NULL ){ - Node f1 = t1->getNodeData(); - Node f2 = t2->getNodeData(); + Node f1 = t1->getData(); + Node f2 = t2->getData(); if( !ee_areEqual( f1, f2 ) ){ Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl; vector< pair > currentPairs; @@ -1818,13 +1822,17 @@ void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers if( t2==NULL ){ if( depth<(arity-1) ){ //add care pairs internal to each child - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - addCarePairs( &it->second, NULL, arity, depth+1, n_pairs ); + for (std::pair& t : t1->d_data) + { + addCarePairs(&t.second, NULL, arity, depth + 1, n_pairs); } } //add care pairs based on each pair of non-disequal arguments - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it; + for (std::map::iterator it = t1->d_data.begin(); + it != t1->d_data.end(); + ++it) + { + std::map::iterator it2 = it; ++it2; for( ; it2 != t1->d_data.end(); ++it2 ){ if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ @@ -1836,11 +1844,15 @@ void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers } }else{ //add care pairs based on product of indices, non-disequal arguments - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){ - if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ - if( !ee_areCareDisequal(it->first, it2->first) ){ - addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs ); + for (std::pair& tt1 : t1->d_data) + { + for (std::pair& tt2 : t2->d_data) + { + if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false)) + { + if (!ee_areCareDisequal(tt1.first, tt2.first)) + { + addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs); } } } @@ -1855,7 +1867,7 @@ void TheorySetsPrivate::computeCareGraph() { unsigned n_pairs = 0; Trace("sets-cg-summary") << "Compute graph for sets, op=" << it->first << "..." << it->second.size() << std::endl; Trace("sets-cg") << "Build index for " << it->first << "..." << std::endl; - std::map< TypeNode, quantifiers::TermArgTrie > index; + std::map index; unsigned arity = 0; //populate indices for( unsigned i=0; isecond.size(); i++ ){ @@ -1882,9 +1894,11 @@ void TheorySetsPrivate::computeCareGraph() { } if( arity>0 ){ //for each index - for( std::map< TypeNode, quantifiers::TermArgTrie >::iterator iti = index.begin(); iti != index.end(); ++iti ){ - Trace("sets-cg") << "Process index " << iti->first << "..." << std::endl; - addCarePairs( &iti->second, NULL, arity, 0, n_pairs ); + for (std::pair& tt : index) + { + Trace("sets-cg") << "Process index " << tt.first << "..." + << std::endl; + addCarePairs(&tt.second, nullptr, arity, 0, n_pairs); } } Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs << std::endl; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index d36e0ddb1..447ac33a1 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -21,18 +21,13 @@ #include "context/cdhashset.h" #include "context/cdqueue.h" - +#include "expr/node_trie.h" +#include "theory/sets/theory_sets_rels.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" -#include "theory/sets/theory_sets_rels.h" namespace CVC4 { namespace theory { - -namespace quantifiers{ - class TermArgTrie; -} - namespace sets { /** Internal classes, forward declared here */ @@ -83,9 +78,13 @@ private: Node getUnivSet( TypeNode tn ); bool hasLemmaCached( Node lem ); bool hasProcessed(); - - void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ); - + + void addCarePairs(TNodeTrie* t1, + TNodeTrie* t2, + unsigned arity, + unsigned depth, + unsigned& n_pairs); + Node d_true; Node d_false; Node d_zero; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e8b753768..9da6fd277 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -24,7 +24,6 @@ #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/ext_theory.h" -#include "theory/quantifiers/term_database.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/type_enumerator.h" @@ -1118,11 +1117,15 @@ void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } } -void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ) { +void TheoryStrings::addCarePairs(TNodeTrie* t1, + TNodeTrie* t2, + unsigned arity, + unsigned depth) +{ if( depth==arity ){ if( t2!=NULL ){ - Node f1 = t1->getNodeData(); - Node f2 = t2->getNodeData(); + Node f1 = t1->getData(); + Node f2 = t2->getData(); if( !d_equalityEngine.areEqual( f1, f2 ) ){ Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; vector< pair > currentPairs; @@ -1151,13 +1154,17 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te if( t2==NULL ){ if( depth<(arity-1) ){ //add care pairs internal to each child - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - addCarePairs( &it->second, NULL, arity, depth+1 ); + for (std::pair& tt : t1->d_data) + { + addCarePairs(&tt.second, nullptr, arity, depth + 1); } } //add care pairs based on each pair of non-disequal arguments - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it; + for (std::map::iterator it = t1->d_data.begin(); + it != t1->d_data.end(); + ++it) + { + std::map::iterator it2 = it; ++it2; for( ; it2 != t1->d_data.end(); ++it2 ){ if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ @@ -1169,11 +1176,15 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te } }else{ //add care pairs based on product of indices, non-disequal arguments - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){ - if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ - if( !areCareDisequal(it->first, it2->first) ){ - addCarePairs( &it->second, &it2->second, arity, depth+1 ); + for (std::pair& tt1 : t1->d_data) + { + for (std::pair& tt2 : t2->d_data) + { + if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false)) + { + if (!areCareDisequal(tt1.first, tt2.first)) + { + addCarePairs(&tt1.second, &tt2.second, arity, depth + 1); } } } @@ -1185,7 +1196,7 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te void TheoryStrings::computeCareGraph(){ //computing the care graph here is probably still necessary, due to operators that take non-string arguments TODO: verify Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl; - std::map< Node, quantifiers::TermArgTrie > index; + std::map index; std::map< Node, unsigned > arity; unsigned functionTerms = d_functionsTerms.size(); for (unsigned i = 0; i < functionTerms; ++ i) { @@ -1206,9 +1217,11 @@ void TheoryStrings::computeCareGraph(){ } } //for each index - for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){ - Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " << itii->first << "..." << std::endl; - addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 ); + for (std::pair& tt : index) + { + Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " + << tt.first << "..." << std::endl; + addCarePairs(&tt.second, nullptr, arity[tt.first], 0); } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index ec250288b..aa86f1bc1 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -22,6 +22,7 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "expr/attribute.h" +#include "expr/node_trie.h" #include "theory/decision_manager.h" #include "theory/strings/regexp_elim.h" #include "theory/strings/regexp_operation.h" @@ -35,11 +36,6 @@ namespace CVC4 { namespace theory { - -namespace quantifiers{ - class TermArgTrie; -} - namespace strings { /** @@ -557,7 +553,10 @@ private: //--------------------------------end for checkMemberships private: - void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ); + void addCarePairs(TNodeTrie* t1, + TNodeTrie* t2, + unsigned arity, + unsigned depth); public: /** preregister term */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 3e9e2354d..645e1f656 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -28,7 +28,6 @@ #include "theory/theory_model.h" #include "theory/type_enumerator.h" #include "theory/uf/theory_uf_strong_solver.h" -#include "theory/quantifiers/term_database.h" #include "options/theory_options.h" #include "theory/uf/theory_uf_rewriter.h" @@ -557,12 +556,15 @@ bool TheoryUF::areCareDisequal(TNode x, TNode y){ return false; } -//TODO: move quantifiers::TermArgTrie to src/theory/ -void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ){ +void TheoryUF::addCarePairs(TNodeTrie* t1, + TNodeTrie* t2, + unsigned arity, + unsigned depth) +{ if( depth==arity ){ if( t2!=NULL ){ - Node f1 = t1->getNodeData(); - Node f2 = t2->getNodeData(); + Node f1 = t1->getData(); + Node f2 = t2->getData(); if( !d_equalityEngine.areEqual( f1, f2 ) ){ Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; vector< pair > currentPairs; @@ -592,13 +594,17 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg if( t2==NULL ){ if( depth<(arity-1) ){ //add care pairs internal to each child - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - addCarePairs( &it->second, NULL, arity, depth+1 ); + for (std::pair& tt : t1->d_data) + { + addCarePairs(&tt.second, NULL, arity, depth + 1); } } //add care pairs based on each pair of non-disequal arguments - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it; + for (std::map::iterator it = t1->d_data.begin(); + it != t1->d_data.end(); + ++it) + { + std::map::iterator it2 = it; ++it2; for( ; it2 != t1->d_data.end(); ++it2 ){ if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ @@ -610,11 +616,15 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg } }else{ //add care pairs based on product of indices, non-disequal arguments - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){ - if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ - if( !areCareDisequal(it->first, it2->first) ){ - addCarePairs( &it->second, &it2->second, arity, depth+1 ); + for (std::pair& tt1 : t1->d_data) + { + for (std::pair& tt2 : t2->d_data) + { + if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false)) + { + if (!areCareDisequal(tt1.first, tt2.first)) + { + addCarePairs(&tt1.second, &tt2.second, arity, depth + 1); } } } @@ -628,7 +638,7 @@ void TheoryUF::computeCareGraph() { if (d_sharedTerms.size() > 0) { //use term indexing Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl; - std::map< Node, quantifiers::TermArgTrie > index; + std::map index; std::map< Node, unsigned > arity; unsigned functionTerms = d_functionsTerms.size(); for (unsigned i = 0; i < functionTerms; ++ i) { @@ -644,14 +654,16 @@ void TheoryUF::computeCareGraph() { } } if( has_trigger_arg ){ - index[op].addTerm( f1, reps, arg_start_index ); + index[op].addTerm(f1, reps); arity[op] = reps.size(); } } //for each index - for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){ - Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << itii->first << "..." << std::endl; - addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 ); + for (std::pair& tt : index) + { + Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " + << tt.first << "..." << std::endl; + addCarePairs(&tt.second, nullptr, arity[tt.first], 0); } Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." << std::endl; } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 2fd23a657..a0380f73a 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -20,24 +20,16 @@ #ifndef __CVC4__THEORY__UF__THEORY_UF_H #define __CVC4__THEORY__UF__THEORY_UF_H +#include "context/cdhashset.h" +#include "context/cdo.h" #include "expr/node.h" -//#include "expr/attribute.h" - +#include "expr/node_trie.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "theory/uf/symmetry_breaker.h" -#include "context/cdo.h" -#include "context/cdhashset.h" - - namespace CVC4 { namespace theory { - -namespace quantifiers{ - class TermArgTrie; -} - namespace uf { class UfTermDb; @@ -313,7 +305,10 @@ private: } private: bool areCareDisequal(TNode x, TNode y); - void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ); + void addCarePairs(TNodeTrie* t1, + TNodeTrie* t2, + unsigned arity, + unsigned depth); };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ -- 2.30.2