From: ajreynol Date: Tue, 12 Apr 2016 21:29:20 +0000 (-0500) Subject: Bug fixes related to parametric datatypes + theory combination + quantifiers. Add... X-Git-Tag: cvc5-1.0.0~6049^2~72 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd01099518aab8d42d788dfadadbe11763ec9d18;p=cvc5.git Bug fixes related to parametric datatypes + theory combination + quantifiers. Add regression. --- diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 1653ab636..eb8b23973 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -540,8 +540,9 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { if( tst==d_true ){ n_ret = sel; }else{ - mkExpDefSkolem( selector, n[0].getType(), n.getType() ); - Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0] ); + TypeNode ndt = n[0].getType(); + mkExpDefSkolem( selector, ndt, n.getType() ); + Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ndt][ selector ], n[0] ); if( tst==NodeManager::currentNM()->mkConst( false ) ){ n_ret = sk; }else{ @@ -994,10 +995,10 @@ void TheoryDatatypes::getSelectorsForCons( Node r, std::map< int, bool >& sels ) } void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) { - if( d_exp_def_skolem.find( sel )==d_exp_def_skolem.end() ){ + if( d_exp_def_skolem[dt].find( sel )==d_exp_def_skolem[dt].end() ){ std::stringstream ss; ss << sel << "_uf"; - d_exp_def_skolem[ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(), + d_exp_def_skolem[dt][ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(), NodeManager::currentNM()->mkFunctionType( dt, rt ) ); } } @@ -1299,7 +1300,8 @@ void TheoryDatatypes::computeCareGraph(){ TNode y = f2[k]; Assert(d_equalityEngine.hasTerm(x)); Assert(d_equalityEngine.hasTerm(y)); - if( areDisequal(x, y) ){ + //need to consider types for parametric selectors + if( x.getType()!=y.getType() || areDisequal(x, y) ){ somePairIsDisequal = true; break; }else if( !d_equalityEngine.areEqual( x, y ) ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index b826780fc..4bf04e08c 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -183,7 +183,7 @@ private: /** counter for forcing assignments (ensures fairness) */ unsigned d_dtfCounter; /** expand definition skolem functions */ - std::map< Node, Node > d_exp_def_skolem; + std::map< TypeNode, std::map< Node, Node > > d_exp_def_skolem; /** sygus utilities */ SygusSplit * d_sygus_split; SygusSymBreak * d_sygus_sym_break; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index bb514f41b..8c67eb95e 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -691,10 +691,13 @@ bool FullSaturation::process( Node f, bool fullEffort ){ if( max_zero[i] ){ //no terms available, will report incomplete instantiation terms.push_back( Node::null() ); + Trace("inst-alg-rd") << " null" << std::endl; }else if( r==0 ){ terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] ); + Trace("inst-alg-rd") << " " << rd->getRDomain( f, i )->d_terms[childIndex[i]] << std::endl; }else{ terms.push_back( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) ); + Trace("inst-alg-rd") << " " << d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) << std::endl; } } if( d_quantEngine->addInstantiation( f, terms, false ) ){ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 1cbfbd99b..c796333b3 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -508,9 +508,9 @@ bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRe if( it!=d_var_rel_dom.end() ){ for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ for( unsigned j=0; jsecond.size(); j++ ){ - Debug("qcf-match-debug2") << n << " in relevant domain " << it2->second << "." << it2->second[j] << "?" << std::endl; + Debug("qcf-match-debug2") << n << " in relevant domain " << it2->first << "." << it2->second[j] << "?" << std::endl; if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){ - Debug("qcf-match-debug") << " -> fail, since " << n << " is not in relevant domain of " << it2->second << "." << it2->second[j] << std::endl; + Debug("qcf-match-debug") << " -> fail, since " << n << " is not in relevant domain of " << it2->first << "." << it2->second[j] << std::endl; return false; } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index ef301c2cf..51c72d7bb 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -126,9 +126,10 @@ Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) { } Node TermDb::getMatchOperator( Node n ) { - //return n.getOperator(); Kind k = n.getKind(); - if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ){ + //datatype operators may be parametric, always assume they are + if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || + k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ){ //since it is parametric, use a particular one as op TypeNode tn = n[0].getType(); Node op = n.getOperator(); @@ -241,10 +242,11 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQ if( itv != visited.end() ){ return itv->second; } - Assert( n.getKind()!=BOUND_VARIABLE ); Trace("term-db-eval") << "evaluate term : " << n << std::endl; Node ret; - if( !qy->hasTerm( n ) ){ + if( n.getKind()==BOUND_VARIABLE ){ + return n; + }else if( !qy->hasTerm( n ) ){ //term is not known to be equal to a representative in equality engine, evaluate it if( n.getKind()==FORALL ){ ret = Node::null(); diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index b51313deb..6b5e0d1ed 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -78,7 +78,8 @@ TESTS = \ pure_dt_cbqi.smt2 \ florian-case-ax.smt2 \ double-pattern.smt2 \ - qcf-rel-dom-opt.smt2 + qcf-rel-dom-opt.smt2 \ + parametric-lists.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/parametric-lists.smt2 b/test/regress/regress0/quantifiers/parametric-lists.smt2 new file mode 100644 index 000000000..c117934f8 --- /dev/null +++ b/test/regress/regress0/quantifiers/parametric-lists.smt2 @@ -0,0 +1,42 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes (T) ((List (cons (head T) (tail (List T))) (nil)))) +(declare-datatypes () ((KV (kv (key Int) (value Int)) (nilKV)))) ; key value pair +(declare-fun mapper ((List Int)) (List KV)) +(assert + (forall + ((input (List Int))) + (ite + (= input (as nil (List Int))) + (= (as nil (List KV)) (mapper input)) + (= (cons (kv 0 (head input)) (mapper (tail input))) (mapper input)) + ) + ) +) +(declare-fun reduce ((List KV)) Int) +(assert + (forall + ((inputk (List KV))) + (ite + (= inputk (as nil (List KV))) + (= 0 (reduce inputk)) + (= (+ (value (head inputk)) (reduce (tail inputk))) (reduce inputk)) + ) + ) +) +(declare-fun sum ((List Int)) Int) +(assert + (forall + ((input (List Int))) + (ite + (= input (as nil (List Int))) + (= 0 (sum input)) + (= (+ (head input) (sum (tail input))) (sum input)) + ) + ) +) +(assert + (not (= (sum (cons 0 (as nil (List Int)))) (reduce (mapper (cons 0 (as nil (List Int))))))) +) +(check-sat) +