diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 5 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 39 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.h | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 31 |
8 files changed, 65 insertions, 36 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 98cc7813d..cd3a7943e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1300,6 +1300,7 @@ void SmtEngine::setDefaults() { } } if( options::dtStcInduction() ){ + //leads to unfairness FIXME if( !options::dtForceAssignment.wasSetByUser() ){ options::dtForceAssignment.set( true ); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index f74384d59..8e90f5056 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -62,6 +62,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_equalityEngine.addFunctionKind(kind::APPLY_UF); d_true = NodeManager::currentNM()->mkConst( true ); + d_dtfCounter = 0; } TheoryDatatypes::~TheoryDatatypes() { @@ -190,8 +191,8 @@ void TheoryDatatypes::check(Effort e) { } } } - - if( !needSplit && options::dtForceAssignment() ){ + //d_dtfCounter++; + if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){ //for the sake of termination, we must choose the constructor of a ground term //NEED GUARENTEE: groundTerm should not contain any subterms of the same type // TODO: this is probably not good enough, actually need fair enumeration strategy diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 132077e29..3592dbe30 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -174,6 +174,8 @@ private: context::CDList<TNode> d_consTerms; /** All the selector terms that the theory has seen */ context::CDList<TNode> d_selTerms; + /** counter for forcing assignments (ensures fairness) */ + unsigned d_dtfCounter; private: /** assert fact */ void assertFact( Node fact, Node exp ); diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 17489b6ba..c775bb558 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -710,12 +710,12 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { Trace("sg-rel-term") << std::endl;
for( unsigned r=0; r<2; r++ ){
- Trace("sg-gen-tg-eqc") << "...from equivalence classes (" << r << ") : ";
+ Trace("sg-rel-term-debug") << "...from equivalence classes (" << r << ") : ";
int index = d_ccand_eqc[r].size()-1;
for( unsigned j=0; j<d_ccand_eqc[r][index].size(); j++ ){
- Trace("sg-gen-tg-eqc") << "e" << d_em[d_ccand_eqc[r][index][j]] << " ";
+ Trace("sg-rel-term-debug") << "e" << d_em[d_ccand_eqc[r][index][j]] << " ";
}
- Trace("sg-gen-tg-eqc") << std::endl;
+ Trace("sg-rel-term-debug") << std::endl;
}
TypeNode tnn = nn.getType();
Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl;
@@ -766,7 +766,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { int index = d_ccand_eqc[1].size()-1;
for( unsigned j=0; j<d_ccand_eqc[1][index].size(); j++ ){
TNode r = d_ccand_eqc[1][index][j];
- Trace("sg-gen-tg-eqc") << " Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;
+ Trace("sg-rel-term-debug") << " Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;
std::map< TypeNode, std::map< unsigned, TNode > > subs;
std::map< TNode, bool > rev_subs;
//only get ground terms
@@ -779,17 +779,17 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { unsigned tindex = typ_to_subs_index[it->first];
for( std::map< unsigned, TNode >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
if( !firstTime ){
- Trace("sg-gen-tg-eqc") << ", ";
+ Trace("sg-rel-term-debug") << ", ";
}else{
firstTime = false;
- Trace("sg-gen-tg-eqc") << " ";
+ Trace("sg-rel-term-debug") << " ";
}
- Trace("sg-gen-tg-eqc") << it->first << ":x" << it2->first << " -> " << it2->second;
+ Trace("sg-rel-term-debug") << it->first << ":x" << it2->first << " -> " << it2->second;
Assert( tindex+it2->first<gsubs_terms.size() );
gsubs_terms[tindex+it2->first] = it2->second;
}
}
- Trace("sg-gen-tg-eqc") << std::endl;
+ Trace("sg-rel-term-debug") << std::endl;
d_rel_pattern_subs_index[nn].addSubstitution( r, gsubs_vars, gsubs_terms );
}
}
@@ -1000,9 +1000,10 @@ bool ConjectureGenerator::considerCurrentTerm() { std::map< TNode, bool > rev_subs;
unsigned mode;
if( r==0 ){
- mode = optReqDistinctVarPatterns() ? 1 : 0;
+ mode = optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;
+ mode = mode | (1 << 2 );
}else{
- mode = (optFilterConfirmation() && optFilterConfirmationOnlyGround() ) ? 2 : 0;
+ mode = (optFilterConfirmation() && optFilterConfirmationOnlyGround() ) ? ( 1 << 1 ) : 0;
}
d_tg_alloc[0].resetMatching( this, d_ccand_eqc[r][i-1][j], mode );
if( d_tg_alloc[0].getNextMatch( this, d_ccand_eqc[r][i-1][j], subs, rev_subs ) ){
@@ -1539,9 +1540,9 @@ void TermGenerator::resetMatching( ConjectureGenerator * s, TNode eqc, unsigned d_match_children_end.clear();
d_match_mode = mode;
//if this term generalizes, it must generalize a non-ground term
- if( mode<2 && s->isGroundEqc( eqc ) && d_status==5 ){
- d_match_status = -1;
- }
+ //if( (d_match_mode & ( 1 << 2 ))!=0 && s->isGroundEqc( eqc ) && d_status==5 ){
+ // d_match_status = -1;
+ //}
}
bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {
@@ -1572,13 +1573,19 @@ bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map< //a variable
if( d_match_status==0 ){
d_match_status++;
- if( d_match_mode>=2 ){
+ if( (d_match_mode & ( 1 << 1 ))!=0 ){
//only ground terms
if( !s->isGroundEqc( eqc ) ){
return false;
}
+ }else if( (d_match_mode & ( 1 << 2 ))!=0 ){
+ //only non-ground terms
+ //if( s->isGroundEqc( eqc ) ){
+ // return false;
+ //}
}
- if( d_match_mode%2==1 ){
+ //store the match : restricted if match_mode.0 = 1
+ if( (d_match_mode & ( 1 << 0 ))!=0 ){
std::map< TNode, bool >::iterator it = rev_subs.find( eqc );
if( it==rev_subs.end() ){
rev_subs[eqc] = true;
@@ -1592,7 +1599,7 @@ bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map< }else{
//clean up
subs[d_typ].erase( d_status_num );
- if( d_match_mode%2==1 ){
+ if( (d_match_mode & ( 1 << 0 ))!=0 ){
rev_subs.erase( eqc );
}
return false;
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 94a13829c..93cda7311 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -85,10 +85,10 @@ public: //match status
int d_match_status;
int d_match_status_child_num;
- //match mode
- //1 : different variables must have different matches
- //2 : variables must map to ground terms
- //3 : both 1 and 2
+ //match mode bits
+ //0 : different variables must have different matches
+ //1 : variables must map to ground terms
+ //2 : variables must map to non-ground terms
unsigned d_match_mode;
//children
std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;
@@ -312,7 +312,6 @@ public: //for generalization return isGeneralization( patg, pat, subs );
}
bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );
-
public: //for property enumeration
//process this candidate conjecture
void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index aa68aefcc..d30e5de4a 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -26,7 +26,7 @@ option prenexQuant /--disable-prenex-quant bool :default true # forall y. P( c, y ) option varElimQuant /--disable-var-elim-quant bool :default true disable simple variable elimination for quantified formulas -option dtVarExpandQuant --dt-var-exp-quant bool :default false +option dtVarExpandQuant --dt-var-exp-quant bool :default true expand datatype variables bound to one constructor in quantifiers option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 504c3dcff..ee4464f87 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2010,9 +2010,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { //try to make a matches making the body false
Trace("qcf-check-debug") << "Get next match..." << std::endl;
while( qi->d_mg->getNextMatch( this, qi ) ){
- Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;
- qi->debugPrintMatch("qcf-check");
- Trace("qcf-check") << std::endl;
+ Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
+ qi->debugPrintMatch("qcf-inst");
+ Trace("qcf-inst") << std::endl;
std::vector< int > assigned;
if( !qi->isMatchSpurious( this ) ){
if( qi->completeMatch( this, assigned ) ){
@@ -2042,7 +2042,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { ++(d_statistics.d_prop_inst);
}
}else{
- Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;
+ Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl;
//Assert( false );
}
}
@@ -2050,10 +2050,10 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { qi->revertMatch( assigned );
d_tempCache.clear();
}else{
- Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
+ Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
}
}else{
- Trace("qcf-check") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
+ Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
}
}
if( d_conflict ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 624856671..754bfacb1 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -368,7 +368,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl; if( it->first.getKind()==EQUAL ){ - if( it->second ){ + if( it->second && options::varElimQuant() ){ for( int i=0; i<2; i++ ){ int j = i==0 ? 1 : 0; std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] ); @@ -388,14 +388,33 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& } } } - /* - else if( options::dtVarExpandQuant() && it->first.getKind()==APPLY_TESTER && it->first[0].getKind()==BOUND_VARIABLE ){ - if( it->second ){ + else if( it->first.getKind()==APPLY_TESTER ){ + if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){ Trace("dt-var-expand") << "Expand datatype variable based on : " << it->first << std::endl; std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] ); + if( ita!=args.end() ){ + vars.push_back( it->first[0] ); + Expr testerExpr = it->first.getOperator().toExpr(); + int index = Datatype::indexOf( testerExpr ); + const Datatype& dt = Datatype::datatypeOf(testerExpr); + const DatatypeConstructor& c = dt[index]; + std::vector< Node > newChildren; + newChildren.push_back( Node::fromExpr( c.getConstructor() ) ); + std::vector< Node > newVars; + for( unsigned j=0; j<c.getNumArgs(); j++ ){ + TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() ); + tn = tn[1]; + Node v = NodeManager::currentNM()->mkBoundVar( tn ); + newChildren.push_back( v ); + newVars.push_back( v ); + } + subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) ); + Trace("dt-var-expand") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl; + args.erase( ita ); + args.insert( args.end(), newVars.begin(), newVars.end() ); + } } } - */ } if( !vars.empty() ){ Trace("var-elim-quant") << "VE " << vars.size() << "/" << args.size() << std::endl; @@ -933,7 +952,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant() && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - return options::varElimQuant(); + return options::varElimQuant() || options::dtVarExpandQuant(); }else if( computeOption==COMPUTE_CNF ){ return false;//return options::cnfQuant() ; FIXME }else if( computeOption==COMPUTE_SPLIT ){ |