summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2020-01-29Merge branch 'master' into oldVarHeuristicPRoldVarHeuristicPRAndrew Reynolds
2020-01-29Modularize more steps in the strings strategy (#3676)Andrew Reynolds
2020-01-29Minor updates to string utilities (#3675)Andrew Reynolds
2020-01-29Better heuristics for marking congruent variablesAndres Noetzli
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-14Generalize example-based sym breaking to conjectures with constant function a...Andrew Reynolds
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
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
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
2019-12-23Initial support for string reverse (#3581)Andrew Reynolds
2019-12-18Increment Taylor degree for tangent and secant plane inferences for transcend...Andrew Reynolds
2019-12-18Avoid calling rewriter from type checker (#3548)Andres Noetzli
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-16Use the evaluator utility in the function definition evaluator (#3576)Andrew Reynolds
2019-12-16Extend model construction with assignment exclusion set (#3377)Andrew Reynolds
2019-12-16Fix evaluator for non-evaluatable nodes (#3575)Andrew Reynolds
2019-12-16Revert evaluate as node. (#3574)Andrew Reynolds
2019-12-16Trace tags for dumping the decision tree in org-mode format (#2871)makaimann
2019-12-15Minor improvement to evaluator (#3570)Andrew Reynolds
2019-12-14Simple optimizations for the core rewriter (#3569)Andrew Reynolds
2019-12-13Eliminate Expr-level calls in TypeNode (#3562)Andrew Reynolds
2019-12-13Add support for set comprehension (#3312)Andrew Reynolds
2019-12-12 FP converter: convert: Use std::vector as instead of std::stack. (#3563)Aina Niemetz
2019-12-12Make CEGIS sampling robust to non-vanilla CEGIS (#3559)Andrew Reynolds
2019-12-12Fix Unif+PI algorithm with symbolic unfolding (#3558)Haniel Barbosa
2019-12-12Use the node-level datatypes API (#3556)Andrew Reynolds
2019-12-11Fix CEGIS refinement for recursive functions evaluation (#3555)Andrew Reynolds
2019-12-11Do not substitute beneath arithmetic terms in the non-linear solver (#3324)Andrew Reynolds
2019-12-11Support symbolic unfolding in UNIF+PI (#3553)Andrew Reynolds
2019-12-10Incorporate rewriting on demand in the evaluator (#3549)Andrew Reynolds
2019-12-09Fix case of uninterpreted constant instantiation in FMF (#3543)Andrew Reynolds
2019-12-09Make theory rewriters non-static (#3547)Andres Noetzli
2019-12-06Simplify rewrite for character matching (#3545)Andres Noetzli
2019-12-06Use str.subtr in str.to.int/int.to.str reduction (#3544)Andres Noetzli
2019-12-06Add lemma for str.to.int/int.to.str (#3541)Andres Noetzli
2019-12-06Optimize the rewriter for DT_SYGUS_EVAL (#3529)Andrew Reynolds
2019-12-06New algorithm for interpolation and abduction based on unsat cores (#3255)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback