You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is Siddharth here. I am requesting an enhancement for this as discussed.
int get_resource(const char * name); // name = "conflicts"/"decisions"
This would be useful in an example incremental flow as shown below,
solver->limit("conflicts",);
solver->limit("decisions",);
//Add clauses
solver->assume(..);
int conflicts,decisions;
if ( solver->solve() == 0 ) { //aborted due to resource limit
conflicts = solver->get_resource("conflicts");
decisionss = solver->get_resource("decisions");
}
//Adjust limits based on conflicts/decisions reached before next incremental call
I was able to get this info with a minor change in solver.cpp (get_resource declared in cadical.hpp)
int Solver::get_resource (const char * arg) {
if ( !is_valid_limit(arg) ) return 0;
//strcmp returns 0 if strings are equal
if ( strcmp(arg,"conflicts") == 0 ) return internal->stats.conflicts;
if ( strcmp(arg,"decisions") == 0 ) return internal->stats.decisions;
return 0;
}
Thanks
The text was updated successfully, but these errors were encountered:
Hi Armin,
This is Siddharth here. I am requesting an enhancement for this as discussed.
int get_resource(const char * name); // name = "conflicts"/"decisions"
This would be useful in an example incremental flow as shown below,
solver->limit("conflicts",);
solver->limit("decisions",);
//Add clauses
solver->assume(..);
int conflicts,decisions;
if ( solver->solve() == 0 ) { //aborted due to resource limit
conflicts = solver->get_resource("conflicts");
decisionss = solver->get_resource("decisions");
}
//Adjust limits based on conflicts/decisions reached before next incremental call
I was able to get this info with a minor change in solver.cpp (get_resource declared in cadical.hpp)
Thanks
The text was updated successfully, but these errors were encountered: