summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-01-29Prefer old variable heuristicoldVarHeuristicAndres Noetzli
2020-01-27Stats per skolem idcav2020submissionAndres Noetzli
2020-01-27Count misses instead of hitsAndres Noetzli
2020-01-27Fix statsAndres Noetzli
2020-01-25Add statsAndres Noetzli
2020-01-25normal form fixAndres Noetzli
2020-01-25Make regexp first classAndres Noetzli
2020-01-25Adds stats and optionAndres Noetzli
2020-01-24Fix skolem lengthAndres Noetzli
2020-01-23Fix trivial solve method for single invocation (#3650)Andrew Reynolds
2020-01-22Fix subtyping for instantiations where internal representatives are chosen ↵Andrew Reynolds
(#3641)
2020-01-22Fix substitution in nl solver (#3638)Andrew Reynolds
* Fix for 3614 * Add regression * Remove regression Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-01-22Fix single invocation partition for non-function non-atomic types (#3642)Andrew Reynolds
2020-01-22Fix check for subtypes in sygus PBE (#3640)Andrew Reynolds
2020-01-22Fix parameteric sorts involving Booleans in sygus default grammars (#3629)Andrew Reynolds
2020-01-21Types and side conditions for affine bounds (#3631)Alex Ozdemir
* Types and side conditions for affine bounds Bounds (being positive, non-negative) actually have an arithmetic. This PR defines that. Useful b/c Farkas proofs are basically just sums of bounded affine functions. * Address Yoni's comments. Thanks! * Moved a positivity-test to th_real * Describe what an affine bound is in better detail
2020-01-21Affine Axioms (#3630)Alex Ozdemir
Used for proving that real terms are affine functions of their variables.
2020-01-21Types & side-conditions for linear and affine fns (#3627)Alex Ozdemir
This commit introduces types for linear combinations of arith variables along with side conditions for their arithmetic. It does the same for affine functions. These primitives are ultimately used in our machinery for Farkas proofs.
2020-01-21Axioms (and side conditions) for tightening bounds (#3613)Alex Ozdemir
* Axioms (and side conditions) for tightening bounds * Side conditions for verifying floor/ceiling-like functions * Axioms for their correct execution * Axioms for bound tightening. * Apply suggestions from code review Co-Authored-By: yoni206 <yoni206@users.noreply.github.com> * Address Yoni's comments by addings documentation. Thanks Yoni! Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
2020-01-17LIRA proof: Arithmetic predicates & reification thereof (#3612)Alex Ozdemir
* Merge branch 'master' into lira-pf-arith-pred * Shorten reify_arith_pred, thanks Yoni! Use recursion! * typo
2020-01-17LIRA sig: int, real terms, and conversions (#3610)Alex Ozdemir
* LIRA sig: int, real terms, and conversions * Address Yoni's comments. * Better description of "reify" functions * explicit (rather than implicit) `fail` when reifying integer division Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
2020-01-17Use axioms when checking goal entailment for abduction algorithm (#3611)Andrew Reynolds
2020-01-15New C++ API: Add nullary constructor for Result. (#3603)Aina Niemetz
2020-01-14Generalize example-based sym breaking to conjectures with constant function ↵Andrew Reynolds
apps (#3605)
2020-01-14Disable unsat cores for regression that times out (#3607)Andres Noetzli
Regression `regress2/strings/issue3203.smt2` is currently timing out depending on the version of the libraries loaded (see #3606 for more info). This commit temporarily disables the regression to get the nightlies to pass again.
2020-01-13Support arbitrary unsigned integer attributes (#3591)Andres Noetzli
Fixes #3586. On macOS, `size_t` resolves to `unsigned long` whereas `uint64_t` resolves to `unsigned long long`. Even though the types have the same bit-width and signedness, they are not considered the same type. This caused issues with `Attribute`s that store `size_t` values because we only specialized the `getTable()` struct for `uint64_t`. This commit changes the specialization to work for arbitrary unsigned integer types of at most 64-bit. It does that by generalizing the specialization of `getTable()` and by implementing a `KindValueToTableValueMapping` for unsigned integer attributes of up to 64-bit that casts integers between the attributes bit-width and `uint64_t`.
2020-01-10Fix side condition check in sygus core connective (#3600)Andrew Reynolds
2020-01-10Fix enum names in AIG bitblaster. (#3599)Mathias Preiner
2020-01-10Fix printing of models of uninterpreted sorts (#3597)Andres Noetzli
2020-01-10Track trivial cases in transition inference (#3598)Andrew Reynolds
2020-01-09Optimize str.substr reduction (#3595)Andres Noetzli
This commit optimizes the `str.substr` reduction by replacing the if-then-else term for the length of the suffix `len(sk2) = ite(len(s) >= n+m, len(s) - (n + m), 0)` with `(len(sk2) = len(s) - (n + m) v len(sk2) = 0) ^ len(skt) <= m`. Experiments have shown that the latter encoding is more efficient.
2020-01-08Fix backtracking issue in sygus fast enumerator (#3593)Andrew Reynolds
2020-01-07Universe set cardinality for finite types with finite cardinality (#3392)mudathirmahgoub
* rewrote set cardinality for finite-types * small changes and format
2020-01-07Fix unary minus parse check (#3594)Andrew Reynolds
2020-01-07Update any-constant and normalization policies for sygus grammars (#3583)Andrew Reynolds
2020-01-04Fix finiteness check for bounded fmf (#3589)Andrew Reynolds
Recently, finite model finding via uninterpreted sorts was decoupled from finite bound inference techniques (the BoundedIntegers module in theory/quantifiers/fmf/). This module assumed that finite model finding was enabled in one place. This fixes the issue by adding an additional check. This fixes a model unsoundness issue where bounds on an uninterpreted sort were not being enforced. This fixes #3587.
2019-12-30[proof] ITE translation fix (#3484)Alex Ozdemir
* Bugfix: convert ifte arms to formulas for printing We have two kinds of ITEs in our LFSC proofs: * ite: for sort-typed expressions * ifte: for formulas Say that we have a Bool-sorted ITE. We had machinery for emitting an `ifte` for it, but this machinery didn't actually convert the arms of the ITE into formulas... Facepalm. Fixed now. * Test the lifting of ITEs from arithmetic. This test verifies that booleans ITEs are correctly lifted to formula ITEs in LRA proofs. It used to fail, but now passes. * clang-format * Typos. * Add test to CMake * Set --check-proofs in test * Address Yoni * Expand printsAsBool documentation * Assert ITE typing soundness * Assert a subtype relation for ITEs, not equality * Update src/proof/arith_proof.h Thanks Yoni! Co-Authored-By: yoni206 <yoni206@users.noreply.github.com> Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
2019-12-23Initial support for string reverse (#3581)Andrew Reynolds
Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`). Also improves support in a few places for tolower/toupper.
2019-12-19Define all options modified by ENABLE_BEST using cvc4_option (#3578)Simon Dierl
Signed-off-by: Simon Dierl <simon.dierl@cs.tu-dortmund.de>
2019-12-19Fix typo in smt_options.toml. (#3579)Mathias Preiner
2019-12-18Increment Taylor degree for tangent and secant plane inferences for ↵Andrew Reynolds
transcendentals (#3577)
2019-12-18Avoid calling rewriter from type checker (#3548)Andres Noetzli
Fixes #3536. The type checker for the chain operator was calling the rewriter. However, the floating-point rewriter was expecting `TheoryFp::expandDefinition()` to be applied before rewriting. If the chain operator had subterms that were supposed to be removed by `TheoryFp::expandDefinition()`, the FP rewriter was throwing an exception. This commit fixes the issue by not calling the full rewriter in the type checker but by just expanding the chain operator. This is a bit less efficient than before because the rewriter does not cache the result of expanding the chain operator anymore but assuming that there are no long chains, the performance impact should be negligible. It also seemed like a reasonable assumption that the rewriter can expect to run after `expandDefinition()` because otherwise the rewriter has to expand definitions, which may be too restrictive.
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
2019-12-17Fix spurious parse error for rational real array constants (#3554)Andrew Reynolds
Currently we can't parse constant arrays that store real values that are given as rationals `(/ n m)`. We throw a spurious parse error for `((as const (Array Int Real)) (/ 1 3))`, indicating that the argument of the array is not constant. This is caused by the fact that `(/ 1 3)` is parsed as a *division* term not a rational value. This adds a special case to constant array construction so that we compute the result of a constant division instead of using the division term `(/ n m)` when constructing an array constant.
2019-12-16Use the evaluator utility in the function definition evaluator (#3576)Andrew Reynolds
Improves performance on ground conjectures with recursive functions. We use the evalutator to (partially) evaluate bodies of recursive functions, instead of relying on substitution+rewriting.
2019-12-16Extend model construction with assignment exclusion set (#3377)Andrew Reynolds
This extends the core model building algorithm in CVC4 with "assignment exclusion sets". This functionality is useful for assigning values to terms of finite type that have specific restrictions on what their value cannot be. In detail, previously, all unassigned terms of finite type were always assigned the first term in the type enumeration. This is done since it is assumed that theories (e.g. datatypes) always do enough work to ensure that *arbitrary* values can be assigned to terms of finite type, and *fresh* values can be assigned to terms of infinite type. However, there are compelling cases (sets+cardinality for finite element types) where one may want to impose restrictions on what values can be assigned to terms of finite types. Thus, we now provide `setAssignmentExclusionSet` as a way of communicating these restrictions. This commit also refactors a few parts of `TheoryEngineModelBuilder::buildModel` to be clearer, in particular by adding a few helper functions, and by caching certain information early in the function instead of recomputing it. This is work towards #1123.
2019-12-16Support ackermannization on uninterpreted sorts in BV (#3372)Ying Sheng
Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.
2019-12-16Move Datatype management to ExprManager (#3568)Andrew Reynolds
This is further work towards decoupling the Expr layer from the Node layer. This commit makes it so that ExprManager does memory management for Datatype while NodeManager maintains a list of DType. As a reminder, the ownership policy (and level of indirection through DatatypeIndex) is necessary due to not being able to store Datatype within Node since this leads to circular dependencies in the Node AST.
2019-12-16Fix evaluator for non-evaluatable nodes (#3575)Andrew Reynolds
This ensures that the Evaluator always returns the result of substitution + rewriting for constant substitutions. This requires a few further extensions to the code, namely: (1) Applying substutitions to operators, (2) Reconstructing all nodes that fail to evaluate by taking into account evaluation of their children.
2019-12-16Revert evaluate as node. (#3574)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback