diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-13 10:29:31 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-13 10:29:31 -0800 |
| commit | 22388f901a88dddfe629dd3c1406b06fafa9675d (patch) | |
| tree | 8e99ba4a2e90fd84468738af7ef26dd971f67848 /src/sat/glucose/Solver.h | |
| parent | 38d72c43435f70eb8703dc922f3c0630132bffcc (diff) | |
| download | abc-22388f901a88dddfe629dd3c1406b06fafa9675d.tar.gz abc-22388f901a88dddfe629dd3c1406b06fafa9675d.tar.bz2 abc-22388f901a88dddfe629dd3c1406b06fafa9675d.zip | |
Adding and integrating new SAT solver APIs.
Diffstat (limited to 'src/sat/glucose/Solver.h')
| -rw-r--r-- | src/sat/glucose/Solver.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h index 43b13db7..3d7d26ea 100644 --- a/src/sat/glucose/Solver.h +++ b/src/sat/glucose/Solver.h @@ -64,6 +64,12 @@ public: vec<int> user_vec; vec<Lit> user_lits; + // circuit-based solving + int jftr; + void sat_solver_set_var_fanin_lit(int, int, int); + void sat_solver_start_new_round(); + void sat_solver_mark_cone(int); + // Problem specification: // Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. @@ -457,6 +463,10 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ v inline void Solver::addVar(Var v) { while (v >= nVars()) newVar(); } +inline void Solver::sat_solver_set_var_fanin_lit(int var, int lit0, int lit1) {} +inline void Solver::sat_solver_start_new_round() {} +inline void Solver::sat_solver_mark_cone(int var) {} + //================================================================================================= // Debug etc: |