summaryrefslogtreecommitdiff
path: root/src/theory/uf/theory_uf.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r--src/theory/uf/theory_uf.cpp354
1 files changed, 19 insertions, 335 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 508bd5002..393d9f640 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -29,6 +29,7 @@
#include "proof/uf_proof.h"
#include "theory/theory_model.h"
#include "theory/type_enumerator.h"
+#include "theory/uf/ho_extension.h"
#include "theory/uf/theory_uf_rewriter.h"
#include "theory/uf/theory_uf_strong_solver.h"
@@ -52,8 +53,6 @@ TheoryUF::TheoryUF(context::Context* c,
d_thss(NULL),
d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true),
d_conflict(c, false),
- d_extensionality(u),
- d_uf_std_skolem(u),
d_functionsTerms(c),
d_symb(u, instanceName)
{
@@ -61,9 +60,6 @@ TheoryUF::TheoryUF(context::Context* c,
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo());
- if( options::ufHo() ){
- d_equalityEngine.addFunctionKind(kind::HO_APPLY);
- }
}
TheoryUF::~TheoryUF() {
@@ -87,6 +83,11 @@ void TheoryUF::finishInit() {
{
d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this);
}
+ if (options::ufHo())
+ {
+ d_equalityEngine.addFunctionKind(kind::HO_APPLY);
+ d_ho = new HoExtension(*this, getSatContext(), getUserContext());
+ }
}
static Node mkAnd(const std::vector<TNode>& conjunctions) {
@@ -143,7 +144,8 @@ void TheoryUF::check(Effort level) {
d_equalityEngine.assertEquality(atom, polarity, fact);
if( options::ufHo() && options::ufHoExt() ){
if( !polarity && !d_conflict && atom[0].getType().isFunction() ){
- applyExtensionality( fact );
+ // apply extensionality eagerly using the ho extension
+ d_ho->applyExtensionality(fact);
}
}
} else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) {
@@ -168,89 +170,22 @@ void TheoryUF::check(Effort level) {
}
if(! d_conflict ){
+ // check with the cardinality constraints extension
if (d_thss != NULL) {
d_thss->check(level);
if( d_thss->isConflict() ){
d_conflict = true;
}
}
+ // check with the higher-order extension
if(! d_conflict && fullEffort(level) ){
if( options::ufHo() ){
- checkHigherOrder();
+ d_ho->check();
}
}
}
}/* 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;
- NodeManager* nm = NodeManager::currentNM();
- if( !TheoryUfRewriter::canUseAsApplyUfOperator( f ) ){
- NodeNodeMap::const_iterator itus = d_uf_std_skolem.find( f );
- if( itus==d_uf_std_skolem.end() ){
- std::unordered_set<Node, NodeHashFunction> fvs;
- expr::getFreeVariables(f, fvs);
- Node lem;
- if (!fvs.empty())
- {
- std::vector<TypeNode> newTypes;
- std::vector<Node> vs;
- std::vector<Node> nvs;
- for (const Node& v : fvs)
- {
- TypeNode vt = v.getType();
- newTypes.push_back(vt);
- Node nv = nm->mkBoundVar(vt);
- vs.push_back(v);
- nvs.push_back(nv);
- }
- TypeNode ft = f.getType();
- std::vector<TypeNode> argTypes = ft.getArgTypes();
- TypeNode rangeType = ft.getRangeType();
-
- newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end());
- TypeNode nft = nm->mkFunctionType(newTypes, rangeType);
- new_f = nm->mkSkolem("app_uf", nft);
- for (const Node& v : vs)
- {
- new_f = nm->mkNode(kind::HO_APPLY, new_f, v);
- }
- Assert(new_f.getType() == f.getType());
- Node eq = new_f.eqNode(f);
- Node seq = eq.substitute(vs.begin(), vs.end(), nvs.begin(), nvs.end());
- lem = nm->mkNode(
- kind::FORALL, nm->mkNode(kind::BOUND_VAR_LIST, nvs), seq);
- }
- else
- {
- // introduce skolem to make a standard APPLY_UF
- new_f = nm->mkSkolem("app_uf", f.getType());
- 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;
- }
- // unroll the HO_APPLY, adding to the first argument position
- // Note arguments in the vector args begin at position 1.
- while (new_f.getKind() == kind::HO_APPLY)
- {
- args.insert(args.begin() + 1, new_f[1]);
- new_f = new_f[0];
- }
- }
- Assert( TheoryUfRewriter::canUseAsApplyUfOperator( new_f ) );
- args[0] = new_f;
- Node ret = nm->mkNode(kind::APPLY_UF, args);
- Assert(ret.getType() == node.getType());
- return ret;
-}
-
Node TheoryUF::getOperatorForApplyTerm( TNode node ) {
Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY );
if( node.getKind()==kind::APPLY_UF ){
@@ -266,18 +201,19 @@ unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) {
}
Node TheoryUF::expandDefinition(LogicRequest &logicRequest, Node node) {
- Trace("uf-ho-debug") << "uf-ho-debug : expanding definition : " << node << std::endl;
+ Trace("uf-exp-def") << "TheoryUF::expandDefinition: 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;
+ Node ret = d_ho->expandDefinition(node);
+ if (ret != node)
+ {
+ Trace("uf-exp-def") << "TheoryUF::expandDefinition: higher-order: "
+ << node << " to " << ret << std::endl;
return ret;
}
}
@@ -391,18 +327,9 @@ bool TheoryUF::collectModelInfo(TheoryModel* m)
}
if( options::ufHo() ){
- for( std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it ){
- Node n = *it;
- // 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)
+ if (!d_ho->collectModelInfoHo(termSet, m))
{
return false;
}
@@ -412,19 +339,6 @@ bool TheoryUF::collectModelInfo(TheoryModel* m)
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);
@@ -749,236 +663,6 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
}
}
-Node TheoryUF::getExtensionalityDeq(TNode deq)
-{
- Assert( deq.getKind()==kind::NOT && deq[0].getKind()==kind::EQUAL );
- Assert( deq[0][0].getType().isFunction() );
- 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;
- 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++)
- {
- 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] = 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;
- }
- return 0;
-}
-
-unsigned TheoryUF::checkExtensionality(TheoryModel* m)
-{
- unsigned num_lemmas = 0;
- 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() ){
- // 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( 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() );
- // 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);
- }
- }
- }
- }
- }
- 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 */
} /* namespace CVC4 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback