Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-02-06 | Generalize containsQuantifiers to hasClosure (#3722) | Andrew Reynolds | |
2020-02-04 | Articulate proof-related debug statements in arith (#3700) | Alex Ozdemir | |
2020-02-04 | --fp-exp: Better warning message. (#3709) | Aina Niemetz | |
2020-02-04 | Split base solver from the theory of strings (#3680) | Andrew Reynolds | |
2020-02-04 | Revert semantic change from refactoring (#3711) | Andres Noetzli | |
2020-02-03 | Fix corner case - might need to REWRITE_AGAIN (#3706) | Clark Barrett | |
2020-02-03 | Fix cardinality of uninterpreted types when univset is not used (#3663) | mudathirmahgoub | |
* Fixed bug 3662 * format * small change * added bug3663.smt2 file * throw Logic Exception * throw Logic Exception * ;EXIT: 1 Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com> | |||
2020-02-03 | Split on model values when repaired model from non-linear is inconsisent (#3668) | Andrew Reynolds | |
2020-02-03 | Fix invariant template inference for trivially infeasible conjecture (#3693) | Andrew Reynolds | |
2020-02-03 | Fix corner case of empty domains in bounded fmf (#3690) | Andrew Reynolds | |
2020-02-03 | Example inference utility (#3670) | Andrew Reynolds | |
2020-01-31 | Refactor relevance vectors for asserted quantifiers (#3666) | Andrew Reynolds | |
2020-01-31 | Update sygus grammar normalization to use node-level datatype. (#3567) | Andrew Reynolds | |
2020-01-31 | Refactor sygus stats (#3684) | Andrew Reynolds | |
2020-01-31 | Minor refactoring of constructor classes in fast enumerator (#3685) | Andrew Reynolds | |
2020-01-31 | Fix arithmetic rewriter for exponential (#3688) | Andres Noetzli | |
2020-01-30 | Fix rep set increment for empty domains (#3682) | Andrew Reynolds | |
2020-01-30 | Make eq chain an aggressive rewrite in extended rewriter (#3679) | Andrew Reynolds | |
2020-01-30 | Eliminate spurious postprocessing step for single invocation (#3674) | Andrew Reynolds | |
2020-01-30 | Ensure literals in FMF decision strategies are in the CNF stream (#3669) | Andrew Reynolds | |
2020-01-30 | Move disequality list to solver state in strings (#3678) | Andrew Reynolds | |
2020-01-30 | Example minimize evaluation utility. (#3671) | Andrew Reynolds | |
2020-01-30 | External cache argument for evaluator (#3672) | Andrew Reynolds | |
2020-01-30 | Do not debug check model for models with approximations (#3673) | Andrew Reynolds | |
We don't run check-model for models with approximate values, however we were still running the internal debugCheckModel method, which leads to assertion failures. This disables this check. Fixes #3652. | |||
2020-01-29 | Better heuristics for marking congruent variables (#3677) | Andres Noetzli | |
2020-01-29 | Modularize more steps in the strings strategy (#3676) | Andrew Reynolds | |
2020-01-29 | Minor updates to string utilities (#3675) | Andrew Reynolds | |
2020-01-28 | Do not insist on bound values being constant in arithmetic instantiation (#3643) | Andrew Reynolds | |
2020-01-28 | Avoid PLUS with one child for bv2nat elimination (#3639) | Andrew Reynolds | |
2020-01-23 | Fix trivial solve method for single invocation (#3650) | Andrew Reynolds | |
2020-01-22 | Fix subtyping for instantiations where internal representatives are chosen ↵ | Andrew Reynolds | |
(#3641) | |||
2020-01-22 | Fix 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-22 | Fix single invocation partition for non-function non-atomic types (#3642) | Andrew Reynolds | |
2020-01-22 | Fix check for subtypes in sygus PBE (#3640) | Andrew Reynolds | |
2020-01-22 | Fix parameteric sorts involving Booleans in sygus default grammars (#3629) | Andrew Reynolds | |
2020-01-17 | Use axioms when checking goal entailment for abduction algorithm (#3611) | Andrew Reynolds | |
2020-01-14 | Generalize example-based sym breaking to conjectures with constant function ↵ | Andrew Reynolds | |
apps (#3605) | |||
2020-01-10 | Fix side condition check in sygus core connective (#3600) | Andrew Reynolds | |
2020-01-10 | Fix enum names in AIG bitblaster. (#3599) | Mathias Preiner | |
2020-01-10 | Track trivial cases in transition inference (#3598) | Andrew Reynolds | |
2020-01-09 | Optimize 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-08 | Fix backtracking issue in sygus fast enumerator (#3593) | Andrew Reynolds | |
2020-01-07 | Universe set cardinality for finite types with finite cardinality (#3392) | mudathirmahgoub | |
* rewrote set cardinality for finite-types * small changes and format | |||
2020-01-07 | Update any-constant and normalization policies for sygus grammars (#3583) | Andrew Reynolds | |
2020-01-04 | Fix 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-23 | Initial 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-18 | Increment Taylor degree for tangent and secant plane inferences for ↵ | Andrew Reynolds | |
transcendentals (#3577) | |||
2019-12-18 | Avoid 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-17 | Generate 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-16 | Use 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. |