| Age | Commit message (Collapse) | Author |
|---|
|
to remove non-invertible operators. Add regression. (#1222)
|
|
* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand.
* Comment
* Pass expression names by reference.
* Update throw specifiers.
* Minor
* Switch expression names to CDMap, simplify interface for printing unsat core names.
* Revert throw specifier change.
* Minor simplifcations
|
|
* Remove restrictions about function types
* Introduce notion of first-class type, improve assertions, add comment on equality type rule.
* Update comment
|
|
This adds option --copyright which displays copyright information for CVC4. It further extends --show-config with copyright information and adds a banner with copyright information in interactive mode.
|
|
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.
|
|
This commit adds the skeleton of the theory solver using a dummy version of the converter (fp_converter.{h,cpp}). The converter is a class that is used to produce bit-vector expressions equivalent to floating-point ones. The commit sets up the equality engine and the infrastructure for interacting with the main theory components. The majority of this code is still agnostic to how the conversion is actually implemented / what kind of theory solver this is. This is pretty much the template code you need to write any kind of theory solver. This includes equality reasoning and so should be able to solve some basic problems.
|
|
* 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.
|
|
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).
|
|
|
|
The COPYING file now only contains the modified BSD license of CVC4 and specifies the software that is either incorporated into CVC4 or can be linked against CVC4. The copyright and license information for each software can now be found in the licenses/<software>-LICENSE.
The COPYING file has now 3 sections:
(1) modified BSD license of CVC4
(2) non-GPLv3 software that is incorporated in CVC4 or that can be linked against CVC4
(3) GPLv3 software that can be optionally linked against CVC4
|
|
This ensures a single success is printed for synth-fun and synth-inv. (#1193)
|
|
* Update model construction for higher order. If HO_APPLY terms are present for a function, we use a curried (tree) model construction to avoid exponential size model representations for function definitions.
* Update comments.
* Change terminology in comment.
* Improve comments.
|
|
This is a patch, originally from mdeters/cdhashmap-default-constructibility that allows CDHashMaps to be declared for objects that don't have default constructors.
|
|
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).
|
|
Quantifiers utilities for higher-order.
This makes the term indexing mechanisms in Term Database take into account equalities between functions, in which case the term indices for the two functions merges.
Also adds required options and a minor utility for implementing app completion.
|
|
Addresses CIDS: 1457252 and 1379620.
Miscellaneous cleanup to ArrayStoreAll.
|
|
* Add regression from pull request #50, which was fixed separately in pull request #1162.
* Improve comment in regression
|
|
Also removed obsolete CUDD related code.
|
|
* Move sygus grammar utilities to separate file.
* Minor
* Move includes
|
|
* Update parser for operator overloading.
* Improvements
* Updates
* Add assert
|
|
This commit is a preparation step for removing the --thread-stack
option (and, ultimately, the dependency on Boost). It just copies the
2017 version of the scripts and changes the --fs-inst flag to
--fs-interleave, following the renaming in commit
7766f0ba088ad6d6c58ea9678477b255c9e52fee.
|
|
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.
|
|
- Add new kinds for partially defined functions
- Print the new kinds
- Type rules for the new total kinds
- Constant folding and rewrites for the new total kinds
|
|
Make eliminateSkolemFunctions(...) iterative and some more minor fixes.
|
|
|
|
isFinished. (#1176)
The throw specifier has been moved to a comment.f
This allows for fixing several CIDs on FloatingPointEnumerator: 1457254, 1457258, 1457260, 1457269, 1457270, 1457274, and 1457275.
This also has miscellaneous formatting, documentation and const labeling improvements.
|
|
|
|
|
|
* 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
|
|
CVC4 was computing hashes for pairs of objects by simply XORing the
hashes of the two objects. This commit implements a better way of
combining hashes based on the FNV-1a hash algorithm. The algorithm is
public domain.
|
|
|
|
cvc4 --show-config reported the wrong configuration for readline since
HAVE_LIBREADLINE is set to 0 or 1 but was checked with #ifdef.
|
|
* Preparing for bv instantiation, initial working version.
* Undoing bv changes to break up into smaller commit.
|
|
* Optimization for model finding for recursive functions involving branching positions. Update documentation, add regressions.
* Simplifications, update comments.
|
|
This forces "counterexample lemmas" (the formula B => ~phi[e] on page 23 of http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf) to be added during TheoryQuantifiers::preRegisterTerm instead of at full effort check. This is required to ensure that CVC4's partial quantifier elimination algorithm produces correct results.
Some background:
"get-qe" and "get-qe-disjunct" are commands in the SMT2 parser. Here is how they can be used:
[declarations]
[assertions A]
(get-qe (exists X F))
returns a ground formula F' such that A ^ F' and A ^ (exists X F) are equivalent.
The command "get-qe-disjunct" provides an interface for doing an incremental version of "get-qe".
[declarations]
[assertions A]
(get-qe-disjunct (exists X F))
returns a ground formula F1' such that A ^ F' implies A ^ (exists X F). It moreover has the property that if you call:
[declarations]
[assertions A]
(assert F1')
(get-qe-disjunct (exists X F))
this will give you a formula F2' where eventually:
[declarations]
[assertions A]
(assert (not (or F1' ... Fn')))
(get-qe-disjunct (exists X F))
will either return "true" or "false", for some finite n.
Here is an example that failed before this commit:
(set-logic LIA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(assert (or (not (>= (+ a (* (- 1) b)) 1)) (not (>= (+ c (* (- 1) d)) 0))))
(get-qe-disjunct (exists ((x Int)) (and (> a b) (> c x) (> d x))))
This should return:
(not (or (not (>= (+ a (* (- 1) b)) 1)) (>= (+ c (* (- 1) d)) 1)))
Previously it was returning:
false
This is because the cbqi algorithm needs to assume the negation of the quantified formula we are doing qe on before it makes any decision.
The get-qe-partial feature is being requested by Cesare and Daniel Larraz for Kind2.
This improves our performance on quantified LIA/LRA:
https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
see CVC4-092617-2-fixQePartial
|
|
This implements side conditions and the instantiation via word-level inversion for operator BITVECTOR_MULT.
|
|
|
|
CVC4's implementation of seek was calculating the pointer difference
between the current position in the input and the seek point to
determine how many characters to consume. This was causing problems when
ANTLR was seeking to a pointer on a line after the current line because
it would result in a big number of characters to consume because each
line is allocated separately. This resulted in issue #1113, where CVC4
was computing a large number of characters to consume and would block
until it received all of them. This commit fixes and simplifies the
code by simply consuming characters until the seek point is reached
without computing a count beforehand.
|
|
to_real takes a single argument as given in kinds.
|
|
|
|
GetModelCommand to nullptr. (#1142)
|
|
|
|
|
|
|
|
(#1135)
|
