From: Andrew Reynolds Date: Tue, 10 Apr 2018 01:09:51 +0000 (-0500) Subject: Fix higher-order term indexing. (#1754) X-Git-Tag: cvc5-1.0.0~5165 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fc9e113c5f9ea99a1308d0f36b1aad778747870c;p=cvc5.git Fix higher-order term indexing. (#1754) --- diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index ec0a4039a..0252def60 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -1042,8 +1042,12 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, TNode t = tat->getNodeData(); Debug("simple-trigger") << "Actual term is " << t << std::endl; //convert to actual used terms - for( std::map< int, int >::iterator it = d_var_num.begin(); it != d_var_num.end(); ++it ){ + for (std::map::iterator it = d_var_num.begin(); + it != d_var_num.end(); + ++it) + { if( it->second>=0 ){ + Assert(it->first < t.getNumChildren()); Debug("simple-trigger") << "...set " << it->second << " " << t[it->first] << std::endl; m.setValue( it->second, t[it->first] ); } diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index cbd5702a0..2e7e3c90c 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -644,8 +644,11 @@ class InstMatchGeneratorSimple : public IMGenerator { std::vector< TypeNode > d_match_pattern_arg_types; /** The match operator d_match_pattern (see TermDb::getMatchOperator). */ Node d_op; - /** Map from child number to variable index. */ - std::map< int, int > d_var_num; + /** + * Map from child number of d_match_pattern to variable index, or -1 if the + * child is not a variable. + */ + std::map d_var_num; /** add instantiations, helper function. * * m is the current match we are building, diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2013bff5d..54c19378a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -222,49 +222,71 @@ Node TermDb::getMatchOperator( Node n ) { } } -void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){ +void TermDb::addTerm(Node n, + std::set& added, + bool withinQuant, + bool withinInstClosure) +{ //don't add terms in quantifier bodies if( withinQuant && !options::registerQuantBodyTerms() ){ return; - }else{ - bool rec = false; - if( d_processed.find( n )==d_processed.end() ){ - d_processed.insert(n); - if( !TermUtil::hasInstConstAttr(n) ){ - Trace("term-db-debug") << "register term : " << n << std::endl; - d_type_map[ n.getType() ].push_back( n ); - //if this is an atomic trigger, consider adding it - if( inst::Trigger::isAtomicTrigger( n ) ){ - Trace("term-db") << "register term in db " << n << std::endl; - - Node op = getMatchOperator( n ); - Trace("term-db-debug") << " match operator is : " << op << std::endl; + } + bool rec = false; + if (d_processed.find(n) == d_processed.end()) + { + d_processed.insert(n); + if (!TermUtil::hasInstConstAttr(n)) + { + Trace("term-db-debug") << "register term : " << n << std::endl; + d_type_map[n.getType()].push_back(n); + // if this is an atomic trigger, consider adding it + if (inst::Trigger::isAtomicTrigger(n)) + { + Trace("term-db") << "register term in db " << n << std::endl; + + Node op = getMatchOperator(n); + Trace("term-db-debug") << " match operator is : " << op << std::endl; + if (d_op_map.find(op) == d_op_map.end()) + { d_ops.push_back(op); - d_op_map[op].push_back( n ); - added.insert( n ); } - }else{ - setTermInactive( n ); + d_op_map[op].push_back(n); + added.insert(n); + // If we are higher-order, we may need to register more terms. + if (options::ufHo()) + { + addTermHo(n, added, withinQuant, withinInstClosure); + } } - rec = true; } - if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){ - d_iclosure_processed.insert( n ); - rec = true; + else + { + setTermInactive(n); } - if( rec && n.getKind()!=FORALL ){ - for( unsigned i=0; igetActiveEqualityEngine(); - for( unsigned j=0; jhasTerm( n[j] ) ? ee->getRepresentative( n[j] ) : n[j]; + for (const TNode& nc : n) + { + TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc; d_arg_reps[n].push_back( r ); } } @@ -272,141 +294,234 @@ void TermDb::computeArgReps( TNode n ) { void TermDb::computeUfEqcTerms( TNode f ) { Assert( f==getOperatorRepresentative( f ) ); - if( d_func_map_eqc_trie.find( f )==d_func_map_eqc_trie.end() ){ - d_func_map_eqc_trie[f].clear(); - // get the matchable operators in the equivalence class of f - std::vector< TNode > ops; - ops.push_back( f ); - if( options::ufHo() ){ - ops.insert( ops.end(), d_ho_op_rep_slaves[f].begin(), d_ho_op_rep_slaves[f].end() ); - } - eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine(); - for( unsigned j=0; jareEqual( ff, f ) ); - for( unsigned i=0; ihasTerm( n ) ? ee->getRepresentative( n ) : n; - d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] ); - } - } + if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end()) + { + return; + } + d_func_map_eqc_trie[f].clear(); + // get the matchable operators in the equivalence class of f + std::vector ops; + ops.push_back(f); + if (options::ufHo()) + { + ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end()); + } + eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); + for (const Node& ff : ops) + { + for (const TNode& n : d_op_map[ff]) + { + if (hasTermCurrent(n) && isTermActive(n)) + { + computeArgReps(n); + TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : n; + d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]); } } } } void TermDb::computeUfTerms( TNode f ) { + if (d_op_nonred_count.find(f) != d_op_nonred_count.end()) + { + // already computed + return; + } Assert( f==getOperatorRepresentative( f ) ); - if( d_op_nonred_count.find( f )==d_op_nonred_count.end() ){ - d_op_nonred_count[ f ] = 0; - // get the matchable operators in the equivalence class of f - std::vector< TNode > ops; - ops.push_back( f ); - if( options::ufHo() ){ - ops.insert( ops.end(), d_ho_op_rep_slaves[f].begin(), d_ho_op_rep_slaves[f].end() ); - } - Trace("term-db-debug") << "computeUfTerms for " << f << std::endl; - unsigned congruentCount = 0; - unsigned nonCongruentCount = 0; - unsigned alreadyCongruentCount = 0; - unsigned relevantCount = 0; - eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); - for( unsigned j=0; jareEqual( ff, f ) ); - std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( ff ); - if( it!=d_op_map.end() ){ - Trace("term-db-debug") - << "Adding terms for operator " << ff << std::endl; - for( unsigned i=0; isecond.size(); i++ ){ - Node n = it->second[i]; - //to be added to term index, term must be relevant, and exist in EE - if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ - relevantCount++; - if( isTermActive( n ) ){ - computeArgReps( n ); - - Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; - for( unsigned i=0; i ops; + ops.push_back(f); + if (options::ufHo()) + { + ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end()); + } + Trace("term-db-debug") << "computeUfTerms for " << f << std::endl; + unsigned congruentCount = 0; + unsigned nonCongruentCount = 0; + unsigned alreadyCongruentCount = 0; + unsigned relevantCount = 0; + eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); + NodeManager* nm = NodeManager::currentNM(); + for (const Node& ff : ops) + { + std::map >::iterator it = d_op_map.find(ff); + if (it == d_op_map.end()) + { + // no terms for this operator + continue; + } + Trace("term-db-debug") << "Adding terms for operator " << ff << std::endl; + for (const Node& n : it->second) + { + // to be added to term index, term must be relevant, and exist in EE + if (!hasTermCurrent(n) || !ee->hasTerm(n)) + { + Trace("term-db-debug") << n << " is not relevant." << std::endl; + continue; + } + + relevantCount++; + if (!isTermActive(n)) + { + Trace("term-db-debug") << n << " is already redundant." << std::endl; + alreadyCongruentCount++; + continue; + } + + computeArgReps(n); + Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; + for (unsigned i = 0, size = d_arg_reps[n].size(); i < size; i++) + { + Trace("term-db-debug") << d_arg_reps[n][i] << " "; + if (std::find(d_func_map_rel_dom[f][i].begin(), + d_func_map_rel_dom[f][i].end(), + d_arg_reps[n][i]) + == d_func_map_rel_dom[f][i].end()) + { + d_func_map_rel_dom[f][i].push_back(d_arg_reps[n][i]); + } + } + Trace("term-db-debug") << std::endl; + Assert(ee->hasTerm(n)); + Trace("term-db-debug") << " and value : " << ee->getRepresentative(n) + << std::endl; + Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]); + Assert(ee->hasTerm(at)); + Trace("term-db-debug2") << "...add term returned " << at << std::endl; + if (at != n && ee->areEqual(at, n)) + { + setTermInactive(n); + Trace("term-db-debug") << n << " is redundant." << std::endl; + congruentCount++; + continue; + } + if (ee->areDisequal(at, n, false)) + { + std::vector lits; + lits.push_back(nm->mkNode(EQUAL, at, n)); + bool success = true; + if (options::ufHo()) + { + // operators might be disequal + if (ops.size() > 1) + { + Node atf = getMatchOperator(at); + Node nf = getMatchOperator(n); + if (atf != nf) + { + if (at.getKind() == APPLY_UF && n.getKind() == APPLY_UF) + { + lits.push_back(atf.eqNode(nf).negate()); } - Trace("term-db-debug") << std::endl; - Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; - Node at = d_func_map_trie[ f ].addOrGetTerm( n, d_arg_reps[n] ); - Trace("term-db-debug2") << "...add term returned " << at << std::endl; - if( at!=n && ee->areEqual( at, n ) ){ - setTermInactive( n ); - Trace("term-db-debug") << n << " is redundant." << std::endl; - congruentCount++; - }else{ - if( at!=n && ee->areDisequal( at, n, false ) ){ - std::vector< Node > lits; - lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at, n ) ); - bool success = true; - if( options::ufHo() ){ - //operators might be disequal - if( ops.size()>1 ){ - Node atf = getMatchOperator( at ); - Node nf = getMatchOperator( n ); - if( atf!=nf ){ - if( at.getKind()==APPLY_UF && n.getKind()==APPLY_UF ){ - lits.push_back( atf.eqNode( nf ).negate() ); - }else{ - success = false; - Assert( false ); - } - } - } - } - if( success ){ - for( unsigned k=0; kmkNode( EQUAL, at[k], n[k] ).negate() ); - } - } - Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits ); - if( Trace.isOn("term-db-lemma") ){ - Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; - if( !d_quantEngine->getTheoryEngine()->needCheck() ){ - Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; - // we should be a full effort check, prior to theory combination - } - Trace("term-db-lemma") << " add lemma : " << lem << std::endl; - } - d_quantEngine->addLemma( lem ); - d_quantEngine->setConflict(); - d_consistent_ee = false; - return; - } - } - nonCongruentCount++; - d_op_nonred_count[ f ]++; + else + { + success = false; + Assert(false); } - }else{ - Trace("term-db-debug") << n << " is already redundant." << std::endl; - alreadyCongruentCount++; } - }else{ - Trace("term-db-debug") << n << " is not relevant." << std::endl; } } - if( Trace.isOn("tdb") ){ - Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / "; - Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / "; - Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl; + if (success) + { + Assert(at.getNumChildren() == n.getNumChildren()); + for (unsigned k = 0, size = at.getNumChildren(); k < size; k++) + { + if (at[k] != n[k]) + { + lits.push_back(nm->mkNode(EQUAL, at[k], n[k]).negate()); + } + } + Node lem = lits.size() == 1 ? lits[0] : nm->mkNode(OR, lits); + if (Trace.isOn("term-db-lemma")) + { + Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " + << n << "!!!!" << std::endl; + if (!d_quantEngine->getTheoryEngine()->needCheck()) + { + Trace("term-db-lemma") << " all theories passed with no lemmas." + << std::endl; + // we should be a full effort check, prior to theory combination + } + Trace("term-db-lemma") << " add lemma : " << lem << std::endl; + } + d_quantEngine->addLemma(lem); + d_quantEngine->setConflict(); + d_consistent_ee = false; + return; } } + nonCongruentCount++; + d_op_nonred_count[f]++; + } + if (Trace.isOn("tdb")) + { + Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount + << " / "; + Trace("tdb") << (nonCongruentCount + congruentCount) << " / " + << (nonCongruentCount + congruentCount + + alreadyCongruentCount) + << " / "; + Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl; } } } +void TermDb::addTermHo(Node n, + std::set& added, + bool withinQuant, + bool withinInstClosure) +{ + Assert(options::ufHo()); + if (n.getType().isFunction()) + { + // nothing special to do with functions + return; + } + NodeManager* nm = NodeManager::currentNM(); + Node curr = n; + std::vector args; + while (curr.getKind() == HO_APPLY) + { + args.insert(args.begin(), curr[1]); + curr = curr[0]; + if (!curr.isVar()) + { + // purify the term + std::map::iterator itp = d_ho_fun_op_purify.find(curr); + Node psk; + if (itp == d_ho_fun_op_purify.end()) + { + psk = nm->mkSkolem("pfun", + curr.getType(), + "purify for function operator term indexing"); + d_ho_fun_op_purify[curr] = psk; + // we do not add it to d_ops since it is an internal operator + } + else + { + psk = itp->second; + } + std::vector children; + children.push_back(psk); + children.insert(children.end(), args.begin(), args.end()); + Node p_n = nm->mkNode(APPLY_UF, children); + Trace("term-db") << "register term in db (via purify) " << p_n + << std::endl; + // also add this one internally + d_op_map[psk].push_back(p_n); + // maintain backwards mapping + d_ho_purify_to_term[p_n] = n; + } + } + if (!args.empty() && curr.isVar()) + { + // also add standard application version + args.insert(args.begin(), curr); + Node uf_n = nm->mkNode(APPLY_UF, args); + addTerm(uf_n, added, withinQuant, withinInstClosure); + } +} Node TermDb::getOperatorRepresentative( TNode op ) const { std::map< TNode, TNode >::const_iterator it = d_ho_op_rep.find( op ); @@ -799,6 +914,37 @@ bool TermDb::reset( Theory::Effort effort ){ d_consistent_ee = true; eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); + + Assert(ee->consistent()); + // if higher-order, add equalities for the purification terms now + if (options::ufHo()) + { + Trace("quant-ho") + << "TermDb::reset : assert higher-order purify equalities..." + << std::endl; + for (std::pair& pp : d_ho_purify_to_term) + { + if (ee->hasTerm(pp.second) + && (!ee->hasTerm(pp.first) || !ee->areEqual(pp.second, pp.first))) + { + Node eq; + std::map::iterator itpe = d_ho_purify_to_eq.find(pp.first); + if (itpe == d_ho_purify_to_eq.end()) + { + eq = Rewriter::rewrite(pp.first.eqNode(pp.second)); + d_ho_purify_to_eq[pp.first] = eq; + } + else + { + eq = itpe->second; + } + Trace("quant-ho") << "- assert purify equality : " << eq << std::endl; + ee->assertEquality(eq, true, eq); + Assert(ee->consistent()); + } + } + } + //compute has map if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){ d_has_map.clear(); @@ -838,8 +984,8 @@ bool TermDb::reset( Theory::Effort effort ){ } } //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed - for( std::unordered_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){ - Node n = *it; + for (const Node& n : d_iclosure_processed) + { if( !ee->hasTerm( n ) ){ ee->addTerm( n ); } @@ -849,31 +995,45 @@ bool TermDb::reset( Theory::Effort effort ){ Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl; // build operator representative map d_ho_op_rep.clear(); - d_ho_op_rep_slaves.clear(); + d_ho_op_slaves.clear(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); if( r.getType().isFunction() ){ + Trace("quant-ho") << " process function eqc " << r << std::endl; Node first; eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); while( !eqc_i.isFinished() ){ TNode n = (*eqc_i); + Node n_use; if (n.isVar()) { - if (d_op_map.find(n) != d_op_map.end()) + n_use = n; + } + else + { + // use its purified variable, if it exists + std::map::iterator itp = d_ho_fun_op_purify.find(n); + if (itp != d_ho_fun_op_purify.end()) { - if (first.isNull()) - { - first = n; - d_ho_op_rep[n] = n; - } - else - { - Trace("quant-ho") << " have : " << n << " == " << first - << ", type = " << n.getType() << std::endl; - d_ho_op_rep[n] = first; - d_ho_op_rep_slaves[first].push_back(n); - } + n_use = itp->second; + } + } + Trace("quant-ho") << " - process " << n_use << ", from " << n + << std::endl; + if (!n_use.isNull() && d_op_map.find(n_use) != d_op_map.end()) + { + if (first.isNull()) + { + first = n_use; + d_ho_op_rep[n_use] = n_use; + } + else + { + Trace("quant-ho") << " have : " << n_use << " == " << first + << ", type = " << n_use.getType() << std::endl; + d_ho_op_rep[n_use] = first; + d_ho_op_slaves[first].push_back(n_use); } } ++eqc_i; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e440e68e9..3268e79d6 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -385,10 +385,55 @@ class TermDb : public QuantifiersUtil { */ void computeArgReps(TNode n); //------------------------------higher-order term indexing + /** + * Map from non-variable function terms to the operator used to purify it in + * this database. For details, see addTermHo. + */ + std::map d_ho_fun_op_purify; + /** + * Map from terms to the term that they purified. For details, see addTermHo. + */ + std::map d_ho_purify_to_term; + /** + * Map from terms in the domain of the above map to an equality between that + * term and its range in the above map. + */ + std::map d_ho_purify_to_eq; /** a map from matchable operators to their representative */ std::map< TNode, TNode > d_ho_op_rep; /** for each representative matchable operator, the list of other matchable operators in their equivalence class */ - std::map< TNode, std::vector< TNode > > d_ho_op_rep_slaves; + std::map > d_ho_op_slaves; + /** add term higher-order + * + * This registers additional terms corresponding to (possibly multiple) + * purifications of a higher-order term n. + * + * Consider the example: + * g : Int -> Int, f : Int x Int -> Int + * constraints: (@ f 0) = g, (f 0 1) = (@ (@ f 0) 1) = 3 + * pattern: (g x) + * where @ is HO_APPLY. + * We have that (g x){ x -> 1 } is an E-match for (@ (@ f 0) 1). + * With the standard registration in addTerm, we construct term indices for + * f, g, @ : Int x Int -> Int, @ : Int -> Int. + * However, to match (g x) with (@ (@ f 0) 1), we require that + * [1] -> (@ (@ f 0) 1) + * is an entry in the term index of g. To do this, we maintain a term + * index for a fresh variable pfun, the purification variable for + * (@ f 0). Thus, we register the term (psk 1) in the call to this function + * for (@ (@ f 0) 1). This ensures that, when processing the equality + * (@ f 0) = g, we merge the term indices of g and pfun. Hence, the entry + * [1] -> (@ (@ f 0) 1) + * is added to the term index of g, assuming g is the representative of + * the equivalence class of g and pfun. + * + * Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and + * d_ho_purify_to_term[(@ (@ f 0) 1)] = (psk 1). + */ + void addTermHo(Node n, + std::set& added, + bool withinQuant, + bool withinInstClosure); /** get operator representative */ Node getOperatorRepresentative( TNode op ) const; //------------------------------end higher-order term indexing diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index c45dd4833..fe9247ae8 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -148,7 +148,11 @@ public: //conversion between HO_APPLY AND APPLY_UF // cannot construct APPLY_UF if operator is partially applied or is not standard return Node::null(); } - // collects arguments into args, returns operator of a curried HO_APPLY node + /** + * Given a curried HO_APPLY term n, this method adds its arguments into args + * and returns its operator. If the argument opInArgs is true, then we add + * its operator to args. + */ static Node decomposeHoApply(TNode n, std::vector& args, bool opInArgs = false) { TNode curr = n; while( curr.getKind() == kind::HO_APPLY ){ diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c5b38dcd8..8f5b9bf4f 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1078,10 +1078,12 @@ REG1_TESTS = \ regress1/fmf/with-ind-104-core.smt2 \ regress1/gensys_brn001.smt2 \ regress1/ho/auth0068.smt2 \ + regress1/ho/fta0210.smt2 \ regress1/ho/fta0409.smt2 \ regress1/ho/ho-exponential-model.smt2 \ regress1/ho/ho-matching-enum-2.smt2 \ regress1/ho/ho-std-fmf.smt2 \ + regress1/ho/match-middle.smt2 \ regress1/hole6.cvc \ regress1/ite5.smt2 \ regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt \ diff --git a/test/regress/regress1/ho/fta0210.smt2 b/test/regress/regress1/ho/fta0210.smt2 new file mode 100644 index 000000000..9f0a39f25 --- /dev/null +++ b/test/regress/regress1/ho/fta0210.smt2 @@ -0,0 +1,64 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic ALL) +(declare-sort A$ 0) +(declare-sort Nat$ 0) +(declare-sort A_poly$ 0) +(declare-sort Nat_poly$ 0) +(declare-sort A_poly_poly$ 0) +(declare-fun p$ () A_poly$) +(declare-fun uu$ (A_poly$ (-> A_poly$ A_poly$) A_poly$) A_poly$) +(declare-fun one$ () Nat$) +(declare-fun suc$ (Nat$) Nat$) +(declare-fun uua$ (A_poly$) A_poly$) +(declare-fun uub$ (A$ (-> A$ A$) A$) A$) +(declare-fun uuc$ (A$) A$) +(declare-fun uud$ (Nat$ (-> Nat$ Nat$) Nat$) Nat$) +(declare-fun uue$ (Nat$) Nat$) +(declare-fun one$a () Nat_poly$) +(declare-fun one$b () A$) +(declare-fun one$c () A_poly$) +(declare-fun plus$ (A_poly$ A_poly$) A_poly$) +(declare-fun poly$ (A_poly$ A$) A$) +(declare-fun zero$ () A_poly$) +(declare-fun pCons$ (A$ A_poly$) A_poly$) +(declare-fun plus$a (Nat$ Nat$) Nat$) +(declare-fun plus$b (A$ A$) A$) +(declare-fun plus$c (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun poly$a (Nat_poly$ Nat$) Nat$) +(declare-fun poly$b (A_poly_poly$ A_poly$) A_poly$) +(declare-fun power$ (A$ Nat$) A$) +(declare-fun psize$ (A_poly$) Nat$) +(declare-fun times$ (A_poly$ A_poly$) A_poly$) +(declare-fun zero$a () Nat$) +(declare-fun zero$b () A$) +(declare-fun zero$c () Nat_poly$) +(declare-fun zero$d () A_poly_poly$) +(declare-fun pCons$a (Nat$ Nat_poly$) Nat_poly$) +(declare-fun pCons$b (A_poly$ A_poly_poly$) A_poly_poly$) +(declare-fun power$a (A_poly$ Nat$) A_poly$) +(declare-fun power$b (Nat_poly$ Nat$) Nat_poly$) +(declare-fun power$c (Nat$ Nat$) Nat$) +(declare-fun psize$a (A_poly_poly$) Nat$) +(declare-fun times$a (Nat$ Nat$) Nat$) +(declare-fun times$b (A$ A$) A$) +(declare-fun times$c (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun times$d (A_poly_poly$ A_poly_poly$) A_poly_poly$) +(declare-fun uminus$ (A_poly$) A_poly$) +(declare-fun uminus$a (A$) A$) +(declare-fun constant$ ((-> A$ A$)) Bool) +(declare-fun pcompose$ (A_poly$ A_poly$) A_poly$) +(declare-fun pcompose$a (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun pcompose$b (A_poly_poly$ A_poly_poly$) A_poly_poly$) +(declare-fun poly_shift$ (Nat$ A_poly$) A_poly$) +(declare-fun fold_coeffs$ ((-> A_poly$ (-> (-> A_poly$ A_poly$) (-> A_poly$ A_poly$))) A_poly_poly$ (-> A_poly$ A_poly$)) (-> A_poly$ A_poly$)) +(declare-fun poly_cutoff$ (Nat$ A_poly$) A_poly$) +(declare-fun fold_coeffs$a ((-> A$ (-> (-> A$ A$) (-> A$ A$))) A_poly$ (-> A$ A$)) (-> A$ A$)) +(declare-fun fold_coeffs$b ((-> Nat$ (-> (-> Nat$ Nat$) (-> Nat$ Nat$))) Nat_poly$ (-> Nat$ Nat$)) (-> Nat$ Nat$)) + +(assert (! (forall ((?v0 A$)) (= (poly$ zero$ ?v0) zero$b)) :named a14)) +(assert (! (forall ((?v0 (-> A$ A$))) (= (constant$ ?v0) (forall ((?v1 A$) (?v2 A$)) (= (?v0 ?v1) (?v0 ?v2))))) :named a69)) +(assert (! (not (constant$ (poly$ zero$))) :named a206)) + +(check-sat) +;(get-proof) diff --git a/test/regress/regress1/ho/match-middle.smt2 b/test/regress/regress1/ho/match-middle.smt2 new file mode 100644 index 000000000..0485f9a6f --- /dev/null +++ b/test/regress/regress1/ho/match-middle.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun f (Int Int Int) Int) +(declare-fun h (Int Int Int) Int) +(declare-fun g (Int Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) + +(assert (or (= (f a) g) (= (h a) g))) + +(assert (= (f a b d) c)) +(assert (= (h a b d) c)) + +(assert (forall ((x Int) (y Int)) (not (= (g x y) c)))) + +(check-sat)