projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cmake: Cleanup CMakeLists.txt files, remove SHARED.
[cvc5.git] / src / theory /
2018-09-22 Mathias Preinercmake: Remove unused CMakeLists.txt tree | commitdiff
2018-09-22 Mathias Preinercmake: Working build infrastructure. tree | commitdiff
2018-09-22 Aina Niemetzcmake: .cpp generation done, .h generation not yet... tree | commitdiff
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. tree | commitdiff
2018-09-19 Andrew ReynoldsDecision strategy: incorporate arrays. (#2495) tree | commitdiff
2018-09-19 Andres NoetzliAdd rewrites for str.contains + str.replace/substr... tree | commitdiff
2018-09-19 Andrew ReynoldsDecision strategy: incorporate separation logic. (... tree | commitdiff
2018-09-19 Andrew ReynoldsAdd two rewrites for string contains character (#2492) tree | commitdiff
2018-09-19 Andrew Reynolds Refactor strings extended functions inferences (#2480) tree | commitdiff
2018-09-18 Andres NoetzliFix issue with str.idof in evaluator (#2493) tree | commitdiff
2018-09-18 Andrew ReynoldsDecision strategy: incorporate strings fmf. (#2485) tree | commitdiff
2018-09-18 Andrew ReynoldsMore aggressive caching of string skolems. (#2491) tree | commitdiff
2018-09-18 Andrew ReynoldsMove and rename sygus solver classes (#2488) tree | commitdiff
2018-09-18 Andrew ReynoldsClean remaining references to getNextDecisionRequest... tree | commitdiff
2018-09-18 Andrew ReynoldsImprovements and fixes for symmetry detection and break... tree | commitdiff
2018-09-17 Andrew ReynoldsMove inst_strategy_cbqi to inst_strategy_cegqi (#2477) tree | commitdiff
2018-09-17 Andrew ReynoldsDecision strategy: incorporate cegis unif (#2482) tree | commitdiff
2018-09-17 Andrew Reynolds Decision strategy: incorporate bounded integers (... tree | commitdiff
2018-09-17 Andrew ReynoldsDecision strategy: incorporate datatypes sygus solver... tree | commitdiff
2018-09-17 Andrew ReynoldsMore aggressive skolem caching for strings, document... tree | commitdiff
2018-09-17 Andrew ReynoldsMake strings model construction robust to lengths that... tree | commitdiff
2018-09-17 Andrew ReynoldsDecision strategy: incorporate UF with cardinality... tree | commitdiff
2018-09-17 Andrew ReynoldsDecision strategy: incorporate sygus feasible and sygus... tree | commitdiff
2018-09-15 Andres NoetzliRefactor how assertions are added to decision engine... tree | commitdiff
2018-09-14 Andrew ReynoldsAdd Skolem cache for strings, refactor length registrat... tree | commitdiff
2018-09-14 Andrew ReynoldsGeneralize CandidateRewriteDatabase to ExprMiner (... tree | commitdiff
2018-09-13 Haniel BarbosaUses information gain heuristic for building better... tree | commitdiff
2018-09-13 Andrew ReynoldsSimplify storing of transcendental function application... tree | commitdiff
2018-09-13 Andrew Reynolds Decision strategy: incorporate CEGQI (#2460) tree | commitdiff
2018-09-12 Andrew Reynolds Initial infrastructure for theory decision manager... tree | commitdiff
2018-09-12 Andrew ReynoldsFix for when strings process loop is disabled. (#2456) tree | commitdiff
2018-09-11 Andrew ReynoldsSupport model cores via option --produce-model-cores... tree | commitdiff
2018-09-11 Haniel Barbosafix (#2446) tree | commitdiff
2018-09-11 Haniel BarbosaUsing a single condition enumerator in sygus-unif ... tree | commitdiff
2018-09-10 Andrew ReynoldsSquash implementation of counterexample-guided instanti... tree | commitdiff
2018-09-10 Andres NoetzliAdd (str.replace (str.replace y w y) y z) rewrite ... tree | commitdiff
2018-09-07 Andrew Reynolds Make isClosedEnumerable a member of TypeNode (#2434) tree | commitdiff
2018-09-06 Andrew Reynolds Further simplify and fix initialization of ce guided... tree | commitdiff
2018-09-06 Andrew ReynoldsRefactor and document quantifiers variable elimination... tree | commitdiff
2018-09-06 Andrew ReynoldsMinor improvements to interface for rep set. (#2435) tree | commitdiff
2018-09-05 Andrew Reynolds More extended rewrites for strings equality (#2431) tree | commitdiff
2018-09-05 Andrew Reynolds Eliminate select over store in quantifier bodies ... tree | commitdiff
2018-09-05 Mathias PreinerUse std::uniqe_ptr for d_eq_infer to make Coverity... tree | commitdiff
2018-09-05 Andrew Reynolds Extended rewriter for string equalities (#2427) tree | commitdiff
2018-09-04 Andrew ReynoldsRemove redundant strings rewrite. (#2422) tree | commitdiff
2018-09-04 Andrew ReynoldsMinor improvements to theory model builder interface... tree | commitdiff
2018-09-04 Andrew ReynoldsMake quantifiers strategies exit immediately when in... tree | commitdiff
2018-09-04 Aina NiemetzTransfer ownership of learned literals from SMT engine... tree | commitdiff
2018-09-04 Andrew ReynoldsRefactor ceg conjecture initialization (#2411) tree | commitdiff
2018-08-31 Haniel BarbosaAllows SAT checks of repair const to have different... tree | commitdiff
2018-08-31 Andrew ReynoldsRefactor and document alpha equivalence. (#2402) tree | commitdiff
2018-08-30 Andres NoetzliUse useBland option in FCSimplexDecisionProcedure ... tree | commitdiff
2018-08-30 Andrew ReynoldsAdd regular expression elimination module (#2400) tree | commitdiff
2018-08-28 Andrew Reynolds Split term canonize utility to own file and document... tree | commitdiff
2018-08-28 Aina NiemetzReorder circuit propagator class. tree | commitdiff
2018-08-28 Aina NiemetzMove flag needsFinish from SMT engine to circuit propag... tree | commitdiff
2018-08-28 Andrew Reynolds Fix for get constraints method in fmf-fun (#2399) tree | commitdiff
2018-08-28 Andrew ReynoldsSolve equalities between Boolean variables in presolve... tree | commitdiff
2018-08-28 Andres NoetzliRemove throw specifiers in FP type checker (#2392) tree | commitdiff
2018-08-28 Andres NoetzliRemove dead code in fp_converter (#2388) tree | commitdiff
2018-08-28 Andrew ReynoldsFix sort inference for quantified variables of interpre... tree | commitdiff
2018-08-28 Andrew Reynolds Address more coverity warnings (#2394) tree | commitdiff
2018-08-28 Andrew ReynoldsFix warning in sygus io. (#2391) tree | commitdiff
2018-08-28 Andres NoetzliRemove dead code in evaluator (#2389) tree | commitdiff
2018-08-28 Andrew ReynoldsRefactor extended rewriter, move rewrites to aggressive... tree | commitdiff
2018-08-27 Mathias PreinerUse std:unique_ptr instead of raw pointers in theory... tree | commitdiff
2018-08-26 Andres NoetzliUse uniform length limit for String constants (#2381) tree | commitdiff
2018-08-26 Andrew ReynoldsFix unsigned integer type issues in strings (#2380) tree | commitdiff
2018-08-26 Andres NoetzliRefactor unconstrained simplification pass (#2374) tree | commitdiff
2018-08-25 yoni206Refactor quantifier macros preprocessing pass (#1840) tree | commitdiff
2018-08-25 Andrew ReynoldsClean up quantifiers engine initialization. (#2371) tree | commitdiff
2018-08-24 Andrew Reynolds Fix more simple coverity warnings (#2372) tree | commitdiff
2018-08-24 Andres NoetzliAdd tests that enumerate and verify rewrite rules ... tree | commitdiff
2018-08-24 Andrew Reynolds Do not print internally generated datatypes in externa... tree | commitdiff
2018-08-23 Andrew Reynolds Fixing some coverity warnings (#2357) tree | commitdiff
2018-08-23 Aina NiemetzRefactor ITE simplification preprocessing pass. (#2360) tree | commitdiff
2018-08-23 yoni206global-negate preprocessing pass (#2317) tree | commitdiff
2018-08-22 Andrew Reynolds More unused code elimination (#2358) tree | commitdiff
2018-08-22 Tim KingWrapping TheorySetsPrivate in a unique_ptr. (#2356) tree | commitdiff
2018-08-22 Andrew ReynoldsFix invalid iterator comparisons (#2349) tree | commitdiff
2018-08-21 Tim KingAdd constexpr annotations to help coverity understand... tree | commitdiff
2018-08-21 Andrew ReynoldsUse cbqi-full for sygus (#2346) tree | commitdiff
2018-08-21 Andrew ReynoldsMore unused code elimination (#2339) tree | commitdiff
2018-08-20 Andrew Reynolds Remove support for prototype (non-sygus) synthesis... tree | commitdiff
2018-08-20 Andrew ReynoldsMinor improvements to the interface for sygus sampler... tree | commitdiff
2018-08-20 Andrew Reynolds Make sygus inference a preprocessing pass (#2334) tree | commitdiff
2018-08-17 Andrew ReynoldsRemove support for flipDecision (#2319) tree | commitdiff
2018-08-17 Andrew ReynoldsRemove miscellaneous unused code (#2333) tree | commitdiff
2018-08-17 Andrew Reynolds Fix spurious warning in sort inference (#2331) tree | commitdiff
2018-08-17 Andrew Reynolds Fix arithmetic division by zero in sygus repair consta... tree | commitdiff
2018-08-17 Andrew Reynolds Eliminate partial operators in sygus grammar normaliza... tree | commitdiff
2018-08-17 Tim King Initialize inputAssertions only when proofRecipe is... tree | commitdiff
2018-08-17 Haniel BarbosaAdding support for bitvector SyGuS problems without... tree | commitdiff
2018-08-17 Tim KingRemoving coverity warnings from theory_sep.cpp (#2320) tree | commitdiff
2018-08-16 Andres NoetzliMove node algorithms to separate file (#2311) tree | commitdiff
2018-08-16 Andrew ReynoldsMinor fixes and improvement for sygus to builtin. ... tree | commitdiff
2018-08-16 Tim KingSwitching an Assert to a CVC4_CHECK to test if it resol... tree | commitdiff
2018-08-15 Andres NoetzliRemove unused tuple classes (#2313) tree | commitdiff
2018-08-15 Andrew ReynoldsMake sort inference a preprocessing pass (#2309) tree | commitdiff
2018-08-15 Andres NoetzliRemove unused declaration (#2310) tree | commitdiff
next