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(),
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)
if( options::ufHo() ){
for( std::set<Node>::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);
}
}
-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<Node, Node>::iterator it = d_extensionality_deq.find(deq);
+ if (it == d_extensionality_deq.end())
+ {
TypeNode tn = deq[0][0].getType();
+ std::vector<TypeNode> argTypes = tn.getArgTypes();
std::vector< Node > skolems;
- for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
- Node k = NodeManager::currentNM()->mkSkolem( "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 ){
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;
}
for( unsigned j=0; j<itf->second.size(); j++ ){
for( unsigned k=(j+1); k<itf->second.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);
+ }
}
}
}
Node d_conflictNode;
/** extensionality has been applied to these disequalities */
- NodeSet d_extensionality_deq;
+ NodeSet d_extensionality;
+
+ /** cache of getExtensionalityDeq below */
+ std::map<Node, Node> d_extensionality_deq;
/** map from non-standard operators to their skolems */
NodeNodeMap d_uf_std_skolem;
/** 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.
*/
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,
projects / cvc5.git / commitdiff