summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2020-02-06Generalize containsQuantifiers to hasClosure (#3722)Andrew Reynolds
2020-02-04Articulate proof-related debug statements in arith (#3700)Alex Ozdemir
2020-02-04--fp-exp: Better warning message. (#3709)Aina Niemetz
2020-02-04Split base solver from the theory of strings (#3680)Andrew Reynolds
2020-02-04Revert semantic change from refactoring (#3711)Andres Noetzli
2020-02-03Fix corner case - might need to REWRITE_AGAIN (#3706)Clark Barrett
2020-02-03Fix 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-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2020-02-03Fix invariant template inference for trivially infeasible conjecture (#3693)Andrew Reynolds
2020-02-03Fix corner case of empty domains in bounded fmf (#3690)Andrew Reynolds
2020-02-03Example inference utility (#3670)Andrew Reynolds
2020-01-31Refactor relevance vectors for asserted quantifiers (#3666)Andrew Reynolds
2020-01-31Update sygus grammar normalization to use node-level datatype. (#3567)Andrew Reynolds
2020-01-31Refactor sygus stats (#3684)Andrew Reynolds
2020-01-31Minor refactoring of constructor classes in fast enumerator (#3685)Andrew Reynolds
2020-01-31Fix arithmetic rewriter for exponential (#3688)Andres Noetzli
2020-01-30Fix rep set increment for empty domains (#3682)Andrew Reynolds
2020-01-30Make eq chain an aggressive rewrite in extended rewriter (#3679)Andrew Reynolds
2020-01-30Eliminate spurious postprocessing step for single invocation (#3674)Andrew Reynolds
2020-01-30Ensure literals in FMF decision strategies are in the CNF stream (#3669)Andrew Reynolds
2020-01-30Move disequality list to solver state in strings (#3678)Andrew Reynolds
2020-01-30Example minimize evaluation utility. (#3671)Andrew Reynolds
2020-01-30External cache argument for evaluator (#3672)Andrew Reynolds
2020-01-30Do 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-29Better heuristics for marking congruent variables (#3677)Andres Noetzli
2020-01-29Modularize more steps in the strings strategy (#3676)Andrew Reynolds
2020-01-29Minor updates to string utilities (#3675)Andrew Reynolds
2020-01-28Do not insist on bound values being constant in arithmetic instantiation (#3643)Andrew Reynolds
2020-01-28Avoid PLUS with one child for bv2nat elimination (#3639)Andrew Reynolds
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-17Use axioms when checking goal entailment for abduction algorithm (#3611)Andrew Reynolds
2020-01-14Generalize example-based sym breaking to conjectures with constant function ↵Andrew Reynolds
apps (#3605)
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-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-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-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-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-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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback