| Age | Commit message (Collapse) | Author |
|---|
|
* LFSC drat output
* Addressed Mathias' review
Addressing Mathias' review with the following changes:
* Added a few blank lines
* Added a unit test for LRAT output as LFSC
|
|
|
|
* Copied old DRAT data-structure files.
Next step: clean up the code, and adapt them to our current usage plans.
* Polished the DRAT class.
Notably, removed the idea of lazy-parsing, this is now just a DRAT
wrapper class.
More explicit about whether methods handle binary or text.
Better constructor patterns
* Added implementation of textual DRAT output
* reordered the DratInstruction structure.
* removed the public modifier from the above struct
* removed the operator << implementation for DratInstruction
* use emplace_back
* Addressing Yoni's first review
* Extracted "write literal in DIMACS format" idea as a function
* Replaced some spurious Debug streams with `os`. (they were left over
from an earlier refactor)
* Improved some documentation
* Removed aside about std::string
* Addressed Mathias' comments
Specifically
* SCREAMING_SNAKE_CASED enum variants.
* Extracted some common logic from two branches of a conditional.
* Cleaned out some undefined behavior from bit manipulation.
* Unit tests for binary DRAT parsing
* Added text output test
* s/white/black/ derp
|
|
--static now implies --no-unit-testing.
Fixes #2672.
|
|
There were two typos in the unit tests that caused OOB accesses. Instead
of doing `d_solver.mkConst(CONST_BITVECTOR, std::string("101"), 6)`, the
closing parenthesis was in the wrong place resulting in
`std::string("101", 6)`. The second argument to `std::string(const
char*, size_t)` says how many characters to copy and results in
undefined behavior if the number is greater than the length of the
string, thus the OOB access. The commit fixes the typo and removes one
of the tests because it should not actually fail (16 is an accepted
base).
|
|
* [LRAT] A C++ data structure for LRAT.
Added a data structure for storing (abstract) LRAT proofs.
The constructor will take a drat binary proof and convert it to LRAT
using drat-trim. However, this is unimplemented in this PR.
Subsequent PRs will add:
* LFSC representation of LRAT
* Bitvector Proofs based on LRAT
* Enabled tests for those proofs
* Documenting LRAT constructors
* Apply suggestions from code review
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Responding to Andres' review
Consisting of
* Naming nits
* Closed fds
* Better implementation of disjoint union for LratInstruction
* DRAT -> LRAT conversion is no longer an LratProof constructor
* include reorder
* Update src/proof/lrat/lrat_proof.h
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
* ANonymous namespaces and name resolution?
* Remove inlines, fix i negation
Thanks Andres!
* Use `std::abs`
Credit to Andres
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Remove uneeded public
|
|
|
|
|
|
PR #2764 removed `Solver::mkBitVector(uint32_t)` (returns a bit-vector
of a given size with value zero), which made the build fail when SymFPU
was enabled because solver_black used it for SymFPU-enabled builds. This
commit simply adds a zero default argument to `mkBitVector(uint32_t,
uint64_t)` to allow users to create zero-valued bit-vectors without
explicitly specifying the value again. Additionally, the commit replaces
the use of the `CVC4_USE_SYMFPU` macro by a call to
`Configuration::isBuiltWithSymFPU()`, making sure that we can catch
compile-time errors regardless of configuration. Finally,
`Solver::mkConst(Kind, uint32_t, uint32_t, Term)` now checks whether
CVC4 has been compiled with SymFPU when creating a `CONST_FLOATINGPOINT`
and throws an exception otherwise (solver_black has been updated
correspondingly).
|
|
* [LRA proof] Recording & Printing LRA Proofs
Now we use the ArithProofRecorder to record and later print arithmetic
proofs.
If an LRA lemma can be proven by a single farkas proof, then that is
done. Otherwise, we `trust` the lemma.
I haven't **really** enabled LRA proofs yet, so `--check-proofs` still
is a no-op for LRA.
To test, do
```
lfsccvc4 <(./bin/cvc4 --dump-proofs ../test/regress/regress0/lemmas/mode_cntrl.induction.smt | tail -n +2)
```
where `lfsccvc4` is an alias invoking `lfscc` with all the necessary
signatures. On my machine that is:
```
alias lfsccvc4="/home/aozdemir/repos/LFSC/build/src/lfscc \
/home/aozdemir/repos/CVC4/proofs/signatures/sat.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/smt.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/lrat.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_base.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_bv.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_bv_bitblast.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_arrays.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_int.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_quant.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf"
```
* Added guards to proof recording
Also reverted some small, unintentional changes.
Also had to add printing for STRING_SUBSTR??
* Responding to Yoni's review
* SimpleFarkasProof examples
* Respond to Aina's comments
* Reorder Constraint declarations
* fix build
* Moved friend declaration in Constraint
* Trichotomy example
* Lift getNumChildren invocation in PLUS case
Credits to aina for spotting it.
* Clang-format
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
drat2er is a C/C++ project which includes support for
* Checking DRAT proofs
* Converting DRAT proofs to LRAT proofs
* Converting DRAT proofs to ER proofs
It does the first 2 by using drat-trim under the hood.
I've modified our CMake configuration to allow drat2er to be linked into
CVC4, and I added a contrib script.
|
|
|
|
* DRAT signature
Added the DRAT signature to CVC4.
We'll need this in order to compare three BV proof pipelines:
1. DRAT -> Resolution -> Check
2. DRAT -> LRAT -> Check
3. DRAT -> Check (this one!)
Tested the signature using the attached test file. i.e. running
```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```
* Added type annotations for tests
* Respond to Yoni's review
* Apply Yoni's suggestions from code review
Documentation polish
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Whoops, missed a spot or two
|
|
|
|
This PR makes the skolem normalization in the string solver quite a bit
more aggressive by reducing more skolems to prefix and suffix skolems.
Experiments show that this PR significantly improves performance on CMU
benchmarks.
|
|
|
|
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.
|
|
|
|
|
