From: Andrew Reynolds Date: Thu, 21 Sep 2017 00:32:46 +0000 (-0500) Subject: Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100) X-Git-Tag: cvc5-1.0.0~5624 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=75ccf2b4ad3dbcb1a0edfc336db35b45719a09f5;p=cvc5.git Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100) * Extend quantifier-free UF solver to higher-order. This includes an extensionality inference, and lazy conversion from APPLY_UF to HO_APPLY terms.Implements collectModelInfo and theory combination for HO_APPLY terms. * Update comments, minor changes to functions. Update APPLY_UF skolem to be user-context dependent. * Remove unused NodeList --- diff --git a/src/options/uf_options b/src/options/uf_options index cbac04b18..7e1cbdb17 100644 --- a/src/options/uf_options +++ b/src/options/uf_options @@ -41,4 +41,9 @@ option ufssFairness --uf-ss-fair bool :default true option ufssFairnessMonotone --uf-ss-fair-monotone bool :read-write :default false group monotone sorts when enforcing fairness for finite model finding +option ufHo --uf-ho bool :read-write :default false + enable support for higher-order reasoning +option ufHoExt --uf-ho-ext bool :read-write :default true + apply extensionality on function symbols + endmodule diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 981e3e2ac..e8cc3b385 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -28,6 +28,7 @@ #include "theory/uf/theory_uf_strong_solver.h" #include "theory/quantifiers/term_database.h" #include "options/theory_options.h" +#include "theory/uf/theory_uf_rewriter.h" using namespace std; @@ -47,13 +48,18 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, d_equalityEngine(d_notify, c, instanceName + "theory::uf::TheoryUF", true), d_conflict(c, false), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), + d_extensionality_deq(u), + d_uf_std_skolem(u), d_functionsTerms(c), d_symb(u, instanceName) { + d_true = NodeManager::currentNM()->mkConst( true ); + // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::APPLY_UF); + d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo()); + if( options::ufHo() ){ + d_equalityEngine.addFunctionKind(kind::HO_APPLY); + } } TheoryUF::~TheoryUF() { @@ -123,6 +129,11 @@ void TheoryUF::check(Effort level) { TNode atom = polarity ? fact : fact[0]; if (atom.getKind() == kind::EQUAL) { d_equalityEngine.assertEquality(atom, polarity, fact); + if( options::ufHo() && options::ufHoExt() ){ + if( !polarity && !d_conflict && atom[0].getType().isFunction() ){ + applyExtensionality( fact ); + } + } } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { if( d_thss == NULL ){ if( !getLogicInfo().hasCardinalityConstraints() ){ @@ -151,9 +162,71 @@ void TheoryUF::check(Effort level) { d_conflict = true; } } + if(! d_conflict && fullEffort(level) ){ + if( options::ufHo() ){ + checkHigherOrder(); + } + } } }/* TheoryUF::check() */ +Node TheoryUF::getApplyUfForHoApply( Node node ) { + Assert( node[0].getType().getNumChildren()==2 ); + std::vector< TNode > args; + Node f = TheoryUfRewriter::decomposeHoApply( node, args, true ); + Node new_f = f; + if( !TheoryUfRewriter::canUseAsApplyUfOperator( f ) ){ + NodeNodeMap::const_iterator itus = d_uf_std_skolem.find( f ); + if( itus==d_uf_std_skolem.end() ){ + // introduce skolem to make a standard APPLY_UF + new_f = NodeManager::currentNM()->mkSkolem( "app_uf", f.getType() ); + Node lem = new_f.eqNode( f ); + Trace("uf-ho-lemma") << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem << std::endl; + d_out->lemma( lem ); + d_uf_std_skolem[f] = new_f; + }else{ + new_f = (*itus).second; + } + } + Assert( TheoryUfRewriter::canUseAsApplyUfOperator( new_f ) ); + args[0] = new_f; + Node ret = NodeManager::currentNM()->mkNode( kind::APPLY_UF, args ); + return ret; +} + +Node TheoryUF::getOperatorForApplyTerm( TNode node ) { + Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY ); + if( node.getKind()==kind::APPLY_UF ){ + return node.getOperator(); + }else{ + return d_equalityEngine.getRepresentative( node[0] ); + } +} + +unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) { + Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY ); + return node.getKind()==kind::APPLY_UF ? 0 : 1; +} + +Node TheoryUF::expandDefinition(LogicRequest &logicRequest, Node node) { + Trace("uf-ho-debug") << "uf-ho-debug : expanding definition : " << node << std::endl; + if( node.getKind()==kind::HO_APPLY ){ + if( !options::ufHo() ){ + std::stringstream ss; + ss << "Partial function applications are not supported in default mode, try --uf-ho."; + throw LogicException(ss.str()); + } + // convert HO_APPLY to APPLY_UF if fully applied + if( node[0].getType().getNumChildren()==2 ){ + Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; + Node ret = getApplyUfForHoApply( node ); + Trace("uf-ho") << "uf-ho : expandDefinition : " << node << " to " << ret << std::endl; + return ret; + } + } + return node; +} + void TheoryUF::preRegisterTerm(TNode node) { Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl; @@ -161,12 +234,17 @@ void TheoryUF::preRegisterTerm(TNode node) { d_thss->preRegisterTerm(node); } + // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order + //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() ); + Assert( node.getKind()!=kind::HO_APPLY || options::ufHo() ); + switch (node.getKind()) { case kind::EQUAL: // Add the trigger for equality d_equalityEngine.addTriggerEquality(node); break; case kind::APPLY_UF: + case kind::HO_APPLY: // Maybe it's a predicate if (node.getType().isBoolean()) { // Get triggered for both equal and dis-equal @@ -251,33 +329,26 @@ Node TheoryUF::explain(TNode literal, eq::EqProof* pf) { } void TheoryUF::collectModelInfo( TheoryModel* m ){ + Debug("uf") << "UF : collectModelInfo " << std::endl; set termSet; // Compute terms appearing in assertions and shared terms computeRelevantTerms(termSet); m->assertEqualityEngine( &d_equalityEngine, &termSet ); - // if( fullModel ){ - // std::map< TypeNode, TypeEnumerator* > type_enums; - // //must choose proper representatives - // // for each equivalence class, specify fresh constant as representative - // eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - // while( !eqcs_i.isFinished() ){ - // Node eqc = (*eqcs_i); - // TypeNode tn = eqc.getType(); - // if( tn.isSort() ){ - // if( type_enums.find( tn )==type_enums.end() ){ - // type_enums[tn] = new TypeEnumerator( tn ); - // } - // Node rep = *(*type_enums[tn]); - // ++(*type_enums[tn]); - // //specify the constant as the representative - // m->assertEquality( eqc, rep, true ); - // m->assertRepresentative( rep ); - // } - // ++eqcs_i; - // } - // } + + if( options::ufHo() ){ + for( std::set::iterator it = termSet.begin(); it != termSet.end(); ++it ){ + Node n = *it; + if( n.getKind()==kind::APPLY_UF ){ + // for model-building with ufHo, we require that APPLY_UF is always expanded to HO_APPLY + Node hn = TheoryUfRewriter::getHoApplyForApplyUf( n ); + m->assertEquality( n, hn, true ); + } + } + } + + Debug("uf") << "UF : finish collectModelInfo " << std::endl; } void TheoryUF::presolve() { @@ -466,7 +537,8 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg if( !d_equalityEngine.areEqual( f1, f2 ) ){ Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; vector< pair > currentPairs; - for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { + unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 ); + for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) { TNode x = f1[k]; TNode y = f2[k]; Assert( d_equalityEngine.hasTerm(x) ); @@ -532,17 +604,18 @@ void TheoryUF::computeCareGraph() { unsigned functionTerms = d_functionsTerms.size(); for (unsigned i = 0; i < functionTerms; ++ i) { TNode f1 = d_functionsTerms[i]; - Node op = f1.getOperator(); + Node op = getOperatorForApplyTerm( f1 ); + unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 ); std::vector< TNode > reps; bool has_trigger_arg = false; - for( unsigned j=0; jfirst << "..." << std::endl; addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 ); } + Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." << std::endl; } }/* TheoryUF::computeCareGraph() */ @@ -586,6 +660,180 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } } +unsigned TheoryUF::applyExtensionality(TNode deq) { + Assert( deq.getKind()==kind::NOT && deq[0].getKind()==kind::EQUAL ); + Assert( deq[0][0].getType().isFunction() ); + // apply extensionality + if( d_extensionality_deq.find( deq )==d_extensionality_deq.end() ){ + d_extensionality_deq.insert( deq ); + TypeNode tn = deq[0][0].getType(); + std::vector< Node > skolems; + for( unsigned i=0; imkSkolem( "k", tn[i], "skolem created for extensionality." ); + skolems.push_back( k ); + } + Node t[2]; + for( unsigned i=0; i<2; i++ ){ + std::vector< Node > children; + Node curr = deq[0][i]; + while( curr.getKind()==kind::HO_APPLY ){ + children.push_back( curr[1] ); + curr = curr[0]; + } + children.push_back( curr ); + std::reverse( children.begin(), children.end() ); + children.insert( children.end(), skolems.begin(), skolems.end() ); + t[i] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, children ); + } + Node conc = t[0].eqNode( t[1] ).negate(); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq[0], conc ); + Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem << std::endl; + d_out->lemma( lem ); + return 1; + }else{ + return 0; + } +} + +unsigned TheoryUF::checkExtensionality() { + unsigned num_lemmas = 0; + Trace("uf-ho") << "TheoryUF::checkExtensionality..." << std::endl; + // This is bit eager: we should allow functions to be neither equal nor disequal during model construction + // However, doing so would require a function-type enumerator. + std::map< TypeNode, std::vector< Node > > func_eqcs; + + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + TypeNode tn = eqc.getType(); + if( tn.isFunction() ){ + func_eqcs[tn].push_back( eqc ); + Trace("uf-ho-debug") << " func eqc : " << tn << " : " << eqc << std::endl; + } + ++eqcs_i; + } + + for( std::map< TypeNode, std::vector< Node > >::iterator itf = func_eqcs.begin(); + itf != func_eqcs.end(); ++itf ){ + for( unsigned j=0; jsecond.size(); j++ ){ + for( unsigned k=(j+1); ksecond.size(); k++ ){ + // if these equivalence classes are not explicitly disequal, do extensionality to ensure distinctness + if( !d_equalityEngine.areDisequal( itf->second[j], itf->second[k], false ) ){ + Node deq = Rewriter::rewrite( itf->second[j].eqNode( itf->second[k] ).negate() ); + num_lemmas += applyExtensionality( deq ); + } + } + } + } + return num_lemmas; +} + +unsigned TheoryUF::applyAppCompletion( TNode n ) { + Assert( n.getKind()==kind::APPLY_UF ); + + //must expand into APPLY_HO version if not there already + Node ret = TheoryUfRewriter::getHoApplyForApplyUf( n ); + if( !d_equalityEngine.hasTerm( ret ) || !d_equalityEngine.areEqual( ret, n ) ){ + Node eq = ret.eqNode( n ); + Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq << std::endl; + d_equalityEngine.assertEquality(eq, true, d_true); + return 1; + }else{ + Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "." << std::endl; + return 0; + } +} + +unsigned TheoryUF::checkAppCompletion() { + Trace("uf-ho") << "TheoryUF::checkApplyCompletion..." << std::endl; + // compute the operators that are relevant (those for which an HO_APPLY exist) + std::set< TNode > rlvOp; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + std::map< TNode, std::vector< Node > > apply_uf; + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + Trace("uf-ho-debug") << " apply completion : visit eqc " << eqc << std::endl; + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + if( n.getKind()==kind::APPLY_UF || n.getKind()==kind::HO_APPLY ){ + int curr_sum = 0; + std::map< TNode, bool > curr_rops; + if( n.getKind()==kind::APPLY_UF ){ + TNode rop = d_equalityEngine.getRepresentative( n.getOperator() ); + if( rlvOp.find( rop )!=rlvOp.end() ){ + // try if its operator is relevant + curr_sum = applyAppCompletion( n ); + if( curr_sum>0 ){ + return curr_sum; + } + }else{ + // add to pending list + apply_uf[rop].push_back( n ); + } + //arguments are also relevant operators FIXME (github issue #1115) + for( unsigned k=0; k::iterator itc = curr_rops.begin(); itc != curr_rops.end(); ++itc ){ + TNode rop = itc->first; + if( rlvOp.find( rop )==rlvOp.end() ){ + rlvOp.insert( rop ); + // now, try each pending APPLY_UF for this operator + std::map< TNode, std::vector< Node > >::iterator itu = apply_uf.find( rop ); + if( itu!=apply_uf.end() ){ + for( unsigned j=0; jsecond.size(); j++ ){ + curr_sum = applyAppCompletion( itu->second[j] ); + if( curr_sum>0 ){ + return curr_sum; + } + } + } + } + } + } + ++eqc_i; + } + ++eqcs_i; + } + return 0; +} + +unsigned TheoryUF::checkHigherOrder() { + Trace("uf-ho") << "TheoryUF::checkHigherOrder..." << std::endl; + + // infer new facts based on apply completion until fixed point + unsigned num_facts; + do{ + num_facts = checkAppCompletion(); + if( d_conflict ){ + Trace("uf-ho") << "...conflict during app-completion." << std::endl; + return 1; + } + }while( num_facts>0 ); + + if( options::ufHoExt() ){ + unsigned num_lemmas = 0; + + num_lemmas = checkExtensionality(); + if( num_lemmas>0 ){ + Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas." << std::endl; + return num_lemmas; + } + } + + Trace("uf-ho") << "...finished check higher order." << std::endl; + + return 0; +} } /* namespace CVC4::theory::uf */ } /* namespace CVC4::theory */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index bd10f5961..0665b8272 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -30,6 +30,7 @@ #include "context/cdo.h" #include "context/cdhashset.h" + namespace CVC4 { namespace theory { @@ -45,7 +46,8 @@ class StrongSolverTheoryUF; class TheoryUF : public Theory { friend class StrongSolverTheoryUF; - + typedef context::CDHashSet NodeSet; + typedef context::CDHashMap NodeNodeMap; public: class NotifyClass : public eq::EqualityEngineNotify { @@ -125,6 +127,15 @@ private: /** The conflict node */ Node d_conflictNode; + /** extensionality has been applied to these disequalities */ + NodeSet d_extensionality_deq; + + /** map from non-standard operators to their skolems */ + NodeNodeMap d_uf_std_skolem; + + /** node for true */ + Node d_true; + /** * Should be called to propagate the literal. We use a node here * since some of the propagated literals are not kept anywhere. @@ -142,12 +153,6 @@ private: */ Node explain(TNode literal, eq::EqProof* pf); - /** Literals to propagate */ - context::CDList d_literalsToPropagate; - - /** Index of the next literal to propagate */ - context::CDO d_literalsToPropagateIndex; - /** All the function terms that the theory has seen */ context::CDList d_functionsTerms; @@ -169,6 +174,57 @@ private: /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); +private: // for higher-order + /** applyExtensionality + * Given disequality deq + * If not already cached, this sends a lemma of the form + * f = g V (f k) != (g k) for fresh constant k. + * on the output channel. + * Return value is the number of lemmas sent. + */ + unsigned applyExtensionality(TNode deq); + + /** check whether extensionality should be applied for any + * pair of terms in the equality engine. + */ + unsigned checkExtensionality(); + + /** applyAppCompletion + * This infers a correspondence between APPLY_UF and HO_APPLY + * versions of terms for higher-order. + * Given APPLY_UF node e.g. (f a b c), this adds the equality to its + * HO_APPLY equivalent: + * (f a b c) == (@ (@ (@ f a) b) c) + * to equality engine, if not already equal. + * Return value is the number of equalities added. + */ + unsigned applyAppCompletion( TNode n ); + + /** check whether app-completion should be applied for any + * pair of terms in the equality engine. + */ + unsigned checkAppCompletion(); + + /** check higher order + * This is called at full effort and infers facts and sends lemmas + * based on higher-order reasoning (specifically, extentionality and + * app completion above). It returns the number of lemmas plus facts + * added to the equality engine. + */ + unsigned checkHigherOrder(); + + /** get apply uf for ho apply + * This returns the APPLY_UF equivalent for the HO_APPLY term node, where + * node has non-functional return type (that is, it corresponds to a fully + * applied function term). + * This call may introduce a skolem for the head operator and send out a lemma + * specifying the definition. + */ + Node getApplyUfForHoApply( Node node ); + /** get the operator for this node (node should be either APPLY_UF or HO_APPLY) */ + Node getOperatorForApplyTerm( TNode node ); + /** get the starting index of the arguments for node (node should be either APPLY_UF or HO_APPLY) */ + unsigned getArgumentStartIndexForApplyTerm( TNode node ); public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ @@ -181,7 +237,8 @@ public: void setMasterEqualityEngine(eq::EqualityEngine* eq); void finishInit(); - void check(Effort); + void check(Effort); + Node expandDefinition(LogicRequest &logicRequest, Node node); void preRegisterTerm(TNode term); Node explain(TNode n);