Generated code contains use of nonexistent object.__getattr__ method. #588
Comments
|
Umm, am I missing something? https://docs.python.org/3/reference/datamodel.html#object.__getattr__ |
|
I think in this fragment, object is used as a placeholder instance name. Otherwise, it's incorrect. The built-in type object does not have the getattr method, it has only getattribute. |
|
I can confirm this is an issue. A project I work on uses swig to generate python bindings with python 2.7.10. The unit tests we wrote for our API bindings worked fine under swig 3.0.7. After an update to 3.0.8, most of our tests are failing due to this issue. Even trying to instantiate any of our API objects fails. |
|
Can you share a unit test where this fails? Obviously it passes all the tests we have... |
|
Please include the command line options that you use to invoke SWIG with the test. |
|
Attached. You may need to edit the included build.sh script to suit your environment. I tested this both with 3.0.7 and 3.0.8. |
|
#584 resolves this (at least, the case that @ahrbe1 has). @nezumisama does whatever was breaking for you also rely on wrapping a class named "Exception"? Note that the point is still legitimate though - while |
|
Switching to It looks like the call to |
|
Hi |
|
Maybe the patch is not correct in all the "mode" supported by swig, i'm sorry for that |
ahnolds
added a commit
to ahnolds/swig
that referenced
this issue
Jan 24, 2016
Cleans up patch swig#232 Fixes misleading error messages from swig#588 If __getattr__ is called, this means that normal attribute lookup has failed. If checking thisown and __swig_getmethods__ fails, then give up and raise AttributeError instead of calling the non-existent object.__getattr__. Note that in practice the result is essentially the same, since trying to access object.__getattr__ fails and raises AttributeError, just with a misleading message. In addition, there's no point in having nondynamic attribute lookup.
|
The AttributeError message has been improved by applying patch #598. |
4tXJ7f
pushed a commit
to cvc5/cvc5
that referenced
this issue
Oct 22, 2018
Ran into this bug when compiling with python3 bindings: swig/swig#588 Instantiating any object crashes python. Since swig3.0.8 is currently the apt-get install for Ubuntu 16.04, I thought it'd be good to have a check for that. If python3 is preferred and the swig version is 3.0.8, it errors out and asks users to downgrade or upgrade SWIG.
adacore-bot
pushed a commit
to AdaCore/spark2014
that referenced
this issue
Apr 18, 2019
Project: cvc4 master 5321dfb1161032a79909a588ed05bb27d42ba579
MS114-013 Merging upstream cvc4 into our master
Change-Id: I1b9af6c730515e0be2156aa595fa62e678a086c7
Only check disequal terms with sygus-rr-verify (#2793)
ClausalBitvectorProof (#2786)
* [DRAT] ClausalBitvectorProof
Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)
It fits into the `BitvectorProof` class hierarchy like this:
```
BitvectorProof
/ \
/ \
ClausalBitvectorProof ResolutionBitvectorProof
```
This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
* CnfStream
* SatSolver (specifically the BvSatSolver)
* CnfProof
* TheoryProof
* TheoryBV
* Both bitblasters
And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.
This means that references to and interactions with (R)BVP were
pervasive.
Nevertheless, an SMT developer must persist.
The change summary:
* Create a subclass of BVP, called ClausalBitvectorProof, which has
most methods stubbed out.
* Make a some modifications to BVP and ResolutionBitvectorProof as the
natural division of labor between the different classes becomes
clear.
* Go through all the components in the first list and try to figure
out which kind of BVP they should **actually** be interacting with,
and how. Make tweaks accordingly.
* Add a hook from CryptoMinisat which pipes the produced DRAT proof
into the new ClausalBitvectorProof.
* Add a debug statement to ClausalBitvectorProof which parses and
prints that DRAT proof, for testing purposes.
Test:
* `make check` to verify that we didn't break any old stuff, including
lazy BB, and eager BB when using bvminisat.
* `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
-d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
1. It crashed with "Unimplemented"
2. Right before that it prints out the (textual) DRAT proof.
* Remove 2 unneeded methods
* Missed a rename
* Typos
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Andres comments
* Reorder members of TBitblaster
LFSC LRAT Output (#2787)
* LFSC ouput & unit test
* Renamed lrat unit test file
* s/DRAT/LRAT/
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
1. Extracted a filter whitespace function.
2. Added @param annotations.
* Addressing Yoni's comments
Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.
LratInstruction inheritance (#2784)
While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.
While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.
This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.
Fixed linking against drat2er, and use drat2er (#2785)
* Fixed linking against drat2er/drat-trim
We have machinery for linking against drat2er. However, this machinery
didn't quite work because libdrat2er.a contains an (undefined) reference
to `run_drat_trim` from libdrat-trim.a.
Thus, when linking against libdrat2er.a, we also need to link against
libdrat-trim.a.
I made this change, and then tested it by actually calling a function
from the drat2er library (CheckAndConvertToLRAT) which relies on
`run_drat_trim`. Since this invocation compiles, we know that the
linking is working properly now.
* Combined the two libs, per Mathias
* drat2er configured gaurds
New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)
New C++ API: Get rid of mkConst functions (simplify API). (#2783)
Do not rewrite 1-constructor sygus testers to true (#2780)
[BV Proofs] Option for proof format (#2777)
We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!
My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`
and that I could not provide random other option values.
Clause proof printing (#2779)
* Print LFSC proofs of CNF formulas
* Unit Test for clause printing
* Added SAT input proof printing unit test
* Fixed cnf_holds reference. Proofs of CMap_holds
There were references to clauses_hold, which should have been references
to cnf_holds.
Also added a function for printing a value of type CMap_holds, and a
test for this function.
LFSC drat output (#2776)
* 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
New C++ API: Add missing getType() calls to kick off type checking. (#2773)
[DRAT] DRAT data structure (#2767)
* 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
cmake: Disable unit tests for static builds. (#2775)
--static now implies --no-unit-testing.
Fixes #2672.
C++ API: Fix OOB read in unit test (#2774)
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. (#2737)
* [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
New C++ API: Add missing catch blocks for std::invalid_argument. (#2772)
API/Smt2 parser: refactor termAtomic (#2674)
C++ API: Reintroduce zero-value mkBitVector method (#2770)
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 (#2758)
* [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
New C++ API: Add tests for mk-functions in solver object. (#2764)
Clean up BV kinds and type rules. (#2766)
Add missing type rules for parameterized operator kinds. (#2766)
Fix issues with REWRITE_DONE in floating point rewriter (#2762)
Remove noop. (#2763)
Configured for linking against drat2er (#2754)
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.
New C++ API: Add tests for term object. (#2755)
DRAT Signature (#2757)
* 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
Revert "Move ss-combine rewrite to extended rewriter (#2703)" (#2759)
[LRA Proof] Storage for LRA proofs (#2747)
* [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.
Fixed typos.
New C++ API: Add tests for opterm object. (#2756)
Fix extended rewriter for binary associative operators. (#2751)
This was causing assertion failures when using Sets + Sygus.
Make single invocation and invariant pre/post condition templates 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.
New C++ API: Add tests for sort functions of solver object. (#2752)
Remove spurious map (#2750)
Fix compiler warnings. (#2748)
API: Add simple empty/sigma regexp unit tests (#2746)
[LRA proof] More complete LRA example proofs. (#2722)
* [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 (#2743)
* [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.
Remove alternate versions of mbqi (#2742)
LRAT signature (#2731)
* 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.
BoolToBV modes (off, ite, all) (#2530)
Strings: Make EXTF_d inference more conservative (#2740)
Arith Constraint Proof Loggin (#2732)
* Arith Constraint Proof Logging
Also a tiny documentation update.
* Debug.isOn check around iterated output
* reference iteratees
Enable BV proofs when using an eager bitblaster (#2733)
* 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
Fix use-after-free due to destruction order (#2739)
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.
Take into account minimality and types for cached PBE solutions (#2738)
Apply extended rewriting on PBE static symmetry breaking. (#2735)
Enable regular expression elimination by default. (#2736)
Seems to have no impact on Norn, and is helpful for a number of applications.
Skip non-cardinality types in sets min card inference (#2734)
Bit vector proof superclass (#2599)
* 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
Optimizations for PBE strings (#2728)
Infrastructure for sygus side conditions (#2729)
Combine sygus stream with PBE (#2726)
Improve interface for sygus grammar cons (#2727)
Information gain heuristic for PBE (#2719)
Optimize re-elim for re.allchar components (#2725)
Improve skolem caching by normalizing skolem args (#2723)
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.
Generalize sygus stream solution filtering to logical strength (#2697)
Improve cegqi engine trace. (#2714)
Make (T)NodeTrie a general utility (#2489)
This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.
Fix coverity warnings in datatypes (#2553)
This caches some information regarding tester applications and changes int -> size_t in a few places.
Lazy model construction in TheoryEngine (#2633)
Reduce lookahead when parsing string literals (#2721)
LRA proof signature fixes and a first proof for linear polynomials (#2713)
* 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.
Use https for antlr3.org downloads (#2701)
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.
Move ss-combine rewrite to extended rewriter (#2703)
We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.
Add rewrite for (str.substr s x y) --> "" (#2695)
This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.
Cache evaluations for PBE (#2699)
Quickly recognize when PBE conjectures are infeasible (#2718)
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.
Obvious rewrites to floating-point < and <=. (#2706)
Support string replace all (#2704)
Fix type enumerator for FP (#2717)
Fix real2int regression. (#2716)
Change lemma proof step storage & iterators (#2712)
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
Clausify context-dependent simplifications in ext theory (#2711)
Fix E-matching for case where candidate generator is not properly initialized (#2708)
Expand definitions prior to model core computation (#2707)
cmake: Require boost 1.50.0 for examples. (#2710)
cmake: Add option to explicitely enable/disable static binaries. (#2698)
Evaluator: add support for str.code (#2696)
Adding default SyGuS grammar construction for arrays (#2685)
Fix collectEmptyEqs in string rewriter (#2692)
Fix for itos reduction (#2691)
Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)
Change default sygus enumeration mode to auto (#2689)
Fix coverity warnings in sygus enumerator (#2687)
New C++ API: Split unit tests. (#2688)
Increasing coverage (#2683)
This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.
API: Fix assignment operators (#2680)
The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.
Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
configure.sh: Fix option parsing to match --help (#2611)
Allow partial models with optimized sygus enumeration (#2682)
Implement option to turn off symmetry breaking for basic enumerators (#2686)
Improves the existing implementation for sygus-active-gen=basic.
Refactor default grammars construction (#2681)
fixes to regression docs (#2679)
Add optimized sygus enumeration (#2677)
Record assumption info in AssertionPipeline (#2678)
Minor improvement to sygus trace (#2675)
CMake: Set RPATH on installed binary (#2671)
Currently, when installing CVC4 with a custom installation directory on
macOS, the resulting binary cannot be executed because the linker cannot
find the required libraries (e.g. our parser). This commit changes our
build system to use the `CMAKE_INSTALL_RPATH` variable to add the
installation directory to the RPATH list in the exectuable.
Do not use lazy trie for sygus-rr-verify (#2668)
Fail for SWIG 3.0.8 (#2656)
Ran into this bug when compiling with python3 bindings: https://github.com/swig/swig/issues/588
Instantiating any object crashes python. Since swig3.0.8 is currently the apt-get install for Ubuntu 16.04, I thought it'd be good to have a check for that. If python3 is preferred and the swig version is 3.0.8, it errors out and asks users to downgrade or upgrade SWIG.
CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)
Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.
[0] https://github.com/CVC4/CVC4/blob/7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36
Only build CryptoMiniSat library, no binary (#2657)
This commit changes the contrib/get-cryptominisat script to only build
the CryptoMiniSat library instead of both the library and the binary.
The advantage of this is that we can compile a static version of the
CryptoMiniSat library without having a static version of glibc or
libstdc++ (this is fine as long as we do a shared library build of
CVC4). This is an issue on Fedora (tested on version 25) where the
contrib/get-cryptominisat script was failing when building the
CryptoMiniSat binary due to the static version of these libraries not
being available. Since we just want to build the library, the commit
also changes the script to not install CryptoMiniSat anymore and updates
the CMake find script to accomodate the new folder structure. Side note:
the folder structure generated after this commit is a bit more uniform
with, e.g. the CaDiCaL script: The source files are directly in the
cryptominisat5 folder, not in a subfolder.
Recover from wrong use of get-info :reason-unknown (#2667)
Fixes #2584. Currently, we are immediately terminating CVC4 if the user
issues a `(get-info :reason-unknown)` command if it didn't succeed a
`(check-sat)` call returning `unknown`. This commit changes the behavior
to return an `(error ...)` but continue executing afterwards. It turns
the `ModalException` thrown in this case into a
`RecoverableModalException` and adds a check in
`GetInfoCommand::invoke()` to turn it into a
`CommandRecoverableFailure`, which solves the issue.
Remove antlr_undefines.h. (#2664)
Is not required anymore since we don't use autotools anymore.
Add substr, contains and equality rewrites (#2665)
Disable dumping test for non-dumping builds (#2662)
Travis: run examples and avoid building them twice (#2663)
`make check` builds the examples but does not run them. This commit
changes our Travis script to run the examples after building them and
removes `makeExamples()` to avoid building them twice.
BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. (#2647)
Simplifications based on the special const is now delegated down, only
the concat is pulled up.
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const. (#2647)
Sygus streaming non-implied predicates (#2660)
Remove autotools build system. (#2639)
Fix util::Random for macOS builds (#2655)
Add helper to detect length one string terms (#2654)
This commit introduces a helper function to detect string terms that
have exactly/at most length one. This is useful for a lot of rewrites
because strings of at most length one are guaranteed to not overlap
multiple components in a concatenation, which allows for more aggressive
rewriting.
This commit has been tested with --sygus-rr-synth-check for >1h on the
string term grammar.
Add OptionException handling during initialization (#2466)
The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:
1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes
This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor). Finally,
the commit adds a simple regression test for invalid dump tags.
cmake: Run regression level 2 for make check. (#2645)
Non-implied mode for model cores (#2653)
Non-contributing find replace rewrite (#2652)
Improve reduction for str.to.int (#2636)
Introducing internal commands for SyGuS commands (#2627)
Constant length regular expression elimination (#2646)
Skip sygus-rr-synth-check regressions when ASAN on (#2651)
This commit disables three regressions when using an ASAN build. The
regressions are all leaking memory when invoking the subsolver (see
issue #2649). Debugging the issue will take a while but is not very
critical since this feature is currently only used by CVC4 developers
but it prevents our nightly builds from going through.
Show if ASAN build in --show-config (#2650)
This commit extends `--show-config` to show whether the current build is
an ASAN build or not. This is done by moving a detection that was
previously done for the unit tests into base/configuration_private.h.
In addition to being convenient, this allows us to easily exclude
regression tests from ASAN builds.
Sygus query generator (#2465)
Fix context-dependent for positive contains reduction (#2644)
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643)
Match: `x_m | concat(y_my, 0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, ~0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)`
On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
| CVC4-base | CVC4-concatpullup-or |
BENCHMARK | SLVD SAT UNSAT TO MO CPU[s] | SLVD SAT UNSAT TO MO CPU[s] |
totals | 38992 13844 25148 1082 28 984887.4 | 39028 13845 25183 1046 28 974819.1 |
```
cmake: Add CxxTest include directory to unit test includes. (#2642)
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ones (#2596).
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 1 (#2596).
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
Improve strings reductions including skolem caching for contains (#2641)
Improve reduction for int.to.str (#2629)
Option for shuffling condition pool in CegisUnif (#2587)
cmake: Generate git_versioninfo.cpp on build time. (#2640)
Delay initialization of theory engine (#2621)
This implements solution number 2 for issue #2613.
Add more (str.replace x y z) rewrites (#2628)
Fix fp-bool.sy grammar and require symfpu (#2631)
Reset input language for ExprMiner subsolver (#2624)
Improvements to rewrite rules from inputs (#2625)
Add rewrites for str.replace in str.contains (#2623)
This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.
Fix heuristic for string length approximation (#2622)
Refactor printing of parameterized operators in smt2 (#2609)
Improve reasoning about empty strings in rewriter (#2615)
Fix partial operator elimination in sygus grammar normalization (#2620)
Fix string ext inference for rewrites that introduce negation (#2618)
Fix default setting of CegisUnif options (#2605)
cmake: Use gcovr instead lcov for coverage report generation. (#2617)
Fix compiler warnings (#2602)
Synthesize rewrite rules from inputs (#2608)
Fix cegis so that evaluation unfolding is not interleaved. (#2614)
Optimize regular expression elimination (#2612)
Add length-based rewrites for (str.substr _ _ _) (#2610)
Support for basic actively-generated enumerators (#2606)
Random: support URNG interface (#2595)
Use std::shuffle (with Random as the unified random generator) instead
of std::random_shuffle for deterministic, reproducable random shuffling.
Allow multiple synthesis conjectures. (#2593)
Fix compiler warnings. (#2601)
BV instantiator: Factor out util functions. (#2604)
Previously, all util functions for the BV instantiator were static functions
in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding
unit test, it was therefore required to include this cpp file in order to
test these functions. This factors out these functions into a
theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h).
Asan reported errors for the corresponing unit test because of this.
BV inverter: Factor out util functions. (#2603)
Previously, all invertibility condition functions were static functions
in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test,
it was therefore required to include this cpp file in order to test
these functions. This factors out these functions into a
theory/quantifiers/bv_inverter_utils.(cpp|h).
Fix string register extended terms (#2597)
A regress2 benchmark was failing, due to a recent change in our strings rewriter.
The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.
The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.
This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.
Cmake: Fix ctest call for example/translator. (#2600)
example/translator expects an input file to translate but none was provided in the ctest call.
This caused the ctest call to hang and wait for input on stdin in some configurations (in
particular in the nightlies).
Address slow sygus regressions (#2598)
Disable extended rewriter when applicable with var agnostic enumeration (#2594)
Fix unif trace (#2550)
Fix cache for sygus post-condition inference (#2592)
Update default options for sygus (#2586)
Fix rewrite rule filtering. (#2591)
New C++ API: Add checks for Sorts. (#2519)
Infrastructure for string length entailments via approximations (#2514)
Only use SKIP_RETURN_CODE with CMake 3.9.0+ (#2590)
With older versions of CMake, skipped tests are reported as failures,
which is undesirable. This commit changes the CMakeLists file to only
use the `SKIP_RETURN_CODE` property if a newer version of CMake is used.
Fix end constraint for regexp elimination (#2571)
Clean remaining references to getNextDecisionRequest and simplify (#2500)
Fix mem leak in sha1_collision example. (#2588)
Fix mem leak in sets_translate example. (#2589)
Simplify datatypes printing (#2573)
Fix compiler warnings. (#2585)
Fix regress (#2575)
Add actively generated sygus enumerators (#2552)
Make CegisUnif with condition independent robust to var agnostic (#2565)
Fix stale op list in sets (#2572)
Eliminate partial operators within lambdas during grammar normalization (#2570)
cmake: Display skipped tests as not run (#2567)
Currently, the run_regression.py script just returns 0 when we skip a
test due to a feature not supported by the current configuration.
Returning 0 marks those tests as passed. To make it more clear which
tests were skipped, this commit adds the `SKIP_RETURN_CODE` [0] property
to the regression tests and changes the regression script to return 77
for skipped tests. The feature is supported since at least CMake 3.0 [0].
For backwards compatibility with autotools, returning 77 for skipped
tests is only active when `--cmake` is passed to the run_regression.py
script.
[0] https://cmake.org/cmake/help/v3.0/prop_test/SKIP_RETURN_CODE.html
Allow (_ to_fp ...) in strict parsing mode (#2566)
When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
unit: Fix ASAN detection for GCC. (#2561)
Make registration of preprocessing passes explicit (#2564)
As it turns out, self-registering types are problematic with static
linkage [0]. Instead of fixing the issue with linker flags, which seems
possible but also brittle (e.g. the flags may be different for different
linkers), this commit adds an explicit registration of each
preprocessing pass.
[0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html
Fix documentation for `make regress`. (#2557)
cmake: Add examples to build-tests, add warning for disabling static build. (#2562)
Fix "catching polymorphic type by value" warnings (#2556)
When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make
sure that we use a reference type for the exception, otherwise the unit
test tries to catch the exception by value, resulting in "catching
polymorphic type by value" warnings.
cmake: Generate compile_commands.json on configure. (#2559)
cmake: Add build target build-tests to build all test dependencies. (#2558)
init scalar class members (coverity issues 1473720 and 1473721) (#2554)
Fix compiler warnings. (#2555)
Fix dumping pre/post preprocessing passes (#2469)
This commit changes the hard-coded list of checks for
preprocessing-related dump tags to take advantage of the new
preprocessing pass registration mechanism from PR #2468. It also fixes a
typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()`
and adds a list of available passes to the `--dump help` output.
Refactor preprocessing pass registration (#2468)
This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.
As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.
This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.
[0] https://llvm.org/docs/WritingAnLLVMPass.html
Add rewrite for solving stoi (#2532)
cmake: Ignore ctest exit code for coverage reports.
Stream concrete values for variable agnostic enumerators (#2526)
Rewrites for (= "" _) and (= (str.replace _) _) (#2546)
cmake: Only do Java tests when unit testing on (#2551)
Right now, we are adding the Java tests even when we are not building
unit tests. This commit changes the build system to only add the Java
tests when unit tests are enabled. There are two reasons for this
change:
- building a production version of CVC4 should not require JUnit
- it seems more intuitive (to me at least) to disable JUnit tests when
unit tests are disabled
This change also simplifies building the Java bindings in our homebrew
formula.
cmake: Add CxxTest finder module to allow custom paths. (#2542)
Remove assertion. (#2549)
Infrastructure for using active enumerators in sygus modules (#2547)
Incorporate all unification enumerators into getTermList. (#2541)
Fix Taylor overapproximation for large exponentials (#2538)
Fix homogeneous string constant rewrite (#2545)
Fix bug in getSymbols. (#2544)
cmake: Only print dumping warning if not disabled by user. (#2543)
Makes SyGuS parsing more robust in invariant problems (#2509)
cmake: Fix test target dependency issues. (#2540)
Enable quantified array regression. (#2539)
Symmetry breaking for variable agnostic enumerators (#2527)
cmake: New INSTALL.md for build and testing instructions. (#2536)
cmake: Exclude examples for coverage target. (#2535)
Eagerly ensure literal on active guards for sygus enumerators (#2531)
cmake: Add check for GCC 4.5.1 and warn user. (#2533)
examples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534)
cmake: configure.sh wrapper: Removed unused option --gmp.
carefully printing trusted assertions in proofs (#2505)
cmake: Fix tag code generation dependencies. (#2529)
Fix warnings uncovered by cmake build (#2521)
Fix quantifiers selector over store rewrite (#2510)
Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in.
After the change, we are +61-7 on SMT LIB:
https://www.starexec.org/starexec/secure/details/job.jsp?id=30581
Allow partial models for multiple sygus enumerators (#2499)
Infrastructure for variable agnostic sygus enumerators (#2511)
Improve non-linear check model error handling (#2497)
Refactor strings equality rewriting (#2513)
This moves the extended rewrites for string equality to the main strings rewriter as a function rewriteEqualityExt, and makes this function called on every equality that is generated (from non-equalities) by our rewriter.
cmake: Fix dependencies for code generation. (#2524)
Fix wiki urls. (#2504)
cmake: Fix git version info (again). (#2523)
cmake: Fix theory order #2. (#2522)
Unify rewrites related to (str.contains x y) --> (= x y) (#2512)
cmake: Fix theory order. (#2518)
Make string rewriter unit tests more robust (#2520)
This commit changes the unit test for the string rewriter to use the
extended rewriter instead of the regular rewriter to make it more
robust, e.g. to different orderings in conjunctions.
cmake: Fix and simplify git version info. (#2516)
cmake: Add program prefix option. (#2515)
Fix generating debug/trace tags.
New C++ API: Add checks for Terms/OpTerms. (#2455)
Fix regress2. (#2502)
cmake: Add python3 option.
cmake: Enable -Wall.
cmake: Fix systemtests dependency.
cmake: Build fully static binaries with option --static.
cmake: Run make coverage in parallel by default.
cmake: Add more documentation, some fixes and cleanup.
cmake: configure.sh wrapper: Use explicit build directory structure.
We don't create build directories for every build type (and
configuration) anymore. The default build directory is now 'build'
(created where you call the wrapper script from). Option --name allows
to configure an individual name (and path) for the build directory.
cmake: configure wrapper: Modify next steps message after configuration.
Since configure.sh is only a wrapper for cmake it prints all the messages from
cmake. At the end we print the next steps after configuration. If configure.sh
is used we add the info to also change into the build directory before calling
make.
cmake: Move PACKAGE_NAME to ConfigureCVC4, more cleanup.
cmake: Refactor cvc4_add_unit_test macro to support test names with '/'.
Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
cmake: Guard GetGitRevisionDescription.
cmake: Add target runexamples.
cmake: Add support for cross-compiling for Windows.
cmake: Require JUnit version 4.
cmake: Do not allow dumping with portfolio build.
cmake: More documentation, clean up.
cmake: Move extracting git information to src/base cmake config file.
cmake: Guard examples that require Boost.
cmake: Disable unit tests if assertions are not enabled.
cmake: FindANTLR: Check if antlr3FileStreamNew is available.
cmake: configure.sh wrapper: Fixes for sh.
travis: Switch to cmake.
cmake: Do not build examples and unit and system tests by default.
cmake: configure.sh wrapper: Add --name option.
cmake: examples: Configure output directory per target.
cmake: Added java examples
cmake: configure.sh wrapper: Add --prefix for install directory.
cmake: Add some more documentation, cleanup.
cmake: Move helper functions to cmake/Helpers.cmake.
cmake: Added target examples (currently .cpp examples only)
cmake: Simplify build type configuration.
cmake: Refactor and clean up build profile printing.
cmake: Added target check
Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.
cmake: Add make install rule.
cmake: configure.sh wrapper: Fix handling of options with arguments.
cmake: Add module finder for Valgrind.
cmake: Various CMakeLists.txt fixes/cleanup.
cmake: Only build libcvc4 and libcvc4parser as libraries.
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.
cmake: Move find_package to where it is actually needed.
cmake: configure.sh wrapper: Removed env vars help text.
cmake: configure.sh wrapper: Configurable build directory
cmake: configure.sh wrapper: Create build dirs for configurations
cmake: configure.sh wrapper: done (except: configurable build dir)
cmake: Updated and prettified configuration printing.
cmake: configure.sh wrapper: option parsing
cmake: Add ENABLE_DEBUG_CONTEXT_MM to enable the debug context memory manager.
cmake: Add ENABLE_BEST to enable best configuration of dependencies.
cmake: Add Java runtime as required dependency (required for ANTLR).
cmake: Add convenience wrappers for tag generation.
cmake: Add library versioning for libcvc4.so.
cmake: Rebase with current master, add new tests/source files.
cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.
cmake: Use target specific includes for libcvc4.
Further, print definitions added with add_definitions(...).
cmake: Add missing dependency.
cmake: Add support for building static binaries/libraries.
cmake: Add options for specifying install directories for dependencies.
cmake: Add module finder for GLPK-cut-log.
cmake: Add module finder for ABC.
cmake: Compile Java tests and add to ctest if Java bindings are enabled.
cmake: Add SWIG support + Python and Java bindings.
cmake: Add dependencies for test targets and support for make coverage.
cmake: Various portfolio/default option fixes.
cmake: Enable parallel execution for test targets regress, units, systemtests.
cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.
cmake: Added system tests and target make systemtests.
cmake: Added regression tests and target make regress.
cmake: Add portfolio support.
cmake: Add ASAN support.
cmake: Enable shared by default.
Further, force shared builds in case of unit tests.
cmake: Disable W-suggest-override for unit tests.
cmake: Add target units.
cmake: Removed obsolete CMakeLists file in test.
cmake: Add support for CxxTest.
cmake: Filter through and disable unused HAVE_* variables from autotools.
cmake: Do not set global output directories for binaries and libraries.
cmake: Fix some includes.
cmake: Added support for coverage and profiling.
cmake: Added 3-valued option handling (to enable detection of user-set options).
cmake: Add module finder for readline.
cmake: Generate token headers.
cmake: Added licensing options and warnings/errors.
cmake: Cleanup CMakeLists.txt files, remove SHARED.
cmake: Add build configurations.
cmake: Fixed compiler flag macros.
cmake: Add module finder for LFSC.
cmake: Add module finder for CaDiCaL.
cmake: Add module finder for CryptoMiniSat.
cmake: Add module finder for SymFPU.
cmake: Add module finder for CLN.
cmake: Add libsignatures for proofs.
cmake: Remove unused CMakeLists.txt
cmake: Generate cvc4autoconfig.h (options currently statically set).
cmake: Added missing dependency for src/util
cmake: Working build infrastructure.
TODO: cvc4autoconfig.h
cmake: Antlr parser generation done.
cmake: Generate trace and debug tags
cmake: .cpp generation done, .h generation not yet complete
cmake: Added initial build infrastructure.
Decision strategy: incorporate arrays. (#2495)
Add rewrites for str.contains + str.replace/substr (#2496)
Decision strategy: incorporate separation logic. (#2494)
Add two rewrites for string contains character (#2492)
Refactor strings extended functions inferences (#2480)
This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type.
This is in preparation for working on solving equations and further inferences in this style.
New C++ API: Introduce new macro and exception for API checks. (#2486)
Fix issue with str.idof in evaluator (#2493)
Decision strategy: incorporate strings fmf. (#2485)
More aggressive caching of string skolems. (#2491)
Move and rename sygus solver classes (#2488)
fix assertion error (#2487)
Clean remaining references to getNextDecisionRequest in quantifiers. (#2484)
Improvements and fixes for symmetry detection and breaking (#2459)
This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.
Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)
Decision strategy: incorporate cegis unif (#2482)
Decision strategy: incorporate bounded integers (#2481)
Decision strategy: incorporate datatypes sygus solver. (#2479)
More aggressive skolem caching for strings, document and clean preprocessor (#2478)
Make strings model construction robust to lengths that are not propagated equal (#2444)
This fixes #2429.
This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment.
We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.
Regardless, the strings model construction should be robust to handle this case, which this PR does.
Follow redirects with cURL in contrib/get* scripts (#2471)
On systems without `wget`, we use `curl` to download dependencies.
However, we were not using the `-L` (follow redirects) option, which is
necessary to download certain dependencies, e.g. CryptoMiniSat.
Remove broken dumping support from portfolio build (#2470)
Dumping support for portfolio builds was introduced in
84f26af22566f7c10dea45b399b944cb50b5e317 but as far as I can tell, the
implementation has already been problematic in the original implementation. The
current implementation has the following issues:
- Dumping with a portfolio build (even when using the single threaded
executable) results in a segfault. The reason is that the DumpChannel variable
is declared as an `extern` and exists for the duration of the program. The
problem is that it stores a `CommandSequence`, which indirectly may store
nodes. When shutting down CVC4, the destructor of `DumpC` is called, which
destroys the `CommandSequence`, which results in a segfault because the
`NodeManager` does not exist anymore. The node manager is (indirectly) owned
and destroyed by the `api::Solver` object.
- Additionally, adding commands to the `CommandSequence` is not thread safe (it
just calls `CommandSequence::addCommand()`, which in turn pushes back to a
vector [0] (which is not thread safe [1]). A single instance of `DumpChannel`
is shared among all threads (it is not declared `thread_local` [2]).
- The `CommandSequence` in `DumpC` was not used in the original implementation
and is still unused on master. The original commit mentions that the portfolio
build stores the commands in the `CommandSequence` but not why.
This commit removes the `CommandSequence` and related methods from `DumpC` to
avoid the issue when destroying `DumpChannel`. It disables dumping for
portfolio builds and adds a check at configure-time that not both options have
been enabled simultaneously. Given that the option was not functional
previously, the problematic implementation, and the fact that the dump of
multiple threads wouldn't be very useful, disabling dumping for portfolio
builds is unlikely to be problem. An improvement that could be made is to
disable dumping support only for the pcvc4 binary and while enabling it for the
single-threaded version, even when using `--with-portfolio`. However, we
currently do not have the infrastructure for that (we use the same libcvc4
library for both binaries).
[0] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/command.cpp#L756
[1] https://en.cppreference.com/w/cpp/container
[2] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/dump.h#L117
Remove unnecessary tracing from preprocessing (#2472)
With the introduction of the PreprocessingPass class,
tracing/dumping/time keeping is done automatically in the base class,
eliminating the need for doing it manually. This commit cleans up
SmtEngine, removing tracing/dumping/time keeping in preprocessing that
is not needed anymore.
Decision strategy: incorporate UF with cardinality constraints (#2476)
Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462)
Refactor how assertions are added to decision engine (#2396)
Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.
Add Skolem cache for strings, refactor length registration (#2457)
This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor).
It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled.
Generalize CandidateRewriteDatabase to ExprMiner (#2340)
Fix #include for minisat headers in bvminisat. (#2463)
Uses information gain heuristic for building better solutions from DTs (#2451)
Simplify storing of transcendental function applications that occur in assertions (#2458)
Decision strategy: incorporate CEGQI (#2460)
New C++ API: Try to fix (false positive) Coverity warnings. (#2454)
Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461)
Initial infrastructure for theory decision manager (#2447)
Fix for when strings process loop is disabled. (#2456)
Fixe compiler warning in line_buffer.cpp. (#2453)
Support model cores via option --produce-model-cores. (#2407)
This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
Avoid calling size() every iteration (#2450)
Fix global negate (#2449)
fix (#2446)
Set NodeManager to nullptr when exporting vars (#2445)
PR #2409 assumed that temporarily setting the NodeManager to nullptr
when creating variables is not needed anymore. However, this made our
portfolio build fail. This commit reintroduces the temporary NodeManager
change while creating variables.
Using a single condition enumerator in sygus-unif (#2440)
This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).
In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:
- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.
A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.
There is also small improvements for trace messages.
Refactor non-clausal simplify preprocessing pass. (#2425)
Squash implementation of counterexample-guided instantiation (#2423)
Add (str.replace (str.replace y w y) y z) rewrite (#2441)
Replace boost::integer_traits with std::numeric_limits. (#2439)
Further, remove redundant gmp.h include in options_handler.cpp.
Remove clock_gettime() replacement for macOS. (#2436)
Not needed anymore since macOS 10.12 introduced clock_gettime().
Make isClosedEnumerable a member of TypeNode (#2434)
Further simplify and fix initialization of ce guided instantiation (#2437)
Refactor and document quantifiers variable elimination and conditional splitting (#2424)
Minor improvements to interface for rep set. (#2435)
More extended rewrites for strings equality (#2431)
Eliminate select over store in quantifier bodies (#2433)
Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)
Remove printing support for sygus enumeration types (#2430)
Finer-grained inference of substitutions in incremental mode (#2403)
Add regex grammar to rewriter verification tests (#2426)
Extended rewriter for string equalities (#2427)
Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)
Remove redundant strings rewrite. (#2422)
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since
re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )
This PR removes the above rewrite, which was implemented incorrectly and was dead code.
Update INSTALL instructions (#2420)
Fixes #2419. This commit adds more information about optional
dependencies, updates macOS-related information, and fixes some details.
Remove CVC3 compatibility layer (#2418)
Remove unused options file (#2413)
Minor improvements to theory model builder interface. (#2408)
Make quantifiers strategies exit immediately when in conflict (#2099)
Transfer ownership of learned literals from SMT engine to circuit propagator. (#2421)
Fix merge mishap of #2359.
Refactor ceg conjecture initialization (#2411)
Allows SAT checks of repair const to have different options (#2412)
Refactor and document alpha equivalence. (#2402)
Fix export of bound variables (#2409)
Refactor theory preprocess into preprocessing pass. (#2395)
Use useBland option in FCSimplexDecisionProcedure (#2405)
Add regular expression elimination module (#2400)
Refactor MipLibTrick preprocessing pass. (#2359)
Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)
fix bv total ops printing (#2365)
Split term canonize utility to own file and document (#2398)
Reorder …
adacore-bot
pushed a commit
to AdaCore/spark2014
that referenced
this issue
Apr 18, 2019
Project: cvc4 master 5321dfb1161032a79909a588ed05bb27d42ba579
MS114-013 Merging upstream cvc4 into our master
Change-Id: I1b9af6c730515e0be2156aa595fa62e678a086c7
Only check disequal terms with sygus-rr-verify (#2793)
ClausalBitvectorProof (#2786)
* [DRAT] ClausalBitvectorProof
Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)
It fits into the `BitvectorProof` class hierarchy like this:
```
BitvectorProof
/ \
/ \
ClausalBitvectorProof ResolutionBitvectorProof
```
This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
* CnfStream
* SatSolver (specifically the BvSatSolver)
* CnfProof
* TheoryProof
* TheoryBV
* Both bitblasters
And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.
This means that references to and interactions with (R)BVP were
pervasive.
Nevertheless, an SMT developer must persist.
The change summary:
* Create a subclass of BVP, called ClausalBitvectorProof, which has
most methods stubbed out.
* Make a some modifications to BVP and ResolutionBitvectorProof as the
natural division of labor between the different classes becomes
clear.
* Go through all the components in the first list and try to figure
out which kind of BVP they should **actually** be interacting with,
and how. Make tweaks accordingly.
* Add a hook from CryptoMinisat which pipes the produced DRAT proof
into the new ClausalBitvectorProof.
* Add a debug statement to ClausalBitvectorProof which parses and
prints that DRAT proof, for testing purposes.
Test:
* `make check` to verify that we didn't break any old stuff, including
lazy BB, and eager BB when using bvminisat.
* `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
-d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
1. It crashed with "Unimplemented"
2. Right before that it prints out the (textual) DRAT proof.
* Remove 2 unneeded methods
* Missed a rename
* Typos
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Andres comments
* Reorder members of TBitblaster
LFSC LRAT Output (#2787)
* LFSC ouput & unit test
* Renamed lrat unit test file
* s/DRAT/LRAT/
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
1. Extracted a filter whitespace function.
2. Added @param annotations.
* Addressing Yoni's comments
Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.
LratInstruction inheritance (#2784)
While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.
While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.
This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.
Fixed linking against drat2er, and use drat2er (#2785)
* Fixed linking against drat2er/drat-trim
We have machinery for linking against drat2er. However, this machinery
didn't quite work because libdrat2er.a contains an (undefined) reference
to `run_drat_trim` from libdrat-trim.a.
Thus, when linking against libdrat2er.a, we also need to link against
libdrat-trim.a.
I made this change, and then tested it by actually calling a function
from the drat2er library (CheckAndConvertToLRAT) which relies on
`run_drat_trim`. Since this invocation compiles, we know that the
linking is working properly now.
* Combined the two libs, per Mathias
* drat2er configured gaurds
New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)
New C++ API: Get rid of mkConst functions (simplify API). (#2783)
Do not rewrite 1-constructor sygus testers to true (#2780)
[BV Proofs] Option for proof format (#2777)
We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!
My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`
and that I could not provide random other option values.
Clause proof printing (#2779)
* Print LFSC proofs of CNF formulas
* Unit Test for clause printing
* Added SAT input proof printing unit test
* Fixed cnf_holds reference. Proofs of CMap_holds
There were references to clauses_hold, which should have been references
to cnf_holds.
Also added a function for printing a value of type CMap_holds, and a
test for this function.
LFSC drat output (#2776)
* 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
New C++ API: Add missing getType() calls to kick off type checking. (#2773)
[DRAT] DRAT data structure (#2767)
* 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
cmake: Disable unit tests for static builds. (#2775)
--static now implies --no-unit-testing.
Fixes #2672.
C++ API: Fix OOB read in unit test (#2774)
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. (#2737)
* [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
New C++ API: Add missing catch blocks for std::invalid_argument. (#2772)
API/Smt2 parser: refactor termAtomic (#2674)
C++ API: Reintroduce zero-value mkBitVector method (#2770)
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 (#2758)
* [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
New C++ API: Add tests for mk-functions in solver object. (#2764)
Clean up BV kinds and type rules. (#2766)
Add missing type rules for parameterized operator kinds. (#2766)
Fix issues with REWRITE_DONE in floating point rewriter (#2762)
Remove noop. (#2763)
Configured for linking against drat2er (#2754)
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.
New C++ API: Add tests for term object. (#2755)
DRAT Signature (#2757)
* 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
Revert "Move ss-combine rewrite to extended rewriter (#2703)" (#2759)
[LRA Proof] Storage for LRA proofs (#2747)
* [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.
Fixed typos.
New C++ API: Add tests for opterm object. (#2756)
Fix extended rewriter for binary associative operators. (#2751)
This was causing assertion failures when using Sets + Sygus.
Make single invocation and invariant pre/post condition templates 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.
New C++ API: Add tests for sort functions of solver object. (#2752)
Remove spurious map (#2750)
Fix compiler warnings. (#2748)
API: Add simple empty/sigma regexp unit tests (#2746)
[LRA proof] More complete LRA example proofs. (#2722)
* [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 (#2743)
* [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.
Remove alternate versions of mbqi (#2742)
LRAT signature (#2731)
* 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.
BoolToBV modes (off, ite, all) (#2530)
Strings: Make EXTF_d inference more conservative (#2740)
Arith Constraint Proof Loggin (#2732)
* Arith Constraint Proof Logging
Also a tiny documentation update.
* Debug.isOn check around iterated output
* reference iteratees
Enable BV proofs when using an eager bitblaster (#2733)
* 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
Fix use-after-free due to destruction order (#2739)
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.
Take into account minimality and types for cached PBE solutions (#2738)
Apply extended rewriting on PBE static symmetry breaking. (#2735)
Enable regular expression elimination by default. (#2736)
Seems to have no impact on Norn, and is helpful for a number of applications.
Skip non-cardinality types in sets min card inference (#2734)
Bit vector proof superclass (#2599)
* 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
Optimizations for PBE strings (#2728)
Infrastructure for sygus side conditions (#2729)
Combine sygus stream with PBE (#2726)
Improve interface for sygus grammar cons (#2727)
Information gain heuristic for PBE (#2719)
Optimize re-elim for re.allchar components (#2725)
Improve skolem caching by normalizing skolem args (#2723)
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.
Generalize sygus stream solution filtering to logical strength (#2697)
Improve cegqi engine trace. (#2714)
Make (T)NodeTrie a general utility (#2489)
This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.
Fix coverity warnings in datatypes (#2553)
This caches some information regarding tester applications and changes int -> size_t in a few places.
Lazy model construction in TheoryEngine (#2633)
Reduce lookahead when parsing string literals (#2721)
LRA proof signature fixes and a first proof for linear polynomials (#2713)
* 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.
Use https for antlr3.org downloads (#2701)
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.
Move ss-combine rewrite to extended rewriter (#2703)
We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.
Add rewrite for (str.substr s x y) --> "" (#2695)
This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.
Cache evaluations for PBE (#2699)
Quickly recognize when PBE conjectures are infeasible (#2718)
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.
Obvious rewrites to floating-point < and <=. (#2706)
Support string replace all (#2704)
Fix type enumerator for FP (#2717)
Fix real2int regression. (#2716)
Change lemma proof step storage & iterators (#2712)
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
Clausify context-dependent simplifications in ext theory (#2711)
Fix E-matching for case where candidate generator is not properly initialized (#2708)
Expand definitions prior to model core computation (#2707)
cmake: Require boost 1.50.0 for examples. (#2710)
cmake: Add option to explicitely enable/disable static binaries. (#2698)
Evaluator: add support for str.code (#2696)
Adding default SyGuS grammar construction for arrays (#2685)
Fix collectEmptyEqs in string rewriter (#2692)
Fix for itos reduction (#2691)
Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)
Change default sygus enumeration mode to auto (#2689)
Fix coverity warnings in sygus enumerator (#2687)
New C++ API: Split unit tests. (#2688)
Increasing coverage (#2683)
This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.
API: Fix assignment operators (#2680)
The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.
Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
configure.sh: Fix option parsing to match --help (#2611)
Allow partial models with optimized sygus enumeration (#2682)
Implement option to turn off symmetry breaking for basic enumerators (#2686)
Improves the existing implementation for sygus-active-gen=basic.
Refactor default grammars construction (#2681)
fixes to regression docs (#2679)
Add optimized sygus enumeration (#2677)
Record assumption info in AssertionPipeline (#2678)
Minor improvement to sygus trace (#2675)
CMake: Set RPATH on installed binary (#2671)
Currently, when installing CVC4 with a custom installation directory on
macOS, the resulting binary cannot be executed because the linker cannot
find the required libraries (e.g. our parser). This commit changes our
build system to use the `CMAKE_INSTALL_RPATH` variable to add the
installation directory to the RPATH list in the exectuable.
Do not use lazy trie for sygus-rr-verify (#2668)
Fail for SWIG 3.0.8 (#2656)
Ran into this bug when compiling with python3 bindings: https://github.com/swig/swig/issues/588
Instantiating any object crashes python. Since swig3.0.8 is currently the apt-get install for Ubuntu 16.04, I thought it'd be good to have a check for that. If python3 is preferred and the swig version is 3.0.8, it errors out and asks users to downgrade or upgrade SWIG.
CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)
Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.
[0] https://github.com/CVC4/CVC4/blob/7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36
Only build CryptoMiniSat library, no binary (#2657)
This commit changes the contrib/get-cryptominisat script to only build
the CryptoMiniSat library instead of both the library and the binary.
The advantage of this is that we can compile a static version of the
CryptoMiniSat library without having a static version of glibc or
libstdc++ (this is fine as long as we do a shared library build of
CVC4). This is an issue on Fedora (tested on version 25) where the
contrib/get-cryptominisat script was failing when building the
CryptoMiniSat binary due to the static version of these libraries not
being available. Since we just want to build the library, the commit
also changes the script to not install CryptoMiniSat anymore and updates
the CMake find script to accomodate the new folder structure. Side note:
the folder structure generated after this commit is a bit more uniform
with, e.g. the CaDiCaL script: The source files are directly in the
cryptominisat5 folder, not in a subfolder.
Recover from wrong use of get-info :reason-unknown (#2667)
Fixes #2584. Currently, we are immediately terminating CVC4 if the user
issues a `(get-info :reason-unknown)` command if it didn't succeed a
`(check-sat)` call returning `unknown`. This commit changes the behavior
to return an `(error ...)` but continue executing afterwards. It turns
the `ModalException` thrown in this case into a
`RecoverableModalException` and adds a check in
`GetInfoCommand::invoke()` to turn it into a
`CommandRecoverableFailure`, which solves the issue.
Remove antlr_undefines.h. (#2664)
Is not required anymore since we don't use autotools anymore.
Add substr, contains and equality rewrites (#2665)
Disable dumping test for non-dumping builds (#2662)
Travis: run examples and avoid building them twice (#2663)
`make check` builds the examples but does not run them. This commit
changes our Travis script to run the examples after building them and
removes `makeExamples()` to avoid building them twice.
BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. (#2647)
Simplifications based on the special const is now delegated down, only
the concat is pulled up.
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const. (#2647)
Sygus streaming non-implied predicates (#2660)
Remove autotools build system. (#2639)
Fix util::Random for macOS builds (#2655)
Add helper to detect length one string terms (#2654)
This commit introduces a helper function to detect string terms that
have exactly/at most length one. This is useful for a lot of rewrites
because strings of at most length one are guaranteed to not overlap
multiple components in a concatenation, which allows for more aggressive
rewriting.
This commit has been tested with --sygus-rr-synth-check for >1h on the
string term grammar.
Add OptionException handling during initialization (#2466)
The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:
1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes
This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor). Finally,
the commit adds a simple regression test for invalid dump tags.
cmake: Run regression level 2 for make check. (#2645)
Non-implied mode for model cores (#2653)
Non-contributing find replace rewrite (#2652)
Improve reduction for str.to.int (#2636)
Introducing internal commands for SyGuS commands (#2627)
Constant length regular expression elimination (#2646)
Skip sygus-rr-synth-check regressions when ASAN on (#2651)
This commit disables three regressions when using an ASAN build. The
regressions are all leaking memory when invoking the subsolver (see
issue #2649). Debugging the issue will take a while but is not very
critical since this feature is currently only used by CVC4 developers
but it prevents our nightly builds from going through.
Show if ASAN build in --show-config (#2650)
This commit extends `--show-config` to show whether the current build is
an ASAN build or not. This is done by moving a detection that was
previously done for the unit tests into base/configuration_private.h.
In addition to being convenient, this allows us to easily exclude
regression tests from ASAN builds.
Sygus query generator (#2465)
Fix context-dependent for positive contains reduction (#2644)
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643)
Match: `x_m | concat(y_my, 0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, ~0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)`
On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
| CVC4-base | CVC4-concatpullup-or |
BENCHMARK | SLVD SAT UNSAT TO MO CPU[s] | SLVD SAT UNSAT TO MO CPU[s] |
totals | 38992 13844 25148 1082 28 984887.4 | 39028 13845 25183 1046 28 974819.1 |
```
cmake: Add CxxTest include directory to unit test includes. (#2642)
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ones (#2596).
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 1 (#2596).
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
Improve strings reductions including skolem caching for contains (#2641)
Improve reduction for int.to.str (#2629)
Option for shuffling condition pool in CegisUnif (#2587)
cmake: Generate git_versioninfo.cpp on build time. (#2640)
Delay initialization of theory engine (#2621)
This implements solution number 2 for issue #2613.
Add more (str.replace x y z) rewrites (#2628)
Fix fp-bool.sy grammar and require symfpu (#2631)
Reset input language for ExprMiner subsolver (#2624)
Improvements to rewrite rules from inputs (#2625)
Add rewrites for str.replace in str.contains (#2623)
This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.
Fix heuristic for string length approximation (#2622)
Refactor printing of parameterized operators in smt2 (#2609)
Improve reasoning about empty strings in rewriter (#2615)
Fix partial operator elimination in sygus grammar normalization (#2620)
Fix string ext inference for rewrites that introduce negation (#2618)
Fix default setting of CegisUnif options (#2605)
cmake: Use gcovr instead lcov for coverage report generation. (#2617)
Fix compiler warnings (#2602)
Synthesize rewrite rules from inputs (#2608)
Fix cegis so that evaluation unfolding is not interleaved. (#2614)
Optimize regular expression elimination (#2612)
Add length-based rewrites for (str.substr _ _ _) (#2610)
Support for basic actively-generated enumerators (#2606)
Random: support URNG interface (#2595)
Use std::shuffle (with Random as the unified random generator) instead
of std::random_shuffle for deterministic, reproducable random shuffling.
Allow multiple synthesis conjectures. (#2593)
Fix compiler warnings. (#2601)
BV instantiator: Factor out util functions. (#2604)
Previously, all util functions for the BV instantiator were static functions
in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding
unit test, it was therefore required to include this cpp file in order to
test these functions. This factors out these functions into a
theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h).
Asan reported errors for the corresponing unit test because of this.
BV inverter: Factor out util functions. (#2603)
Previously, all invertibility condition functions were static functions
in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test,
it was therefore required to include this cpp file in order to test
these functions. This factors out these functions into a
theory/quantifiers/bv_inverter_utils.(cpp|h).
Fix string register extended terms (#2597)
A regress2 benchmark was failing, due to a recent change in our strings rewriter.
The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.
The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.
This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.
Cmake: Fix ctest call for example/translator. (#2600)
example/translator expects an input file to translate but none was provided in the ctest call.
This caused the ctest call to hang and wait for input on stdin in some configurations (in
particular in the nightlies).
Address slow sygus regressions (#2598)
Disable extended rewriter when applicable with var agnostic enumeration (#2594)
Fix unif trace (#2550)
Fix cache for sygus post-condition inference (#2592)
Update default options for sygus (#2586)
Fix rewrite rule filtering. (#2591)
New C++ API: Add checks for Sorts. (#2519)
Infrastructure for string length entailments via approximations (#2514)
Only use SKIP_RETURN_CODE with CMake 3.9.0+ (#2590)
With older versions of CMake, skipped tests are reported as failures,
which is undesirable. This commit changes the CMakeLists file to only
use the `SKIP_RETURN_CODE` property if a newer version of CMake is used.
Fix end constraint for regexp elimination (#2571)
Clean remaining references to getNextDecisionRequest and simplify (#2500)
Fix mem leak in sha1_collision example. (#2588)
Fix mem leak in sets_translate example. (#2589)
Simplify datatypes printing (#2573)
Fix compiler warnings. (#2585)
Fix regress (#2575)
Add actively generated sygus enumerators (#2552)
Make CegisUnif with condition independent robust to var agnostic (#2565)
Fix stale op list in sets (#2572)
Eliminate partial operators within lambdas during grammar normalization (#2570)
cmake: Display skipped tests as not run (#2567)
Currently, the run_regression.py script just returns 0 when we skip a
test due to a feature not supported by the current configuration.
Returning 0 marks those tests as passed. To make it more clear which
tests were skipped, this commit adds the `SKIP_RETURN_CODE` [0] property
to the regression tests and changes the regression script to return 77
for skipped tests. The feature is supported since at least CMake 3.0 [0].
For backwards compatibility with autotools, returning 77 for skipped
tests is only active when `--cmake` is passed to the run_regression.py
script.
[0] https://cmake.org/cmake/help/v3.0/prop_test/SKIP_RETURN_CODE.html
Allow (_ to_fp ...) in strict parsing mode (#2566)
When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
unit: Fix ASAN detection for GCC. (#2561)
Make registration of preprocessing passes explicit (#2564)
As it turns out, self-registering types are problematic with static
linkage [0]. Instead of fixing the issue with linker flags, which seems
possible but also brittle (e.g. the flags may be different for different
linkers), this commit adds an explicit registration of each
preprocessing pass.
[0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html
Fix documentation for `make regress`. (#2557)
cmake: Add examples to build-tests, add warning for disabling static build. (#2562)
Fix "catching polymorphic type by value" warnings (#2556)
When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make
sure that we use a reference type for the exception, otherwise the unit
test tries to catch the exception by value, resulting in "catching
polymorphic type by value" warnings.
cmake: Generate compile_commands.json on configure. (#2559)
cmake: Add build target build-tests to build all test dependencies. (#2558)
init scalar class members (coverity issues 1473720 and 1473721) (#2554)
Fix compiler warnings. (#2555)
Fix dumping pre/post preprocessing passes (#2469)
This commit changes the hard-coded list of checks for
preprocessing-related dump tags to take advantage of the new
preprocessing pass registration mechanism from PR #2468. It also fixes a
typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()`
and adds a list of available passes to the `--dump help` output.
Refactor preprocessing pass registration (#2468)
This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.
As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.
This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.
[0] https://llvm.org/docs/WritingAnLLVMPass.html
Add rewrite for solving stoi (#2532)
cmake: Ignore ctest exit code for coverage reports.
Stream concrete values for variable agnostic enumerators (#2526)
Rewrites for (= "" _) and (= (str.replace _) _) (#2546)
cmake: Only do Java tests when unit testing on (#2551)
Right now, we are adding the Java tests even when we are not building
unit tests. This commit changes the build system to only add the Java
tests when unit tests are enabled. There are two reasons for this
change:
- building a production version of CVC4 should not require JUnit
- it seems more intuitive (to me at least) to disable JUnit tests when
unit tests are disabled
This change also simplifies building the Java bindings in our homebrew
formula.
cmake: Add CxxTest finder module to allow custom paths. (#2542)
Remove assertion. (#2549)
Infrastructure for using active enumerators in sygus modules (#2547)
Incorporate all unification enumerators into getTermList. (#2541)
Fix Taylor overapproximation for large exponentials (#2538)
Fix homogeneous string constant rewrite (#2545)
Fix bug in getSymbols. (#2544)
cmake: Only print dumping warning if not disabled by user. (#2543)
Makes SyGuS parsing more robust in invariant problems (#2509)
cmake: Fix test target dependency issues. (#2540)
Enable quantified array regression. (#2539)
Symmetry breaking for variable agnostic enumerators (#2527)
cmake: New INSTALL.md for build and testing instructions. (#2536)
cmake: Exclude examples for coverage target. (#2535)
Eagerly ensure literal on active guards for sygus enumerators (#2531)
cmake: Add check for GCC 4.5.1 and warn user. (#2533)
examples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534)
cmake: configure.sh wrapper: Removed unused option --gmp.
carefully printing trusted assertions in proofs (#2505)
cmake: Fix tag code generation dependencies. (#2529)
Fix warnings uncovered by cmake build (#2521)
Fix quantifiers selector over store rewrite (#2510)
Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in.
After the change, we are +61-7 on SMT LIB:
https://www.starexec.org/starexec/secure/details/job.jsp?id=30581
Allow partial models for multiple sygus enumerators (#2499)
Infrastructure for variable agnostic sygus enumerators (#2511)
Improve non-linear check model error handling (#2497)
Refactor strings equality rewriting (#2513)
This moves the extended rewrites for string equality to the main strings rewriter as a function rewriteEqualityExt, and makes this function called on every equality that is generated (from non-equalities) by our rewriter.
cmake: Fix dependencies for code generation. (#2524)
Fix wiki urls. (#2504)
cmake: Fix git version info (again). (#2523)
cmake: Fix theory order #2. (#2522)
Unify rewrites related to (str.contains x y) --> (= x y) (#2512)
cmake: Fix theory order. (#2518)
Make string rewriter unit tests more robust (#2520)
This commit changes the unit test for the string rewriter to use the
extended rewriter instead of the regular rewriter to make it more
robust, e.g. to different orderings in conjunctions.
cmake: Fix and simplify git version info. (#2516)
cmake: Add program prefix option. (#2515)
Fix generating debug/trace tags.
New C++ API: Add checks for Terms/OpTerms. (#2455)
Fix regress2. (#2502)
cmake: Add python3 option.
cmake: Enable -Wall.
cmake: Fix systemtests dependency.
cmake: Build fully static binaries with option --static.
cmake: Run make coverage in parallel by default.
cmake: Add more documentation, some fixes and cleanup.
cmake: configure.sh wrapper: Use explicit build directory structure.
We don't create build directories for every build type (and
configuration) anymore. The default build directory is now 'build'
(created where you call the wrapper script from). Option --name allows
to configure an individual name (and path) for the build directory.
cmake: configure wrapper: Modify next steps message after configuration.
Since configure.sh is only a wrapper for cmake it prints all the messages from
cmake. At the end we print the next steps after configuration. If configure.sh
is used we add the info to also change into the build directory before calling
make.
cmake: Move PACKAGE_NAME to ConfigureCVC4, more cleanup.
cmake: Refactor cvc4_add_unit_test macro to support test names with '/'.
Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
cmake: Guard GetGitRevisionDescription.
cmake: Add target runexamples.
cmake: Add support for cross-compiling for Windows.
cmake: Require JUnit version 4.
cmake: Do not allow dumping with portfolio build.
cmake: More documentation, clean up.
cmake: Move extracting git information to src/base cmake config file.
cmake: Guard examples that require Boost.
cmake: Disable unit tests if assertions are not enabled.
cmake: FindANTLR: Check if antlr3FileStreamNew is available.
cmake: configure.sh wrapper: Fixes for sh.
travis: Switch to cmake.
cmake: Do not build examples and unit and system tests by default.
cmake: configure.sh wrapper: Add --name option.
cmake: examples: Configure output directory per target.
cmake: Added java examples
cmake: configure.sh wrapper: Add --prefix for install directory.
cmake: Add some more documentation, cleanup.
cmake: Move helper functions to cmake/Helpers.cmake.
cmake: Added target examples (currently .cpp examples only)
cmake: Simplify build type configuration.
cmake: Refactor and clean up build profile printing.
cmake: Added target check
Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.
cmake: Add make install rule.
cmake: configure.sh wrapper: Fix handling of options with arguments.
cmake: Add module finder for Valgrind.
cmake: Various CMakeLists.txt fixes/cleanup.
cmake: Only build libcvc4 and libcvc4parser as libraries.
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.
cmake: Move find_package to where it is actually needed.
cmake: configure.sh wrapper: Removed env vars help text.
cmake: configure.sh wrapper: Configurable build directory
cmake: configure.sh wrapper: Create build dirs for configurations
cmake: configure.sh wrapper: done (except: configurable build dir)
cmake: Updated and prettified configuration printing.
cmake: configure.sh wrapper: option parsing
cmake: Add ENABLE_DEBUG_CONTEXT_MM to enable the debug context memory manager.
cmake: Add ENABLE_BEST to enable best configuration of dependencies.
cmake: Add Java runtime as required dependency (required for ANTLR).
cmake: Add convenience wrappers for tag generation.
cmake: Add library versioning for libcvc4.so.
cmake: Rebase with current master, add new tests/source files.
cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.
cmake: Use target specific includes for libcvc4.
Further, print definitions added with add_definitions(...).
cmake: Add missing dependency.
cmake: Add support for building static binaries/libraries.
cmake: Add options for specifying install directories for dependencies.
cmake: Add module finder for GLPK-cut-log.
cmake: Add module finder for ABC.
cmake: Compile Java tests and add to ctest if Java bindings are enabled.
cmake: Add SWIG support + Python and Java bindings.
cmake: Add dependencies for test targets and support for make coverage.
cmake: Various portfolio/default option fixes.
cmake: Enable parallel execution for test targets regress, units, systemtests.
cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.
cmake: Added system tests and target make systemtests.
cmake: Added regression tests and target make regress.
cmake: Add portfolio support.
cmake: Add ASAN support.
cmake: Enable shared by default.
Further, force shared builds in case of unit tests.
cmake: Disable W-suggest-override for unit tests.
cmake: Add target units.
cmake: Removed obsolete CMakeLists file in test.
cmake: Add support for CxxTest.
cmake: Filter through and disable unused HAVE_* variables from autotools.
cmake: Do not set global output directories for binaries and libraries.
cmake: Fix some includes.
cmake: Added support for coverage and profiling.
cmake: Added 3-valued option handling (to enable detection of user-set options).
cmake: Add module finder for readline.
cmake: Generate token headers.
cmake: Added licensing options and warnings/errors.
cmake: Cleanup CMakeLists.txt files, remove SHARED.
cmake: Add build configurations.
cmake: Fixed compiler flag macros.
cmake: Add module finder for LFSC.
cmake: Add module finder for CaDiCaL.
cmake: Add module finder for CryptoMiniSat.
cmake: Add module finder for SymFPU.
cmake: Add module finder for CLN.
cmake: Add libsignatures for proofs.
cmake: Remove unused CMakeLists.txt
cmake: Generate cvc4autoconfig.h (options currently statically set).
cmake: Added missing dependency for src/util
cmake: Working build infrastructure.
TODO: cvc4autoconfig.h
cmake: Antlr parser generation done.
cmake: Generate trace and debug tags
cmake: .cpp generation done, .h generation not yet complete
cmake: Added initial build infrastructure.
Decision strategy: incorporate arrays. (#2495)
Add rewrites for str.contains + str.replace/substr (#2496)
Decision strategy: incorporate separation logic. (#2494)
Add two rewrites for string contains character (#2492)
Refactor strings extended functions inferences (#2480)
This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type.
This is in preparation for working on solving equations and further inferences in this style.
New C++ API: Introduce new macro and exception for API checks. (#2486)
Fix issue with str.idof in evaluator (#2493)
Decision strategy: incorporate strings fmf. (#2485)
More aggressive caching of string skolems. (#2491)
Move and rename sygus solver classes (#2488)
fix assertion error (#2487)
Clean remaining references to getNextDecisionRequest in quantifiers. (#2484)
Improvements and fixes for symmetry detection and breaking (#2459)
This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.
Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)
Decision strategy: incorporate cegis unif (#2482)
Decision strategy: incorporate bounded integers (#2481)
Decision strategy: incorporate datatypes sygus solver. (#2479)
More aggressive skolem caching for strings, document and clean preprocessor (#2478)
Make strings model construction robust to lengths that are not propagated equal (#2444)
This fixes #2429.
This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment.
We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.
Regardless, the strings model construction should be robust to handle this case, which this PR does.
Follow redirects with cURL in contrib/get* scripts (#2471)
On systems without `wget`, we use `curl` to download dependencies.
However, we were not using the `-L` (follow redirects) option, which is
necessary to download certain dependencies, e.g. CryptoMiniSat.
Remove broken dumping support from portfolio build (#2470)
Dumping support for portfolio builds was introduced in
84f26af22566f7c10dea45b399b944cb50b5e317 but as far as I can tell, the
implementation has already been problematic in the original implementation. The
current implementation has the following issues:
- Dumping with a portfolio build (even when using the single threaded
executable) results in a segfault. The reason is that the DumpChannel variable
is declared as an `extern` and exists for the duration of the program. The
problem is that it stores a `CommandSequence`, which indirectly may store
nodes. When shutting down CVC4, the destructor of `DumpC` is called, which
destroys the `CommandSequence`, which results in a segfault because the
`NodeManager` does not exist anymore. The node manager is (indirectly) owned
and destroyed by the `api::Solver` object.
- Additionally, adding commands to the `CommandSequence` is not thread safe (it
just calls `CommandSequence::addCommand()`, which in turn pushes back to a
vector [0] (which is not thread safe [1]). A single instance of `DumpChannel`
is shared among all threads (it is not declared `thread_local` [2]).
- The `CommandSequence` in `DumpC` was not used in the original implementation
and is still unused on master. The original commit mentions that the portfolio
build stores the commands in the `CommandSequence` but not why.
This commit removes the `CommandSequence` and related methods from `DumpC` to
avoid the issue when destroying `DumpChannel`. It disables dumping for
portfolio builds and adds a check at configure-time that not both options have
been enabled simultaneously. Given that the option was not functional
previously, the problematic implementation, and the fact that the dump of
multiple threads wouldn't be very useful, disabling dumping for portfolio
builds is unlikely to be problem. An improvement that could be made is to
disable dumping support only for the pcvc4 binary and while enabling it for the
single-threaded version, even when using `--with-portfolio`. However, we
currently do not have the infrastructure for that (we use the same libcvc4
library for both binaries).
[0] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/command.cpp#L756
[1] https://en.cppreference.com/w/cpp/container
[2] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/dump.h#L117
Remove unnecessary tracing from preprocessing (#2472)
With the introduction of the PreprocessingPass class,
tracing/dumping/time keeping is done automatically in the base class,
eliminating the need for doing it manually. This commit cleans up
SmtEngine, removing tracing/dumping/time keeping in preprocessing that
is not needed anymore.
Decision strategy: incorporate UF with cardinality constraints (#2476)
Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462)
Refactor how assertions are added to decision engine (#2396)
Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.
Add Skolem cache for strings, refactor length registration (#2457)
This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor).
It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled.
Generalize CandidateRewriteDatabase to ExprMiner (#2340)
Fix #include for minisat headers in bvminisat. (#2463)
Uses information gain heuristic for building better solutions from DTs (#2451)
Simplify storing of transcendental function applications that occur in assertions (#2458)
Decision strategy: incorporate CEGQI (#2460)
New C++ API: Try to fix (false positive) Coverity warnings. (#2454)
Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461)
Initial infrastructure for theory decision manager (#2447)
Fix for when strings process loop is disabled. (#2456)
Fixe compiler warning in line_buffer.cpp. (#2453)
Support model cores via option --produce-model-cores. (#2407)
This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
Avoid calling size() every iteration (#2450)
Fix global negate (#2449)
fix (#2446)
Set NodeManager to nullptr when exporting vars (#2445)
PR #2409 assumed that temporarily setting the NodeManager to nullptr
when creating variables is not needed anymore. However, this made our
portfolio build fail. This commit reintroduces the temporary NodeManager
change while creating variables.
Using a single condition enumerator in sygus-unif (#2440)
This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).
In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:
- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.
A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.
There is also small improvements for trace messages.
Refactor non-clausal simplify preprocessing pass. (#2425)
Squash implementation of counterexample-guided instantiation (#2423)
Add (str.replace (str.replace y w y) y z) rewrite (#2441)
Replace boost::integer_traits with std::numeric_limits. (#2439)
Further, remove redundant gmp.h include in options_handler.cpp.
Remove clock_gettime() replacement for macOS. (#2436)
Not needed anymore since macOS 10.12 introduced clock_gettime().
Make isClosedEnumerable a member of TypeNode (#2434)
Further simplify and fix initialization of ce guided instantiation (#2437)
Refactor and document quantifiers variable elimination and conditional splitting (#2424)
Minor improvements to interface for rep set. (#2435)
More extended rewrites for strings equality (#2431)
Eliminate select over store in quantifier bodies (#2433)
Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)
Remove printing support for sygus enumeration types (#2430)
Finer-grained inference of substitutions in incremental mode (#2403)
Add regex grammar to rewriter verification tests (#2426)
Extended rewriter for string equalities (#2427)
Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)
Remove redundant strings rewrite. (#2422)
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since
re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )
This PR removes the above rewrite, which was implemented incorrectly and was dead code.
Update INSTALL instructions (#2420)
Fixes #2419. This commit adds more information about optional
dependencies, updates macOS-related information, and fixes some details.
Remove CVC3 compatibility layer (#2418)
Remove unused options file (#2413)
Minor improvements to theory model builder interface. (#2408)
Make quantifiers strategies exit immediately when in conflict (#2099)
Transfer ownership of learned literals from SMT engine to circuit propagator. (#2421)
Fix merge mishap of #2359.
Refactor ceg conjecture initialization (#2411)
Allows SAT checks of repair const to have different options (#2412)
Refactor and document alpha equivalence. (#2402)
Fix export of bound variables (#2409)
Refactor theory preprocess into preprocessing pass. (#2395)
Use useBland option in FCSimplexDecisionProcedure (#2405)
Add regular expression elimination module (#2400)
Refactor MipLibTrick preprocessing pass. (#2359)
Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)
fix bv total ops printing (#2365)
Split term canonize utility to own file and document (#2398)
Reorder …
adacore-bot
pushed a commit
to AdaCore/spark2014
that referenced
this issue
Apr 18, 2019
Project: cvc4 master 5321dfb1161032a79909a588ed05bb27d42ba579
MS114-013 Merging upstream cvc4 into our master
Change-Id: I1b9af6c730515e0be2156aa595fa62e678a086c7
Only check disequal terms with sygus-rr-verify (#2793)
ClausalBitvectorProof (#2786)
* [DRAT] ClausalBitvectorProof
Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)
It fits into the `BitvectorProof` class hierarchy like this:
```
BitvectorProof
/ \
/ \
ClausalBitvectorProof ResolutionBitvectorProof
```
This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
* CnfStream
* SatSolver (specifically the BvSatSolver)
* CnfProof
* TheoryProof
* TheoryBV
* Both bitblasters
And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.
This means that references to and interactions with (R)BVP were
pervasive.
Nevertheless, an SMT developer must persist.
The change summary:
* Create a subclass of BVP, called ClausalBitvectorProof, which has
most methods stubbed out.
* Make a some modifications to BVP and ResolutionBitvectorProof as the
natural division of labor between the different classes becomes
clear.
* Go through all the components in the first list and try to figure
out which kind of BVP they should **actually** be interacting with,
and how. Make tweaks accordingly.
* Add a hook from CryptoMinisat which pipes the produced DRAT proof
into the new ClausalBitvectorProof.
* Add a debug statement to ClausalBitvectorProof which parses and
prints that DRAT proof, for testing purposes.
Test:
* `make check` to verify that we didn't break any old stuff, including
lazy BB, and eager BB when using bvminisat.
* `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
-d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
1. It crashed with "Unimplemented"
2. Right before that it prints out the (textual) DRAT proof.
* Remove 2 unneeded methods
* Missed a rename
* Typos
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Andres comments
* Reorder members of TBitblaster
LFSC LRAT Output (#2787)
* LFSC ouput & unit test
* Renamed lrat unit test file
* s/DRAT/LRAT/
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
1. Extracted a filter whitespace function.
2. Added @param annotations.
* Addressing Yoni's comments
Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.
LratInstruction inheritance (#2784)
While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.
While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.
This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.
Fixed linking against drat2er, and use drat2er (#2785)
* Fixed linking against drat2er/drat-trim
We have machinery for linking against drat2er. However, this machinery
didn't quite work because libdrat2er.a contains an (undefined) reference
to `run_drat_trim` from libdrat-trim.a.
Thus, when linking against libdrat2er.a, we also need to link against
libdrat-trim.a.
I made this change, and then tested it by actually calling a function
from the drat2er library (CheckAndConvertToLRAT) which relies on
`run_drat_trim`. Since this invocation compiles, we know that the
linking is working properly now.
* Combined the two libs, per Mathias
* drat2er configured gaurds
New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)
New C++ API: Get rid of mkConst functions (simplify API). (#2783)
Do not rewrite 1-constructor sygus testers to true (#2780)
[BV Proofs] Option for proof format (#2777)
We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!
My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`
and that I could not provide random other option values.
Clause proof printing (#2779)
* Print LFSC proofs of CNF formulas
* Unit Test for clause printing
* Added SAT input proof printing unit test
* Fixed cnf_holds reference. Proofs of CMap_holds
There were references to clauses_hold, which should have been references
to cnf_holds.
Also added a function for printing a value of type CMap_holds, and a
test for this function.
LFSC drat output (#2776)
* 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
New C++ API: Add missing getType() calls to kick off type checking. (#2773)
[DRAT] DRAT data structure (#2767)
* 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
cmake: Disable unit tests for static builds. (#2775)
--static now implies --no-unit-testing.
Fixes #2672.
C++ API: Fix OOB read in unit test (#2774)
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. (#2737)
* [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
New C++ API: Add missing catch blocks for std::invalid_argument. (#2772)
API/Smt2 parser: refactor termAtomic (#2674)
C++ API: Reintroduce zero-value mkBitVector method (#2770)
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 (#2758)
* [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
New C++ API: Add tests for mk-functions in solver object. (#2764)
Clean up BV kinds and type rules. (#2766)
Add missing type rules for parameterized operator kinds. (#2766)
Fix issues with REWRITE_DONE in floating point rewriter (#2762)
Remove noop. (#2763)
Configured for linking against drat2er (#2754)
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.
New C++ API: Add tests for term object. (#2755)
DRAT Signature (#2757)
* 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
Revert "Move ss-combine rewrite to extended rewriter (#2703)" (#2759)
[LRA Proof] Storage for LRA proofs (#2747)
* [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.
Fixed typos.
New C++ API: Add tests for opterm object. (#2756)
Fix extended rewriter for binary associative operators. (#2751)
This was causing assertion failures when using Sets + Sygus.
Make single invocation and invariant pre/post condition templates 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.
New C++ API: Add tests for sort functions of solver object. (#2752)
Remove spurious map (#2750)
Fix compiler warnings. (#2748)
API: Add simple empty/sigma regexp unit tests (#2746)
[LRA proof] More complete LRA example proofs. (#2722)
* [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 (#2743)
* [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.
Remove alternate versions of mbqi (#2742)
LRAT signature (#2731)
* 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.
BoolToBV modes (off, ite, all) (#2530)
Strings: Make EXTF_d inference more conservative (#2740)
Arith Constraint Proof Loggin (#2732)
* Arith Constraint Proof Logging
Also a tiny documentation update.
* Debug.isOn check around iterated output
* reference iteratees
Enable BV proofs when using an eager bitblaster (#2733)
* 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
Fix use-after-free due to destruction order (#2739)
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.
Take into account minimality and types for cached PBE solutions (#2738)
Apply extended rewriting on PBE static symmetry breaking. (#2735)
Enable regular expression elimination by default. (#2736)
Seems to have no impact on Norn, and is helpful for a number of applications.
Skip non-cardinality types in sets min card inference (#2734)
Bit vector proof superclass (#2599)
* 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
Optimizations for PBE strings (#2728)
Infrastructure for sygus side conditions (#2729)
Combine sygus stream with PBE (#2726)
Improve interface for sygus grammar cons (#2727)
Information gain heuristic for PBE (#2719)
Optimize re-elim for re.allchar components (#2725)
Improve skolem caching by normalizing skolem args (#2723)
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.
Generalize sygus stream solution filtering to logical strength (#2697)
Improve cegqi engine trace. (#2714)
Make (T)NodeTrie a general utility (#2489)
This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.
Fix coverity warnings in datatypes (#2553)
This caches some information regarding tester applications and changes int -> size_t in a few places.
Lazy model construction in TheoryEngine (#2633)
Reduce lookahead when parsing string literals (#2721)
LRA proof signature fixes and a first proof for linear polynomials (#2713)
* 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.
Use https for antlr3.org downloads (#2701)
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.
Move ss-combine rewrite to extended rewriter (#2703)
We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.
Add rewrite for (str.substr s x y) --> "" (#2695)
This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.
Cache evaluations for PBE (#2699)
Quickly recognize when PBE conjectures are infeasible (#2718)
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.
Obvious rewrites to floating-point < and <=. (#2706)
Support string replace all (#2704)
Fix type enumerator for FP (#2717)
Fix real2int regression. (#2716)
Change lemma proof step storage & iterators (#2712)
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
Clausify context-dependent simplifications in ext theory (#2711)
Fix E-matching for case where candidate generator is not properly initialized (#2708)
Expand definitions prior to model core computation (#2707)
cmake: Require boost 1.50.0 for examples. (#2710)
cmake: Add option to explicitely enable/disable static binaries. (#2698)
Evaluator: add support for str.code (#2696)
Adding default SyGuS grammar construction for arrays (#2685)
Fix collectEmptyEqs in string rewriter (#2692)
Fix for itos reduction (#2691)
Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)
Change default sygus enumeration mode to auto (#2689)
Fix coverity warnings in sygus enumerator (#2687)
New C++ API: Split unit tests. (#2688)
Increasing coverage (#2683)
This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.
API: Fix assignment operators (#2680)
The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.
Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
configure.sh: Fix option parsing to match --help (#2611)
Allow partial models with optimized sygus enumeration (#2682)
Implement option to turn off symmetry breaking for basic enumerators (#2686)
Improves the existing implementation for sygus-active-gen=basic.
Refactor default grammars construction (#2681)
fixes to regression docs (#2679)
Add optimized sygus enumeration (#2677)
Record assumption info in AssertionPipeline (#2678)
Minor improvement to sygus trace (#2675)
CMake: Set RPATH on installed binary (#2671)
Currently, when installing CVC4 with a custom installation directory on
macOS, the resulting binary cannot be executed because the linker cannot
find the required libraries (e.g. our parser). This commit changes our
build system to use the `CMAKE_INSTALL_RPATH` variable to add the
installation directory to the RPATH list in the exectuable.
Do not use lazy trie for sygus-rr-verify (#2668)
Fail for SWIG 3.0.8 (#2656)
Ran into this bug when compiling with python3 bindings: https://github.com/swig/swig/issues/588
Instantiating any object crashes python. Since swig3.0.8 is currently the apt-get install for Ubuntu 16.04, I thought it'd be good to have a check for that. If python3 is preferred and the swig version is 3.0.8, it errors out and asks users to downgrade or upgrade SWIG.
CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)
Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.
[0] https://github.com/CVC4/CVC4/blob/7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36
Only build CryptoMiniSat library, no binary (#2657)
This commit changes the contrib/get-cryptominisat script to only build
the CryptoMiniSat library instead of both the library and the binary.
The advantage of this is that we can compile a static version of the
CryptoMiniSat library without having a static version of glibc or
libstdc++ (this is fine as long as we do a shared library build of
CVC4). This is an issue on Fedora (tested on version 25) where the
contrib/get-cryptominisat script was failing when building the
CryptoMiniSat binary due to the static version of these libraries not
being available. Since we just want to build the library, the commit
also changes the script to not install CryptoMiniSat anymore and updates
the CMake find script to accomodate the new folder structure. Side note:
the folder structure generated after this commit is a bit more uniform
with, e.g. the CaDiCaL script: The source files are directly in the
cryptominisat5 folder, not in a subfolder.
Recover from wrong use of get-info :reason-unknown (#2667)
Fixes #2584. Currently, we are immediately terminating CVC4 if the user
issues a `(get-info :reason-unknown)` command if it didn't succeed a
`(check-sat)` call returning `unknown`. This commit changes the behavior
to return an `(error ...)` but continue executing afterwards. It turns
the `ModalException` thrown in this case into a
`RecoverableModalException` and adds a check in
`GetInfoCommand::invoke()` to turn it into a
`CommandRecoverableFailure`, which solves the issue.
Remove antlr_undefines.h. (#2664)
Is not required anymore since we don't use autotools anymore.
Add substr, contains and equality rewrites (#2665)
Disable dumping test for non-dumping builds (#2662)
Travis: run examples and avoid building them twice (#2663)
`make check` builds the examples but does not run them. This commit
changes our Travis script to run the examples after building them and
removes `makeExamples()` to avoid building them twice.
BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. (#2647)
Simplifications based on the special const is now delegated down, only
the concat is pulled up.
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const. (#2647)
Sygus streaming non-implied predicates (#2660)
Remove autotools build system. (#2639)
Fix util::Random for macOS builds (#2655)
Add helper to detect length one string terms (#2654)
This commit introduces a helper function to detect string terms that
have exactly/at most length one. This is useful for a lot of rewrites
because strings of at most length one are guaranteed to not overlap
multiple components in a concatenation, which allows for more aggressive
rewriting.
This commit has been tested with --sygus-rr-synth-check for >1h on the
string term grammar.
Add OptionException handling during initialization (#2466)
The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:
1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes
This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor). Finally,
the commit adds a simple regression test for invalid dump tags.
cmake: Run regression level 2 for make check. (#2645)
Non-implied mode for model cores (#2653)
Non-contributing find replace rewrite (#2652)
Improve reduction for str.to.int (#2636)
Introducing internal commands for SyGuS commands (#2627)
Constant length regular expression elimination (#2646)
Skip sygus-rr-synth-check regressions when ASAN on (#2651)
This commit disables three regressions when using an ASAN build. The
regressions are all leaking memory when invoking the subsolver (see
issue #2649). Debugging the issue will take a while but is not very
critical since this feature is currently only used by CVC4 developers
but it prevents our nightly builds from going through.
Show if ASAN build in --show-config (#2650)
This commit extends `--show-config` to show whether the current build is
an ASAN build or not. This is done by moving a detection that was
previously done for the unit tests into base/configuration_private.h.
In addition to being convenient, this allows us to easily exclude
regression tests from ASAN builds.
Sygus query generator (#2465)
Fix context-dependent for positive contains reduction (#2644)
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643)
Match: `x_m | concat(y_my, 0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, ~0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)`
On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
| CVC4-base | CVC4-concatpullup-or |
BENCHMARK | SLVD SAT UNSAT TO MO CPU[s] | SLVD SAT UNSAT TO MO CPU[s] |
totals | 38992 13844 25148 1082 28 984887.4 | 39028 13845 25183 1046 28 974819.1 |
```
cmake: Add CxxTest include directory to unit test includes. (#2642)
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ones (#2596).
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 1 (#2596).
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
Improve strings reductions including skolem caching for contains (#2641)
Improve reduction for int.to.str (#2629)
Option for shuffling condition pool in CegisUnif (#2587)
cmake: Generate git_versioninfo.cpp on build time. (#2640)
Delay initialization of theory engine (#2621)
This implements solution number 2 for issue #2613.
Add more (str.replace x y z) rewrites (#2628)
Fix fp-bool.sy grammar and require symfpu (#2631)
Reset input language for ExprMiner subsolver (#2624)
Improvements to rewrite rules from inputs (#2625)
Add rewrites for str.replace in str.contains (#2623)
This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.
Fix heuristic for string length approximation (#2622)
Refactor printing of parameterized operators in smt2 (#2609)
Improve reasoning about empty strings in rewriter (#2615)
Fix partial operator elimination in sygus grammar normalization (#2620)
Fix string ext inference for rewrites that introduce negation (#2618)
Fix default setting of CegisUnif options (#2605)
cmake: Use gcovr instead lcov for coverage report generation. (#2617)
Fix compiler warnings (#2602)
Synthesize rewrite rules from inputs (#2608)
Fix cegis so that evaluation unfolding is not interleaved. (#2614)
Optimize regular expression elimination (#2612)
Add length-based rewrites for (str.substr _ _ _) (#2610)
Support for basic actively-generated enumerators (#2606)
Random: support URNG interface (#2595)
Use std::shuffle (with Random as the unified random generator) instead
of std::random_shuffle for deterministic, reproducable random shuffling.
Allow multiple synthesis conjectures. (#2593)
Fix compiler warnings. (#2601)
BV instantiator: Factor out util functions. (#2604)
Previously, all util functions for the BV instantiator were static functions
in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding
unit test, it was therefore required to include this cpp file in order to
test these functions. This factors out these functions into a
theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h).
Asan reported errors for the corresponing unit test because of this.
BV inverter: Factor out util functions. (#2603)
Previously, all invertibility condition functions were static functions
in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test,
it was therefore required to include this cpp file in order to test
these functions. This factors out these functions into a
theory/quantifiers/bv_inverter_utils.(cpp|h).
Fix string register extended terms (#2597)
A regress2 benchmark was failing, due to a recent change in our strings rewriter.
The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.
The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.
This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.
Cmake: Fix ctest call for example/translator. (#2600)
example/translator expects an input file to translate but none was provided in the ctest call.
This caused the ctest call to hang and wait for input on stdin in some configurations (in
particular in the nightlies).
Address slow sygus regressions (#2598)
Disable extended rewriter when applicable with var agnostic enumeration (#2594)
Fix unif trace (#2550)
Fix cache for sygus post-condition inference (#2592)
Update default options for sygus (#2586)
Fix rewrite rule filtering. (#2591)
New C++ API: Add checks for Sorts. (#2519)
Infrastructure for string length entailments via approximations (#2514)
Only use SKIP_RETURN_CODE with CMake 3.9.0+ (#2590)
With older versions of CMake, skipped tests are reported as failures,
which is undesirable. This commit changes the CMakeLists file to only
use the `SKIP_RETURN_CODE` property if a newer version of CMake is used.
Fix end constraint for regexp elimination (#2571)
Clean remaining references to getNextDecisionRequest and simplify (#2500)
Fix mem leak in sha1_collision example. (#2588)
Fix mem leak in sets_translate example. (#2589)
Simplify datatypes printing (#2573)
Fix compiler warnings. (#2585)
Fix regress (#2575)
Add actively generated sygus enumerators (#2552)
Make CegisUnif with condition independent robust to var agnostic (#2565)
Fix stale op list in sets (#2572)
Eliminate partial operators within lambdas during grammar normalization (#2570)
cmake: Display skipped tests as not run (#2567)
Currently, the run_regression.py script just returns 0 when we skip a
test due to a feature not supported by the current configuration.
Returning 0 marks those tests as passed. To make it more clear which
tests were skipped, this commit adds the `SKIP_RETURN_CODE` [0] property
to the regression tests and changes the regression script to return 77
for skipped tests. The feature is supported since at least CMake 3.0 [0].
For backwards compatibility with autotools, returning 77 for skipped
tests is only active when `--cmake` is passed to the run_regression.py
script.
[0] https://cmake.org/cmake/help/v3.0/prop_test/SKIP_RETURN_CODE.html
Allow (_ to_fp ...) in strict parsing mode (#2566)
When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
unit: Fix ASAN detection for GCC. (#2561)
Make registration of preprocessing passes explicit (#2564)
As it turns out, self-registering types are problematic with static
linkage [0]. Instead of fixing the issue with linker flags, which seems
possible but also brittle (e.g. the flags may be different for different
linkers), this commit adds an explicit registration of each
preprocessing pass.
[0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html
Fix documentation for `make regress`. (#2557)
cmake: Add examples to build-tests, add warning for disabling static build. (#2562)
Fix "catching polymorphic type by value" warnings (#2556)
When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make
sure that we use a reference type for the exception, otherwise the unit
test tries to catch the exception by value, resulting in "catching
polymorphic type by value" warnings.
cmake: Generate compile_commands.json on configure. (#2559)
cmake: Add build target build-tests to build all test dependencies. (#2558)
init scalar class members (coverity issues 1473720 and 1473721) (#2554)
Fix compiler warnings. (#2555)
Fix dumping pre/post preprocessing passes (#2469)
This commit changes the hard-coded list of checks for
preprocessing-related dump tags to take advantage of the new
preprocessing pass registration mechanism from PR #2468. It also fixes a
typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()`
and adds a list of available passes to the `--dump help` output.
Refactor preprocessing pass registration (#2468)
This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.
As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.
This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.
[0] https://llvm.org/docs/WritingAnLLVMPass.html
Add rewrite for solving stoi (#2532)
cmake: Ignore ctest exit code for coverage reports.
Stream concrete values for variable agnostic enumerators (#2526)
Rewrites for (= "" _) and (= (str.replace _) _) (#2546)
cmake: Only do Java tests when unit testing on (#2551)
Right now, we are adding the Java tests even when we are not building
unit tests. This commit changes the build system to only add the Java
tests when unit tests are enabled. There are two reasons for this
change:
- building a production version of CVC4 should not require JUnit
- it seems more intuitive (to me at least) to disable JUnit tests when
unit tests are disabled
This change also simplifies building the Java bindings in our homebrew
formula.
cmake: Add CxxTest finder module to allow custom paths. (#2542)
Remove assertion. (#2549)
Infrastructure for using active enumerators in sygus modules (#2547)
Incorporate all unification enumerators into getTermList. (#2541)
Fix Taylor overapproximation for large exponentials (#2538)
Fix homogeneous string constant rewrite (#2545)
Fix bug in getSymbols. (#2544)
cmake: Only print dumping warning if not disabled by user. (#2543)
Makes SyGuS parsing more robust in invariant problems (#2509)
cmake: Fix test target dependency issues. (#2540)
Enable quantified array regression. (#2539)
Symmetry breaking for variable agnostic enumerators (#2527)
cmake: New INSTALL.md for build and testing instructions. (#2536)
cmake: Exclude examples for coverage target. (#2535)
Eagerly ensure literal on active guards for sygus enumerators (#2531)
cmake: Add check for GCC 4.5.1 and warn user. (#2533)
examples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534)
cmake: configure.sh wrapper: Removed unused option --gmp.
carefully printing trusted assertions in proofs (#2505)
cmake: Fix tag code generation dependencies. (#2529)
Fix warnings uncovered by cmake build (#2521)
Fix quantifiers selector over store rewrite (#2510)
Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in.
After the change, we are +61-7 on SMT LIB:
https://www.starexec.org/starexec/secure/details/job.jsp?id=30581
Allow partial models for multiple sygus enumerators (#2499)
Infrastructure for variable agnostic sygus enumerators (#2511)
Improve non-linear check model error handling (#2497)
Refactor strings equality rewriting (#2513)
This moves the extended rewrites for string equality to the main strings rewriter as a function rewriteEqualityExt, and makes this function called on every equality that is generated (from non-equalities) by our rewriter.
cmake: Fix dependencies for code generation. (#2524)
Fix wiki urls. (#2504)
cmake: Fix git version info (again). (#2523)
cmake: Fix theory order #2. (#2522)
Unify rewrites related to (str.contains x y) --> (= x y) (#2512)
cmake: Fix theory order. (#2518)
Make string rewriter unit tests more robust (#2520)
This commit changes the unit test for the string rewriter to use the
extended rewriter instead of the regular rewriter to make it more
robust, e.g. to different orderings in conjunctions.
cmake: Fix and simplify git version info. (#2516)
cmake: Add program prefix option. (#2515)
Fix generating debug/trace tags.
New C++ API: Add checks for Terms/OpTerms. (#2455)
Fix regress2. (#2502)
cmake: Add python3 option.
cmake: Enable -Wall.
cmake: Fix systemtests dependency.
cmake: Build fully static binaries with option --static.
cmake: Run make coverage in parallel by default.
cmake: Add more documentation, some fixes and cleanup.
cmake: configure.sh wrapper: Use explicit build directory structure.
We don't create build directories for every build type (and
configuration) anymore. The default build directory is now 'build'
(created where you call the wrapper script from). Option --name allows
to configure an individual name (and path) for the build directory.
cmake: configure wrapper: Modify next steps message after configuration.
Since configure.sh is only a wrapper for cmake it prints all the messages from
cmake. At the end we print the next steps after configuration. If configure.sh
is used we add the info to also change into the build directory before calling
make.
cmake: Move PACKAGE_NAME to ConfigureCVC4, more cleanup.
cmake: Refactor cvc4_add_unit_test macro to support test names with '/'.
Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
cmake: Guard GetGitRevisionDescription.
cmake: Add target runexamples.
cmake: Add support for cross-compiling for Windows.
cmake: Require JUnit version 4.
cmake: Do not allow dumping with portfolio build.
cmake: More documentation, clean up.
cmake: Move extracting git information to src/base cmake config file.
cmake: Guard examples that require Boost.
cmake: Disable unit tests if assertions are not enabled.
cmake: FindANTLR: Check if antlr3FileStreamNew is available.
cmake: configure.sh wrapper: Fixes for sh.
travis: Switch to cmake.
cmake: Do not build examples and unit and system tests by default.
cmake: configure.sh wrapper: Add --name option.
cmake: examples: Configure output directory per target.
cmake: Added java examples
cmake: configure.sh wrapper: Add --prefix for install directory.
cmake: Add some more documentation, cleanup.
cmake: Move helper functions to cmake/Helpers.cmake.
cmake: Added target examples (currently .cpp examples only)
cmake: Simplify build type configuration.
cmake: Refactor and clean up build profile printing.
cmake: Added target check
Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.
cmake: Add make install rule.
cmake: configure.sh wrapper: Fix handling of options with arguments.
cmake: Add module finder for Valgrind.
cmake: Various CMakeLists.txt fixes/cleanup.
cmake: Only build libcvc4 and libcvc4parser as libraries.
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.
cmake: Move find_package to where it is actually needed.
cmake: configure.sh wrapper: Removed env vars help text.
cmake: configure.sh wrapper: Configurable build directory
cmake: configure.sh wrapper: Create build dirs for configurations
cmake: configure.sh wrapper: done (except: configurable build dir)
cmake: Updated and prettified configuration printing.
cmake: configure.sh wrapper: option parsing
cmake: Add ENABLE_DEBUG_CONTEXT_MM to enable the debug context memory manager.
cmake: Add ENABLE_BEST to enable best configuration of dependencies.
cmake: Add Java runtime as required dependency (required for ANTLR).
cmake: Add convenience wrappers for tag generation.
cmake: Add library versioning for libcvc4.so.
cmake: Rebase with current master, add new tests/source files.
cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.
cmake: Use target specific includes for libcvc4.
Further, print definitions added with add_definitions(...).
cmake: Add missing dependency.
cmake: Add support for building static binaries/libraries.
cmake: Add options for specifying install directories for dependencies.
cmake: Add module finder for GLPK-cut-log.
cmake: Add module finder for ABC.
cmake: Compile Java tests and add to ctest if Java bindings are enabled.
cmake: Add SWIG support + Python and Java bindings.
cmake: Add dependencies for test targets and support for make coverage.
cmake: Various portfolio/default option fixes.
cmake: Enable parallel execution for test targets regress, units, systemtests.
cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.
cmake: Added system tests and target make systemtests.
cmake: Added regression tests and target make regress.
cmake: Add portfolio support.
cmake: Add ASAN support.
cmake: Enable shared by default.
Further, force shared builds in case of unit tests.
cmake: Disable W-suggest-override for unit tests.
cmake: Add target units.
cmake: Removed obsolete CMakeLists file in test.
cmake: Add support for CxxTest.
cmake: Filter through and disable unused HAVE_* variables from autotools.
cmake: Do not set global output directories for binaries and libraries.
cmake: Fix some includes.
cmake: Added support for coverage and profiling.
cmake: Added 3-valued option handling (to enable detection of user-set options).
cmake: Add module finder for readline.
cmake: Generate token headers.
cmake: Added licensing options and warnings/errors.
cmake: Cleanup CMakeLists.txt files, remove SHARED.
cmake: Add build configurations.
cmake: Fixed compiler flag macros.
cmake: Add module finder for LFSC.
cmake: Add module finder for CaDiCaL.
cmake: Add module finder for CryptoMiniSat.
cmake: Add module finder for SymFPU.
cmake: Add module finder for CLN.
cmake: Add libsignatures for proofs.
cmake: Remove unused CMakeLists.txt
cmake: Generate cvc4autoconfig.h (options currently statically set).
cmake: Added missing dependency for src/util
cmake: Working build infrastructure.
TODO: cvc4autoconfig.h
cmake: Antlr parser generation done.
cmake: Generate trace and debug tags
cmake: .cpp generation done, .h generation not yet complete
cmake: Added initial build infrastructure.
Decision strategy: incorporate arrays. (#2495)
Add rewrites for str.contains + str.replace/substr (#2496)
Decision strategy: incorporate separation logic. (#2494)
Add two rewrites for string contains character (#2492)
Refactor strings extended functions inferences (#2480)
This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type.
This is in preparation for working on solving equations and further inferences in this style.
New C++ API: Introduce new macro and exception for API checks. (#2486)
Fix issue with str.idof in evaluator (#2493)
Decision strategy: incorporate strings fmf. (#2485)
More aggressive caching of string skolems. (#2491)
Move and rename sygus solver classes (#2488)
fix assertion error (#2487)
Clean remaining references to getNextDecisionRequest in quantifiers. (#2484)
Improvements and fixes for symmetry detection and breaking (#2459)
This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.
Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)
Decision strategy: incorporate cegis unif (#2482)
Decision strategy: incorporate bounded integers (#2481)
Decision strategy: incorporate datatypes sygus solver. (#2479)
More aggressive skolem caching for strings, document and clean preprocessor (#2478)
Make strings model construction robust to lengths that are not propagated equal (#2444)
This fixes #2429.
This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment.
We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.
Regardless, the strings model construction should be robust to handle this case, which this PR does.
Follow redirects with cURL in contrib/get* scripts (#2471)
On systems without `wget`, we use `curl` to download dependencies.
However, we were not using the `-L` (follow redirects) option, which is
necessary to download certain dependencies, e.g. CryptoMiniSat.
Remove broken dumping support from portfolio build (#2470)
Dumping support for portfolio builds was introduced in
84f26af22566f7c10dea45b399b944cb50b5e317 but as far as I can tell, the
implementation has already been problematic in the original implementation. The
current implementation has the following issues:
- Dumping with a portfolio build (even when using the single threaded
executable) results in a segfault. The reason is that the DumpChannel variable
is declared as an `extern` and exists for the duration of the program. The
problem is that it stores a `CommandSequence`, which indirectly may store
nodes. When shutting down CVC4, the destructor of `DumpC` is called, which
destroys the `CommandSequence`, which results in a segfault because the
`NodeManager` does not exist anymore. The node manager is (indirectly) owned
and destroyed by the `api::Solver` object.
- Additionally, adding commands to the `CommandSequence` is not thread safe (it
just calls `CommandSequence::addCommand()`, which in turn pushes back to a
vector [0] (which is not thread safe [1]). A single instance of `DumpChannel`
is shared among all threads (it is not declared `thread_local` [2]).
- The `CommandSequence` in `DumpC` was not used in the original implementation
and is still unused on master. The original commit mentions that the portfolio
build stores the commands in the `CommandSequence` but not why.
This commit removes the `CommandSequence` and related methods from `DumpC` to
avoid the issue when destroying `DumpChannel`. It disables dumping for
portfolio builds and adds a check at configure-time that not both options have
been enabled simultaneously. Given that the option was not functional
previously, the problematic implementation, and the fact that the dump of
multiple threads wouldn't be very useful, disabling dumping for portfolio
builds is unlikely to be problem. An improvement that could be made is to
disable dumping support only for the pcvc4 binary and while enabling it for the
single-threaded version, even when using `--with-portfolio`. However, we
currently do not have the infrastructure for that (we use the same libcvc4
library for both binaries).
[0] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/command.cpp#L756
[1] https://en.cppreference.com/w/cpp/container
[2] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/dump.h#L117
Remove unnecessary tracing from preprocessing (#2472)
With the introduction of the PreprocessingPass class,
tracing/dumping/time keeping is done automatically in the base class,
eliminating the need for doing it manually. This commit cleans up
SmtEngine, removing tracing/dumping/time keeping in preprocessing that
is not needed anymore.
Decision strategy: incorporate UF with cardinality constraints (#2476)
Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462)
Refactor how assertions are added to decision engine (#2396)
Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.
Add Skolem cache for strings, refactor length registration (#2457)
This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor).
It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled.
Generalize CandidateRewriteDatabase to ExprMiner (#2340)
Fix #include for minisat headers in bvminisat. (#2463)
Uses information gain heuristic for building better solutions from DTs (#2451)
Simplify storing of transcendental function applications that occur in assertions (#2458)
Decision strategy: incorporate CEGQI (#2460)
New C++ API: Try to fix (false positive) Coverity warnings. (#2454)
Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461)
Initial infrastructure for theory decision manager (#2447)
Fix for when strings process loop is disabled. (#2456)
Fixe compiler warning in line_buffer.cpp. (#2453)
Support model cores via option --produce-model-cores. (#2407)
This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
Avoid calling size() every iteration (#2450)
Fix global negate (#2449)
fix (#2446)
Set NodeManager to nullptr when exporting vars (#2445)
PR #2409 assumed that temporarily setting the NodeManager to nullptr
when creating variables is not needed anymore. However, this made our
portfolio build fail. This commit reintroduces the temporary NodeManager
change while creating variables.
Using a single condition enumerator in sygus-unif (#2440)
This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).
In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:
- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.
A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.
There is also small improvements for trace messages.
Refactor non-clausal simplify preprocessing pass. (#2425)
Squash implementation of counterexample-guided instantiation (#2423)
Add (str.replace (str.replace y w y) y z) rewrite (#2441)
Replace boost::integer_traits with std::numeric_limits. (#2439)
Further, remove redundant gmp.h include in options_handler.cpp.
Remove clock_gettime() replacement for macOS. (#2436)
Not needed anymore since macOS 10.12 introduced clock_gettime().
Make isClosedEnumerable a member of TypeNode (#2434)
Further simplify and fix initialization of ce guided instantiation (#2437)
Refactor and document quantifiers variable elimination and conditional splitting (#2424)
Minor improvements to interface for rep set. (#2435)
More extended rewrites for strings equality (#2431)
Eliminate select over store in quantifier bodies (#2433)
Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)
Remove printing support for sygus enumeration types (#2430)
Finer-grained inference of substitutions in incremental mode (#2403)
Add regex grammar to rewriter verification tests (#2426)
Extended rewriter for string equalities (#2427)
Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)
Remove redundant strings rewrite. (#2422)
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since
re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )
This PR removes the above rewrite, which was implemented incorrectly and was dead code.
Update INSTALL instructions (#2420)
Fixes #2419. This commit adds more information about optional
dependencies, updates macOS-related information, and fixes some details.
Remove CVC3 compatibility layer (#2418)
Remove unused options file (#2413)
Minor improvements to theory model builder interface. (#2408)
Make quantifiers strategies exit immediately when in conflict (#2099)
Transfer ownership of learned literals from SMT engine to circuit propagator. (#2421)
Fix merge mishap of #2359.
Refactor ceg conjecture initialization (#2411)
Allows SAT checks of repair const to have different options (#2412)
Refactor and document alpha equivalence. (#2402)
Fix export of bound variables (#2409)
Refactor theory preprocess into preprocessing pass. (#2395)
Use useBland option in FCSimplexDecisionProcedure (#2405)
Add regular expression elimination module (#2400)
Refactor MipLibTrick preprocessing pass. (#2359)
Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)
fix bv total ops printing (#2365)
Split term canonize utility to own file and document (#2398)
Reorder …
adacore-bot
pushed a commit
to AdaCore/spark2014
that referenced
this issue
Apr 18, 2019
Project: cvc4 master 5321dfb1161032a79909a588ed05bb27d42ba579
MS114-013 Merging upstream cvc4 into our master
Change-Id: I1b9af6c730515e0be2156aa595fa62e678a086c7
Only check disequal terms with sygus-rr-verify (#2793)
ClausalBitvectorProof (#2786)
* [DRAT] ClausalBitvectorProof
Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)
It fits into the `BitvectorProof` class hierarchy like this:
```
BitvectorProof
/ \
/ \
ClausalBitvectorProof ResolutionBitvectorProof
```
This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
* CnfStream
* SatSolver (specifically the BvSatSolver)
* CnfProof
* TheoryProof
* TheoryBV
* Both bitblasters
And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.
This means that references to and interactions with (R)BVP were
pervasive.
Nevertheless, an SMT developer must persist.
The change summary:
* Create a subclass of BVP, called ClausalBitvectorProof, which has
most methods stubbed out.
* Make a some modifications to BVP and ResolutionBitvectorProof as the
natural division of labor between the different classes becomes
clear.
* Go through all the components in the first list and try to figure
out which kind of BVP they should **actually** be interacting with,
and how. Make tweaks accordingly.
* Add a hook from CryptoMinisat which pipes the produced DRAT proof
into the new ClausalBitvectorProof.
* Add a debug statement to ClausalBitvectorProof which parses and
prints that DRAT proof, for testing purposes.
Test:
* `make check` to verify that we didn't break any old stuff, including
lazy BB, and eager BB when using bvminisat.
* `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
-d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
1. It crashed with "Unimplemented"
2. Right before that it prints out the (textual) DRAT proof.
* Remove 2 unneeded methods
* Missed a rename
* Typos
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Andres comments
* Reorder members of TBitblaster
LFSC LRAT Output (#2787)
* LFSC ouput & unit test
* Renamed lrat unit test file
* s/DRAT/LRAT/
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
1. Extracted a filter whitespace function.
2. Added @param annotations.
* Addressing Yoni's comments
Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.
LratInstruction inheritance (#2784)
While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.
While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.
This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.
Fixed linking against drat2er, and use drat2er (#2785)
* Fixed linking against drat2er/drat-trim
We have machinery for linking against drat2er. However, this machinery
didn't quite work because libdrat2er.a contains an (undefined) reference
to `run_drat_trim` from libdrat-trim.a.
Thus, when linking against libdrat2er.a, we also need to link against
libdrat-trim.a.
I made this change, and then tested it by actually calling a function
from the drat2er library (CheckAndConvertToLRAT) which relies on
`run_drat_trim`. Since this invocation compiles, we know that the
linking is working properly now.
* Combined the two libs, per Mathias
* drat2er configured gaurds
New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)
New C++ API: Get rid of mkConst functions (simplify API). (#2783)
Do not rewrite 1-constructor sygus testers to true (#2780)
[BV Proofs] Option for proof format (#2777)
We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!
My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`
and that I could not provide random other option values.
Clause proof printing (#2779)
* Print LFSC proofs of CNF formulas
* Unit Test for clause printing
* Added SAT input proof printing unit test
* Fixed cnf_holds reference. Proofs of CMap_holds
There were references to clauses_hold, which should have been references
to cnf_holds.
Also added a function for printing a value of type CMap_holds, and a
test for this function.
LFSC drat output (#2776)
* 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
New C++ API: Add missing getType() calls to kick off type checking. (#2773)
[DRAT] DRAT data structure (#2767)
* 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
cmake: Disable unit tests for static builds. (#2775)
--static now implies --no-unit-testing.
Fixes #2672.
C++ API: Fix OOB read in unit test (#2774)
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. (#2737)
* [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
New C++ API: Add missing catch blocks for std::invalid_argument. (#2772)
API/Smt2 parser: refactor termAtomic (#2674)
C++ API: Reintroduce zero-value mkBitVector method (#2770)
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 (#2758)
* [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
New C++ API: Add tests for mk-functions in solver object. (#2764)
Clean up BV kinds and type rules. (#2766)
Add missing type rules for parameterized operator kinds. (#2766)
Fix issues with REWRITE_DONE in floating point rewriter (#2762)
Remove noop. (#2763)
Configured for linking against drat2er (#2754)
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.
New C++ API: Add tests for term object. (#2755)
DRAT Signature (#2757)
* 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
Revert "Move ss-combine rewrite to extended rewriter (#2703)" (#2759)
[LRA Proof] Storage for LRA proofs (#2747)
* [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.
Fixed typos.
New C++ API: Add tests for opterm object. (#2756)
Fix extended rewriter for binary associative operators. (#2751)
This was causing assertion failures when using Sets + Sygus.
Make single invocation and invariant pre/post condition templates 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.
New C++ API: Add tests for sort functions of solver object. (#2752)
Remove spurious map (#2750)
Fix compiler warnings. (#2748)
API: Add simple empty/sigma regexp unit tests (#2746)
[LRA proof] More complete LRA example proofs. (#2722)
* [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 (#2743)
* [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.
Remove alternate versions of mbqi (#2742)
LRAT signature (#2731)
* 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.
BoolToBV modes (off, ite, all) (#2530)
Strings: Make EXTF_d inference more conservative (#2740)
Arith Constraint Proof Loggin (#2732)
* Arith Constraint Proof Logging
Also a tiny documentation update.
* Debug.isOn check around iterated output
* reference iteratees
Enable BV proofs when using an eager bitblaster (#2733)
* 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
Fix use-after-free due to destruction order (#2739)
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.
Take into account minimality and types for cached PBE solutions (#2738)
Apply extended rewriting on PBE static symmetry breaking. (#2735)
Enable regular expression elimination by default. (#2736)
Seems to have no impact on Norn, and is helpful for a number of applications.
Skip non-cardinality types in sets min card inference (#2734)
Bit vector proof superclass (#2599)
* 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
Optimizations for PBE strings (#2728)
Infrastructure for sygus side conditions (#2729)
Combine sygus stream with PBE (#2726)
Improve interface for sygus grammar cons (#2727)
Information gain heuristic for PBE (#2719)
Optimize re-elim for re.allchar components (#2725)
Improve skolem caching by normalizing skolem args (#2723)
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.
Generalize sygus stream solution filtering to logical strength (#2697)
Improve cegqi engine trace. (#2714)
Make (T)NodeTrie a general utility (#2489)
This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.
Fix coverity warnings in datatypes (#2553)
This caches some information regarding tester applications and changes int -> size_t in a few places.
Lazy model construction in TheoryEngine (#2633)
Reduce lookahead when parsing string literals (#2721)
LRA proof signature fixes and a first proof for linear polynomials (#2713)
* 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.
Use https for antlr3.org downloads (#2701)
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.
Move ss-combine rewrite to extended rewriter (#2703)
We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.
Add rewrite for (str.substr s x y) --> "" (#2695)
This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.
Cache evaluations for PBE (#2699)
Quickly recognize when PBE conjectures are infeasible (#2718)
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.
Obvious rewrites to floating-point < and <=. (#2706)
Support string replace all (#2704)
Fix type enumerator for FP (#2717)
Fix real2int regression. (#2716)
Change lemma proof step storage & iterators (#2712)
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
Clausify context-dependent simplifications in ext theory (#2711)
Fix E-matching for case where candidate generator is not properly initialized (#2708)
Expand definitions prior to model core computation (#2707)
cmake: Require boost 1.50.0 for examples. (#2710)
cmake: Add option to explicitely enable/disable static binaries. (#2698)
Evaluator: add support for str.code (#2696)
Adding default SyGuS grammar construction for arrays (#2685)
Fix collectEmptyEqs in string rewriter (#2692)
Fix for itos reduction (#2691)
Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)
Change default sygus enumeration mode to auto (#2689)
Fix coverity warnings in sygus enumerator (#2687)
New C++ API: Split unit tests. (#2688)
Increasing coverage (#2683)
This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.
API: Fix assignment operators (#2680)
The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.
Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
configure.sh: Fix option parsing to match --help (#2611)
Allow partial models with optimized sygus enumeration (#2682)
Implement option to turn off symmetry breaking for basic enumerators (#2686)
Improves the existing implementation for sygus-active-gen=basic.
Refactor default grammars construction (#2681)
fixes to regression docs (#2679)
Add optimized sygus enumeration (#2677)
Record assumption info in AssertionPipeline (#2678)
Minor improvement to sygus trace (#2675)
CMake: Set RPATH on installed binary (#2671)
Currently, when installing CVC4 with a custom installation directory on
macOS, the resulting binary cannot be executed because the linker cannot
find the required libraries (e.g. our parser). This commit changes our
build system to use the `CMAKE_INSTALL_RPATH` variable to add the
installation directory to the RPATH list in the exectuable.
Do not use lazy trie for sygus-rr-verify (#2668)
Fail for SWIG 3.0.8 (#2656)
Ran into this bug when compiling with python3 bindings: https://github.com/swig/swig/issues/588
Instantiating any object crashes python. Since swig3.0.8 is currently the apt-get install for Ubuntu 16.04, I thought it'd be good to have a check for that. If python3 is preferred and the swig version is 3.0.8, it errors out and asks users to downgrade or upgrade SWIG.
CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)
Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.
[0] https://github.com/CVC4/CVC4/blob/7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36
Only build CryptoMiniSat library, no binary (#2657)
This commit changes the contrib/get-cryptominisat script to only build
the CryptoMiniSat library instead of both the library and the binary.
The advantage of this is that we can compile a static version of the
CryptoMiniSat library without having a static version of glibc or
libstdc++ (this is fine as long as we do a shared library build of
CVC4). This is an issue on Fedora (tested on version 25) where the
contrib/get-cryptominisat script was failing when building the
CryptoMiniSat binary due to the static version of these libraries not
being available. Since we just want to build the library, the commit
also changes the script to not install CryptoMiniSat anymore and updates
the CMake find script to accomodate the new folder structure. Side note:
the folder structure generated after this commit is a bit more uniform
with, e.g. the CaDiCaL script: The source files are directly in the
cryptominisat5 folder, not in a subfolder.
Recover from wrong use of get-info :reason-unknown (#2667)
Fixes #2584. Currently, we are immediately terminating CVC4 if the user
issues a `(get-info :reason-unknown)` command if it didn't succeed a
`(check-sat)` call returning `unknown`. This commit changes the behavior
to return an `(error ...)` but continue executing afterwards. It turns
the `ModalException` thrown in this case into a
`RecoverableModalException` and adds a check in
`GetInfoCommand::invoke()` to turn it into a
`CommandRecoverableFailure`, which solves the issue.
Remove antlr_undefines.h. (#2664)
Is not required anymore since we don't use autotools anymore.
Add substr, contains and equality rewrites (#2665)
Disable dumping test for non-dumping builds (#2662)
Travis: run examples and avoid building them twice (#2663)
`make check` builds the examples but does not run them. This commit
changes our Travis script to run the examples after building them and
removes `makeExamples()` to avoid building them twice.
BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. (#2647)
Simplifications based on the special const is now delegated down, only
the concat is pulled up.
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const. (#2647)
Sygus streaming non-implied predicates (#2660)
Remove autotools build system. (#2639)
Fix util::Random for macOS builds (#2655)
Add helper to detect length one string terms (#2654)
This commit introduces a helper function to detect string terms that
have exactly/at most length one. This is useful for a lot of rewrites
because strings of at most length one are guaranteed to not overlap
multiple components in a concatenation, which allows for more aggressive
rewriting.
This commit has been tested with --sygus-rr-synth-check for >1h on the
string term grammar.
Add OptionException handling during initialization (#2466)
The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:
1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes
This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor). Finally,
the commit adds a simple regression test for invalid dump tags.
cmake: Run regression level 2 for make check. (#2645)
Non-implied mode for model cores (#2653)
Non-contributing find replace rewrite (#2652)
Improve reduction for str.to.int (#2636)
Introducing internal commands for SyGuS commands (#2627)
Constant length regular expression elimination (#2646)
Skip sygus-rr-synth-check regressions when ASAN on (#2651)
This commit disables three regressions when using an ASAN build. The
regressions are all leaking memory when invoking the subsolver (see
issue #2649). Debugging the issue will take a while but is not very
critical since this feature is currently only used by CVC4 developers
but it prevents our nightly builds from going through.
Show if ASAN build in --show-config (#2650)
This commit extends `--show-config` to show whether the current build is
an ASAN build or not. This is done by moving a detection that was
previously done for the unit tests into base/configuration_private.h.
In addition to being convenient, this allows us to easily exclude
regression tests from ASAN builds.
Sygus query generator (#2465)
Fix context-dependent for positive contains reduction (#2644)
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643)
Match: `x_m | concat(y_my, 0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, ~0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)`
On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
| CVC4-base | CVC4-concatpullup-or |
BENCHMARK | SLVD SAT UNSAT TO MO CPU[s] | SLVD SAT UNSAT TO MO CPU[s] |
totals | 38992 13844 25148 1082 28 984887.4 | 39028 13845 25183 1046 28 974819.1 |
```
cmake: Add CxxTest include directory to unit test includes. (#2642)
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ones (#2596).
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 1 (#2596).
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
Improve strings reductions including skolem caching for contains (#2641)
Improve reduction for int.to.str (#2629)
Option for shuffling condition pool in CegisUnif (#2587)
cmake: Generate git_versioninfo.cpp on build time. (#2640)
Delay initialization of theory engine (#2621)
This implements solution number 2 for issue #2613.
Add more (str.replace x y z) rewrites (#2628)
Fix fp-bool.sy grammar and require symfpu (#2631)
Reset input language for ExprMiner subsolver (#2624)
Improvements to rewrite rules from inputs (#2625)
Add rewrites for str.replace in str.contains (#2623)
This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.
Fix heuristic for string length approximation (#2622)
Refactor printing of parameterized operators in smt2 (#2609)
Improve reasoning about empty strings in rewriter (#2615)
Fix partial operator elimination in sygus grammar normalization (#2620)
Fix string ext inference for rewrites that introduce negation (#2618)
Fix default setting of CegisUnif options (#2605)
cmake: Use gcovr instead lcov for coverage report generation. (#2617)
Fix compiler warnings (#2602)
Synthesize rewrite rules from inputs (#2608)
Fix cegis so that evaluation unfolding is not interleaved. (#2614)
Optimize regular expression elimination (#2612)
Add length-based rewrites for (str.substr _ _ _) (#2610)
Support for basic actively-generated enumerators (#2606)
Random: support URNG interface (#2595)
Use std::shuffle (with Random as the unified random generator) instead
of std::random_shuffle for deterministic, reproducable random shuffling.
Allow multiple synthesis conjectures. (#2593)
Fix compiler warnings. (#2601)
BV instantiator: Factor out util functions. (#2604)
Previously, all util functions for the BV instantiator were static functions
in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding
unit test, it was therefore required to include this cpp file in order to
test these functions. This factors out these functions into a
theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h).
Asan reported errors for the corresponing unit test because of this.
BV inverter: Factor out util functions. (#2603)
Previously, all invertibility condition functions were static functions
in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test,
it was therefore required to include this cpp file in order to test
these functions. This factors out these functions into a
theory/quantifiers/bv_inverter_utils.(cpp|h).
Fix string register extended terms (#2597)
A regress2 benchmark was failing, due to a recent change in our strings rewriter.
The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.
The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.
This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.
Cmake: Fix ctest call for example/translator. (#2600)
example/translator expects an input file to translate but none was provided in the ctest call.
This caused the ctest call to hang and wait for input on stdin in some configurations (in
particular in the nightlies).
Address slow sygus regressions (#2598)
Disable extended rewriter when applicable with var agnostic enumeration (#2594)
Fix unif trace (#2550)
Fix cache for sygus post-condition inference (#2592)
Update default options for sygus (#2586)
Fix rewrite rule filtering. (#2591)
New C++ API: Add checks for Sorts. (#2519)
Infrastructure for string length entailments via approximations (#2514)
Only use SKIP_RETURN_CODE with CMake 3.9.0+ (#2590)
With older versions of CMake, skipped tests are reported as failures,
which is undesirable. This commit changes the CMakeLists file to only
use the `SKIP_RETURN_CODE` property if a newer version of CMake is used.
Fix end constraint for regexp elimination (#2571)
Clean remaining references to getNextDecisionRequest and simplify (#2500)
Fix mem leak in sha1_collision example. (#2588)
Fix mem leak in sets_translate example. (#2589)
Simplify datatypes printing (#2573)
Fix compiler warnings. (#2585)
Fix regress (#2575)
Add actively generated sygus enumerators (#2552)
Make CegisUnif with condition independent robust to var agnostic (#2565)
Fix stale op list in sets (#2572)
Eliminate partial operators within lambdas during grammar normalization (#2570)
cmake: Display skipped tests as not run (#2567)
Currently, the run_regression.py script just returns 0 when we skip a
test due to a feature not supported by the current configuration.
Returning 0 marks those tests as passed. To make it more clear which
tests were skipped, this commit adds the `SKIP_RETURN_CODE` [0] property
to the regression tests and changes the regression script to return 77
for skipped tests. The feature is supported since at least CMake 3.0 [0].
For backwards compatibility with autotools, returning 77 for skipped
tests is only active when `--cmake` is passed to the run_regression.py
script.
[0] https://cmake.org/cmake/help/v3.0/prop_test/SKIP_RETURN_CODE.html
Allow (_ to_fp ...) in strict parsing mode (#2566)
When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
unit: Fix ASAN detection for GCC. (#2561)
Make registration of preprocessing passes explicit (#2564)
As it turns out, self-registering types are problematic with static
linkage [0]. Instead of fixing the issue with linker flags, which seems
possible but also brittle (e.g. the flags may be different for different
linkers), this commit adds an explicit registration of each
preprocessing pass.
[0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html
Fix documentation for `make regress`. (#2557)
cmake: Add examples to build-tests, add warning for disabling static build. (#2562)
Fix "catching polymorphic type by value" warnings (#2556)
When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make
sure that we use a reference type for the exception, otherwise the unit
test tries to catch the exception by value, resulting in "catching
polymorphic type by value" warnings.
cmake: Generate compile_commands.json on configure. (#2559)
cmake: Add build target build-tests to build all test dependencies. (#2558)
init scalar class members (coverity issues 1473720 and 1473721) (#2554)
Fix compiler warnings. (#2555)
Fix dumping pre/post preprocessing passes (#2469)
This commit changes the hard-coded list of checks for
preprocessing-related dump tags to take advantage of the new
preprocessing pass registration mechanism from PR #2468. It also fixes a
typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()`
and adds a list of available passes to the `--dump help` output.
Refactor preprocessing pass registration (#2468)
This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.
As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.
This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.
[0] https://llvm.org/docs/WritingAnLLVMPass.html
Add rewrite for solving stoi (#2532)
cmake: Ignore ctest exit code for coverage reports.
Stream concrete values for variable agnostic enumerators (#2526)
Rewrites for (= "" _) and (= (str.replace _) _) (#2546)
cmake: Only do Java tests when unit testing on (#2551)
Right now, we are adding the Java tests even when we are not building
unit tests. This commit changes the build system to only add the Java
tests when unit tests are enabled. There are two reasons for this
change:
- building a production version of CVC4 should not require JUnit
- it seems more intuitive (to me at least) to disable JUnit tests when
unit tests are disabled
This change also simplifies building the Java bindings in our homebrew
formula.
cmake: Add CxxTest finder module to allow custom paths. (#2542)
Remove assertion. (#2549)
Infrastructure for using active enumerators in sygus modules (#2547)
Incorporate all unification enumerators into getTermList. (#2541)
Fix Taylor overapproximation for large exponentials (#2538)
Fix homogeneous string constant rewrite (#2545)
Fix bug in getSymbols. (#2544)
cmake: Only print dumping warning if not disabled by user. (#2543)
Makes SyGuS parsing more robust in invariant problems (#2509)
cmake: Fix test target dependency issues. (#2540)
Enable quantified array regression. (#2539)
Symmetry breaking for variable agnostic enumerators (#2527)
cmake: New INSTALL.md for build and testing instructions. (#2536)
cmake: Exclude examples for coverage target. (#2535)
Eagerly ensure literal on active guards for sygus enumerators (#2531)
cmake: Add check for GCC 4.5.1 and warn user. (#2533)
examples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534)
cmake: configure.sh wrapper: Removed unused option --gmp.
carefully printing trusted assertions in proofs (#2505)
cmake: Fix tag code generation dependencies. (#2529)
Fix warnings uncovered by cmake build (#2521)
Fix quantifiers selector over store rewrite (#2510)
Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in.
After the change, we are +61-7 on SMT LIB:
https://www.starexec.org/starexec/secure/details/job.jsp?id=30581
Allow partial models for multiple sygus enumerators (#2499)
Infrastructure for variable agnostic sygus enumerators (#2511)
Improve non-linear check model error handling (#2497)
Refactor strings equality rewriting (#2513)
This moves the extended rewrites for string equality to the main strings rewriter as a function rewriteEqualityExt, and makes this function called on every equality that is generated (from non-equalities) by our rewriter.
cmake: Fix dependencies for code generation. (#2524)
Fix wiki urls. (#2504)
cmake: Fix git version info (again). (#2523)
cmake: Fix theory order #2. (#2522)
Unify rewrites related to (str.contains x y) --> (= x y) (#2512)
cmake: Fix theory order. (#2518)
Make string rewriter unit tests more robust (#2520)
This commit changes the unit test for the string rewriter to use the
extended rewriter instead of the regular rewriter to make it more
robust, e.g. to different orderings in conjunctions.
cmake: Fix and simplify git version info. (#2516)
cmake: Add program prefix option. (#2515)
Fix generating debug/trace tags.
New C++ API: Add checks for Terms/OpTerms. (#2455)
Fix regress2. (#2502)
cmake: Add python3 option.
cmake: Enable -Wall.
cmake: Fix systemtests dependency.
cmake: Build fully static binaries with option --static.
cmake: Run make coverage in parallel by default.
cmake: Add more documentation, some fixes and cleanup.
cmake: configure.sh wrapper: Use explicit build directory structure.
We don't create build directories for every build type (and
configuration) anymore. The default build directory is now 'build'
(created where you call the wrapper script from). Option --name allows
to configure an individual name (and path) for the build directory.
cmake: configure wrapper: Modify next steps message after configuration.
Since configure.sh is only a wrapper for cmake it prints all the messages from
cmake. At the end we print the next steps after configuration. If configure.sh
is used we add the info to also change into the build directory before calling
make.
cmake: Move PACKAGE_NAME to ConfigureCVC4, more cleanup.
cmake: Refactor cvc4_add_unit_test macro to support test names with '/'.
Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
cmake: Guard GetGitRevisionDescription.
cmake: Add target runexamples.
cmake: Add support for cross-compiling for Windows.
cmake: Require JUnit version 4.
cmake: Do not allow dumping with portfolio build.
cmake: More documentation, clean up.
cmake: Move extracting git information to src/base cmake config file.
cmake: Guard examples that require Boost.
cmake: Disable unit tests if assertions are not enabled.
cmake: FindANTLR: Check if antlr3FileStreamNew is available.
cmake: configure.sh wrapper: Fixes for sh.
travis: Switch to cmake.
cmake: Do not build examples and unit and system tests by default.
cmake: configure.sh wrapper: Add --name option.
cmake: examples: Configure output directory per target.
cmake: Added java examples
cmake: configure.sh wrapper: Add --prefix for install directory.
cmake: Add some more documentation, cleanup.
cmake: Move helper functions to cmake/Helpers.cmake.
cmake: Added target examples (currently .cpp examples only)
cmake: Simplify build type configuration.
cmake: Refactor and clean up build profile printing.
cmake: Added target check
Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.
cmake: Add make install rule.
cmake: configure.sh wrapper: Fix handling of options with arguments.
cmake: Add module finder for Valgrind.
cmake: Various CMakeLists.txt fixes/cleanup.
cmake: Only build libcvc4 and libcvc4parser as libraries.
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.
cmake: Move find_package to where it is actually needed.
cmake: configure.sh wrapper: Removed env vars help text.
cmake: configure.sh wrapper: Configurable build directory
cmake: configure.sh wrapper: Create build dirs for configurations
cmake: configure.sh wrapper: done (except: configurable build dir)
cmake: Updated and prettified configuration printing.
cmake: configure.sh wrapper: option parsing
cmake: Add ENABLE_DEBUG_CONTEXT_MM to enable the debug context memory manager.
cmake: Add ENABLE_BEST to enable best configuration of dependencies.
cmake: Add Java runtime as required dependency (required for ANTLR).
cmake: Add convenience wrappers for tag generation.
cmake: Add library versioning for libcvc4.so.
cmake: Rebase with current master, add new tests/source files.
cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.
cmake: Use target specific includes for libcvc4.
Further, print definitions added with add_definitions(...).
cmake: Add missing dependency.
cmake: Add support for building static binaries/libraries.
cmake: Add options for specifying install directories for dependencies.
cmake: Add module finder for GLPK-cut-log.
cmake: Add module finder for ABC.
cmake: Compile Java tests and add to ctest if Java bindings are enabled.
cmake: Add SWIG support + Python and Java bindings.
cmake: Add dependencies for test targets and support for make coverage.
cmake: Various portfolio/default option fixes.
cmake: Enable parallel execution for test targets regress, units, systemtests.
cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.
cmake: Added system tests and target make systemtests.
cmake: Added regression tests and target make regress.
cmake: Add portfolio support.
cmake: Add ASAN support.
cmake: Enable shared by default.
Further, force shared builds in case of unit tests.
cmake: Disable W-suggest-override for unit tests.
cmake: Add target units.
cmake: Removed obsolete CMakeLists file in test.
cmake: Add support for CxxTest.
cmake: Filter through and disable unused HAVE_* variables from autotools.
cmake: Do not set global output directories for binaries and libraries.
cmake: Fix some includes.
cmake: Added support for coverage and profiling.
cmake: Added 3-valued option handling (to enable detection of user-set options).
cmake: Add module finder for readline.
cmake: Generate token headers.
cmake: Added licensing options and warnings/errors.
cmake: Cleanup CMakeLists.txt files, remove SHARED.
cmake: Add build configurations.
cmake: Fixed compiler flag macros.
cmake: Add module finder for LFSC.
cmake: Add module finder for CaDiCaL.
cmake: Add module finder for CryptoMiniSat.
cmake: Add module finder for SymFPU.
cmake: Add module finder for CLN.
cmake: Add libsignatures for proofs.
cmake: Remove unused CMakeLists.txt
cmake: Generate cvc4autoconfig.h (options currently statically set).
cmake: Added missing dependency for src/util
cmake: Working build infrastructure.
TODO: cvc4autoconfig.h
cmake: Antlr parser generation done.
cmake: Generate trace and debug tags
cmake: .cpp generation done, .h generation not yet complete
cmake: Added initial build infrastructure.
Decision strategy: incorporate arrays. (#2495)
Add rewrites for str.contains + str.replace/substr (#2496)
Decision strategy: incorporate separation logic. (#2494)
Add two rewrites for string contains character (#2492)
Refactor strings extended functions inferences (#2480)
This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type.
This is in preparation for working on solving equations and further inferences in this style.
New C++ API: Introduce new macro and exception for API checks. (#2486)
Fix issue with str.idof in evaluator (#2493)
Decision strategy: incorporate strings fmf. (#2485)
More aggressive caching of string skolems. (#2491)
Move and rename sygus solver classes (#2488)
fix assertion error (#2487)
Clean remaining references to getNextDecisionRequest in quantifiers. (#2484)
Improvements and fixes for symmetry detection and breaking (#2459)
This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.
Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)
Decision strategy: incorporate cegis unif (#2482)
Decision strategy: incorporate bounded integers (#2481)
Decision strategy: incorporate datatypes sygus solver. (#2479)
More aggressive skolem caching for strings, document and clean preprocessor (#2478)
Make strings model construction robust to lengths that are not propagated equal (#2444)
This fixes #2429.
This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment.
We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.
Regardless, the strings model construction should be robust to handle this case, which this PR does.
Follow redirects with cURL in contrib/get* scripts (#2471)
On systems without `wget`, we use `curl` to download dependencies.
However, we were not using the `-L` (follow redirects) option, which is
necessary to download certain dependencies, e.g. CryptoMiniSat.
Remove broken dumping support from portfolio build (#2470)
Dumping support for portfolio builds was introduced in
84f26af22566f7c10dea45b399b944cb50b5e317 but as far as I can tell, the
implementation has already been problematic in the original implementation. The
current implementation has the following issues:
- Dumping with a portfolio build (even when using the single threaded
executable) results in a segfault. The reason is that the DumpChannel variable
is declared as an `extern` and exists for the duration of the program. The
problem is that it stores a `CommandSequence`, which indirectly may store
nodes. When shutting down CVC4, the destructor of `DumpC` is called, which
destroys the `CommandSequence`, which results in a segfault because the
`NodeManager` does not exist anymore. The node manager is (indirectly) owned
and destroyed by the `api::Solver` object.
- Additionally, adding commands to the `CommandSequence` is not thread safe (it
just calls `CommandSequence::addCommand()`, which in turn pushes back to a
vector [0] (which is not thread safe [1]). A single instance of `DumpChannel`
is shared among all threads (it is not declared `thread_local` [2]).
- The `CommandSequence` in `DumpC` was not used in the original implementation
and is still unused on master. The original commit mentions that the portfolio
build stores the commands in the `CommandSequence` but not why.
This commit removes the `CommandSequence` and related methods from `DumpC` to
avoid the issue when destroying `DumpChannel`. It disables dumping for
portfolio builds and adds a check at configure-time that not both options have
been enabled simultaneously. Given that the option was not functional
previously, the problematic implementation, and the fact that the dump of
multiple threads wouldn't be very useful, disabling dumping for portfolio
builds is unlikely to be problem. An improvement that could be made is to
disable dumping support only for the pcvc4 binary and while enabling it for the
single-threaded version, even when using `--with-portfolio`. However, we
currently do not have the infrastructure for that (we use the same libcvc4
library for both binaries).
[0] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/command.cpp#L756
[1] https://en.cppreference.com/w/cpp/container
[2] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/dump.h#L117
Remove unnecessary tracing from preprocessing (#2472)
With the introduction of the PreprocessingPass class,
tracing/dumping/time keeping is done automatically in the base class,
eliminating the need for doing it manually. This commit cleans up
SmtEngine, removing tracing/dumping/time keeping in preprocessing that
is not needed anymore.
Decision strategy: incorporate UF with cardinality constraints (#2476)
Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462)
Refactor how assertions are added to decision engine (#2396)
Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.
Add Skolem cache for strings, refactor length registration (#2457)
This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor).
It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled.
Generalize CandidateRewriteDatabase to ExprMiner (#2340)
Fix #include for minisat headers in bvminisat. (#2463)
Uses information gain heuristic for building better solutions from DTs (#2451)
Simplify storing of transcendental function applications that occur in assertions (#2458)
Decision strategy: incorporate CEGQI (#2460)
New C++ API: Try to fix (false positive) Coverity warnings. (#2454)
Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461)
Initial infrastructure for theory decision manager (#2447)
Fix for when strings process loop is disabled. (#2456)
Fixe compiler warning in line_buffer.cpp. (#2453)
Support model cores via option --produce-model-cores. (#2407)
This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
Avoid calling size() every iteration (#2450)
Fix global negate (#2449)
fix (#2446)
Set NodeManager to nullptr when exporting vars (#2445)
PR #2409 assumed that temporarily setting the NodeManager to nullptr
when creating variables is not needed anymore. However, this made our
portfolio build fail. This commit reintroduces the temporary NodeManager
change while creating variables.
Using a single condition enumerator in sygus-unif (#2440)
This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).
In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:
- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.
A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.
There is also small improvements for trace messages.
Refactor non-clausal simplify preprocessing pass. (#2425)
Squash implementation of counterexample-guided instantiation (#2423)
Add (str.replace (str.replace y w y) y z) rewrite (#2441)
Replace boost::integer_traits with std::numeric_limits. (#2439)
Further, remove redundant gmp.h include in options_handler.cpp.
Remove clock_gettime() replacement for macOS. (#2436)
Not needed anymore since macOS 10.12 introduced clock_gettime().
Make isClosedEnumerable a member of TypeNode (#2434)
Further simplify and fix initialization of ce guided instantiation (#2437)
Refactor and document quantifiers variable elimination and conditional splitting (#2424)
Minor improvements to interface for rep set. (#2435)
More extended rewrites for strings equality (#2431)
Eliminate select over store in quantifier bodies (#2433)
Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)
Remove printing support for sygus enumeration types (#2430)
Finer-grained inference of substitutions in incremental mode (#2403)
Add regex grammar to rewriter verification tests (#2426)
Extended rewriter for string equalities (#2427)
Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)
Remove redundant strings rewrite. (#2422)
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since
re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )
This PR removes the above rewrite, which was implemented incorrectly and was dead code.
Update INSTALL instructions (#2420)
Fixes #2419. This commit adds more information about optional
dependencies, updates macOS-related information, and fixes some details.
Remove CVC3 compatibility layer (#2418)
Remove unused options file (#2413)
Minor improvements to theory model builder interface. (#2408)
Make quantifiers strategies exit immediately when in conflict (#2099)
Transfer ownership of learned literals from SMT engine to circuit propagator. (#2421)
Fix merge mishap of #2359.
Refactor ceg conjecture initialization (#2411)
Allows SAT checks of repair const to have different options (#2412)
Refactor and document alpha equivalence. (#2402)
Fix export of bound variables (#2409)
Refactor theory preprocess into preprocessing pass. (#2395)
Use useBland option in FCSimplexDecisionProcedure (#2405)
Add regular expression elimination module (#2400)
Refactor MipLibTrick preprocessing pass. (#2359)
Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)
fix bv total ops printing (#2365)
Split term canonize utility to own file and document (#2398)
Reorder …
adacore-bot
pushed a commit
to AdaCore/spark2014
that referenced
this issue
Apr 18, 2019
Project: cvc4 master 5321dfb1161032a79909a588ed05bb27d42ba579
MS114-013 Merging upstream cvc4 into our master
Change-Id: I1b9af6c730515e0be2156aa595fa62e678a086c7
Only check disequal terms with sygus-rr-verify (#2793)
ClausalBitvectorProof (#2786)
* [DRAT] ClausalBitvectorProof
Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)
It fits into the `BitvectorProof` class hierarchy like this:
```
BitvectorProof
/ \
/ \
ClausalBitvectorProof ResolutionBitvectorProof
```
This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
* CnfStream
* SatSolver (specifically the BvSatSolver)
* CnfProof
* TheoryProof
* TheoryBV
* Both bitblasters
And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.
This means that references to and interactions with (R)BVP were
pervasive.
Nevertheless, an SMT developer must persist.
The change summary:
* Create a subclass of BVP, called ClausalBitvectorProof, which has
most methods stubbed out.
* Make a some modifications to BVP and ResolutionBitvectorProof as the
natural division of labor between the different classes becomes
clear.
* Go through all the components in the first list and try to figure
out which kind of BVP they should **actually** be interacting with,
and how. Make tweaks accordingly.
* Add a hook from CryptoMinisat which pipes the produced DRAT proof
into the new ClausalBitvectorProof.
* Add a debug statement to ClausalBitvectorProof which parses and
prints that DRAT proof, for testing purposes.
Test:
* `make check` to verify that we didn't break any old stuff, including
lazy BB, and eager BB when using bvminisat.
* `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
-d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
1. It crashed with "Unimplemented"
2. Right before that it prints out the (textual) DRAT proof.
* Remove 2 unneeded methods
* Missed a rename
* Typos
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Andres comments
* Reorder members of TBitblaster
LFSC LRAT Output (#2787)
* LFSC ouput & unit test
* Renamed lrat unit test file
* s/DRAT/LRAT/
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
1. Extracted a filter whitespace function.
2. Added @param annotations.
* Addressing Yoni's comments
Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.
LratInstruction inheritance (#2784)
While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.
While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.
This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.
Fixed linking against drat2er, and use drat2er (#2785)
* Fixed linking against drat2er/drat-trim
We have machinery for linking against drat2er. However, this machinery
didn't quite work because libdrat2er.a contains an (undefined) reference
to `run_drat_trim` from libdrat-trim.a.
Thus, when linking against libdrat2er.a, we also need to link against
libdrat-trim.a.
I made this change, and then tested it by actually calling a function
from the drat2er library (CheckAndConvertToLRAT) which relies on
`run_drat_trim`. Since this invocation compiles, we know that the
linking is working properly now.
* Combined the two libs, per Mathias
* drat2er configured gaurds
New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)
New C++ API: Get rid of mkConst functions (simplify API). (#2783)
Do not rewrite 1-constructor sygus testers to true (#2780)
[BV Proofs] Option for proof format (#2777)
We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!
My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`
and that I could not provide random other option values.
Clause proof printing (#2779)
* Print LFSC proofs of CNF formulas
* Unit Test for clause printing
* Added SAT input proof printing unit test
* Fixed cnf_holds reference. Proofs of CMap_holds
There were references to clauses_hold, which should have been references
to cnf_holds.
Also added a function for printing a value of type CMap_holds, and a
test for this function.
LFSC drat output (#2776)
* 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
New C++ API: Add missing getType() calls to kick off type checking. (#2773)
[DRAT] DRAT data structure (#2767)
* 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
cmake: Disable unit tests for static builds. (#2775)
--static now implies --no-unit-testing.
Fixes #2672.
C++ API: Fix OOB read in unit test (#2774)
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. (#2737)
* [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
New C++ API: Add missing catch blocks for std::invalid_argument. (#2772)
API/Smt2 parser: refactor termAtomic (#2674)
C++ API: Reintroduce zero-value mkBitVector method (#2770)
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 (#2758)
* [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
New C++ API: Add tests for mk-functions in solver object. (#2764)
Clean up BV kinds and type rules. (#2766)
Add missing type rules for parameterized operator kinds. (#2766)
Fix issues with REWRITE_DONE in floating point rewriter (#2762)
Remove noop. (#2763)
Configured for linking against drat2er (#2754)
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.
New C++ API: Add tests for term object. (#2755)
DRAT Signature (#2757)
* 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
Revert "Move ss-combine rewrite to extended rewriter (#2703)" (#2759)
[LRA Proof] Storage for LRA proofs (#2747)
* [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.
Fixed typos.
New C++ API: Add tests for opterm object. (#2756)
Fix extended rewriter for binary associative operators. (#2751)
This was causing assertion failures when using Sets + Sygus.
Make single invocation and invariant pre/post condition templates 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.
New C++ API: Add tests for sort functions of solver object. (#2752)
Remove spurious map (#2750)
Fix compiler warnings. (#2748)
API: Add simple empty/sigma regexp unit tests (#2746)
[LRA proof] More complete LRA example proofs. (#2722)
* [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 (#2743)
* [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.
Remove alternate versions of mbqi (#2742)
LRAT signature (#2731)
* 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.
BoolToBV modes (off, ite, all) (#2530)
Strings: Make EXTF_d inference more conservative (#2740)
Arith Constraint Proof Loggin (#2732)
* Arith Constraint Proof Logging
Also a tiny documentation update.
* Debug.isOn check around iterated output
* reference iteratees
Enable BV proofs when using an eager bitblaster (#2733)
* 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
Fix use-after-free due to destruction order (#2739)
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.
Take into account minimality and types for cached PBE solutions (#2738)
Apply extended rewriting on PBE static symmetry breaking. (#2735)
Enable regular expression elimination by default. (#2736)
Seems to have no impact on Norn, and is helpful for a number of applications.
Skip non-cardinality types in sets min card inference (#2734)
Bit vector proof superclass (#2599)
* 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
Optimizations for PBE strings (#2728)
Infrastructure for sygus side conditions (#2729)
Combine sygus stream with PBE (#2726)
Improve interface for sygus grammar cons (#2727)
Information gain heuristic for PBE (#2719)
Optimize re-elim for re.allchar components (#2725)
Improve skolem caching by normalizing skolem args (#2723)
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.
Generalize sygus stream solution filtering to logical strength (#2697)
Improve cegqi engine trace. (#2714)
Make (T)NodeTrie a general utility (#2489)
This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.
Fix coverity warnings in datatypes (#2553)
This caches some information regarding tester applications and changes int -> size_t in a few places.
Lazy model construction in TheoryEngine (#2633)
Reduce lookahead when parsing string literals (#2721)
LRA proof signature fixes and a first proof for linear polynomials (#2713)
* 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.
Use https for antlr3.org downloads (#2701)
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.
Move ss-combine rewrite to extended rewriter (#2703)
We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.
Add rewrite for (str.substr s x y) --> "" (#2695)
This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.
Cache evaluations for PBE (#2699)
Quickly recognize when PBE conjectures are infeasible (#2718)
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.
Obvious rewrites to floating-point < and <=. (#2706)
Support string replace all (#2704)
Fix type enumerator for FP (#2717)
Fix real2int regression. (#2716)
Change lemma proof step storage & iterators (#2712)
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
Clausify context-dependent simplifications in ext theory (#2711)
Fix E-matching for case where candidate generator is not properly initialized (#2708)
Expand definitions prior to model core computation (#2707)
cmake: Require boost 1.50.0 for examples. (#2710)
cmake: Add option to explicitely enable/disable static binaries. (#2698)
Evaluator: add support for str.code (#2696)
Adding default SyGuS grammar construction for arrays (#2685)
Fix collectEmptyEqs in string rewriter (#2692)
Fix for itos reduction (#2691)
Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)
Change default sygus enumeration mode to auto (#2689)
Fix coverity warnings in sygus enumerator (#2687)
New C++ API: Split unit tests. (#2688)
Increasing coverage (#2683)
This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.
API: Fix assignment operators (#2680)
The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.
Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
configure.sh: Fix option parsing to match --help (#2611)
Allow partial models with optimized sygus enumeration (#2682)
Implement option to turn off symmetry breaking for basic enumerators (#2686)
Improves the existing implementation for sygus-active-gen=basic.
Refactor default grammars construction (#2681)
fixes to regression docs (#2679)
Add optimized sygus enumeration (#2677)
Record assumption info in AssertionPipeline (#2678)
Minor improvement to sygus trace (#2675)
CMake: Set RPATH on installed binary (#2671)
Currently, when installing CVC4 with a custom installation directory on
macOS, the resulting binary cannot be executed because the linker cannot
find the required libraries (e.g. our parser). This commit changes our
build system to use the `CMAKE_INSTALL_RPATH` variable to add the
installation directory to the RPATH list in the exectuable.
Do not use lazy trie for sygus-rr-verify (#2668)
Fail for SWIG 3.0.8 (#2656)
Ran into this bug when compiling with python3 bindings: https://github.com/swig/swig/issues/588
Instantiating any object crashes python. Since swig3.0.8 is currently the apt-get install for Ubuntu 16.04, I thought it'd be good to have a check for that. If python3 is preferred and the swig version is 3.0.8, it errors out and asks users to downgrade or upgrade SWIG.
CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)
Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.
[0] https://github.com/CVC4/CVC4/blob/7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36
Only build CryptoMiniSat library, no binary (#2657)
This commit changes the contrib/get-cryptominisat script to only build
the CryptoMiniSat library instead of both the library and the binary.
The advantage of this is that we can compile a static version of the
CryptoMiniSat library without having a static version of glibc or
libstdc++ (this is fine as long as we do a shared library build of
CVC4). This is an issue on Fedora (tested on version 25) where the
contrib/get-cryptominisat script was failing when building the
CryptoMiniSat binary due to the static version of these libraries not
being available. Since we just want to build the library, the commit
also changes the script to not install CryptoMiniSat anymore and updates
the CMake find script to accomodate the new folder structure. Side note:
the folder structure generated after this commit is a bit more uniform
with, e.g. the CaDiCaL script: The source files are directly in the
cryptominisat5 folder, not in a subfolder.
Recover from wrong use of get-info :reason-unknown (#2667)
Fixes #2584. Currently, we are immediately terminating CVC4 if the user
issues a `(get-info :reason-unknown)` command if it didn't succeed a
`(check-sat)` call returning `unknown`. This commit changes the behavior
to return an `(error ...)` but continue executing afterwards. It turns
the `ModalException` thrown in this case into a
`RecoverableModalException` and adds a check in
`GetInfoCommand::invoke()` to turn it into a
`CommandRecoverableFailure`, which solves the issue.
Remove antlr_undefines.h. (#2664)
Is not required anymore since we don't use autotools anymore.
Add substr, contains and equality rewrites (#2665)
Disable dumping test for non-dumping builds (#2662)
Travis: run examples and avoid building them twice (#2663)
`make check` builds the examples but does not run them. This commit
changes our Travis script to run the examples after building them and
removes `makeExamples()` to avoid building them twice.
BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. (#2647)
Simplifications based on the special const is now delegated down, only
the concat is pulled up.
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const. (#2647)
Sygus streaming non-implied predicates (#2660)
Remove autotools build system. (#2639)
Fix util::Random for macOS builds (#2655)
Add helper to detect length one string terms (#2654)
This commit introduces a helper function to detect string terms that
have exactly/at most length one. This is useful for a lot of rewrites
because strings of at most length one are guaranteed to not overlap
multiple components in a concatenation, which allows for more aggressive
rewriting.
This commit has been tested with --sygus-rr-synth-check for >1h on the
string term grammar.
Add OptionException handling during initialization (#2466)
The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:
1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes
This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor). Finally,
the commit adds a simple regression test for invalid dump tags.
cmake: Run regression level 2 for make check. (#2645)
Non-implied mode for model cores (#2653)
Non-contributing find replace rewrite (#2652)
Improve reduction for str.to.int (#2636)
Introducing internal commands for SyGuS commands (#2627)
Constant length regular expression elimination (#2646)
Skip sygus-rr-synth-check regressions when ASAN on (#2651)
This commit disables three regressions when using an ASAN build. The
regressions are all leaking memory when invoking the subsolver (see
issue #2649). Debugging the issue will take a while but is not very
critical since this feature is currently only used by CVC4 developers
but it prevents our nightly builds from going through.
Show if ASAN build in --show-config (#2650)
This commit extends `--show-config` to show whether the current build is
an ASAN build or not. This is done by moving a detection that was
previously done for the unit tests into base/configuration_private.h.
In addition to being convenient, this allows us to easily exclude
regression tests from ASAN builds.
Sygus query generator (#2465)
Fix context-dependent for positive contains reduction (#2644)
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643)
Match: `x_m | concat(y_my, 0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, ~0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)`
On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
| CVC4-base | CVC4-concatpullup-or |
BENCHMARK | SLVD SAT UNSAT TO MO CPU[s] | SLVD SAT UNSAT TO MO CPU[s] |
totals | 38992 13844 25148 1082 28 984887.4 | 39028 13845 25183 1046 28 974819.1 |
```
cmake: Add CxxTest include directory to unit test includes. (#2642)
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ones (#2596).
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 1 (#2596).
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
Improve strings reductions including skolem caching for contains (#2641)
Improve reduction for int.to.str (#2629)
Option for shuffling condition pool in CegisUnif (#2587)
cmake: Generate git_versioninfo.cpp on build time. (#2640)
Delay initialization of theory engine (#2621)
This implements solution number 2 for issue #2613.
Add more (str.replace x y z) rewrites (#2628)
Fix fp-bool.sy grammar and require symfpu (#2631)
Reset input language for ExprMiner subsolver (#2624)
Improvements to rewrite rules from inputs (#2625)
Add rewrites for str.replace in str.contains (#2623)
This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.
Fix heuristic for string length approximation (#2622)
Refactor printing of parameterized operators in smt2 (#2609)
Improve reasoning about empty strings in rewriter (#2615)
Fix partial operator elimination in sygus grammar normalization (#2620)
Fix string ext inference for rewrites that introduce negation (#2618)
Fix default setting of CegisUnif options (#2605)
cmake: Use gcovr instead lcov for coverage report generation. (#2617)
Fix compiler warnings (#2602)
Synthesize rewrite rules from inputs (#2608)
Fix cegis so that evaluation unfolding is not interleaved. (#2614)
Optimize regular expression elimination (#2612)
Add length-based rewrites for (str.substr _ _ _) (#2610)
Support for basic actively-generated enumerators (#2606)
Random: support URNG interface (#2595)
Use std::shuffle (with Random as the unified random generator) instead
of std::random_shuffle for deterministic, reproducable random shuffling.
Allow multiple synthesis conjectures. (#2593)
Fix compiler warnings. (#2601)
BV instantiator: Factor out util functions. (#2604)
Previously, all util functions for the BV instantiator were static functions
in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding
unit test, it was therefore required to include this cpp file in order to
test these functions. This factors out these functions into a
theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h).
Asan reported errors for the corresponing unit test because of this.
BV inverter: Factor out util functions. (#2603)
Previously, all invertibility condition functions were static functions
in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test,
it was therefore required to include this cpp file in order to test
these functions. This factors out these functions into a
theory/quantifiers/bv_inverter_utils.(cpp|h).
Fix string register extended terms (#2597)
A regress2 benchmark was failing, due to a recent change in our strings rewriter.
The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.
The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.
This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.
Cmake: Fix ctest call for example/translator. (#2600)
example/translator expects an input file to translate but none was provided in the ctest call.
This caused the ctest call to hang and wait for input on stdin in some configurations (in
particular in the nightlies).
Address slow sygus regressions (#2598)
Disable extended rewriter when applicable with var agnostic enumeration (#2594)
Fix unif trace (#2550)
Fix cache for sygus post-condition inference (#2592)
Update default options for sygus (#2586)
Fix rewrite rule filtering. (#2591)
New C++ API: Add checks for Sorts. (#2519)
Infrastructure for string length entailments via approximations (#2514)
Only use SKIP_RETURN_CODE with CMake 3.9.0+ (#2590)
With older versions of CMake, skipped tests are reported as failures,
which is undesirable. This commit changes the CMakeLists file to only
use the `SKIP_RETURN_CODE` property if a newer version of CMake is used.
Fix end constraint for regexp elimination (#2571)
Clean remaining references to getNextDecisionRequest and simplify (#2500)
Fix mem leak in sha1_collision example. (#2588)
Fix mem leak in sets_translate example. (#2589)
Simplify datatypes printing (#2573)
Fix compiler warnings. (#2585)
Fix regress (#2575)
Add actively generated sygus enumerators (#2552)
Make CegisUnif with condition independent robust to var agnostic (#2565)
Fix stale op list in sets (#2572)
Eliminate partial operators within lambdas during grammar normalization (#2570)
cmake: Display skipped tests as not run (#2567)
Currently, the run_regression.py script just returns 0 when we skip a
test due to a feature not supported by the current configuration.
Returning 0 marks those tests as passed. To make it more clear which
tests were skipped, this commit adds the `SKIP_RETURN_CODE` [0] property
to the regression tests and changes the regression script to return 77
for skipped tests. The feature is supported since at least CMake 3.0 [0].
For backwards compatibility with autotools, returning 77 for skipped
tests is only active when `--cmake` is passed to the run_regression.py
script.
[0] https://cmake.org/cmake/help/v3.0/prop_test/SKIP_RETURN_CODE.html
Allow (_ to_fp ...) in strict parsing mode (#2566)
When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
unit: Fix ASAN detection for GCC. (#2561)
Make registration of preprocessing passes explicit (#2564)
As it turns out, self-registering types are problematic with static
linkage [0]. Instead of fixing the issue with linker flags, which seems
possible but also brittle (e.g. the flags may be different for different
linkers), this commit adds an explicit registration of each
preprocessing pass.
[0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html
Fix documentation for `make regress`. (#2557)
cmake: Add examples to build-tests, add warning for disabling static build. (#2562)
Fix "catching polymorphic type by value" warnings (#2556)
When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make
sure that we use a reference type for the exception, otherwise the unit
test tries to catch the exception by value, resulting in "catching
polymorphic type by value" warnings.
cmake: Generate compile_commands.json on configure. (#2559)
cmake: Add build target build-tests to build all test dependencies. (#2558)
init scalar class members (coverity issues 1473720 and 1473721) (#2554)
Fix compiler warnings. (#2555)
Fix dumping pre/post preprocessing passes (#2469)
This commit changes the hard-coded list of checks for
preprocessing-related dump tags to take advantage of the new
preprocessing pass registration mechanism from PR #2468. It also fixes a
typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()`
and adds a list of available passes to the `--dump help` output.
Refactor preprocessing pass registration (#2468)
This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.
As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.
This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.
[0] https://llvm.org/docs/WritingAnLLVMPass.html
Add rewrite for solving stoi (#2532)
cmake: Ignore ctest exit code for coverage reports.
Stream concrete values for variable agnostic enumerators (#2526)
Rewrites for (= "" _) and (= (str.replace _) _) (#2546)
cmake: Only do Java tests when unit testing on (#2551)
Right now, we are adding the Java tests even when we are not building
unit tests. This commit changes the build system to only add the Java
tests when unit tests are enabled. There are two reasons for this
change:
- building a production version of CVC4 should not require JUnit
- it seems more intuitive (to me at least) to disable JUnit tests when
unit tests are disabled
This change also simplifies building the Java bindings in our homebrew
formula.
cmake: Add CxxTest finder module to allow custom paths. (#2542)
Remove assertion. (#2549)
Infrastructure for using active enumerators in sygus modules (#2547)
Incorporate all unification enumerators into getTermList. (#2541)
Fix Taylor overapproximation for large exponentials (#2538)
Fix homogeneous string constant rewrite (#2545)
Fix bug in getSymbols. (#2544)
cmake: Only print dumping warning if not disabled by user. (#2543)
Makes SyGuS parsing more robust in invariant problems (#2509)
cmake: Fix test target dependency issues. (#2540)
Enable quantified array regression. (#2539)
Symmetry breaking for variable agnostic enumerators (#2527)
cmake: New INSTALL.md for build and testing instructions. (#2536)
cmake: Exclude examples for coverage target. (#2535)
Eagerly ensure literal on active guards for sygus enumerators (#2531)
cmake: Add check for GCC 4.5.1 and warn user. (#2533)
examples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534)
cmake: configure.sh wrapper: Removed unused option --gmp.
carefully printing trusted assertions in proofs (#2505)
cmake: Fix tag code generation dependencies. (#2529)
Fix warnings uncovered by cmake build (#2521)
Fix quantifiers selector over store rewrite (#2510)
Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in.
After the change, we are +61-7 on SMT LIB:
https://www.starexec.org/starexec/secure/details/job.jsp?id=30581
Allow partial models for multiple sygus enumerators (#2499)
Infrastructure for variable agnostic sygus enumerators (#2511)
Improve non-linear check model error handling (#2497)
Refactor strings equality rewriting (#2513)
This moves the extended rewrites for string equality to the main strings rewriter as a function rewriteEqualityExt, and makes this function called on every equality that is generated (from non-equalities) by our rewriter.
cmake: Fix dependencies for code generation. (#2524)
Fix wiki urls. (#2504)
cmake: Fix git version info (again). (#2523)
cmake: Fix theory order #2. (#2522)
Unify rewrites related to (str.contains x y) --> (= x y) (#2512)
cmake: Fix theory order. (#2518)
Make string rewriter unit tests more robust (#2520)
This commit changes the unit test for the string rewriter to use the
extended rewriter instead of the regular rewriter to make it more
robust, e.g. to different orderings in conjunctions.
cmake: Fix and simplify git version info. (#2516)
cmake: Add program prefix option. (#2515)
Fix generating debug/trace tags.
New C++ API: Add checks for Terms/OpTerms. (#2455)
Fix regress2. (#2502)
cmake: Add python3 option.
cmake: Enable -Wall.
cmake: Fix systemtests dependency.
cmake: Build fully static binaries with option --static.
cmake: Run make coverage in parallel by default.
cmake: Add more documentation, some fixes and cleanup.
cmake: configure.sh wrapper: Use explicit build directory structure.
We don't create build directories for every build type (and
configuration) anymore. The default build directory is now 'build'
(created where you call the wrapper script from). Option --name allows
to configure an individual name (and path) for the build directory.
cmake: configure wrapper: Modify next steps message after configuration.
Since configure.sh is only a wrapper for cmake it prints all the messages from
cmake. At the end we print the next steps after configuration. If configure.sh
is used we add the info to also change into the build directory before calling
make.
cmake: Move PACKAGE_NAME to ConfigureCVC4, more cleanup.
cmake: Refactor cvc4_add_unit_test macro to support test names with '/'.
Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
cmake: Guard GetGitRevisionDescription.
cmake: Add target runexamples.
cmake: Add support for cross-compiling for Windows.
cmake: Require JUnit version 4.
cmake: Do not allow dumping with portfolio build.
cmake: More documentation, clean up.
cmake: Move extracting git information to src/base cmake config file.
cmake: Guard examples that require Boost.
cmake: Disable unit tests if assertions are not enabled.
cmake: FindANTLR: Check if antlr3FileStreamNew is available.
cmake: configure.sh wrapper: Fixes for sh.
travis: Switch to cmake.
cmake: Do not build examples and unit and system tests by default.
cmake: configure.sh wrapper: Add --name option.
cmake: examples: Configure output directory per target.
cmake: Added java examples
cmake: configure.sh wrapper: Add --prefix for install directory.
cmake: Add some more documentation, cleanup.
cmake: Move helper functions to cmake/Helpers.cmake.
cmake: Added target examples (currently .cpp examples only)
cmake: Simplify build type configuration.
cmake: Refactor and clean up build profile printing.
cmake: Added target check
Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.
cmake: Add make install rule.
cmake: configure.sh wrapper: Fix handling of options with arguments.
cmake: Add module finder for Valgrind.
cmake: Various CMakeLists.txt fixes/cleanup.
cmake: Only build libcvc4 and libcvc4parser as libraries.
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.
cmake: Move find_package to where it is actually needed.
cmake: configure.sh wrapper: Removed env vars help text.
cmake: configure.sh wrapper: Configurable build directory
cmake: configure.sh wrapper: Create build dirs for configurations
cmake: configure.sh wrapper: done (except: configurable build dir)
cmake: Updated and prettified configuration printing.
cmake: configure.sh wrapper: option parsing
cmake: Add ENABLE_DEBUG_CONTEXT_MM to enable the debug context memory manager.
cmake: Add ENABLE_BEST to enable best configuration of dependencies.
cmake: Add Java runtime as required dependency (required for ANTLR).
cmake: Add convenience wrappers for tag generation.
cmake: Add library versioning for libcvc4.so.
cmake: Rebase with current master, add new tests/source files.
cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.
cmake: Use target specific includes for libcvc4.
Further, print definitions added with add_definitions(...).
cmake: Add missing dependency.
cmake: Add support for building static binaries/libraries.
cmake: Add options for specifying install directories for dependencies.
cmake: Add module finder for GLPK-cut-log.
cmake: Add module finder for ABC.
cmake: Compile Java tests and add to ctest if Java bindings are enabled.
cmake: Add SWIG support + Python and Java bindings.
cmake: Add dependencies for test targets and support for make coverage.
cmake: Various portfolio/default option fixes.
cmake: Enable parallel execution for test targets regress, units, systemtests.
cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.
cmake: Added system tests and target make systemtests.
cmake: Added regression tests and target make regress.
cmake: Add portfolio support.
cmake: Add ASAN support.
cmake: Enable shared by default.
Further, force shared builds in case of unit tests.
cmake: Disable W-suggest-override for unit tests.
cmake: Add target units.
cmake: Removed obsolete CMakeLists file in test.
cmake: Add support for CxxTest.
cmake: Filter through and disable unused HAVE_* variables from autotools.
cmake: Do not set global output directories for binaries and libraries.
cmake: Fix some includes.
cmake: Added support for coverage and profiling.
cmake: Added 3-valued option handling (to enable detection of user-set options).
cmake: Add module finder for readline.
cmake: Generate token headers.
cmake: Added licensing options and warnings/errors.
cmake: Cleanup CMakeLists.txt files, remove SHARED.
cmake: Add build configurations.
cmake: Fixed compiler flag macros.
cmake: Add module finder for LFSC.
cmake: Add module finder for CaDiCaL.
cmake: Add module finder for CryptoMiniSat.
cmake: Add module finder for SymFPU.
cmake: Add module finder for CLN.
cmake: Add libsignatures for proofs.
cmake: Remove unused CMakeLists.txt
cmake: Generate cvc4autoconfig.h (options currently statically set).
cmake: Added missing dependency for src/util
cmake: Working build infrastructure.
TODO: cvc4autoconfig.h
cmake: Antlr parser generation done.
cmake: Generate trace and debug tags
cmake: .cpp generation done, .h generation not yet complete
cmake: Added initial build infrastructure.
Decision strategy: incorporate arrays. (#2495)
Add rewrites for str.contains + str.replace/substr (#2496)
Decision strategy: incorporate separation logic. (#2494)
Add two rewrites for string contains character (#2492)
Refactor strings extended functions inferences (#2480)
This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type.
This is in preparation for working on solving equations and further inferences in this style.
New C++ API: Introduce new macro and exception for API checks. (#2486)
Fix issue with str.idof in evaluator (#2493)
Decision strategy: incorporate strings fmf. (#2485)
More aggressive caching of string skolems. (#2491)
Move and rename sygus solver classes (#2488)
fix assertion error (#2487)
Clean remaining references to getNextDecisionRequest in quantifiers. (#2484)
Improvements and fixes for symmetry detection and breaking (#2459)
This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.
Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)
Decision strategy: incorporate cegis unif (#2482)
Decision strategy: incorporate bounded integers (#2481)
Decision strategy: incorporate datatypes sygus solver. (#2479)
More aggressive skolem caching for strings, document and clean preprocessor (#2478)
Make strings model construction robust to lengths that are not propagated equal (#2444)
This fixes #2429.
This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment.
We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.
Regardless, the strings model construction should be robust to handle this case, which this PR does.
Follow redirects with cURL in contrib/get* scripts (#2471)
On systems without `wget`, we use `curl` to download dependencies.
However, we were not using the `-L` (follow redirects) option, which is
necessary to download certain dependencies, e.g. CryptoMiniSat.
Remove broken dumping support from portfolio build (#2470)
Dumping support for portfolio builds was introduced in
84f26af22566f7c10dea45b399b944cb50b5e317 but as far as I can tell, the
implementation has already been problematic in the original implementation. The
current implementation has the following issues:
- Dumping with a portfolio build (even when using the single threaded
executable) results in a segfault. The reason is that the DumpChannel variable
is declared as an `extern` and exists for the duration of the program. The
problem is that it stores a `CommandSequence`, which indirectly may store
nodes. When shutting down CVC4, the destructor of `DumpC` is called, which
destroys the `CommandSequence`, which results in a segfault because the
`NodeManager` does not exist anymore. The node manager is (indirectly) owned
and destroyed by the `api::Solver` object.
- Additionally, adding commands to the `CommandSequence` is not thread safe (it
just calls `CommandSequence::addCommand()`, which in turn pushes back to a
vector [0] (which is not thread safe [1]). A single instance of `DumpChannel`
is shared among all threads (it is not declared `thread_local` [2]).
- The `CommandSequence` in `DumpC` was not used in the original implementation
and is still unused on master. The original commit mentions that the portfolio
build stores the commands in the `CommandSequence` but not why.
This commit removes the `CommandSequence` and related methods from `DumpC` to
avoid the issue when destroying `DumpChannel`. It disables dumping for
portfolio builds and adds a check at configure-time that not both options have
been enabled simultaneously. Given that the option was not functional
previously, the problematic implementation, and the fact that the dump of
multiple threads wouldn't be very useful, disabling dumping for portfolio
builds is unlikely to be problem. An improvement that could be made is to
disable dumping support only for the pcvc4 binary and while enabling it for the
single-threaded version, even when using `--with-portfolio`. However, we
currently do not have the infrastructure for that (we use the same libcvc4
library for both binaries).
[0] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/command.cpp#L756
[1] https://en.cppreference.com/w/cpp/container
[2] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/dump.h#L117
Remove unnecessary tracing from preprocessing (#2472)
With the introduction of the PreprocessingPass class,
tracing/dumping/time keeping is done automatically in the base class,
eliminating the need for doing it manually. This commit cleans up
SmtEngine, removing tracing/dumping/time keeping in preprocessing that
is not needed anymore.
Decision strategy: incorporate UF with cardinality constraints (#2476)
Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462)
Refactor how assertions are added to decision engine (#2396)
Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.
Add Skolem cache for strings, refactor length registration (#2457)
This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor).
It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled.
Generalize CandidateRewriteDatabase to ExprMiner (#2340)
Fix #include for minisat headers in bvminisat. (#2463)
Uses information gain heuristic for building better solutions from DTs (#2451)
Simplify storing of transcendental function applications that occur in assertions (#2458)
Decision strategy: incorporate CEGQI (#2460)
New C++ API: Try to fix (false positive) Coverity warnings. (#2454)
Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461)
Initial infrastructure for theory decision manager (#2447)
Fix for when strings process loop is disabled. (#2456)
Fixe compiler warning in line_buffer.cpp. (#2453)
Support model cores via option --produce-model-cores. (#2407)
This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
Avoid calling size() every iteration (#2450)
Fix global negate (#2449)
fix (#2446)
Set NodeManager to nullptr when exporting vars (#2445)
PR #2409 assumed that temporarily setting the NodeManager to nullptr
when creating variables is not needed anymore. However, this made our
portfolio build fail. This commit reintroduces the temporary NodeManager
change while creating variables.
Using a single condition enumerator in sygus-unif (#2440)
This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).
In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:
- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.
A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.
There is also small improvements for trace messages.
Refactor non-clausal simplify preprocessing pass. (#2425)
Squash implementation of counterexample-guided instantiation (#2423)
Add (str.replace (str.replace y w y) y z) rewrite (#2441)
Replace boost::integer_traits with std::numeric_limits. (#2439)
Further, remove redundant gmp.h include in options_handler.cpp.
Remove clock_gettime() replacement for macOS. (#2436)
Not needed anymore since macOS 10.12 introduced clock_gettime().
Make isClosedEnumerable a member of TypeNode (#2434)
Further simplify and fix initialization of ce guided instantiation (#2437)
Refactor and document quantifiers variable elimination and conditional splitting (#2424)
Minor improvements to interface for rep set. (#2435)
More extended rewrites for strings equality (#2431)
Eliminate select over store in quantifier bodies (#2433)
Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)
Remove printing support for sygus enumeration types (#2430)
Finer-grained inference of substitutions in incremental mode (#2403)
Add regex grammar to rewriter verification tests (#2426)
Extended rewriter for string equalities (#2427)
Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)
Remove redundant strings rewrite. (#2422)
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since
re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )
This PR removes the above rewrite, which was implemented incorrectly and was dead code.
Update INSTALL instructions (#2420)
Fixes #2419. This commit adds more information about optional
dependencies, updates macOS-related information, and fixes some details.
Remove CVC3 compatibility layer (#2418)
Remove unused options file (#2413)
Minor improvements to theory model builder interface. (#2408)
Make quantifiers strategies exit immediately when in conflict (#2099)
Transfer ownership of learned literals from SMT engine to circuit propagator. (#2421)
Fix merge mishap of #2359.
Refactor ceg conjecture initialization (#2411)
Allows SAT checks of repair const to have different options (#2412)
Refactor and document alpha equivalence. (#2402)
Fix export of bound variables (#2409)
Refactor theory preprocess into preprocessing pass. (#2395)
Use useBland option in FCSimplexDecisionProcedure (#2405)
Add regular expression elimination module (#2400)
Refactor MipLibTrick preprocessing pass. (#2359)
Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)
fix bv total ops printing (#2365)
Split term canonize utility to own file and document (#2398)
Reorder …
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Python code generated from Source/Modules/python.cxx contains use of nonexistent object.getattr method. In Python3 the object type doesn't have this method, it has getattribute, which can be used instead.
The text was updated successfully, but these errors were encountered: