Stephan Falke
unread,Nov 2, 2011, 11:53:48 AM11/2/11Sign in to reply to author
Sign in to forward
You do not have permission to delete messages in this group
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to stp-users
Hi,
The following patch makes it possible to select a SAT solver in the C
interface.
Kind regards,
Stephan
Index: c_interface.cpp
===================================================================
--- c_interface.cpp (revision 1407)
+++ c_interface.cpp (working copy)
@@ -145,12 +145,30 @@
case EXPRDELETE:
cinterface_exprdelete_on_flag = param_value != 0;
break;
+ case MS:
+ {
+ bmstar b = (bmstar)(((stpstar)vc)->bm);
+ b->UserFlags.solver_to_use =
BEEV::UserDefinedFlags::MINISAT_SOLVER;
+ break;
+ }
+ case SMS:
+ {
+ bmstar b = (bmstar)(((stpstar)vc)->bm);
+ b->UserFlags.solver_to_use =
BEEV::UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER;
+ break;
+ }
case CMS2:
{
bmstar b = (bmstar)(((stpstar)vc)->bm);
b->UserFlags.solver_to_use =
BEEV::UserDefinedFlags::CRYPTOMINISAT_SOLVER;
break;
}
+ case MSP:
+ {
+ bmstar b = (bmstar)(((stpstar)vc)->bm);
+ b->UserFlags.solver_to_use =
BEEV::UserDefinedFlags::MINISAT_PROPAGATORS;
+ break;
+ }
default:
BEEV::FatalError("C_interface: vc_setInterfaceFlags: Unrecognized
flag\n");
break;
Index: c_interface.h
===================================================================
--- c_interface.h (revision 1407)
+++ c_interface.h (working copy)
@@ -58,7 +58,10 @@
the time that vc_Destroy is called, vc_Destroy will automatically
delete them. */
EXPRDELETE,
- CMS2
+ MS,
+ SMS,
+ CMS2,
+ MSP
};
void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int
param_value);