Skip to content

Commit 30f62b9

Browse files
mgudemannmgudemann
committed
Apply clang-format diff
1 parent 675461f commit 30f62b9

File tree

9 files changed

+83
-65
lines changed

9 files changed

+83
-65
lines changed

‎src/ic3/build_prob/g3en_cnf.cc

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,19 +5,20 @@ Module: CNF Generation (Part 4)
55
Author: Eugene Goldberg, eu.goldberg@gmail.com
66
77
******************************************************/
8+
#include <util/invariant.h>
9+
10+
#include "ccircuit.hh"
11+
#include "dnf_io.hh"
12+
#include "m0ic3.hh"
13+
14+
#include <algorithm>
815
#include <iostream>
9-
#include <set>
1016
#include <map>
11-
#include <algorithm>
1217
#include <queue>
13-
#include <util/invariant.h>
18+
#include <set>
1419

1520
#include "minisat/core/Solver.h"
1621
#include "minisat/simp/SimpSolver.h"
17-
#include "dnf_io.hh"
18-
#include "ccircuit.hh"
19-
#include "m0ic3.hh"
20-
2122

2223
/*=======================================
2324

‎src/ic3/e4xclude_state.cc

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6,17 +6,20 @@ Module: Excludes a state from which a bad state is
66
Author: Eugene Goldberg, eu.goldberg@gmail.com
77
88
******************************************************/
9-
#include <queue>
10-
#include <set>
11-
#include <map>
9+
#include <util/invariant.h>
10+
11+
#include "ccircuit.hh"
12+
#include "dnf_io.hh"
13+
#include "m0ic3.hh"
14+
1215
#include <algorithm>
1316
#include <iostream>
14-
#include <util/invariant.h>
17+
#include <map>
18+
#include <queue>
19+
#include <set>
20+
1521
#include "minisat/core/Solver.h"
1622
#include "minisat/simp/SimpSolver.h"
17-
#include "dnf_io.hh"
18-
#include "ccircuit.hh"
19-
#include "m0ic3.hh"
2023

2124
/*=========================================
2225
@@ -92,8 +95,7 @@ void CompInfo::form_res_cnf(CNF &G,int tf_ind,CUBE &St_cube)
9295
add_assumps1(Assmps,St_cube);
9396

9497
bool sat_form = Slvr.Mst->solve(Assmps);
95-
INVARIANT(sat_form == false,
96-
"SAT check should fail here.");
98+
INVARIANT(sat_form == false, "SAT check should fail here.");
9799
CLAUSE C;
98100
gen_assump_clause(C,Slvr,Assmps);
99101
G.push_back(C);

‎src/ic3/i1nit.cc

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,20 @@ Module: Initialization of IC3
55
Author: Eugene Goldberg, eu.goldberg@gmail.com
66
77
******************************************************/
8+
#include <util/invariant.h>
9+
10+
#include "ccircuit.hh"
11+
#include "dnf_io.hh"
12+
#include "m0ic3.hh"
13+
14+
#include <algorithm>
815
#include <iostream>
16+
#include <map>
917
#include <queue>
1018
#include <set>
11-
#include <map>
12-
#include <algorithm>
13-
#include <util/invariant.h>
19+
1420
#include "minisat/core/Solver.h"
1521
#include "minisat/simp/SimpSolver.h"
16-
#include "dnf_io.hh"
17-
#include "ccircuit.hh"
18-
#include "m0ic3.hh"
1922
/*==============================
2023
2124
C I _ I N I T

‎src/ic3/i2nit_sat_solvers.cc

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,16 +5,19 @@ Module: Initialization of Sat-solvers (Part 1)
55
Author: Eugene Goldberg, eu.goldberg@gmail.com
66
77
******************************************************/
8+
#include <util/invariant.h>
9+
10+
#include "ccircuit.hh"
11+
#include "dnf_io.hh"
12+
#include "m0ic3.hh"
13+
14+
#include <algorithm>
15+
#include <map>
816
#include <queue>
917
#include <set>
10-
#include <map>
11-
#include <algorithm>
12-
#include <util/invariant.h>
18+
1319
#include "minisat/core/Solver.h"
1420
#include "minisat/simp/SimpSolver.h"
15-
#include "dnf_io.hh"
16-
#include "ccircuit.hh"
17-
#include "m0ic3.hh"
1821

