summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xsrc/theory/quantifiers/quant_conflict_find.cpp6
-rw-r--r--src/theory/quantifiers/term_database.cpp20
-rw-r--r--src/theory/quantifiers/term_database.h2
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp4
-rw-r--r--src/theory/quantifiers/trigger.cpp11
-rw-r--r--src/theory/quantifiers/trigger.h1
-rw-r--r--src/theory/sets/theory_sets.cpp4
-rw-r--r--src/theory/sets/theory_sets.h2
-rw-r--r--src/theory/sets/theory_sets_private.cpp4
-rw-r--r--src/theory/sets/theory_sets_private.h2
10 files changed, 37 insertions, 19 deletions
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback