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"
# 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
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"
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"
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);
}
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);
}
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);
}
}
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");
}
}
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");
<< (*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());
}
}
}
}
}
+ 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 ){
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] );
}
}
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;
}
}
}
- //term enumerator?
+ //TODO : term enumerator?
return false;
}
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(
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;
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{
}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++ ){
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();
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++ ){
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
}
//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;
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++ ){
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() ){
}
}
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 );
}
}
}
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;
//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();
}
}
}
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 );
}
}
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;
}
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();
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());
}
}
; 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)
(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)
(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-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)
(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)
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;
projects / cvc5.git / commitdiff