#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;
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() {
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() ){
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;
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
}
void TheoryUF::collectModelInfo( TheoryModel* m ){
+ Debug("uf") << "UF : collectModelInfo " << std::endl;
set<Node> 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<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 );
+ m->assertEquality( n, hn, true );
+ }
+ }
+ }
+
+ Debug("uf") << "UF : finish collectModelInfo " << std::endl;
}
void TheoryUF::presolve() {
if( !d_equalityEngine.areEqual( f1, f2 ) ){
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
vector< pair<TNode, TNode> > 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) );
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; j<f1.getNumChildren(); j++ ){
+ for( unsigned j=arg_start_index; j<f1.getNumChildren(); j++ ){
reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_UF ) ){
has_trigger_arg = true;
}
}
if( has_trigger_arg ){
- index[op].addTerm( f1, reps );
+ index[op].addTerm( f1, reps, arg_start_index );
arity[op] = reps.size();
}
}
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << itii->first << "..." << std::endl;
addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 );
}
+ Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." << std::endl;
}
}/* TheoryUF::computeCareGraph() */
}
}
+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; i<tn.getNumChildren()-1; i++ ){
+ Node k = NodeManager::currentNM()->mkSkolem( "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; 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 ) ){
+ 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<n.getNumChildren(); k++ ){
+ if( n[k].getType().isFunction() ){
+ TNode rop = d_equalityEngine.getRepresentative( n[k] );
+ curr_rops[rop] = true;
+ }
+ }
+ }else{
+ Assert( n.getKind()==kind::HO_APPLY );
+ TNode rop = d_equalityEngine.getRepresentative( n[0] );
+ curr_rops[rop] = true;
+ }
+ for( std::map< TNode, bool >::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; j<itu->second.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 */
#include "context/cdo.h"
#include "context/cdhashset.h"
+
namespace CVC4 {
namespace theory {
class TheoryUF : public Theory {
friend class StrongSolverTheoryUF;
-
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
public:
class NotifyClass : public eq::EqualityEngineNotify {
/** 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.
*/
Node explain(TNode literal, eq::EqProof* pf);
- /** Literals to propagate */
- context::CDList<Node> d_literalsToPropagate;
-
- /** Index of the next literal to propagate */
- context::CDO<unsigned> d_literalsToPropagateIndex;
-
/** All the function terms that the theory has seen */
context::CDList<TNode> d_functionsTerms;
/** 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.*/
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);
projects / cvc5.git / commitdiff