| Age | Commit message (Collapse) | Author |
|---|
|
This commit enables DRAT-optimization, which consists of two sub-processes:
1. removing unnecessary instructions from DRAT-proofs and
2. not proving clauses which are not needed by DRAT proofs.
These changes have the effect of dramatically shortening some some bit-vector proofs. Specifically, proofs using lemmas in the ER, DRAT, and LRAT formats, since proofs in any of these formats are derived from a (now optimized!) DRAT proof produced by CryptoMiniSat. What follows is a description of the main parts of this PR:
## DRAT Optimization
The DRAT-optimization is done by `drat-trim`, which is bundled with `drat2er`. The (new) function `ClausalBitVectorProof::optimizeDratProof` is our interface to the optimization machinery, and most of the new logic in this PR is in that function.
## CNF Representation
The ability to not prove unused clauses requires a slight architectural change as well. In particular, we need to be able to describe **which** subset of the original clause set actually needs to be proved. To facilitate this, when the clause set for CryptoMiniSat is first formed it is represented as a (a) map from clause indices to clauses and (b) a list of indices. Then, when the CNF is optimized, we temporarily store a new list of the clauses in the optimized formula. This change in representation requires a number of small tweaks throughout the code.
## Small Fixes to Signatures
When we decided to check and accept two different kinds of DRAT, some of our DRAT-checking broke. In particular, when supporting one kind of DRAT, it is okay to `fail` (crash) when a proof fails to check. If you're supporting two kinds of DRAT, crashing in response to the first checker rejecting the proof denies the second checker an opportunity to check the proof. This PR tweaks the signatures slightly (and soundly!) to do something else instead of `fail`ing.
|
|
Due to issues in the current proof code, this commit also disables proof
checking for five QF_LRA benchmarks (see issue #2855).
|
|
|
|
|
|
* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
* Specifically, CNF proofs broke when proving tautological clauses.
Now they don't.
|
|
* Extended DRAT signature to operational DRAT
The DRAT signature now supports both operational and specified DRAT.
That is, either kind of proof will be accepted.
The goal of this implementation of operational DRAT was to re-use as
much of the specified DRAT machinery as possible. However, by writing a
separate operational signature, we could make it much more efficient
(after all, operational DRAT came about because of a push for efficient
cheking).
You can run the new AND old DRAT tests by running
```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```
* Apply suggestions from code review (Yoni)
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
|
|
* Bugfix: LFSC clause equality
My implementation of clause equality had an undocumented assumption that
the clauses didn't have any duplicate literals. Now that assumption is
gone, and the tests suite has been expanded.
* Added an empty clause test
* Typo fix: Yoni
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Yoni's comments
* Remove a duplicate clause_eq test.
* Add an ordering clause_eq test.
* Improve the documentation of clause_eq.
|
|
* Extended Resolution Signature
While extended resolution is a fairly general technique, the paper
"Extended Resolution Simulates DRAT" / the drat2er uses exactly one new
type of rule: definitions of the form
new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)
This PR adds axioms supporting this kind of definition, and adds a test
making use of those new axioms. The axioms support the following ideas:
1. Introducing a **fresh** variable, defined in the form above
2. Clausifying that definition to produce proofs of $$ n + 2 $$ new
clauses in the form of two clauses, and a cnf with $$ n $$ clauses
3. An axiom for unrolling the proof of the cnf into proofs of the
original clauses.
* Addressing Yoni's comments
1. Added a new (trivial) test
2. Improved a bunch of documentation
* Update proofs/signatures/er.plf
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Removed references to RATs from the signature
There are still a few references in the header comment.
* Aside on continuations
* Scrap the elision annotations
|
|
* 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
|
|
* [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.
|
|
* 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.
|
|
|
|
|
|
The sources of all previous libraries are now added to libcvc4 and built as
libcvc4. This removes circular dependencies between libcvc4 and libexpr.
Further, we now only have one parser library and don't build additional
libraries for each language.
|
|
|
|
|
|
|
|
Proof checking failed when applying the instantiation rule so that the original formula and the instantiated formula are the same. Fixed using the new "ifequal" construct in lfsc.
|
|
|
|
LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution
anymore. As a consequence, we
+ Add --with-lfsc and --with-lfsc-directory as configure options.
In the case where CVC4 has not been built with integrated LFSC, all code that interacts with
LFSC is disabled.
+ Disable proof checking if CVC4_USE_LFSC is not defined.
Configuring the build with --check-proofs but without --with-lfsc results in an error.
+ Do not call LFSC's cleanup function (but we should in the future).
LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt.
Disabled call to lfscc_cleanup until the problem in lfscc is fixed.
+ Disable building with LFSC for the distcheck travis build since it is not part of the distribution
anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker
before calling make check on the temp build (the build of the unpacked distribution tar ball).
|
|
The nightly competition build has been failing due to a remaining use of
hash_set in approx_simplex.cpp. This commit changes the remaining uses
of hash_set to unordered_set.
The remaining uses of hash_set were in LFSC. Switching to C++11 for LFSC
required changing the configure.ac for LFSC to require C++11 support to
make sure that it can be compiled independently from the rest of CVC4 (some
of our Travis tests do that as well). To have the macros for these additional
checks available, the commit adds a symlink to the files in config that contain
the macros). I did not find a way to add macros from a parent's folder that
did not break `make distcheck
|
|
Fix several spelling errors
|
|
LFSC did not detect when the number of arguments provided to a side
condition did not match the expected number of arguments, which could
lead to out-of-bounds reads and writes. This commit adds a check and
fixes one of the proof rules that provided the wrong number of
arguments.
|
|
|
|
new proof constructs generated by the equality engine.
proof production for bool-array.smt2 passes
|
|
|
|
|
|
Squashed commit of the following:
commit 5197a663eb262afbeb7740f53b5bd27479dccea0
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon Mar 6 00:16:16 2017 -0800
Remove IFF case
commit 2119b25a30ed42eca54f632e7232c9f76ae5755a
Author: guykatzz <katz911@gmail.com>
Date: Mon Feb 20 12:37:06 2017 -0800
proof support for bvcomp
commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri Feb 17 21:09:04 2017 -0800
Added missing cases to operator<< for bv rewrite rules.
commit 0ed797c31d0e66cadc35b2397716c841d1aff270
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri Feb 17 11:43:51 2017 -0800
Added rewrite rules for new bitvector kinds.
commit 3b23dffb317de5559f8a95118fef633f711c114a
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon Feb 13 14:41:49 2017 -0800
First draft of bool-to-bv pass.
|
|
For certain proofs, the performance was drastically different on
different OSes. The cause for this difference was a pointer comparison
in the deduplication in `Expr::defeq()`. Depending on how the OS
allocated the memory, an expression `a` would get replaced with an
equivalent expression `b` or vice versa, which in turn affected
performance of `Expr::free_in()` dramatically (sub-second vs. >5 min
running times). This commit makes the process more deterministic by
using a heuristic that favors symbolic expressions and greedily tries to
make small refcounts smaller when replacing, and changes
`Expr::free_in()` to not repeatedly explore the same subexpressions.
|
|
|
|
linebreaks.
|
|
[LFSC] Minor fixes/improvements
|
|
- Avoid mixing new/delete with malloc/free
- Remove reimplementation of strcmp
- Add assertions
|
|
In certain cases, LFSC was creating CExprs with the single-argument
constructor, which allocates an array of one child, only to immediately
replace it with a new array (without deleting the old one).
Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ
expressions (the null pointer is appended automatically by the single
argument constructor, an array with two null pointer entries should not
be necessary).
|
|
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing
changes made to 5f415d4585134612bc24e9a823289fee35541a01.
|
|
Conflicts:
src/options/quantifiers_options
|
|
|
|
|
|
child arguments after successful comparison).
|
|
|
|
Conflicts:
proofs/signatures/Makefile.am
src/Makefile.am
src/expr/datatype.cpp
src/options/datatypes_options
src/options/options_template.cpp
src/options/quantifiers_options
src/proof/arith_proof.cpp
src/proof/arith_proof.h
src/proof/array_proof.cpp
src/proof/array_proof.h
src/proof/bitvector_proof.cpp
src/proof/bitvector_proof.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/skolemization_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/proof/uf_proof.cpp
src/proof/uf_proof.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp
src/theory/arrays/array_proof_reconstruction.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/quantifiers/ceg_instantiator.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/equality_infer.cpp
src/theory/quantifiers/equality_infer.h
src/theory/quantifiers/inst_match_generator.cpp
src/theory/quantifiers/inst_propagator.cpp
src/theory/quantifiers/inst_propagator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_rules.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/strings/Makefile.am
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/max2-univ.sy
|
|
Added a flag to enable/disbale this feature (enabled by default).
Also, added some infrastructure for proving rewrite rules.
|
|
Added support for the BV case
|
|
the decl_bblast step, instead of having an individual "with alias" rule for each BV operation
|
|
|
|
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
|
|
|
|
irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
|
