From: ajreynol Date: Tue, 3 Jun 2014 12:01:01 +0000 (+0200) Subject: Support E-matching/QCF for Set operators. X-Git-Tag: cvc5-1.0.0~6866 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6480823e5620b316b4c319453f45f6d7d452e2b1;p=cvc5.git Support E-matching/QCF for Set operators. --- diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 24f17d0c1..731b53dc4 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -20,6 +20,7 @@ #include "theory/theory_engine.h" #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/trigger.h" using namespace CVC4; using namespace CVC4::kind; @@ -1692,8 +1693,9 @@ bool MatchGen::isHandledBoolConnective( TNode n ) { } bool MatchGen::isHandledUfTerm( TNode n ) { - return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; + //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT || + // n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; + return inst::Trigger::isAtomicTriggerKind( n.getKind() ); } Node MatchGen::getOperator( QuantConflictFind * p, Node n ) { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5636e0c5f..9f25b0825 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -73,25 +73,21 @@ unsigned TermDb::getNumGroundTerms( Node f ) { Node TermDb::getOperator( Node n ) { //return n.getOperator(); - - if( n.getKind()==SELECT || n.getKind()==STORE ){ + Kind k = n.getKind(); + if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON ){ //since it is parametric, use a particular one as op - TypeNode tn1 = n[0].getType(); - TypeNode tn2 = n[1].getType(); + TypeNode tn = n[0].getType(); Node op = n.getOperator(); - std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > >::iterator ito = d_par_op_map.find( op ); + std::map< Node, std::map< TypeNode, Node > >::iterator ito = d_par_op_map.find( op ); if( ito!=d_par_op_map.end() ){ - std::map< TypeNode, std::map< TypeNode, Node > >::iterator it = ito->second.find( tn1 ); + std::map< TypeNode, Node >::iterator it = ito->second.find( tn ); if( it!=ito->second.end() ){ - std::map< TypeNode, Node >::iterator it2 = it->second.find( tn2 ); - if( it2!=it->second.end() ){ - return it2->second; - } + return it->second; } } - d_par_op_map[op][tn1][tn2] = n; + d_par_op_map[op][tn] = n; return n; - }else if( inst::Trigger::isAtomicTrigger( n ) ){ + }else if( inst::Trigger::isAtomicTriggerKind( k ) ){ return n.getOperator(); }else{ return Node::null(); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 2592e1fd6..e82fcd00d 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -97,7 +97,7 @@ private: std::hash_set< Node, NodeHashFunction > d_processed; private: /** select op map */ - std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > > d_par_op_map; + std::map< Node, std::map< TypeNode, Node > > d_par_op_map; /** count number of ground terms per operator (user-context dependent) */ NodeIntMap d_op_ccount; public: diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 5802632da..8335a084a 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -109,10 +109,10 @@ void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) { void TheoryQuantifiers::check(Effort e) { CodeTimer codeTimer(d_theoryTime); - Debug("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl; + Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl; while(!done()) { Node assertion = get(); - Debug("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl; + Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl; switch(assertion.getKind()) { case kind::FORALL: assertUniversal( assertion ); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 3de12b9c9..77a4efff5 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -323,9 +323,16 @@ bool Trigger::isUsableTrigger( Node n, Node f ){ } bool Trigger::isAtomicTrigger( Node n ){ - return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; + Kind k = n.getKind(); + return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || + ( k!=APPLY_UF && isAtomicTriggerKind( k ) ); } +bool Trigger::isAtomicTriggerKind( Kind k ) { + return k==APPLY_UF || k==SELECT || k==STORE || + k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || + k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON; +} + bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 74fc16764..9254105dd 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -107,6 +107,7 @@ public: static bool isUsableTrigger( std::vector< Node >& nodes, Node f ); static bool isUsableTrigger( Node n, Node f ); static bool isAtomicTrigger( Node n ); + static bool isAtomicTriggerKind( Kind k ); static bool isSimpleTrigger( Node n ); /** get pattern arithmetic */ static bool isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ); diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 3a5b61390..c230b9ac5 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -34,6 +34,10 @@ TheorySets::~TheorySets() { delete d_internal; } +void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_internal->setMasterEqualityEngine(eq); +} + void TheorySets::addSharedTerm(TNode n) { d_internal->addSharedTerm(n); } diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 9f74064cb..6ff41d5f5 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -48,6 +48,8 @@ public: ~TheorySets(); + void setMasterEqualityEngine(eq::EqualityEngine* eq); + void addSharedTerm(TNode); void check(Effort); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index af96b50d0..8c9441483 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -880,6 +880,10 @@ bool TheorySetsPrivate::propagate(TNode literal) { }/* TheorySetsPropagate::propagate(TNode) */ +void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalityEngine.setMasterEqualityEngine(eq); +} + void TheorySetsPrivate::addSharedTerm(TNode n) { Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl; d_equalityEngine.addTriggerTerm(n, THEORY_SETS); diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 73c0c419e..90dec7c0b 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -47,6 +47,8 @@ public: context::UserContext* u); ~TheorySetsPrivate(); + + void setMasterEqualityEngine(eq::EqualityEngine* eq); void addSharedTerm(TNode);