From 58c511a607a7a3560590b49f17ee3e92b364dbcf Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 27 Aug 2012 19:27:28 +0000 Subject: [PATCH] * Reversing commit r4258 (which disabled failing regressions). Fixed the problem so they're no longer failing (in the quantifiers rewriter). Resolves bug #381. * Added LAMBDA kind and type rule, and Node::isClosure(). (this commit was certified error- and warning-free by the test-and-commit script.) --- src/expr/node.h | 8 ++++++++ src/theory/builtin/kinds | 3 +++ src/theory/builtin/theory_builtin_type_rules.h | 18 ++++++++++++++++++ .../quantifiers/quantifiers_rewriter.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 10 +++++----- .../theory_rewriterules_type_rules.h | 2 +- test/regress/regress0/quantifiers/Makefile.am | 13 +++++-------- 7 files changed, 41 insertions(+), 15 deletions(-) diff --git a/src/expr/node.h b/src/expr/node.h index 0ce042654..7108ba74a 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -453,6 +453,14 @@ public: return getMetaKind() == kind::metakind::VARIABLE; } + inline bool isClosure() const { + assertTNodeNotExpired(); + return getKind() == kind::LAMBDA || + getKind() == kind::FORALL || + getKind() == kind::EXISTS || + getKind() == kind::REWRITE_RULE; + } + /** * Returns the unique id of this node * @return the ud diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 48fe4d84a..c4c3435a2 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -298,6 +298,8 @@ variable BOUND_VARIABLE "bound variable" variable SKOLEM "skolem var" operator TUPLE 1: "a tuple" +operator LAMBDA 2 "lambda" + constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ ::CVC4::TypeConstantHashFunction \ @@ -338,6 +340,7 @@ typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule +typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule constant SUBTYPE_TYPE \ ::CVC4::Predicate \ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 68d9e8702..95ede1c46 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -145,6 +145,24 @@ public: } };/* class StringConstantTypeRule */ +class LambdaTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + if( n[0].getType(check) != nodeManager->boundVarListType() ) { + std::stringstream ss; + ss << "expected a bound var list for LAMBDA expression, got `" + << n[0].getType().toString() << "'"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + std::vector argTypes; + for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) { + argTypes.push_back((*i).getType()); + } + TypeNode rangeType = n[1].getType(check); + return nodeManager->mkFunctionType(argTypes, rangeType); + } +};/* class LambdaTypeRule */ + class SortProperties { public: inline static bool isWellFounded(TypeNode type) { diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index e928010b6..b0728de29 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -473,7 +473,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){ terms.push_back( body[0][i] ); - subs.push_back( NodeManager::currentNM()->mkSkolem( body[0][i].getType() ) ); + subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) ); } args.insert( args.end(), subs.begin(), subs.end() ); }else{ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cc74e3e76..a73d42a31 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -14,11 +14,11 @@ ** \brief Implementation of term databse class **/ - #include "theory/quantifiers/term_database.h" - #include "theory/quantifiers_engine.h" - #include "theory/uf/theory_uf_instantiator.h" - #include "theory/theory_engine.h" - #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers/first_order_model.h" using namespace std; using namespace CVC4; diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h index 605324b20..f03fba73a 100644 --- a/src/theory/rewriterules/theory_rewriterules_type_rules.h +++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h @@ -60,7 +60,7 @@ public: } return nodeManager->booleanType(); } -};/* class RewriterulesTypeRule */ +};/* class RewriteRuleTypeRule */ class RRRewriteTypeRule { diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 8880bf3ca..38cc59125 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -28,16 +28,13 @@ TESTS = \ opisavailable-12.smt2 \ ricart-agrawala6.smt2 \ set8.smt2 \ + smtlib384a03.smt2 \ + smtlib46f14a.smt2 \ + smtlibf957ea.smt2 \ + gauss_init_0030.fof.smt2 \ + piVC_5581bd.smt2 \ set3.smt2 -# removed because failing -# smtlib384a03.smt2 \ -# smtlib46f14a.smt2 \ -# smtlibf957ea.smt2 \ -# gauss_init_0030.fof.smt2 \ -# piVC_5581bd.smt2 \ -# - # removed because it now reports unknown # symmetric_unsat_7.smt2 \ # -- 2.30.2