From 19697d530ae6eaf0165270bc3628f76124a45953 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 9 Feb 2014 16:14:31 -0600 Subject: [PATCH] More complete guess instantiation strategy, cvc4 now typically times out instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc --- src/theory/quantifiers/first_order_model.cpp | 10 +- src/theory/quantifiers/first_order_model.h | 4 + .../quantifiers/inst_strategy_e_matching.cpp | 124 +++++++++++------- .../quantifiers/quant_conflict_find.cpp | 3 +- src/theory/quantifiers/relevant_domain.cpp | 94 ++++++++++--- src/theory/quantifiers/relevant_domain.h | 4 +- test/regress/regress0/bug512.minimized.smt2 | 1 + test/regress/regress0/bug519.smt2 | 2 +- test/regress/regress0/decision/Makefile.am | 1 - test/regress/regress0/quantifiers/Makefile.am | 2 - test/regress/regress0/quantifiers/ex1.smt2 | 13 -- .../regress0/quantifiers/ex1.smt2.expect | 2 - test/regress/regress0/quantifiers/ex7.smt2 | 13 -- .../regress0/quantifiers/ex7.smt2.expect | 2 - 14 files changed, 166 insertions(+), 109 deletions(-) delete mode 100644 test/regress/regress0/quantifiers/ex1.smt2 delete mode 100644 test/regress/regress0/quantifiers/ex1.smt2.expect delete mode 100644 test/regress/regress0/quantifiers/ex7.smt2 delete mode 100644 test/regress/regress0/quantifiers/ex7.smt2.expect diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index a05abfa29..8c00c5af4 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -603,15 +603,19 @@ void FirstOrderModelFmc::processInitializeModelForTerm(Node n) { bool FirstOrderModelFmc::isStar(Node n) { - return n==getStar(n.getType()); + //return n==getStar(n.getType()); + return n.getAttribute(IsStarAttribute()); } Node FirstOrderModelFmc::getStar(TypeNode tn) { - if( d_type_star.find(tn)==d_type_star.end() ){ + std::map::iterator it = d_type_star.find( tn ); + if( it==d_type_star.end() ){ Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" ); d_type_star[tn] = st; + st.setAttribute(IsStarAttribute(), true ); + return st; } - return d_type_star[tn]; + return it->second; } Node FirstOrderModelFmc::getStarElement(TypeNode tn) { diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index ab3a1aa52..2ac9dadcf 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -19,6 +19,7 @@ #include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" +#include "expr/attribute.h" namespace CVC4 { namespace theory { @@ -35,6 +36,9 @@ namespace fmcheck { } class FirstOrderModelQInt; +struct IsStarAttributeId {}; +typedef expr::Attribute IsStarAttribute; + class FirstOrderModel : public TheoryModel { protected: diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 25a62a4e8..5e2353e8a 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -359,65 +359,87 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ return STATUS_UNFINISHED; }else{ //first, try from relevant domain - Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; - bool success; - ///* TODO: add back RelevantDomain * rd = d_quantEngine->getRelevantDomain(); - if( rd ){ - rd->compute(); - unsigned final_max_i = 0; - for(unsigned i=0; igetRDomain( f, i )->d_terms.size(); - if( ts>final_max_i ){ - final_max_i = ts; + for( unsigned r=0; r<2; r++ ){ + if( rd || r==1 ){ + if( r==0 ){ + Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; + }else{ + Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; } - } + rd->compute(); + unsigned final_max_i = 0; + std::vector< unsigned > maxs; + for(unsigned i=0; igetRDomain( f, i )->d_terms.size(); + }else{ + ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size(); + } + maxs.push_back( ts ); + Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl; + if( ts>final_max_i ){ + final_max_i = ts; + } + } + Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl; - unsigned max_i = 0; - while( max_i<=final_max_i ){ - std::vector< unsigned > childIndex; - int index = 0; - do { - while( index>=0 && index<(int)f[0].getNumChildren() ){ - if( index==(int)childIndex.size() ){ - childIndex.push_back( -1 ); - }else{ - Assert( index==(int)(childIndex.size())-1 ); - unsigned nv = childIndex[index]+1; - if( nvgetRDomain( f, index )->d_terms.size() && nv childIndex; + int index = 0; + do { + while( index>=0 && index<(int)f[0].getNumChildren() ){ + if( index==(int)childIndex.size() ){ + childIndex.push_back( -1 ); }else{ - childIndex.pop_back(); - index--; + Assert( index==(int)(childIndex.size())-1 ); + unsigned nv = childIndex[index]+1; + if( nv=0; - if( success ){ - index--; - //try instantiation - std::vector< Node > terms; - for( unsigned i=0; igetRDomain( f, i )->d_terms[childIndex[i]] ); - } - if( d_quantEngine->addInstantiation( f, terms, false ) ){ - ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); - return STATUS_UNKNOWN; + success = index>=0; + if( success ){ + Trace("inst-alg-rd") << "Try instantiation..." << std::endl; + index--; + //try instantiation + std::vector< Node > terms; + for( unsigned i=0; igetRDomain( f, i )->d_terms[childIndex[i]] ); + }else{ + terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] ); + } + } + if( d_quantEngine->addInstantiation( f, terms, false ) ){ + Trace("inst-alg-rd") << "Success!" << std::endl; + ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); + return STATUS_UNKNOWN; + } } - } - }while( success ); - max_i++; + }while( success ); + max_i++; + } } - } - //*/ - - if( d_guessed.find( f )==d_guessed.end() ){ - Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; - d_guessed[f] = true; - InstMatch m( f ); - if( d_quantEngine->addInstantiation( f, m ) ){ - ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); + if( r==0 ){ + if( d_guessed.find( f )==d_guessed.end() ){ + Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; + d_guessed[f] = true; + InstMatch m( f ); + if( d_quantEngine->addInstantiation( f, m ) ){ + ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); + return STATUS_UNKNOWN; + } + } } } return STATUS_UNKNOWN; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 4a5c92c7e..08bd0f179 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -116,6 +116,7 @@ void QuantInfo::initialize( Node q, Node qn ) { } */ } + Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl; } void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) { @@ -700,7 +701,7 @@ void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbva void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) { Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl; - bool isCom = d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF; + bool isCom = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ); std::map< int, std::vector< int > > c_to_vars; std::map< int, std::vector< int > > vars_to_c; std::map< int, int > vb_count; diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 9166b81e8..0452278f2 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -34,9 +34,15 @@ void RelevantDomain::RDomain::merge( RDomain * r ) { d_terms.clear(); } -void RelevantDomain::RDomain::addTerm( Node t ) { - if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){ - d_terms.push_back( t ); +void RelevantDomain::RDomain::addTerm( Node t, bool nonGround ) { + if( !nonGround ){ + if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){ + d_terms.push_back( t ); + } + }else{ + if( std::find( d_ng_terms.begin(), d_ng_terms.end(), t )==d_ng_terms.end() ){ + d_ng_terms.push_back( t ); + } } } @@ -138,33 +144,83 @@ void RelevantDomain::compute(){ } void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { - + Node op = d_qe->getTermDatabase()->getOperator( n ); for( unsigned i=0; igetTermDatabase()->getOperator( n ); if( !op.isNull() ){ RDomain * rf = getRDomain( op, i ); + if( n[i].getKind()==ITE ){ + for( unsigned j=1; j<=2; j++ ){ + computeRelevantDomainOpCh( rf, n[i][j] ); + } + }else{ + computeRelevantDomainOpCh( rf, n[i] ); + } + } + //TODO + if( n[i].getKind()!=FORALL ){ + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); + computeRelevantDomain( n[i], newHasPol, newPol ); + } + } + + if( n.getKind()==EQUAL || n.getKind()==GEQ ){ + int varCount = 0; + std::vector< RDomain * > rds; + int varCh = -1; + for( unsigned i=0; igetTermDatabase()->getInstConstAttr( n[i] ); - //merge the RDomains unsigned id = n[i].getAttribute(InstVarNumAttribute()); - Trace("rel-dom-debug") << n[i] << " is variable # " << id << " for " << q; - Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl; - RDomain * rq = getRDomain( q, id ); - if( rf!=rq ){ - rq->merge( rf ); + rds.push_back( getRDomain( q, id ) ); + varCount++; + varCh = i; + }else{ + rds.push_back( NULL ); + } + } + if( varCount==2 ){ + //merge the two relevant domains + if( ( !hasPol || pol ) && rds[0]!=rds[1] ){ + rds[0]->merge( rds[1] ); + } + }else if( varCount==1 ){ + int oCh = varCh==0 ? 1 : 0; + bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] ); + //the negative occurrence adds the term to the domain + if( !hasPol || !pol ){ + rds[varCh]->addTerm( n[oCh] ); + } + //the positive occurence adds other terms + if( ( !hasPol || pol ) && n[0].getType().isInteger() ){ + if( n.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + rds[varCh]->addTerm( QuantArith::offset( n[oCh], i==0 ? 1 : -1 ), ng ); + } + }else if( n.getKind()==GEQ ){ + Node nt = QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ); + rds[varCh]->addTerm( QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ), ng ); } - }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n[i] ) ){ - //term to add - rf->addTerm( n[i] ); } } + } +} - //TODO - if( n[i].getKind()!=FORALL ){ - bool newHasPol = hasPol; - bool newPol = pol; - computeRelevantDomain( n[i], newHasPol, newPol ); +void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { + if( n.getKind()==INST_CONSTANT ){ + Node q = d_qe->getTermDatabase()->getInstConstAttr( n ); + //merge the RDomains + unsigned id = n.getAttribute(InstVarNumAttribute()); + Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q; + Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl; + RDomain * rq = getRDomain( q, id ); + if( rf!=rq ){ + rq->merge( rf ); } + }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n ) ){ + //term to add + rf->addTerm( n ); } } diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 0f5afcadd..200e49a72 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -33,8 +33,9 @@ private: void reset() { d_parent = NULL; d_terms.clear(); } RDomain * d_parent; std::vector< Node > d_terms; + std::vector< Node > d_ng_terms; void merge( RDomain * r ); - void addTerm( Node t ); + void addTerm( Node t, bool nonGround = false ); RDomain * getParent(); void removeRedundantTerms( FirstOrderModel * fm ); bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); } @@ -45,6 +46,7 @@ private: QuantifiersEngine* d_qe; FirstOrderModel* d_model; void computeRelevantDomain( Node n, bool hasPol, bool pol ); + void computeRelevantDomainOpCh( RDomain * rf, Node n ); bool d_is_computed; public: RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ); diff --git a/test/regress/regress0/bug512.minimized.smt2 b/test/regress/regress0/bug512.minimized.smt2 index 0b19f26df..1a2aaf56f 100644 --- a/test/regress/regress0/bug512.minimized.smt2 +++ b/test/regress/regress0/bug512.minimized.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --tlimit-per 1000 ; EXPECT: unknown (set-logic UF) (declare-sort T 0) diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress0/bug519.smt2 index 22fdff674..406cb0c1b 100644 --- a/test/regress/regress0/bug519.smt2 +++ b/test/regress/regress0/bug519.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -mi +; COMMAND-LINE: -mi --tlimit-per 1000 ; EXPECT: unknown ; EXPECT: unsat diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index 366204191..90a18f0e2 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -25,7 +25,6 @@ TESTS = \ bitvec5.smt \ quant-Arrays_Q1-noinfer.smt2 \ quant-ex1.smt2 \ - quant-ex1.disable_miniscope.smt2 \ uflia-xs-09-16-3-4-1-5.delta03.smt \ aufbv-fuzz01.smt \ bug347.smt \ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 93d513d9f..c478248da 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -28,10 +28,8 @@ TESTS = \ bug269.smt2 \ burns13.smt2 \ burns4.smt2 \ - ex1.smt2 \ ex3.smt2 \ ex6.smt2 \ - ex7.smt2 \ opisavailable-12.smt2 \ ricart-agrawala6.smt2 \ set8.smt2 \ diff --git a/test/regress/regress0/quantifiers/ex1.smt2 b/test/regress/regress0/quantifiers/ex1.smt2 deleted file mode 100644 index 20230a6fa..000000000 --- a/test/regress/regress0/quantifiers/ex1.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-logic AUFLIRA) -(set-info :smt-lib-version 2.0) -(set-info :category "industrial") -(set-info :status sat) -(declare-sort U 0) -(declare-fun a () U) -(declare-fun b () U) -(declare-fun f (U) U) -(declare-fun p () Bool) -(assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p)))) -(check-sat) -(get-info :reason-unknown) -(exit) diff --git a/test/regress/regress0/quantifiers/ex1.smt2.expect b/test/regress/regress0/quantifiers/ex1.smt2.expect deleted file mode 100644 index 2bd8349de..000000000 --- a/test/regress/regress0/quantifiers/ex1.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% EXPECT: unknown -% EXPECT: (:reason-unknown incomplete) diff --git a/test/regress/regress0/quantifiers/ex7.smt2 b/test/regress/regress0/quantifiers/ex7.smt2 deleted file mode 100644 index 11a83fdc4..000000000 --- a/test/regress/regress0/quantifiers/ex7.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-logic AUFLIRA) -(set-info :smt-lib-version 2.0) -(set-info :category "industrial") -(set-info :status sat) -(declare-sort U 0) -(declare-fun a () U) -(declare-fun b () U) -(declare-fun c () U) -(declare-fun f (U) U) -(assert (and (= a b) (forall ((x U)) (=> (or (= (f x) c) (= x a)) (= x b))))) -(check-sat) -(get-info :reason-unknown) -(exit) diff --git a/test/regress/regress0/quantifiers/ex7.smt2.expect b/test/regress/regress0/quantifiers/ex7.smt2.expect deleted file mode 100644 index 2bd8349de..000000000 --- a/test/regress/regress0/quantifiers/ex7.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% EXPECT: unknown -% EXPECT: (:reason-unknown incomplete) -- 2.30.2