diff options
19 files changed, 108 insertions, 84 deletions
diff --git a/contrib/run-script-casc26-fnt b/contrib/run-script-casc26-fnt index c3c12f937..c89d3eb0a 100644 --- a/contrib/run-script-casc26-fnt +++ b/contrib/run-script-casc26-fnt @@ -33,5 +33,5 @@ function finishwith { trywith 60 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair trywith 30 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair trywith 60 --finite-model-find --decision=internal --sort-inference --uf-ss-fair -finishwith --finite-model-find --mbqi=abs --sort-inference --uf-ss-fair +finishwith --finite-model-find --macros-quant --macros-quant-mode=all --sort-inference --uf-ss-fair # echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc26-fof b/contrib/run-script-casc26-fof index 376d18b15..5ec312cb7 100644 --- a/contrib/run-script-casc26-fof +++ b/contrib/run-script-casc26-fof @@ -34,7 +34,7 @@ function finishwith { # designed for 300 seconds trywith 20 --relational-triggers --full-saturate-quant trywith 20 --no-e-matching --full-saturate-quant -trywith 15 --finite-model-find --mbqi=abs +trywith 15 --finite-model-find --uf-ss=no-minimal trywith 5 --multi-trigger-when-single --full-saturate-quant trywith 5 --trigger-sel=max --full-saturate-quant trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant @@ -43,8 +43,8 @@ trywith 15 --prenex-quant=none --full-saturate-quant trywith 15 --fs-inst --decision=internal --full-saturate-quant trywith 15 --relevant-triggers --full-saturate-quant trywith 15 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair -trywith 30 --full-saturate-quant --macros-quant -trywith 30 --fs-inst --full-saturate-quant +trywith 30 --decision=internal --full-saturate-quant +trywith 30 --qcf-vo-exp --full-saturate-quant trywith 30 --no-quant-cf --full-saturate-quant -finishwith --qcf-vo-exp --full-saturate-quant +finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant # echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc26-tfa b/contrib/run-script-casc26-tfa index aa65a938f..05062bf5c 100644 --- a/contrib/run-script-casc26-tfa +++ b/contrib/run-script-casc26-tfa @@ -31,9 +31,9 @@ function finishwith { trywith 10 --decision=internal --full-saturate-quant trywith 10 --finite-model-find --decision=internal -trywith 10 --nl-ext --nl-ext-tplanes --full-saturate-quant +trywith 10 --multi-trigger-when-single --multi-trigger-priority --nl-ext --nl-ext-tplanes --full-saturate-quant trywith 10 --partial-triggers --full-saturate-quant trywith 15 --cbqi-all --purify-triggers --full-saturate-quant trywith 15 --nl-ext --fs-inst --full-saturate-quant -finishwith --full-saturate-quant --macros-quant +finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant # echo "% SZS status" "GaveUp for $filename" diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 4e73fa6cf..dcee52337 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -353,7 +353,7 @@ definedFun[CVC4::Expr& expr] MK_EXPR(CVC4::kind::TO_INTEGER, expr), MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr)))); if(remainder) { - expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)); + expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d))); } expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); } @@ -368,7 +368,7 @@ definedFun[CVC4::Expr& expr] MK_EXPR(CVC4::kind::TO_INTEGER, expr), MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr)))); if(remainder) { - expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)); + expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d))); } expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); } @@ -381,7 +381,7 @@ definedFun[CVC4::Expr& expr] expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d); expr = MK_EXPR(CVC4::kind::TO_INTEGER, expr); if(remainder) { - expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)); + expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d))); } expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); } diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index d817fb179..082fa2580 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -37,6 +37,7 @@ struct ArraySelectTypeRule { } TypeNode indexType = n[1].getType(check); if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ + //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ //FIXME:typing throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array"); } } @@ -56,9 +57,11 @@ struct ArrayStoreTypeRule { TypeNode indexType = n[1].getType(check); TypeNode valueType = n[2].getType(check); if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ + //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ //FIXME:typing throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); } - if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){ + if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){ + //if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ //FIXME:typing Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl; Debug("array-types") << "value types: " << valueType << std::endl; throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array"); diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 412b3d7ec..0540044b5 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -80,9 +80,12 @@ struct DatatypeConstructorTypeRule { << (*tchild_it) << std::endl; TypeNode argumentType = *tchild_it; if (!childType.isComparableTo(argumentType)) { + //if (!childType.isSubtypeOf(argumentType)) { //FIXME:typing std::stringstream ss; - ss << "bad type for constructor argument:\nexpected: " - << argumentType << "\ngot : " << childType; + ss << "bad type for constructor argument:\n" + << "child type: " << childType << "\n" + << "not subtype: " << argumentType << "\n" + << "in term : " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } } diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 1543b2ebd..521f1c978 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -502,6 +502,14 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node } } } + if( Trace.isOn("cegqi-si-apply-subs-debug") ){ + Trace("cegqi-si-apply-subs-debug") << "req_coeff = " << req_coeff << " " << tn << std::endl; + for( unsigned i=0; i<subs.size(); i++ ){ + Trace("cegqi-si-apply-subs-debug") << " " << vars[i] << " -> " << subs[i] << " types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl; + Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) ); + } + } + if( !req_coeff ){ Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); if( n!=nret ){ @@ -515,8 +523,12 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node std::vector< Node > nsubs; for( unsigned i=0; i<vars.size(); i++ ){ if( !coeff[i].isNull() ){ + Assert( vars[i].getType().isInteger() ); Assert( coeff[i].isConst() ); - nsubs.push_back( Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst<Rational>() ) ) )); + Node nn =NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst<Rational>() ) ); + nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn ); + nn = Rewriter::rewrite( nn ); + nsubs.push_back( nn ); }else{ nsubs.push_back( subs[i] ); } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 2cef4f6a1..2a7b589d0 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -659,6 +659,10 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { } bool FullSaturation::process( Node f, bool fullEffort ){ + // ignore if constant true (rare case of non-standard quantifier whose body is rewritten to true) + if( f[1].isConst() && f[1].getConst<bool>() ){ + return false; + } //first, try from relevant domain RelevantDomain * rd = d_quantEngine->getRelevantDomain(); unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; @@ -770,7 +774,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){ } } } - //term enumerator? + //TODO : term enumerator? return false; } diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 636bfdb59..99dbb7ab9 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -44,7 +44,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl; //first, collect macro definitions std::vector< Node > macro_assertions; - for( unsigned i=0; i<assertions.size(); i++ ){ + for( int i=0; i<(int)assertions.size(); i++ ){ Trace("macros-debug") << " process assertion " << assertions[i] << std::endl; if( processAssertion( assertions[i] ) ){ PROOF( @@ -167,6 +167,7 @@ bool QuantifierMacros::isBoundVarApplyUf( Node n ) { Assert( n.getKind()==APPLY_UF ); TypeNode tno = n.getOperator().getType(); std::map< Node, bool > vars; + // allow if a vector of unique variables of the same type as UF arguments for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( n[i].getKind()!=BOUND_VARIABLE ){ return false; @@ -174,11 +175,6 @@ bool QuantifierMacros::isBoundVarApplyUf( Node n ) { if( n[i].getType()!=tno[i] ){ return false; } - if( !tno[i].isSort() && !tno[i].isReal() && ( !tno[i].isDatatype() || tno[i].isParametricDatatype() ) && - !tno[i].isBitVector() && !tno[i].isString() && !tno[i].isFloatingPoint() ){ - //only non-parametric types are supported - return false; - } if( vars.find( n[i] )==vars.end() ){ vars[n[i]] = true; }else{ @@ -331,6 +327,7 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod }else{ //literal case if( isMacroLiteral( n, pol ) ){ + Trace("macros-debug") << "Check macro literal : " << n << std::endl; std::map< Node, bool > visited; std::vector< Node > candidates; for( size_t i=0; i<n.getNumChildren(); i++ ){ @@ -339,6 +336,7 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod for( size_t i=0; i<candidates.size(); i++ ){ Node m = candidates[i]; Node op = m.getOperator(); + Trace("macros-debug") << "Check macro candidate : " << m << std::endl; if( d_macro_defs.find( op )==d_macro_defs.end() ){ std::vector< Node > fvs; visited.clear(); @@ -416,6 +414,7 @@ Node QuantifierMacros::simplify( Node n ){ if( it!=d_macro_defs.end() && !it->second.isNull() ){ //only apply if children are subtypes of arguments bool success = true; + // FIXME : this can be eliminated when we have proper typing rules std::vector< Node > cond; TypeNode tno = op.getType(); for( unsigned i=0; i<children.size(); i++ ){ @@ -423,13 +422,13 @@ Node QuantifierMacros::simplify( Node n ){ if( etc.isNull() ){ //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op, // and not ensuring it applies to n when its types are correct. - //however, this should never fail: we never process types for which we cannot constuct conditions that ensure correct types, e.g. (is-int t). - Assert( false ); + //Assert( false ); success = false; break; }else if( !etc.isConst() ){ cond.push_back( etc ); } + Assert( children[i].getType().isSubtypeOf( tno[i] ) ); } if( success ){ //do substitution if necessary diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index f2a4e6d17..5b02a877a 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -398,49 +398,46 @@ bool Trigger::isSimpleTrigger( Node n ){ } //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula -void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, +void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, - bool pol, bool hasPol, bool epol, bool hasEPol ){ - std::map< Node, Node >::iterator itv = visited.find( n ); + bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable ){ + std::map< Node, std::vector< Node > >::iterator itv = visited.find( n ); if( itv==visited.end() ){ - visited[ n ] = Node::null(); + visited[ n ].clear(); Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl; if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){ Node nu; bool nu_single = false; - if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ + if( knowIsUsable ){ + nu = n; + }else if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ nu = getIsUsableTrigger( n, q ); - if( !nu.isNull() ){ - Assert( nu.getKind()!=NOT ); - Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl; - Node reqEq; - if( nu.getKind()==EQUAL ){ - if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){ - if( hasPol ){ - reqEq = nu[1]; - } - nu = nu[0]; - } - } - Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) ); - Assert( isUsableTrigger( nu, q ) ); - //do not add if already visited - bool add = true; - if( n!=nu ){ - std::map< Node, Node >::iterator itvu = visited.find( nu ); - if( itvu!=visited.end() ){ - add = false; + if( !nu.isNull() && nu!=n ){ + collectPatTerms2( q, nu, visited, tinfo, tstrt, exclude, added, pol, hasPol, epol, hasEPol, true ); + // copy to n + visited[n].insert( visited[n].end(), added.begin(), added.end() ); + return; + } + } + if( !nu.isNull() ){ + Assert( nu==n ); + Assert( nu.getKind()!=NOT ); + Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl; + Node reqEq; + if( nu.getKind()==EQUAL ){ + if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){ + if( hasPol ){ + reqEq = nu[1]; } - } - if( add ){ - Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl; - visited[ nu ] = nu; - tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq ); - nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren(); - }else{ - nu = Node::null(); + nu = nu[0]; } } + Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) ); + Assert( isUsableTrigger( nu, q ) ); + //tinfo.find( nu )==tinfo.end() + Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl; + tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq ); + nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren(); } Node nrec = nu.isNull() ? n : nu; std::vector< Node > added2; @@ -451,6 +448,7 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol ); collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol ); } + // if this is not a usable trigger, don't worry about caching the results, since triggers do not contain non-usable subterms if( !nu.isNull() ){ bool rm_nu = false; for( unsigned i=0; i<added2.size(); i++ ){ @@ -461,7 +459,7 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ //discard all subterms Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl; - visited[added2[i]] = Node::null(); + visited[ added2[i] ].clear(); tinfo.erase( added2[i] ); }else{ if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){ @@ -476,18 +474,20 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, } } if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){ - visited[nu] = Node::null(); tinfo.erase( nu ); }else{ - Assert( std::find( added.begin(), added.end(), nu )==added.end() ); - added.push_back( nu ); + if( std::find( added.begin(), added.end(), nu )==added.end() ){ + added.push_back( nu ); + } } + visited[n].insert( visited[n].end(), added.begin(), added.end() ); } } }else{ - if( !itv->second.isNull() ){ - if( std::find( added.begin(), added.end(), itv->second )==added.end() ){ - added.push_back( itv->second ); + for( unsigned i=0; i<itv->second.size(); ++i ){ + Node t = itv->second[i]; + if( std::find( added.begin(), added.end(), t )==added.end() ){ + added.push_back( t ); } } } @@ -573,7 +573,7 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){ - std::map< Node, Node > visited; + std::map< Node, std::vector< Node > > visited; if( filterInst ){ //immediately do not consider any term t for which another term is an instance of t std::vector< Node > patTerms2; @@ -607,7 +607,7 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu //do not consider terms that have instances for( unsigned i=0; i<patTerms2.size(); i++ ){ if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){ - visited[ patTerms2[i] ] = Node::null(); + visited[ patTerms2[i] ].clear(); } } } @@ -615,9 +615,7 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu std::vector< Node > added; collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true ); for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){ - if( !visited[it->first].isNull() ){ - patTerms.push_back( it->first ); - } + patTerms.push_back( it->first ); } } diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 234025e7b..8d8f01926 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -137,9 +137,9 @@ private: static Node getIsUsableEq( Node q, Node eq ); static bool isUsableEqTerms( Node q, Node n1, Node n2 ); /** collect all APPLY_UF pattern terms for f in n */ - static void collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, + static void collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, - bool pol, bool hasPol, bool epol, bool hasEPol ); + bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false ); std::vector< Node > d_nodes; diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index a5a78e691..e2830b57e 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -116,7 +116,13 @@ struct MemberTypeRule { } TypeNode elementType = n[0].getType(check); if(!elementType.isComparableTo(setType.getSetElementType())) { - throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types"); + //if(!elementType.isSubtypeOf(setType.getSetElementType())) { //FIXME:typing + std::stringstream ss; + ss << "member operating on sets of different types:\n" + << "child type: " << elementType << "\n" + << "not subtype: " << setType.getSetElementType() << "\n" + << "in term : " << n; + throw TypeCheckingExceptionPrivate(n, ss.str()); } } return nodeManager->booleanType(); diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 5d97dda38..6f97a9662 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -46,12 +46,14 @@ class UfTypeRule { TypeNode currentArgument = (*argument_it).getType(); TypeNode currentArgumentType = *argument_type_it; if (!currentArgument.isComparableTo(currentArgumentType)) { + //if (!currentArgument.isSubtypeOf(currentArgumentType)) { //FIXME:typing std::stringstream ss; ss << "argument type is not a subtype of the function's argument " << "type:\n" << "argument: " << *argument_it << "\n" << "has type: " << (*argument_it).getType() << "\n" - << "not subtype: " << *argument_type_it; + << "not subtype: " << *argument_type_it << "\n" + << "in term : " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } } diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 index 20de79047..586aa64c7 100644 --- a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 +++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 @@ -1,18 +1,17 @@ ; COMMAND-LINE: --macros-quant ; EXPECT: unknown -; this will fail if type rule for APPLY_UF requires to be subtypes (set-logic ALL_SUPPORTED) (declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) -(declare-fun R ((List Int)) Bool) +(declare-fun R ((List Real)) Bool) (assert (forall ((x (List Int))) (R x))) (declare-fun j1 () (List Real)) (assert (not (R j1))) -(declare-fun Q ((Array Real Int)) Bool) +(declare-fun Q ((Array Int Real)) Bool) (assert (forall ((x (Array Real Int))) (Q x))) -(declare-fun j2 () (Array Int Real)) +(declare-fun j2 () (Array Real Real)) (assert (not (Q j2))) (check-sat) diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2 index 675c96d68..edacdbe37 100644 --- a/test/regress/regress0/quantifiers/macros-real-arg.smt2 +++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2 @@ -6,6 +6,6 @@ (assert (forall ((x Int)) (P x))) (declare-fun k () Real) (declare-fun k2 () Int) -(assert (or (not (P k)) (not (P k2)))) +(assert (or (not (P (to_int k))) (not (P k2)))) (assert (= k 0)) (check-sat) diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 index 836449cb9..42cfb3a11 100644 --- a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 +++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 @@ -5,8 +5,7 @@ (declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) -(declare-fun R ((List Int)) Bool) - +(declare-fun R ((List Real)) Bool) (assert (forall ((x (List Int))) (R x))) (declare-fun j1 () (List Real)) (assert (not (R j1))) diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2 index 08615abf6..a7fe58ac9 100644 --- a/test/regress/regress0/quantifiers/subtype-param.smt2 +++ b/test/regress/regress0/quantifiers/subtype-param.smt2 @@ -3,7 +3,7 @@ (declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) -(declare-fun R ((List Int)) Bool) +(declare-fun R ((List Real)) Bool) (assert (forall ((x (List Real))) (R x))) (declare-fun Q ((Array Int Real)) Bool) diff --git a/test/regress/regress0/sets/sets-poly-nonint.smt2 b/test/regress/regress0/sets/sets-poly-nonint.smt2 index 441716dcf..a0e883ace 100644 --- a/test/regress/regress0/sets/sets-poly-nonint.smt2 +++ b/test/regress/regress0/sets/sets-poly-nonint.smt2 @@ -7,5 +7,5 @@ (assert (member 1.5 t)) (assert (member 2.5 r)) (assert (member 3.5 u)) -(assert (or (member 4.5 s) (= s t) (= s r) (= s u) (= s (singleton 6.5)))) +(assert (or (= s t) (= s r) (= s u))) (check-sat) diff --git a/test/regress/regress0/sets/sets-tuple-poly.cvc b/test/regress/regress0/sets/sets-tuple-poly.cvc index 8d87345f6..64fb310be 100644 --- a/test/regress/regress0/sets/sets-tuple-poly.cvc +++ b/test/regress/regress0/sets/sets-tuple-poly.cvc @@ -7,11 +7,10 @@ b : SET OF [INT, REAL]; x : [ REAL, REAL ]; - ASSERT NOT x = (0,0); -ASSERT x IS_IN a; -ASSERT x IS_IN b; +ASSERT (x.0, FLOOR(x.1)) IS_IN a; +ASSERT (FLOOR(x.0), x.1) IS_IN b; ASSERT NOT x.0 = x.1; |