From 7ff0098a91df9c912cbe98fb128fcf2cbc71e95c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 23 Jan 2015 10:04:38 +0100 Subject: [PATCH] Rework inst-closure. --- src/parser/smt2/Smt2.g | 4 ++++ src/theory/quantifiers/kinds | 3 +++ src/theory/quantifiers/term_database.cpp | 11 ++++++++--- src/theory/quantifiers/term_database.h | 4 +++- src/theory/quantifiers/theory_quantifiers.cpp | 10 ++++++++++ .../quantifiers/theory_quantifiers_type_rules.h | 15 +++++++++++++++ src/theory/quantifiers_engine.cpp | 4 ++-- src/theory/quantifiers_engine.h | 2 +- 8 files changed, 46 insertions(+), 7 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 81e93ebe6..e536ed7cc 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2002,6 +2002,8 @@ builtinOp[CVC4::Kind& kind] | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } + | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; } + | FP_TOK { $kind = CVC4::kind::FLOATINGPOINT_FP; } | FP_EQ_TOK { $kind = CVC4::kind::FLOATINGPOINT_EQ; } | FP_ABS_TOK { $kind = CVC4::kind::FLOATINGPOINT_ABS; } @@ -2470,6 +2472,8 @@ DTSIZE_TOK : 'dt.size'; FMFCARD_TOK : 'fmf.card'; +INST_CLOSURE_TOK : 'inst-closure'; + EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; // Other set theory operators are not // tokenized and handled directly when diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index a8774440e..793e4a611 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -44,6 +44,8 @@ sort INST_PATTERN_LIST_TYPE \ # a list of instantiation patterns operator INST_PATTERN_LIST 1: "a list of instantiation patterns" +operator INST_CLOSURE 1 "predicate for specifying term in instantiation closure." + typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule @@ -51,6 +53,7 @@ typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule +typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule # for rewrite rules # types... diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index bb0b3248d..69271e021 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -111,7 +111,7 @@ Node TermDb::getOperator( Node n ) { } } -void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ +void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){ //don't add terms in quantifier bodies if( withinQuant && !options::registerQuantBodyTerms() ){ return; @@ -152,9 +152,13 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } rec = true; } + if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){ + d_iclosure_processed.insert( n ); + rec = true; + } if( rec ){ for( size_t i=0; ifirst << std::endl; for( unsigned i=0; isecond.size(); i++ ){ Node n = it->second[i]; - if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ + //to be added to term index, term must be relevant, and either exist in EE or be an inst closure term + if( hasTermCurrent( n ) && ( ee->hasTerm( n ) || d_iclosure_processed.find( n )!=d_iclosure_processed.end() ) ){ if( !n.getAttribute(NoMatchAttribute()) ){ if( options::finiteModelFind() ){ computeModelBasisArgAttribute( n ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index fca2e1261..f841bb2d8 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -127,6 +127,8 @@ private: QuantifiersEngine* d_quantEngine; /** terms processed */ std::hash_set< Node, NodeHashFunction > d_processed; + /** terms processed */ + std::hash_set< Node, NodeHashFunction > d_iclosure_processed; private: /** select op map */ std::map< Node, std::map< TypeNode, Node > > d_par_op_map; @@ -158,7 +160,7 @@ public: /** map from type nodes to terms of that type */ std::map< TypeNode, std::vector< Node > > d_type_map; /** add a term to the database */ - void addTerm( Node n, std::set< Node >& added, bool withinQuant = false ); + void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false ); /** reset (calculate which terms are active) */ void reset( Theory::Effort effort ); /** get operator*/ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 89549a71b..12edaa31c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -129,12 +129,22 @@ void TheoryQuantifiers::check(Effort e) { case kind::FORALL: assertUniversal( assertion ); break; + case kind::INST_CLOSURE: + getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); + break; + case kind::EQUAL: + //do nothing + break; case kind::NOT: { switch( assertion[0].getKind()) { case kind::FORALL: assertExistential( assertion ); break; + case kind::EQUAL: + //do nothing + break; + case kind::INST_CLOSURE: default: Unhandled(assertion[0].getKind()); break; diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 2d5cce6ed..3ce0250fe 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -125,6 +125,21 @@ struct QuantifierInstPatternListTypeRule { } };/* struct QuantifierInstPatternListTypeRule */ +struct QuantifierInstClosureTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::INST_CLOSURE ); + if( check ){ + TypeNode tn = n[0].getType(check); + if( tn.isBoolean() ){ + throw TypeCheckingExceptionPrivate(n, "argument of inst-closure must be non-boolean"); + } + } + return nodeManager->booleanType(); + } +};/* struct QuantifierInstClosureTypeRule */ + + class RewriteRuleTypeRule { public: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 3ef5b4a65..52b4fd17d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -497,9 +497,9 @@ Node QuantifiersEngine::getNextDecisionRequest(){ return Node::null(); } -void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ +void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){ std::set< Node > added; - getTermDatabase()->addTerm( n, added, withinQuant ); + getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure ); //maybe have triggered instantiations if we are doing eager instantiation if( options::eagerInstQuant() ){ flushLemmas(); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 2fc479f4c..14e26f2b6 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -297,7 +297,7 @@ public: /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ - void addTermToDatabase( Node n, bool withinQuant = false ); + void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** get the master equality engine */ eq::EqualityEngine* getMasterEqualityEngine() ; /** debug print equality engine */ -- 2.30.2