summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/candidate_generator.cpp36
-rwxr-xr-xsrc/theory/quantifiers/quant_conflict_find.cpp3
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp14
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.h1
-rw-r--r--src/theory/quantifiers/term_database.cpp19
-rw-r--r--src/theory/quantifiers/term_database.h10
6 files changed, 17 insertions, 66 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 0f2adf3b4..29640e18f 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -101,6 +101,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
//get next candidate term in the uf term database
while( d_term_iter<d_term_iter_limit ){
Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+ //Assert( d_qe->getEqualityQuery()->hasTerm( n ) );
d_term_iter++;
if( isLegalCandidate( n ) ){
return n;
@@ -126,41 +127,6 @@ Node CandidateGeneratorQE::getNextCandidate(){
return Node::null();
}
-//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) :
-// d_qe( qe ), d_eq_class( eqc ){
-// d_eci = NULL;
-//}
-//void CandidateGeneratorQEDisequal::resetInstantiationRound(){
-//
-//}
-////we will iterate over all terms that are disequal from eqc
-//void CandidateGeneratorQEDisequal::reset( Node eqc ){
-// //Assert( !eqc.isNull() );
-// ////begin iterating over equivalence classes that are disequal from eqc
-// //d_eci = d_ith->getEquivalenceClassInfo( eqc );
-// //if( d_eci ){
-// // d_eqci_iter = d_eci->d_disequal.begin();
-// //}
-//}
-//Node CandidateGeneratorQEDisequal::getNextCandidate(){
-// //if( d_eci ){
-// // while( d_eqci_iter != d_eci->d_disequal.end() ){
-// // if( (*d_eqci_iter).second ){
-// // //we have an equivalence class that is disequal from eqc
-// // d_cg->reset( (*d_eqci_iter).first );
-// // Node n = d_cg->getNextCandidate();
-// // //if there is a candidate in this equivalence class, return it
-// // if( !n.isNull() ){
-// // return n;
-// // }
-// // }
-// // ++d_eqci_iter;
-// // }
-// //}
-// return Node::null();
-//}
-
-
CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
d_match_pattern( mpat ), d_qe( qe ){
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index d58ce14b1..768ba63de 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1886,8 +1886,7 @@ Node QuantConflictFind::evaluateTerm( Node n ) {
/** new node */
void QuantConflictFind::newEqClass( Node n ) {
- //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;
- //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;
+
}
/** merge */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index fb7ff679b..0d338f283 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -105,6 +105,7 @@ void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node
}
void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ) {
+ Assert( activeArgs.empty() );
std::map< Node, bool > activeMap;
computeArgs( args, activeMap, n );
for( unsigned i=0; i<args.size(); i++ ){
@@ -114,6 +115,17 @@ void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector<
}
}
+void QuantifiersRewriter::computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ) {
+ Assert( activeArgs.empty() );
+ std::map< Node, bool > activeMap;
+ computeArgs( args, activeMap, n );
+ computeArgs( args, activeMap, ipl );
+ for( unsigned i=0; i<args.size(); i++ ){
+ if( activeMap[args[i]] ){
+ activeArgs.push_back( args[i] );
+ }
+ }
+}
bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){
if( std::find( args.begin(), args.end(), n )!=args.end() ){
@@ -728,7 +740,7 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >&
Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
std::vector< Node > activeArgs;
- computeArgVec( args, activeArgs, body );
+ computeArgVec2( args, activeArgs, body, ipl );
if( activeArgs.empty() ){
return body;
}else{
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index e2137b9f4..901a47f79 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -40,6 +40,7 @@ private:
static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n );
static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
+ static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
static bool hasArg( std::vector< Node >& args, Node n );
static void setNestedQuantifiers( Node n, Node q );
static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 392fc269a..c35adef6a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -329,6 +329,7 @@ void TermDb::reset( Theory::Effort effort ){
if( !it->second.empty() ){
for( unsigned i=0; i<it->second.size(); i++ ){
Node n = it->second[i];
+ //Assert( d_quantEngine->getEqualityQuery()->hasTerm( n ) );
computeModelBasisArgAttribute( n );
if( !n.getAttribute(NoMatchAttribute()) ){
computeArgReps( n );
@@ -794,24 +795,6 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){
return d_free_vars[tn];
}
-const std::vector<Node> & TermDb::getParents(TNode n, TNode f, int arg){
- std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >,NodeHashFunction >,NodeHashFunction >::const_iterator
- rn = d_parents.find( n );
- if( rn !=d_parents.end() ){
- std::hash_map< Node, std::hash_map< int, std::vector< Node > > , NodeHashFunction > ::const_iterator
- rf = rn->second.find(f);
- if( rf != rn->second.end() ){
- std::hash_map< int, std::vector< Node > > ::const_iterator
- ra = rf->second.find(arg);
- if( ra != rf->second.end() ){
- return ra->second;
- }
- }
- }
- static std::vector<Node> empty;
- return empty;
-}
-
void TermDb::computeVarContains( Node n ) {
if( d_var_contains.find( n )==d_var_contains.end() ){
d_var_contains[n].clear();
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e40635d4e..1d3757d65 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -170,16 +170,6 @@ public:
TNode evaluateTerm( TNode n );
/** is entailed (incomplete check) */
bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
-public:
- /** parent structure (for efficient E-matching):
- n -> op -> index -> L
- map from node "n" to a list of nodes "L", where each node n' in L
- has operator "op", and n'["index"] = n.
- for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... }
- */
- /* Todo replace int by size_t */
- std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction > , NodeHashFunction > d_parents;
- const std::vector<Node> & getParents(TNode n, TNode f, int arg);
//for model basis
private:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback