projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Remove obsolete gcc check. (#6041)
[cvc5.git] / src /
2021-03-03 Andrew Reynolds(proof-new) Simplifications to arithmetic operator... tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-03 Abdalrhman MohamedRemove uses of SExpr class. (#6035) tree | commitdiff
2021-03-03 mudathirmahgoubAdd tuple projection operator (#5904) tree | commitdiff
2021-03-02 Mathias PreinerRemove non-ASCII characters from source files. (#6039) tree | commitdiff
2021-03-02 Gereon KremerImprove handling of utf8 encoded inputs (#5694) tree | commitdiff
2021-03-02 Mathias PreinerAdd aarch64 (ARM64) cross-compile support. (#6033) tree | commitdiff
2021-03-02 Mathias PreinerFix nightly errors. (#6034) tree | commitdiff
2021-03-02 Andrew ReynoldsIntroduce quantifiers term registry (#5983) tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-03-01 Gereon KremerRefactor collection of debug and trace tags (#5996) tree | commitdiff
2021-02-27 Aina Niemetzgoogle test: theory: Migrate theory_white. (#6006) tree | commitdiff
2021-02-26 Haniel BarbosaSome formatting and better tracing in prop engine ... tree | commitdiff
2021-02-26 Andrew ReynoldsMinor improvement and fix to smt2 printer (#6009) tree | commitdiff
2021-02-26 Andrew ReynoldsOptionally permit creation of non-flat function types... tree | commitdiff
2021-02-26 Gereon KremerStore Node instead of TNode (#5993) tree | commitdiff
2021-02-26 Andrew Reynolds(proof-new) Fix regular expression unfolding under... tree | commitdiff
2021-02-25 Gereon KremerMove (optional) rewrite from TrustSubstitutionMap to... tree | commitdiff
2021-02-25 yoni206Datatypes lemmas: share only external types (#5997) tree | commitdiff
2021-02-25 Mathias PreinerEnable -Werror. (#5969) tree | commitdiff
2021-02-24 Gereon KremerEnsure static-learning adds rewritten assertions. ... tree | commitdiff
2021-02-24 Gereon Kremer(proof-new) Add proofs for CAD solver (#5981) tree | commitdiff
2021-02-24 Andrew ReynoldsAdd state and inference manager to inst match generator... tree | commitdiff
2021-02-24 Andrew ReynoldsAdd interface to TheoryState for sort inference and... tree | commitdiff
2021-02-23 Mathias PreinerSwitch to C++17. (#5959) tree | commitdiff
2021-02-23 Gereon KremerAdd proof for mult sign lemma (#5966) tree | commitdiff
2021-02-23 Haniel Barbosa[proof-new] Fix dangling pointer in SAT proof generatio... tree | commitdiff
2021-02-23 Gereon KremerAdd proof for monomial bounds check (#5965) tree | commitdiff
2021-02-23 Gereon Kremer(proof-new) Add proof generator for CAD solver (#5964) tree | commitdiff
2021-02-23 Haniel Barbosa[proof-new] Fix handling of removable clauses in proof... tree | commitdiff
2021-02-23 Gereon KremerAdd trans secant proofs. (#5957) tree | commitdiff
2021-02-23 Andrew ReynoldsExplanation of failure for instantiate, use in enumerat... tree | commitdiff
2021-02-22 Andrew ReynoldsEliminate raw use of output channel and valuation in... tree | commitdiff
2021-02-22 Andrew ReynoldsMove quantifiers attributes to quantifiers registry... tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Change proof-new option to proof (#5955) tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add proofs for exponential functions (... tree | commitdiff
2021-02-22 Andrew ReynoldsRequire length-in-conclusion form for strings inference... tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Option to automatically add SYMM steps... tree | commitdiff
2021-02-22 Haniel Barbosa[proof-new] Optionally print conclusion in the AST... tree | commitdiff
2021-02-22 Gereon KremerAdd the LazyTreeProofGenerator. (#5948) tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDIC... tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add proofs for sine lemmas in the transcend... tree | commitdiff
2021-02-22 Gereon KremerCleanup in transcendental solver, add ApproximationBoun... tree | commitdiff
2021-02-22 Gereon Kremeradd pruneRedundantIntervals (#5950) tree | commitdiff
2021-02-22 Andrew ReynoldsFix datatypes inference manager when proofs are enabled... tree | commitdiff
2021-02-19 Andrew ReynoldsSimplify interface to instantiate (#5926) tree | commitdiff
2021-02-19 Andrew ReynoldsFill in missing inference ids in datatypes theory ... tree | commitdiff
2021-02-19 Andrew ReynoldsRefactoring theory inference process (#5920) tree | commitdiff
2021-02-19 Andrew ReynoldsFix rewrite for contains over replace (#5924) tree | commitdiff
2021-02-19 Andrew ReynoldsRemove string stat for inferences (#5932) tree | commitdiff
2021-02-19 Gereon KremerCleanup of inferences in arithmetic theory (#5927) tree | commitdiff
2021-02-18 Gereon KremerAdd statistic for InferenceId to TheoryInferenceManager... tree | commitdiff
2021-02-18 Gereon KremerAdd InferenceIds for sets theory. (#5900) tree | commitdiff
2021-02-18 Gereon KremerNew InferenceIds for BV theory (#5909) tree | commitdiff
2021-02-18 Andrew ReynoldsDocument UF inferences (#5917) tree | commitdiff
2021-02-18 Andrew ReynoldsEliminate non-static members in term util (#5919) tree | commitdiff
2021-02-18 Andrew ReynoldsMove first order model for full model check to own... tree | commitdiff
2021-02-17 Andrew ReynoldsMove methods from term util to quantifiers registry... tree | commitdiff
2021-02-17 Andrew ReynoldsCompute fact or lemma in datatypes prior to buffering... tree | commitdiff
2021-02-17 Gereon KremerUse InferenceId in sep theory. (#5912) tree | commitdiff
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
next