| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
TypeCheckingExceptionPrivate. (#1733)
While throwing a TypeCheckingExceptionPrivate, an IllegalArgumentException was thrown when
trying calling toString() on a malformed node. Fixed by printing the kind of the node and its children
rather than calling toString() on the malformed node.
|
|
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
Adds missing override keywords.
|
|
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
When compiling the Java bindings on macOS, the linker complained about
CVC4::ExprManager::mkConst<CVC4::TypeConstant>() and
CVC4::Expr::getConst<CVC4::TypeConstant>() being undefined. After some
research, I found that the issue has been introduced by commit
36bf9f8bcb2a1a3aea1f90eb4d13aed3bbf6da8f. It looks like adding the
-no-undefined flags resulted in the symbols in question being omitted
due to TypeConstant not being exported. This commit makes TypeConstant
CVC4_PUBLIC, which fixes the issue.
|
|
|
|
lambdas (#1403)
This partially solves issue #1344. Definitions are expanded when the grammar normalizer is called. When this becomes default then the code that expands definitions elsewhere will be removed.
The PR also contains minor changes to the PrintCallback and SygusGrammarNormalize module.
|
|
|
|
* Initial infrastructure for sygus printing.
* Minor
* Minor improvements
* Format
* Minor
* Empty constructor printer.
* Format
* Minor
* Format
* Address.
|
|
and 1362931. (#1373)
|
|
* Clean and document datatype.h.
* More, make TODOs.
* More documentation
* More
* Reference issue.
* Format
* Fixes and improvements.
* Minor
* Minor
* Minor
* Fix
* Minor
* Format
|
|
* 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.
|
|
* 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.
|
|
* Remove restrictions about function types
* Introduce notion of first-class type, improve assertions, add comment on equality type rule.
* Update comment
|
|
* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
|
|
Addresses CIDS: 1457252 and 1379620.
Miscellaneous cleanup to ArrayStoreAll.
|
|
CVC4 was implementing multiple, slightly different hash functions for
pairs. With pull request #1157, we have a decent generic hash function
for pairs. This commit replaces the existing hash function
implementations with a typedef of the generic hash function.
|
|
|
|
|
|
const_iterator. (#1140)
|
|
Removes the following warning when compiling with gcc version 4.8.4 :
../../../../../src/expr/kind_template.h:95:55: warning: '__visibility__' attribute ignored on non-class types [-Wattributes]
Tested with clang-3.5.
|
|
|
|
* 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)).
|
|
Changes needed for the bit-blasting floating-point solver which are outside of it's area and / or applicable independently.
|
|
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.
|
