From e5d09628376cc101cbd3646dd64041170dacb402 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 10 Apr 2018 20:24:34 -0500 Subject: [PATCH] Properly implement function extensionality based on cardinality (#1765) --- src/expr/type_node.cpp | 16 +++ src/theory/uf/theory_uf.cpp | 135 ++++++++++++++----- src/theory/uf/theory_uf.h | 81 ++++++++--- test/regress/Makefile.tests | 1 + test/regress/regress0/ho/finite-fun-ext.smt2 | 14 ++ 5 files changed, 196 insertions(+), 51 deletions(-) create mode 100644 test/regress/regress0/ho/finite-fun-ext.smt2 diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 9e61e713b..e7775cf7f 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -82,6 +82,22 @@ bool TypeNode::isInterpretedFinite() const { }else if( isSet() ) { return getSetElementType().isInterpretedFinite(); } + else if (isFunction()) + { + if (!getRangeType().isInterpretedFinite()) + { + return false; + } + std::vector argTypes = getArgTypes(); + for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) + { + if (!argTypes[i].isInterpretedFinite()) + { + return false; + } + } + return true; + } } return false; } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index b3fb8e211..f5748549e 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -39,9 +39,12 @@ namespace theory { namespace uf { /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ -TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, std::string instanceName) +TheoryUF::TheoryUF(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + std::string instanceName) : Theory(THEORY_UF, c, u, out, valuation, logicInfo, instanceName), d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), @@ -49,7 +52,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, d_thss(NULL), d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true), d_conflict(c, false), - d_extensionality_deq(u), + d_extensionality(u), d_uf_std_skolem(u), d_functionsTerms(c), d_symb(u, instanceName) @@ -345,21 +348,38 @@ bool TheoryUF::collectModelInfo(TheoryModel* m) 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 ); - if (!m->assertEquality(n, hn, true)) - { - return false; - } + // for model-building with ufHo, we require that APPLY_UF is always + // expanded to HO_APPLY + if (!collectModelInfoHoTerm(n, m)) + { + return false; } } + // must add extensionality disequalities for all pairs of (non-disequal) + // function equivalence classes. + if (checkExtensionality(m) != 0) + { + return false; + } } Debug("uf") << "UF : finish collectModelInfo " << std::endl; return true; } +bool TheoryUF::collectModelInfoHoTerm(Node n, TheoryModel* m) +{ + if (n.getKind() == kind::APPLY_UF) + { + Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n); + if (!m->assertEquality(n, hn, true)) + { + return false; + } + } + return true; +} + void TheoryUF::presolve() { // TimerStat::CodeTimer codeTimer(d_presolveTimer); @@ -670,20 +690,26 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } } -unsigned TheoryUF::applyExtensionality(TNode deq) { +Node TheoryUF::getExtensionalityDeq(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 ); + std::map::iterator it = d_extensionality_deq.find(deq); + if (it == d_extensionality_deq.end()) + { TypeNode tn = deq[0][0].getType(); + std::vector argTypes = tn.getArgTypes(); std::vector< Node > skolems; - for( unsigned i=0; imkSkolem( "k", tn[i], "skolem created for extensionality." ); + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) + { + Node k = + nm->mkSkolem("k", argTypes[i], "skolem created for extensionality."); skolems.push_back( k ); } Node t[2]; - for( unsigned i=0; i<2; i++ ){ + for (unsigned i = 0; i < 2; i++) + { std::vector< Node > children; Node curr = deq[0][i]; while( curr.getKind()==kind::HO_APPLY ){ @@ -693,32 +719,52 @@ unsigned TheoryUF::applyExtensionality(TNode deq) { 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 ); + t[i] = nm->mkNode(kind::APPLY_UF, children); } Node conc = t[0].eqNode( t[1] ).negate(); + d_extensionality_deq[deq] = conc; + return conc; + } + return it->second; +} + +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.find(deq) == d_extensionality.end()) + { + d_extensionality.insert(deq); + Node conc = getExtensionalityDeq(deq); 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; } + return 0; } -unsigned TheoryUF::checkExtensionality() { +unsigned TheoryUF::checkExtensionality(TheoryModel* m) +{ 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. + bool isCollectModel = (m != nullptr); + Trace("uf-ho") << "TheoryUF::checkExtensionality, collectModel=" + << isCollectModel << "..." << std::endl; 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; + // if during collect model, must have an infinite type + // if not during collect model, must have a finite type + if (tn.isInterpretedFinite() != isCollectModel) + { + func_eqcs[tn].push_back(eqc); + Trace("uf-ho-debug") + << " func eqc : " << tn << " : " << eqc << std::endl; + } } ++eqcs_i; } @@ -728,9 +774,38 @@ unsigned TheoryUF::checkExtensionality() { 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 ) ){ + 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 ); + // either add to model, or add lemma + if (isCollectModel) + { + // add extentionality disequality to the model + Node edeq = getExtensionalityDeq(deq); + Assert(edeq.getKind() == kind::NOT + && edeq[0].getKind() == kind::EQUAL); + // introducing terms, must add required constraints, e.g. to + // force equalities between APPLY_UF and HO_APPLY terms + for (unsigned r = 0; r < 2; r++) + { + if (!collectModelInfoHoTerm(edeq[0][r], m)) + { + return 1; + } + } + Trace("uf-ho-debug") + << "Add extensionality deq to model : " << edeq << std::endl; + if (!m->assertEquality(edeq[0][0], edeq[0][1], false)) + { + return 1; + } + } + else + { + // apply extensionality lemma + num_lemmas += applyExtensionality(deq); + } } } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index bac03c34c..790968360 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -139,7 +139,10 @@ private: Node d_conflictNode; /** extensionality has been applied to these disequalities */ - NodeSet d_extensionality_deq; + NodeSet d_extensionality; + + /** cache of getExtensionalityDeq below */ + std::map d_extensionality_deq; /** map from non-standard operators to their skolems */ NodeNodeMap d_uf_std_skolem; @@ -185,31 +188,55 @@ 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 + private: // for higher-order + /** get extensionality disequality + * + * Given disequality deq f != g, this returns the disequality: + * (f k) != (g k) for fresh constant(s) k. + */ + Node getExtensionalityDeq(TNode deq); + + /** applyExtensionality + * + * Given disequality deq f != g, 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. + * on the output channel. This is an "extensionality lemma". + * Return value is the number of lemmas of this form sent on the output + * channel. */ unsigned applyExtensionality(TNode deq); - /** check whether extensionality should be applied for any - * pair of terms in the equality engine. + /** + * Check whether extensionality should be applied for any pair of terms in the + * equality engine. + * + * If we pass a null model m to this function, then we add extensionality + * lemmas to the output channel and return the total number of lemmas added. + * We only add lemmas for functions whose type is finite, since pairs of + * functions whose types are infinite can be made disequal in a model by + * witnessing a point they are disequal. + * + * If we pass a non-null model m to this function, then we add disequalities + * that correspond to the conclusion of extensionality lemmas to the model's + * equality engine. We return 0 if the equality engine of m is consistent + * after this call, and 1 otherwise. We only add disequalities for functions + * whose type is infinite, since our decision procedure guarantees that + * extensionality lemmas are added for all pairs of functions whose types are + * finite. */ - unsigned checkExtensionality(); - + unsigned checkExtensionality(TheoryModel* m = nullptr); + /** applyAppCompletion - * This infers a correspondence between APPLY_UF and HO_APPLY + * 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 + * 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 ); + unsigned applyAppCompletion(TNode n); /** check whether app-completion should be applied for any * pair of terms in the equality engine. @@ -224,19 +251,31 @@ private: // for higher-order */ unsigned checkHigherOrder(); - /** get apply uf for ho apply + /** collect model info for higher-order term + * + * This adds required constraints to m for term n. In particular, if n is + * an APPLY_UF term, we add its HO_APPLY equivalent in this call. We return + * true if the model m is consistent after this call. + */ + bool collectModelInfoHoTerm(Node n, TheoryModel* m); + + /** 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: + 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.*/ TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 46d856156..3899ff367 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -443,6 +443,7 @@ REG0_TESTS = \ regress0/ho/ext-ho.smt2 \ regress0/ho/ext-sat-partial-eval.smt2 \ regress0/ho/ext-sat.smt2 \ + regress0/ho/finite-fun-ext.smt2 \ regress0/ho/ho-match-fun-suffix.smt2 \ regress0/ho/ho-matching-enum.smt2 \ regress0/ho/ho-matching-nested-app.smt2 \ diff --git a/test/regress/regress0/ho/finite-fun-ext.smt2 b/test/regress/regress0/ho/finite-fun-ext.smt2 new file mode 100644 index 000000000..005a2109a --- /dev/null +++ b/test/regress/regress0/ho/finite-fun-ext.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic ALL) + +(declare-datatype Unit ((unit))) + +(declare-fun f (Int) Unit) +(declare-fun g (Int) Unit) +(declare-fun P ((-> Int Unit)) Bool) + +(assert (P f)) +(assert (not (P g))) + +(check-sat) -- 2.30.2