diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-13 16:31:12 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-13 16:31:12 -0500 |
commit | a90b9e2b70be427d1380cb5e65dc33c86e4a63b2 (patch) | |
tree | a6cae3c98ec5c25b65c605dafd0d9e36e110245d /src/expr | |
parent | e69f6c3aa94e382d082d23f847709a97d9470f31 (diff) |
Disallow let in sygus grammars, check for free variables in sygus constructors (#3259)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.cpp | 33 |
1 files changed, 32 insertions, 1 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 5e1343bb0..cd78728b1 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -25,10 +25,11 @@ #include "expr/expr_manager_scope.h" #include "expr/matcher.h" #include "expr/node.h" +#include "expr/node_algorithm.h" #include "expr/node_manager.h" #include "expr/type.h" -#include "options/set_language.h" #include "options/datatypes_options.h" +#include "options/set_language.h" using namespace std; @@ -154,6 +155,36 @@ void Datatype::resolve(ExprManager* em, } d_record = new Record(fields); } + + if (isSygus()) + { + // all datatype constructors should be sygus and have sygus operators whose + // free variables are subsets of sygus bound var list. + Node sbvln = Node::fromExpr(d_sygus_bvl); + std::unordered_set<Node, NodeHashFunction> svs; + for (const Node& sv : sbvln) + { + svs.insert(sv); + } + for (unsigned i = 0, ncons = d_constructors.size(); i < ncons; i++) + { + Expr sop = d_constructors[i].getSygusOp(); + PrettyCheckArgument(!sop.isNull(), + this, + "Sygus datatype contains a non-sygus constructor"); + Node sopn = Node::fromExpr(sop); + std::unordered_set<Node, NodeHashFunction> fvs; + expr::getFreeVariables(sopn, fvs); + for (const Node& v : fvs) + { + PrettyCheckArgument( + svs.find(v) != svs.end(), + this, + "Sygus constructor has an operator with a free variable that is " + "not in the formal argument list of the function-to-synthesize"); + } + } + } } void Datatype::addConstructor(const DatatypeConstructor& c) { |