summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2022-01-18Merge branch 'master' into fix-cln-static-downloadfix-cln-static-downloadAndrew Reynolds
2022-01-18Print original form for substitutions and learned literals (#7959)Andrew Reynolds
2022-01-17Refactor options related to rewriting and symmetry breaking in sygus (#7949)Andrew Reynolds
2022-01-17[Strings] Fix rewriter for `re.loop` (#7956)Andres Noetzli
2022-01-15Fix CMake script for static, auto-download, cln configurationMatthew Sotoudeh
2022-01-15Change how RANs are printed (#7955)Gereon Kremer
2022-01-15Add inverse inference for update-over-concat (#7954)Andrew Reynolds
2022-01-14Improve names for sygus enumeration option (#7945)Andrew Reynolds
2022-01-14Clean enumerative instantiation options (#7947)Andrew Reynolds
2022-01-14Implement -o subs to show learned top-level substitutions (#7944)Andrew Reynolds
2022-01-14Rename python APIs (#7950)Alex Ozdemir
2022-01-14Preprare central model building for RANs (#7951)Gereon Kremer
2022-01-14refactor div rewriter, add support for ran (#7941)Gereon Kremer
2022-01-14Fix learned rewrite pass for non-real equalties (#7936)Andrew Reynolds
2022-01-14Add operator<<(RewriteStatus) (#7952)Gereon Kremer
2022-01-14Weaken assertion in relevance manager (#7943)Andrew Reynolds
2022-01-14Refactor arithmetic pre-rewriter for multiplication (#7930)Gereon Kremer
2022-01-14Add support for RANs in rewriter for `MULT` (#7940)Gereon Kremer
2022-01-14Add RAN support in UMINUS rewriter (#7933)Gereon Kremer
2022-01-13Add arithmetic rewriter for RAN (#7929)Gereon Kremer
2022-01-13Fix bug in evaluator for division by zero (#7942)Andrew Reynolds
2022-01-13Unify abstract values and uninterpreted constants (#7424)Andres Noetzli
2022-01-13Refactor post rewriter for addition (#7931)Gereon Kremer
2022-01-13Fix check whether we have a tag (#7901)Gereon Kremer
2022-01-12Add -o learned-lits to output learned literals (#7934)Andrew Reynolds
2022-01-12Refactor atom rewriting to be RAN-aware (#7928)Gereon Kremer
2022-01-12Refactor rewriteMinus (#7932)Gereon Kremer
2022-01-12Ensure configuration of shared selectors is consistent in SyGuS subsolver (#7...Andrew Reynolds
2022-01-12Always enable RAN, but disable its implementation without poly (#7910)Gereon Kremer
2022-01-12Add mkRealAlgebraicNumber (#7923)Gereon Kremer
2022-01-12Always use partial function for sqrt (#7926)Andrew Reynolds
2022-01-12Eliminate use of subtyping from results of quantifier elimination (#7885)Andrew Reynolds
2022-01-11Adds a kind to hold RealAlgebraicNumber constants (#7908)Gereon Kremer
2022-01-11Disable filtering of shapes in sygus-rcons pool. (#7922)Abdalrhman Mohamed
2022-01-11Fix `TypeNode::substitute()` for type constants (#7920)Andres Noetzli
2022-01-11api: Fix formatting of docs for Term::getSetValue(). (#7914)Aina Niemetz
2022-01-11Remove static accesses to options (#7913)Gereon Kremer
2022-01-11Tighten policy for unsat cores in sygus core connective (#7911)Andrew Reynolds
2022-01-11Guard use of unsat core mode pp-only (#7899)Andrew Reynolds
2022-01-11Fix `TypeNode::substitute()` (#7916)Andres Noetzli
2022-01-11Check the synthesized funs of `check-synth-next`. (#7915)Abdalrhman Mohamed
2022-01-11Add new idiomatic examples (#7912)Alex Ozdemir
2022-01-11[Win64] Link LibPoly statically for static builds (#7891)Andres Noetzli
2022-01-10Fix internal type error when printing lambdas with more than one variable in ...Andrew Reynolds
2022-01-10Check arity in Sort::instantiate (#7897)Andrew Reynolds
2022-01-10Add new methods for RealAlgebraicNumber (#7907)Gereon Kremer
2022-01-10Update to latest libpoly version (#7906)Gereon Kremer
2022-01-10api: Remove Sort::isComparableTo(). (#7903)Aina Niemetz
2022-01-10Avoid gcc/10.1.0 bug by moving some configuration into a namespaceMatthew Sotoudeh
2022-01-07Start post-release for 0.0.5Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback