diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 12:08:55 +0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 12:08:55 +0700 |
commit | 29cb71f98bccf50fe18d795f17a71790c6c59e05 (patch) | |
tree | 89ed234561ef3e0fc3f23cd32df19aa946dd8f46 /src/proof/pdr/pdrInt.h | |
parent | 6ff66ed49e004900854fb3507385f3392240e1f5 (diff) | |
download | abc-29cb71f98bccf50fe18d795f17a71790c6c59e05.tar.gz abc-29cb71f98bccf50fe18d795f17a71790c6c59e05.tar.bz2 abc-29cb71f98bccf50fe18d795f17a71790c6c59e05.zip |
Integrating Satoko into pdr.
Diffstat (limited to 'src/proof/pdr/pdrInt.h')
-rw-r--r-- | src/proof/pdr/pdrInt.h | 26 |
1 files changed, 25 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 2a8ab023..639276db 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -28,11 +28,35 @@ #include "aig/saig/saig.h" #include "misc/vec/vecWec.h" #include "sat/cnf/cnf.h" -#include "sat/bsat/satSolver.h" #include "pdr.h" #include "misc/hash/hashInt.h" #include "aig/gia/giaAig.h" +//#define PDR_USE_SATOKO 1 + +#ifndef PDR_USE_SATOKO + #include "sat/bsat/satSolver.h" +#else + #include "sat/satoko/satoko.h" + #include "sat/satoko/solver.h" + #define l_Undef 0 + #define l_True 1 + #define l_False -1 + #define sat_solver satoko_t + #define sat_solver_new satoko_create + #define sat_solver_delete satoko_destroy + #define zsat_solver_new_seed(s) satoko_create() + #define zsat_solver_restart_seed(s,a) satoko_reset(s) + #define sat_solver_nvars solver_varnum + #define sat_solver_setnvars satoko_setnvars + #define sat_solver_addclause(s,b,e) satoko_add_clause(s,b,e-b) + #define sat_solver_final satoko_final_conflict + #define sat_solver_solve(s,b,e,c,x,y,z) satoko_solve_assumptions_limit(s,b,e-b,(int)c) + #define sat_solver_var_value solver_read_cex_varvalue + #define sat_solver_set_runtime_limit solver_set_runtime_limit + #define sat_solver_compress(s) +#endif + ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// |