summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-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
-rw-r--r--src/theory/theory_engine.cpp11
-rw-r--r--src/util/sort_inference.cpp19
8 files changed, 34 insertions, 79 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:
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7fb989a5a..12a169e09 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -92,19 +92,10 @@ void TheoryEngine::finishInit() {
void TheoryEngine::eqNotifyNewClass(TNode t){
d_quantEngine->addTermToDatabase( t );
- if( d_logicInfo.isQuantified() && options::quantConflictFind() ){
- d_quantEngine->getConflictFind()->newEqClass( t );
- }
}
void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
- //TODO: add notification to efficient E-matching
- if( d_logicInfo.isQuantified() ){
- //d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
- if( options::quantConflictFind() ){
- d_quantEngine->getConflictFind()->merge( t1, t2 );
- }
- }
+
}
void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 066ba6103..dbd1dcd16 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -171,7 +171,9 @@ bool SortInference::simplify( std::vector< Node >& assertions ){
for( unsigned i=0; i<assertions.size(); i++ ){
Node prev = assertions[i];
std::map< Node, Node > var_bound;
+ Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl;
assertions[i] = simplify( assertions[i], var_bound );
+ Trace("sort-inference-debug") << "Done." << std::endl;
if( prev!=assertions[i] ){
assertions[i] = theory::Rewriter::rewrite( assertions[i] );
rewritten = true;
@@ -512,6 +514,7 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){
}
Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
+ Trace("sort-inference-debug2") << "Simplify " << n << std::endl;
std::vector< Node > children;
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
//recreate based on types of variables
@@ -519,6 +522,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
for( size_t i=0; i<n[0].getNumChildren(); i++ ){
TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() );
Node v = getNewSymbol( n[0][i], tn );
+ Trace("sort-inference-debug2") << "Map variable " << n[0][i] << " to " << v << std::endl;
new_children.push_back( v );
var_bound[ n[0][i] ] = v;
}
@@ -529,13 +533,17 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
children.push_back( n.getOperator() );
}
+ bool childChanged = false;
for( size_t i=0; i<n.getNumChildren(); i++ ){
bool processChild = true;
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1;
}
if( processChild ){
- children.push_back( simplify( n[i], var_bound ) );
+ Node nc = simplify( n[i], var_bound );
+ Trace("sort-inference-debug2") << "Simplify " << i << " " << n[i] << " returned " << nc << std::endl;
+ children.push_back( nc );
+ childChanged = childChanged || nc!=n[i];
}
}
@@ -543,6 +551,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
//erase from variable bound
for( size_t i=0; i<n[0].getNumChildren(); i++ ){
+ Trace("sort-inference-debug2") << "Remove bound for " << n[0][i] << std::endl;
var_bound.erase( n[0][i] );
}
return NodeManager::currentNM()->mkNode( n.getKind(), children );
@@ -596,7 +605,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
if( n[i].isConst() ){
children[i+1] = getNewSymbol( n[i], tna );
}else{
- Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl;
+ Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl;
Assert( false );
}
}
@@ -616,7 +625,11 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
//just return n, we will fix at higher scope
return n;
}else{
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ if( childChanged ){
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }else{
+ return n;
+ }
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback