Simplify rust API project build script.

We no longer need to know where the individual solver libraries are located,
as they have been built into the libcprover.a static library we are now building
against.

Author: NlightNFotis

CMakeLists.txt

@@ -274,7 +274,7 @@ else()
 
     corrosion_import_crate(MANIFEST_PATH src/libcprover-rust/Cargo.toml)
     list(JOIN sat_impl " " sat_impl_str)
-    corrosion_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR} "SAT_IMPL=${sat_impl_str}")
+    corrosion_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR})
     corrosion_link_libraries(cprover-api-rust cprover-api-cpp)
     install(TARGETS cprover-api-rust RUNTIME DESTINATION lib)
     # NOTE: We want to rename to a name consistent with the name of the

src/libcprover-rust/build.rs

@@ -26,47 +26,6 @@ fn get_library_build_dir() -> std::io::Result<PathBuf> {
     ))
 }
 
-fn get_cadical_build_dir() -> std::io::Result<PathBuf> {
-    let env_var_fetch_result = get_build_directory();
-    if let Ok(build_dir) = env_var_fetch_result {
-        let mut path = PathBuf::new();
-        path.push(build_dir);
-        path.push("cadical-src/build/");
-        return Ok(path);
-    }
-    Err(Error::new(
-        ErrorKind::Other,
-        "failed to get build output directory",
-    ))
-}
-
-fn get_sat_libraries() -> std::io::Result<Vec<&'static str>> {
-    let env_var_name = "SAT_IMPL";
-    let env_var_fetch_result = env::var(env_var_name);
-    if let Ok(sat_impls) = env_var_fetch_result {
-        let mut solver_libs = Vec::new();
-        for sat_impl in sat_impls.split(" ") {
-            let solver_lib = match sat_impl {
-                "minisat2" => "minisat2-condensed",
-                "glucose" => "glucose-condensed",
-                "cadical" => "cadical",
-                _ => {
-                    return Err(Error::new(
-                        ErrorKind::Other,
-                        "no identifiable solver detected",
-                    ))
-                }
-            };
-            solver_libs.push(solver_lib);
-        }
-        return Ok(solver_libs);
-    }
-    Err(Error::new(
-        ErrorKind::Other,
-        "SAT_IMPL environment variable not set",
-    ))
-}
-
 fn main() {
     let cbmc_source_path = Path::new("..");
     let cpp_api_path = Path::new("../libcprover-cpp/");
@@ -86,27 +45,6 @@ fn main() {
         Err(err) => panic!("Error: {}", err),
     };
 
-    let solver_libs = match get_sat_libraries() {
-        Ok(solvers) => solvers,
-        Err(err) => panic!("Error: {}", err),
-    };
-
-    for solver_lib in solver_libs.iter() {
-        // Cadical is being built in its own directory, with the resultant artefacts being
-        // present only there. Hence, we need to instruct cargo to look for them in cadical's
-        // build directory, otherwise we're going to get build errors.
-        if *solver_lib == "cadical" {
-            let cadical_build_dir = match get_cadical_build_dir() {
-                Ok(cadical_directory) => cadical_directory,
-                Err(err) => panic!("Error: {}", err),
-            };
-            println!(
-                "cargo:rustc-link-search=native={}",
-                cadical_build_dir.display()
-            );
-        }
-    }
-
     println!(
         "cargo:rustc-link-search=native={}",
         libraries_path.display()