diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 5 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/macros.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 88 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.h | 4 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 8 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 4 |
9 files changed, 89 insertions, 62 deletions
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()); } } |