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
}
}
+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\
#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"
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);
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;
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"
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
#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"
"--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)
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;
}
//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 "
<< 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;
Trace("strings-loop") << "Strings::Loop: tails are different."
<< std::endl;
sendInference(info.d_ant, conc, "Loop Conflict", true);
- return false;
+ return ProcessLoopResult::CONFLICT;
}
}
// 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
{
}
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
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
LENGTH_ONE,
LENGTH_GEQ_ONE
};
+
/** register length
*
* This method is called on non-constant string terms n. It sends a lemma
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,
projects / cvc5.git / commitdiff