projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fix another rewrite involving iand (#8054)
[cvc5.git] / src / theory /
2022-02-05 Andrew ReynoldsFix another rewrite involving iand (#8054) tree | commitdiff
2022-02-04 Andres Noetzli[Rewriter] Always rewrite again when kind changes ... tree | commitdiff
2022-02-04 Aina NiemetzFP: Rename tester kinds. (#8037) tree | commitdiff
2022-02-03 Andrew ReynoldsSimplify handling of disequalities in strings (#8047) tree | commitdiff
2022-02-03 Gereon KremerImprove theory combination over real algebraic models... tree | commitdiff
2022-02-03 Andrew ReynoldsEliminate even more static uses of rewrite (#8044) tree | commitdiff
2022-02-03 Gereon KremerReplace a some more static options (#8042) tree | commitdiff
2022-02-03 Andrew ReynoldsEliminate more static uses of rewrite (#8040) tree | commitdiff
2022-02-03 mudathirmahgoubAdd table.product operator (#8020) tree | commitdiff
2022-02-03 Gereon KremerAdd node utils for the arithmetic rewriter (#8012) tree | commitdiff
2022-02-03 Andres NoetzliSend all `nth` terms to the core array solver (#7990) tree | commitdiff
2022-02-03 Aina NiemetzRename kind PLUS -> ADD. (#8036) tree | commitdiff
2022-02-02 Andrew ReynoldsFix rewrite for eliminating constant factors of PI... tree | commitdiff
2022-02-02 Aina NiemetzRename kinds MINUS -> SUB and UMINUS -> NEG. (#8035) tree | commitdiff
2022-02-02 Andrew ReynoldsFix invalid rewrite involving iand (#8026) tree | commitdiff
2022-02-02 Gereon KremerAdd additional check to avoid cyclic substitution ... tree | commitdiff
2022-02-02 mudathirmahgoubUpdate datatypes.rst (#8009) tree | commitdiff
2022-02-02 Andrew ReynoldsRemove more static calls to rewrite (#8025) tree | commitdiff
2022-02-02 Andrew ReynoldsExtend proof step buffer to optionally ensure unique... tree | commitdiff
2022-02-01 Andres Noetzli[BV] Fix strategy for `RewriteExtract` (#8011) tree | commitdiff
2022-02-01 Andres Noetzli[BV] Fix order of rewrites for `concat` (#8010) tree | commitdiff
2022-02-01 Gereon KremerAdd new ordering utility (#8008) tree | commitdiff
2022-02-01 Andrew ReynoldsAdd variant of get-difficulty for full effort lemmas... tree | commitdiff
2022-02-01 Andres Noetzli[Arrays] Fix response for `store` chains (#8015) tree | commitdiff
2022-02-01 mudathirmahgoubAdd bag.filter operator (#8006) tree | commitdiff
2022-02-01 Gereon KremerConsider RANs in variable ordering (#7964) tree | commitdiff
2022-01-31 Gereon KremerAdd utilities for flattening nodes (#7961) tree | commitdiff
2022-01-31 Andres NoetzliFix memory leak in quantifier info (#8005) tree | commitdiff
2022-01-28 Bruno DutertreTry a bit harder on the EQ_NCTN rewrite rule (#7998) tree | commitdiff
2022-01-26 Andrew ReynoldsInitial refactoring of conflict-based instantiation... tree | commitdiff
2022-01-26 mudathirmahgoubAdd Card solver to bags (#7986) tree | commitdiff
2022-01-26 Andrew ReynoldsMore fixes and improvements for query generator (#7988) tree | commitdiff
2022-01-25 Andres NoetzliSend `nth(unit(...), ...)` terms to array solver (... tree | commitdiff
2022-01-25 Andrew ReynoldsFixes and improvements to sygus satisfiable query gener... tree | commitdiff
2022-01-25 Andres Noetzli[Strings] Avoid trivial explanation (#7982) tree | commitdiff
2022-01-25 Andres Noetzli[Strings] Remove redundant call to rewriter (#7978) tree | commitdiff
2022-01-25 Andres Noetzli[FP] Fix unused variable warning (#7977) tree | commitdiff
2022-01-24 Gereon KremerUse proper RAN nodes for nl model (#7939) tree | commitdiff
2022-01-24 Gereon KremerRefactor how arith rewriting checks for mult-by-zero... tree | commitdiff
2022-01-21 Andrew ReynoldsRef count nodes in trigger trie (#7972) tree | commitdiff
2022-01-21 Andrew ReynoldsFix trivial explantions in sequences array solver ... tree | commitdiff
2022-01-20 Andres NoetzliFix `Nth-Update` rule, add `Update-Bound` rule (#7968) tree | commitdiff
2022-01-20 Andrew ReynoldsFix proofs for trivial cases of datatypes tester merge... tree | commitdiff
2022-01-20 Gereon KremerRefactor abs rewriting (#7935) tree | commitdiff
2022-01-19 Andres NoetzliAdd rewrites for `seq.update`/`seq.nth` (#7966) tree | commitdiff
2022-01-19 Gereon KremerFix a subtle issue with double negations in coverings... tree | commitdiff
2022-01-19 Gereon KremerMake tracing for arithmetic rewriter more consistent... tree | commitdiff
2022-01-18 Andrew ReynoldsDistinguish purification types for strings proof recons... tree | commitdiff
2022-01-17 Andrew ReynoldsRefactor options related to rewriting and symmetry... tree | commitdiff
2022-01-17 Andres Noetzli[Strings] Fix rewriter for `re.loop` (#7956) tree | commitdiff
2022-01-15 Andrew ReynoldsAdd inverse inference for update-over-concat (#7954) tree | commitdiff
2022-01-14 Andrew ReynoldsImprove names for sygus enumeration option (#7945) tree | commitdiff
2022-01-14 Andrew ReynoldsClean enumerative instantiation options (#7947) tree | commitdiff
2022-01-14 Andrew ReynoldsImplement -o subs to show learned top-level substitutio... tree | commitdiff
2022-01-14 Gereon KremerPreprare central model building for RANs (#7951) tree | commitdiff
2022-01-14 Gereon Kremerrefactor div rewriter, add support for ran (#7941) tree | commitdiff
2022-01-14 Gereon KremerAdd operator<<(RewriteStatus) (#7952) tree | commitdiff
2022-01-14 Andrew ReynoldsWeaken assertion in relevance manager (#7943) tree | commitdiff
2022-01-14 Gereon KremerRefactor arithmetic pre-rewriter for multiplication... tree | commitdiff
2022-01-14 Gereon KremerAdd support for RANs in rewriter for `MULT` (#7940) tree | commitdiff
2022-01-14 Gereon KremerAdd RAN support in UMINUS rewriter (#7933) tree | commitdiff
2022-01-13 Gereon KremerAdd arithmetic rewriter for RAN (#7929) tree | commitdiff
2022-01-13 Andrew ReynoldsFix bug in evaluator for division by zero (#7942) tree | commitdiff
2022-01-13 Andres NoetzliUnify abstract values and uninterpreted constants ... tree | commitdiff
2022-01-13 Gereon KremerRefactor post rewriter for addition (#7931) tree | commitdiff
2022-01-12 Andrew ReynoldsAdd -o learned-lits to output learned literals (#7934) tree | commitdiff
2022-01-12 Gereon KremerRefactor atom rewriting to be RAN-aware (#7928) tree | commitdiff
2022-01-12 Gereon KremerRefactor rewriteMinus (#7932) tree | commitdiff
2022-01-12 Andrew ReynoldsEnsure configuration of shared selectors is consistent... tree | commitdiff
2022-01-12 Gereon KremerAdd mkRealAlgebraicNumber (#7923) tree | commitdiff
2022-01-12 Andrew ReynoldsAlways use partial function for sqrt (#7926) tree | commitdiff
2022-01-11 Gereon KremerAdds a kind to hold RealAlgebraicNumber constants ... tree | commitdiff
2022-01-11 Abdalrhman MohamedDisable filtering of shapes in sygus-rcons pool. (... tree | commitdiff
2022-01-11 Gereon KremerRemove static accesses to options (#7913) tree | commitdiff
2022-01-11 Andrew ReynoldsTighten policy for unsat cores in sygus core connective... tree | commitdiff
2022-01-06 Andrew ReynoldsMake alpha equivalence user context dependent (#7889) tree | commitdiff
2022-01-06 Gereon KremerImprove theory combination in the presence of real... tree | commitdiff
2022-01-06 Andrew ReynoldsFix non-idempotent rewrite in arrays (#7887) tree | commitdiff
2022-01-06 Andrew ReynoldsMinor cleaning of non-clausal simplification (#7886) tree | commitdiff
2022-01-05 Andrew ReynoldsTrack input list for atoms in difficulty manager (... tree | commitdiff
2022-01-04 Andrew ReynoldsFix proofs for datatype purify (#7841) tree | commitdiff
2022-01-04 Andrew ReynoldsAdd utility expr::isBooleanConnective (#7869) tree | commitdiff
2022-01-04 Andrew ReynoldsRemove unused shutdown infrastructure (#7872) tree | commitdiff
2022-01-04 Andrew ReynoldsFix int blaster (#7856) tree | commitdiff
2022-01-04 mudathirmahgoubAdd bag.member operator to theory of bags (#7857) tree | commitdiff
2022-01-04 mudathirmahgoubRefactor bag solver (#7770) tree | commitdiff
2022-01-03 Andrew ReynoldsUpdate quantifiers compute elim symbols to be iterative... tree | commitdiff
2022-01-03 Andres Noetzli[BV] Remove non-existent `friend` class (#7864) tree | commitdiff
2021-12-22 Andrew ReynoldsRemove most uses of mkRationalNode (#7854) tree | commitdiff
2021-12-22 Andrew ReynoldsAdd support for incremental + interpolants (#7853) tree | commitdiff
2021-12-21 Andrew ReynoldsEliminate remaining calls to callExtendedRewrite (... tree | commitdiff
2021-12-21 yoni206Rewrite (pow2 x) to (pow 2 x) when x is a constant... tree | commitdiff
2021-12-21 Andrew ReynoldsConnect sequences array solver to strategy in theory... tree | commitdiff
2021-12-20 Andrew ReynoldsEliminating some uses of const rational in arithmetic... tree | commitdiff
2021-12-20 Andrew ReynoldsAllow SyGuS subsolver to be reused in incremental mode... tree | commitdiff
2021-12-20 Andres Noetzli[Sequences/Array Solver] Minor refactoring (#7843) tree | commitdiff
2021-12-17 Andres Noetzli[Strings] Minor fixes/improvements (#7837) tree | commitdiff
2021-12-17 Ying ShengArray-inspired Sequence Solver - Fixing several issues... tree | commitdiff
2021-12-17 Andres NoetzliFix rewrite for `str.update(str.rev(s), n, t))` (#7838) tree | commitdiff
2021-12-17 Gereon KremerFix tracker in SubstitutionMap (#7829) tree | commitdiff
next