diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-11 11:07:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-11 11:07:27 -0600 |
commit | 08cf2fcc63aadd2a7bb4f78b12ceda17ee570121 (patch) | |
tree | f70f7a88aa9704c7a0506fd8a0e6fdb69667414b /src | |
parent | 96c48c057b9e9f8d5c4bf9b2fa3b94c1d5861de7 (diff) | |
parent | 5d1c52999d78d5e825654d729279df8c49488133 (diff) |
Merge branch 'master' into fix3089fix3089
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 38 | ||||
-rw-r--r-- | src/theory/quantifiers/fun_def_evaluator.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 33 | ||||
-rw-r--r-- | src/theory/sets/rels_utils.h | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 24 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 2 |
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; |