projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
TheoryIds for UF theory. (#5901)
[cvc5.git] / src /
2021-02-17 Gereon KremerTheoryIds for UF theory. (#5901) tree | commitdiff
2021-02-17 Gereon KremerAdd InferenceIds for theory of arrays (#5910) tree | commitdiff
2021-02-17 Gereon KremerAdd InferenceId to buffered inference manager (#5911) tree | commitdiff
2021-02-17 Gereon KremerAdd new IntegralHistogramStat (#5898) tree | commitdiff
2021-02-17 Mathias PreinerAdd bit-level propagation support to BV bitblast solver... tree | commitdiff
2021-02-15 Gereon KremerRemove now obsolete sendLemmas and inferences stat... tree | commitdiff
2021-02-13 Andrew ReynoldsMoving methods from quantifiers engine to quantifiers... tree | commitdiff
2021-02-13 Mathias PreinerProperly set up equality engine for BV bitblast solver... tree | commitdiff
2021-02-12 Andrew ReynoldsSimplify and fix decision engine's handling of skolem... tree | commitdiff
2021-02-12 Andrew Reynolds(proof-new) Option to not automatically consider symmet... tree | commitdiff
2021-02-11 Gereon KremerMake most methods of TheoryInferenceManager expect... tree | commitdiff
2021-02-11 Gereon KremerAdd InferenceId member to TheoryInference, adapt all... tree | commitdiff
2021-02-11 Haniel Barbosa[proof-new] Adding a proof-producing ensure literal... tree | commitdiff
2021-02-11 Gereon KremerMerge InferenceIds into one enum (#5892) tree | commitdiff
2021-02-11 Andrew ReynoldsFix spurious assertion failure in regexp normalization... tree | commitdiff
2021-02-11 Andrew ReynoldsSimplify interface for preprocessor (#5890) tree | commitdiff
2021-02-10 Andrew ReynoldsRefactor term registration visitors (#5875) tree | commitdiff
2021-02-10 Andrew ReynoldsFix open proof for factoring lemma (#5885) tree | commitdiff
2021-02-10 Andrew ReynoldsSimplify method for inferring proxy lemmas in strings... tree | commitdiff
2021-02-10 Andrew ReynoldsRemove track instantiations infrastructure (#5883) tree | commitdiff
2021-02-10 Andrew ReynoldsOptimize get skolems method (#5876) tree | commitdiff
2021-02-10 Andrew ReynoldsDo not traverse quantifiers in term formula removal... tree | commitdiff
2021-02-09 Mathias Preinercmake: Make Python3 default and improve toml error... tree | commitdiff
2021-02-09 Andrew ReynoldsEliminating dependencies from inst utils (#5882) tree | commitdiff
2021-02-09 Andrew ReynoldsMake term database optionally SAT-context-dependent... tree | commitdiff
2021-02-09 Haniel Barbosa[quantifiers] Fix prenex computation (#5879) tree | commitdiff
2021-02-08 Andrew ReynoldsUse quantifiers inference manager for lemma management... tree | commitdiff
2021-02-08 Andrew ReynoldsFix disequality between seq.unit terms (#5880) tree | commitdiff
2021-02-08 Haniel BarbosaFix dumping of assertions for monolithic preprocessing... tree | commitdiff
2021-02-08 Andrew ReynoldsRemove support for inst closure (#5874) tree | commitdiff
2021-02-08 Andrew ReynoldsAvoid spurious traversal of terms during preregistratio... tree | commitdiff
2021-02-06 Andrew ReynoldsDo not combine theories if theory engine needs check... tree | commitdiff
2021-02-05 Andrew ReynoldsMinor cleaning of quantifiers engine (#5858) tree | commitdiff
2021-02-05 Andrew ReynoldsMiscellaneous cleaning in theory engine (#5854) tree | commitdiff
2021-02-04 yoni206Adding an option to optimize polite combination for... tree | commitdiff
2021-02-04 Andrew ReynoldsIntroduce quantifiers registry utility (#5829) tree | commitdiff
2021-02-04 Andrew ReynoldsEliminate equality query dependence on quantifiers... tree | commitdiff
2021-02-04 Haniel Barbosa[proof-new] Catch trivial cycles in SAT proof generatio... tree | commitdiff
2021-02-03 Mathias PreinerAdd BV solver bitblast. (#5851) tree | commitdiff
2021-02-03 Haniel Barbosa[proof-new] Fix MACRO_RESOLUTION expansion for singleto... tree | commitdiff
2021-02-02 Andrew Reynolds(proof-new) Miscellaneous fixes and regressions (#5841) tree | commitdiff
2021-02-02 Andrew Reynolds(proof-new) Refactor theory preprocessing (#5835) tree | commitdiff
2021-02-02 Andrew ReynoldsCleanup some includes (#5847) tree | commitdiff
2021-02-02 Andrew ReynoldsImprovements for NL traces (#5846) tree | commitdiff
2021-02-02 Haniel Barbosa[proof-new] Fix bug in expansion of MACRO_RESOLUTION... tree | commitdiff
2021-02-01 Andrew ReynoldsEliminate PREPROCESS lemma property (#5827) tree | commitdiff
2021-02-01 Andrew ReynoldsSimplify alpha equivalence module (#5839) tree | commitdiff
2021-02-01 Abdalrhman MohamedAvoid calling the printers while converting sexpr to... tree | commitdiff
2021-02-01 mudathirmahgoubFix BagsRewriter::rewriteUnionDisjoint (#5840) tree | commitdiff
2021-01-30 Andrew ReynoldsFix unguarded call to get representative (#5838) tree | commitdiff
2021-01-29 Haniel Barbosa[proof-new] Connecting new unsat cores (#5834) tree | commitdiff
2021-01-29 mudathirmahgoubAdd bag inferences for operators: intersection, duplica... tree | commitdiff
2021-01-29 Andrew Reynolds(proof-new) Distinguish pre vs post rewrites in term... tree | commitdiff
2021-01-28 Andrew ReynoldsReorganize calls to quantifiers engine from SmtEngine... tree | commitdiff
2021-01-28 mudathirmahgoubRemove regex header from cvc4cpp.cpp (#5826) tree | commitdiff
2021-01-28 Andrew ReynoldsSimplify lemma interface (#5819) tree | commitdiff
2021-01-28 Andrew ReynoldsUse standard equality engine information in quantifiers... tree | commitdiff
2021-01-28 Andrew ReynoldsAlways theory-preprocess lemmas (#5817) tree | commitdiff
2021-01-27 Andrew ReynoldsAdd option for whether to filter candidate rewrite... tree | commitdiff
2021-01-27 Andrew ReynoldsSplit pattern term selector from trigger (#5811) tree | commitdiff
2021-01-27 Andrew Reynolds(proof-new) Improvements to quantifiers engine and... tree | commitdiff
2021-01-27 Alex OzdemirThread proofs through arith channels & similar (#5818) tree | commitdiff
2021-01-27 Andrew ReynoldsUse term canonizer utility locally in quantifiers ... tree | commitdiff
2021-01-27 Andrew ReynoldsUse standard conflict mechanism in quantifiers state... tree | commitdiff
2021-01-26 Andrew ReynoldsIntroduce quantifiers inference manager (#5821) tree | commitdiff
2021-01-26 Andrew ReynoldsRemove deprecated quantifiers modules (#5820) tree | commitdiff
2021-01-26 Andrew ReynoldsRefactor quantifiers engine initialization (#5813) tree | commitdiff
2021-01-26 Haniel BarbosaReestablishing support for define-sort (#5810) tree | commitdiff
2021-01-26 Alex OzdemirAdd proofs to TheoryArithPrivate::propagate (#5812) tree | commitdiff
2021-01-25 mudathirmahgoubRefactor bags::SolverState (#5783) tree | commitdiff
2021-01-25 Andrew ReynoldsEnsure uses of ground terms in triggers are preprocesse... tree | commitdiff
2021-01-25 Andrew ReynoldsSplit inst match generator into multiple files (#5805) tree | commitdiff
2021-01-25 Andrew ReynoldsSplit E-matching strategies to own files (#5807) tree | commitdiff
2021-01-25 mudathirmahgoubrename InferInfo::d_newSkolem to InferInfo::d_skolems... tree | commitdiff
2021-01-24 Andrew Reynolds Initial cleaning of e-matching instantiation strategy... tree | commitdiff
2021-01-24 Andrew ReynoldsInitial cleaning of triggers (#5795) tree | commitdiff
2021-01-24 Andrew ReynoldsInitial cleaning of inst match generator (#5794) tree | commitdiff
2021-01-24 Andrew Reynolds(proof-new) Instantiation list utility (#5768) tree | commitdiff
2021-01-24 Andrew ReynoldsAdd interface for getting preprocessed term (#5798) tree | commitdiff
2021-01-22 Haniel Barbosa[proof-new] Expanding MACRO_RESOLUTION in post-processi... tree | commitdiff
2021-01-21 Andrew ReynoldsAdd div, mod, abs in non-strict parsing mode (#5793) tree | commitdiff
2021-01-21 Alex Ozdemirarith: Proofs for Diophantine cuts (#5792) tree | commitdiff
2021-01-20 Andrew ReynoldsRefactoring the single invocation solver (#5706) tree | commitdiff
2021-01-20 Andrew ReynoldsFix type issues with relevant domain computation (... tree | commitdiff
2021-01-20 Andrew ReynoldsFix corner case of wrongly applied selector as trigger... tree | commitdiff
2021-01-20 Andrew ReynoldsDo not track processed in remove term formulas loop... tree | commitdiff
2021-01-20 Aina NiemetzSMT2 parser: Do not add non-linear symbols for linear... tree | commitdiff
2021-01-20 Andrew ReynoldsUse arbitrary ground term assignment for sorts where... tree | commitdiff
2021-01-19 Alex OzdemirImplement proofs for arith BRAB lemmas (#5784) tree | commitdiff
2021-01-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass... tree | commitdiff
2021-01-14 Andrew ReynoldsUpdates to theory preprocess equality (#5776) tree | commitdiff
2021-01-13 Andrew ReynoldsSplit eager solver from strings solver state (#5775) tree | commitdiff
2021-01-13 Andrew ReynoldsDo not call ppRewrite on Boolean equalities (#5762) tree | commitdiff
2021-01-12 yoni206Foreign theory rewrite option (#5763) tree | commitdiff
2021-01-11 Andrew ReynoldsMerge theory registrar and theory proxy (#5758) tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-11 Andrew ReynoldsRemove extended rewrite for arithmetic (#5760) tree | commitdiff
2021-01-09 yoni206Strings arith checks preprocessing pass: step 2 (#5750) tree | commitdiff
2021-01-09 mudathirmahgoubFix issue 5513 (#5757) tree | commitdiff
2021-01-08 mudathirmahgoubRename getAntecedent to getPremises (#5754) tree | commitdiff
next