From 1bceb5036a208746bfba1ec42d65862d0d231a83 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 9 Nov 2019 16:09:11 -0600 Subject: Fixes in relations related to datatypes not passed by reference (#3449) The current code is creating/destroying datatypes unnecessarily. --- src/theory/sets/rels_utils.h | 6 +++--- src/theory/sets/theory_sets_rels.cpp | 24 ++++++++++++++---------- src/theory/sets/theory_sets_rewriter.cpp | 2 +- 3 files changed, 18 insertions(+), 14 deletions(-) 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 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 r1_element; std::vector 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; -- cgit v1.2.3 From 7f7c4e5f7bfb5c38611afa3a016f4f767d5b86fd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 10 Nov 2019 08:45:39 -0600 Subject: Fix bugs related to sygus higher-order + recursive functions (#3448) --- src/theory/quantifiers/fun_def_evaluator.cpp | 10 +------ .../quantifiers/sygus/sygus_grammar_cons.cpp | 33 ++++++++++++++++++++-- test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/list_recursor.sy | 26 +++++++++++++++++ 4 files changed, 58 insertions(+), 12 deletions(-) create mode 100644 test/regress/regress1/sygus/list_recursor.sy 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 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& vars = ti.getVarList(); + Assert(!vars.empty()); + std::vector vs; + for (const Node& v : vars) + { + vs.push_back(nm->mkBoundVar(v.getType())); + } + Node lvl = nm->mkNode(BOUND_VAR_LIST, vs); + std::vector 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/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c98dd1be2..aa5329e2f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1718,6 +1718,7 @@ set(regress_1_tests regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy + regress1/sygus/list_recursor.sy regress1/sygus/logiccell_help.sy regress1/sygus/max.sy regress1/sygus/max2-bv.sy diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy new file mode 100644 index 000000000..53c55397e --- /dev/null +++ b/test/regress/regress1/sygus/list_recursor.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 --uf-ho + +(set-logic ALL) + +(declare-datatype List ((cons (head Int) (tail List)) (nil))) + +(define-fun-rec List_rec ((x Int) (y (-> Int List Int Int)) (l List)) Int + (ite ((_ is nil) l) x + (y (head l) (tail l) (List_rec x y (tail l))))) + +(synth-fun f () Int + ((I Int)) + ((I Int (0 1 (+ I I))))) + +(synth-fun g ((x Int) (y List) (z Int)) Int + ((I Int) (L List)) + ((I Int (x z (+ I I) (head L) 0 1)) + (L List (y (tail y))))) + + +(constraint (= (List_rec f g (cons 0 (cons 1 nil))) 2)) +(constraint (= (List_rec f g (cons 0 (cons 0 nil))) 2)) +(constraint (= (List_rec f g (cons 5 (cons 3 (cons 3 (cons 0 nil))))) 4)) +(constraint (= (List_rec f g nil) 0)) +(check-synth) -- cgit v1.2.3 From 62e2ba213a6488197fa0a9b3cdd7845fc397d32b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 11 Nov 2019 10:09:00 -0600 Subject: Eliminate remaining references to type/expr in datatype type rules. (#3450) --- src/theory/datatypes/theory_datatypes_type_rules.h | 38 +++++++++++++--------- 1 file changed, 23 insertions(+), 15 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(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) -- cgit v1.2.3 From 5d1c52999d78d5e825654d729279df8c49488133 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 11 Nov 2019 09:07:14 -0800 Subject: Update README according to the new website (#3438) --- README.md | 33 +++++++++++++-------------------- 1 file changed, 13 insertions(+), 20 deletions(-) diff --git a/README.md b/README.md index faef42e66..b22882d57 100644 --- a/README.md +++ b/README.md @@ -13,6 +13,11 @@ modulo a first order theory (or a combination of such theories). It is the fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code from any previous version. +If you are using CVC4 in your work, or incorporating it into software of your +own, we invite you to send us a description and link to your +project/software, so that we can link it on our [Third Party +Applications](https://cvc4.github.io/third-party-applications.html) page. + CVC4 is intended to be an open and extensible SMT engine. It can be used as a stand-alone tool or as a library. It has been designed to increase the performance and reduce the memory overhead of its predecessors. It is written @@ -22,10 +27,17 @@ entirely in C++ and is released under an open-source software license (see file Website ------------------------------------------------------------------------------- +CVC4's website is available at: +http://cvc4.cs.stanford.edu/ -More information about CVC4 is available at: +Documentation +------------------------------------------------------------------------------- +Documentation for users of CVC4 is available at: http://cvc4.cs.stanford.edu/ +Documentation for developers is available at: +https://github.com/CVC4/CVC4/wiki/Developer-Guide + Download ------------------------------------------------------------------------------- @@ -47,25 +59,6 @@ For detailed build and installation instructions on these platforms, see file [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md). -Getting Started -------------------------------------------------------------------------------- - -We recommend that you visit our CVC4 tutorials online at: - - http://cvc4.cs.stanford.edu/wiki/Tutorials - -for help getting started using CVC4. - -If you need help with using CVC4, please refer to -[http://cvc4.stanford.edu#technical-support]( - http://cvc4.stanford.edu#technical-support). - -If you are using CVC4 in your work, or incorporating it into software of your -own, we'd like to invite you to leave a description and link to your -project/software on our [Third Party -Applications](http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications). - - Bug Reports ------------------------------------------------------------------------------- -- cgit v1.2.3