From cac3967b52ae44fae3962ee9eba456221e0efda3 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Mon, 6 Feb 2017 11:34:52 -0800 Subject: =?UTF-8?q?Adding=20a=20new=20SAT=20solver=20to=20ABC.=20(Satoko)?= =?UTF-8?q?=20The=20command=20is=20=E2=80=98satoko=E2=80=99?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/base/abci/abc.c | 82 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 81 insertions(+), 1 deletion(-) (limited to 'src/base/abci/abc.c') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 008adbae..efb82fcc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -43,6 +43,7 @@ #include "map/amap/amap.h" #include "opt/ret/retInt.h" #include "sat/xsat/xsat.h" +#include "sat/satoko/satoko.h" #include "sat/cnf/cnf.h" #include "proof/cec/cec.h" #include "proof/acec/acec.h" @@ -308,6 +309,7 @@ static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandXSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSatoko ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -956,6 +958,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "xsat", Abc_CommandXSat, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "satoko", Abc_CommandSatoko, 0 ); Cmd_CommandAdd( pAbc, "Verification", "psat", Abc_CommandPSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 ); @@ -23302,6 +23305,83 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + abctime clk; + int c; + satoko_opts_t opts; + + satoko_default_opts(&opts); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Chv" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + opts.conf_limit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.conf_limit < 0 ) + goto usage; + break; + case 'h': + goto usage; + case 'v': + opts.verbose ^= 1; + break; + + default: + goto usage; + } + } + + if ( argc == globalUtilOptind + 1 ) + { + char * pFileName = argv[globalUtilOptind]; + satoko_t * p; + int status; + + satoko_parse_dimacs( pFileName, &p ); + satoko_configure(p, &opts); + + clk = Abc_Clock(); + status = satoko_solve( p ); + + if ( status == SATOKO_UNDEC ) + Abc_Print( 1, "UNDECIDED " ); + else if ( status == SATOKO_SAT ) + Abc_Print( 1, "SATISFIABLE " ); + else + Abc_Print( 1, "UNSATISFIABLE " ); + + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + satoko_destroy( p ); + return 0; + } + +usage: + Abc_Print( -2, "usage: satoko [-CILDE num] [-hv].cnf\n" ); + Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit ); + Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} /**Function************************************************************* Synopsis [] @@ -26238,7 +26318,7 @@ usage: Abc_Print( -2, "\t Zyad Hassan, Aaron R. Bradley, Fabio Somenzi, \"Better Generalization in IC3\", FMCAD 2013.\n"); Abc_Print( -2, "\t (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/85-Better-Generalization-IC3.pdf)\n"); - + return 1; } -- cgit v1.2.3