Replacing C-like input/output with C++ style code, some other changes #22
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…unimplemented properties
|
|
Hi Daniel,
I temporarily removed BDD2 and just forgot to put it back. ebmc was
failing this test by consuming a growing amount of memory and so hanging
my computer.
I will make the necessary changes with status and error messages.
Eugene
…On Mon, Jul 3, 2017 at 4:19 AM, Daniel Kroening ***@***.***> wrote:
Is there a reason why the BDD2 test got removed?
Also, note that we use a custom stream for status and error messages, to
be found in util/message.h. Do not use std::cout and std::cerr.
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#22 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCpeA-GEViywiJMFtVjLty18AG5R0ks5sKKP-gaJpZM4OL9R8>
.
|
|
Hi Eugene,
the BDD2/3/5 regression tests are solved once
diffblue/cbmc#1062 hits CBMC and we move the
submodule pointer.
Matthias
|
mgudemann
suggested changes
Jul 3, 2017
There was a problem hiding this comment.
there are some recurring changes, in particular for what was char[...] before and is std::string now that can be simplified. It seems that this was mainly to format some intergal values, this can be don easily using std::to_string(...) to get a string, no need to create an std::ostringstream and call .str() on it.
also, all ic3_? regression tests fail, e.g., ic3_1 with
~/s/d/h/r/e/ic3_1 (new_ic3_bugs) $ ebmc pdtvispeterson.sv --ic3
Parsing pdtvispeterson.sv
Converting
Type-checking Verilog::pdtvispeterson
Using module `pdtvispeterson'
Generating Netlist
fish: “ebmc pdtvispeterson.sv --ic3” terminated by signal SIGSEGV (Address boundary error)
src/ic3/build_prob/g0en_cnf.cc
Outdated
| print_var_indexes(fname1); | ||
| fname1 = fname; | ||
| fname1 += ".ind"; | ||
| print_var_indexes(fname1.c_str()); |
There was a problem hiding this comment.
should be print_var_indexes(fname+".ind") and print_var_indexes should take const std::string & argument and also be renamed to print_var_indices
src/ic3/build_prob/g0en_cnf.cc
Outdated
| @@ -108,11 +108,11 @@ void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version) | |||
| add_truth_table_gate_cubes(H,gate_ind,shift); | |||
| break; | |||
| case COMPLEX: | |||
| printf("complex gates are not allowed\n"); | |||
| exit(1); | |||
| std::cout << "complex gates are not allowed\n"; | |||
There was a problem hiding this comment.
please use custom error stream
src/ic3/build_prob/g2en_cnf.cc
Outdated
| @@ -24,8 +25,8 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com | |||
| ==================================*/ | |||
| void CompInfo::add_constrs() | |||
| { | |||
| printf("adding %d unit constraints\n",(int) (Constr_ilits.size() + | |||
| Constr_nilits.size())); | |||
| std::cout << "adding " << Constr_ilits.size() + Constr_nilits.size() | |||
There was a problem hiding this comment.
please use custom status output stream
src/ic3/build_prob/g2en_cnf.cc
Outdated
| { | ||
|
|
||
|
|
||
| FILE *fp = fopen(fname,"w"); | ||
| assert(fp != NULL); | ||
| std::ofstream Out_str(fname,std::ios::out); |
There was a problem hiding this comment.
variables should be lowercase
src/ic3/build_prob/g2en_cnf.cc
Outdated
| Out_str << "topological level " << i << "\n"; | ||
| CUBE &Gates = topol_levels[i]; | ||
| for (size_t j=0; j < Gates.size(); j++) { | ||
| int gate_ind = Gates[j]; |
src/ic3/s1tat.cc
Outdated
| Tf.num_bnd_cls,tf_lind+1, | ||
| Time_frames[tf_lind+1].num_bnd_cls); | ||
| std::cout << "new derived clauses Bnd[" << tf_lind <<"]=" << Tf.num_bnd_cls | ||
| << ", Bnd[" << tf_lind+1 << "]=" |
src/ic3/seq_circ/a3dd_gate.cc
Outdated
| } | ||
|
|
||
| for(size_t i=0;i < Buff.str().size();i++) | ||
| fake_name.push_back(Buff.str()[i]); |
There was a problem hiding this comment.
fake_name+=std::to_string(ind), remove Buff
src/ic3/seq_circ/a5dd_spec_buffs.cc
Outdated
| Gate &G = N->get_gate(gate_ind); | ||
|
|
||
| assert(G.spec_buff_ind >= 0); | ||
|
|
||
| sprintf(buff,"%d",G.spec_buff_ind); | ||
| Buff << G.spec_buff_ind; |
There was a problem hiding this comment.
use const cstd::string s(std::to_string(G.spec_buff_ind))
src/ic3/seq_circ/a5dd_spec_buffs.cc
Outdated
| Buff << G.spec_buff_ind; | ||
|
|
||
| for(size_t i=0;i < Buff.str().size();i++) | ||
| Name.push_back(Buff.str()[i]); |
src/ic3/i2nit_sat_solvers.cc
Outdated
|
|
||
| std::ostringstream Buff; | ||
| Buff << "Tf_sat" << tf_ind; | ||
| std::string Slv_name = Buff.str(); |
There was a problem hiding this comment.
use std::string slv_name("Tf_sat"+std::to_string(tf_ind));
|
Strange.
All ic3_? regression tests finish successfully on my computer
(after running 'make test' in 'ebmc' directory).
Eugene
…On Mon, Jul 3, 2017 at 3:16 PM, Matthias Güdemann ***@***.***> wrote:
***@***.**** requested changes on this pull request.
there are some recurring changes, in particular for what was char[...]
before and is std::string now that can be simplified. It seems that this
was mainly to format some intergal values, this can be don easily using
std::to_string(...) to get a string, no need to create an
std::ostringstream and call .str() on it.
also, all ic3_? regression tests fail, e.g., ic3_1 with
~/s/d/h/r/e/ic3_1 (new_ic3_bugs) $ ebmc pdtvispeterson.sv --ic3
Parsing pdtvispeterson.sv
Converting
Type-checking Verilog::pdtvispeterson
Using module `pdtvispeterson'
Generating Netlist
fish: “ebmc pdtvispeterson.sv --ic3” terminated by signal SIGSEGV (Address boundary error)
------------------------------
In src/ic3/build_prob/g0en_cnf.cc
<#22 (comment)>:
>
if (print_flag) {
// print index file
- strcpy(fname1,fname);
- strcat(fname1,".ind");
- print_var_indexes(fname1);
+ fname1 = fname;
+ fname1 += ".ind";
+ print_var_indexes(fname1.c_str());
should be print_var_indexes(fname+".ind") and print_var_indexes should
take const std::string & argument and also be renamed to print_var_indices
------------------------------
In src/ic3/build_prob/g0en_cnf.cc
<#22 (comment)>:
> @@ -108,11 +108,11 @@ void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version)
add_truth_table_gate_cubes(H,gate_ind,shift);
break;
case COMPLEX:
- printf("complex gates are not allowed\n");
- exit(1);
+ std::cout << "complex gates are not allowed\n";
please use custom error stream
------------------------------
In src/ic3/build_prob/g2en_cnf.cc
<#22 (comment)>:
> @@ -24,8 +25,8 @@ Author: Eugene Goldberg, ***@***.***
==================================*/
void CompInfo::add_constrs()
{
- printf("adding %d unit constraints\n",(int) (Constr_ilits.size() +
- Constr_nilits.size()));
+ std::cout << "adding " << Constr_ilits.size() + Constr_nilits.size()
please use custom status output stream
------------------------------
In src/ic3/build_prob/g2en_cnf.cc
<#22 (comment)>:
> {
- FILE *fp = fopen(fname,"w");
- assert(fp != NULL);
+ std::ofstream Out_str(fname,std::ios::out);
variables should be lowercase
------------------------------
In src/ic3/build_prob/g2en_cnf.cc
<#22 (comment)>:
> - default: assert(false);
- }
- fprint_name(fp,G.Gate_name);
- fprintf(fp," %d\n",Gate_to_var[gate_ind]);
- int tmp = Gate_to_var[gate_ind];
- if (marked_vars[tmp] != 0)
- {fprintf(fp,"variable %d is shared!!\n",tmp);
- }
- marked_vars[tmp] = 1;
+ // print var indexes in topological order
+ for (size_t i=0; i <= N->max_levels; i++) {
+ Out_str << "--------------------------------------\n";
+ Out_str << "topological level " << i << "\n";
+ CUBE &Gates = topol_levels[i];
+ for (size_t j=0; j < Gates.size(); j++) {
+ int gate_ind = Gates[j];
should be unsigned
------------------------------
In src/ic3/build_prob/g2en_cnf.cc
<#22 (comment)>:
> }
- }
- fclose(fp);
+ fprint_name(Out_str,G.Gate_name);
+ Out_str << " " << Gate_to_var[gate_ind] << "\n";
+ int tmp = Gate_to_var[gate_ind];
+ if (marked_vars[tmp] != 0)
+ Out_str << "variable " << tmp << " is shared!!\n";
why is this indented differently?
------------------------------
In src/ic3/i1nit.cc
<#22 (comment)>:
> @@ -165,9 +165,11 @@ void CompInfo::form_bad_states0(CNF &Bstates)
int var_ind1 = Pres_to_next[var_ind];
if (var_ind1 < 0) {
p();
- printf("Pres_svars.size() = %d\n",(int) Pres_svars.size());
- printf("Next_svars.size() = %d\n",(int) Next_svars.size());
- exit(100);
+ std::cout << "Pres_svars.size() = " << Pres_svars.size()
+ << std::endl;
+ std::cout << "Next_svars.size() = " << Next_svars.size()
+ << std::endl;
please use custom status stream, does not have to be broken down into two
outputs
------------------------------
In src/ic3/m4y_aiger_print.cc
<#22 (comment)>:
> @@ -34,24 +35,27 @@ void CompInfo::print_aiger_format()
check_circuit(num_buffs,num_consts);
assert(num_consts <= 2);
std::string full_name;
- assert(strlen(out_file) > 0);
+ assert(out_file.size() > 0);
please use !....empty()
------------------------------
In src/ic3/o1utput.cc
<#22 (comment)>:
> @@ -24,9 +25,8 @@ Author: Eugene Goldberg, ***@***.***
void CompInfo::fprint_cex2()
{
- char fname[MAX_NAME];
- strcpy(fname,out_file);
- strcat(fname,".cex.cnf");
+ std::string fname = out_file;
+ fname += ".cex.cnf";
do std::string fname(outfile+".cex.cnf");
------------------------------
In src/ic3/o1utput.cc
<#22 (comment)>:
> @@ -41,24 +41,26 @@ void CompInfo::fprint_cex2()
void CompInfo::fprint_cex1()
{
- char fname[MAX_NAME];
- strcpy(fname,out_file);
- strcat(fname,".cex.txt");
- FILE *fp = fopen(fname,"w");
- assert(fp != NULL);
+ std::string fname = out_file;
+ fname += ".cex.txt";
as above
------------------------------
In src/ic3/o1utput.cc
<#22 (comment)>:
> @@ -78,10 +80,10 @@ void CompInfo::print_invariant(bool only_new_clauses)
if (Cex.size() == 0)
assert(Time_frames[inv_ind].num_bnd_cls == 0);
add_dnf(Res,H);
- char fname[MAX_NAME];
- strcpy(fname,out_file);
- if (inv_ind < 0) strcat(fname,".clauses.cnf");
- else strcat(fname,".inv.cnf");
+ std::string fname = out_file;
fname(out_file)
------------------------------
In src/ic3/o1utput.cc
<#22 (comment)>:
> @@ -95,9 +97,8 @@ void CompInfo::print_fclauses()
{
- char fname[MAX_NAME];
- strcpy(fname,out_file);
- strcat(fname,".clauses.cnf");
+ std::string fname = out_file;
+ fname += ".clauses.cnf";
as above
------------------------------
In src/ic3/r1ead_input.cc
<#22 (comment)>:
> assert(found);
- assert(Prop.expr.id()==ID_sva_always);
+
+ if (Prop.expr.id()!=ID_sva_always) {
ID_AG ?
------------------------------
In src/ic3/r1ead_input.cc
<#22 (comment)>:
> @@ -256,3 +252,17 @@ void conv_to_vect(CCUBE &Name1,std::string &Name0)
} /* end of function conv_to_vect */
+/*===============================
+
+ C O N V _ T O _ V E C T
+
+ =============================*/
+void conv_to_vect(CCUBE &Name1,const std::string &Name0)
+{
+ Name1.clear();
+ for (size_t i=0; i < Name0.size(); i++)
+ Name1.push_back(Name0[i]);
+
please do std::string s(name1.begin(), name1.end()); and return the
string and append if needed, instead of using the side effect.
------------------------------
In src/ic3/r6ead_input.cc
<#22 (comment)>:
>
- strcat(fname,".cnstr");
+ fname += ".cnstr";
as above, use std::string fname(source_name+".cnstr")
------------------------------
In src/ic3/r6ead_input.cc
<#22 (comment)>:
> @@ -131,9 +127,9 @@ void ic3_enginet::form_orig_names()
irep_idt Lname = it->first;
std::string Sname = short_name(Lname);
if (var.bits.size() > 1) {
- char buf[100];
- sprintf(buf,"[%zu]",j);
- Sname += buf;
+ std::ostringstream Buff;
+ Buff << "[" << j << "]";
+ Sname += Buff.str();
Sname+="[]"+std::to_string(j)+"]";
------------------------------
In src/ic3/s1tat.cc
<#22 (comment)>:
> }
TimeFrame &Tf = Time_frames[tf_lind];
if (verbose > 0)
- printf("new derived clauses Bnd[%d]=%d, Bnd[%d]=%d\n",tf_lind,
- Tf.num_bnd_cls,tf_lind+1,
- Time_frames[tf_lind+1].num_bnd_cls);
+ std::cout << "new derived clauses Bnd[" << tf_lind <<"]=" << Tf.num_bnd_cls
+ << ", Bnd[" << tf_lind+1 << "]="
is this a \tab?
------------------------------
In src/ic3/seq_circ/a3dd_gate.cc
<#22 (comment)>:
>
- for(int i=0; ;i++) {
- if (buf[i] == 0) break;
- fake_name.push_back(buf[i]);
- }
-
+ for(size_t i=0;i < Buff.str().size();i++)
+ fake_name.push_back(Buff.str()[i]);
fake_name+=std::to_string(ind), remove Buff
------------------------------
In src/ic3/seq_circ/a5dd_spec_buffs.cc
<#22 (comment)>:
> Gate &G = N->get_gate(gate_ind);
assert(G.spec_buff_ind >= 0);
- sprintf(buff,"%d",G.spec_buff_ind);
+ Buff << G.spec_buff_ind;
use const cstd::string s(std::to_string(G.spec_buff_ind))
------------------------------
In src/ic3/seq_circ/a5dd_spec_buffs.cc
<#22 (comment)>:
> Gate &G = N->get_gate(gate_ind);
assert(G.spec_buff_ind >= 0);
- sprintf(buff,"%d",G.spec_buff_ind);
+ Buff << G.spec_buff_ind;
+
+ for(size_t i=0;i < Buff.str().size();i++)
+ Name.push_back(Buff.str()[i]);
Buff.str() -> s
------------------------------
In src/ic3/i2nit_sat_solvers.cc
<#22 (comment)>:
> @@ -101,9 +102,13 @@ void CompInfo::init_time_frame_solver(int tf_ind)
{
SatSolver &Slvr = Time_frames[tf_ind].Slvr;
- char Name[MAX_NAME];
- sprintf(Name,"Tf_sat%d",tf_ind);
- std::string Slv_name = Name;
+
+
+ std::ostringstream Buff;
+ Buff << "Tf_sat" << tf_ind;
+ std::string Slv_name = Buff.str();
use std::string slv_name("Tf_sat"+std::to_string(tf_ind));
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#22 (review)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCs-H5vgeQSA9KBXCoeZDuc-poAQAks5sKT3wgaJpZM4OL9R8>
.
|
|
I have made changes that Daniel and Matthias recommended except for one
thing. The code still has variables with capitalized names (used to name
classes and arrays as opposed to variables of basic types). If need be I
will get rid of capitalized names.
One more thing that I have not done yet is to groom the code to satisfy
'cpplint.py'.
…On Mon, Jul 3, 2017 at 3:16 PM, Matthias Güdemann ***@***.***> wrote:
***@***.**** requested changes on this pull request.
there are some recurring changes, in particular for what was char[...]
before and is std::string now that can be simplified. It seems that this
was mainly to format some intergal values, this can be don easily using
std::to_string(...) to get a string, no need to create an
std::ostringstream and call .str() on it.
also, all ic3_? regression tests fail, e.g., ic3_1 with
~/s/d/h/r/e/ic3_1 (new_ic3_bugs) $ ebmc pdtvispeterson.sv --ic3
Parsing pdtvispeterson.sv
Converting
Type-checking Verilog::pdtvispeterson
Using module `pdtvispeterson'
Generating Netlist
fish: “ebmc pdtvispeterson.sv --ic3” terminated by signal SIGSEGV (Address boundary error)
------------------------------
In src/ic3/build_prob/g0en_cnf.cc
<#22 (comment)>:
>
if (print_flag) {
// print index file
- strcpy(fname1,fname);
- strcat(fname1,".ind");
- print_var_indexes(fname1);
+ fname1 = fname;
+ fname1 += ".ind";
+ print_var_indexes(fname1.c_str());
should be print_var_indexes(fname+".ind") and print_var_indexes should
take const std::string & argument and also be renamed to print_var_indices
------------------------------
In src/ic3/build_prob/g0en_cnf.cc
<#22 (comment)>:
> @@ -108,11 +108,11 @@ void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version)
add_truth_table_gate_cubes(H,gate_ind,shift);
break;
case COMPLEX:
- printf("complex gates are not allowed\n");
- exit(1);
+ std::cout << "complex gates are not allowed\n";
please use custom error stream
------------------------------
In src/ic3/build_prob/g2en_cnf.cc
<#22 (comment)>:
> @@ -24,8 +25,8 @@ Author: Eugene Goldberg, ***@***.***
==================================*/
void CompInfo::add_constrs()
{
- printf("adding %d unit constraints\n",(int) (Constr_ilits.size() +
- Constr_nilits.size()));
+ std::cout << "adding " << Constr_ilits.size() + Constr_nilits.size()
please use custom status output stream
------------------------------
In src/ic3/build_prob/g2en_cnf.cc
<#22 (comment)>:
> {
- FILE *fp = fopen(fname,"w");
- assert(fp != NULL);
+ std::ofstream Out_str(fname,std::ios::out);
variables should be lowercase
------------------------------
In src/ic3/build_prob/g2en_cnf.cc
<#22 (comment)>:
> - default: assert(false);
- }
- fprint_name(fp,G.Gate_name);
- fprintf(fp," %d\n",Gate_to_var[gate_ind]);
- int tmp = Gate_to_var[gate_ind];
- if (marked_vars[tmp] != 0)
- {fprintf(fp,"variable %d is shared!!\n",tmp);
- }
- marked_vars[tmp] = 1;
+ // print var indexes in topological order
+ for (size_t i=0; i <= N->max_levels; i++) {
+ Out_str << "--------------------------------------\n";
+ Out_str << "topological level " << i << "\n";
+ CUBE &Gates = topol_levels[i];
+ for (size_t j=0; j < Gates.size(); j++) {
+ int gate_ind = Gates[j];
should be unsigned
------------------------------
In src/ic3/build_prob/g2en_cnf.cc
<#22 (comment)>:
> }
- }
- fclose(fp);
+ fprint_name(Out_str,G.Gate_name);
+ Out_str << " " << Gate_to_var[gate_ind] << "\n";
+ int tmp = Gate_to_var[gate_ind];
+ if (marked_vars[tmp] != 0)
+ Out_str << "variable " << tmp << " is shared!!\n";
why is this indented differently?
------------------------------
In src/ic3/i1nit.cc
<#22 (comment)>:
> @@ -165,9 +165,11 @@ void CompInfo::form_bad_states0(CNF &Bstates)
int var_ind1 = Pres_to_next[var_ind];
if (var_ind1 < 0) {
p();
- printf("Pres_svars.size() = %d\n",(int) Pres_svars.size());
- printf("Next_svars.size() = %d\n",(int) Next_svars.size());
- exit(100);
+ std::cout << "Pres_svars.size() = " << Pres_svars.size()
+ << std::endl;
+ std::cout << "Next_svars.size() = " << Next_svars.size()
+ << std::endl;
please use custom status stream, does not have to be broken down into two
outputs
------------------------------
In src/ic3/m4y_aiger_print.cc
<#22 (comment)>:
> @@ -34,24 +35,27 @@ void CompInfo::print_aiger_format()
check_circuit(num_buffs,num_consts);
assert(num_consts <= 2);
std::string full_name;
- assert(strlen(out_file) > 0);
+ assert(out_file.size() > 0);
please use !....empty()
------------------------------
In src/ic3/o1utput.cc
<#22 (comment)>:
> @@ -24,9 +25,8 @@ Author: Eugene Goldberg, ***@***.***
void CompInfo::fprint_cex2()
{
- char fname[MAX_NAME];
- strcpy(fname,out_file);
- strcat(fname,".cex.cnf");
+ std::string fname = out_file;
+ fname += ".cex.cnf";
do std::string fname(outfile+".cex.cnf");
------------------------------
In src/ic3/o1utput.cc
<#22 (comment)>:
> @@ -41,24 +41,26 @@ void CompInfo::fprint_cex2()
void CompInfo::fprint_cex1()
{
- char fname[MAX_NAME];
- strcpy(fname,out_file);
- strcat(fname,".cex.txt");
- FILE *fp = fopen(fname,"w");
- assert(fp != NULL);
+ std::string fname = out_file;
+ fname += ".cex.txt";
as above
------------------------------
In src/ic3/o1utput.cc
<#22 (comment)>:
> @@ -78,10 +80,10 @@ void CompInfo::print_invariant(bool only_new_clauses)
if (Cex.size() == 0)
assert(Time_frames[inv_ind].num_bnd_cls == 0);
add_dnf(Res,H);
- char fname[MAX_NAME];
- strcpy(fname,out_file);
- if (inv_ind < 0) strcat(fname,".clauses.cnf");
- else strcat(fname,".inv.cnf");
+ std::string fname = out_file;
fname(out_file)
------------------------------
In src/ic3/o1utput.cc
<#22 (comment)>:
> @@ -95,9 +97,8 @@ void CompInfo::print_fclauses()
{
- char fname[MAX_NAME];
- strcpy(fname,out_file);
- strcat(fname,".clauses.cnf");
+ std::string fname = out_file;
+ fname += ".clauses.cnf";
as above
------------------------------
In src/ic3/r1ead_input.cc
<#22 (comment)>:
> assert(found);
- assert(Prop.expr.id()==ID_sva_always);
+
+ if (Prop.expr.id()!=ID_sva_always) {
ID_AG ?
------------------------------
In src/ic3/r1ead_input.cc
<#22 (comment)>:
> @@ -256,3 +252,17 @@ void conv_to_vect(CCUBE &Name1,std::string &Name0)
} /* end of function conv_to_vect */
+/*===============================
+
+ C O N V _ T O _ V E C T
+
+ =============================*/
+void conv_to_vect(CCUBE &Name1,const std::string &Name0)
+{
+ Name1.clear();
+ for (size_t i=0; i < Name0.size(); i++)
+ Name1.push_back(Name0[i]);
+
please do std::string s(name1.begin(), name1.end()); and return the
string and append if needed, instead of using the side effect.
------------------------------
In src/ic3/r6ead_input.cc
<#22 (comment)>:
>
- strcat(fname,".cnstr");
+ fname += ".cnstr";
as above, use std::string fname(source_name+".cnstr")
------------------------------
In src/ic3/r6ead_input.cc
<#22 (comment)>:
> @@ -131,9 +127,9 @@ void ic3_enginet::form_orig_names()
irep_idt Lname = it->first;
std::string Sname = short_name(Lname);
if (var.bits.size() > 1) {
- char buf[100];
- sprintf(buf,"[%zu]",j);
- Sname += buf;
+ std::ostringstream Buff;
+ Buff << "[" << j << "]";
+ Sname += Buff.str();
Sname+="[]"+std::to_string(j)+"]";
------------------------------
In src/ic3/s1tat.cc
<#22 (comment)>:
> }
TimeFrame &Tf = Time_frames[tf_lind];
if (verbose > 0)
- printf("new derived clauses Bnd[%d]=%d, Bnd[%d]=%d\n",tf_lind,
- Tf.num_bnd_cls,tf_lind+1,
- Time_frames[tf_lind+1].num_bnd_cls);
+ std::cout << "new derived clauses Bnd[" << tf_lind <<"]=" << Tf.num_bnd_cls
+ << ", Bnd[" << tf_lind+1 << "]="
is this a \tab?
------------------------------
In src/ic3/seq_circ/a3dd_gate.cc
<#22 (comment)>:
>
- for(int i=0; ;i++) {
- if (buf[i] == 0) break;
- fake_name.push_back(buf[i]);
- }
-
+ for(size_t i=0;i < Buff.str().size();i++)
+ fake_name.push_back(Buff.str()[i]);
fake_name+=std::to_string(ind), remove Buff
------------------------------
In src/ic3/seq_circ/a5dd_spec_buffs.cc
<#22 (comment)>:
> Gate &G = N->get_gate(gate_ind);
assert(G.spec_buff_ind >= 0);
- sprintf(buff,"%d",G.spec_buff_ind);
+ Buff << G.spec_buff_ind;
use const cstd::string s(std::to_string(G.spec_buff_ind))
------------------------------
In src/ic3/seq_circ/a5dd_spec_buffs.cc
<#22 (comment)>:
> Gate &G = N->get_gate(gate_ind);
assert(G.spec_buff_ind >= 0);
- sprintf(buff,"%d",G.spec_buff_ind);
+ Buff << G.spec_buff_ind;
+
+ for(size_t i=0;i < Buff.str().size();i++)
+ Name.push_back(Buff.str()[i]);
Buff.str() -> s
------------------------------
In src/ic3/i2nit_sat_solvers.cc
<#22 (comment)>:
> @@ -101,9 +102,13 @@ void CompInfo::init_time_frame_solver(int tf_ind)
{
SatSolver &Slvr = Time_frames[tf_ind].Slvr;
- char Name[MAX_NAME];
- sprintf(Name,"Tf_sat%d",tf_ind);
- std::string Slv_name = Name;
+
+
+ std::ostringstream Buff;
+ Buff << "Tf_sat" << tf_ind;
+ std::string Slv_name = Buff.str();
use std::string slv_name("Tf_sat"+std::to_string(tf_ind));
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#22 (review)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCs-H5vgeQSA9KBXCoeZDuc-poAQAks5sKT3wgaJpZM4OL9R8>
.
|
|
@eigold starts looking good, please remove the changes to BDD test cases from commit and squash commits according to nature of changes, e.g., |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.