summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/datatypes/theory_datatypes_type_rules.h38
-rw-r--r--src/theory/quantifiers/fun_def_evaluator.cpp10
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.cpp33
-rw-r--r--src/theory/sets/rels_utils.h6
-rw-r--r--src/theory/sets/theory_sets_rels.cpp24
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp2
6 files changed, 72 insertions, 41 deletions
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 219124d8e..60841a5dd 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -20,6 +20,7 @@
#define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
#include "expr/type_matcher.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
namespace CVC4 {
@@ -42,16 +43,17 @@ struct DatatypeConstructorTypeRule {
TypeNode consType = n.getOperator().getType(check);
TypeNode t = consType.getConstructorRangeType();
Assert(t.isDatatype());
- DatatypeType dt = DatatypeType(t.toType());
TNode::iterator child_it = n.begin();
TNode::iterator child_it_end = n.end();
TypeNode::iterator tchild_it = consType.begin();
- if ((dt.isParametric() || check) &&
- n.getNumChildren() != consType.getNumChildren() - 1) {
+ if ((t.isParametricDatatype() || check)
+ && n.getNumChildren() != consType.getNumChildren() - 1)
+ {
throw TypeCheckingExceptionPrivate(
n, "number of arguments does not match the constructor type");
}
- if (dt.isParametric()) {
+ if (t.isParametricDatatype())
+ {
Debug("typecheck-idt") << "typecheck parameterized datatype " << n
<< std::endl;
TypeMatcher m(t);
@@ -67,7 +69,9 @@ struct DatatypeConstructorTypeRule {
TypeNode range = t.instantiateParametricDatatype(instTypes);
Debug("typecheck-idt") << "Return " << range << std::endl;
return range;
- } else {
+ }
+ else
+ {
if (check) {
Debug("typecheck-idt") << "typecheck cons: " << n << " "
<< n.getNumChildren() << std::endl;
@@ -128,12 +132,13 @@ struct DatatypeSelectorTypeRule {
TypeNode selType = n.getOperator().getType(check);
TypeNode t = selType[0];
Assert(t.isDatatype());
- DatatypeType dt = DatatypeType(t.toType());
- if ((dt.isParametric() || check) && n.getNumChildren() != 1) {
+ if ((t.isParametricDatatype() || check) && n.getNumChildren() != 1)
+ {
throw TypeCheckingExceptionPrivate(
n, "number of arguments does not match the selector type");
}
- if (dt.isParametric()) {
+ if (t.isParametricDatatype())
+ {
Debug("typecheck-idt") << "typecheck parameterized sel: " << n
<< std::endl;
TypeMatcher m(t);
@@ -155,7 +160,9 @@ struct DatatypeSelectorTypeRule {
types.begin(), types.end(), matches.begin(), matches.end());
Debug("typecheck-idt") << "Return " << range << std::endl;
return range;
- } else {
+ }
+ else
+ {
if (check) {
Debug("typecheck-idt") << "typecheck sel: " << n << std::endl;
Debug("typecheck-idt") << "sel type: " << selType << std::endl;
@@ -185,8 +192,8 @@ struct DatatypeTesterTypeRule {
TypeNode childType = n[0].getType(check);
TypeNode t = testType[0];
Assert(t.isDatatype());
- DatatypeType dt = DatatypeType(t.toType());
- if (dt.isParametric()) {
+ if (t.isParametricDatatype())
+ {
Debug("typecheck-idt") << "typecheck parameterized tester: " << n
<< std::endl;
TypeMatcher m(t);
@@ -195,7 +202,9 @@ struct DatatypeTesterTypeRule {
n,
"matching failed for tester argument of parameterized datatype");
}
- } else {
+ }
+ else
+ {
Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
Debug("typecheck-idt") << "test type: " << testType << std::endl;
if (!testType[0].isComparableTo(childType)) {
@@ -395,8 +404,7 @@ class DtSyguEvalTypeRule
throw TypeCheckingExceptionPrivate(
n, "datatype sygus eval takes a datatype head");
}
- const Datatype& dt =
- static_cast<DatatypeType>(headType.toType()).getDatatype();
+ const Datatype& dt = headType.getDatatype();
if (!dt.isSygus())
{
throw TypeCheckingExceptionPrivate(
@@ -490,7 +498,7 @@ class MatchTypeRule
}
bvs.erase(arg);
}
- unsigned ci = Datatype::indexOf(nc[pindex].getOperator().toExpr());
+ unsigned ci = utils::indexOf(nc[pindex].getOperator());
patIndices.insert(ci);
}
else if (ncpk == kind::BOUND_VARIABLE)
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index 83debe0d9..376d0eb47 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -150,17 +150,10 @@ Node FunDefEvaluator::evaluate(Node n) const
ret = nm->mkNode(cur.getKind(), children);
ret = Rewriter::rewrite(ret);
}
- if (!ret.isConst())
- {
- Trace("fd-eval") << "FunDefEvaluator: non-constant subterm " << ret
- << ", FAIL" << std::endl;
- // failed, possibly due to free variable
- return Node::null();
- }
visited[cur] = ret;
}
}
- else if (!curEval.isConst())
+ else if (cur != curEval && !curEval.isConst())
{
Trace("fd-eval-debug") << "from body " << cur << std::endl;
// we had to evaluate our body, which should have a definition now
@@ -168,7 +161,6 @@ Node FunDefEvaluator::evaluate(Node n) const
Assert(it != visited.end());
// our definition is the result of the body
visited[cur] = it->second;
- Assert(it->second.isConst());
}
}
} while (!visit.empty());
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 8f935de27..b8bf6c865 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -287,6 +287,7 @@ Node CegGrammarConstructor::convertToEmbedding(Node n)
std::stack<TNode> visit;
TNode cur;
visit.push(n);
+ TermDbSygus* tds = d_qe->getTermDatabaseSygus();
do {
cur = visit.top();
visit.pop();
@@ -337,12 +338,38 @@ Node CegGrammarConstructor::convertToEmbedding(Node n)
}
if (makeEvalFun)
{
- // will make into an application of an evaluation function
- ret = nm->mkNode(DT_SYGUS_EVAL, children);
+ if (!cur.getType().isFunction())
+ {
+ // will make into an application of an evaluation function
+ ret = nm->mkNode(DT_SYGUS_EVAL, children);
+ }
+ else
+ {
+ Assert(children.size() == 1);
+ Node ef = children[0];
+ // Otherwise, we are using the function-to-synthesize itself in a
+ // higher-order setting. We must return the lambda term:
+ // lambda x1...xn. (DT_SYGUS_EVAL ef x1 ... xn)
+ // where ef is the first order variable for the
+ // function-to-synthesize.
+ SygusTypeInfo& ti = tds->getTypeInfo(ef.getType());
+ const std::vector<Node>& vars = ti.getVarList();
+ Assert(!vars.empty());
+ std::vector<Node> vs;
+ for (const Node& v : vars)
+ {
+ vs.push_back(nm->mkBoundVar(v.getType()));
+ }
+ Node lvl = nm->mkNode(BOUND_VAR_LIST, vs);
+ std::vector<Node> eargs;
+ eargs.push_back(ef);
+ eargs.insert(eargs.end(), vs.begin(), vs.end());
+ ret = nm->mkNode(LAMBDA, lvl, nm->mkNode(DT_SYGUS_EVAL, eargs));
+ }
}
else if (childChanged)
{
- ret = NodeManager::currentNM()->mkNode(ret_k, children);
+ ret = nm->mkNode(ret_k, children);
}
visited[cur] = ret;
}
diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index 6354b59e9..8ce314c94 100644
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -67,7 +67,7 @@ public:
return tuple[n_th];
}
TypeNode tn = tuple.getType();
- Datatype dt = tn.getDatatype();
+ const Datatype& dt = tn.getDatatype();
return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal( tn.toType(), n_th ), tuple);
}
@@ -77,7 +77,7 @@ public:
std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
std::reverse( tuple_types.begin(), tuple_types.end() );
TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types );
- Datatype dt = tn.getDatatype();
+ const Datatype& dt = tn.getDatatype();
elements.push_back( Node::fromExpr(dt[0].getConstructor() ) );
for(int i = tuple_types.size() - 1; i >= 0; --i) {
elements.push_back( nthElementOfTuple(tuple, i) );
@@ -85,7 +85,7 @@ public:
return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements );
}
static Node constructPair(Node rel, Node a, Node b) {
- Datatype dt = rel.getType().getSetElementType().getDatatype();
+ const Datatype& dt = rel.getType().getSetElementType().getDatatype();
return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b);
}
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 5c24cb088..e8724aa8b 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -299,7 +299,8 @@ void TheorySetsRels::check(Theory::Effort level)
}
hasChecked.insert( fst_mem_rep );
- Datatype dt = join_image_term.getType().getSetElementType().getDatatype();
+ const Datatype& dt =
+ join_image_term.getType().getSetElementType().getDatatype();
Node new_membership = NodeManager::currentNM()->mkNode(kind::MEMBER,
NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR,
Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ),
@@ -428,7 +429,8 @@ void TheorySetsRels::check(Theory::Effort level)
Node reason = exp;
Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 );
Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 );
- Datatype dt = iden_term[0].getType().getSetElementType().getDatatype();
+ const Datatype& dt =
+ iden_term[0].getType().getSetElementType().getDatatype();
Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ), iden_term[0] );
if( exp[1] != iden_term ) {
@@ -765,18 +767,18 @@ void TheorySetsRels::check(Theory::Effort level)
Node mem = exp[0];
std::vector<Node> r1_element;
std::vector<Node> r2_element;
- Datatype dt = pt_rel[0].getType().getSetElementType().getDatatype();
+ const Datatype& dt1 = pt_rel[0].getType().getSetElementType().getDatatype();
unsigned int s1_len = pt_rel[0].getType().getSetElementType().getTupleLength();
unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength();
- r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+ r1_element.push_back(Node::fromExpr(dt1[0].getConstructor()));
unsigned int i = 0;
for(; i < s1_len; ++i) {
r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
}
- dt = pt_rel[1].getType().getSetElementType().getDatatype();
- r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+ const Datatype& dt2 = pt_rel[1].getType().getSetElementType().getDatatype();
+ r2_element.push_back(Node::fromExpr(dt2[0].getConstructor()));
for(; i < tup_len; ++i) {
r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
}
@@ -823,18 +825,20 @@ void TheorySetsRels::check(Theory::Effort level)
TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0];
Node shared_x = d_state.getSkolemCache().mkTypedSkolemCached(
shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj");
- Datatype dt = join_rel[0].getType().getSetElementType().getDatatype();
+ const Datatype& dt1 =
+ join_rel[0].getType().getSetElementType().getDatatype();
unsigned int s1_len = join_rel[0].getType().getSetElementType().getTupleLength();
unsigned int tup_len = join_rel.getType().getSetElementType().getTupleLength();
unsigned int i = 0;
- r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+ r1_element.push_back(Node::fromExpr(dt1[0].getConstructor()));
for(; i < s1_len-1; ++i) {
r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
}
r1_element.push_back(shared_x);
- dt = join_rel[1].getType().getSetElementType().getDatatype();
- r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+ const Datatype& dt2 =
+ join_rel[1].getType().getSetElementType().getDatatype();
+ r2_element.push_back(Node::fromExpr(dt2[0].getConstructor()));
r2_element.push_back(shared_x);
for(; i < tup_len; ++i) {
r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index aa6f4de3f..a7c506582 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -431,7 +431,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
++rel_mems_it_snd;
}
if( existing_mems.size() >= min_card ) {
- Datatype dt = node.getType().getSetElementType().getDatatype();
+ const Datatype& dt = node.getType().getSetElementType().getDatatype();
join_img_mems.insert(NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ));
}
++rel_mems_it;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback