summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/datatypes/theory_datatypes_utils.cpp37
-rw-r--r--src/theory/datatypes/theory_datatypes_utils.h6
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_red.cpp6
-rw-r--r--src/theory/quantifiers/sygus/term_database_sygus.cpp21
-rw-r--r--src/theory/quantifiers/sygus/term_database_sygus.h12
-rw-r--r--src/theory/quantifiers/sygus/type_info.cpp2
6 files changed, 63 insertions, 21 deletions
diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index c3b145b15..bb62ab8ae 100644
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -116,7 +116,8 @@ Kind getOperatorKindForSygusBuiltin(Node op)
Node mkSygusTerm(const Datatype& dt,
unsigned i,
- const std::vector<Node>& children)
+ const std::vector<Node>& children,
+ bool doBetaReduction)
{
Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i
<< "] with children: " << children << std::endl;
@@ -138,26 +139,44 @@ Node mkSygusTerm(const Datatype& dt,
Assert(children.size() == 1);
return children[0];
}
- if (op.getKind() != BUILTIN)
+ // get the kind of the operator
+ Kind ok = op.getKind();
+ if (ok != BUILTIN)
{
- schildren.push_back(op);
+ if (ok == LAMBDA && doBetaReduction)
+ {
+ // Do immediate beta reduction. It suffices to use a normal substitution
+ // since neither op nor children have quantifiers, since they are
+ // generated by sygus grammars.
+ std::vector<Node> vars{op[0].begin(), op[0].end()};
+ Assert(vars.size() == children.size());
+ Node ret = op[1].substitute(
+ vars.begin(), vars.end(), children.begin(), children.end());
+ Trace("dt-sygus-util") << "...return (beta-reduce) " << ret << std::endl;
+ return ret;
+ }
+ else
+ {
+ schildren.push_back(op);
+ }
}
schildren.insert(schildren.end(), children.begin(), children.end());
Node ret;
- if (op.getKind() == BUILTIN)
+ if (ok == BUILTIN)
{
ret = NodeManager::currentNM()->mkNode(op, schildren);
Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl;
return ret;
}
- Kind ok = NodeManager::operatorToKind(op);
- Trace("dt-sygus-util") << "operator kind is " << ok << std::endl;
- if (ok != UNDEFINED_KIND)
+ // get the kind used for applying op
+ Kind otk = NodeManager::operatorToKind(op);
+ Trace("dt-sygus-util") << "operator kind is " << otk << std::endl;
+ if (otk != UNDEFINED_KIND)
{
// If it is an APPLY_UF operator, we should have at least an operator and
// a child.
- Assert(ok != APPLY_UF || schildren.size() != 1);
- ret = NodeManager::currentNM()->mkNode(ok, schildren);
+ Assert(otk != APPLY_UF || schildren.size() != 1);
+ ret = NodeManager::currentNM()->mkNode(otk, schildren);
Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
return ret;
}
diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h
index ba0643567..92783c2f7 100644
--- a/src/theory/datatypes/theory_datatypes_utils.h
+++ b/src/theory/datatypes/theory_datatypes_utils.h
@@ -146,11 +146,13 @@ Kind getOperatorKindForSygusBuiltin(Node op);
*
* This function returns a builtin term f( children[0], ..., children[n] )
* where f is the builtin op that the i^th constructor of sygus datatype dt
- * encodes.
+ * encodes. If doBetaReduction is true, then lambdas are eagerly eliminated
+ * via beta reduction.
*/
Node mkSygusTerm(const Datatype& dt,
unsigned i,
- const std::vector<Node>& children);
+ const std::vector<Node>& children,
+ bool doBetaReduction = true);
/**
* n is a builtin term that is an application of operator op.
*
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index a566ebfff..6bf8c56fb 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -42,7 +42,9 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
Trace("sygus-red") << " Is " << dt[i].getName() << " a redundant operator?"
<< std::endl;
std::map<int, Node> pre;
- Node g = tds->mkGeneric(dt, i, pre);
+ // We do not do beta reduction, since we want the arguments to match the
+ // the types of the datatype.
+ Node g = tds->mkGeneric(dt, i, pre, false);
Trace("sygus-red-debug") << " ...pre-rewrite : " << g << std::endl;
d_gen_terms[i] = g;
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
@@ -73,6 +75,8 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
}
d_sygus_red_status.push_back(red ? 1 : 0);
}
+ Trace("sygus-red") << "Compute redundant cons for " << tn << " finished"
+ << std::endl;
}
void SygusRedundantCons::getRedundant(std::vector<unsigned>& indices)
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 7fb54f14e..d4ee11453 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -162,7 +162,8 @@ TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
Node TermDbSygus::mkGeneric(const Datatype& dt,
unsigned c,
std::map<TypeNode, int>& var_count,
- std::map<int, Node>& pre)
+ std::map<int, Node>& pre,
+ bool doBetaRed)
{
Assert(c < dt.getNumConstructors());
Assert(dt.isSygus());
@@ -176,6 +177,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
std::map< int, Node >::iterator it = pre.find( i );
if( it!=pre.end() ){
a = it->second;
+ Trace("sygus-db-debug") << "From pre: " << a << std::endl;
}else{
TypeNode tna = TypeNode::fromType(dt[c].getArgType(i));
a = getFreeVarInc( tna, var_count, true );
@@ -185,19 +187,24 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
Assert(!a.isNull());
children.push_back( a );
}
- return datatypes::utils::mkSygusTerm(dt, c, children);
+ Node ret = datatypes::utils::mkSygusTerm(dt, c, children, doBetaRed);
+ Trace("sygus-db-debug") << "mkGeneric returns " << ret << std::endl;
+ return ret;
}
-Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre)
+Node TermDbSygus::mkGeneric(const Datatype& dt,
+ int c,
+ std::map<int, Node>& pre,
+ bool doBetaRed)
{
std::map<TypeNode, int> var_count;
- return mkGeneric(dt, c, var_count, pre);
+ return mkGeneric(dt, c, var_count, pre, doBetaRed);
}
-Node TermDbSygus::mkGeneric(const Datatype& dt, int c)
+Node TermDbSygus::mkGeneric(const Datatype& dt, int c, bool doBetaRed)
{
std::map<int, Node> pre;
- return mkGeneric(dt, c, pre);
+ return mkGeneric(dt, c, pre, doBetaRed);
}
struct CanonizeBuiltinAttributeId
@@ -293,6 +300,8 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
{
pre[j] = sygusToBuiltin(n[j], TypeNode::fromType(dt[i].getArgType(j)));
+ Trace("sygus-db-debug")
+ << "sygus to builtin " << n[j] << " is " << pre[j] << std::endl;
}
Node ret = mkGeneric(dt, i, pre);
Trace("sygus-db-debug")
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 6c62d7a1b..68381fb2a 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -223,15 +223,21 @@ class TermDbSygus {
* If i is in the domain of pre, then ti = pre[i].
* If i is not in the domain of pre, then ti = d_fv[1][ var_count[Ti ] ],
* and var_count[Ti] is incremented.
+ * If doBetaRed is true, then lambda operators are eagerly eliminated via
+ * beta reduction.
*/
Node mkGeneric(const Datatype& dt,
unsigned c,
std::map<TypeNode, int>& var_count,
- std::map<int, Node>& pre);
+ std::map<int, Node>& pre,
+ bool doBetaRed = true);
/** same as above, but with empty var_count */
- Node mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre);
+ Node mkGeneric(const Datatype& dt,
+ int c,
+ std::map<int, Node>& pre,
+ bool doBetaRed = true);
/** same as above, but with empty pre */
- Node mkGeneric(const Datatype& dt, int c);
+ Node mkGeneric(const Datatype& dt, int c, bool doBetaRed = true);
/** makes a symbolic term concrete
*
* Given a sygus datatype term n of type tn with holes (symbolic constructor
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index 8f280c587..5f51d8dec 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -187,6 +187,8 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
}
d_min_cons_term_size[i] = csize;
}
+ Trace("sygus-db") << "Register type " << dt.getName() << " finished"
+ << std::endl;
}
void SygusTypeInfo::initializeVarSubclasses()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback