Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Kučera Petr RNDr. Ph.D.
PCCompile
Commits
92078159
Commit
92078159
authored
Sep 03, 2021
by
Kučera Petr RNDr. Ph.D.
Browse files
timeouts changed to long double
parent
efaa4001
Changes
7
Hide whitespace changes
Inline
Side-by-side
bin/pccheck.cpp
View file @
92078159
...
...
@@ -444,28 +444,6 @@ input(const config_t &conf, SUBool::CNF *cnf)
return
0
;
}
template
<
class
T
,
class
R
>
R
wait_with_timeout
(
double
timeout
,
std
::
future
<
R
>
&
fut
,
T
&
comp
)
{
if
(
timeout
>
0.0
)
{
if
(
fut
.
wait_for
(
std
::
chrono
::
duration
<
double
>
(
timeout
))
==
std
::
future_status
::
timeout
)
{
comp
.
Abort
(
"timed out"
);
comp
.
PrintStatistics
(
1
);
fut
.
wait
();
return
SUBool
::
AbsComp
::
RESULT
::
TIMED_OUT
;
//_Exit(3);
}
}
else
{
fut
.
wait
();
}
return
fut
.
get
();
}
int
encode
(
const
config_t
&
conf
,
const
SUBool
::
CompHypothesis
&
hyp
,
SUBool
::
AbsCheckerSAT
&
checker
)
...
...
bin/pccompile.cpp
View file @
92078159
...
...
@@ -53,7 +53,7 @@ struct config_t
SUBool
::
PCLearnComp
::
INITIAL_NEGATIVES
initial_negatives
{
SUBool
::
PCLearnComp
::
INITIAL_NEGATIVES
::
ALL_EMPOWERING
};
unsigned
long
long
random_seed
{
0
};
double
timeout
{
-
1.0
};
long
double
timeout
{
-
1.0
};
SUBool
::
AbsComp
::
BaseConfig
comp_base_config
{
SUBool
::
PCEncoder
::
UP_EMPOWER
::
ONE_LEVEL
,
50
,
...
...
@@ -628,11 +628,11 @@ input(const config_t &conf, SUBool::CNF *cnf)
template
<
class
T
,
class
R
>
R
wait_with_timeout
(
double
timeout
,
std
::
future
<
R
>
&
fut
,
T
&
comp
)
wait_with_timeout
(
long
double
timeout
,
std
::
future
<
R
>
&
fut
,
T
&
comp
)
{
if
(
timeout
>
0.0
)
{
if
(
fut
.
wait_for
(
std
::
chrono
::
duration
<
double
>
(
timeout
))
if
(
fut
.
wait_for
(
std
::
chrono
::
duration
<
long
double
>
(
timeout
))
==
std
::
future_status
::
timeout
)
{
comp
.
Abort
(
"timed out"
);
...
...
bin/pcminimize.cpp
View file @
92078159
...
...
@@ -42,7 +42,7 @@ struct config_t
SUBool
::
MINIMIZE_METHOD
minimize_method
{
SUBool
::
MINIMIZE_METHOD
::
FULL
};
bool
backbones
{
false
};
// Whether backbones should be propagated
bool
prime
{
false
};
// make prime before minimization
double
timeout
{
-
1.0
};
long
double
timeout
{
-
1.0
l
};
};
void
...
...
@@ -75,7 +75,7 @@ parse_arguments(int argc, char *argv[])
(
"prime,p"
,
po
::
bool_switch
(
&
conf
.
prime
),
"Make CNF prime before running the minimization (this implies using "
"backbone propagation)"
)
//
(
"timeout,t"
,
po
::
value
<
double
>
(
&
conf
.
timeout
),
(
"timeout,t"
,
po
::
value
<
long
double
>
(
&
conf
.
timeout
),
"Timeout for compilation in seconds as a fractional number. After "
"this amount of seconds, the process finishes. Value t<=0.0 means "
"no timeout. The timer uses CLOCK_REALTIME."
);
...
...
@@ -117,11 +117,11 @@ input(const config_t &conf, SUBool::CNF *cnf)
template
<
class
T
,
class
R
>
bool
wait_with_timeout
(
double
timeout
,
std
::
future
<
R
>
&
fut
,
T
&
comp
)
wait_with_timeout
(
long
double
timeout
,
std
::
future
<
R
>
&
fut
,
T
&
comp
)
{
if
(
timeout
>
0.0
)
{
if
(
fut
.
wait_for
(
std
::
chrono
::
duration
<
double
>
(
timeout
))
if
(
fut
.
wait_for
(
std
::
chrono
::
duration
<
long
double
>
(
timeout
))
==
std
::
future_status
::
timeout
)
{
comp
.
Abort
(
"timed out"
);
...
...
@@ -157,7 +157,8 @@ write_output(const config_t &conf, const SUBool::CNF &cnf)
template
<
class
F
>
bool
run_with_timeout
(
bool
no_timeout
,
double
timeout
,
F
f
,
const
std
::
string
&
desc
)
run_with_timeout
(
bool
no_timeout
,
long
double
timeout
,
F
f
,
const
std
::
string
&
desc
)
{
if
(
no_timeout
)
{
...
...
@@ -168,7 +169,7 @@ run_with_timeout(bool no_timeout, double timeout, F f, const std::string &desc)
if
(
timeout
>
0.0
f
)
{
auto
fut
=
std
::
async
(
std
::
launch
::
async
,
f
);
if
(
fut
.
wait_for
(
std
::
chrono
::
duration
<
double
>
(
timeout
))
if
(
fut
.
wait_for
(
std
::
chrono
::
duration
<
long
double
>
(
timeout
))
==
std
::
future_status
::
timeout
)
{
SUBool
::
logs
.
TLog
(
2
)
<<
"Timed out during "
<<
desc
<<
std
::
endl
;
...
...
lib/pc_opt.h
View file @
92078159
...
...
@@ -9,6 +9,8 @@
#ifndef __PC_OPT_H
#define __PC_OPT_H
#include <chrono>
#include "drenc.h"
#include "empower.h"
#include "enum_opt.h"
...
...
@@ -206,6 +208,20 @@ namespace SUBool
unsigned
MinimizeSteps
()
const
;
bool
NoLevelMinimize
()
const
;
};
class
PCTimeoutsOptions
:
public
OptionsGroup
{
AbsCheckerSAT
::
Timeouts
mEmpTimeouts
{};
long
double
mTimeout
{
-
1.0
};
public:
PCTimeoutsOptions
();
virtual
bool
GetValues
()
override
;
const
AbsCheckerSAT
::
Timeouts
&
EmpTimeouts
()
const
;
long
double
Timeout
()
const
;
};
}
// namespace SUBool
inline
auto
...
...
lib/pcchecker.cpp
View file @
92078159
...
...
@@ -27,14 +27,14 @@ SUBool::AbsCheckerSAT::InitBase(unsigned max_up_level_bound,
(
wait_before_max_level_check
?
STATE
::
NO_INCREASE
:
STATE
::
NO_SPLIT
);
}
double
long
double
SUBool
::
AbsCheckerSAT
::
Timeout
(
unsigned
level
)
const
{
double
t
=
mTimeouts
.
timeout
;
auto
t
=
mTimeouts
.
timeout
;
if
(
level
>
0
&&
level
<
mMaxUPLevelBound
&&
mTimeouts
.
level_base
>
0.0
)
{
double
lt
=
mTimeouts
.
level_base
+
static_cast
<
double
>
(
level
-
1
)
*
mTimeouts
.
level_factor
;
auto
lt
=
mTimeouts
.
level_base
+
static_cast
<
double
>
(
level
-
1
)
*
mTimeouts
.
level_factor
;
if
(
t
<
0.0
||
lt
<
t
)
{
t
=
lt
;
...
...
@@ -113,7 +113,8 @@ SUBool::AbsCheckerSAT::FindEmpoweringWithLevel(const CNF &cnf,
}
bool
SUBool
::
AbsCheckerSAT
::
CallSolve
(
SUBool
::
SolverInterface
&
g
,
double
timeout
)
SUBool
::
AbsCheckerSAT
::
CallSolve
(
SUBool
::
SolverInterface
&
g
,
long
double
timeout
)
{
if
(
mState
==
STATE
::
INTERRUPT
)
{
...
...
@@ -122,7 +123,8 @@ SUBool::AbsCheckerSAT::CallSolve(SUBool::SolverInterface &g, double timeout)
mTimedOut
=
false
;
if
(
timeout
>
0.0
)
{
auto
res
=
g
.
SolveWithTimeout
(
std
::
chrono
::
duration
<
double
>
(
timeout
));
auto
res
=
g
.
SolveWithTimeout
(
std
::
chrono
::
duration
<
long
double
>
(
timeout
));
mTimedOut
=
(
res
==
PartialValue
::
UNDEF
);
return
(
res
==
PartialValue
::
TRUE
);
}
...
...
lib/pcchecker.h
View file @
92078159
...
...
@@ -27,17 +27,17 @@ namespace SUBool
public:
struct
Timeouts
{
double
timeout
{
-
1.0
};
double
level_base
{
-
1.0
};
double
level_factor
{
0.0
};
long
double
timeout
{
-
1.0
l
};
long
double
level_base
{
-
1.0
l
};
long
double
level_factor
{
0.0
l
};
};
private:
unsigned
mMaxUPLevelBound
{
0
};
unsigned
mCurrentUPLevelBound
{
1
};
double
mTotalTime
{
0.0
};
double
mTotalTimeSAT
{
0.0
};
double
mTotalTimeUNSAT
{
0.0
};
long
double
mTotalTime
{
0.0
l
};
long
double
mTotalTimeSAT
{
0.0
l
};
long
double
mTotalTimeUNSAT
{
0.0
l
};
unsigned
mSolveCountSAT
{
0
};
unsigned
mSolveCountUNSAT
{
0
};
unsigned
mLastWitnessVariable
{
0
};
...
...
@@ -50,28 +50,26 @@ namespace SUBool
INTERRUPT
};
std
::
atomic
<
STATE
>
mState
{
STATE
::
NO_SPLIT
};
Timeouts
mTimeouts
{
-
1.0
,
-
1.0
,
0.0
};
Timeouts
mTimeouts
{};
bool
mTimedOut
{
false
};
double
Timeout
(
unsigned
level
)
const
;
bool
CallSolve
(
SolverInterface
&
g
,
double
timeout
);
long
double
Timeout
(
unsigned
level
)
const
;
bool
CallSolve
(
SolverInterface
&
g
,
long
double
timeout
);
protected:
void
InitBase
(
unsigned
max_up_level_bound
,
bool
wait_before_max_level_check
,
const
Timeouts
&
timeouts
);
bool
wait_before_max_level_check
,
const
Timeouts
&
timeouts
);
public:
virtual
~
AbsCheckerSAT
()
=
default
;
virtual
std
::
unique_ptr
<
AbsEncoder
>
Encoder
(
unsigned
up_level_bound
)
=
0
;
virtual
std
::
optional
<
Clause
>
FindEmpowering
(
const
CNF
&
cnf
,
const
ClausesToLiterals
&
cl2lit
,
const
LitImplSystem
&
impl_system
,
const
LitISGraph
&
scc_graph
);
std
::
pair
<
std
::
optional
<
Clause
>
,
unsigned
>
FindEmpoweringWithLevel
(
const
CNF
&
cnf
,
const
ClausesToLiterals
&
cl2lit
,
const
LitImplSystem
&
impl_system
,
const
LitISGraph
&
scc_graph
,
unsigned
level
,
bool
assume_sat
);
virtual
std
::
optional
<
Clause
>
FindEmpowering
(
const
CNF
&
cnf
,
const
ClausesToLiterals
&
cl2lit
,
const
LitImplSystem
&
impl_system
,
const
LitISGraph
&
scc_graph
);
std
::
pair
<
std
::
optional
<
Clause
>
,
unsigned
>
FindEmpoweringWithLevel
(
const
CNF
&
cnf
,
const
ClausesToLiterals
&
cl2lit
,
const
LitImplSystem
&
impl_system
,
const
LitISGraph
&
scc_graph
,
unsigned
level
,
bool
assume_sat
);
virtual
bool
RequiresImplSystem
()
const
=
0
;
virtual
bool
RequiresSCCGraph
()
const
=
0
;
virtual
unsigned
CurrentUPLevelBound
()
const
;
...
...
@@ -118,7 +116,7 @@ namespace SUBool
virtual
void
Init
(
typename
T
::
Config
conf
,
bool
wait_before_max_level_check
,
const
Timeouts
&
timeouts
)
const
Timeouts
&
timeouts
)
{
mEncConf
=
std
::
move
(
conf
);
InitBase
(
conf
.
up_level_bound
,
wait_before_max_level_check
,
timeouts
);
...
...
@@ -162,11 +160,10 @@ namespace SUBool
public:
UCPCInterleaveCheckerSAT
()
:
AbsCheckerSAT
(),
mEncConf
(),
mPCEncConf
()
{}
virtual
void
Init
(
UCEncoder
::
Config
uc_enc_conf
,
PCEncoder
::
Config
pc_enc_conf
,
bool
wait_before_max_level_check
,
const
Timeouts
&
timeouts
);
virtual
std
::
unique_ptr
<
AbsEncoder
>
Encoder
(
unsigned
up_level_bound
)
override
;
PCEncoder
::
Config
pc_enc_conf
,
bool
wait_before_max_level_check
,
const
Timeouts
&
timeouts
);
virtual
std
::
unique_ptr
<
AbsEncoder
>
Encoder
(
unsigned
up_level_bound
)
override
;
virtual
bool
RequiresImplSystem
()
const
override
;
virtual
bool
RequiresSCCGraph
()
const
override
;
...
...
lib/task.h
View file @
92078159
...
...
@@ -21,17 +21,17 @@ namespace SUBool
{
CPUTime
mCPUTime
{};
std
::
atomic
<
bool
>
mAborted
{
false
};
std
::
atomic
<
double
>
mTimeout
{
-
1.0
};
std
::
atomic
<
long
double
>
mTimeout
{
-
1.0
l
};
public:
// TODO: Constructors with other budgets
Task
(
double
timeout
)
:
mTimeout
(
timeout
)
{}
Task
(
long
double
timeout
)
:
mTimeout
(
timeout
)
{}
std
::
optional
<
double
>
std
::
optional
<
long
double
>
TimeoutRemains
()
const
{
return
(
mTimeout
>=
0.0
f
?
mTimeout
-
mCPUTime
.
TimeSpan
()
:
std
::
optional
<
double
>
());
return
(
mTimeout
>=
0.0
l
?
mTimeout
-
mCPUTime
.
TimeSpan
()
:
std
::
optional
<
long
double
>
());
}
bool
Aborted
()
const
...
...
@@ -68,7 +68,7 @@ namespace SUBool
template
<
typename
...
Args
>
TaskPtr
new_task
(
Args
&&
...
args
)
new_task
(
Args
&&
...
args
)
{
return
std
::
make_shared
<
Task
>
(
std
::
forward
<
Args
>
(
args
)...);
};
...
...
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