From ec2a8ad5e5be550f4f0c5c3be92ee20bf2977efa Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 3 Sep 2014 17:23:04 +0200 Subject: [PATCH] Implement and enable --dt-var-exp-quant, cleanup trace messages, minor changes for relevant term filtering. --- src/smt/smt_engine.cpp | 1 + src/theory/datatypes/theory_datatypes.cpp | 5 ++- src/theory/datatypes/theory_datatypes.h | 2 + .../quantifiers/conjecture_generator.cpp | 39 +++++++++++-------- src/theory/quantifiers/conjecture_generator.h | 9 ++--- src/theory/quantifiers/options | 2 +- .../quantifiers/quant_conflict_find.cpp | 12 +++--- .../quantifiers/quantifiers_rewriter.cpp | 31 ++++++++++++--- test/regress/regress0/bug567.smt2 | 2 +- 9 files changed, 66 insertions(+), 37 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 d_consTerms; /** All the selector terms that the theory has seen */ context::CDList 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 > 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->firstfirst] = 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; jmkBoundVar( 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 ){ diff --git a/test/regress/regress0/bug567.smt2 b/test/regress/regress0/bug567.smt2 index 109940090..37403d8a3 100644 --- a/test/regress/regress0/bug567.smt2 +++ b/test/regress/regress0/bug567.smt2 @@ -1,7 +1,7 @@ (set-logic ALL_SUPPORTED) ; COMMAND-LINE: --incremental ; EXPECT: unknown -; EXPECT: unknown +; EXPECT: unsat ; EXPECT: unknown (declare-datatypes () ((OptInt0 (Some (value0 Int)) (None)))) (declare-datatypes () ((List0 (Cons (head0 Int) (tail0 List0)) (Nil)))) -- 2.30.2