diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-15 10:28:47 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-15 10:28:47 -0800 |
| commit | 4a38be3b9ac133655602a989f1136cd24ed89bc6 (patch) | |
| tree | d8a03c6a78a822b658587cbd06af2e0c1e5bd50f /src/theory/strings/theory_strings.h | |
| parent | da504025a3a77e9a3201af33ee6f96f937802807 (diff) | |
Strings: Add option to change loop process mode (#2794)
This commit adds an option `--strings-process-loop-mode` that allows
finer-grained control over CVC4 processes looping word equation. In
particular, performing normal loop breaking sometimes leads to worse
performance. The "simple" mode disables that inference.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 28 |
1 files changed, 26 insertions, 2 deletions
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, |