Age | Commit message (Collapse) | Author |
|
* Decouple sygus term database and term database.
* Clang format
* Fix include
|
|
This adds functions on Integers to compute modular addition, multiplication and inverse.
This is required for the Gaussian Elimination preprocessing pass for BV.
|
|
|
|
|
|
|
|
* Initialize TimerStat::d_start.
* 0 initializing d_data.
|
|
Logic enum with an UNSET value. (#1329)
|
|
|
|
* Removing an unused member from Tptp. Initializing members of Tptp.
* Removing delcaration for myPopCharStream.
|
|
enum. Always initializing VarInfo::d_type. (#1333)
|
|
* Allow FORALL passed as an argument to get-qe.
* Document
* Format
* Minor
|
|
|
|
|
|
|
|
* Updates to interface for grammar construction.
* Minor
* Format
|
|
* Unrecursify rewrite assertion for cbqi bv.
* Format
|
|
Returns a copy of d_value to enable public access of GMP and CLN data.
|
|
* 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.
|
|
|
|
* Remove front end hack for sygus.
* Remove other hack, add sygus solution output mode.
* Clang format
* Minor
* Fix
* Minor
* Remove unused field.
|
|
* 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.
|
|
|
|
|
|
* Change bvudiv semantics based on input language
The semantics of division by zero have changed from SMT 2.5 to SMT 2.6.
This commit sets the default options for the division semantics based on
the language version used. The input language was already kept track of
in the options, so this commit just updates the input language option
when there is a set-info command. This mirrors how the code already
deals with the output language.
Note: With this commit, set-info overwrites the option set by the user.
This is done to be consistent with the parser.
This partially fixes #1241.
* clang format
|
|
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.
|
|
* Use uintptr_t for pointer casts in Swig files
CVC4's Swig interface files were casting pointers to longs in multiple
instances. The problem with that is that on certain platforms *cough*
Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit
executable (they use the LLP64 data model). This made the compilation of
language bindings fail with MinGW. This commit changes the types to
uintptr_t defined in Swig's stdint.i.
* Modify LDFLAGS to support shared libraries for Win
This commit adds "-no-undefined" to the LDFLAGS of CVC4's library, which
is required for building DLLs (shared libraries on Windows). It also
adds "--export-all-symbols" to the linker flags of the parser to ensure
that there are no unresolved symbols when linking against it (see
comment in the Makefile.am for details).
* Fix for non-Windows builds
* add no-undefined to libcvc4compatjni
|
|
* 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
|
|
older versions of SWIG. (#1281)
|
|
* Do not allow function variants with operator overloading.
* Minor.
* New clang format.
* Minor improvements.
|
|
CVC4's Swig interface files were casting pointers to longs in multiple
instances. The problem with that is that on certain platforms *cough*
Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit
executable (they use the LLP64 data model). This made the compilation of
language bindings fail with MinGW. This commit changes the types to
uintptr_t defined in Swig's stdint.i.
|
|
|
|
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).
|