From: Andrew Reynolds Date: Tue, 18 Sep 2018 21:56:24 +0000 (-0500) Subject: Decision strategy: incorporate strings fmf. (#2485) X-Git-Tag: cvc5-1.0.0~4631 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e9d45556f4ca8f370ffbd8383885231fe0e456dc;p=cvc5.git Decision strategy: incorporate strings fmf. (#2485) --- diff --git a/src/theory/decision_manager.h b/src/theory/decision_manager.h index ff30a13f8..7ac27a531 100644 --- a/src/theory/decision_manager.h +++ b/src/theory/decision_manager.h @@ -71,9 +71,9 @@ class DecisionManager STRAT_UF_CARD, STRAT_DT_SYGUS_ENUM_ACTIVE, STRAT_DT_SYGUS_ENUM_SIZE, + STRAT_STRINGS_SUM_LENGTHS, STRAT_QUANT_BOUND_INT_SIZE, STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, - STRAT_STRINGS_SUM_LENGTHS, STRAT_SEP_NEG_GUARD, // placeholder for last finite-model-complete required strategy STRAT_LAST_FM_COMPLETE, diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f007ae1df..4b73e496e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -136,6 +136,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_input_var_lsum(u), d_cardinality_lits(u), d_curr_cardinality(c, 0), + d_sslds(nullptr), d_strategy_init(false) { setupExtTheory(); @@ -490,6 +491,25 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) { void TheoryStrings::presolve() { Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl; initializeStrategy(); + + // if strings fmf is enabled, register the strategy + if (options::stringFMF()) + { + d_sslds.reset(new StringSumLengthDecisionStrategy( + getSatContext(), getUserContext(), d_valuation)); + Trace("strings-dstrat-reg") + << "presolve: register decision strategy." << std::endl; + std::vector inputVars; + for (NodeSet::const_iterator itr = d_input_vars.begin(); + itr != d_input_vars.end(); + ++itr) + { + inputVars.push_back(*itr); + } + d_sslds->initialize(inputVars); + getDecisionManager()->registerStrategy( + DecisionManager::STRAT_STRINGS_SUM_LENGTHS, d_sslds.get()); + } } @@ -816,6 +836,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { : kindToTheoryId(k) != THEORY_STRINGS)) { d_input_vars.insert(n); + Trace("strings-dstrat-reg") << "input variable: " << n << std::endl; } d_equalityEngine.addTerm(n); } else if (tn.isBoolean()) { @@ -936,7 +957,7 @@ void TheoryStrings::check(Effort e) { bool TheoryStrings::needsCheckLastEffort() { if( options::stringGuessModel() ){ - return d_has_extf.get(); + return d_has_extf.get(); }else{ return false; } @@ -4328,65 +4349,49 @@ void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) { } - //// Finite Model Finding -Node TheoryStrings::getNextDecisionRequest( unsigned& priority ) { - if( options::stringFMF() && !d_conflict ){ - Node in_var_lsum = d_input_var_lsum.get(); - //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl; - //initialize the term we will minimize - if( in_var_lsum.isNull() && !d_input_vars.empty() ){ - Trace("strings-fmf-debug") << "Input variables: "; - std::vector< Node > ll; - for(NodeSet::key_iterator itr = d_input_vars.key_begin(); - itr != d_input_vars.key_end(); ++itr) { - Trace("strings-fmf-debug") << " " << (*itr) ; - ll.push_back( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr ) ); - } - Trace("strings-fmf-debug") << std::endl; - in_var_lsum = ll.size()==1 ? ll[0] : NodeManager::currentNM()->mkNode( kind::PLUS, ll ); - in_var_lsum = Rewriter::rewrite( in_var_lsum ); - d_input_var_lsum.set( in_var_lsum ); - } - if( !in_var_lsum.isNull() ){ - //Trace("strings-fmf") << "Get next decision request." << std::endl; - //check if we need to decide on something - int decideCard = d_curr_cardinality.get(); - if( d_cardinality_lits.find( decideCard )!=d_cardinality_lits.end() ){ - bool value; - Node cnode = d_cardinality_lits[ d_curr_cardinality.get() ]; - if( d_valuation.hasSatValue( cnode, value ) ) { - if( !value ){ - d_curr_cardinality.set( d_curr_cardinality.get() + 1 ); - decideCard = d_curr_cardinality.get(); - Trace("strings-fmf-debug") << "Has false SAT value, increment and decide." << std::endl; - }else{ - decideCard = -1; - Trace("strings-fmf-debug") << "Has true SAT value, do not decide." << std::endl; - } - }else{ - Trace("strings-fmf-debug") << "No SAT value, decide." << std::endl; - } - } - if( decideCard!=-1 ){ - if( d_cardinality_lits.find( decideCard )==d_cardinality_lits.end() ){ - Node lit = NodeManager::currentNM()->mkNode( kind::LEQ, in_var_lsum, NodeManager::currentNM()->mkConst( Rational( decideCard ) ) ); - lit = Rewriter::rewrite( lit ); - d_cardinality_lits[decideCard] = lit; - Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() ); - Trace("strings-fmf") << "Strings::FMF: Add decision lemma " << lem << ", decideCard = " << decideCard << std::endl; - d_out->lemma( lem ); - d_out->requirePhase( lit, true ); - } - Node lit = d_cardinality_lits[ decideCard ]; - Trace("strings-fmf") << "Strings::FMF: Decide positive on " << lit << std::endl; - priority = 1; - return lit; - } +TheoryStrings::StringSumLengthDecisionStrategy::StringSumLengthDecisionStrategy( + context::Context* c, context::UserContext* u, Valuation valuation) + : DecisionStrategyFmf(c, valuation), d_input_var_lsum(u) +{ +} + +bool TheoryStrings::StringSumLengthDecisionStrategy::isInitialized() +{ + return !d_input_var_lsum.get().isNull(); +} + +void TheoryStrings::StringSumLengthDecisionStrategy::initialize( + const std::vector& vars) +{ + if (d_input_var_lsum.get().isNull() && !vars.empty()) + { + NodeManager* nm = NodeManager::currentNM(); + std::vector sum; + for (const Node& v : vars) + { + sum.push_back(nm->mkNode(STRING_LENGTH, v)); } + Node sumn = sum.size() == 1 ? sum[0] : nm->mkNode(PLUS, sum); + d_input_var_lsum.set(sumn); } - return Node::null(); +} + +Node TheoryStrings::StringSumLengthDecisionStrategy::mkLiteral(unsigned i) +{ + if (d_input_var_lsum.get().isNull()) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); + Node lit = nm->mkNode(LEQ, d_input_var_lsum.get(), nm->mkConst(Rational(i))); + Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit << std::endl; + return lit; +} +std::string TheoryStrings::StringSumLengthDecisionStrategy::identify() const +{ + return std::string("string_sum_len"); } Node TheoryStrings::ppRewrite(TNode atom) { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 77dae0cf3..73906d029 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -22,6 +22,7 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "expr/attribute.h" +#include "theory/decision_manager.h" #include "theory/strings/regexp_elim.h" #include "theory/strings/regexp_operation.h" #include "theory/strings/skolem_cache.h" @@ -643,10 +644,40 @@ private: context::CDO< Node > d_input_var_lsum; context::CDHashMap< int, Node > d_cardinality_lits; context::CDO< int > d_curr_cardinality; + /** String sum of lengths decision strategy + * + * This decision strategy enforces that len(x_1) + ... + len(x_k) <= n + * for a minimal natural number n, where x_1, ..., x_n is the list of + * input variables of the problem of type String. + * + * This decision strategy is enabled by option::stringsFmf(). + */ + class StringSumLengthDecisionStrategy : public DecisionStrategyFmf + { + public: + StringSumLengthDecisionStrategy(context::Context* c, + context::UserContext* u, + Valuation valuation); + /** make literal */ + Node mkLiteral(unsigned i) override; + /** identify */ + std::string identify() const override; + /** is initialized */ + bool isInitialized(); + /** initialize */ + void initialize(const std::vector& vars); + + private: + /** + * User-context-dependent node corresponding to the sum of the lengths of + * input variables of type string + */ + context::CDO d_input_var_lsum; + }; + /** an instance of the above class */ + std::unique_ptr d_sslds; public: - //for finite model finding - Node getNextDecisionRequest(unsigned& priority) override; // ppRewrite Node ppRewrite(TNode atom) override;