cvc5.git
2021-02-24 Aina Niemetzgoogle test: theory: Migrate theory_bags_normal_form_wh...
2021-02-24 Aina Niemetzgoogle test: theory: Migrate logic_info_white. (#5973)
2021-02-24 Aina Niemetzgoogle test: theory: Migrate theory_bags_rewriter_white...
2021-02-24 Aina Niemetzgoogle test: theory: Migrate theory_arith_white. (...
2021-02-24 Aina Niemetzgoogle test: theory: Migrate evaluator_white. (#5972)
2021-02-24 Aina Niemetzgoogle test: prop: Migrate cnf_stream_white. (#5971)
2021-02-24 Andrew ReynoldsAdd state and inference manager to inst match generator...
2021-02-24 Andrew ReynoldsAdd interface to TheoryState for sort inference and...
2021-02-23 Mathias PreinerSwitch to C++17. (#5959)
2021-02-23 Aina Niemetzgoogle test: theory: Migrate regexp_operation_black...
2021-02-23 Aina Niemetzgoogle test: theory: Migrate strings_rewriter_white...
2021-02-23 Gereon KremerAdd proof for mult sign lemma (#5966)
2021-02-23 Haniel Barbosa[proof-new] Fix dangling pointer in SAT proof generatio...
2021-02-23 Gereon KremerAdd proof for monomial bounds check (#5965)
2021-02-23 Gereon Kremer(proof-new) Add proof generator for CAD solver (#5964)
2021-02-23 Haniel Barbosa[proof-new] Fix handling of removable clauses in proof...
2021-02-23 Gereon KremerAdd trans secant proofs. (#5957)
2021-02-23 Andrew ReynoldsExplanation of failure for instantiate, use in enumerat...
2021-02-23 Aina Niemetzgoogle test: preprocessing: Migrate pass_bv_gauss_white...
2021-02-22 Andrew ReynoldsEliminate raw use of output channel and valuation in...
2021-02-22 Andrew ReynoldsMove quantifiers attributes to quantifiers registry...
2021-02-22 Andrew Reynolds(proof-new) Change proof-new option to proof (#5955)
2021-02-22 Gereon Kremer(proof-new) Add proofs for exponential functions (...
2021-02-22 Andrew ReynoldsRequire length-in-conclusion form for strings inference...
2021-02-22 Andrew Reynolds(proof-new) Option to automatically add SYMM steps...
2021-02-22 Haniel Barbosa[proof-new] Optionally print conclusion in the AST...
2021-02-22 Aina Niemetzgoogle test: preprocessing: Migrate pass_foreign_theory...
2021-02-22 Gereon KremerAdd the LazyTreeProofGenerator. (#5948)
2021-02-22 Gereon Kremer(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDIC...
2021-02-22 Gereon Kremer(proof-new) Add proofs for sine lemmas in the transcend...
2021-02-22 Gereon KremerCleanup in transcendental solver, add ApproximationBoun...
2021-02-22 Gereon Kremeradd pruneRedundantIntervals (#5950)
2021-02-22 Andrew ReynoldsFix datatypes inference manager when proofs are enabled...
2021-02-19 Andrew ReynoldsSimplify interface to instantiate (#5926)
2021-02-19 Andrew ReynoldsFill in missing inference ids in datatypes theory ...
2021-02-19 Andrew ReynoldsRefactoring theory inference process (#5920)
2021-02-19 Andrew ReynoldsFix rewrite for contains over replace (#5924)
2021-02-19 Andrew ReynoldsRemove string stat for inferences (#5932)
2021-02-19 Gereon KremerCleanup of inferences in arithmetic theory (#5927)
2021-02-19 Aina NiemetzAdd Gereon to AUTHORS list. (#5930)
2021-02-18 Gereon KremerAdd statistic for InferenceId to TheoryInferenceManager...
2021-02-18 Gereon KremerAdd InferenceIds for sets theory. (#5900)
2021-02-18 Gereon KremerNew InferenceIds for BV theory (#5909)
2021-02-18 Andrew ReynoldsDocument UF inferences (#5917)
2021-02-18 Andrew ReynoldsEliminate non-static members in term util (#5919)
2021-02-18 Andrew ReynoldsMove first order model for full model check to own...
2021-02-17 Andrew ReynoldsMove methods from term util to quantifiers registry...
2021-02-17 Andrew ReynoldsCompute fact or lemma in datatypes prior to buffering...
2021-02-17 Gereon KremerUse InferenceId in sep theory. (#5912)
2021-02-17 Gereon KremerTheoryIds for UF theory. (#5901)
2021-02-17 Gereon KremerAdd InferenceIds for theory of arrays (#5910)
2021-02-17 Gereon KremerAdd InferenceId to buffered inference manager (#5911)
2021-02-17 Gereon KremerAdd new IntegralHistogramStat (#5898)
2021-02-17 Mathias PreinerAdd bit-level propagation support to BV bitblast solver...
2021-02-16 Aina Niemetzgoogle test: parser: Migrate parser_builder_black....
2021-02-15 Gereon KremerRemove now obsolete sendLemmas and inferences stat...
2021-02-13 Andrew ReynoldsMoving methods from quantifiers engine to quantifiers...
2021-02-13 Mathias PreinerProperly set up equality engine for BV bitblast solver...
2021-02-12 Andrew ReynoldsSimplify and fix decision engine's handling of skolem...
2021-02-12 Andrew Reynolds(proof-new) Option to not automatically consider symmet...
2021-02-11 Aina Niemetzgoogle test: parser: Migrate parser_black. (#5886)
2021-02-11 Gereon KremerMake most methods of TheoryInferenceManager expect...
2021-02-11 Gereon KremerAdd InferenceId member to TheoryInference, adapt all...
2021-02-11 Haniel Barbosa[proof-new] Adding a proof-producing ensure literal...
2021-02-11 Gereon KremerMerge InferenceIds into one enum (#5892)
2021-02-11 Andrew ReynoldsFix spurious assertion failure in regexp normalization...
2021-02-11 Andrew ReynoldsSimplify interface for preprocessor (#5890)
2021-02-10 Andrew ReynoldsRefactor term registration visitors (#5875)
2021-02-10 Andrew ReynoldsFix open proof for factoring lemma (#5885)
2021-02-10 Andrew ReynoldsSimplify method for inferring proxy lemmas in strings...
2021-02-10 Andrew ReynoldsRemove track instantiations infrastructure (#5883)
2021-02-10 Andrew ReynoldsOptimize get skolems method (#5876)
2021-02-10 Andrew ReynoldsDo not traverse quantifiers in term formula removal...
2021-02-09 Mathias Preinercmake: Make Python3 default and improve toml error...
2021-02-09 Andrew ReynoldsEliminating dependencies from inst utils (#5882)
2021-02-09 Andrew ReynoldsMake term database optionally SAT-context-dependent...
2021-02-09 Aina Niemetzgoogle test: expr: Migrate node_manager_black. (#5857)
2021-02-09 Aina Niemetzgoogle test: main: Migrate interactive_shell_black...
2021-02-09 Aina Niemetzgoogle test: expr: Migrate type_cardinality_black....
2021-02-09 Aina Niemetzgoogle test: expr: Migrate node_self_iterator_black...
2021-02-09 Haniel Barbosa[quantifiers] Fix prenex computation (#5879)
2021-02-09 Aina Niemetzgoogle test: expr: Migrate type_node_white. (#5872)
2021-02-08 Andrew ReynoldsUse quantifiers inference manager for lemma management...
2021-02-08 Andrew ReynoldsFix disequality between seq.unit terms (#5880)
2021-02-08 Aina Niemetzgoogle test: expr: Migrate node_white. (#5869)
2021-02-08 Haniel BarbosaFix dumping of assertions for monolithic preprocessing...
2021-02-08 Andrew ReynoldsRemove support for inst closure (#5874)
2021-02-08 Aina NiemetzUse consistent names for fixtures in unit tests. (...
2021-02-08 Aina Niemetzgoogle test: expr: Migrate node_traversal_black. (...
2021-02-08 Andrew ReynoldsAvoid spurious traversal of terms during preregistratio...
2021-02-06 Andrew ReynoldsDo not combine theories if theory engine needs check...
2021-02-05 Aina Niemetzgoogle test: expr: Migrate symbol_table_black. (#5870)
2021-02-05 Andrew ReynoldsMinor cleaning of quantifiers engine (#5858)
2021-02-05 Aina Niemetzgoogle test: expr: Migrate node_manager_white. (#5864)
2021-02-05 Aina NiemetzRemove obsolete include from node_black unit test....
2021-02-05 Aina Niemetzgoogle test: expr: Migrate node_builder_black. (#5855)
2021-02-05 Andrew ReynoldsMiscellaneous cleaning in theory engine (#5854)
2021-02-04 yoni206Adding an option to optimize polite combination for...
2021-02-04 Andrew ReynoldsIntroduce quantifiers registry utility (#5829)
2021-02-04 yoni206Clarifying documentation of `--static-binary` (#5844)
next