diff options
| -rw-r--r-- | src/options/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 55 | ||||
| -rw-r--r-- | src/options/options_handler.h | 5 | ||||
| -rw-r--r-- | src/options/strings_options.toml | 24 | ||||
| -rw-r--r-- | src/options/strings_process_loop_mode.cpp | 50 | ||||
| -rw-r--r-- | src/options/strings_process_loop_mode.h | 55 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 65 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 28 |
9 files changed, 260 insertions, 34 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index b86db8d00..fc725978e 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -37,6 +37,8 @@ libcvc4_add_sources( set_language.h smt_modes.cpp smt_modes.h + strings_process_loop_mode.cpp + strings_process_loop_mode.h sygus_out_mode.h theoryof_mode.cpp theoryof_mode.h diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index c08c59d89..84b9f3b4c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1337,6 +1337,61 @@ theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode( } } +const std::string OptionsHandler::s_stringToStringsProcessLoopModeHelp = + "Loop processing modes supported by the --strings-process-loop-mode " + "option:\n" + "\n" + "full (default)\n" + "+ Perform full processing of looping word equations\n" + "\n" + "simple (default with --strings-fmf)\n" + "+ Omit normal loop breaking\n" + "\n" + "simple-abort\n" + "+ Abort when normal loop breaking is required\n" + "\n" + "none\n" + "+ Omit loop processing\n" + "\n" + "abort\n" + "+ Abort if looping word equations are encountered\n"; + +theory::strings::ProcessLoopMode OptionsHandler::stringToStringsProcessLoopMode( + std::string option, std::string optarg) +{ + if (optarg == "full") + { + return theory::strings::ProcessLoopMode::FULL; + } + else if (optarg == "simple") + { + return theory::strings::ProcessLoopMode::SIMPLE; + } + else if (optarg == "simple-abort") + { + return theory::strings::ProcessLoopMode::SIMPLE_ABORT; + } + else if (optarg == "none") + { + return theory::strings::ProcessLoopMode::NONE; + } + else if (optarg == "abort") + { + return theory::strings::ProcessLoopMode::ABORT; + } + else if (optarg == "help") + { + puts(s_stringToStringsProcessLoopModeHelp.c_str()); + exit(1); + } + else + { + throw OptionException( + std::string("unknown option for --strings-process-loop-mode: `") + + optarg + "'. Try --strings-process-loop-mode=help."); + } +} + const std::string OptionsHandler::s_boolToBVModeHelp = "\ BoolToBV pass modes supported by the --bool-to-bv option:\n\ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 126538436..8b2629db7 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -37,6 +37,7 @@ #include "options/printer_modes.h" #include "options/quantifiers_modes.h" #include "options/smt_modes.h" +#include "options/strings_process_loop_mode.h" #include "options/sygus_out_mode.h" #include "options/theoryof_mode.h" #include "options/ufss_mode.h" @@ -148,6 +149,9 @@ public: theory::bv::BvProofFormat stringToBvProofFormat(std::string option, std::string optarg); + theory::strings::ProcessLoopMode stringToStringsProcessLoopMode( + std::string option, std::string optarg); + // theory/uf/options_handlers.h theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg); @@ -236,6 +240,7 @@ public: static const std::string s_bvProofFormatHelp; static const std::string s_booleanTermConversionModeHelp; static const std::string s_bvSlicerModeHelp; + static const std::string s_stringToStringsProcessLoopModeHelp; static const std::string s_boolToBVModeHelp; static const std::string s_cegqiFairModeHelp; static const std::string s_decisionModeHelp; diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 3544c37fe..fd00b8917 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -129,22 +129,14 @@ header = "options/strings_options.h" help = "check entailment between length terms to reduce splitting" [[option]] - name = "stringProcessLoop" - category = "regular" - long = "strings-process-loop" - type = "bool" - default = "true" - read_only = true - help = "reduce looping word equations to regular expressions" - -[[option]] - name = "stringAbortLoop" - category = "regular" - long = "strings-abort-loop" - type = "bool" - default = "false" - read_only = true - help = "abort when a looping word equation is encountered" + name = "stringProcessLoopMode" + category = "expert" + long = "strings-process-loop-mode=MODE" + type = "CVC4::theory::strings::ProcessLoopMode" + default = "CVC4::theory::strings::ProcessLoopMode::FULL" + handler = "stringToStringsProcessLoopMode" + includes = ["options/strings_process_loop_mode.h"] + help = "choose how to process looping string equations, see --strings-process-loop-mode=help for details" [[option]] name = "stringInferAsLemmas" diff --git a/src/options/strings_process_loop_mode.cpp b/src/options/strings_process_loop_mode.cpp new file mode 100644 index 000000000..59667ea75 --- /dev/null +++ b/src/options/strings_process_loop_mode.cpp @@ -0,0 +1,50 @@ +/********************* */ +/*! \file strings_process_loop_mode.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Modes for processing looping word equations in the string solver. + ** + ** Modes for processing looping word equations in the string solver. + **/ + +#include "options/strings_process_loop_mode.h" + +#include <cstdint> +#include <iostream> + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, + theory::strings::ProcessLoopMode mode) +{ + switch (mode) + { + case theory::strings::ProcessLoopMode::FULL: + out << "ProcessLoopMode::FULL"; + break; + case theory::strings::ProcessLoopMode::SIMPLE: + out << "ProcessLoopMode::SIMPLE"; + break; + case theory::strings::ProcessLoopMode::SIMPLE_ABORT: + out << "ProcessLoopMode::SIMPLE_ABORT"; + break; + case theory::strings::ProcessLoopMode::NONE: + out << "ProcessLoopMode::NONE"; + break; + case theory::strings::ProcessLoopMode::ABORT: + out << "ProcessLoopMode::ABORT"; + break; + default: + out << "ProcessLoopMode:UNKNOWN![" << static_cast<int64_t>(mode) << "]"; + } + return out; +} + +} // namespace CVC4 diff --git a/src/options/strings_process_loop_mode.h b/src/options/strings_process_loop_mode.h new file mode 100644 index 000000000..2933e034f --- /dev/null +++ b/src/options/strings_process_loop_mode.h @@ -0,0 +1,55 @@ +/********************* */ +/*! \file strings_process_loop_mode.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Modes for processing looping word equations in the string solver. + ** + ** Modes for processing looping word equations in the string solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H +#define __CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H + +#include <iosfwd> + +namespace CVC4 { +namespace theory { +namespace strings { + +/** Enumeration of bit-blasting modes */ +enum class ProcessLoopMode +{ + /** Perform full loop processing. */ + FULL, + + /** Omit normal loop breaking. */ + SIMPLE, + + /** Abort if normal loop breaking is required. */ + SIMPLE_ABORT, + + /** Omit loop processing. */ + NONE, + + /** Abort if looping word equations are encountered. */ + ABORT +}; // enum ProcessLoopMode + +} // namespace strings +} // namespace theory + +std::ostream& operator<<(std::ostream& out, + theory::strings::ProcessLoopMode mode); + +} // namespace CVC4 + +#endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ae20fa156..747fc3ac8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -68,6 +68,7 @@ #include "options/set_language.h" #include "options/smt_options.h" #include "options/strings_options.h" +#include "options/strings_process_loop_mode.h" #include "options/theory_options.h" #include "options/uf_options.h" #include "preprocessing/preprocessing_pass.h" @@ -2262,6 +2263,15 @@ void SmtEngine::setDefaults() { "--sygus-expr-miner-check-use-export"); } } + + if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser()) + { + Trace("smt") << "settting stringProcessLoopMode to 'simple' since " + "--strings-fmf enabled" + << endl; + options::stringProcessLoopMode.set( + theory::strings::ProcessLoopMode::SIMPLE); + } } void SmtEngine::setProblemExtended(bool value) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5179ddab3..e89a8f917 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3083,15 +3083,29 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl; int loop_in_i = -1; int loop_in_j = -1; + ProcessLoopResult plr = ProcessLoopResult::SKIPPED; if( detectLoop( normal_forms, i, j, index, loop_in_i, loop_in_j, rproc ) ){ if( !isRev ){ //FIXME getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, -1, isRev, info.d_ant ); //set info - if( processLoop( normal_forms, normal_form_src, i, j, loop_in_i!=-1 ? i : j, loop_in_i!=-1 ? j : i, loop_in_i!=-1 ? loop_in_i : loop_in_j, index, info ) ){ + plr = processLoop(normal_forms, + normal_form_src, + i, + j, + loop_in_i != -1 ? i : j, + loop_in_i != -1 ? j : i, + loop_in_i != -1 ? loop_in_i : loop_in_j, + index, + info); + if (plr == ProcessLoopResult::INFERENCE) + { info_valid = true; } } - }else{ + } + + if (plr == ProcessLoopResult::SKIPPED) + { //AJR: length entailment here? if( normal_forms[i][index].getKind() == kind::CONST_STRING || normal_forms[j][index].getKind() == kind::CONST_STRING ){ unsigned const_k = normal_forms[i][index].getKind() == kind::CONST_STRING ? i : j; @@ -3311,18 +3325,27 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms } //xs(zy)=t(yz)xr -bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, - int i, int j, int loop_n_index, int other_n_index, int loop_index, int index, InferInfo& info ){ - if( options::stringAbortLoop() ){ - std::stringstream ss; - ss << "Looping word equation encountered." << std::endl; - throw LogicException(ss.str()); - } - if (!options::stringProcessLoop()) +TheoryStrings::ProcessLoopResult TheoryStrings::processLoop( + const std::vector<std::vector<Node> >& normal_forms, + const std::vector<Node>& normal_form_src, + int i, + int j, + int loop_n_index, + int other_n_index, + int loop_index, + int index, + InferInfo& info) +{ + if (options::stringProcessLoopMode() == ProcessLoopMode::ABORT) + { + throw LogicException("Looping word equation encountered."); + } + else if (options::stringProcessLoopMode() == ProcessLoopMode::NONE) { d_out->setIncomplete(); - return false; + return ProcessLoopResult::SKIPPED; } + NodeManager* nm = NodeManager::currentNM(); Node conc; Trace("strings-loop") << "Detected possible loop for " @@ -3331,12 +3354,12 @@ bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_form << std::endl; Trace("strings-loop") << " ... T(Y.Z)= "; - std::vector<Node>& veci = normal_forms[loop_n_index]; + const std::vector<Node>& veci = normal_forms[loop_n_index]; std::vector<Node> vec_t(veci.begin() + index, veci.begin() + loop_index); Node t_yz = mkConcat(vec_t); Trace("strings-loop") << " (" << t_yz << ")" << std::endl; Trace("strings-loop") << " ... S(Z.Y)= "; - std::vector<Node>& vecoi = normal_forms[other_n_index]; + const std::vector<Node>& vecoi = normal_forms[other_n_index]; std::vector<Node> vec_s(vecoi.begin() + index + 1, vecoi.end()); Node s_zy = mkConcat(vec_s); Trace("strings-loop") << s_zy << std::endl; @@ -3366,7 +3389,7 @@ bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_form Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl; sendInference(info.d_ant, conc, "Loop Conflict", true); - return false; + return ProcessLoopResult::CONFLICT; } } @@ -3384,7 +3407,7 @@ bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_form // try to make t equal to empty to avoid loop info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate()); info.d_id = INFER_LEN_SPLIT_EMP; - return true; + return ProcessLoopResult::INFERENCE; } else { @@ -3464,6 +3487,16 @@ bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_form } else { + if (options::stringProcessLoopMode() == ProcessLoopMode::SIMPLE_ABORT) + { + throw LogicException("Normal looping word equation encountered."); + } + else if (options::stringProcessLoopMode() == ProcessLoopMode::SIMPLE) + { + d_out->setIncomplete(); + return ProcessLoopResult::SKIPPED; + } + Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking." << std::endl; // right @@ -3505,7 +3538,7 @@ bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_form info.d_id = INFER_FLOOP; info.d_nf_pair[0] = normal_form_src[i]; info.d_nf_pair[1] = normal_form_src[j]; - return true; + return ProcessLoopResult::INFERENCE; } //return true for lemma, false if we succeed diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index aa86f1bc1..70e75db54 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -409,6 +409,7 @@ private: LENGTH_ONE, LENGTH_GEQ_ONE }; + /** register length * * This method is called on non-constant string terms n. It sends a lemma @@ -520,8 +521,31 @@ private: void getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ); bool detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, int index, int &loop_in_i, int &loop_in_j, unsigned rproc ); - bool processLoop( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, - int i, int j, int loop_n_index, int other_n_index,int loop_index, int index, InferInfo& info ); + + /** + * Result of processLoop() below. + */ + enum class ProcessLoopResult + { + /** Loop processing made an inference */ + INFERENCE, + /** Loop processing detected a conflict */ + CONFLICT, + /** Loop not processed or no loop detected */ + SKIPPED, + }; + + ProcessLoopResult processLoop( + const std::vector<std::vector<Node> >& normal_forms, + const std::vector<Node>& normal_form_src, + int i, + int j, + int loop_n_index, + int other_n_index, + int loop_index, + int index, + InferInfo& info); + void processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ); void processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, |