diff options
| author | Bruno Schmitt <bruno@oschmitt.com> | 2017-08-29 09:40:51 +0200 |
|---|---|---|
| committer | Bruno Schmitt <bruno@oschmitt.com> | 2017-08-29 09:40:51 +0200 |
| commit | ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27 (patch) | |
| tree | b8575b157b1019275f5f1da040b18d3c36fd6e11 /src/proof/pdr/pdrInt.h | |
| parent | d0f81fcf2952b8a46548c0dd74f95fa1cd0a504f (diff) | |
| download | abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.tar.gz abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.tar.bz2 abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.zip | |
Fixing bronken C++ build; Satoko internal header, solver.h, should not be used in other packages
Diffstat (limited to 'src/proof/pdr/pdrInt.h')
| -rw-r--r-- | src/proof/pdr/pdrInt.h | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 639276db..ea6b24af 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -38,7 +38,6 @@ #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 @@ -47,13 +46,13 @@ #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_nvars satoko_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_var_value satoko_read_cex_varvalue + #define sat_solver_set_runtime_limit satoko_set_runtime_limit #define sat_solver_compress(s) #endif |