| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This reverts commit eb7226ebeabf7cc70ec023107d74ffc5c1bad5e7. After
merging #2740, our experiments show that the ss-combine rewrite is
now beneficial for solving performance.
|
|
* [LRA Proof] Storage for LRA proofs
During LRA solving the `ConstraintDatabase` contains the reasoning
behind different constraints. Combinations of constraints are
periodically used to justify lemmas (conflict clauses, propegations, ...
?). `ConstraintDatabase` is SAT context-dependent.
ArithProofRecorder will be used to store concise representations of the
proof for each lemma raised by the (LR)A theory. The (LR)A theory will
write to it, and the ArithProof class will read from it to produce LFSC
proofs.
Right now, it's pretty simplistic -- it allows for only Farkas proofs.
In future PRs I'll:
1. add logic that stores proofs therein
2. add logic that retrieves and prints proofs
3. enable LRA proof production, checking, and testing
* Document ArithProofRecorder use-sites
* Update src/proof/arith_proof_recorder.cpp
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Yoni's review
* clang-format
* Response to Mathias' review.
|
|
|
|
|
|
This was causing assertion failures when using Sets + Sygus.
|
|
independent (#2749)
--cegqi-si=none previously disabled pre/post-condition templates for invariant synthesis. This PR eliminates this dependency.
There are no major code changes in this PR, unfortunately a large block of code changed indentation so I refactored it to be more up to date with the coding guidelines.
|
|
|
|
|
|
|
|
|
|
* [LRA proof] Refine "poly" and "term Real" distinction
Short Version:
Refined the LRA signature and used the refined version to write two new
test proofs which are close to interface compatible with the LRA proofs
that CVC4 will produce.
Love Version:
LRA proofs have the following interface:
* Given predicates between real terms
* Prove bottom
However, even though the type of the interface does not express this,
the predicates are **linear bounds**, not arbitrary real bounds. Thus
LRA proofs have the following structure:
1. Prove that the input predicates are equivalent to a set of linear
bounds.
2. Use the linear bounds to prove bottom using farkas coefficients.
Notice that the distinction between linear bounds (associated in the
signature with the string "poly") and real predicates (which relate
"term Real"s to one another) matters quite a bit. We have certain inds
of axioms for one, and other axioms for the other.
The signature used to muddy this distinction using a constructor called
"term_poly" which converted between them. I decided it was better to buy
into the distinction fully.
Now all of the axioms for step (2) use the linear bounds and axioms for
step (1) use both kinds of bounds, which makes sense because step (1) is
basically a conversion.
Also had to add an axiom or two, because some were missing.
* Update proofs/signatures/th_lra.plf
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Improved test readability, removed unused axioms
The LRA proof tests did not have appropriate documentation, and did not
specify **what** they proved. Now they each have a header comment
stating their premises and conclusion, and that conclusion is enforced
by a type annotation in the test.
The LRA signature included some unused axioms concerning `poly_term`.
Now they've been removed.
Credits to Yoni for noticing both problems.
|
|
* [LRAT] signature robust against duplicate literals
The LRAT signature previously had complex, surprising, and occasionally
incorrect behavior when given clauses with duplicate literals.
Now it does not. Now clauses have true set semantics, and clauses with
duplicate literals are treated identically to those without.
* Test with logically = but structurally != clauses.
|
|
|
|
* LRAT signature
Added an LRAT signature. It is almost entirely side-conditions, but it
works.
There is also a collection of tests for it. You can run them by invoking
```
lfscc smt.plf sat.plf lrat.plf lrat_test.plf
```
* Update proofs/signatures/lrat.plf per Yoni's suggestion.
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Responding to Yoni's comments.
* Removed unused varaibles
Some tests declared `var`s which were unused.
Now they don't.
|
|
|
|
|
|
* Arith Constraint Proof Logging
Also a tiny documentation update.
* Debug.isOn check around iterated output
* reference iteratees
|
|
* Enable BV proofs when using and eager bitblaster
Specifically:
* Removed assertions that blocked them.
* Made sure that only bitvectors were stored in the BV const let-map
* Prevented true/false from being bit-blasted by the eager bitblaster
Also:
* uncommented "no-check-proofs" from relevant tests
* Option handler logic for BV proofs
BV eager proofs only work when minisat is the sat solver being used by
the BV theory.
Added logic to the --proof hanlder to verify this or throw an option
exception.
* Bugfix for proof options handler
I forgot that proofEnabledBuild runs even if the --proof option is
negated. In my handler I now check that proofs are enabled.
* Clang-format
|
|
A test for PR #2737 was failing even though the PR only added dead code.
This PR fixes the issue by fixing two use-after-free bugs:
- `ResolutionBitVectorProof` has a `Context` and a
`std::unique_ptr<BVSatProof>` member. The `BVSatProof` depends on the
`Context` and tries to access it (indirectly) in its constructor but
because the context was declared after the proof, the context was
destroyed before the proof, leading to a use-after-free in a method
called from the proof's destructor. This commit reorders the two
members.
- `TLazyBitblaster` was destroyed before the `LFSCCnfProof` in
`BitVectorProof` because `SmtEngine`'s destructor first destroyed the
theory engine and then the proof manager. This lead to a use-after-free
because `LFSCCnfProof` was using the `d_nullContext` of
`TLazyBitblaster`, which got indirectly accessed in `LFSCCnfProof`'s
destructor. This commit moves the destruction of `ProofManager` above
the destruction of the theory engine.
The issues were likely introduced by #2599. They went undetected because
our nightlies' ASAN check does not use proofs due to known memory leaks
in the proof module of CVC4.
I have tested this PR up to regression level 2 with ASAN with leak
detection disabled.
|
|
|
|
|
|
Seems to have no impact on Norn, and is helpful for a number of applications.
|
|
|
|
* Split BitvectorProof into a sub/superclass
The superclass contains general printing knowledge.
The subclass contains CNF or Resolution-specific knowledge.
* Renames & code moves
* Nits cleaned in prep for PR
* Moved CNF-proof from ResolutionBitVectorProof to BitVectorProof
Since DRAT BV proofs will also contain a CNF-proof, the CNF proof should
be stored in `BitVectorProof`.
* Unique pointers, comments, and code movement.
Adjusted the distribution of code between BVP and RBVP.
Notably, put the CNF proof in BVP because it isn't
resolution-specific.
Added comments to the headers of both files -- mostly BVP.
Changed two owned pointers into unique_ptr.
BVP's pointer to a CNF proof
RBVP's pointer to a resolution proof
BVP: `BitVectorProof`
RBVP: `ResolutionBitVectorProof`
* clang-format
* Undo manual copyright modification
* s/superclass/base class/
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* make LFSCBitVectorProof::printOwnedSort public
* Andres's Comments
Mostly cleaning up (or trying to clean up) includes.
* Cleaned up one header cycle
However, this only allowed me to move the forward-decl, not eliminate
it, because there were actually two underlying include cycles that the
forward-decl solved.
* Added single _s to header gaurds
* Fix Class name in debug output
Credits to Andres
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Reordered methods in BitVectorProof per original ordering
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In certain cases, we can share skolems between similar reductions, e.g.
`(str.replace x y z)` and `(str.replace (str.substr x 0 n) y z)` because the
first occurrence of `y` in `x` has to be the first occurrence
of `y` in `(str.substr x 0 n)` (assuming that `y` appears in both, otherwise the value of
the skolems does not matter). This commit adds a helper function in the
skolem cache that does some of those simplifications.
|
|
|
|
|
|
This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.
|
|
This caches some information regarding tester applications and changes int -> size_t in a few places.
|
|
|
|
|
|
* LRA proof signature fixes and a first proof
The existing LRA signature had a few problems (e.g. referencing symbols
that didn't exist, extra parentheses, etc). I patched it up and wrote an
first example LRA proof. load `th_lra_test.plf` last to run that test.
* Add dependency info to signatures
I chose to indicate shallow dependencies only.
|
|
This commit changes the two www,antlr3.org URL's in contrib/get-antlr-3.4 to use https instead of http, which is more secure.
|
|
We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.
|
|
This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.
|
|
|
|
Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE.
This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust.
After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible.
|
|
|
|
|
|
|
|
|
|
Proof steps were in a std::list, which is a linked list, but really, we
only needed a stack, so I changed it to a vector, because LL's are
usually slower.
Also added an iterator for the proof steps, and << implementations
|
