summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/ematching/ho_trigger.cpp84
-rw-r--r--src/theory/quantifiers/term_database.cpp28
-rw-r--r--test/regress/Makefile.tests1
-rw-r--r--test/regress/regress0/ho/ho-match-fun-suffix.smt213
4 files changed, 96 insertions, 30 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 0e0955119..fad6334b8 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -236,7 +236,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
{
TNode var = ha.first;
unsigned vnum = var.getAttribute(InstVarNumAttribute());
- Node value = m.d_vals[vnum];
+ TNode value = m.d_vals[vnum];
Trace("ho-unif-debug") << " val[" << var << "] = " << value << std::endl;
Trace("ho-unif-debug2") << "initialize lambda information..."
@@ -256,7 +256,17 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
for (unsigned i = 0; i < ha.second.size(); i++)
{
std::vector<TNode> args;
- Node f = uf::TheoryUfRewriter::decomposeHoApply(ha.second[i], args);
+ // must substitute the operator we matched with the original
+ // higher-order variable (var) that matched it. This ensures that the
+ // argument vector (args) below is of the proper length. This handles,
+ // for example, matches like:
+ // (@ x y) with (@ (@ k1 k2) k3)
+ // where k3 but not k2 should be an argument of the match.
+ Node hmatch = ha.second[i];
+ Trace("ho-unif-debug2") << "Match is " << hmatch << std::endl;
+ hmatch = hmatch.substitute(value, var);
+ Trace("ho-unif-debug2") << "Pre-subs match is " << hmatch << std::endl;
+ Node f = uf::TheoryUfRewriter::decomposeHoApply(hmatch, args);
// Assert( f==value );
for (unsigned k = 0, size = args.size(); k < size; k++)
{
@@ -348,7 +358,9 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
Trace("ho-unif-debug2") << "finished." << std::endl;
}
- return sendInstantiation(m, 0);
+ bool ret = sendInstantiation(m, 0);
+ Trace("ho-unif-debug") << "Finished, success = " << ret << std::endl;
+ return ret;
}
else
{
@@ -361,6 +373,8 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
// occurring as pattern operators (very small)
bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index)
{
+ Trace("ho-unif-debug2") << "send inst " << var_index << " / "
+ << d_ho_var_list.size() << std::endl;
if (var_index == d_ho_var_list.size())
{
// we now have an instantiation to try
@@ -394,13 +408,18 @@ bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m,
Node lbvl,
bool arg_changed)
{
+ Trace("ho-unif-debug2") << "send inst arg " << arg_index << " / "
+ << lbvl.getNumChildren() << std::endl;
if (arg_index == lbvl.getNumChildren())
{
// construct the lambda
if (arg_changed)
{
+ Trace("ho-unif-debug2")
+ << " make lambda from children: " << d_lchildren[vnum] << std::endl;
Node body =
NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_lchildren[vnum]);
+ Trace("ho-unif-debug2") << " got " << body << std::endl;
Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, lbvl, body);
m.d_vals[vnum] = lam;
Trace("ho-unif-debug2") << " try " << vnum << " -> " << lam << std::endl;
@@ -438,35 +457,58 @@ bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m,
int HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
{
+ if (d_ho_var_types.empty())
+ {
+ return 0;
+ }
+ Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
unsigned numLemmas = 0;
- if (!d_ho_var_types.empty())
+ // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
+ unsigned size = d_quantEngine->getTermDatabase()->getNumOperators();
+ quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil();
+ NodeManager* nm = NodeManager::currentNM();
+ for (unsigned j = 0; j < size; j++)
{
- // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
- unsigned size = d_quantEngine->getTermDatabase()->getNumOperators();
- for (unsigned j = 0; j < size; j++)
+ Node f = d_quantEngine->getTermDatabase()->getOperator(j);
+ if (f.isVar())
{
- Node f = d_quantEngine->getTermDatabase()->getOperator(j);
- if (f.isVar())
+ TypeNode tn = f.getType();
+ if (tn.isFunction())
{
- TypeNode tn = f.getType();
- if (d_ho_var_types.find(tn) != d_ho_var_types.end())
+ std::vector<TypeNode> argTypes = tn.getArgTypes();
+ Assert(argTypes.size() > 0);
+ TypeNode range = tn.getRangeType();
+ // for each function type suffix of the type of f, for example if
+ // f : (Int -> (Int -> Int))
+ // we iterate with stn = (Int -> (Int -> Int)) and (Int -> Int)
+ for (unsigned a = 0, size = argTypes.size(); a < size; a++)
{
- Node u = d_quantEngine->getTermUtil()->getHoTypeMatchPredicate(tn);
- Node au = NodeManager::currentNM()->mkNode(kind::APPLY_UF, u, f);
- if (d_quantEngine->addLemma(au))
+ std::vector<TypeNode> sargts;
+ sargts.insert(sargts.begin(), argTypes.begin() + a, argTypes.end());
+ Assert(sargts.size() > 0);
+ TypeNode stn = nm->mkFunctionType(sargts, range);
+ Trace("ho-quant-trigger-debug")
+ << "For " << f << ", check " << stn << "..." << std::endl;
+ // if a variable of this type occurs in this trigger
+ if (d_ho_var_types.find(stn) != d_ho_var_types.end())
{
- // this forces f to be a first-class member of the quantifier-free
- // equality engine,
- // which in turn forces the quantifier-free theory solver to expand
- // it to HO_APPLY
- Trace("ho-quant") << "Added ho match predicate lemma : " << au
- << std::endl;
- numLemmas++;
+ Node u = tutil->getHoTypeMatchPredicate(tn);
+ Node au = nm->mkNode(kind::APPLY_UF, u, f);
+ if (d_quantEngine->addLemma(au))
+ {
+ // this forces f to be a first-class member of the quantifier-free
+ // equality engine, which in turn forces the quantifier-free
+ // theory solver to expand it to an HO_APPLY chain.
+ Trace("ho-quant")
+ << "Added ho match predicate lemma : " << au << std::endl;
+ numLemmas++;
+ }
}
}
}
}
}
+
return numLemmas;
}
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 8e22b2ced..2013bff5d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -308,6 +308,7 @@ void TermDb::computeUfTerms( TNode f ) {
if( options::ufHo() ){
ops.insert( ops.end(), d_ho_op_rep_slaves[f].begin(), d_ho_op_rep_slaves[f].end() );
}
+ Trace("term-db-debug") << "computeUfTerms for " << f << std::endl;
unsigned congruentCount = 0;
unsigned nonCongruentCount = 0;
unsigned alreadyCongruentCount = 0;
@@ -318,7 +319,8 @@ void TermDb::computeUfTerms( TNode f ) {
//Assert( !options::ufHo() || ee->areEqual( ff, f ) );
std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( ff );
if( it!=d_op_map.end() ){
- Trace("term-db-debug") << "Adding terms for operator " << f << std::endl;
+ Trace("term-db-debug")
+ << "Adding terms for operator " << ff << std::endl;
for( unsigned i=0; i<it->second.size(); i++ ){
Node n = it->second[i];
//to be added to term index, term must be relevant, and exist in EE
@@ -856,14 +858,22 @@ bool TermDb::reset( Theory::Effort effort ){
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
while( !eqc_i.isFinished() ){
TNode n = (*eqc_i);
- if( d_op_map.find( n )!=d_op_map.end() ){
- if( first.isNull() ){
- first = n;
- d_ho_op_rep[n] = n;
- }else{
- Trace("quant-ho") << " have : " << n << " == " << first << ", type = " << n.getType() << std::endl;
- d_ho_op_rep[n] = first;
- d_ho_op_rep_slaves[first].push_back( n );
+ if (n.isVar())
+ {
+ if (d_op_map.find(n) != d_op_map.end())
+ {
+ if (first.isNull())
+ {
+ first = n;
+ d_ho_op_rep[n] = n;
+ }
+ else
+ {
+ Trace("quant-ho") << " have : " << n << " == " << first
+ << ", type = " << n.getType() << std::endl;
+ d_ho_op_rep[n] = first;
+ d_ho_op_rep_slaves[first].push_back(n);
+ }
}
}
++eqc_i;
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 4fb9065c6..de80368a4 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/ho-match-fun-suffix.smt2 \
regress0/ho/ho-matching-enum.smt2 \
regress0/ho/ho-matching-nested-app.smt2 \
regress0/ho/ite-apply-eq.smt2 \
diff --git a/test/regress/regress0/ho/ho-match-fun-suffix.smt2 b/test/regress/regress0/ho/ho-match-fun-suffix.smt2
new file mode 100644
index 000000000..1e4ad243c
--- /dev/null
+++ b/test/regress/regress0/ho/ho-match-fun-suffix.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun f (Int Int) Int)
+(declare-fun a () Int)
+(declare-fun b () Int)
+
+(assert (forall ((x (-> Int Int)) (y Int)) (not (= (x y) 0))))
+
+(assert (= (f a b) 0))
+
+(check-sat) \ No newline at end of file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback