From 32b0aba2c2c27ad038d34c8554a4bae76e8dd363 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 21 Nov 2014 09:42:07 +0100 Subject: Change default option to --inst-when=full-last-call (interleave instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs. --- src/smt/smt_engine.cpp | 9 ++++++++- src/theory/quantifiers/options | 6 +++--- src/theory/quantifiers/options_handlers.h | 10 +++++----- src/theory/quantifiers/quantifiers_rewriter.cpp | 24 ++++++++++++++++++++---- test/regress/regress0/quantifiers/burns4.smt2 | 2 ++ 5 files changed, 38 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 86b0faaf6..74cdee0b7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1319,7 +1319,6 @@ void SmtEngine::setDefaults() { if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); } - //for finite model finding if( ! options::instWhenMode.wasSetByUser()){ //instantiate only on last call if( options::eMatching() ){ @@ -1327,6 +1326,14 @@ void SmtEngine::setDefaults() { options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } + if( options::mbqiMode()==quantifiers::MBQI_ABS ){ + if( !options::preSkolemQuant.wasSetByUser() ){ + options::preSkolemQuant.set( true ); + } + if( !options::fmfOneInstPerRound.wasSetByUser() ){ + options::fmfOneInstPerRound.set( true ); + } + } } //implied options... diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index dad173ff5..a428633cc 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -41,7 +41,7 @@ option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true option cnfQuant --cnf-quant bool :default false apply CNF conversion to quantified formulas # Whether to NNF quantifier bodies -option nnfQuant --nnf-quant bool :default false +option nnfQuant --nnf-quant bool :default true apply NNF conversion to quantified formulas option clauseSplit --clause-split bool :default false @@ -88,7 +88,7 @@ option fmfFunWellDefined --fmf-fun bool :default false option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching -option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) @@ -127,7 +127,7 @@ option finiteModelFind finite-model-find --finite-model-find bool :default false option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" choose mode for model-based quantifier instantiation -option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false +option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false only add one instantiation per quantifier per round for mbqi option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false only add instantiations for one quantifier per round for mbqi diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 08fcf319d..e9f85d454 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -29,17 +29,17 @@ namespace quantifiers { static const std::string instWhenHelp = "\ Modes currently supported by the --inst-when option:\n\ \n\ -full (default)\n\ +full-last-call (default)\n\ ++ Alternate running instantiation rounds at full effort and last\n\ + call. In other words, interleave instantiation and theory combination.\n\ +\n\ +full\n\ + Run instantiation round at full effort, before theory combination.\n\ \n\ full-delay \n\ + Run instantiation round at full effort, before theory combination, after\n\ all other theories have finished.\n\ \n\ -full-last-call\n\ -+ Alternate running instantiation rounds at full effort and last\n\ - call. In other words, interleave instantiation and theory combination.\n\ -\n\ last-call\n\ + Run instantiation at last call effort, after theory combination and\n\ and theories report sat.\n\ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0ed175393..1e6ec3a02 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -309,11 +309,19 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else{ std::vector< Node > children; Kind k = body[0].getKind(); + if( body[0].getKind()==OR || body[0].getKind()==AND ){ + k = body[0].getKind()==AND ? OR : AND; for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - children.push_back( computeNNF( body[0][i].notNode() ) ); + Node nc = computeNNF( body[0][i].notNode() ); + if( nc.getKind()==k ){ + for( unsigned j=0; j children; bool childrenChanged = false; + bool isAssoc = body.getKind()==AND || body.getKind()==OR; for( int i=0; i<(int)body.getNumChildren(); i++ ){ Node nc = computeNNF( body[i] ); - children.push_back( nc ); - childrenChanged = childrenChanged || nc!=body[i]; + if( isAssoc && nc.getKind()==body.getKind() ){ + for( unsigned j=0; jmkNode( body.getKind(), children ); diff --git a/test/regress/regress0/quantifiers/burns4.smt2 b/test/regress/regress0/quantifiers/burns4.smt2 index 886d6f5c8..72023fd4f 100644 --- a/test/regress/regress0/quantifiers/burns4.smt2 +++ b/test/regress/regress0/quantifiers/burns4.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat (set-logic AUFLIA) (set-info :source | Burns mutual exclusion protocol. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo de Moura |) (set-info :smt-lib-version 2.0) -- cgit v1.2.3 From 5b09650edeac065f816247b5f88571ea72e79c3f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 21 Nov 2014 10:48:17 +0100 Subject: Throw error when pattern is not list of terms. --- .../quantifiers/theory_quantifiers_type_rules.h | 6 ++++++ .../quantifiers/stream-x2014-09-18-unsat.smt2 | 24 +++++++++++----------- 2 files changed, 18 insertions(+), 12 deletions(-) diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 5d86c29c0..e44712412 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -84,6 +84,12 @@ struct QuantifierInstPatternTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate) { Assert(n.getKind() == kind::INST_PATTERN ); + if( check ){ + TypeNode tn = n[0].getType(check); + if( tn.isFunction() ){ + throw TypeCheckingExceptionPrivate(n[0], "Pattern must be a list of fully-applied terms."); + } + } return nodeManager->instPatternType(); } };/* struct QuantifierInstPatternTypeRule */ diff --git a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 index 5f20cb3b5..615d43fe8 100644 --- a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 +++ b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 @@ -112,18 +112,18 @@ (assert (! (= (smap$f id$e) id$b) :named a12)) (assert (! (= (smap$a id$) id$e) :named a13)) (assert (! (= (smap$b id$a) id$d) :named a14)) -(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern (fun_app$j id$b ?v0))) :named a15)) -(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern (fun_app$i id$c ?v0))) :named a16)) -(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern (fun_app$e id$d ?v0))) :named a17)) -(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern (fun_app$c id$e ?v0))) :named a18)) -(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern (fun_app$d id$ ?v0))) :named a19)) -(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern (fun_app$f id$a ?v0))) :named a20)) -(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern (fun_app$j id$b ?v0))) :named a21)) -(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern (fun_app$i id$c ?v0))) :named a22)) -(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern (fun_app$e id$d ?v0))) :named a23)) -(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern (fun_app$c id$e ?v0))) :named a24)) -(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern (fun_app$d id$ ?v0))) :named a25)) -(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern (fun_app$f id$a ?v0))) :named a26)) +(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern ((fun_app$j id$b ?v0)))) :named a15)) +(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern ((fun_app$i id$c ?v0)))) :named a16)) +(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern ((fun_app$e id$d ?v0)))) :named a17)) +(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern ((fun_app$c id$e ?v0)))) :named a18)) +(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern ((fun_app$d id$ ?v0)))) :named a19)) +(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern ((fun_app$f id$a ?v0)))) :named a20)) +(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern ((fun_app$j id$b ?v0)))) :named a21)) +(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern ((fun_app$i id$c ?v0)))) :named a22)) +(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern ((fun_app$e id$d ?v0)))) :named a23)) +(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern ((fun_app$c id$e ?v0)))) :named a24)) +(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern ((fun_app$d id$ ?v0)))) :named a25)) +(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern ((fun_app$f id$a ?v0)))) :named a26)) (assert (! (forall ((?v0 B_b_stream_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$ (smap$g ?v0 ?v1) ?v2) (fun_app$ ?v0 (snth$a ?v1 ?v2)))) :named a27)) (assert (! (forall ((?v0 B_a_stream_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$b (smap$h ?v0 ?v1) ?v2) (fun_app$k ?v0 (snth$a ?v1 ?v2)))) :named a28)) (assert (! (forall ((?v0 A_b_stream_fun$) (?v1 A_stream$) (?v2 Nat$)) (= (snth$ (smap$i ?v0 ?v1) ?v2) (fun_app$l ?v0 (snth$c ?v1 ?v2)))) :named a29)) -- cgit v1.2.3 From 38e077ab219082ee044c2e17ed809e3519c80842 Mon Sep 17 00:00:00 2001 From: lianah Date: Sat, 22 Nov 2014 10:11:19 -0800 Subject: added number of resource units used as a stat --- src/smt/smt_engine.cpp | 9 +++++++-- src/util/resource_manager.cpp | 2 +- src/util/resource_manager.h | 2 +- 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 74cdee0b7..8f5ba2024 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -209,6 +209,8 @@ struct SmtEngineStatistics { /** Has something simplified to false? */ IntStat d_simplifiedToFalse; + /** Number of resource units spent. */ + ReferenceStat d_resourceUnitsUsed; SmtEngineStatistics() : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), @@ -231,7 +233,8 @@ struct SmtEngineStatistics { d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), - d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) + d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0), + d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed") { StatisticsRegistry::registerStat(&d_definitionExpansionTime); @@ -255,6 +258,7 @@ struct SmtEngineStatistics { StatisticsRegistry::registerStat(&d_pushPopTime); StatisticsRegistry::registerStat(&d_processAssertionsTime); StatisticsRegistry::registerStat(&d_simplifiedToFalse); + StatisticsRegistry::registerStat(&d_resourceUnitsUsed); } ~SmtEngineStatistics() { @@ -279,6 +283,7 @@ struct SmtEngineStatistics { StatisticsRegistry::unregisterStat(&d_pushPopTime); StatisticsRegistry::unregisterStat(&d_processAssertionsTime); StatisticsRegistry::unregisterStat(&d_simplifiedToFalse); + StatisticsRegistry::unregisterStat(&d_resourceUnitsUsed); } };/* struct SmtEngineStatistics */ @@ -708,7 +713,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_private = new smt::SmtEnginePrivate(*this); d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); - + d_stats->d_resourceUnitsUsed.setData(d_private->getResourceManager()->d_cumulativeResourceUsed); // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast(d_logic)); diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index b0fd37fd2..7aeb2fc0f 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -172,10 +172,10 @@ unsigned long ResourceManager::getTimeRemaining() const { void ResourceManager::spendResource() throw (UnsafeInterruptException) { ++d_spendResourceCalls; + ++d_cumulativeResourceUsed; if (!d_on) return; Debug("limit") << "ResourceManager::spendResource()" << std::endl; - ++d_cumulativeResourceUsed; ++d_thisCallResourceUsed; if(out()) { Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index a16f60910..94e7dbba2 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -150,7 +150,7 @@ public: void endCall(); static unsigned long getFrequencyCount() { return s_resourceCount; } - + friend class SmtEngine; };/* class ResourceManager */ }/* CVC4 namespace */ -- cgit v1.2.3 From 29bdfca306a7cd35801c7d9cb3023d78a8b82a1f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 25 Nov 2014 16:15:10 +0100 Subject: Fix bug in --term-db-mode=relevant with variable triggers. Support inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers. --- src/parser/smt2/Smt2.g | 4 + src/theory/quantifiers/candidate_generator.cpp | 9 ++- src/theory/quantifiers/ce_guided_instantiation.cpp | 4 +- src/theory/quantifiers/kinds | 3 + src/theory/quantifiers/options | 2 + src/theory/quantifiers/term_database.cpp | 86 ++++++++++++++++------ src/theory/quantifiers/term_database.h | 8 +- src/theory/quantifiers/theory_quantifiers.cpp | 33 ++++----- src/theory/quantifiers/theory_quantifiers.h | 7 +- .../quantifiers/theory_quantifiers_type_rules.h | 14 ++++ src/theory/quantifiers_engine.cpp | 4 +- src/theory/quantifiers_engine.h | 2 +- 12 files changed, 122 insertions(+), 54 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index bdad45606..511b67997 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1620,6 +1620,8 @@ builtinOp[CVC4::Kind& kind] | DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; } | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } + + | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; } // NOTE: Theory operators go here ; @@ -2026,6 +2028,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/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index cfaa6d1ad..9e3fed20a 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -197,16 +197,17 @@ void CandidateGeneratorQEAll::reset( Node eqc ) { Node CandidateGeneratorQEAll::getNextCandidate() { while( !d_eq.isFinished() ){ - Node n = (*d_eq); + TNode n = (*d_eq); ++d_eq; if( n.getType().isSubtypeOf( d_match_pattern_type ) ){ - if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ + TNode nh = d_qe->getTermDatabase()->getHasTermEqc( n ); + if( !nh.isNull() ){ if( options::instMaxLevel()!=-1 ){ - n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index ); + nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index ); } d_firstTime = false; //an equivalence class with the same type as the pattern, return it - return n; + return nh; } } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index ffe64beba..bf9409f06 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -248,7 +248,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { for( unsigned i=0; id_candidates.size(); i++ ){ Node t = getModelTerm( conj->d_candidates[i] ); model_terms.push_back( t ); - Trace("cegqi-engine") << t << " "; + Trace("cegqi-engine") << conj->d_candidates[i] << " -> " << t << " "; } Trace("cegqi-engine") << std::endl; d_quantEngine->addInstantiation( q, model_terms, false ); @@ -279,7 +279,7 @@ bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node for( unsigned i=0; i " << nv << " "; if( nv.isNull() ){ success = false; } 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/options b/src/theory/quantifiers/options index a428633cc..cac78af46 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -196,5 +196,7 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo option localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions +option termDbInstClosure --term-db-inst-closure bool :default false + only consider inst closure terms for E-matching endmodule diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a95de086a..34c40c8c4 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -111,13 +111,17 @@ 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; } + bool rec = false; if( d_processed.find( n )==d_processed.end() ){ d_processed.insert(n); + if( withinInstClosure ){ + d_iclosure_processed.insert( n ); + } d_type_map[ n.getType() ].push_back( n ); //if this is an atomic trigger, consider adding it //Call the children? @@ -137,9 +141,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ d_op_map[op].push_back( n ); added.insert( n ); - for( size_t i=0; i& added, bool withinQuant ){ } } } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - addTerm( n[i], added, withinQuant ); - } + } + rec = true; + }else 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; i& subs, bool subsRep, } bool TermDb::hasTermCurrent( Node n ) { - //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); - if( options::termDbMode()==TERM_DB_ALL ){ - return true; - }else if( options::termDbMode()==TERM_DB_RELEVANT ){ - return d_has_map.find( n )!=d_has_map.end(); - }else{ - Assert( false ); + if( options::termDbInstClosure() && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){ return false; + }else{ + //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE + if( options::termDbMode()==TERM_DB_ALL ){ + return true; + }else if( options::termDbMode()==TERM_DB_RELEVANT ){ + return d_has_map.find( n )!=d_has_map.end(); + }else{ + Assert( false ); + return false; + } } } -void TermDb::setHasTerm( Node n ) { - if( inst::Trigger::isAtomicTrigger( n ) ){ - if( d_has_map.find( n )==d_has_map.end() ){ - d_has_map[n] = true; - for( unsigned i=0; i::iterator it = d_has_eqc.find( r ); + if( it==d_has_eqc.end() ){ + Node h; + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( h.isNull() && !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + ++eqc_i; + if( hasTermCurrent( n ) ){ + h = n; + } + } + d_has_eqc[r] = h; + return h; + }else{ + return it->second; } + }else{ + //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc + return Node::null(); + } + } +} + +void TermDb::setHasTerm( Node n ) { + //if( inst::Trigger::isAtomicTrigger( n ) ){ + if( d_has_map.find( n )==d_has_map.end() ){ + d_has_map[n] = true; + for( unsigned i=0; igetMasterEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); while( !eqcs_i.isFinished() ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 2b151bb04..cb9f5eeef 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -123,6 +123,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; @@ -144,6 +146,8 @@ public: std::map< Node, std::vector< Node > > d_op_map; /** has map */ std::map< Node, bool > d_has_map; + /** map from reps to a term in eqc in d_has_map */ + std::map< Node, Node > d_has_eqc; /** map from APPLY_UF functions to trie */ std::map< Node, TermArgTrie > d_func_map_trie; std::map< Node, TermArgTrie > d_func_map_eqc_trie; @@ -152,7 +156,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*/ @@ -176,6 +180,8 @@ public: bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); /** has term */ bool hasTermCurrent( Node n ); + /** get has term eqc */ + Node getHasTermEqc( Node r ); //for model basis private: diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 5c68e52a7..de0f98af6 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -35,7 +35,6 @@ using namespace CVC4::theory::quantifiers; TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo), - d_numRestarts(0), d_masterEqualityEngine(0) { d_numInstantiations = 0; @@ -97,6 +96,10 @@ Node TheoryQuantifiers::getValue(TNode n) { } } +void TheoryQuantifiers::computeCareGraph() { + //do nothing +} + void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) { if(fullModel) { for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { @@ -126,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: //cannot negate inst closure default: Unhandled(assertion[0].getKind()); break; @@ -182,23 +195,7 @@ bool TheoryQuantifiers::flipDecision(){ //}else{ // return false; //} - - if( !d_out->flipDecision() ){ - return restart(); - } - return true; -} - -bool TheoryQuantifiers::restart(){ - static const int restartLimit = 0; - if( d_numRestarts==restartLimit ){ - Debug("quantifiers-flip") << "No more restarts." << std::endl; - return false; - }else{ - d_numRestarts++; - Debug("quantifiers-flip") << "Do restart." << std::endl; - return true; - } + return false; } void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector node_values, std::string str_value){ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index aace13b24..6d3fa4d46 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -44,17 +44,15 @@ private: /** number of instantiations */ int d_numInstantiations; int d_baseDecLevel; - /** number of restarts */ - int d_numRestarts; eq::EqualityEngine* d_masterEqualityEngine; - +private: + void computeCareGraph(); public: TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryQuantifiers(); void setMasterEqualityEngine(eq::EqualityEngine* eq); - void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void preRegisterTerm(TNode n); @@ -73,7 +71,6 @@ public: private: void assertUniversal( Node n ); void assertExistential( Node n ); - bool restart(); };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index e44712412..341e656c7 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -126,6 +126,20 @@ 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 04b6c5d16..4dc8df09d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -472,9 +472,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 199fe79b9..2b466b96b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -290,7 +290,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 */ -- cgit v1.2.3 From 435e694d3bc594cf1cb6912823f064a66766854e Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 26 Nov 2014 18:11:35 -0600 Subject: add more functions for regular expressions --- src/theory/strings/regexp_operation.cpp | 109 +++++++++- src/theory/strings/regexp_operation.h | 2 + src/theory/strings/theory_strings.cpp | 352 ++++++++++++++++++++++++++++++-- src/theory/strings/theory_strings.h | 20 +- 4 files changed, 468 insertions(+), 15 deletions(-) diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 69b089c84..2752886cf 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1653,8 +1653,115 @@ void RegExpOpr::splitRegExp(Node r, std::vector< PairNodes > &pset) { } } +void RegExpOpr::flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec) { + Assert(false); + Assert(checkConstRegExp(r)); + switch( r.getKind() ) { + case kind::REGEXP_EMPTY: { + //TODO + break; + } + case kind::REGEXP_SIGMA: { + CVC4::String s("a"); + std::pair< CVC4::String, unsigned > tmp(s, 0); + //TODO + break; + } + case kind::STRING_TO_REGEXP: { + Assert(r[0].isConst()); + CVC4::String s = r[0].getConst< CVC4::String >(); + std::pair< CVC4::String, unsigned > tmp(s, 0); + //TODO + break; + } + case kind::REGEXP_CONCAT: { + for(unsigned i=0; i &vec_or) { + switch(r.getKind()) { + case kind::REGEXP_EMPTY: { + vec_or.push_back(r); + break; + } + case kind::REGEXP_SIGMA: { + vec_or.push_back(r); + break; + } + case kind::STRING_TO_REGEXP: { + vec_or.push_back(r); + break; + } + case kind::REGEXP_CONCAT: { + disjunctRegExp(r[0], vec_or); + for(unsigned i=1; i vec_con; + disjunctRegExp(r[i], vec_con); + std::vector vec_or2; + for(unsigned k1=0; k1mkNode(kind::REGEXP_CONCAT, vec_or[k1], vec_con[k2]) ); + if(std::find(vec_or2.begin(), vec_or2.end(), tmp) == vec_or2.end()) { + vec_or2.push_back( tmp ); + } + } + } + vec_or = vec_or2; + } + break; + } + case kind::REGEXP_UNION: { + for(unsigned i=0; i vec_or2; + disjunctRegExp(r[i], vec_or2); + vec_or.insert(vec_or.end(), vec_or2.begin(), vec_or2.end()); + } + break; + } + case kind::REGEXP_INTER: { + Assert(checkConstRegExp(r)); + Node rtmp = r[0]; + bool spflag = false; + for(unsigned i=1; i().toString() ; return s == "" ? "{E}" : ( s == " " ? "{ }" : s.size()>1? "("+s+")" : s ); diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index ce3093528..6a31a23fb 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -96,6 +96,8 @@ public: Node intersect(Node r1, Node r2, bool &spflag); Node complement(Node r, int &ret); void splitRegExp(Node r, std::vector< PairNodes > &pset); + void flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec); + void disjunctRegExp(Node r, std::vector &vec_or); std::string mkString( Node r ); }; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e8bf87a17..782a68e18 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -56,9 +56,11 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_regexp_memberships(c), d_regexp_ucached(u), d_regexp_ccached(c), - d_str_re_map(c), + d_pos_memberships(c), + d_neg_memberships(c), d_inter_cache(c), d_inter_index(c), + d_processed_memberships(c), d_regexp_ant(c), d_input_vars(u), d_input_var_lsum(u), @@ -483,8 +485,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { if( n.getKind() == kind::VARIABLE && options::stringFMF() ) { d_input_vars.insert(n); } - } - if (n.getType().isBoolean()) { + } else if (n.getType().isBoolean()) { // Get triggered for both equal and dis-equal d_equalityEngine.addTriggerPredicate(n); } else { @@ -2502,6 +2503,318 @@ Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) { } } +Node TheoryStrings::normalizeRegexp(Node r) { + Node nf_r = r; + if(d_nf_regexps.find(r) != d_nf_regexps.end()) { + nf_r = d_nf_regexps[r]; + } else { + std::vector< Node > nf_exp; + if(!d_regexp_opr.checkConstRegExp(r)) { + switch( r.getKind() ) { + case kind::REGEXP_EMPTY: + case kind::REGEXP_SIGMA: { + break; + } + case kind::STRING_TO_REGEXP: { + if(r[0].isConst()) { + break; + } else { + if(d_normal_forms.find( r[0] ) != d_normal_forms.end()) { + nf_r = mkConcat( d_normal_forms[r[0]] ); + Debug("regexp-nf") << "Term: " << r[0] << " has a normal form " << nf_r << std::endl; + nf_exp.insert(nf_exp.end(), d_normal_forms_exp[r[0]].begin(), d_normal_forms_exp[r[0]].end()); + nf_r = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, nf_r) ); + } + } + } + case kind::REGEXP_CONCAT: + case kind::REGEXP_UNION: + case kind::REGEXP_INTER: { + bool flag = false; + std::vector< Node > vec_nodes; + for(unsigned i=0; imkNode(r.getKind(), vec_nodes); + nf_r = Rewriter::rewrite( rtmp ); + } + } + case kind::REGEXP_STAR: { + Node rtmp = normalizeRegexp(r[0]); + if(rtmp != r[0]) { + rtmp = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, rtmp); + nf_r = Rewriter::rewrite( rtmp ); + } + } + default: { + Unreachable(); + } + } + } + d_nf_regexps[r] = nf_r; + d_nf_regexps_exp[r] = nf_exp; + } + return nf_r; +} + +bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps) { + std::map< Node, std::vector< Node > > unprocessed_x_exps; + std::map< Node, std::vector< Node > > unprocessed_memberships; + std::map< Node, std::vector< Node > > unprocessed_memberships_bases; + bool addLemma = false; + + Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl; + + for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); + itr_xr != d_pos_memberships.end(); ++itr_xr ) { + Node x = (*itr_xr).first; + NodeList* lst = (*itr_xr).second; + Node nf_x = x; + std::vector< Node > nf_x_exp; + if(d_normal_forms.find( x ) != d_normal_forms.end()) { + //nf_x = mkConcat( d_normal_forms[x] ); + nf_x_exp.insert(nf_x_exp.end(), d_normal_forms_exp[x].begin(), d_normal_forms_exp[x].end()); + //Debug("regexp-nf") << "Term: " << x << " has a normal form " << ret << std::endl; + } else { + Assert(false); + } + Trace("regexp-nf") << "Checking Memberships for N(" << x << ") = " << nf_x << " :" << std::endl; + + std::vector< Node > vec_x; + std::vector< Node > vec_r; + for(NodeList::const_iterator itr_lst = lst->begin(); + itr_lst != lst->end(); ++itr_lst) { + Node r = *itr_lst; + Node nf_r = normalizeRegexp((*lst)[0]); + Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, nf_r); + if(d_processed_memberships.find(memb) == d_processed_memberships.end()) { + if(d_regexp_opr.checkConstRegExp(nf_r)) { + vec_x.push_back(x); + vec_r.push_back(r); + } else { + Trace("regexp-nf") << "Handling Symbolic Regexp for N(" << r << ") = " << nf_r << std::endl; + //TODO: handle symbolic ones + addLemma = true; + } + d_processed_memberships.insert(memb); + } + } + if(!vec_x.empty()) { + if(unprocessed_x_exps.find(nf_x) == unprocessed_x_exps.end()) { + unprocessed_x_exps[nf_x] = nf_x_exp; + unprocessed_memberships[nf_x] = vec_r; + unprocessed_memberships_bases[nf_x] = vec_x; + } else { + unprocessed_x_exps[nf_x].insert(unprocessed_x_exps[nf_x].end(), nf_x_exp.begin(), nf_x_exp.end()); + unprocessed_memberships[nf_x].insert(unprocessed_memberships[nf_x].end(), vec_r.begin(), vec_r.end()); + unprocessed_memberships_bases[nf_x].insert(unprocessed_memberships_bases[nf_x].end(), vec_x.begin(), vec_x.end()); + } + } + } + //Intersection + for(std::map< Node, std::vector< Node > >::const_iterator itr = unprocessed_memberships.begin(); + itr != unprocessed_memberships.end(); ++itr) { + Node nf_x = itr->first; + std::vector< Node > exp( unprocessed_x_exps[nf_x] ); + Node r = itr->second[0]; + //get nf_r + Node inter_r = d_nf_regexps[r]; + exp.insert(exp.end(), d_nf_regexps_exp[r].begin(), d_nf_regexps_exp[r].end()); + Node x = unprocessed_memberships_bases[itr->first][0]; + Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r); + exp.push_back(memb); + for(std::size_t i=1; i < itr->second.size(); i++) { + //exps + Node r2 = itr->second[i]; + Node inter_r2 = d_nf_regexps[r2]; + exp.insert(exp.end(), d_nf_regexps_exp[r2].begin(), d_nf_regexps_exp[r2].end()); + Node x2 = unprocessed_memberships_bases[itr->first][i]; + memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x2, r2); + exp.push_back(memb); + //intersection + bool spflag = false; + inter_r = d_regexp_opr.intersect(inter_r, inter_r2, spflag); + if(inter_r == d_emptyRegexp) { + //conflict + Node antec = exp.size() == 1? exp[0] : NodeManager::currentNM()->mkNode(kind::AND, exp); + Node conc; + sendLemma(antec, conc, "INTERSEC CONFLICT"); + addLemma = true; + break; + } + } + //infer + if(!d_conflict) { + memb = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, inter_r) ); + memb_with_exps[memb] = exp; + } else { + break; + } + } + + return addLemma; +} + +bool TheoryStrings::applyRConsume( CVC4::String &s, Node &r) { + Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s << ", r= " << r << std::endl; + Assert( d_regexp_opr.checkConstRegExp(r) ); + + if( !s.isEmptyString() ) { + Node dc = r; + + for(unsigned i=0; i > vec_can; + d_regexp_opr.splitRegExp(r, vec_can); + //TODO: lazy cache or eager? + std::vector< Node > vec_or; + + for(unsigned int i=0; imkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first); + Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second); + Node c = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, m1, m2) ); + vec_or.push_back( c ); + } + Node conc = vec_or.size()==0? Node::null() : vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) ); + return conc; +} + +bool TheoryStrings::applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps) { + if(XinR_with_exps.size() > 0) { + //TODO: get vector, var, store. + return true; + } else { + return false; + } +} + +bool TheoryStrings::checkMembershipsWithoutLength( + std::map< Node, std::vector< Node > > &memb_with_exps, + std::map< Node, std::vector< Node > > &XinR_with_exps) { + for(std::map< Node, std::vector< Node > >::const_iterator itr = memb_with_exps.begin(); + itr != memb_with_exps.end(); ++itr) { + Node memb = itr->first; + Node s = memb[0]; + Node r = memb[1]; + if(s.isConst()) { + memb = Rewriter::rewrite( memb ); + if(memb == d_false) { + Node antec = itr->second.size() == 1? itr->second[0] : NodeManager::currentNM()->mkNode(kind::AND, itr->second); + Node conc; + sendLemma(antec, conc, "MEMBERSHIP CONFLICT"); + //addLemma = true; + return true; + } else { + Assert(memb == d_true); + } + } else if(s.getKind() == kind::VARIABLE) { + //add to XinR + XinR_with_exps[itr->first] = itr->second; + } else { + Assert(s.getKind() == kind::STRING_CONCAT); + Node antec = itr->second.size() == 1? itr->second[0] : NodeManager::currentNM()->mkNode(kind::AND, itr->second); + Node conc; + for( unsigned i=0; i() ); + //R-Consume, see Tianyi's thesis + if(!applyRConsume(str, r)) { + sendLemma(antec, conc, "R-Consume CONFLICT"); + //addLemma = true; + return true; + } + } else { + //R-Split, see Tianyi's thesis + if(i == s.getNumChildren() - 1) { + //add to XinR + Node memb2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s[i], r); + XinR_with_exps[itr->first] = itr->second; + } else { + Node s1 = s[i]; + std::vector< Node > vec_s2; + for( unsigned j=i+1; j > memb_with_exps; + std::map< Node, std::vector< Node > > XinR_with_exps; + + addedLemma = normalizePosMemberships( memb_with_exps ); + if(!d_conflict) { + // main procedure + addedLemma |= checkMembershipsWithoutLength( memb_with_exps, XinR_with_exps ); + //TODO: check addlemma + if (!addedLemma && !d_conflict) { + for(std::map< Node, std::vector< Node > >::const_iterator itr = XinR_with_exps.begin(); + itr != XinR_with_exps.end(); ++itr) { + std::vector vec_or; + d_regexp_opr.disjunctRegExp( itr->first, vec_or ); + Node tmp = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_or); + Trace("regexp-process") << "Got r: " << itr->first << " to " << tmp << std::endl; + /* + if(r.getKind() == kind::REGEXP_STAR) { + //TODO: apply R-Len + addedLemma = applyRLen(XinR_with_exps); + } else { + //TODO: split + } + */ + } + Assert(false); //TODO:tmp + } + } + + return addedLemma; +} + bool TheoryStrings::checkMemberships() { bool addedLemma = false; bool changed = false; @@ -2511,8 +2824,8 @@ bool TheoryStrings::checkMemberships() { Trace("regexp-debug") << "Checking Memberships ... " << std::endl; //if(options::stringEIT()) { //TODO: Opt for normal forms - for(NodeListMap::const_iterator itr_xr = d_str_re_map.begin(); - itr_xr != d_str_re_map.end(); ++itr_xr ) { + for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); + itr_xr != d_pos_memberships.end(); ++itr_xr ) { bool spflag = false; Node x = (*itr_xr).first; NodeList* lst = (*itr_xr).second; @@ -3120,11 +3433,11 @@ void TheoryStrings::addMembership(Node assertion) { Node r = atom[1]; if(polarity) { NodeList* lst; - NodeListMap::iterator itr_xr = d_str_re_map.find( x ); - if( itr_xr == d_str_re_map.end() ){ + NodeListMap::iterator itr_xr = d_pos_memberships.find( x ); + if( itr_xr == d_pos_memberships.end() ){ lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_str_re_map.insertDataFromContextMemory( x, lst ); + d_pos_memberships.insertDataFromContextMemory( x, lst ); } else { lst = (*itr_xr).second; } @@ -3135,16 +3448,29 @@ void TheoryStrings::addMembership(Node assertion) { } } lst->push_back( r ); - }/* else { - if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { + } else { + /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { int rt; Node r2 = d_regexp_opr.complement(r, rt); Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2); - d_regexp_memberships.push_back( a ); + }*/ + NodeList* lst; + NodeListMap::iterator itr_xr = d_neg_memberships.find( x ); + if( itr_xr == d_neg_memberships.end() ){ + lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator(getSatContext()->getCMM()) ); + d_neg_memberships.insertDataFromContextMemory( x, lst ); } else { - d_regexp_memberships.push_back( assertion ); + lst = (*itr_xr).second; } - }*/ + //check + for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { + if( r == *itr ) { + return; + } + } + lst->push_back( r ); + } d_regexp_memberships.push_back( assertion ); } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 95eba27bc..06c95a476 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -246,7 +246,18 @@ private: bool checkLengthsEqc(); bool checkCardinality(); bool checkInductiveEquations(); + //check membership constraints + Node normalizeRegexp(Node r); + bool normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps); + bool applyRConsume( CVC4::String &s, Node &r); + Node applyRSplit(Node s1, Node s2, Node r); + bool applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps); + bool checkMembershipsWithoutLength( + std::map< Node, std::vector< Node > > &memb_with_exps, + std::map< Node, std::vector< Node > > &XinR_with_exps); bool checkMemberships(); + //temp + bool checkMemberships2(); bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &processed, std::vector< Node > &cprocessed, std::vector< Node > &nf_exp); @@ -325,10 +336,17 @@ private: NodeList d_regexp_memberships; NodeSet d_regexp_ucached; NodeSet d_regexp_ccached; + // stored assertions + NodeListMap d_pos_memberships; + NodeListMap d_neg_memberships; + // semi normal forms for symbolic expression + std::map< Node, Node > d_nf_regexps; + std::map< Node, std::vector< Node > > d_nf_regexps_exp; // intersection - NodeListMap d_str_re_map; NodeNodeMap d_inter_cache; NodeIntMap d_inter_index; + // processed memberships + NodeSet d_processed_memberships; // antecedant for why regexp membership must be true NodeNodeMap d_regexp_ant; // membership length -- cgit v1.2.3 From 0e7313581342ee70133a673ae515e22824c57597 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 26 Nov 2014 19:32:32 -0600 Subject: add more regexp rewriting --- src/theory/strings/regexp_operation.cpp | 12 +++++++----- src/theory/strings/theory_strings_rewriter.cpp | 10 ++++++++-- 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 2752886cf..da8410a94 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1157,9 +1157,10 @@ void RegExpOpr::getCharSet( Node r, std::set &pcset, SetNodes &pvset ) } case kind::REGEXP_INTER: { //TODO: Overapproximation for now - for(unsigned i=0; i::const_iterator itrcache = cache.find(p); @@ -1459,7 +1460,6 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node PairNodes p(r1, r2); cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt))); Node rt = intersectInternal2(r1l, r2l, cache2, spflag, cnt+1); - rt = convert1(cnt, rt); if(spflag) { //TODO: return Node::null(); @@ -1471,6 +1471,8 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes); rNode = Rewriter::rewrite( rNode ); + rNode = convert1(cnt, rNode); + rNode = Rewriter::rewrite( rNode ); } else { //TODO: non-empty var set spflag = true; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index c952a7b3c..99a062f20 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -100,7 +100,7 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { if(!preNode.isNull()) { if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) { preNode = rewriteConcatString( - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) ); + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) ); node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); preNode = Node::null(); } else { @@ -143,7 +143,10 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); } else { if(!preNode.isNull()) { - node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + bool bflag = (preNode.getKind() == kind::CONST_STRING && preNode.getConst().isEmptyString() ); + if(node_vec.empty() || !bflag ) { + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + } } if(node_vec.size() > 1) { retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, node_vec); @@ -161,6 +164,7 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { Node retNode = node; std::vector node_vec; bool flag = false; + //bool allflag = false; for(unsigned i=0; i().isEmptyString()) { + retNode = node[0]; } } else if(node.getKind() == kind::REGEXP_PLUS) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0], -- cgit v1.2.3 From 34e2436636d7a43dd6b9ec5439884f0d8960f06b Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 26 Nov 2014 18:11:35 -0600 Subject: add more functions for regular expressions --- src/theory/strings/regexp_operation.cpp | 109 +++++++++- src/theory/strings/regexp_operation.h | 2 + src/theory/strings/theory_strings.cpp | 352 ++++++++++++++++++++++++++++++-- src/theory/strings/theory_strings.h | 20 +- 4 files changed, 468 insertions(+), 15 deletions(-) diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 69b089c84..2752886cf 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1653,8 +1653,115 @@ void RegExpOpr::splitRegExp(Node r, std::vector< PairNodes > &pset) { } } +void RegExpOpr::flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec) { + Assert(false); + Assert(checkConstRegExp(r)); + switch( r.getKind() ) { + case kind::REGEXP_EMPTY: { + //TODO + break; + } + case kind::REGEXP_SIGMA: { + CVC4::String s("a"); + std::pair< CVC4::String, unsigned > tmp(s, 0); + //TODO + break; + } + case kind::STRING_TO_REGEXP: { + Assert(r[0].isConst()); + CVC4::String s = r[0].getConst< CVC4::String >(); + std::pair< CVC4::String, unsigned > tmp(s, 0); + //TODO + break; + } + case kind::REGEXP_CONCAT: { + for(unsigned i=0; i &vec_or) { + switch(r.getKind()) { + case kind::REGEXP_EMPTY: { + vec_or.push_back(r); + break; + } + case kind::REGEXP_SIGMA: { + vec_or.push_back(r); + break; + } + case kind::STRING_TO_REGEXP: { + vec_or.push_back(r); + break; + } + case kind::REGEXP_CONCAT: { + disjunctRegExp(r[0], vec_or); + for(unsigned i=1; i vec_con; + disjunctRegExp(r[i], vec_con); + std::vector vec_or2; + for(unsigned k1=0; k1mkNode(kind::REGEXP_CONCAT, vec_or[k1], vec_con[k2]) ); + if(std::find(vec_or2.begin(), vec_or2.end(), tmp) == vec_or2.end()) { + vec_or2.push_back( tmp ); + } + } + } + vec_or = vec_or2; + } + break; + } + case kind::REGEXP_UNION: { + for(unsigned i=0; i vec_or2; + disjunctRegExp(r[i], vec_or2); + vec_or.insert(vec_or.end(), vec_or2.begin(), vec_or2.end()); + } + break; + } + case kind::REGEXP_INTER: { + Assert(checkConstRegExp(r)); + Node rtmp = r[0]; + bool spflag = false; + for(unsigned i=1; i().toString() ; return s == "" ? "{E}" : ( s == " " ? "{ }" : s.size()>1? "("+s+")" : s ); diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index ce3093528..6a31a23fb 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -96,6 +96,8 @@ public: Node intersect(Node r1, Node r2, bool &spflag); Node complement(Node r, int &ret); void splitRegExp(Node r, std::vector< PairNodes > &pset); + void flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec); + void disjunctRegExp(Node r, std::vector &vec_or); std::string mkString( Node r ); }; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ead8a44f8..0df551847 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -55,9 +55,11 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_regexp_memberships(c), d_regexp_ucached(u), d_regexp_ccached(c), - d_str_re_map(c), + d_pos_memberships(c), + d_neg_memberships(c), d_inter_cache(c), d_inter_index(c), + d_processed_memberships(c), d_regexp_ant(c), d_input_vars(u), d_input_var_lsum(u), @@ -484,8 +486,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { if( n.getKind() == kind::VARIABLE && options::stringFMF() ) { d_input_vars.insert(n); } - } - if (n.getType().isBoolean()) { + } else if (n.getType().isBoolean()) { // Get triggered for both equal and dis-equal d_equalityEngine.addTriggerPredicate(n); } else { @@ -2514,6 +2515,318 @@ Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) { } } +Node TheoryStrings::normalizeRegexp(Node r) { + Node nf_r = r; + if(d_nf_regexps.find(r) != d_nf_regexps.end()) { + nf_r = d_nf_regexps[r]; + } else { + std::vector< Node > nf_exp; + if(!d_regexp_opr.checkConstRegExp(r)) { + switch( r.getKind() ) { + case kind::REGEXP_EMPTY: + case kind::REGEXP_SIGMA: { + break; + } + case kind::STRING_TO_REGEXP: { + if(r[0].isConst()) { + break; + } else { + if(d_normal_forms.find( r[0] ) != d_normal_forms.end()) { + nf_r = mkConcat( d_normal_forms[r[0]] ); + Debug("regexp-nf") << "Term: " << r[0] << " has a normal form " << nf_r << std::endl; + nf_exp.insert(nf_exp.end(), d_normal_forms_exp[r[0]].begin(), d_normal_forms_exp[r[0]].end()); + nf_r = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, nf_r) ); + } + } + } + case kind::REGEXP_CONCAT: + case kind::REGEXP_UNION: + case kind::REGEXP_INTER: { + bool flag = false; + std::vector< Node > vec_nodes; + for(unsigned i=0; imkNode(r.getKind(), vec_nodes); + nf_r = Rewriter::rewrite( rtmp ); + } + } + case kind::REGEXP_STAR: { + Node rtmp = normalizeRegexp(r[0]); + if(rtmp != r[0]) { + rtmp = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, rtmp); + nf_r = Rewriter::rewrite( rtmp ); + } + } + default: { + Unreachable(); + } + } + } + d_nf_regexps[r] = nf_r; + d_nf_regexps_exp[r] = nf_exp; + } + return nf_r; +} + +bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps) { + std::map< Node, std::vector< Node > > unprocessed_x_exps; + std::map< Node, std::vector< Node > > unprocessed_memberships; + std::map< Node, std::vector< Node > > unprocessed_memberships_bases; + bool addLemma = false; + + Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl; + + for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); + itr_xr != d_pos_memberships.end(); ++itr_xr ) { + Node x = (*itr_xr).first; + NodeList* lst = (*itr_xr).second; + Node nf_x = x; + std::vector< Node > nf_x_exp; + if(d_normal_forms.find( x ) != d_normal_forms.end()) { + //nf_x = mkConcat( d_normal_forms[x] ); + nf_x_exp.insert(nf_x_exp.end(), d_normal_forms_exp[x].begin(), d_normal_forms_exp[x].end()); + //Debug("regexp-nf") << "Term: " << x << " has a normal form " << ret << std::endl; + } else { + Assert(false); + } + Trace("regexp-nf") << "Checking Memberships for N(" << x << ") = " << nf_x << " :" << std::endl; + + std::vector< Node > vec_x; + std::vector< Node > vec_r; + for(NodeList::const_iterator itr_lst = lst->begin(); + itr_lst != lst->end(); ++itr_lst) { + Node r = *itr_lst; + Node nf_r = normalizeRegexp((*lst)[0]); + Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, nf_r); + if(d_processed_memberships.find(memb) == d_processed_memberships.end()) { + if(d_regexp_opr.checkConstRegExp(nf_r)) { + vec_x.push_back(x); + vec_r.push_back(r); + } else { + Trace("regexp-nf") << "Handling Symbolic Regexp for N(" << r << ") = " << nf_r << std::endl; + //TODO: handle symbolic ones + addLemma = true; + } + d_processed_memberships.insert(memb); + } + } + if(!vec_x.empty()) { + if(unprocessed_x_exps.find(nf_x) == unprocessed_x_exps.end()) { + unprocessed_x_exps[nf_x] = nf_x_exp; + unprocessed_memberships[nf_x] = vec_r; + unprocessed_memberships_bases[nf_x] = vec_x; + } else { + unprocessed_x_exps[nf_x].insert(unprocessed_x_exps[nf_x].end(), nf_x_exp.begin(), nf_x_exp.end()); + unprocessed_memberships[nf_x].insert(unprocessed_memberships[nf_x].end(), vec_r.begin(), vec_r.end()); + unprocessed_memberships_bases[nf_x].insert(unprocessed_memberships_bases[nf_x].end(), vec_x.begin(), vec_x.end()); + } + } + } + //Intersection + for(std::map< Node, std::vector< Node > >::const_iterator itr = unprocessed_memberships.begin(); + itr != unprocessed_memberships.end(); ++itr) { + Node nf_x = itr->first; + std::vector< Node > exp( unprocessed_x_exps[nf_x] ); + Node r = itr->second[0]; + //get nf_r + Node inter_r = d_nf_regexps[r]; + exp.insert(exp.end(), d_nf_regexps_exp[r].begin(), d_nf_regexps_exp[r].end()); + Node x = unprocessed_memberships_bases[itr->first][0]; + Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r); + exp.push_back(memb); + for(std::size_t i=1; i < itr->second.size(); i++) { + //exps + Node r2 = itr->second[i]; + Node inter_r2 = d_nf_regexps[r2]; + exp.insert(exp.end(), d_nf_regexps_exp[r2].begin(), d_nf_regexps_exp[r2].end()); + Node x2 = unprocessed_memberships_bases[itr->first][i]; + memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x2, r2); + exp.push_back(memb); + //intersection + bool spflag = false; + inter_r = d_regexp_opr.intersect(inter_r, inter_r2, spflag); + if(inter_r == d_emptyRegexp) { + //conflict + Node antec = exp.size() == 1? exp[0] : NodeManager::currentNM()->mkNode(kind::AND, exp); + Node conc; + sendLemma(antec, conc, "INTERSEC CONFLICT"); + addLemma = true; + break; + } + } + //infer + if(!d_conflict) { + memb = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, inter_r) ); + memb_with_exps[memb] = exp; + } else { + break; + } + } + + return addLemma; +} + +bool TheoryStrings::applyRConsume( CVC4::String &s, Node &r) { + Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s << ", r= " << r << std::endl; + Assert( d_regexp_opr.checkConstRegExp(r) ); + + if( !s.isEmptyString() ) { + Node dc = r; + + for(unsigned i=0; i > vec_can; + d_regexp_opr.splitRegExp(r, vec_can); + //TODO: lazy cache or eager? + std::vector< Node > vec_or; + + for(unsigned int i=0; imkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first); + Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second); + Node c = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, m1, m2) ); + vec_or.push_back( c ); + } + Node conc = vec_or.size()==0? Node::null() : vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) ); + return conc; +} + +bool TheoryStrings::applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps) { + if(XinR_with_exps.size() > 0) { + //TODO: get vector, var, store. + return true; + } else { + return false; + } +} + +bool TheoryStrings::checkMembershipsWithoutLength( + std::map< Node, std::vector< Node > > &memb_with_exps, + std::map< Node, std::vector< Node > > &XinR_with_exps) { + for(std::map< Node, std::vector< Node > >::const_iterator itr = memb_with_exps.begin(); + itr != memb_with_exps.end(); ++itr) { + Node memb = itr->first; + Node s = memb[0]; + Node r = memb[1]; + if(s.isConst()) { + memb = Rewriter::rewrite( memb ); + if(memb == d_false) { + Node antec = itr->second.size() == 1? itr->second[0] : NodeManager::currentNM()->mkNode(kind::AND, itr->second); + Node conc; + sendLemma(antec, conc, "MEMBERSHIP CONFLICT"); + //addLemma = true; + return true; + } else { + Assert(memb == d_true); + } + } else if(s.getKind() == kind::VARIABLE) { + //add to XinR + XinR_with_exps[itr->first] = itr->second; + } else { + Assert(s.getKind() == kind::STRING_CONCAT); + Node antec = itr->second.size() == 1? itr->second[0] : NodeManager::currentNM()->mkNode(kind::AND, itr->second); + Node conc; + for( unsigned i=0; i() ); + //R-Consume, see Tianyi's thesis + if(!applyRConsume(str, r)) { + sendLemma(antec, conc, "R-Consume CONFLICT"); + //addLemma = true; + return true; + } + } else { + //R-Split, see Tianyi's thesis + if(i == s.getNumChildren() - 1) { + //add to XinR + Node memb2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s[i], r); + XinR_with_exps[itr->first] = itr->second; + } else { + Node s1 = s[i]; + std::vector< Node > vec_s2; + for( unsigned j=i+1; j > memb_with_exps; + std::map< Node, std::vector< Node > > XinR_with_exps; + + addedLemma = normalizePosMemberships( memb_with_exps ); + if(!d_conflict) { + // main procedure + addedLemma |= checkMembershipsWithoutLength( memb_with_exps, XinR_with_exps ); + //TODO: check addlemma + if (!addedLemma && !d_conflict) { + for(std::map< Node, std::vector< Node > >::const_iterator itr = XinR_with_exps.begin(); + itr != XinR_with_exps.end(); ++itr) { + std::vector vec_or; + d_regexp_opr.disjunctRegExp( itr->first, vec_or ); + Node tmp = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_or); + Trace("regexp-process") << "Got r: " << itr->first << " to " << tmp << std::endl; + /* + if(r.getKind() == kind::REGEXP_STAR) { + //TODO: apply R-Len + addedLemma = applyRLen(XinR_with_exps); + } else { + //TODO: split + } + */ + } + Assert(false); //TODO:tmp + } + } + + return addedLemma; +} + bool TheoryStrings::checkMemberships() { bool addedLemma = false; bool changed = false; @@ -2523,8 +2836,8 @@ bool TheoryStrings::checkMemberships() { Trace("regexp-debug") << "Checking Memberships ... " << std::endl; //if(options::stringEIT()) { //TODO: Opt for normal forms - for(NodeListMap::const_iterator itr_xr = d_str_re_map.begin(); - itr_xr != d_str_re_map.end(); ++itr_xr ) { + for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); + itr_xr != d_pos_memberships.end(); ++itr_xr ) { bool spflag = false; Node x = (*itr_xr).first; NodeList* lst = (*itr_xr).second; @@ -3132,11 +3445,11 @@ void TheoryStrings::addMembership(Node assertion) { Node r = atom[1]; if(polarity) { NodeList* lst; - NodeListMap::iterator itr_xr = d_str_re_map.find( x ); - if( itr_xr == d_str_re_map.end() ){ + NodeListMap::iterator itr_xr = d_pos_memberships.find( x ); + if( itr_xr == d_pos_memberships.end() ){ lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_str_re_map.insertDataFromContextMemory( x, lst ); + d_pos_memberships.insertDataFromContextMemory( x, lst ); } else { lst = (*itr_xr).second; } @@ -3147,16 +3460,29 @@ void TheoryStrings::addMembership(Node assertion) { } } lst->push_back( r ); - }/* else { - if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { + } else { + /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { int rt; Node r2 = d_regexp_opr.complement(r, rt); Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2); - d_regexp_memberships.push_back( a ); + }*/ + NodeList* lst; + NodeListMap::iterator itr_xr = d_neg_memberships.find( x ); + if( itr_xr == d_neg_memberships.end() ){ + lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator(getSatContext()->getCMM()) ); + d_neg_memberships.insertDataFromContextMemory( x, lst ); } else { - d_regexp_memberships.push_back( assertion ); + lst = (*itr_xr).second; } - }*/ + //check + for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { + if( r == *itr ) { + return; + } + } + lst->push_back( r ); + } d_regexp_memberships.push_back( assertion ); } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index d9326c316..623647942 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -245,7 +245,18 @@ private: bool checkLengthsEqc(); bool checkCardinality(); bool checkInductiveEquations(); + //check membership constraints + Node normalizeRegexp(Node r); + bool normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps); + bool applyRConsume( CVC4::String &s, Node &r); + Node applyRSplit(Node s1, Node s2, Node r); + bool applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps); + bool checkMembershipsWithoutLength( + std::map< Node, std::vector< Node > > &memb_with_exps, + std::map< Node, std::vector< Node > > &XinR_with_exps); bool checkMemberships(); + //temp + bool checkMemberships2(); bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &processed, std::vector< Node > &cprocessed, std::vector< Node > &nf_exp); @@ -325,10 +336,17 @@ private: NodeList d_regexp_memberships; NodeSet d_regexp_ucached; NodeSet d_regexp_ccached; + // stored assertions + NodeListMap d_pos_memberships; + NodeListMap d_neg_memberships; + // semi normal forms for symbolic expression + std::map< Node, Node > d_nf_regexps; + std::map< Node, std::vector< Node > > d_nf_regexps_exp; // intersection - NodeListMap d_str_re_map; NodeNodeMap d_inter_cache; NodeIntMap d_inter_index; + // processed memberships + NodeSet d_processed_memberships; // antecedant for why regexp membership must be true NodeNodeMap d_regexp_ant; // membership length -- cgit v1.2.3 From 4bd4eb16ff7666321f16805b3aa0602019ef54ec Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 26 Nov 2014 19:32:32 -0600 Subject: add more regexp rewriting --- src/theory/strings/regexp_operation.cpp | 12 +++++++----- src/theory/strings/theory_strings_rewriter.cpp | 10 ++++++++-- 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 2752886cf..da8410a94 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1157,9 +1157,10 @@ void RegExpOpr::getCharSet( Node r, std::set &pcset, SetNodes &pvset ) } case kind::REGEXP_INTER: { //TODO: Overapproximation for now - for(unsigned i=0; i::const_iterator itrcache = cache.find(p); @@ -1459,7 +1460,6 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node PairNodes p(r1, r2); cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt))); Node rt = intersectInternal2(r1l, r2l, cache2, spflag, cnt+1); - rt = convert1(cnt, rt); if(spflag) { //TODO: return Node::null(); @@ -1471,6 +1471,8 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes); rNode = Rewriter::rewrite( rNode ); + rNode = convert1(cnt, rNode); + rNode = Rewriter::rewrite( rNode ); } else { //TODO: non-empty var set spflag = true; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index c952a7b3c..99a062f20 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -100,7 +100,7 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { if(!preNode.isNull()) { if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) { preNode = rewriteConcatString( - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) ); + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) ); node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); preNode = Node::null(); } else { @@ -143,7 +143,10 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); } else { if(!preNode.isNull()) { - node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + bool bflag = (preNode.getKind() == kind::CONST_STRING && preNode.getConst().isEmptyString() ); + if(node_vec.empty() || !bflag ) { + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + } } if(node_vec.size() > 1) { retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, node_vec); @@ -161,6 +164,7 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { Node retNode = node; std::vector node_vec; bool flag = false; + //bool allflag = false; for(unsigned i=0; i().isEmptyString()) { + retNode = node[0]; } } else if(node.getKind() == kind::REGEXP_PLUS) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0], -- cgit v1.2.3 From 388a6acf4acd50a7611faae91b3489ac2209e584 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 26 Nov 2014 22:09:38 -0600 Subject: add intersection rewriting --- src/theory/strings/regexp_operation.cpp | 74 +++++++++++++++++++++++-- src/theory/strings/regexp_operation.h | 2 + src/theory/strings/theory_strings_rewriter.cpp | 75 +++++++++++++++++++++++--- src/theory/strings/theory_strings_rewriter.h | 1 + test/regress/regress0/strings/Makefile.am | 1 + test/regress/regress0/strings/regexp003.smt2 | 13 +++++ 6 files changed, 154 insertions(+), 12 deletions(-) create mode 100644 test/regress/regress0/strings/regexp003.smt2 diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index da8410a94..adfd9a3f6 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1484,11 +1484,75 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node Trace("regexp-intersect") << "End of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl; return rNode; } + +Node RegExpOpr::removeIntersection(Node r) { + Assert( checkConstRegExp(r) ); + std::map < Node, Node >::const_iterator itr = d_rm_inter_cache.find(r); + Node retNode; + if(itr != d_rm_inter_cache.end()) { + retNode = itr->second; + } else { + switch(r.getKind()) { + case kind::REGEXP_EMPTY: { + retNode = r; + break; + } + case kind::REGEXP_SIGMA: { + retNode = r; + break; + } + case kind::STRING_TO_REGEXP: { + retNode = r; + break; + } + case kind::REGEXP_CONCAT: { + std::vector< Node > vec_nodes; + for(unsigned i=0; imkNode(kind::REGEXP_CONCAT, vec_nodes) ); + break; + } + case kind::REGEXP_UNION: { + std::vector< Node > vec_nodes; + for(unsigned i=0; imkNode(kind::REGEXP_UNION, vec_nodes) ); + break; + } + case kind::REGEXP_INTER: { + retNode = removeIntersection( r[0] ); + for(unsigned i=1; imkNode(kind::REGEXP_STAR, retNode) ); + break; + } + default: { + Unreachable(); + } + } + d_rm_inter_cache[r] = retNode; + } + Trace("regexp-intersect") << "Remove INTERSECTION( " << mkString(r) << " ) = " << mkString(retNode) << std::endl; + return retNode; +} + Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) { - //std::map< unsigned, std::set< PairNodes > > cache; - std::map< PairNodes, Node > cache; if(checkConstRegExp(r1) && checkConstRegExp(r2)) { - return intersectInternal2(r1, r2, cache, spflag, 1); + Node rr1 = removeIntersection(r1); + Node rr2 = removeIntersection(r2); + std::map< PairNodes, Node > cache; + return intersectInternal2(rr1, rr2, cache, spflag, 1); } else { spflag = true; return Node::null(); @@ -1775,12 +1839,12 @@ std::string RegExpOpr::niceChar(Node r) { std::string RegExpOpr::mkString( Node r ) { std::string retStr; if(r.isNull()) { - retStr = "Empty"; + retStr = "Phi"; } else { int k = r.getKind(); switch( k ) { case kind::REGEXP_EMPTY: { - retStr += "Empty"; + retStr += "Phi"; break; } case kind::REGEXP_SIGMA: { diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 6a31a23fb..3b898e5f5 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -64,6 +64,7 @@ private: std::map< Node, std::pair< std::set, std::set > > d_cset_cache; std::map< Node, std::pair< std::set, std::set > > d_fset_cache; std::map< PairNodes, Node > d_inter_cache; + std::map< Node, Node > d_rm_inter_cache; std::map< Node, std::vector< PairNodes > > d_split_cache; //bool checkStarPlus( Node t ); void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes ); @@ -79,6 +80,7 @@ private: Node convert1(unsigned cnt, Node n); void convert2(unsigned cnt, Node n, Node &r1, Node &r2); Node intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node > cache, bool &spflag, unsigned cnt ); + Node removeIntersection(Node r); void firstChars( Node r, std::set &pcset, SetNodes &pvset ); //TODO: for intersection diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 99a062f20..fc9a7c058 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -163,26 +163,38 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl; Node retNode = node; std::vector node_vec; - bool flag = false; - //bool allflag = false; + bool allflag = false; for(unsigned i=0; i nvec; retNode = node_vec.size() == 0 ? NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ) : node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec); @@ -191,6 +203,53 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { return retNode; } +Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) { + Assert( node.getKind() == kind::REGEXP_INTER ); + Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl; + Node retNode = node; + std::vector node_vec; + bool emptyflag = false; + //Node allNode = Node::null(); + for(unsigned i=0; i nvec; + retNode = node_vec.size() == 0 ? + NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, nvec)) : + node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_INTER, node_vec); + } + Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl; + return retNode; +} + bool TheoryStringsRewriter::checkConstRegExp( TNode t ) { if( t.getKind() != kind::STRING_TO_REGEXP ) { for( unsigned i = 0; i Date: Fri, 28 Nov 2014 16:27:19 +0100 Subject: Synchronize conjecture generation with E-matching. Minor fix to --full-saturate-quant. --- src/theory/quantifiers/conjecture_generator.cpp | 3 +- .../quantifiers/inst_strategy_e_matching.cpp | 14 ++++++---- src/theory/quantifiers/instantiation_engine.cpp | 30 ++------------------ src/theory/quantifiers/instantiation_engine.h | 2 -- src/theory/quantifiers_engine.cpp | 32 +++++++++++++++++++++- src/theory/quantifiers_engine.h | 5 ++++ 6 files changed, 49 insertions(+), 37 deletions(-) diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 06552196d..2f8822b53 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -352,7 +352,8 @@ bool ConjectureGenerator::isGroundTerm( TNode n ) { } bool ConjectureGenerator::needsCheck( Theory::Effort e ) { - return e==Theory::EFFORT_FULL; + // synchonized with instantiation engine + return d_quantEngine->getInstWhenNeedsCheck( e ); } bool ConjectureGenerator::hasEnumeratedUf( Node n ) { diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 8918a6dac..b9e8aef09 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -530,12 +530,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ //skip inst constant nodes while( nvgetTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ - childIndex[index]++; - nv = childIndex[index]+1; + nv++; } } if( nv=0; if( success ){ - Trace("inst-alg-rd") << "Try instantiation..." << std::endl; - index--; + Trace("inst-alg-rd") << "Try instantiation { "; + for( unsigned j=0; j terms; for( unsigned i=0; igetInstantiationEngine()->d_statistics.d_instantiations_guess); return STATUS_UNKNOWN; + }else{ + index--; } } }while( success ); diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index ade6d4313..b53919aaf 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -31,7 +31,7 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){ +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ){ } @@ -178,37 +178,11 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } bool InstantiationEngine::needsCheck( Theory::Effort e ){ - if( e==Theory::EFFORT_FULL ){ - d_ierCounter++; - } - //determine if we should perform check, based on instWhenMode - bool performCheck = false; - if( options::instWhenMode()==INST_WHEN_FULL ){ - performCheck = ( e >= Theory::EFFORT_FULL ); - }else if( options::instWhenMode()==INST_WHEN_FULL_DELAY ){ - performCheck = ( e >= Theory::EFFORT_FULL ) && !d_quantEngine->getTheoryEngine()->needCheck(); - }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){ - performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); - }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){ - performCheck = ( e >= Theory::EFFORT_LAST_CALL ); - }else{ - performCheck = true; - } - static int ierCounter2 = 0; - if( e==Theory::EFFORT_LAST_CALL ){ - ierCounter2++; - //with bounded integers, skip every other last call, - // since matching loops may occur with infinite quantification - if( ierCounter2%2==0 && options::fmfBoundInt() ){ - performCheck = false; - } - } - return performCheck; + return d_quantEngine->getInstWhenNeedsCheck( e ); } void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ - Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl; double clSet = 0; if( Trace.isOn("inst-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 2fa37ac35..2d427ae0a 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -84,8 +84,6 @@ private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** whether the instantiation engine should set incomplete if it cannot answer SAT */ bool d_setIncomplete; - /** inst round counter */ - int d_ierCounter; /** whether each quantifier is active */ std::map< Node, bool > d_quant_active; /** whether we have added cbqi lemma */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4dc8df09d..d6c6f4667 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -171,8 +171,9 @@ d_lemmas_produced_c(u){ d_builder = NULL; } - //options d_total_inst_count_debug = 0; + d_ierCounter = 0; + d_ierCounter_lc = 0; } QuantifiersEngine::~QuantifiersEngine(){ @@ -251,6 +252,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; } + if( e==Theory::EFFORT_FULL ){ + d_ierCounter++; + }else if( e==Theory::EFFORT_LAST_CALL ){ + d_ierCounter_lc++; + } bool needsCheck = false; bool needsModel = false; bool needsFullModel = false; @@ -825,6 +831,30 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool return addSplit( fm ); } +bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { + //determine if we should perform check, based on instWhenMode + bool performCheck = false; + if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){ + performCheck = ( e >= Theory::EFFORT_FULL ); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){ + performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck(); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){ + performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){ + performCheck = ( e >= Theory::EFFORT_LAST_CALL ); + }else{ + performCheck = true; + } + if( e==Theory::EFFORT_LAST_CALL ){ + //with bounded integers, skip every other last call, + // since matching loops may occur with infinite quantification + if( d_ierCounter_lc%2==0 && options::fmfBoundInt() ){ + performCheck = false; + } + } + return performCheck; +} + void QuantifiersEngine::flushLemmas(){ if( !d_lemmas_waiting.empty() ){ //take default output channel if none is provided diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 2b466b96b..ac782a536 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -169,6 +169,9 @@ private: std::map< Node, int > d_total_inst_debug; std::map< Node, int > d_temp_inst_debug; int d_total_inst_count_debug; + /** inst round counters */ + int d_ierCounter; + int d_ierCounter_lc; private: KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); public: @@ -273,6 +276,8 @@ public: bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } /** get number of waiting lemmas */ int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); } + /** get needs check */ + bool getInstWhenNeedsCheck( Theory::Effort e ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, uint64_t level ); /** is term eligble for instantiation? */ -- cgit v1.2.3 From fa6ac807d931518790df89206c4f3aeceff8e395 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 2 Dec 2014 23:44:26 -0600 Subject: disable inter cache --- src/theory/strings/regexp_operation.cpp | 107 ++++++++++++------------- src/theory/strings/theory_strings_rewriter.cpp | 44 +++++++++- src/theory/strings/theory_strings_rewriter.h | 1 + 3 files changed, 93 insertions(+), 59 deletions(-) diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index adfd9a3f6..016983059 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1383,7 +1383,8 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { } } Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node > cache, bool &spflag, unsigned cnt ) { - Trace("regexp-intersect") << "Starting INTERSECT:\n "<< mkString(r1) << ",\n " << mkString(r2) << std::endl; + //(checkConstRegExp(r1) && checkConstRegExp(r2)) + Trace("regexp-intersect") << "Starting INTERSECT(" << cnt << "):\n "<< mkString(r1) << ",\n " << mkString(r2) << std::endl; //if(Trace.isOn("regexp-debug")) { // Trace("regexp-debug") << "... with cache:\n"; // for(std::map< PairNodes, Node >::const_iterator itr=cache.begin(); @@ -1398,9 +1399,9 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node std::pair < Node, Node > p(r1, r2); std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_inter_cache.find(p); Node rNode; - if(itr != d_inter_cache.end()) { - rNode = itr->second; - } else { +// if(itr != d_inter_cache.end()) { +// rNode = itr->second; +// } else { if(r1 == d_emptyRegexp || r2 == d_emptyRegexp) { rNode = d_emptyRegexp; } else if(r1 == d_emptySingleton || r2 == d_emptySingleton) { @@ -1422,66 +1423,60 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node if(itrcache != cache.end()) { rNode = itrcache->second; } else { - if(checkConstRegExp(r1) && checkConstRegExp(r2)) { - std::vector< unsigned > cset; - std::set< unsigned > cset1, cset2; - std::set< Node > vset1, vset2; - firstChars(r1, cset1, vset1); - firstChars(r2, cset2, vset2); - std::set_intersection(cset1.begin(), cset1.end(), cset2.begin(), cset1.end(), - std::inserter(cset, cset.begin())); - std::vector< Node > vec_nodes; - Node delta_exp; - int flag = delta(r1, delta_exp); - int flag2 = delta(r2, delta_exp); - if(flag != 2 && flag2 != 2) { - if(flag == 1 && flag2 == 1) { - vec_nodes.push_back(d_emptySingleton); - } else { - //TODO - spflag = true; - } - } - if(Trace.isOn("regexp-debug")) { - Trace("regexp-debug") << "Try CSET( " << cset.size() << " ) = "; - for(std::vector::const_iterator itr = cset.begin(); - itr != cset.end(); itr++) { - CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) ); - Trace("regexp-debug") << c << ", "; - } - Trace("regexp-debug") << std::endl; + std::vector< unsigned > cset; + std::set< unsigned > cset1, cset2; + std::set< Node > vset1, vset2; + firstChars(r1, cset1, vset1); + firstChars(r2, cset2, vset2); + std::set_intersection(cset1.begin(), cset1.end(), cset2.begin(), cset1.end(), + std::inserter(cset, cset.begin())); + std::vector< Node > vec_nodes; + Node delta_exp; + int flag = delta(r1, delta_exp); + int flag2 = delta(r2, delta_exp); + if(flag != 2 && flag2 != 2) { + if(flag == 1 && flag2 == 1) { + vec_nodes.push_back(d_emptySingleton); + } else { + //TODO + spflag = true; } + } + if(Trace.isOn("regexp-debug")) { + Trace("regexp-debug") << "Try CSET( " << cset.size() << " ) = "; for(std::vector::const_iterator itr = cset.begin(); itr != cset.end(); itr++) { CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) ); - Node r1l = derivativeSingle(r1, c); - Node r2l = derivativeSingle(r2, c); - std::map< PairNodes, Node > cache2(cache); - PairNodes p(r1, r2); - cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt))); - Node rt = intersectInternal2(r1l, r2l, cache2, spflag, cnt+1); - if(spflag) { - //TODO: - return Node::null(); - } - rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, - NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) ); - vec_nodes.push_back(rt); + Trace("regexp-debug") << c << ", "; } - rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] : - NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes); - rNode = Rewriter::rewrite( rNode ); - rNode = convert1(cnt, rNode); - rNode = Rewriter::rewrite( rNode ); - } else { - //TODO: non-empty var set - spflag = true; + Trace("regexp-debug") << std::endl; } + for(std::vector::const_iterator itr = cset.begin(); + itr != cset.end(); itr++) { + CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) ); + Node r1l = derivativeSingle(r1, c); + Node r2l = derivativeSingle(r2, c); + std::map< PairNodes, Node > cache2(cache); + PairNodes p(r1, r2); + cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt))); + Node rt = intersectInternal2(r1l, r2l, cache2, spflag, cnt+1); + //if(spflag) { + //return Node::null(); + //} + rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, + NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) ); + vec_nodes.push_back(rt); + } + rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] : + NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes); + rNode = Rewriter::rewrite( rNode ); + rNode = convert1(cnt, rNode); + rNode = Rewriter::rewrite( rNode ); } } - d_inter_cache[p] = rNode; - } - Trace("regexp-intersect") << "End of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl; +// d_inter_cache[p] = rNode; +// } + Trace("regexp-intersect") << "End(" << cnt << ") of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl; return rNode; } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index fc9a7c058..dfec0a795 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -170,7 +170,9 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { if(tmpNode.getKind() == kind::REGEXP_UNION) { for(unsigned int j=0; j().isEmptyString()) { + return true; + } + } + return false; +} + RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { Node retNode = node; Node orig = retNode; @@ -684,6 +699,29 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { retNode = node[0]; } else if(node[0].getKind() == kind::STRING_TO_REGEXP && node[0][0].getKind() == kind::CONST_STRING && node[0][0].getConst().isEmptyString()) { retNode = node[0]; + } else if(node[0].getKind() == kind::REGEXP_EMPTY) { + retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, + NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); + } else if(node[0].getKind() == kind::REGEXP_UNION) { + Node tmpNode = prerewriteOrRegExp(node[0]); + if(tmpNode.getKind() == kind::REGEXP_UNION) { + if(hasEpsilonNode(node[0])) { + std::vector< Node > node_vec; + for(unsigned int i=0; i().isEmptyString()) { + //return true; + } else { + node_vec.push_back(node[0][i]); + } + } + retNode = node_vec.size()==1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec); + retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, retNode); + } + } else if(tmpNode.getKind() == kind::STRING_TO_REGEXP && tmpNode[0].getKind() == kind::CONST_STRING && tmpNode[0].getConst().isEmptyString()) { + retNode = tmpNode; + } else { + retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, tmpNode); + } } } else if(node.getKind() == kind::REGEXP_PLUS) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0], diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index dafab75cb..a1098f631 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -42,6 +42,7 @@ public: static RewriteResponse postRewrite(TNode node); + static bool hasEpsilonNode(TNode node); static RewriteResponse preRewrite(TNode node); static inline void init() {} -- cgit v1.2.3