summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-10-20Unify abstract values and uninterpreted constantsabstractValsAndres Noetzli
2021-10-20Moreajreynol
2021-10-20Formatajreynol
2021-10-20Fixajreynol
2021-10-20Formatajreynol
2021-10-20Correctly parse uninterpreted constant values in get-valueajreynol
2021-10-20Correctly parse uninterpreted constant values in get-value (#7393)Andrew Reynolds
2021-10-20Avoid escaping `double-quotes` twice. (#7409)Abdalrhman Mohamed
2021-10-20Make proofs of rewrites robust to use in internal subsolvers (#7411)Andrew Reynolds
2021-10-20Add basic regular expression type enumerator (#7416)Andrew Reynolds
2021-10-19Fix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM...Andrew Reynolds
2021-10-19Support sequences of fixed finite cardinality (#7371)Andrew Reynolds
2021-10-19Fix issue related to sanity checking integer models (#7363)Andrew Reynolds
2021-10-19Remove setDefaults methods (#7413)Gereon Kremer
2021-10-18Add regression for fixed issue (#7395)Andrew Reynolds
2021-10-18Move check for experimental arrays features to `theory_arrays.cpp`. (#7391)Abdalrhman Mohamed
2021-10-18Update SMT-COMP script (#7389)Andres Noetzli
2021-10-15Python api documentation: Op, Grammar, Result, Enums (#7095)yoni206
2021-10-15Add more regressions for fixed issues (#7382)Andrew Reynolds
2021-10-15Have docs_upload properly upload tags. (#7352)Gereon Kremer
2021-10-15Fix bad cast in the python API (#7359)Alex Ozdemir
2021-10-15Fix issues related to proofs of lemmas with duplicate conclusions in strings ...Andrew Reynolds
2021-10-14Add regressions for fixed issues (#7369)Andrew Reynolds
2021-10-14Fix (get-info :authors) (#7373)Gereon Kremer
2021-10-14Improve ManagedStreams (#7367)Gereon Kremer
2021-10-14Add regression for fixed issue (#7365)Andrew Reynolds
2021-10-14Improve parser for tuple select (#7364)Andrew Reynolds
2021-10-14Split entailment check from term database (#7342)Andrew Reynolds
2021-10-14Also test older cmake versions (#7347)Gereon Kremer
2021-10-14Fix quantifiers variable elimination for parametric datatypes (#7358)Andrew Reynolds
2021-10-14Fix GLPK linking (#7357)Gereon Kremer
2021-10-14Add core LFSC signatures (#7289)Andrew Reynolds
2021-10-13Eliminate uses of rewrite from datatypes theory (#7354)Andrew Reynolds
2021-10-13Make (proof) equality engine use Env (#7336)Andrew Reynolds
2021-10-12Simplify refinement in sygus solver (#7343)Andrew Reynolds
2021-10-12Eliminate calls to currentResourceManager (#7350)Andrew Reynolds
2021-10-12cmake: Fix git info if build directory is outside of source tree. (#7351)Mathias Preiner
2021-10-12Clean up occurrences of SmtEngine in comments. (#7349)Aina Niemetz
2021-10-12Get rid of unused member d_smtStats in ExpandDefs. (#7346)Aina Niemetz
2021-10-12Rename SmtEngineState to SolverEngineState. (#7344)Aina Niemetz
2021-10-12Fix glpk, add antlr.so (#7341)Gereon Kremer
2021-10-12Provide a non-traversal interface to term formula removal (#7328)Andrew Reynolds
2021-10-12Minor cleaning of instantiation utilities (#7334)Andrew Reynolds
2021-10-12Simplify skolemization in sygus solver (#7331)Andrew Reynolds
2021-10-12fix deprecation of std::iterator (#7332)Ouyancheng
2021-10-11Start post-release for 0.0.2Mathias Preiner
2021-10-11Bump version to 0.0.2Mathias Preiner
2021-10-11Fix release action.Mathias Preiner
2021-10-11Rename SmtEngineStatistics to SolverEngineStatistics. (#7339)Aina Niemetz
2021-10-11Start post-release for 0.0.1Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback