diff options
| author | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
| commit | 5f072a19d299191dbedc4b69c8e0eda694cfa957 (patch) | |
| tree | 0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4 /src/prop/bvminisat/simp/SimpSolver.h | |
| parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) | |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'src/prop/bvminisat/simp/SimpSolver.h')
| -rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 4af82b02d..d808daa22 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -58,6 +58,7 @@ class SimpSolver : public Solver { // bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); + lbool solveLimited(bool do_simp = true, bool turn_off_simp = false); bool solve ( bool do_simp = true, bool turn_off_simp = false); bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); @@ -96,7 +97,7 @@ class SimpSolver : public Solver { int merges; int asymm_lits; int eliminated_vars; - CVC4::TimerStat total_eliminate_time; + // CVC4::TimerStat total_eliminate_time; protected: @@ -195,6 +196,9 @@ inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, boo inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); } +inline lbool SimpSolver::solveLimited (bool do_simp, bool turn_off_simp){ + return solve_(do_simp, turn_off_simp); } + //================================================================================================= } |