| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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)
|
|
Older versions of GMP in combination with newer versions of GCC and
C++11 cause errors [0]. This commit adds the necessary includes of
<cstddef>.
[0] https://gcc.gnu.org/gcc-4.9/porting_to.html
|
|
const_iterator. (#1140)
|
|
This refactors the apply substitution mechanism for counterexample-guided quantifier instantiation (CEGQI).
Improvements to the code:
(1) Methods have been added to the TermProperties class that summarize their theory-independent behavior (including "getModifiedTerm", "isBasic" etc.). For now, I have not made a "TermPropertiesArith" class yet since this will require more fundamental refactoring.
(2) The terminology "has_coeff" is replaced "is_non_basic" throughout.
(3) Added the applySubstitutionToLiteral method.
(4) Both applySubstitution and applySubstitutionToLiteral are now private within CegInstantiator. This means that theory-specific instantiators do not need to implement custom ways of applying substitutions (previously the arithmetic instantiator was).
(5) applySubstitutionToLiteral is automatically called on all literals (see line 297 of ceg_instantiator.cpp). This means that BvInstantiator::processAssertion is now called on substituted literals. So for instance if our context contains two literals:
x = bv2, bvmul(x,y) = bv4
Say we are asked to solve for x first, and return the substitution {x -> bv2}, then if we are later asked to solve for y, we will call processAssertion for the literal bvmul(bv2,y)=bv4
(6) LIA-specific information "d_theta" in SolvedForm is encapsulated inside the class (with the understanding that this will be made virtual).
This commit has no impact on quantified LIA / LRA: https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
(see CVC4-092217-cegqiRefactorSubs)
|
|
|
|
|
|
Switching members of InstantiationEngine to uniqur_ptr to simplify such cases. (#1133)
|
|
* Fixing CID 1362895: Initializing d_bvp to nullptr. Miscellaneous cleanup.
|
|
|
|
* 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.
|
|
* Extend quantifier-free UF solver to higher-order. This includes an extensionality inference, and lazy conversion from APPLY_UF to HO_APPLY terms.Implements collectModelInfo and theory combination for HO_APPLY terms.
* Update comments, minor changes to functions. Update APPLY_UF skolem to be user-context dependent.
* Remove unused NodeList
|
|
The variable `g` could be set multiple times depending on
the options (e.g. a combination of `--dump-unsat-cores`
and `--dump-synth`), which could lead to memory leaks and
missing output. This commit fixes the issue by replacing
`g` with a list of `getterCommands` that are all executed and
deleted.
|
|
|
|
|
|
|
|
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.
|
|
of instantiation for LIA. (#1111)
|
|
This was introduced by changing the implementation of "isNumber" in this commit:
a94318b
This fixes issue #1105.
|
|
- Update the parser to the new constant construction
- Fix the problem with parsing +/-zero and remove some dead code
- Extend the interface for literal floating-point values.
- Add a constructor so that a parameteric operator structure can be created from a type
- Add constructors so parametric operator constants can be easily converted
- Update SMT2 printing so that it uses the informative output
|
|
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.
|
|
Floating-point comparison operators are chainable according to the standard.
|
|
|
|
* 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)).
|
|
CVC4::Exception. (#1085)
|
|
Changes needed for the bit-blasting floating-point solver which are outside of it's area and / or applicable independently.
|
|
This consists of a binary apply symbol HO_APPLY that returns the result of applying its first argument to its second argument. Update the UF rewriter to ensure that non-standard APPLY_UF applications are rewritten into curried applications of HO_APPLY.
|
|
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.
|
|
This is required for reasoning higher-order, since we may have equalities between functions, which are operators of APPLY_UF terms.
This commit gets around the previous 1% slowdown by modifying the changes to the equality engine to be minimal impact. Previously the "isInternal" flag could be reset to false after a term is marked as internal=true. This provides an interface for whether operators of a kind should be marked as internal=false from the start. When using higher-order, APPLY_UF operators will be marked as being external when the higher-order option ufHo is set to true.
This has <.001% impact on performance on QF smtlib : https://www.starexec.org/starexec/secure/details/job.jsp?id=24445
|
|
Commit 62b673a6b8444c14c169a984dd6e3fc8f685851e remove most of the
record/tuple infrastructure but did not remove the classes RecordSelect and
TupleSelect which lead to issues with Java bindings (the references to the
corresponding mkConst implementations could not be resolved). This commit
removes the remaining traces of those classes.
|
|
* Initial infrastructure for BV instantiation via word-level inversions.
* Minor clean up.
* Change visited to unordered set.
|
|
TheoryStrings::normalizeRegexp. Minor code reorganization and applying clang-tidy to the function. (#1079)
|
|
root cause is that d_normal_forms_exp[r[0]] could have referred to different vectors (as operator[] is inserting for maps). (#1080)
|
|
* 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.
|
|
Commit 546d795470ca7c30fc62fe9b6c7b8e5838e1eed4
caused our nightly builds to fail because it did
not replace CVC4_THREADLOCAL with
CVC4_THREAD_LOCAL in interactive_shell. This
commit fixes the issue and adds readline to
Travis, s.t. readline related code gets compiled
as part of our CI tests.
|
|
constraints from user input, add regressions. (#1060)
|
