diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-11 09:03:47 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-11 09:03:47 -0500 |
| commit | d4099f01bfad0924f1039cbd466279b5ebc551ce (patch) | |
| tree | c19adb6c3ce21159f9ca3621ff5702ee7d981c66 /src/theory/strings/theory_strings.h | |
| parent | e8598e2420e2ee2c75abfb6629818299c7ab40f6 (diff) | |
Minor change to strings, introduce proxy vars only when necessary.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 1cead2c22..3cab81a70 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -344,7 +344,7 @@ private: void processSimpleNEq( 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, unsigned i, unsigned j, unsigned& index, bool isRev, unsigned rproc, std::vector< InferInfo >& pinfer ); - bool processDeq( Node n1, Node n2 ); + void processDeq( Node n1, Node n2 ); int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ); int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ); void checkDeqNF(); |