Age | Commit message (Collapse) | Author |
|
* Decouple sygus term database and term database.
* Clang format
* Fix include
|
|
|
|
|
|
|
|
enum. Always initializing VarInfo::d_type. (#1333)
|
|
|
|
|
|
|
|
* Updates to interface for grammar construction.
* Minor
* Format
|
|
* Unrecursify rewrite assertion for cbqi bv.
* Format
|
|
* Generalize component contains, some infrastructure.
* Length entailment, substr for component contains, int.to.str for constant can contain concat.
* Disable rewrite.
* Fix, reenable length entailment for contains.
* Clang format, minor.
* Comment
* Minor fixes and improvements for comments.
* Improvements
* Clang format
* Fixes
* Clang format
* Fix, improve.
* Format
* Fix assertion
|
|
* Make higher-order a flag in logic info.
* Format
* Minor
* Format
|
|
* Support SAT logic.
* Add lustre example.
* Add to smt1 as well.
* Fix.
* Fix.
* Fix for new option.
|
|
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
|
|
* Fix some documentation.
* Move model basis out of term db.
* Moving
* Finished moving.
* Document Skolemize and term enumeration.
* Minor
* Model basis to first order model.
* Change function name.
* Minor
* Clang format.
* Minor
* Format
* Minor
* Format
* Address review.
|
|
* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.
* Minor
* Make unique bound variables for choice functions in BvInstantor, clean up.
* Incorporate missing optimizations
* Clang format
* Unused field.
* Minor
* Fix, add regression.
* Fix regression.
* Fix bug that led to incorrect cleanup of instantiations.
* Add missing regression
* Improve handling of choice rewriting.
* Fix
* Clang format
* Use canonical variables for choice functions in cbqi bv.
* Add regression
* Clang format.
* Address review.
* Clang format
|
|
* Move type set to its own file and document.
* Move theory engine model builder to its own class.
* Working on documentation.
* Document Theory Model.
* Minor
* Document theory model builder.
* Clang format
* Address review.
|
|
|
|
|
|
document (#1290)
* Move, document, and rename enumerative instantiation.
* Clang format.
|
|
* Initial infrastructure for static preprocessing for sygus conjectures.
* Initial infrastructure.
* Minor change in terminology, move enumerator to synth-fun mapping to sygus term database, minor fix and add documentation to NegContainsInvarianceTest.
* Clang format
* Fixing comments, more initial infrastructure.
* More
* Minor
* New clang format.
* Address review.
|
|
* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206.
* Minor
* Minor
* Change namespace style.
* Address review
* Fix incorrectly merged portion that led to regression failures.
* New clang format, fully document relevant domain.
* Clang format again.
* Minor
|
|
* Work on rewriter for string contains.
* Add rewrites that mix str.to.int and str.contains. Documentation, add regression.
* Minor
* Minor
* Address review, add a few TODOs. Improve some non-digit -> not is number.
* Fix
* Simplify.
* Clang format, minor fixing of comments.
|
|
* Initial documentation, incomplete.
* Document arith utilities in quantifiers.
* Minor
* Clang format
* Minor
* Clang format.
* Minor
* Apply new clang format.
* Document ordering.
|
|
* Multi-instantiation heuristic for cbqi bv.
* New clang format.
* Minor
* Minor.
* Minor
|
|
* Refactor theory model, working on making RepSet references const.
* Encapsulation of members of rep set.
* More documentation on rep set.
* Swap names
* Reference issues.
* Minor
* Minor
* New clang format.
|
|
* Initial support for Hilbert choice operator.
* Clang format.
* Fix
* Minor
|
|
|
|
This clarifies the memory ownership of EqProofs.
|
|
This adds inverse handling for BITVECTOR_XOR, BITVECTOR_SIGN_EXTENDS, BITVECTOR_COMP, BITVECTOR_ASHR. Function isInvertible() now corresponds to exactly the operators (plus index) for which we can determine an inverse, which avoids traversing along non-invertible paths.
This further enables a test case that I missed to enable in PR #1268.
|
|
* Add mode for cbqi bv inequality handling.
* Implement the mode.
* Clang format
* Apply new clang format.
* Revert "Apply new clang format."
This reverts commit 1fec0ed999e45daacc4c756f11b5ecb4690f6561.
* Revert "Clang format"
This reverts commit 17042edb82d64c159aeddfe0264cd663998d0471.
* Clang format, second try.
* Revert "Clang format, second try."
This reverts commit f862c47c34bc313f5bc49a26b7586a4824e5aae0.
* Apply clang format, try 3.
|
|
|
|
This adds inverse handling for ULT(BV), SLT(BV) and disequalities. Rewriting of inequalities and disequalities to equalities with slack can now be disabled with an option (--cbqi-bv-inv-in-dis-eq). Function solve_bv_constraint is now merged into solve_bv_lit.
|
|
* Initial documentation and clean up of SyGuS PBE class, fix issue with concat strategy.
* More documentation, cleanup.
* Do not use concat strategy for 3+ arguments to concat, add regression.
* Minor
|
|
|
|
If a newly introduced atom is not rewritten it can happen that the
literals of both the original atom and the rewritten atom end up in the CNF.
However, only the original atom has a BB definition and the literal of the
rewritten atom is unconstrained (no BB definition).
|
|
* Add option sygus-abort-size, which tells the enumerative SyGuS solver to abort when it reaches a given term size.
* Apply clang format.
|
|
* Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks.
* Minor fix
* Fix bug in Node::hasBoundVar for non-ground operators.
* Add regression.
* Address review.
* Apply clang format.
|
|
This refactors function solve_bv_constraint to use a switch-case over kinds rather than an if-else chain.
|
|
|
|
* Initial revision of mapping sygus enumeration terms to CegConjectures. This will allow us to generalize conjecture-specific symmetry breaking.
* Change function names, simplify.
* Fix assertion, minor optimization
* Cleanup, documentation, simplification.
* Address review.
* Apply clang format.
|
|
This adds inverse handling for BITVECTOR_EXTRACT. Fixes previously disabled regressions. These regressions are now enabled.
|
|
Adds two heuristics for cbqi-bv, both disabled by default.
The first optimistically solves for boundary points of inequalities.
The second randomly interleaves inversion and value instantiations.
Adds some newly solved regressions from SMT LIB.
|
|
* Initial support for solving bit-vector inequalities in cegqi-bv using conversion to positive equality + model value slack.
* Clang format, remove heuristic.
* Update regressions.
* Simplify interface for CegInstantiator
|
|
This fixes and enables previously added regression tests for CBQI BV. It further removes one of the tests that was obsolete (since it goes through even without --cbqi-bv).
This further fixes the inverse computation for BITVECTOR_LSHR, which was broken due to a mismatching bit-width when creating a shift node.
|
|
|
|
|
|
to remove non-invertible operators. Add regression. (#1222)
|
|
* Remove restrictions about function types
* Introduce notion of first-class type, improve assertions, add comment on equality type rule.
* Update comment
|
|
Commit 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 introduced a memory leak
where d_quant_attr was not deleted when the QuantifiersEngine was
destroyed. This commit fixes the issue by turning d_quant_attr into an
std::unique_ptr.
|