fix(opensmt/smtsolvers/CoreSMTSolver.h): make CoreSMTSolver::filterUn…

…assigned pure virtual
soonhokong · May 7, 2015 · 854c4fb · 854c4fb
1 parent 248af48
commit 854c4fb
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/src/opensmt/smtsolvers/CoreSMTSolver.C b/src/opensmt/smtsolvers/CoreSMTSolver.C
@@ -1839,9 +1839,6 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts)
   }
 }
 
-void CoreSMTSolver::filterUnassigned(){
-}
-
 double CoreSMTSolver::progressEstimate() const
 {
   double  progress = 0;

diff --git a/src/opensmt/smtsolvers/CoreSMTSolver.h b/src/opensmt/smtsolvers/CoreSMTSolver.h
@@ -247,7 +247,7 @@ class CoreSMTSolver : public SMTSolver
         lbool    search           (int nof_conflicts, int nof_learnts);                    // Search for a given number of conflicts.
         void     reduceDB         ();                                                      // Reduce the set of learnt clauses.
         void     removeSatisfied  (vec<Clause*>& cs);                                      // Shrink 'cs' to contain only non-satisfied clauses.
-	virtual void     filterUnassigned ();                                                      // Filter decision variables that don't need a decision
+        virtual void filterUnassigned () = 0;                                              // Filter decision variables that don't need a decision
 
         // Maintaining Variable/Clause activity:
         //
-Original file line number
+Diff line change
@@ Expand Up @@
       }
     }
-    void CoreSMTSolver::filterUnassigned(){
-    }
     double CoreSMTSolver::progressEstimate() const
     {
       double  progress = 0;
@@ Expand Down @@