From 4046c8e7cbd5b9db8562344c21c15c3db6248e7d Mon Sep 17 00:00:00 2001 From: ahorn Date: Mon, 12 May 2014 15:13:56 +0100 Subject: Add SimplifyExpressions command line option Allow users to bypass ConstraintManager::simplifyExpr(ref). --- lib/Core/Executor.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'lib/Core') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index abb023eb..fb1a6698 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -164,6 +164,11 @@ namespace { SimplifySymIndices("simplify-sym-indices", cl::init(false)); + cl::opt + SimplifyExpressions("simplify-expressions", + cl::init(true), + cl::desc("Simplify symbolic expressions before querying the solver (default=on).")); + cl::opt MaxSymArraySize("max-sym-array-size", cl::init(0)); @@ -333,7 +338,7 @@ Executor::Executor(const InterpreterOptions &opts, interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME)); - this->solver = new TimingSolver(solver); + this->solver = new TimingSolver(solver, SimplifyExpressions); memory = new MemoryManager(); } -- cgit 1.4.1 From 0a7ec5db72a0baa624a0103ae8618d6379e35a76 Mon Sep 17 00:00:00 2001 From: ahorn Date: Mon, 19 May 2014 20:44:24 +0100 Subject: Rename command line option for equality substitutions --- lib/Core/Executor.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/Core') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index fb1a6698..9a3fbaa0 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -165,9 +165,9 @@ namespace { cl::init(false)); cl::opt - SimplifyExpressions("simplify-expressions", + EqualitySubstitution("equality-substitution", cl::init(true), - cl::desc("Simplify symbolic expressions before querying the solver (default=on).")); + cl::desc("Simplify equality expressions before querying the solver (default=on).")); cl::opt MaxSymArraySize("max-sym-array-size", @@ -338,7 +338,7 @@ Executor::Executor(const InterpreterOptions &opts, interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME)); - this->solver = new TimingSolver(solver, SimplifyExpressions); + this->solver = new TimingSolver(solver, EqualitySubstitution); memory = new MemoryManager(); } -- cgit 1.4.1