summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2020-02-07Example evaluation cache utility (#3698)Andrew Reynolds
2020-02-06Fix exact sqrt (#3721)Andrew Reynolds
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-04Fix header installation on MacOS. (#3660)Mathias Preiner
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-03Utility function for getting component types (#3703)Andrew Reynolds
2020-02-03Fix cardinality of uninterpreted types when univset is not used (#3663)mudathirmahgoub
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-02-02Renaming '--bsd' to '--no-gpl' (#3609)Andrew V. Jones
2020-01-31Handle `expectedType` in TheoryProofEngine (#3691)Alex Ozdemir
2020-01-31Allow PBE symmetry breaking with sygus stream (#3686)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-30Weaken assertion for models with approximations (#3667)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
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-29expectedType in proof-printing code (#3665)Alex Ozdemir
2020-01-29Fix isLeq function in String utility (#3659)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
2020-01-22Fix substitution in nl solver (#3638)Andrew Reynolds
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-15New C++ API: Add nullary constructor for Result. (#3603)Aina Niemetz
2020-01-14Generalize example-based sym breaking to conjectures with constant function a...Andrew Reynolds
2020-01-13Support arbitrary unsigned integer attributes (#3591)Andres Noetzli
2020-01-10Fix side condition check in sygus core connective (#3600)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback