Merge pull request #3734 from tautschnig/solvers-no-langapi

Remove (unused) langapi dependency from solvers/

Author: tautschnig

src/Makefile

@@ -45,7 +45,7 @@ languages: util.dir langapi.dir \
            cpp.dir ansi-c.dir xmllang.dir assembler.dir \
            jsil.dir json.dir json-symtab-language.dir
 
-solvers.dir: util.dir langapi.dir
+solvers.dir: util.dir
 
 goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
                      goto-symex.dir linking.dir analyses.dir solvers.dir

src/solvers/Makefile

@@ -229,5 +229,5 @@ solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB)
 -include $(smt2/smt2_solver$(DEPEXT))
 
 smt2_solver$(EXEEXT): $(OBJ) smt2/smt2_solver$(OBJEXT) \
-	../util/util$(LIBEXT) ../langapi/langapi$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB)
+	../util/util$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB)
 	$(LINKBIN)

src/solvers/refinement/module_dependencies.txt

@@ -1,4 +1,3 @@
-langapi # should go away
 solvers/flattening
 solvers/floatbv
 solvers/refinement

src/solvers/refinement/refine_arithmetic.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 #include <util/arith_tools.h>
 
-#include <langapi/language_util.h>
-
 #include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/floatbv/float_utils.h>
 
@@ -527,9 +525,5 @@ bv_refinementt::add_approximation(
 
 std::string bv_refinementt::approximationt::as_string() const
 {
-  #if 0
-  return from_expr(expr);
-  #else
   return std::to_string(id_nr)+"/"+id2string(expr.id());
-  #endif
 }