From decde5be0b6409b9c1b84f40c8383bb8483e4566 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 13 Apr 2016 11:22:43 -0500 Subject: [PATCH] Handle parametric datatypes with --quant-ind. Minor updates. --- src/options/quantifiers_options | 2 ++ src/smt/smt_engine.cpp | 10 +++++++ src/theory/datatypes/datatypes_rewriter.h | 4 --- .../quantifiers/conjecture_generator.cpp | 5 +++- src/theory/quantifiers/term_database.cpp | 27 ++++++++++++++----- 5 files changed, 37 insertions(+), 11 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index c27b21e23..74b3011a6 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -210,6 +210,8 @@ option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50 number of ground terms to generate for model filtering option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false more aggressive merging for universal equality engine, introduces terms +option conjectureGenMaxDepth --conjecture-gen-max-depth=N int :default 3 + maximum depth of terms to consider for conjectures ### synthesis options diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bff8e187f..bd67af466 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1095,20 +1095,27 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : } void SmtEngine::finishInit() { + Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; // ensure that our heuristics are properly set up setDefaults(); + + Trace("smt-debug") << "Making decision engine..." << std::endl; d_decisionEngine = new DecisionEngine(d_context, d_userContext); d_decisionEngine->init(); // enable appropriate strategies + Trace("smt-debug") << "Making prop engine..." << std::endl; d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, d_userContext, d_private->getReplayLog(), d_replayStream, d_channels); + Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(d_propEngine); d_theoryEngine->setDecisionEngine(d_decisionEngine); + Trace("smt-debug") << "Finishing init for theory engine..." << std::endl; d_theoryEngine->finishInit(); + Trace("smt-debug") << "Set up assertion list..." << std::endl; // [MGD 10/20/2011] keep around in incremental mode, due to a // cleanup ordering issue and Nodes/TNodes. If SAT is popped // first, some user-context-dependent TNodes might still exist @@ -1129,6 +1136,7 @@ void SmtEngine::finishInit() { << SetBenchmarkLogicCommand(everything.getLogicString()); } + Trace("smt-debug") << "Dump declaration commands..." << std::endl; // dump out any pending declaration commands for(unsigned i = 0; i < d_dumpCommands.size(); ++i) { Dump("declarations") << *d_dumpCommands[i]; @@ -1137,6 +1145,7 @@ void SmtEngine::finishInit() { d_dumpCommands.clear(); PROOF( ProofManager::currentPM()->setLogic(d_logic); ); + Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; } void SmtEngine::finalOptionsAreSet() { @@ -3638,6 +3647,7 @@ Result SmtEngine::check() { // Make sure the prop layer has all of the assertions Trace("smt") << "SmtEngine::check(): processing assertions" << endl; d_private->processAssertions(); + Trace("smt") << "SmtEngine::check(): done processing assertions" << endl; // Turn off stop only for QF_LRA // TODO: Bring up in a meeting where to put this diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index cd31778ec..dd2803d30 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -260,10 +260,6 @@ public: /** get instantiate cons */ static Node getInstCons( Node n, const Datatype& dt, int index ) { Assert( index>=0 && index<(int)dt.getNumConstructors() ); - Type tspec; - if( dt.isParametric() ){ - tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); - } std::vector< Node > children; children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 27bbb0f5f..2cc49ef5a 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -605,7 +605,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { std::vector< TypeNode > rt_types; std::map< TypeNode, std::map< int, std::vector< Node > > > conj_lhs; unsigned addedLemmas = 0; - for( unsigned depth=1; depth<=3; depth++ ){ + unsigned maxDepth = options::conjectureGenMaxDepth(); + for( unsigned depth=1; depth<=maxDepth; depth++ ){ Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..." << std::endl; Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : " << std::endl; //set up environment @@ -1167,6 +1168,8 @@ void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsi d_waiting_conjectures_score.push_back( score ); d_waiting_conjectures[lhs].push_back( rhs ); d_waiting_conjectures[rhs].push_back( lhs ); + }else{ + Trace("sg-conjecture-debug2") << "...do not consider " << lhs << " == " << rhs << ", score = " << score << std::endl; } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 51c72d7bb..8b09d8e5d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1016,14 +1016,29 @@ Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) { } -void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){ +void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){ + TypeNode tspec; + if( dt.isParametric() ){ + tspec = TypeNode::fromType( dc.getSpecializedConstructorType(n.getType().toType()) ); + Trace("sk-ind-debug") << "Specialized constructor type : " << tspec << std::endl; + Assert( tspec.getNumChildren()==dc.getNumArgs() ); + } + Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " << dt.getName() << std::endl; for( unsigned j=0; j ssc; - if( tn==ntn ){ - ssc.push_back( n ); + if( dt.isParametric() ){ + Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn << std::endl; + if( tspec[j]==ntn ){ + ssc.push_back( n ); + } + }else{ + TypeNode tn = TypeNode::fromType( dc[j].getRangeType() ); + Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl; + if( tn==ntn ){ + ssc.push_back( n ); + } } - /* TODO + /* TODO: more than weak structural induction else if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) && std::find( visited.begin(), visited.end(), tn )==visited.end() ){ visited.push_back( tn ); const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype(); @@ -1101,7 +1116,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes std::vector< Node > disj; for( unsigned i=0; i selfSel; - getSelfSel( dt[i], k, tn, selfSel ); + getSelfSel( dt, dt[i], k, tn, selfSel ); std::vector< Node > conj; conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() ); for( unsigned j=0; j