| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This cleans up naming of API functions to create first-order constants and variables.
mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.
Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).
|
|
|
|
Fixes 2887.
|
|
* [BV] An option for SAT proof optimization
The option doesn't **do** anything yet, but exists.
* CopyPaste Fix: BvOptimizeSatProof documentation
It was the documentation for a different option. Now it has been
updated.
* Fix Typos per Mathias' review.
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit adds an extended rewrite that splits a given string equality
into multiple equalities if it can find prefixes of equal lengths.
For example: `(= (str.++ x "AB" z) (str.++ "A" x y)) ---> (and (=
(str.++ x "A") (str.++ "A" x)) (= (str.++ "B" z) y))`
|
|
|
|
Fixes #2958.
The issue was: we had substr(x,0,2) in R, and the "derivable substitution" modifed this to substr(substr(x,0,2),0,2) in R, since substr(x,0,2) was the representative of x (which is a bad choice, but regardless is legal). Then decomposition inference asked "can i reduce substr(substr(x,0,2),0,2) in R"? It determines substr(substr(x,0,2),0,2) in R rewrites to substr(x,0,2) in R, which is already true. However, substr(x,0,2) in R was what we started with.
The fix makes things much more conservative: we never mark extended functions reduced based on decomposition, since there isnt a strong argument based on an ordering.
|
|
|
|
The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor}
[0, 1] as left-associative. CVC4 treats all but bvxnor as having
variable arity anyway but the arity check was too strict when using
`--strict-parsing`. This commit changes the strict parsing check. For
bvxnor, it adds code to the parser that expands an application of bvxnor
into multiple applications of a binary bvxnor if needed.
References:
[0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand,
bvor, bvadd, bvmul)
[1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor)
|
|
|
|
|
|
This is a minor fix for systems with glibc version < 2.17. In that case, we need to link with `-lrt` according to the clock_gettime man page.
|
|
|
|
|
|
|
|
|
|
* SatClauseHashFunction
Added to the same file as SatLiteralHashFunction.
* clang-format
Thanks Andres!
|
|
|
|
|
|
|
|
For a simple query `(not (= (fp.isSubnormal x) false))`, we were getting
a wrong model. The issue was that `(sign x)` was not assigned a value
and did not appear in the shared terms. In
`TheoryFp::collectModelInfo()`, however, we generate an expression that
connects the components of `x` to `x`, which contains `(sign x)`. As a
result, the normalization while building a model did not result in a
constant. This commit fixes the issue by marking `(sign x)` (and
`(significand x)`) as assignable. Assignable terms can take any value
while building a model if there is no existing value.
|
|
`TheoryBVRewriter::RewriteITEBv()` is currently always returning the
status `REWRITE_DONE`. This can result in a situation where a rewritten
node can be rewritten again (which breaks the contract of our rewriter).
The unit test in this commit illustrates the issue. The commit fixes the
issue by returning `REWRITE_AGAIN` or `REWRITE_AGAIN_FULL` if a node
changed. `REWRITE_AGAIN_FULL` is needed if the resulting node may have a
child that is not a subterm of the original expression.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
ASAN was reporting memory leaks in regression tests that were using
subsolvers. First, I am going to describe the origin of the leaks and
then the solution implemented in this commit.
Recall an `Expr` stores the `NodeManager` that the internal node is
associated with. `Node::toExpr()` converts a `Node` to an `Expr` and
assumes that the active `NodeManager` (returned by
`NodeManager::currentNM()` is the one associated with the node. In
`ExportPrivate::exportInternal()`, when we were exporting a skolem, we
created a skolem in the target `NodeManager` by calling
`NodeManager::mkSkolem()` (`ExprManager`s do not support the creation of
skolems) but then we called `Node::toExpr()` on the resulting skolem
while the origin `NodeManager` was the active `NodeManager`. One of the
issues of having the wrong `NodeManager` in the `Expr` is that when the
`Expr` is destroyed and the internal node's refcount reaches zero in
destructor of `Expr`, then the node value associated with the node is
added to the set of zombie nodes (nodes waiting to be garbage collected
or resurrected) of the wrong `NodeManager`. The problem here is that the
set of zombie nodes uses the node id to hash and compare nodes. Node
ids, however, are only unique within a given `NodeManager`. Thus, if we
have two nodes with the same id from different `NodeManager`s and both
reach refcount zero in the context of the same `NodeManager`, only one
of them will end up in the set of zombies and thus only that one will be
freed.
Using a subsolver realiably triggered this issue.
`ExportPrivate::exportInternal()` stored the `Expr` with the wrong
`NodeManager` in an `ExprManagerMapCollection` which associates
variables in the original `ExprManager` with the variables in the target
`ExprManager`. When we created a subsolver, we created the
`ExprManagerMapCollection` before creating our subsolver, so it was
deleted after the subsolver and so deleting the
`ExprManagerMapCollection` deleted the last reference to `Expr`s holding
skolem nodes associated with the wrong `NodeManager`.
This commit fixes the issue by making sure that the correct
`NodeManager` is in scope when converting the skolem/bound variable
nodes to an `Expr`. It also swaps the creation order of
`ExprManagerMapCollection` and `ExprManager` to make sure that
`ExprManagerMapCollection` is deleted before the `ExprManager` that the
`Expr`s belong to. Additionally, the commit makes it harder to make a
similar mistake by asserting that the `Expr`s in the
`ExprManagerMapCollection` are associated with the expected
`ExprManager`s. Finally, it adds an assertion that tries to identify
such issues by checking whether the list of zombies contains a node with
the same id but located at a different address.
|
|
This commit adds a rewrite that strips endpoints from `str.indexof`
operators if they don't overlap with the string that is being searched
for using `stripConstantEndpoints()`. In addition to that, it makes
`stripConstantEndpoints()` slightly more aggressive by allowing it to
drop substring components that have zero overlap with the string that we
are looking at. Finally, the commit fixes the default argument for
`fullRewriter` of `checkEntailContains()` to be true instead of false,
which should allow for more rewriting opportunities.
|
|
|
|
|
