Solver choice in C interface

28 views
Skip to first unread message

Stephan Falke

unread,
Nov 2, 2011, 11:53:48 AM11/2/11
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);

Trevor Hansen

unread,
Nov 10, 2011, 6:58:29 AM11/10/11
to stp-users
Hi Stephan,

Thanks for the patch! It's applied in revision 1408.

Trev.
Reply all
Reply to author
Forward
0 new messages