Skip to content
Projects
Groups
Snippets
Help
This project
Loading...
Sign in / Register
Toggle navigation
A
abc
Overview
Overview
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
lvzhengyang
abc
Commits
316238d4
Commit
316238d4
authored
Feb 18, 2017
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Compiler warnings.
parent
429f52ce
Show whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
8 additions
and
8 deletions
+8
-8
src/aig/gia/giaUtil.c
+1
-1
src/sat/satoko/satoko.h
+2
-2
src/sat/satoko/solver_api.c
+5
-5
No files found.
src/aig/gia/giaUtil.c
View file @
316238d4
...
@@ -2063,7 +2063,7 @@ void Gia_AigerWriteLut( Gia_Man_t * p, char * pFileName )
...
@@ -2063,7 +2063,7 @@ void Gia_AigerWriteLut( Gia_Man_t * p, char * pFileName )
***********************************************************************/
***********************************************************************/
void
Gia_ManDetectMuxes
(
Gia_Man_t
*
p
)
void
Gia_ManDetectMuxes
(
Gia_Man_t
*
p
)
{
{
Gia_Obj_t
*
pObj
,
*
pNodeT
,
*
pNodeE
;
int
i
;
Gia_Obj_t
*
pObj
=
NULL
,
*
pNodeT
,
*
pNodeE
;
int
i
;
Gia_ManForEachObj
(
p
,
pObj
,
i
);
Gia_ManForEachObj
(
p
,
pObj
,
i
);
if
(
Gia_ObjIsAnd
(
pObj
)
&&
Gia_ObjRecognizeMux
(
pObj
,
&
pNodeT
,
&
pNodeE
)
)
if
(
Gia_ObjIsAnd
(
pObj
)
&&
Gia_ObjRecognizeMux
(
pObj
,
&
pNodeT
,
&
pNodeE
)
)
pObj
->
fMark0
=
1
;
pObj
->
fMark0
=
1
;
...
...
src/sat/satoko/satoko.h
View file @
316238d4
...
@@ -84,8 +84,8 @@ extern void satoko_default_opts(satoko_opts_t *);
...
@@ -84,8 +84,8 @@ extern void satoko_default_opts(satoko_opts_t *);
extern
void
satoko_configure
(
satoko_t
*
,
satoko_opts_t
*
);
extern
void
satoko_configure
(
satoko_t
*
,
satoko_opts_t
*
);
extern
int
satoko_parse_dimacs
(
char
*
,
satoko_t
**
);
extern
int
satoko_parse_dimacs
(
char
*
,
satoko_t
**
);
extern
int
satoko_add_variable
(
satoko_t
*
,
char
);
extern
int
satoko_add_variable
(
satoko_t
*
,
char
);
extern
int
satoko_add_clause
(
satoko_t
*
,
unsigned
*
,
unsigned
);
extern
int
satoko_add_clause
(
satoko_t
*
,
int
*
,
int
);
extern
void
satoko_assump_push
(
satoko_t
*
s
,
unsigned
);
extern
void
satoko_assump_push
(
satoko_t
*
s
,
int
);
extern
void
satoko_assump_pop
(
satoko_t
*
s
);
extern
void
satoko_assump_pop
(
satoko_t
*
s
);
extern
int
satoko_simplify
(
satoko_t
*
);
extern
int
satoko_simplify
(
satoko_t
*
);
extern
int
satoko_solve
(
satoko_t
*
);
extern
int
satoko_solve
(
satoko_t
*
);
...
...
src/sat/satoko/solver_api.c
View file @
316238d4
...
@@ -234,7 +234,7 @@ int satoko_add_variable(solver_t *s, char sign)
...
@@ -234,7 +234,7 @@ int satoko_add_variable(solver_t *s, char sign)
return
var
;
return
var
;
}
}
int
satoko_add_clause
(
solver_t
*
s
,
unsigned
*
lits
,
unsigned
size
)
int
satoko_add_clause
(
solver_t
*
s
,
int
*
lits
,
int
size
)
{
{
unsigned
i
,
j
;
unsigned
i
,
j
;
unsigned
prev_lit
;
unsigned
prev_lit
;
...
@@ -249,10 +249,10 @@ int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
...
@@ -249,10 +249,10 @@ int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
vec_uint_clear
(
s
->
temp_lits
);
vec_uint_clear
(
s
->
temp_lits
);
j
=
0
;
j
=
0
;
prev_lit
=
UNDEF
;
prev_lit
=
UNDEF
;
for
(
i
=
0
;
i
<
size
;
i
++
)
{
for
(
i
=
0
;
i
<
(
unsigned
)
size
;
i
++
)
{
if
(
lits
[
i
]
==
lit_neg
(
prev_lit
)
||
lit_value
(
s
,
lits
[
i
])
==
LIT_TRUE
)
if
(
(
unsigned
)
lits
[
i
]
==
lit_neg
(
prev_lit
)
||
lit_value
(
s
,
lits
[
i
])
==
LIT_TRUE
)
return
SATOKO_OK
;
return
SATOKO_OK
;
else
if
(
lits
[
i
]
!=
prev_lit
&&
var_value
(
s
,
lit2var
(
lits
[
i
]))
==
VAR_UNASSING
)
{
else
if
(
(
unsigned
)
lits
[
i
]
!=
prev_lit
&&
var_value
(
s
,
lit2var
(
lits
[
i
]))
==
VAR_UNASSING
)
{
prev_lit
=
lits
[
i
];
prev_lit
=
lits
[
i
];
vec_uint_push_back
(
s
->
temp_lits
,
lits
[
i
]);
vec_uint_push_back
(
s
->
temp_lits
,
lits
[
i
]);
}
}
...
@@ -270,7 +270,7 @@ int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
...
@@ -270,7 +270,7 @@ int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
return
SATOKO_OK
;
return
SATOKO_OK
;
}
}
void
satoko_assump_push
(
solver_t
*
s
,
unsigned
lit
)
void
satoko_assump_push
(
solver_t
*
s
,
int
lit
)
{
{
vec_uint_push_back
(
s
->
assumptions
,
lit
);
vec_uint_push_back
(
s
->
assumptions
,
lit
);
}
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment