| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Support directory
|
|
``stp/stplog.h`` header file in the current version of STP
and no support in the build system for setting this define so
this code is completly dead.
|
|
|
|
The '%' operater in C is not Gauss Modulo
but remainder operations.
Using a negative number as right operand
can result in a negative number.
Fix appropriate SRem building
Note: MetaSMTlib implementation doesn't have that bug.
|
|
Fix signed division by constant 1/ -1
|
|
|
|
Division by constant divisor get optimized
using shift and multiplication operations in STP builder.
The used method cannot be applied for divisor 1 and -1.
In that case use slow path.
|
|
New version of the get initial values functionality which makes use of the independent solver.
|
|
The super-set check in the CexCachingSolver takes MUCH longer than the
sub-set check. Upon closer inspection, the super-set check gets slower
and slower as more counterexamples fill the UBTree. Pretty quickly,
the cost of the super-set check becomes larger than the time required
to simply bypass it and go to the Solver.
|
|
This function should be used solely in assertion statements and is
intended as a sanity check to make sure that the solution constructed
by IndependentSolver::getInitialValues() produces and answer that in
fact satisfies the the query.
|
|
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.
|
|
This functionality is necessary in order to more effectively handle
calls to IndependentSolver::getInitialValues. An incoming query will
be broken down into its smaller parts, and each piece will be solved
for. At the end, the pieces will be recombined into a larger solution.
The IndependentElementSet::getAllFactors() method takes a query and
breaks it down into all of it's non-interacting factors. The
IndependentElementSet::calculateArrays() method calculates which
arrays are involved in a particular factor.
|
|
|
|
This is important for future changes to IndependentSolver::
getInitialValues() so that an incoming constraint can be broken
down into its smallest possible parts. Each of these individual
parts may then be solved for and then the solutions to each piece
combined to create a final answer.
Finally, several fields which had previously been private are now
public to facilitate the smaller solutions being combined into a
larger solution.
|
|
Fix overshift check
|
|
Shifting by bitwidth-1 is valid
|
|
|
|
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET)
* Remove the now defunct ExprSMTLIBLetPrinter
* Improve performance of ExprSMTLIBPrinter::scan() by keeping
track of visited Expr to avoid visiting them again
* Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
|
|
|
|
- See comment, this is a gross workaround for Darwin's very small default limit
on shared memory size. I'm not sure how big of a counterexample users can
actually expect STP to solve in practice -- if there is a practical use for
larger ones it would probably be good for us to write a fallback strategy.
|
|
not asserts.
|
|
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling
the checks in that mode).
- Eventually it would be nice to just move off of LLVM's DEBUG infrastructure
entirely and just have our own copy, but this works for now.
- Fixes #150.
|
|
unordered_{map,set} includes.
- I'm not sure what the status of libstdcxx's c++11 support is. It may be we
can just move over to <unordered_map> everywhere, but I don't have a Linux
test machine handy at the moment.
|
|
|
|
iostream injects static constructor function into every compilation unit.
Remove this to avoid it.
|
|
According to LLVM: lightweight and simpler implementation of streams.
|
|
|
|
MetaSMTBuilder.
|
|
warning.
|
|
|
|
|
|
that is the samw width of the "expr" expression.
It probably is the same width (it defintely is in SMT-LIB but I'm not
sure about STP) but it is probably better to be explicit.
|
|
|
|
overshifts to zero. Test case is included.
|
|
to zero. Test case is included.
|
|
overshifts to zero. Test case is included.
|
|
to zero. Test case is included.
|
|
zero. A test case was added for this.
In addition the use to vc_bvExtract() was removed for shifting left by an
expression because we don't want/need bitmasked behaviour anymore.
|
|
a bug in the previous commit where 32-bit width was assumed.
|
|
The other shift operators still need to be changed
|
|
|
|
not supported; a test case modified to not fail because of this.
|
|
|
|
|
|
Fix queries not being logged correctly if an assertion failure is hit.
|
|
|
|
get correctly logged if an assertion failure is hit later on.
|
|
STPSolver to base Solver and SolverImpl classes, and consequently redefined in derived classes to call the corresponding methods down the solver chain. Method setTimeout() renamed to setCoreSolverTimeout().
|
