From 76b6ae9a16dcb643456a98a845dc8d44df3aa049 Mon Sep 17 00:00:00 2001 From: Eric Rizzi Date: Mon, 16 Feb 2015 11:46:01 -0500 Subject: Commit of improved IndependentSolver::getIniitalValues(). Previous implementation simply passed the entire constraint forward without any factoring of the constraint at all. This is a problem since it is highly likely that there are cached solutions to pieces of the constraint. The new implementation breaks the entire constraint down into its requisite factors and passes each piece forward, one by one, down the solver chain. After an answer is returned, it is integrated into a larger solution. Since, by definition, no factor can affect another, we can safely create a solution to the larger constraint from the answers of its smaller pieces. The reconstruction of the solution is done by analyzing which parts of an array a factor touches. If the factor is the only one to reference a particular array, then all of the values calculated in the solution for that array are included in the final answer. If the factor references a particular element of the array (for example, arr[1]), then only the value in index 1 of array arr will be included in the solution. --- include/klee/util/Assignment.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'include') diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index 63df4b65..6fee5cb1 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -29,13 +29,13 @@ namespace klee { public: Assignment(bool _allowFreeValues=false) : allowFreeValues(_allowFreeValues) {} - Assignment(std::vector &objects, + Assignment(const std::vector &objects, std::vector< std::vector > &values, bool _allowFreeValues=false) : allowFreeValues(_allowFreeValues){ std::vector< std::vector >::iterator valIt = values.begin(); - for (std::vector::iterator it = objects.begin(), + for (std::vector::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { const Array *os = *it; std::vector &arr = *valIt; -- cgit 1.4.1