1922
/*======================================
2023
@@ -142,8 +145,8 @@ void CompInfo::init_lbs_sat_solver()
142145
for (size_t i=0; i < Fun_coi_lits.size(); i++) {
143146
int lit = Fun_coi_lits[i];
144147
int var_ind = abs(lit)-1;
145-
INVARIANT(Var_info[var_ind].type == INTERN,
146-
"Type of literal should be INTERN");
148+
INVARIANT(
149+
Var_info[var_ind].type == INTERN, "Type of literal should be INTERN");
147150
U.push_back(-lit);
148151
}
149152

‎src/ic3/my_printf.cc

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,18 @@ Module: Structuring the output of large numbers by
66
Author: Eugene Goldberg, eu.goldberg@gmail.com
77
88
******************************************************/
9+
#include <util/invariant.h>
10+
11+
#include "dnf_io.hh"
12+
13+
#include <algorithm>
914
#include <assert.h>
15+
#include <iostream>
16+
#include <map>
17+
#include <queue>
18+
#include <set>
1019
#include <stdarg.h>
1120
#include <stdio.h>
12-
#include <set>
13-
#include <algorithm>
14-
#include <queue>
15-
#include <map>
16-
#include <iostream>
17-
#include <util/invariant.h>
18-
#include "dnf_io.hh"
1921
const int factor = 1000;
2022

2123
/*================================================

‎src/ic3/p5ick_lit.cc

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -6,18 +6,20 @@ Module: Picking a literal to remove when generalizing
66
Author: Eugene Goldberg, eu.goldberg@gmail.com
77
88
******************************************************/
9-
#include <queue>
10-
#include <set>
11-
#include <map>
12-
#include <algorithm>
13-
#include <iostream>
149
#include <util/invariant.h>
15-
#include "minisat/core/Solver.h"
16-
#include "minisat/simp/SimpSolver.h"
17-
#include "dnf_io.hh"
10+
1811
#include "ccircuit.hh"
12+
#include "dnf_io.hh"
1913
#include "m0ic3.hh"
2014

15+
#include <algorithm>
16+
#include <iostream>
17+
#include <map>
18+
#include <queue>
19+
#include <set>
20+
21+
#include "minisat/core/Solver.h"
22+
#include "minisat/simp/SimpSolver.h"
2123

2224
/*=============================
2325

‎src/ic3/r0ead_input.cc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,7 @@ void ic3_enginet::form_inputs()
128128
CCUBE Name;
129129
if (orig_names) {
130130
bool ok = form_orig_name(Name,lit);
131-
INVARIANT(ok, "Literal should have an original name.");
131+
INVARIANT(ok, "Literal should have an original name.");
132132
}
133133
else {
134134
char Inp_name[MAX_NAME];

‎src/ic3/s2horten_clause.cc

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,20 @@ Module: Generalization of an inductive clause
55
Author: Eugene Goldberg, eu.goldberg@gmail.com
66
77
******************************************************/
8-
#include <queue>
9-
#include <set>
10-
#include <map>
8+
#include <util/invariant.h>
9+
10+
#include "ccircuit.hh"
11+
#include "dnf_io.hh"
12+
#include "m0ic3.hh"
13+
1114
#include <algorithm>
1215
#include <iostream>
13-
#include <util/invariant.h>
16+
#include <map>
17+
#include <queue>
18+
#include <set>
19+
1420
#include "minisat/core/Solver.h"
1521
#include "minisat/simp/SimpSolver.h"
16-
#include "dnf_io.hh"
17-
#include "ccircuit.hh"
18-
#include "m0ic3.hh"
1922

2023
/*==================================
2124
@@ -87,7 +90,7 @@ void CompInfo::find_fixed_pnt(CLAUSE &C,CLAUSE &C0,SatSolver &Slvr,
8790
// run a SAT-check
8891

8992
bool sat_form = check_sat2(Slvr,Assmps);
90-
93+
9194
INVARIANT(sat_form == false, "SAT check should fail here.");
9295
CLAUSE B;
9396
gen_assump_clause(B,Slvr,Assmps);

‎src/ic3/seq_circ/a4dd_spec_buffs.cc

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -6,19 +6,20 @@ Module: Treating the case when a gate feeds more
66
Author: Eugene Goldberg, eu.goldberg@gmail.com
77
88
******************************************************/
9+
#include <util/invariant.h>
10+
11+
#include "ccircuit.hh"
12+
#include "dnf_io.hh"
13+
14+
#include <algorithm>
15+
#include <assert.h>
916
#include <iostream>
10-
#include <vector>
11-
#include <set>
1217
#include <map>
13-
#include <algorithm>
1418
#include <queue>
15-
#include <assert.h>
16-
#include <string.h>
19+
#include <set>
1720
#include <stdio.h>
18-
#include <util/invariant.h>
19-
#include "dnf_io.hh"
20-
#include "ccircuit.hh"
21-
21+
#include <string.h>
22+
#include <vector>
2223

2324
/*=========================================
2425
@@ -122,8 +123,9 @@ int spec_buff_gate_ind(Circuit *N,int ind)
122123
int gate_ind = N->Pin_list[fake_name];
123124

124125
Gate &G = N->get_gate(gate_ind);
125-
INVARIANT(G.spec_buff_ind == ind,
126-
"Special buffer index of gate should be equal to value of `ind`");
126+
INVARIANT(
127+
G.spec_buff_ind == ind,
128+
"Special buffer index of gate should be equal to value of `ind`");
127129

128130
return(gate_ind);
129131

0 commit comments

Comments
 (0)