From 6ae07a91cdd4f20f8fdccd7e31d217c6ca34ee45 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Apr 2014 15:50:56 -0500 Subject: [PATCH] Expand definitions in theory datatypes, now has the expected semantics for incorrectly applied selector terms. --- src/parser/smt2/smt2.cpp | 1 + src/printer/cvc/cvc_printer.cpp | 1 + src/printer/smt2/smt2_printer.cpp | 1 + src/smt/boolean_terms.cpp | 4 +- src/theory/datatypes/datatypes_rewriter.h | 4 +- src/theory/datatypes/kinds | 2 + src/theory/datatypes/theory_datatypes.cpp | 55 ++++++++++++++++--- src/theory/datatypes/theory_datatypes.h | 3 + .../datatypes/theory_datatypes_type_rules.h | 2 +- src/theory/quantifiers/options_handlers.h | 23 ++++---- .../quantifiers/quant_conflict_find.cpp | 2 +- src/theory/quantifiers/trigger.cpp | 2 +- src/theory/theory_model.cpp | 4 +- test/regress/regress0/datatypes/Makefile.am | 3 +- test/regress/regress0/datatypes/datatype1.cvc | 2 +- test/regress/regress0/datatypes/datatype3.cvc | 2 +- .../regress0/datatypes/wrong-sel-simp.cvc | 2 +- 17 files changed, 80 insertions(+), 33 deletions(-) diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 64b321613..e9e6ba857 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -158,6 +158,7 @@ void Smt2::addTheory(Theory theory) { Parser::addOperator(kind::APPLY_CONSTRUCTOR); Parser::addOperator(kind::APPLY_TESTER); Parser::addOperator(kind::APPLY_SELECTOR); + Parser::addOperator(kind::APPLY_SELECTOR_TOTAL); break; case THEORY_STRINGS: diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 4d784c383..63529c2a5 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -316,6 +316,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: + case kind::APPLY_SELECTOR_TOTAL: case kind::APPLY_TESTER: toStream(op, n.getOperator(), depth, types, false); break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ea335f2e5..1250bc659 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -424,6 +424,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::APPLY_TESTER: case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: + case kind::APPLY_SELECTOR_TOTAL: case kind::PARAMETRIC_DATATYPE: break; diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 111324dfa..e46a76ed7 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -152,7 +152,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); appctorb << (*dt2)[i].getConstructor(); for(size_t j = 0; j < ctor.getNumArgs(); ++j) { - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); } Node appctor = appctorb; if(i == 0) { @@ -191,7 +191,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { for(size_t j = 0; j < ctor.getNumArgs(); ++j) { TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()); asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), asType); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType); } Node appctor = appctorb; if(i == 0) { diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 37a656555..8cb3fb4a2 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -88,7 +88,7 @@ public: const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst(); return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst().getField())]); } - if(in.getKind() == kind::APPLY_SELECTOR && + if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) { // These strange (half-tuple-converted) terms can be created by // the system if you have something like "foo.1" for a tuple @@ -118,7 +118,7 @@ public: Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); } - if(in.getKind() == kind::APPLY_SELECTOR && + if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions // where the selector doesn't match the constructor, diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index bb6fd4373..b222738ae 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -39,6 +39,7 @@ cardinality TESTER_TYPE \ parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application" parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application" +parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1: "selector application (total)" parameterized APPLY_TESTER TESTER_TYPE 1: "tester application" @@ -82,6 +83,7 @@ constant ASCRIPTION_TYPE \ typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule +typerule APPLY_SELECTOR_TOTAL ::CVC4::theory::datatypes::DatatypeSelectorTypeRule typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index b00b4148d..0b0f5807c 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -54,7 +54,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); } @@ -318,6 +318,47 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { flushPendingFacts(); } +Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { + switch( n.getKind() ){ + case kind::APPLY_SELECTOR: { + Node selector = n.getOperator(); + Expr selectorExpr = selector.toExpr(); + size_t selectorIndex = Datatype::cindexOf(selectorExpr); + const Datatype& dt = Datatype::datatypeOf(selectorExpr); + const DatatypeConstructor& c = dt[selectorIndex]; + Expr tester = c.getTester(); + Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] ); + tst = Rewriter::rewrite( tst ); + Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] ); + Node n_ret; + if( tst==NodeManager::currentNM()->mkConst( true ) ){ + n_ret = sel; + }else{ + if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){ + std::stringstream ss; + ss << selector << "_uf"; + d_exp_def_skolem[ selector ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(), + NodeManager::currentNM()->mkFunctionType( n[0].getType(), n.getType() ) ); + } + Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0] ); + if( tst==NodeManager::currentNM()->mkConst( false ) ){ + n_ret = sk; + }else{ + n_ret = NodeManager::currentNM()->mkNode( kind::ITE, tst, sel, sk ); + } + } + //n_ret = Rewriter::rewrite( n_ret ); + Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl; + return n_ret; + } + break; + default: + return n; + break; + } + Unreachable(); +} + void TheoryDatatypes::presolve() { Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; } @@ -332,7 +373,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { } TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst().getIndex()].getSelector()), in[0]); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst().getIndex()].getSelector()), in[0]); } else if(in.getKind() == kind::RECORD_SELECT) { TypeNode t = in[0].getType(); if(t.hasAttribute(expr::DatatypeRecordAttr())) { @@ -340,7 +381,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { } TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst().getField()].getSelector()), in[0]); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst().getField()].getSelector()), in[0]); } TypeNode t = in.getType(); @@ -404,7 +445,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { b << in[1]; Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl; } else { - b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]); + b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][i].getSelector()), in[0]); Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl; } } @@ -848,7 +889,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ } void TheoryDatatypes::collapseSelector( Node s, Node c ) { - Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, s.getOperator(), c ); + Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); Node rr = Rewriter::rewrite( r ); //if( r!=rr ){ //Node eq_exp = NodeManager::currentNM()->mkConst(true); @@ -1075,7 +1116,7 @@ void TheoryDatatypes::collectTerms( Node n ) { //eqc->d_selectors = true; } */ - }else if( n.getKind() == APPLY_SELECTOR ){ + }else if( n.getKind() == APPLY_SELECTOR_TOTAL ){ //we must also record which selectors exist Debug("datatypes") << " Found selector " << n << endl; if (n.getType().isBoolean()) { @@ -1117,7 +1158,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, std::vector< Node > children; children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ - Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n ); + Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n ); if( mkVar ){ TypeNode tn = nc.getType(); if( dt.isParametric() ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 3a29433f8..2a93878d0 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -166,6 +166,8 @@ private: std::vector< Node > d_pending; std::map< Node, Node > d_pending_exp; std::vector< Node > d_pending_merge; + /** expand definition skolem functions */ + std::map< Node, Node > d_exp_def_skolem; private: /** assert fact */ void assertFact( Node fact, Node exp ); @@ -208,6 +210,7 @@ public: void check(Effort e); void preRegisterTerm(TNode n); + Node expandDefinition(LogicRequest &logicRequest, Node n); Node ppRewrite(TNode n); void presolve(); void addSharedTerm(TNode t); diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 527d110e0..d08b511dd 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -98,7 +98,7 @@ struct DatatypeConstructorTypeRule { struct DatatypeSelectorTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate) { - Assert(n.getKind() == kind::APPLY_SELECTOR); + Assert(n.getKind() == kind::APPLY_SELECTOR || n.getKind() == kind::APPLY_SELECTOR_TOTAL ); TypeNode selType = n.getOperator().getType(check); Type t = selType[0].toType(); Assert( t.isDatatype() ); diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 164e9e643..b7e624a66 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -92,8 +92,8 @@ instgen \n\ + Use instantiation algorithm that mimics Inst-Gen calculus. \n\ \n\ gen-ev \n\ -+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper.\n\ ++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ + model finding paper based on generalizing evaluations.\n\ \n\ fmc-interval \n\ + Same as default, but with intervals for models of integer functions.\n\ @@ -131,9 +131,6 @@ conflict \n\ partial \n\ + Apply QCF algorithm to instantiate heuristically as well. \n\ \n\ -partial \n\ -+ Apply QCF to instantiate heuristically as well. \n\ -\n\ mc \n\ + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ \n\ @@ -217,21 +214,21 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar } inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "gen-ev") { + if(optarg == "gen-ev") { return MBQI_GEN_EVAL; - } else if(optarg == "none") { + } else if(optarg == "none") { return MBQI_NONE; - } else if(optarg == "instgen") { + } else if(optarg == "instgen") { return MBQI_INST_GEN; - } else if(optarg == "default" || optarg == "fmc") { + } else if(optarg == "default" || optarg == "fmc") { return MBQI_FMC; - } else if(optarg == "fmc-interval") { + } else if(optarg == "fmc-interval") { return MBQI_FMC_INTERVAL; - } else if(optarg == "interval") { + } else if(optarg == "interval") { return MBQI_INTERVAL; - } else if(optarg == "trust") { + } else if(optarg == "trust") { return MBQI_TRUST; - } else if(optarg == "help") { + } else if(optarg == "help") { puts(mbqiModeHelp.c_str()); exit(1); } else { diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index c0b318f23..e27d438be 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1488,7 +1488,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) { bool MatchGen::isHandledUfTerm( TNode n ) { return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ; + n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; } Node MatchGen::getOperator( QuantConflictFind * p, Node n ) { diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 6912c9e89..3de12b9c9 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){ bool Trigger::isAtomicTrigger( Node n ){ return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER; + n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; } bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 405fceb6f..f207bdb8e 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -41,7 +41,7 @@ TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFunc d_equalityEngine->addFunctionKind(kind::SELECT); // d_equalityEngine->addFunctionKind(kind::STORE); d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); d_eeContext->push(); } @@ -422,7 +422,7 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t bool TheoryEngineModelBuilder::isAssignable(TNode n) { - return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR); + return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL); } diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 84adb4f84..e8a8f16f5 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -31,7 +31,6 @@ TESTS = \ datatype0.cvc \ datatype1.cvc \ datatype2.cvc \ - datatype3.cvc \ datatype4.cvc \ datatype13.cvc \ empty_tuprec.cvc \ @@ -64,6 +63,8 @@ TESTS = \ FAILING_TESTS = \ datatype-dump.cvc +# takes a long time to build model on debug : datatype3.cvc + EXTRA_DIST = $(TESTS) if CVC4_BUILD_PROFILE_COMPETITION diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc index 5172eeb48..3934959f1 100644 --- a/test/regress/regress0/datatypes/datatype1.cvc +++ b/test/regress/regress0/datatypes/datatype1.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc index 5f130b6ae..fff1a5dd7 100644 --- a/test/regress/regress0/datatypes/datatype3.cvc +++ b/test/regress/regress0/datatypes/datatype3.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc index 7455f809c..b0dbdc46e 100644 --- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc +++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE nat = succ(pred : nat) | zero END; -- 2.30.2