cvc5.git
2018-09-22 Aina Niemetzcmake: Fixed compiler flag macros.
2018-09-22 Mathias Preinercmake: Add module finder for LFSC.
2018-09-22 Mathias Preinercmake: Add module finder for CaDiCaL.
2018-09-22 Mathias Preinercmake: Add module finder for CryptoMiniSat.
2018-09-22 Mathias Preinercmake: Add module finder for SymFPU.
2018-09-22 Mathias Preinercmake: Add module finder for CLN.
2018-09-22 Mathias Preinercmake: Add libsignatures for proofs.
2018-09-22 Mathias Preinercmake: Remove unused CMakeLists.txt
2018-09-22 Aina Niemetzcmake: Generate cvc4autoconfig.h (options currently...
2018-09-22 Aina Niemetzcmake: Added missing dependency for src/util
2018-09-22 Mathias Preinercmake: Working build infrastructure.
2018-09-22 Mathias Preinercmake: Antlr parser generation done.
2018-09-22 Aina Niemetzcmake: Generate trace and debug tags
2018-09-22 Aina Niemetzcmake: .cpp generation done, .h generation not yet...
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure.
2018-09-19 Andrew ReynoldsDecision strategy: incorporate arrays. (#2495)
2018-09-19 Andres NoetzliAdd rewrites for str.contains + str.replace/substr...
2018-09-19 Andrew ReynoldsDecision strategy: incorporate separation logic. (...
2018-09-19 Andrew ReynoldsAdd two rewrites for string contains character (#2492)
2018-09-19 Andrew Reynolds Refactor strings extended functions inferences (#2480)
2018-09-19 Aina NiemetzNew C++ API: Introduce new macro and exception for...
2018-09-18 Andres NoetzliFix issue with str.idof in evaluator (#2493)
2018-09-18 Andrew ReynoldsDecision strategy: incorporate strings fmf. (#2485)
2018-09-18 Andrew ReynoldsMore aggressive caching of string skolems. (#2491)
2018-09-18 Andrew ReynoldsMove and rename sygus solver classes (#2488)
2018-09-18 Haniel Barbosafix assertion error (#2487)
2018-09-18 Andrew ReynoldsClean remaining references to getNextDecisionRequest...
2018-09-18 Andrew ReynoldsImprovements and fixes for symmetry detection and break...
2018-09-17 Andrew ReynoldsMove inst_strategy_cbqi to inst_strategy_cegqi (#2477)
2018-09-17 Andrew ReynoldsDecision strategy: incorporate cegis unif (#2482)
2018-09-17 Andrew Reynolds Decision strategy: incorporate bounded integers (...
2018-09-17 Andrew ReynoldsDecision strategy: incorporate datatypes sygus solver...
2018-09-17 Andrew ReynoldsMore aggressive skolem caching for strings, document...
2018-09-17 Andrew ReynoldsMake strings model construction robust to lengths that...
2018-09-17 Andres NoetzliFollow redirects with cURL in contrib/get* scripts...
2018-09-17 Andres NoetzliRemove broken dumping support from portfolio build...
2018-09-17 Andres NoetzliRemove unnecessary tracing from preprocessing (#2472)
2018-09-17 Andrew ReynoldsDecision strategy: incorporate UF with cardinality...
2018-09-17 Andrew ReynoldsDecision strategy: incorporate sygus feasible and sygus...
2018-09-15 Andres NoetzliRefactor how assertions are added to decision engine...
2018-09-14 Andrew ReynoldsAdd Skolem cache for strings, refactor length registrat...
2018-09-14 Andrew ReynoldsGeneralize CandidateRewriteDatabase to ExprMiner (...
2018-09-13 Mathias PreinerFix #include for minisat headers in bvminisat. (#2463)
2018-09-13 Haniel BarbosaUses information gain heuristic for building better...
2018-09-13 Andrew ReynoldsSimplify storing of transcendental function application...
2018-09-13 Andrew Reynolds Decision strategy: incorporate CEGQI (#2460)
2018-09-12 Aina NiemetzNew C++ API: Try to fix (false positive) Coverity warni...
2018-09-12 Aina NiemetzExamples: Remove obsolete flag CVC4_MAKE_EXAMPLES....
2018-09-12 Andrew Reynolds Initial infrastructure for theory decision manager...
2018-09-12 Andrew ReynoldsFix for when strings process loop is disabled. (#2456)
2018-09-11 Aina NiemetzFixe compiler warning in line_buffer.cpp. (#2453)
2018-09-11 Andrew ReynoldsSupport model cores via option --produce-model-cores...
2018-09-11 yoni206Avoid calling size() every iteration (#2450)
2018-09-11 Andrew ReynoldsFix global negate (#2449)
2018-09-11 Haniel Barbosafix (#2446)
2018-09-11 Andres NoetzliSet NodeManager to nullptr when exporting vars (#2445)
2018-09-11 Haniel BarbosaUsing a single condition enumerator in sygus-unif ...
2018-09-11 Aina NiemetzRefactor non-clausal simplify preprocessing pass. ...
2018-09-10 Andrew ReynoldsSquash implementation of counterexample-guided instanti...
2018-09-10 Andres NoetzliAdd (str.replace (str.replace y w y) y z) rewrite ...
2018-09-07 Mathias PreinerReplace boost::integer_traits with std::numeric_limits...
2018-09-07 Mathias PreinerRemove clock_gettime() replacement for macOS. (#2436)
2018-09-07 Andrew Reynolds Make isClosedEnumerable a member of TypeNode (#2434)
2018-09-06 Andrew Reynolds Further simplify and fix initialization of ce guided...
2018-09-06 Andrew ReynoldsRefactor and document quantifiers variable elimination...
2018-09-06 Andrew ReynoldsMinor improvements to interface for rep set. (#2435)
2018-09-05 Andrew Reynolds More extended rewrites for strings equality (#2431)
2018-09-05 Andrew Reynolds Eliminate select over store in quantifier bodies ...
2018-09-05 Mathias PreinerUse std::uniqe_ptr for d_eq_infer to make Coverity...
2018-09-05 Andrew ReynoldsRemove printing support for sygus enumeration types...
2018-09-05 Andrew ReynoldsFiner-grained inference of substitutions in incremental...
2018-09-05 Andres NoetzliAdd regex grammar to rewriter verification tests (...
2018-09-05 Andrew Reynolds Extended rewriter for string equalities (#2427)
2018-09-05 Mathias PreinerAdd HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)
2018-09-04 Andrew ReynoldsRemove redundant strings rewrite. (#2422)
2018-09-04 Andres NoetzliUpdate INSTALL instructions (#2420)
2018-09-04 Andres NoetzliRemove CVC3 compatibility layer (#2418)
2018-09-04 Andres NoetzliRemove unused options file (#2413)
2018-09-04 Andrew ReynoldsMinor improvements to theory model builder interface...
2018-09-04 Andrew ReynoldsMake quantifiers strategies exit immediately when in...
2018-09-04 Aina NiemetzTransfer ownership of learned literals from SMT engine...
2018-09-04 Aina NiemetzFix merge mishap of #2359.
2018-09-04 Andrew ReynoldsRefactor ceg conjecture initialization (#2411)
2018-08-31 Haniel BarbosaAllows SAT checks of repair const to have different...
2018-08-31 Andrew ReynoldsRefactor and document alpha equivalence. (#2402)
2018-08-31 Haniel BarbosaFix export of bound variables (#2409)
2018-08-30 Mathias PreinerRefactor theory preprocess into preprocessing pass...
2018-08-30 Andres NoetzliUse useBland option in FCSimplexDecisionProcedure ...
2018-08-30 Andrew ReynoldsAdd regular expression elimination module (#2400)
2018-08-29 Mathias PreinerRefactor MipLibTrick preprocessing pass. (#2359)
2018-08-29 Tim KingForcing attribute_internals.h to use uint64_t's for...
2018-08-29 Haniel Barbosafix bv total ops printing (#2365)
2018-08-28 Andrew Reynolds Split term canonize utility to own file and document...
2018-08-28 Aina NiemetzReorder circuit propagator class.
2018-08-28 Aina NiemetzMove flag needsFinish from SMT engine to circuit propag...
2018-08-28 Andrew Reynolds Fix for get constraints method in fmf-fun (#2399)
2018-08-28 Andrew ReynoldsSolve equalities between Boolean variables in presolve...
2018-08-28 Andres NoetzliRemove throw specifiers in FP type checker (#2392)
2018-08-28 Andres NoetzliRemove dead code in fp_converter (#2388)
2018-08-28 Andrew ReynoldsFix sort inference for quantified variables of interpre...
next