projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
TheoryIds for UF theory. (#5901)
[cvc5.git] / test /
2021-02-17 Gereon KremerAdd new IntegralHistogramStat (#5898) tree | commitdiff
2021-02-16 Aina Niemetzgoogle test: parser: Migrate parser_builder_black.... tree | commitdiff
2021-02-11 Aina Niemetzgoogle test: parser: Migrate parser_black. (#5886) tree | commitdiff
2021-02-11 Andrew ReynoldsFix spurious assertion failure in regexp normalization... 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-09 Aina Niemetzgoogle test: expr: Migrate node_manager_black. (#5857) tree | commitdiff
2021-02-09 Aina Niemetzgoogle test: main: Migrate interactive_shell_black... tree | commitdiff
2021-02-09 Aina Niemetzgoogle test: expr: Migrate type_cardinality_black.... tree | commitdiff
2021-02-09 Aina Niemetzgoogle test: expr: Migrate node_self_iterator_black... tree | commitdiff
2021-02-09 Haniel Barbosa[quantifiers] Fix prenex computation (#5879) tree | commitdiff
2021-02-09 Aina Niemetzgoogle test: expr: Migrate type_node_white. (#5872) tree | commitdiff
2021-02-08 Andrew ReynoldsFix disequality between seq.unit terms (#5880) tree | commitdiff
2021-02-08 Aina Niemetzgoogle test: expr: Migrate node_white. (#5869) tree | commitdiff
2021-02-08 Aina NiemetzUse consistent names for fixtures in unit tests. (... tree | commitdiff
2021-02-08 Aina Niemetzgoogle test: expr: Migrate node_traversal_black. (... tree | commitdiff
2021-02-06 Andrew ReynoldsDo not combine theories if theory engine needs check... tree | commitdiff
2021-02-05 Aina Niemetzgoogle test: expr: Migrate symbol_table_black. (#5870) tree | commitdiff
2021-02-05 Aina Niemetzgoogle test: expr: Migrate node_manager_white. (#5864) tree | commitdiff
2021-02-05 Aina NiemetzRemove obsolete include from node_black unit test.... tree | commitdiff
2021-02-05 Aina Niemetzgoogle test: expr: Migrate node_builder_black. (#5855) tree | commitdiff
2021-02-04 Haniel Barbosa[proof-new] Catch trivial cycles in SAT proof generatio... 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 ReynoldsRemove quantifiers regression from decision folder... tree | commitdiff
2021-02-02 Haniel Barbosa[proof-new] Fix bug in expansion of MACRO_RESOLUTION... 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-28 mudathirmahgoubRemove regex header from cvc4cpp.cpp (#5826) tree | commitdiff
2021-01-28 Andrew ReynoldsSimplify lemma interface (#5819) tree | commitdiff
2021-01-28 Andrew ReynoldsAlways theory-preprocess lemmas (#5817) tree | commitdiff
2021-01-27 Andrew Reynolds(proof-new) Improvements to quantifiers engine and... tree | commitdiff
2021-01-26 Andrew ReynoldsRemove deprecated quantifiers modules (#5820) tree | commitdiff
2021-01-26 Haniel BarbosaReestablishing support for define-sort (#5810) 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-21 Andrew ReynoldsAdd div, mod, abs in non-strict parsing mode (#5793) 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-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass... tree | commitdiff
2021-01-13 Ying ShengAdd unit test for api getInterpolant() -- issue #5593... tree | commitdiff
2021-01-13 Andrew ReynoldsDo not call ppRewrite on Boolean equalities (#5762) tree | commitdiff
2021-01-12 Aina Niemetzgoogle test: expr: Migrate node_black. (#5764) tree | commitdiff
2021-01-12 Aina Niemetzgoogle test: Use ASSERT_* instead of EXPECT_*. (#5765) 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-08 mudathirmahgoubAdd bags inference generator (#5731) tree | commitdiff
2021-01-07 Gereon KremerMake sure polynomials are properly factorized in nl... tree | commitdiff
2021-01-05 yoni206Adding str.len to triggers (#5746) tree | commitdiff
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) tree | commitdiff
2020-12-22 Andrew ReynoldsMove slow regression to regress3 (#5715) tree | commitdiff
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... tree | commitdiff
2020-12-22 Andrew ReynoldsRemove preregister instantiation heuristic (#5713) tree | commitdiff
2020-12-21 Haniel BarbosaHave unsat core regression agnostic to number of assert... tree | commitdiff
2020-12-21 Andrew ReynoldsEliminate recursion from the internals of term formula... tree | commitdiff
2020-12-18 Alex OzdemirBugfix: proofs for props of non-normal arith lits ... tree | commitdiff
2020-12-17 Andrew ReynoldsSimplify and fix check models (#5685) tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify preprocessing (#5647) tree | commitdiff
2020-12-16 Andrew ReynoldsMark quantifier instantiations as needs justify (#5684) tree | commitdiff
2020-12-15 Andrew ReynoldsRemove bv divide by zero option (#5672) tree | commitdiff
2020-12-15 Gereon KremerAdd getters to retrieve constants from api::Term (... tree | commitdiff
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) tree | commitdiff
2020-12-14 Andrew ReynoldsFix SAT-context dependent issue in strings preregistrat... tree | commitdiff
2020-12-11 yoni206bv-to-int: new tests from an issue (#5654) tree | commitdiff
2020-12-11 Andrew ReynoldsFix length assumption for deq norm emp rule (#5623) tree | commitdiff
2020-12-10 Gereon KremerRefactor KindMap (#5646) tree | commitdiff
2020-12-10 Aina Niemetzgoogle test: expr: Migrate node_algorithm_black. (... tree | commitdiff
2020-12-10 Andrew ReynoldsRefactor regressions (#5639) tree | commitdiff
2020-12-10 Aina Niemetzgoogle test: expr: Migrate kind_black. (#5634) tree | commitdiff
2020-12-09 Aina Niemetzgoogle test: expr: Migrate kind_map_black. (#5640) tree | commitdiff
2020-12-09 Aina Niemetzgoogle test: expr: Migrate attribute_white. (#5632) tree | commitdiff
2020-12-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline... tree | commitdiff
2020-12-09 Andrew ReynoldsRemove obsolete regressions (#5633) tree | commitdiff
2020-12-09 Aina Niemetzgoogle test: context: Migrate context_white. (#5630) tree | commitdiff
2020-12-09 Aina NiemetzDelete obsolete unit tests for Expr and ExprManager... tree | commitdiff
2020-12-09 Andrew ReynoldsEnsure CEGQI is applied for parametric datatypes when... tree | commitdiff
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_mm_black. (#5592) tree | commitdiff
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_black. (#5587) tree | commitdiff
2020-12-08 Gereon KremerAdd regression from #1978. (#5552) tree | commitdiff
2020-12-08 Abdalrhman MohamedFix a bug with synth-fun printer (#5512) tree | commitdiff
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem... tree | commitdiff
2020-12-08 Andrew ReynoldsMake term indices in the strings base solver aware... tree | commitdiff
2020-12-08 Andrew ReynoldsProper implementation of expand definitions for sequenc... tree | commitdiff
2020-12-08 Andrew ReynoldsFix collect model values for sequences of sequences... tree | commitdiff
2020-12-08 Mathias PreinerDisable algebraic BV subtheory by default and make... tree | commitdiff
2020-12-07 Andrew ReynoldsFix and reenable fact vs lemma optimization in datatype... tree | commitdiff
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) tree | commitdiff
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier... tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-07 Gereon KremerAdd regression from #4927 (#5556) tree | commitdiff
2020-12-04 Aina Niemetzgoogle test: expr: Migrate attribute_black. (#5598) tree | commitdiff
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdo_black. (#5586) tree | commitdiff
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdmap_white. (#5585) tree | commitdiff
next