summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/sygus_datatype.cpp44
-rw-r--r--src/expr/sygus_datatype.h54
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_norm.cpp14
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_red.cpp28
4 files changed, 101 insertions, 39 deletions
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index d8ee2e1ea..73f7c5769 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -26,15 +26,16 @@ std::string SygusDatatype::getName() const { return d_dt.getName(); }
void SygusDatatype::addConstructor(Node op,
const std::string& name,
- const std::vector<TypeNode>& consTypes,
+ const std::vector<TypeNode>& argTypes,
std::shared_ptr<SygusPrintCallback> spc,
int weight)
{
- d_ops.push_back(op);
- d_cons_names.push_back(std::string(name));
- d_pc.push_back(spc);
- d_weight.push_back(weight);
- d_consArgs.push_back(consTypes);
+ d_cons.push_back(SygusDatatypeConstructor());
+ d_cons.back().d_op = op;
+ d_cons.back().d_name = name;
+ d_cons.back().d_argTypes = argTypes;
+ d_cons.back().d_pc = spc;
+ d_cons.back().d_weight = weight;
}
void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
@@ -53,15 +54,21 @@ void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
av, cname, builtinArg, printer::SygusEmptyPrintCallback::getEmptyPC(), 0);
}
void SygusDatatype::addConstructor(Kind k,
- const std::vector<TypeNode>& consTypes,
+ const std::vector<TypeNode>& argTypes,
std::shared_ptr<SygusPrintCallback> spc,
int weight)
{
NodeManager* nm = NodeManager::currentNM();
- addConstructor(nm->operatorOf(k), kindToString(k), consTypes, spc, weight);
+ addConstructor(nm->operatorOf(k), kindToString(k), argTypes, spc, weight);
}
-size_t SygusDatatype::getNumConstructors() const { return d_ops.size(); }
+size_t SygusDatatype::getNumConstructors() const { return d_cons.size(); }
+
+const SygusDatatypeConstructor& SygusDatatype::getConstructor(unsigned i) const
+{
+ Assert(i < d_cons.size());
+ return d_cons[i];
+}
void SygusDatatype::initializeDatatype(TypeNode sygusType,
Node sygusVars,
@@ -69,21 +76,26 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType,
bool allowAll)
{
// should not have initialized (set sygus) yet
- Assert(!d_dt.isSygus());
+ Assert(!isInitialized());
+ // should have added a constructor
+ Assert(!d_cons.empty());
/* Use the sygus type to not lose reference to the original types (Bool,
* Int, etc) */
d_dt.setSygus(sygusType.toType(), sygusVars.toExpr(), allowConst, allowAll);
- for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
+ for (unsigned i = 0, ncons = d_cons.size(); i < ncons; ++i)
{
// must convert to type now
std::vector<Type> cargs;
- for (TypeNode& ct : d_consArgs[i])
+ for (TypeNode& ct : d_cons[i].d_argTypes)
{
cargs.push_back(ct.toType());
}
// add (sygus) constructor
- d_dt.addSygusConstructor(
- d_ops[i].toExpr(), d_cons_names[i], cargs, d_pc[i], d_weight[i]);
+ d_dt.addSygusConstructor(d_cons[i].d_op.toExpr(),
+ d_cons[i].d_name,
+ cargs,
+ d_cons[i].d_pc,
+ d_cons[i].d_weight);
}
Trace("sygus-type-cons") << "...built datatype " << d_dt << " ";
}
@@ -91,8 +103,10 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType,
const Datatype& SygusDatatype::getDatatype() const
{
// should have initialized by this point
- Assert(d_dt.isSygus());
+ Assert(isInitialized());
return d_dt;
}
+bool SygusDatatype::isInitialized() const { return d_dt.isSygus(); }
+
} // namespace CVC4
diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h
index 132406c69..e7b60f3a3 100644
--- a/src/expr/sygus_datatype.h
+++ b/src/expr/sygus_datatype.h
@@ -33,6 +33,25 @@ struct SygusAnyConstAttributeId
typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
/**
+ * Information necessary to specify a sygus constructor. Further detail on these
+ * fields can be found in SygusDatatype below.
+ */
+class SygusDatatypeConstructor
+{
+ public:
+ /** The operator that the constructor encodes. */
+ Node d_op;
+ /** Name of the constructor. */
+ std::string d_name;
+ /** List of argument types. */
+ std::vector<TypeNode> d_argTypes;
+ /** Print callback of the constructor. */
+ std::shared_ptr<SygusPrintCallback> d_pc;
+ /** Weight of the constructor. */
+ int d_weight;
+};
+
+/**
* Keeps the necessary information for initializing a sygus datatype, which
* includes the operators, names, print callbacks and list of argument types
* for each constructor.
@@ -57,28 +76,28 @@ class SygusDatatype
*
* op: the builtin operator,
* name: the name of the constructor,
- * spc: the print callback (for custom printing of this node),
- * weight: the weight of this constructor,
- * consTypes: the argument types of the constructor (typically other sygus
+ * argTypes: the argument types of the constructor (typically other sygus
* datatype types).
+ * spc: the print callback (for custom printing of this node),
+ * weight: the weight of this constructor.
*
- * It should be the case that consTypes are sygus datatype types (possibly
+ * It should be the case that argTypes are sygus datatype types (possibly
* unresolved) that encode the arguments of the builtin operator. That is,
- * if op is the builtin PLUS operator, then consTypes could contain 2+
+ * if op is the builtin PLUS operator, then argTypes could contain 2+
* sygus datatype types that encode integer.
*/
void addConstructor(Node op,
const std::string& name,
- const std::vector<TypeNode>& consTypes,
+ const std::vector<TypeNode>& argTypes,
std::shared_ptr<SygusPrintCallback> spc = nullptr,
int weight = -1);
/**
* Add constructor that encodes an application of builtin kind k. Like above,
- * the arguments consTypes should correspond to sygus datatypes that encode
+ * the arguments argTypes should correspond to sygus datatypes that encode
* the types of the arguments of the kind.
*/
void addConstructor(Kind k,
- const std::vector<TypeNode>& consTypes,
+ const std::vector<TypeNode>& argTypes,
std::shared_ptr<SygusPrintCallback> spc = nullptr,
int weight = -1);
/**
@@ -90,6 +109,9 @@ class SygusDatatype
/** Get the number of constructors added to this class so far */
size_t getNumConstructors() const;
+ /** Get constructor at index i */
+ const SygusDatatypeConstructor& getConstructor(unsigned i) const;
+
/** builds a datatype with the information in the type object
*
* sygusType: the builtin type that this datatype encodes,
@@ -106,18 +128,12 @@ class SygusDatatype
/** Get the sygus datatype initialized by this class */
const Datatype& getDatatype() const;
+ /** is initialized */
+ bool isInitialized() const;
+
private:
- //---------- information to build normalized type node
- /** Operators for each constructor. */
- std::vector<Node> d_ops;
- /** Names for each constructor. */
- std::vector<std::string> d_cons_names;
- /** Print callbacks for each constructor */
- std::vector<std::shared_ptr<SygusPrintCallback>> d_pc;
- /** Weights for each constructor */
- std::vector<int> d_weight;
- /** List of argument types for each constructor */
- std::vector<std::vector<TypeNode>> d_consArgs;
+ /** Information for each constructor. */
+ std::vector<SygusDatatypeConstructor> d_cons;
/** Datatype to represent type's structure */
Datatype d_dt;
};
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 40046ef15..019abc28a 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -495,6 +495,7 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
const Datatype& dt,
std::vector<unsigned>& op_pos)
{
+ Assert(tn.isDatatype());
/* Corresponding type node to tn with the given operator positions. To be
* retrieved (if cached) or defined (otherwise) */
TypeNode unres_tn;
@@ -591,8 +592,19 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn)
{
+ if (!tn.isDatatype())
+ {
+ // Might not be a sygus datatype, e.g. if the input grammar had the
+ // any constant constructor.
+ return tn;
+ }
/* Collect all operators for normalization */
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const Datatype& dt = tn.getDatatype();
+ if (!dt.isSygus())
+ {
+ // datatype but not sygus datatype case
+ return tn;
+ }
std::vector<unsigned> op_pos(dt.getNumConstructors());
std::iota(op_pos.begin(), op_pos.end(), 0);
return normalizeSygusRec(tn, dt, op_pos);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 6bf8c56fb..b1b1ea62c 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -14,6 +14,7 @@
#include "theory/quantifiers/sygus/sygus_grammar_red.h"
+#include "expr/sygus_datatype.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
@@ -41,18 +42,37 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
{
Trace("sygus-red") << " Is " << dt[i].getName() << " a redundant operator?"
<< std::endl;
+ Node sop = Node::fromExpr(dt[i].getSygusOp());
+ if (sop.getAttribute(SygusAnyConstAttribute()))
+ {
+ // the any constant constructor is never redundant
+ d_sygus_red_status.push_back(0);
+ continue;
+ }
std::map<int, Node> 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++)
+ // a list of variants of the generic term (see getGenericList).
+ std::vector<Node> glist;
+ if (sop.isConst() || sop.getKind() == LAMBDA)
+ {
+ Assert(g.getNumChildren() == dt[i].getNumArgs());
+ for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+ {
+ pre[j] = g[j];
+ }
+ getGenericList(tds, dt, i, 0, pre, glist);
+ }
+ else
{
- pre[j] = g[j];
+ // It is a builtin (possibly) ground term. Its children do not correspond
+ // one-to-one with the arugments of the constructor. Hence, we consider
+ // only g itself as a variant.
+ glist.push_back(g);
}
- std::vector<Node> glist;
- getGenericList(tds, dt, i, 0, pre, glist);
// call the extended rewriter
bool red = false;
for (const Node& gr : glist)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback