cvc5.git
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...
2018-08-28 Andrew Reynolds Address more coverity warnings (#2394)
2018-08-28 Andrew ReynoldsFix warning in sygus io. (#2391)
2018-08-28 Andres NoetzliRemove dead code in evaluator (#2389)
2018-08-28 Andrew ReynoldsRefactor extended rewriter, move rewrites to aggressive...
2018-08-28 Aina NiemetzNew C++ API: Fix isDefinedKind() to not be ambigious...
2018-08-27 Mathias PreinerUse std:unique_ptr instead of raw pointers in theory...
2018-08-27 Andres NoetzliResolution proof: separate printing from proof (#1964)
2018-08-27 Andrew ReynoldsMake division chainable in the smt2 parser (#2367)
2018-08-27 Andres NoetzliRemove Coverity build from Travis (#2373)
2018-08-26 Andres NoetzliUse uniform length limit for String constants (#2381)
2018-08-26 Andrew ReynoldsFix unsigned integer type issues in strings (#2380)
2018-08-26 Andres NoetzliRefactor unconstrained simplification pass (#2374)
2018-08-25 yoni206Refactor quantifier macros preprocessing pass (#1840)
2018-08-25 Haniel BarbosaRefactor nlExtPurify preprocessing pass (#1963)
2018-08-25 Andrew ReynoldsClean up quantifiers engine initialization. (#2371)
2018-08-24 Andrew Reynolds Fix more simple coverity warnings (#2372)
2018-08-24 Andrew Reynolds Remove spurious disabling of cbqi-all (#2368)
2018-08-24 Andres NoetzliAdd tests that enumerate and verify rewrite rules ...
2018-08-24 Andrew Reynolds Do not print internally generated datatypes in externa...
2018-08-24 Aina NiemetzNew C++ API: Add checks for kind arguments. (#2369)
2018-08-23 Andres NoetzliAdd missing overrides in unit tests (#2362)
2018-08-23 Tim KingReplacing allocatedInCMM and d_noTrash with false every...
2018-08-23 Haniel BarbosaMakes the filename be set in the SMT engine by default...
2018-08-23 Andrew Reynolds Fixing some coverity warnings (#2357)
2018-08-23 Andrew ReynoldsFix regression requiring proof build. (#2364)
2018-08-23 Aina NiemetzRefactor ITE simplification preprocessing pass. (#2360)
2018-08-23 Andres NoetzliUse "filename" instead of "name" in SmtEngine::setInfo...
2018-08-23 yoni206global-negate preprocessing pass (#2317)
2018-08-23 Andrew ReynoldsMore regressions that increase coverage (#2354)
2018-08-22 Andrew Reynolds More unused code elimination (#2358)
2018-08-22 yoni206Generating less consistency lemmas in bv-ackermann...
2018-08-22 Tim KingWrapping TheorySetsPrivate in a unique_ptr. (#2356)
2018-08-22 Andrew ReynoldsFix option for real2int regression. (#2353)
2018-08-22 Haniel BarbosaAdds regression test for automatic generation of SyGuS...
2018-08-22 Andrew ReynoldsFix invalid iterator comparisons (#2349)
2018-08-22 Andrew Reynolds Fix processing of nested Variable construct in sygus...
2018-08-21 Tim KingRemoving unused bool members in command.cpp. Also initi...
2018-08-21 Andrew ReynoldsWarn and enable quantifiers when using sygus + logics...
2018-08-21 Haniel BarbosaMakes the new row propagation system default (#2335)
2018-08-21 Mathias PreinerMove d_realAssertionsEnd from SmtEnginePrivate to Asser...
2018-08-21 Tim KingAdd constexpr annotations to help coverity understand...
2018-08-21 Andrew ReynoldsUse cbqi-full for sygus (#2346)
2018-08-21 Andres NoetzliRemove support for *.expect files in regressions (...
2018-08-21 Aina NiemetzFix initialization of d_smt in ValidityChecker for...
2018-08-21 Aina NiemetzRemove disabled system test cvc3_george. (#2342)
2018-08-21 Andrew ReynoldsMore unused code elimination (#2339)
2018-08-20 Andrew Reynolds Remove support for prototype (non-sygus) synthesis...
2018-08-20 Andrew ReynoldsAdd regressions that increase coverage (#2337)
2018-08-20 Andrew ReynoldsMinor improvements to the interface for sygus sampler...
2018-08-20 Andrew Reynolds Make sygus inference a preprocessing pass (#2334)
2018-08-18 Aina Niemetzrun-regress script: Exit with exit code > 0 on failure...
2018-08-17 Andrew ReynoldsRemove support for flipDecision (#2319)
2018-08-17 Andrew ReynoldsRemove miscellaneous unused code (#2333)
2018-08-17 Andrew Reynolds Add sygus stream regressions (#2330)
2018-08-17 Andrew ReynoldsSplit sygus grammar to its own ANTLR grammar (#2307)
2018-08-17 Andrew Reynolds Fix spurious warning in sort inference (#2331)
next