| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
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
|
|
* 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.
|
|
* Fix for bug 1247: in incremental mode, there was a corner case where
a skolem variable introduced during ITE removal became a solved-for
variable (part of the substitution map). But then if the same skolem
was introduced again as part of a subsequent ITE removal pass, the
substitution was not properly applied and an incorrect result was obtained.
The handling of substitutions in incremental mode is quite kludgey - I
opened an issue to revisit this.
* fixing regression
|
|
Extends test/unit/expr/node_black.h with tests that show Node and TNode can work with C++11 for each loops.
|
|
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
|
|
* Allow any smt2 logic to be a sygus logic. Add non-linear SyGuS regressions.
* Minor
* Add case for reals, comment.
* Fix regress1.
|
|
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)
|
|
This implements side conditions and the instantiation via word-level inversion for operators BITVECTOR_AND, BITVECTOR_OR, BITVECTOR_UREM (Index=1), BITVECTOR_LSHR (index=0).
|
|
This adds several utility functions for the theory BV. Function mkUmulo encodes an unsigned multiplication overflow detection operation, which we need for CBQI BV. In the future, we will introduce a Umulo node kind (and a corresponding bit-blasting strategy based on the encoding implemented in mkUmulo).
|
|
* Add regression from pull request #50, which was fixed separately in pull request #1162.
* Improve comment in regression
|
|
* Update parser for operator overloading.
* Improvements
* Updates
* Add assert
|
|
|
|
* Refactor conjecture class in ce guided instantiation, move to own file. In preparation for sygus streaming mode.
* Infrastructure for streaming guards, more cleanup.
* Do explicit exclusion to move to next solution for sygus streaming option, now functional. More cleanup.
* More cleanup, add comments.
* Update comments
* Optimizations for invariant synthesis. Fix corner case for single invocation inference, more encapsulation in single inv utility. Minor fix for variable elimination in quantifiers rewriter.
* Fix makefile.
* Cleanup.
* Remove unused includes.
* Minor
|
|
* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression.
* Enable other regression
|
|
* Initial work on BV CEGQI, still working on avoid circular dependencies with inversion skolems.
* Guard by option, minor notes.
* Minor
* Minor fixes.
* Minor
|
|
* Optimization for model finding for recursive functions involving branching positions. Update documentation, add regressions.
* Simplifications, update comments.
|
|
|
|
* Decouple single invocation techniques from deep embedding techniques. Embed templates for invariant synthesis into grammar instead of as a global substitution. Add regression.
* Update comment on class
* Cleanup
* Comments for sygus type construction.
|
|
Commit 54d24c786d6a843cc72dfb5e377603349ea5e420 was
changing CVC4 to handle certain non-fatal errors
(such as calling get-unsat-core without a proceding
unsat check-sat command) without terminating the
solver. In the case of get-unsat-cores, the changes
lead to the solver crashing because it was trying to
print an unsat core initialized with the default
constructor, so the member variable d_smt was NULL,
which lead to a dereference of a null pointer.
One of the issues of the way non-fatal errors were
handled was that the error reporting was done in the
invoke() method of the command instead of the
printResult() method, which lead to the error
described above and other issues such as a call to
get-value printing a value after reporting an error.
This commit aims to improve the design by adding a
RecoverableModalException for errors that the solver
can recover from and CommandRecoverableFailure to
communicate that a command failed in a way that does
not prohibit the solver from continuing to execute.
The exception RecoverableModalException is thrown by
the SMTEngine and the commands catch it and turn it
into a CommandRecoverableFailure. The commit changes
all error conditions from the commit above and adds a
regression test for them.
|
|
This was introduced by changing the implementation of "isNumber" in this commit:
a94318b
This fixes issue #1105.
|
|
* Remove unhandled subtypes, which consequently makes typing rules uniformly stricter based on weakening the subtype relation. Ensure coercions in the smt2 and cvc parser for Real decimal constants whose type is Integer. Ensure type annotations are computed during preRewrite to ensure rewriting (which does not preserve types) does not impact term construction for parametric datatypes. This fixes issue #1048 (we now give an type exception).
* Update unit test for parametric datatypes to reflect new subtyping relation.
* Remove deprecated test.
* Make array construction for lambdas work with new subtype relations to handle lambdas like (lambda ((x Int) (y Int)) (ite (= x 0) 0.5 0.0)).
|
|
Add isConst check for lambda expressions by conversions to and from an Array representation where isConst is implemented. This enables check-model to succeed on higher-order benchmarks. Change the builtin rewriter for lambda to attempt to put lambdas into constant form. Update regression.
|
|
* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.
* Add comments concerning expandDefinitions
* Expand comment, move to .h
|
|
* Remove support for conversions between uint32/uint16 and string.
* Temporarily disable regression.
|
|
constraints from user input, add regressions. (#1060)
|
|
Fix model construction for parametric types so that we enumerate types in order of dependencies, and avoid subterms of previously enumerated values.
There was a bug in model construction for parametric types which was related to enumerating values that are subterms of other previously enumerated values created during model construction (which were not recorded).
This commit adds all subterms of values we enumerate to the "already used value" sets of their respective types, as reflected in the changes to TypeSet.
There is an extra wrinkle in making the above change, which was caught by the regression test/regress/regress0/fmf/dt-proper-model.smt2. The issue is specific to finite model finding and can be corrected by ensuring that base types (e.g. uninterpreted sorts) are enumerated first.
The change to TheoryModel::buildModel that replaces "allTypes" with "type_list" fixes this wrinkle. This constructs a partially ordered list of types where T1 comes before T2 if values of T2 can contain terms of type T1 but not vice versa. Ordering our enumeration in this way is probably a good idea in general. This ensures we enumerate values for equivalence classes of e.g. Int before (Array Int Int) and means we exclude fewer intermediate values during model construction.
|
|
|
|
|
|
As discussed in pull request #220, commit
360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 mostly got rid of SubrangeBound(s).
There were still a few mentions of it left in the code, most of them commented
out. The occurrences in expr.i and expr_manager.i, however, created issues with
the Python wrapper. This commit removes the SubrangeBound(s) implementation and
other leftovers.
|
|
- Build fixes for Windows
- Make proof checking tempfile handling portable
- Test suite fixes for Windows
|
|
|
|
To prevent timing out on Travis, this commit adds the option to split
the regression tests into groups and run each group in a separate job.
The group of a test is determined by computing a checksum of its name.
|
|
sygus), update regressions.
|
|
|
|
configure.ac. (#200)
CxxTest headers were included in test/unit/Makefile.am as -I@CXXTEST@. However, in configure.ac if CXXTEST was not set by the user, it was initially set to `dirname "$CXXTESTGEN"` while determining the path to the header files. If CXXTESTGEN pointed to /usr/bin and if the headers were found in /usr/include, CXXTEST was not reset, which led to CXXTEST being replaced by /usr/bin in test/unit/Makefile.am. As a consequence, the locale binary in /usr/bin got included instead of the locale header file.
|
|
|
|
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
|
|
|
|
Removing it as well.
|
|
|
|
Disable support for subrange and predicate subtypes (which were only partially supported previously).
|
|
|
|
of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
|
